Re: [isabelle] I need an ML function to get the THY path and filename



Makarius,

First, it seems to me that ML is a decent scripting language. There's val and fun, and those two are easy to use for some unsophisticated scripting, as usual. And poly.exe has a --script command line option.

Second, I think I have the things I need from all of this: "Isabelle_System.bash" and "bash_output", "thy_decl" for safe file operations, the outer syntax example for bash, and just clicking on cntl-hover links to take me to the signatures in file.ML, etc.. Just looking at the signatures, I've found the conversion functions I've needed.

Third, the continuous output can result in all those extra files being created, but turning continuous checking on and off is easy.

Fourth, the tricky part is getting the file directory change to stick. I use this "ML{*File.cd (Thy_Load.master_directory @{theory});*}", but sometimes I still end up working in the wrong folder.

On 14-04-04 07:57, Makarius wrote:
I ran the ideas through this filter: "Does any of this give me something over and above what I already have, like Windows Explorer for file management?"

No. One would have to make more substantial reforms of stateless operating systems to fit it into the PIDE model and get real benefits from it. (Apple's Time Machine and the ZFS file-system are actually moving a bit in that direction.)

Was that a yes I heard? Call it the "language assistant". I need to learn ML, Perl, the many facets of pipes and redirection, and Perl's flavor of regular expressions. The "language assistant" is already helping me, and it's because of its instantaneous output.

Working with regular expressions and piping takes a lot of experimentation to figure out what works, and this is like a huge plugin to get feedback on what works and doesn't work.

I've looked through this briefly. Note that the double-quoted strings of Parse.name can be avoided by using Parse.text: that category also allows "verbatim" tokens of form {* ... *}.

That helped a lot.

There's a free book "Higher-Order Perl", http://hop.perl.plover.com/, and Perl 6 is supposed to have some functional programming features.

I show a screen shot of some of the usual Unix commands I've defined. Files are what tie all the commands together.

Regards,
GB



Attachment: i140331c__Bash_inner_outer.png
Description: PNG image

theory i140331c__Bash_inner_outer
imports Complex_Main 
keywords 
  "PWD" "CD" "cp_ls" "cat" "cat_ls" "bash" "bash_ls" "obash" "echo_ls"
  "lsls" "lsal" "perle" "perle_ls" "perleX" "rm_ls" "touch_ls" :: thy_decl
begin

(******************************************************************************)
(* ML BASH COMMANDS ***********************************************************)
(******************************************************************************)

ML{*fun bash cmd = Isabelle_System.bash cmd*}
ML{*fun bash_ls cmd = bash (cmd ^ "; ls -al; pwd;")*}
ML{*fun obash cmd = fst(Isabelle_System.bash_output cmd)*}
ML{*fun cat cmd = bash ("cat " ^ cmd)*}
ML{*fun ocat cmd = obash ("cat " ^ cmd)*}
ML{*fun cd_ls cmd = bash ("cd " ^ cmd ^ "; ls -al; pwd;")*}
ML{*fun cp_ls cmd = bash ("cp " ^ cmd ^ "; ls -al; pwd;")*}
ML{*fun echo cmd = bash ("echo " ^ (cmd))*}
ML{*fun oecho cmd = obash ("echo " ^ cmd)*}
ML{*fun lsal cmd = bash ("ls -al " ^ cmd ^ "; pwd")*}
ML{*fun rm_ls cmd = bash ("rm " ^ cmd ^ "; ls -al; pwd;")*}
ML{*fun touch_ls cmd = bash ("touch " ^ cmd ^ "; ls -al; pwd;")*}
ML{*fun perle cmd = bash ("perl -e " ^ cmd)*}
ML{*fun operle cmd = obash ("perl -e " ^ cmd)*}

(******************************************************************************)
(* OUTER SYNTAX BASH COMMANDS *************************************************)
(******************************************************************************)

ML {*
structure CD = Theory_Data
(
  type T = Path.T;
  val empty = Path.current;
  fun extend _ = empty;
  fun merge _ = empty;
)
fun pwd thy = writeln (Path.print (CD.get thy));
(*PWD*)
Outer_Syntax.improper_command @{command_spec "PWD"}
  "print current working directory of theory context"
  (Scan.succeed (Toplevel.keep (fn st => pwd (Toplevel.theory_of st))));
(*CD*)
Outer_Syntax.improper_command @{command_spec "CD"}
  "change current working directory within theory"
  (Parse.path >> (fn name => Toplevel.theory 
    (CD.put (Path.expand (Path.explode name)) #> tap pwd)));
*}

ML {*
(*bash*)
Outer_Syntax.improper_command @{command_spec "bash"}
  "invoke GNU Bourne Again Shell command-line, relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash ("cd " ^ File.shell_path cd ^ "; " ^ cmd)
    in writeln (string_of_int rc) end  )));
(*bash_ls*)
Outer_Syntax.improper_command @{command_spec "bash_ls"}
  "invoke GNU Bourne Again Shell command-line, relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ "; " ^ cmd ^ "; ls -al; pwd;")
    in writeln (string_of_int rc) end  )));
(*obash*)      
Outer_Syntax.improper_command @{command_spec "obash"}
  "invoke GNU Bourne Again Shell command-line, relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash_output 
        ("cd " ^ File.shell_path cd ^ "; " ^ cmd)
    in writeln (fst rc) end  )));
(*cat*)
Outer_Syntax.improper_command @{command_spec "cat"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";cat " ^ cmd)
    in writeln (string_of_int rc) end)));
(*cat_ls*)
Outer_Syntax.improper_command @{command_spec "cat_ls"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";cat " ^ cmd ^ ";ls -al ;pwd")
    in writeln (string_of_int rc) end)));
(*cp_ls*)
Outer_Syntax.improper_command @{command_spec "cp_ls"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";cp " ^ cmd ^ ";ls -al ;pwd")
    in writeln (string_of_int rc) end)));
(*echo_ls*)
Outer_Syntax.improper_command @{command_spec "echo_ls"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";echo " ^ cmd ^ "; ls -al; pwd;")
    in writeln (string_of_int rc) end)));
(*perle*)
Outer_Syntax.improper_command @{command_spec "perle"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";perl -e " ^ cmd)
    in writeln (string_of_int rc) end)));      
(*perle_ls*)
Outer_Syntax.improper_command @{command_spec "perle_ls"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";perl -e " ^ cmd ^ ";ls -al; pwd;")
    in writeln (string_of_int rc) end)));      
(*lsls*)
Outer_Syntax.improper_command @{command_spec "lsls"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";ls " ^ cmd ^ ";pwd")
    in writeln (string_of_int rc) end)));
(*lsal*)
Outer_Syntax.improper_command @{command_spec "lsal"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";ls -al " ^ cmd ^ ";pwd")
    in writeln (string_of_int rc) end)));
(*rm_ls*)
Outer_Syntax.improper_command @{command_spec "rm_ls"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";rm " ^ cmd ^ "; ls -al; pwd;")
    in writeln (string_of_int rc) end)));
(*touch_ls*)
Outer_Syntax.improper_command @{command_spec "touch_ls"}
  "invoke Isabelle_System.bash 'bash perl -e', relative to working\
   \directory of theory"
  (Parse.text >> (fn cmd => Toplevel.keep (fn st =>
    let
      val cd = CD.get (Toplevel.theory_of st);
      val rc = Isabelle_System.bash 
        ("cd " ^ File.shell_path cd ^ ";touch " ^ cmd ^ "; ls -al; pwd;")
    in writeln (string_of_int rc) end)));
*}

(******************************************************************************)
(* EXAMPLES *******************************************************************)
(******************************************************************************)

ML{*File.cd (Thy_Load.master_directory @{theory});*} lsal""

perle_ls{*' 
  $first_name = "Melanie"; 
  $last_name = "Quigley";
  $salary = 125000.00;
  print $first_name, " ", $last_name,  " ", $salary '\
  > TEST_perle_ls.txt *}

cat "TEST_perle_ls.txt"

cat_ls "TEST_perle_ls.txt | perl -ne 'print uc' > TEST.txt"

cat "TEST.txt"

cp_ls "TEST.txt TEST.bak"
echo_ls{* " -----TEST TEXT-----" | cat TEST.txt - > TEST2.txt *}
cat_ls "TEST2.txt"

touch_ls "BASH_TOUCH_TEST.txt"

ML{*
  val TEST2_in = ocat "TEST2.txt"
  fun cat_string n = case (n)
   of 0 => TEST2_in
    | n => TEST2_in ^ cat_string (n - 1);

  echo ( "'" ^ (cat_string 5) ^ "' > TEST3.txt" );
  oecho ( "'" ^ (cat_string 20) ^ "' | perl -ne 'print lc' > TEST4.txt" );
*}
cat_ls "TEST3.txt"
cat_ls "TEST4.txt"  

(******************************************************************************)
end
(******************************************************************************)








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.