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



On 14-03-31 14:42, Makarius wrote:
Use Isabelle_System.bash or Isabelle_System.bash_output instead. (Isabelle/Scala provides similar operations.)
On 14-03-31 14:36, Makarius wrote:
This is how to access the master directory in an ad-hoc example: ML {* Thy_Load.master_directory @{theory} *}

This is how to get... ML {* Context.theory_name @{theory} *}

Makarius, thanks for the detailed explanation. Two big solutions today. Your info on commands to help keep me internal to the THY, which tied into finally getting a small example of how to go from HOL nat to ML int, to do concrete computations.

The key word is "internal". When the PIDE is powered up, the goal is to stay working internal to a THY and the related THY and ML files, as much as possible. I click on a cntl-hover link to get me files. I access Unix essentials in the THY, viewing results in the output panel, not having to resort to the Console, which will allow me to create a history of commands. Occasionally, I'll have to execute a macro to build something.

You have surely noticed already that export_code... it leaves a dirty trace of file-name prefixes in your directory.

It is a game, with a rule. If I keep the PIDE in error while typing the file name, until the closing brace, I win. If I don't, I lose, and I have to delete 5 or 6 files.

It ends up not being a problem. I'll have one export_code command at the bottom, or in an appendix THY. The output file will be fixed. I'll add functions to it as I need to, and do my calculations down there. With code export, everything that's needed gets output for every command, so I'd generally not want all that duplication.

You can probably avoid all these complications with files, if you use the generated ML code directly... via the @{code}... It is also possible to pass around ML sources...

I'll remember that I can pass around sources, but getting into the details takes more knowledge. If I can use the forthcoming SML_file command to import what I exported, writing function based on that will show that the code can be used external to Isabelle.

...In that respect Scala is closer to Perl, e.g. it also supports nice pattern matching with regexps.

Learning Scala is the one thing that would increase my economic value, but with Scala, Java, and the JVM, it's near all encompassing. With any library I think about wanting to create, I start thinking about turning it into a huge application with Scala, when all I need to do is a few perfomance checks. Maybe I'll delete the Eclipse Scala IDE, and limit my options. If I could limit the amount of effort I put into it, it might work out.

*Concrete Nats, I Got 'Em; It's Hard Until You Figure It Out, Then It's Easy, Unless It Ends Up Being Harder Than You Thought Down the Road*

It's not obvious at all how one goes from proving things about nat in the proof assistant, to using those things concretely in a programming language. I had assumed too much about the code generator, because when I finally got around to looking at what I exported a while back, nat, int, and rat were just as abstract in the exported code as in the THY.

It's premature to engage in prodigious thanks to people, but if I dropped out today, all these things are and will be useful to other people.

Thanks to Brian Huffman for clarifying how to use the 5 Library/Code_XXXX.thy files. Listed in those files is Stefan Berghofer and Florian Haftmann, so thanks to them. Andreas Lochbihler is involved with code generation, so thanks to Andreas. Makarius Wenzel points out the work of David Mathews for Poly/ML, so thanks to David Mathews, because speed and performance are huge.

Thanks to the French for supporting Makarius Wenzel, to the British for supporting Larry Paulson and the HOL4 group, to the Germans for supporting Tobias Nipkow the big group he leads. Thanks to the Australians for supporting NICTA.

The way it works with credit is that everyone gets too much credit, or way too little.

As to the Americans, who are mostly absent from the scene in regards to proof assistants that can cater to the masses, thanks to them for staying loyal to their 5mm mechanical pencils. It's just more opportunity for the little guy, in the USA.

I attach a screenshot and THY to show I'm one, small step closer to the end result.

Regards,
GB






Attachment: i140331b__nat2x_to_code.png
Description: PNG image

theory i140331b__nat2x_to_code
imports Complex_Main  "~~/src/HOL/Library/Code_Target_Nat"
begin
(*They say it's just theoretical? No, no, no. Not at all. The ML big ints are
  in the house, are they not? Let no man or woman offend my constructivist 
  sensibilities, by suggesting I'm not doing concrete mathematics, all the
  time, except when I'm using SOME, and paying the price of code generator
  smack down.*)

definition nat2x :: "nat => nat" where "nat2x x = 2 * x"

export_code nat2x in SML file "i140331b__nat2x_to_code.ML"

ML_file "i140331b__nat2x_to_code.ML"

ML{*val x = i140331b__nat2x_to_code.nat2x (Arith.Nat 
  111111222222211111111133333111111888888888811111119999999999999111444111111)*}
  
(*** UNIX for Windows inside the THY! HUGE! HUGE! HUGE! ***********************)

ML{* val bashI = Isabelle_System.bash                                         *}
ML{* fun cdI path = bashI ("cd " ^ "\"" ^ path ^ "\"")                        *}
ML{* fun lsI args path = bashI ("ls " ^ args ^ " \"" ^ path ^ "\"")           *}

(*** Info for keeping it internal to the THY! Did I say HUGE! HUGE! HUGE!? ****)

ML{* val homeStr = File.platform_path (Thy_Load.master_directory @{theory})   *}
ML{* val homePathT = Thy_Load.master_directory @{theory}                      *}
ML{* writeln (Context.theory_name @{theory})                                  *}

(*** The Console for output? No, no, no! The Output for output! ***************)

ML{* cdI (homeStr ^ "/../..");(*No affect. File.cd below will be persistent.*)*}
     pwd 
ML{* lsI "-al" homeStr                                                        *}

(*** Cntl-hover links let you find related functions at hyper-link speed! *****)

ML{* (*File.cd homePathT*)                                                    *}
     pwd
end


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