5 Outer syntax for Isabelle/Isac's Calculation. |
5 Outer syntax for Isabelle/Isac's Calculation. |
6 *) |
6 *) |
7 |
7 |
8 theory Calculation |
8 theory Calculation |
9 imports |
9 imports |
10 (**) "~~/src/Tools/isac/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*) |
10 (**)"~~/src/Tools/isac/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*) |
11 (**)"~~/src/Tools/isac/MathEngine/MathEngine" |
11 (**)"~~/src/Tools/isac/MathEngine/MathEngine" |
12 (**) "HOL-SPARK.SPARK" (*remove after devel.of BridgeJEdit*) |
12 (**)"HOL-SPARK.SPARK" (*remove after devel.of BridgeJEdit*) |
13 keywords |
13 keywords |
14 (*WAS "Example" :: thy_load ("str") ..in Isabelle2020*) |
14 "Example" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*) |
15 (**) "Example" :: thy_load (*(isac_example) ..would involve registering in Isabelle/Scala*) |
15 and(**)"Problem" :: thy_decl (*r oot-problem + recursively in Solution *) |
16 and(**)"Problem" :: thy_decl (* root-problem + recursively in Solution; |
16 and "Specification" "Model" "References" :: diag (* structure only *) |
17 "spark_vc" :: thy_goal *) |
|
18 and "Specification" "Model" "References" :: diag |
|
19 (*TRIED: diag quasi_command qed_script thy_decl thy_defn thy_goal thy_goal_stmt thy_stmt vvv *) |
|
20 and "Solution" :: thy_decl (* structure only *) |
17 and "Solution" :: thy_decl (* structure only *) |
21 and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term, cp.from "from".."have" *) |
18 and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term *) |
22 (* ^^^^^^ :: .. see Pure/Isar/keyword.ML (* command categories *) TRIED COMBINATIONS WITH ^^^: |
|
23 before_command quasi_command thy_decl thy_defn thy_stmt diag prf_decl *) |
|
24 (*and "Where" (* only output, preliminarily *)*) |
19 (*and "Where" (* only output, preliminarily *)*) |
25 and "RTheory" :: thy_decl (* await input of string; "R" distingues "Problem".."RProblem" *) |
20 and "RTheory" :: thy_decl (* await input of string; "R" distingues "Problem".."RProblem" *) |
26 and "RProblem" "RMethod" :: thy_decl (* await input of string list *) |
21 and "RProblem" "RMethod" :: thy_decl (* await input of string list *) |
27 and "Tactic" (* optional for each step 0..end of calculation *) |
22 and "Tactic" (* optional for each step 0..end of calculation *) |
28 begin |
23 begin |
29 declare [[ML_print_depth = 99999]] |
24 (** )declare [[ML_print_depth = 99999]]( **) |
30 (**)ML_file parseC.sml(**) |
25 ML_file parseC.sml |
31 (**)ML_file preliminary.sml(**) |
26 ML_file preliminary.sml |
32 |
27 |
33 |
28 |
34 section \<open>new code for Outer_Syntax Example, Problem, ...\<close> |
29 section \<open>new code for Outer_Syntax Example, Problem, ...\<close> |
35 text \<open> |
30 text \<open> |
36 code for Example, Problem shifted into structure Preliminary. |
31 code for Example, Problem shifted into structure Preliminary. |
118 \<close> |
109 \<close> |
119 |
110 |
120 section \<open>setup command_keyword + preliminary test\<close> |
111 section \<open>setup command_keyword + preliminary test\<close> |
121 ML \<open> |
112 ML \<open> |
122 \<close> ML \<open> |
113 \<close> ML \<open> |
123 (**) |
|
124 val _ = |
114 val _ = |
125 Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file" |
115 Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file" |
126 (Resources.provide_parse_file -- Parse.parname |
116 (Resources.provide_parse_file -- Parse.parname |
127 >> (Toplevel.theory o (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*) |
117 >> (Toplevel.theory o (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*) |
128 (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) ); |
118 (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) ); |
129 (**) |
|
130 \<close> ML \<open> |
|
131 (Toplevel.theory o (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) |
|
132 : |
|
133 (theory -> Token.file * theory) * string -> |
|
134 Toplevel.transition -> Toplevel.transition |
|
135 (* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*) |
|
136 \<close> ML \<open> |
119 \<close> ML \<open> |
137 val _ = |
120 val _ = |
138 Outer_Syntax.command \<^command_keyword>\<open>Problem\<close> |
121 Outer_Syntax.command \<^command_keyword>\<open>Problem\<close> |
139 "start a Specification, either from scratch or from preceding 'Example'" |
122 "start a Specification, either from scratch or from preceding 'Example'" |
140 (** )(ParseC.problem >> (Toplevel.theory o Preliminary.init_specify));( **) |
123 ((writeln o Token.s_to_string, ParseC.problem_headline) |
141 (**)((writeln o Token.s_to_string, ParseC.problem_headline) |
124 @@>> (Toplevel.theory o Preliminary.init_specify)); |
142 @@>> (Toplevel.theory o Preliminary.init_specify));(**) |
|
143 \<close> ML \<open> |
125 \<close> ML \<open> |
144 Preliminary.init_specify: ParseC.problem_headline -> theory -> theory; |
126 Preliminary.init_specify: ParseC.problem_headline -> theory -> theory; |
145 (Toplevel.theory o Preliminary.init_specify) |
127 (Toplevel.theory o Preliminary.init_specify) |
146 : ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition; |
128 : ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition; |
147 \<close> ML \<open> |
129 \<close> ML \<open> |
148 (**) Preliminary.init_specify: ParseC.problem_headline -> theory -> theory;(**) |
130 (**) Preliminary.init_specify: ParseC.problem_headline -> theory -> theory;(**) |
149 (* ^^^^^^ ^^^^^^*) |
131 (* ^^^^^^ ^^^^^^*) |
150 (**)(Toplevel.theory o Preliminary.init_specify): |
132 (**)(Toplevel.theory o Preliminary.init_specify): |
151 ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition;(**) |
133 ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition;(**) |
152 (* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*) |
134 (* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*) |
153 \<close> ML \<open> |
|
154 \<close> ML \<open> |
|
155 OMod_Data.get |
|
156 \<close> ML \<open> |
135 \<close> ML \<open> |
157 fun dummy (_(*":"*): string) thy = |
136 fun dummy (_(*":"*): string) thy = |
158 let |
137 let |
159 val refs' = Refs_Data.get thy |
138 val refs' = Refs_Data.get thy |
160 val o_model = OMod_Data.get thy |
139 val o_model = OMod_Data.get thy |
161 val i_model = IMod_Data.get thy |
140 val i_model = IMod_Data.get thy |
162 val _ = |
141 val _ = |
163 @{print} {a = "### dummy Specification", refs = refs', o_model = o_model, i_model = i_model} |
142 @{print} {a = "### dummy Specification", refs = refs', o_model = o_model, i_model = i_model} |
164 in |
143 in thy end; |
165 thy |
144 \<close> ML \<open> |
166 end; |
145 val _ = |
167 \<close> ML \<open> |
146 Outer_Syntax.command \<^command_keyword>\<open>Specification\<close> "Specification dummy" |
168 (Toplevel.theory o dummy): string -> Toplevel.transition -> Toplevel.transition |
|
169 \<close> ML \<open> |
|
170 val _ = |
|
171 (*Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language" |
|
172 (Parse.input Parse.cartouche >> (fn input => |
|
173 Toplevel.keep (fn _ => ignore (ML_Lex.read_source (*true*) input)))) |
|
174 *)Outer_Syntax.command \<^command_keyword>\<open>Specification\<close> "Specification dummy" |
|
175 ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy)) |
147 ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy)) |
176 \<close> ML \<open> |
148 \<close> ML \<open> |
177 val _ = |
149 val _ = |
178 Outer_Syntax.command \<^command_keyword>\<open>Model\<close> "Model dummy" |
150 Outer_Syntax.command \<^command_keyword>\<open>Model\<close> "Model dummy" |
179 ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy)) |
151 ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy)) |