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

On 14-04-01 14:04, Makarius wrote:
Of course, unpredictable or really bad things will happen, when you modify the file system in any of these bash commands.

Thanks for the heads up, a casual comment that belies the real message, "WARNING! YOU MAY DESTROY YOUR FILE SYSTEM, FOOL!"

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?"

At first, my mind was empty as to any real needs I have for using your outer syntax commands CD, PWD, and bash, so I felt like I wasted your time.

I then modified CD imperfectly to get CDH, to take me to my theory folder, "Thy_Load.master_directory @{theory}". After that, I started getting lots of ideas.

One big use would be to create a THY that contains information I've sorted through and grepped on in $ISABELLE_HOME/src/HOL. If I put 8 hours of work trying to understand what the sources do, I can have a document reflects some of what I've done, and which I can go back to if I need to refresh my mind. If I've done the right kind of greps, I can just leave the commands there. It's an efficient use of THY space, with information on demand in the output panel.

There is something bigger here, though, and that's trying to combine Isar, ML, and Perl for scripting. Consider the following 3 descriptions;

(1) One-liner Perl commands which are invoked using bash with the "-e" option, where the one-liners can contain as many Perl commands as I want. Perl is important because
  (a) it requires no setup, such as environment variables or installs,
  (b) it has a global replace command in its regular expressions,
(c) it has the -e, -n, and -p command line options, ( (c) and its regular expressions don't need to be compiled like with some languages.

(2) Isar as a scripting language to execute a series of Perl one-liner bash commands. The output can't be processed by Isar, so the output would be for info, or to see what affect my regular expressions have on a piped input string to the regular expression.

(3) ML as a scripting language which uses Perl one-liner bash commands, the output which can be processed with ML as a full-blown programming language.

Why would I want to work like this? Because I'm totally fixated on trying not to invest large amounts of time into learning languages which do not build on what I'm doing in Isabelle. If I'm in another IDE working on Perl or Scala, then I'm not in Isar. If I'm executing Perl one-liners with Isar or ML, then I'm in Isar.

Take Perl. I don't need all the power of Perl. What I need from Perl is its regular expressions, for doing search and replaces on a file.

I can suffer through ML not being the perfect language for scripting, and I think any suffering like that will make me a better ML programmer, just because I'm using ML. Well, the context is that I have Perl to take up the slack for regular expressions.

That's the idea I'm pursuing.

I can't know right now whether lots of calls through bash will work. If not, I could resort to calling some Perl scripts.

I finally found a good, commercially produced book for Perl on the web.

There are lots of good Perl books, but I need a free, good one for some web stuff I may put up.

I attach a THY, along with the one you sent me, to be complete. I make my requests in the THY, and there are 8 comment headings which give an overview of what each section does.

The last thing I did was define, as a ML string, a 6 line Perl example from the free book. The example contains a sub-routine, and I have it formatted across multiple lines. The free book, published in 1996, is here:

Thanks for your help,

theory Bash
imports Pure
keywords "CD" :: thy_decl
  and "PWD" "bash" :: diag

ML {*
structure CD = Theory_Data
  type T = Path.T;
  val empty = Path.current;
  fun extend _ = empty;
  fun merge _ = empty;

ML {*
  fun pwd thy = writeln (Path.print (CD.get thy));

  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))));

  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)));

  Outer_Syntax.improper_command @{command_spec "bash"}
    "invoke GNU Bourne Again Shell command-line, relatively to working directory of theory"
    ( >> (fn cmd =>
      Toplevel.keep (fn st =>
          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)));

theory Bash_tests
imports Complex_Main "Bash"
keywords "CDH" :: thy_decl

(** The home folder for a theory is the folder it's in. ***********************)
  (*I couldn't figure out how to get rid of it have to take an argument.*)
  ML {*
    Outer_Syntax.improper_command @{command_spec "CDH"}
      "change to the theory working directory"
      (Parse.path >> (fn _ =>
        Toplevel.theory (CD.put (Thy_Load.master_directory @{theory}) #> tap pwd)));

(** Possible wants for outer syntax, where input arguments are strings. *******)

  (A1) A "basho" for Isabelle_System.bash_output, to see what the string looks 
  (A2) THOME, or whatever you think it should be named, for the theory home, a
       string alias for "Thy_Load.master_directory @{theory}", to be used with 
       commands such as "ls".
  (B1) The Isar ability to define strings for use in bash commands.
  (B2) An Isar concat operator for strings, for concatenating string aliases 
  (B3) The ability to use `bash {*...*}` instead of only `bash "..."`, to keep
       from having to escape double quotes.
  The safe file system operations:
  (C1) File.rm
  (C2) File.copy
  (C3) Isabelle_System.mkdir
  (C4) Isabelle_System.copy_dir

(** I use CDH to take me to my theory home. I can use "cat", "env", and get
    some help for commands. I have my output panel taking up the full right
    hand side, so I see a lot of the printout.**)

  CDH "" (*Takes me to this theory's folder, where I'd be working a lot.*)
  bash "ls -al"
  bash "cat Bash_tests.thy"
  bash "perl -h"
  bash "grep --help"
  bash "env"
  bash "ls -l $ISABELLE_HOME/src/HOL"
(** Piping echo strings. ************************)
  bash "echo 'stufferama' | cat"
  bash "echo heeeeeeelllo | sed 's/\\(.\\)\\1\\+/\\1/g'" 
(** Piping echo strings to Perl one-liners with -e, and -e multiple times. ****)
  (*It prints out spaces before "I", because I have it indented.*)
  bash "
    echo 'Amigo, how about this Isar? Is that tower in France still leaning? 
          I assume it is.' |
    perl -ne 'print uc;' "
  bash "perl -e 'print \"stuff1\";' -e 'print \" stuff2\"'"
  bash "perl -e '
    print \"hello world1!\\n\"; 
    print \"hello world2!\" ' "
(** Using ML bash and (perl >> bash_output >> writeln). ***********************)
  (*Using the ML line continuation, I micromanage the spaces.*)
  ML{*Isabelle_System.bash "\
   \echo 'Amigo, how about this Isar? Is that tower in France still leaning? \ 
         \I assume it is. Adios, amigo. Mucho bueno, muy, muy bueno. It is\
         \todos bueno.'\
  \|perl -ne 'print uc;'" *}

  ML{*val perl_cmd_str = "'\
  \print \"stuff1\\n\";\
  \print \"stuff2\\n\";\
  \print \"stuff3\\n\";\
  \print \"stuff4\\n\";\
  \print \"stuff5\\n\";\
  \print \"stuff6\\n\";\
  \print \"stuff7\\n\";\
  ML{*val perl_out = Isabelle_System.bash_output ("perl -e " ^ perl_cmd_str) *}
  ML{*writeln (fst perl_out)*}
  (*Perl by Example Listing 5.1,*)
  ML{*val perl5_by_example_5_1 = "perl -e '\
  \$areaOfFirstCircle = areaOfCircle(5);\
  \sub areaOfCircle {\
  \    $radius = $_[0];\
  \    return(3.1415 * ($radius ** 2));\
  ML{*Isabelle_System.bash perl5_by_example_5_1*}

(** OS.FileSys: the way to safely create and delete files? ********************)

  (* *)

(** Inner and Outer CD seem to work independent. **********************)

  (*What I can do with outer syntax, I figure I want to be able to do with
    inner syntax in a ML{*...*}, as a data processing tool for ML programs.*)

  ML{* (Thy_Load.master_directory @{theory})*}
  CD "~~/src/HOL"
  bash "ls -al"
  ML{*Isabelle_System.bash "ls -al"*}
  ML{* (Path.explode "~/.isabelle/Isabelle2013-2/jedit")*}
  CD "~~/src/HOL/Algebra"
  bash "ls -al"
  ML{*Isabelle_System.bash "ls -al"*}

(** M.WENZEL'S ORIGINAL EXAMPLES **********************************************)

  CD "~"
  bash "ls -al"
  CD "~~"
  bash "ls -al"
  bash "ls -al"


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