|
1 (* Title: src/Tools/isac/BridgeJEdit/parseC.sml |
|
2 Author: Walther Neuper, JKU Linz |
|
3 (c) due to copyright terms |
|
4 |
|
5 Outer syntax for Isabelle/Isac. Compare src/Pure/Pure.thy |
|
6 *) |
|
7 |
|
8 theory Calculation |
|
9 imports "~~/src/Tools/isac/MathEngine/MathEngine" (** )"HOL-SPARK.SPARK"( *prelim.for devel.*) |
|
10 keywords |
|
11 "Example" :: thy_load ("str") and (* "spark_vc" :: thy_goal *) |
|
12 "Problem" and (* root-problem + recursively in Solution *) |
|
13 "Specification" "Model" "References" "Solution" and (* structure only *) |
|
14 "Given" "Find" "Relate" "Where" and (* await input of term *) |
|
15 "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) |
|
16 "RProblem" "RMethod" and (* await input of string list *) |
|
17 "Tactic" (* optional for each step 0..end of calculation *) |
|
18 begin |
|
19 |
|
20 ML_file parseC.sml |
|
21 |
|
22 section \<open>\<close> |
|
23 ML \<open> |
|
24 \<close> ML \<open> |
|
25 ParseC.problem (* not yet used *) |
|
26 \<close> ML \<open> |
|
27 |
|
28 (*** get data from a file and initialise a calculation ***) |
|
29 |
|
30 (** data from file (~~ spark_open) **) |
|
31 |
|
32 \<close> ML \<open> |
|
33 \<close> ML \<open> (*spark_commands.ML: Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close>*) |
|
34 \<close> ML \<open> (*1st arg.of >>*) |
|
35 Resources.provide_parse_files "Example" -- Parse.parname: |
|
36 Token.T list -> ((theory -> Token.file list * theory) * string) * Token.T list; |
|
37 Resources.provide_parse_files "Example" -- Parse.parname: |
|
38 ((theory -> Token.file list * theory) * string) parser |
|
39 \<close> ML \<open> |
|
40 \<close> ML \<open> (*2nd arg.of >>*) |
|
41 type chars = (string * Position.T) list; |
|
42 val e_chars = []: (string * Position.T) list; |
|
43 |
|
44 type banner = string * string * string; val e_banner = ("b1", "b2", "b3") |
|
45 type date = string * string * string; val e_date = ("d1", "d2", "d3") |
|
46 type time = string * string * string * string option; val e_time = ("t1", "t2", "t3", SOME "t4") |
|
47 |
|
48 fun vcg_header (_: chars) = ((e_banner, SOME (e_date, e_time)), e_chars); |
|
49 (*^^^^^^^^^^^^*) |
|
50 vcg_header: chars -> (banner * (date * time) option) * chars |
|
51 \<close> ML \<open> |
|
52 fun spark_open (_: (*Fdl_Lexer.*)chars -> 'a * (*Fdl_Lexer.*)chars) |
|
53 (*^^^^^^^^^^^^*) |
|
54 (_: ('b -> Token.file list * theory) * string) (_: 'b) = @{theory}; |
|
55 spark_open: (chars -> 'a * chars) -> ('b -> Token.file list * theory) * string -> 'b -> theory |
|
56 \<close> ML \<open> |
|
57 val exp_file = "~~/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str" |
|
58 \<close> ML \<open> |
|
59 \<close> ML \<open> |
|
60 \<close> ML \<open> |
|
61 \<close> ML \<open> |
|
62 \<close> ML \<open> |
|
63 \<close> |
|
64 |
|
65 section \<open>setup command_keyword \<close> |
|
66 (** ISAC **) |
|
67 ML \<open> |
|
68 \<close> ML \<open> |
|
69 val _ = |
|
70 Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start example from file" |
|
71 (*preliminary from spark_open*) |
|
72 (Resources.provide_parse_files "spark_open" -- Parse.parname (*1st arg of >>*) |
|
73 >> (Toplevel.theory o spark_open (*Fdl_Lexer.*)vcg_header)); (*2nd arg of >>*) |
|
74 \<close> ML \<open> |
|
75 \<close> |
|
76 |
|
77 section \<open>tests, before -> test/*\<close> |
|
78 |
|
79 end |