1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/BridgeJEdit/BridgeJEdit.thy Sun Aug 02 12:32:34 2020 +0200
1.3 @@ -0,0 +1,13 @@
1.4 +(* Title: src/Tools/isac/BridgeJEdit/BridgeJEdit.thy
1.5 + Author: Walther Neuper, JKU Linz
1.6 + (c) due to copyright terms
1.7 +
1.8 +Auxiliary file for bootstrapping Isac
1.9 +*)
1.10 +
1.11 +theory BridgeJEdit
1.12 + imports Isac
1.13 +begin
1.14 +
1.15 +end
1.16 +
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/isac/BridgeJEdit/Isac.thy Sun Aug 02 12:32:34 2020 +0200
2.3 @@ -0,0 +1,39 @@
2.4 +(* Title: src/Tools/isac/BridgeJEdit/parseC.sml
2.5 + Author: Walther Neuper, JKU Linz
2.6 + (c) due to copyright terms
2.7 +
2.8 +Outer syntax for Isabelle/Isac. Compare src/Pure/Pure.thy
2.9 +*)
2.10 +
2.11 +theory Isac
2.12 + imports "~~/src/Tools/isac/MathEngine/MathEngine"
2.13 + keywords
2.14 + (* this has a type and thus is a "major keyword" *)
2.15 + "ISAC" :: diag
2.16 + (* the following are without type: "minor keywords" *)
2.17 + and "Problem" (* root-problem + recursively in Solution *)
2.18 + and "Specification" "Model" "References" "Solution" (* structure only *)
2.19 + and "Given" "Find" "Relate" "Where" (* await input of term *)
2.20 + and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
2.21 + "RProblem" "RMethod" (* await input of string list *)
2.22 + and "Tactic" (* optionally repeated with each step 0..end of calculation *)
2.23 +begin
2.24 + ML_file parseC.sml
2.25 +
2.26 +ML \<open>
2.27 +\<close> ML \<open>
2.28 +ParseC.problem (* not yet used *)
2.29 +\<close> ML \<open>
2.30 +\<close>
2.31 +
2.32 +(** setup command_keyword ISAC **)
2.33 +ML \<open>
2.34 +\<close> ML \<open>
2.35 +val _ =
2.36 + Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"
2.37 + (Parse.input ((**)Parse.cartouche (** )--(**) ParseC.problem( **)) >> (fn input =>
2.38 + Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
2.39 +\<close> ML \<open>
2.40 +\<close>
2.41 +
2.42 +end
2.43 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Sun Aug 02 12:32:34 2020 +0200
3.3 @@ -0,0 +1,219 @@
3.4 +(* Title: Tools/isac/BridgeJEdit/parseC.sml
3.5 + Author: Walther Neuper, JKU Linz
3.6 + (c) due to copyright terms
3.7 +
3.8 +Outer token syntax for Isabelle/Isac.
3.9 +*)
3.10 +
3.11 +signature PARSE_C =
3.12 +sig
3.13 + type problem
3.14 + val problem: problem parser
3.15 +
3.16 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.17 + (*tools*)
3.18 + val tokenize: string -> Token.T list
3.19 + val string_of_toks: Token.T list -> string
3.20 + val parse: (Token.T list -> 'a * Token.T list) -> Token.T list -> 'a * Token.T list
3.21 +
3.22 + (*Problem headline*)
3.23 + type problem_headline
3.24 + val problem_headline: problem_headline parser
3.25 +
3.26 + (*Specification*)
3.27 + type specification
3.28 + val specification: specification parser
3.29 +
3.30 + (*Model*)
3.31 + type model
3.32 + val model: model parser
3.33 +
3.34 + (*References*)
3.35 + type refs
3.36 + val refs_dummy: refs
3.37 + val references: ((string * string) * refs) parser
3.38 +
3.39 + (*compose Specification*)
3.40 + type model_refs_dummy
3.41 + val model_refs_dummy: model_refs_dummy
3.42 +
3.43 + (*Tactics *)
3.44 + val tactic: (string * string) parser
3.45 +
3.46 + val exec_check_postcond: string * string list -> string
3.47 + val check_postcond: Token.T list -> (string * string list) * Token.T list
3.48 + val exec_rewrite_set_inst: (string * string) * string -> string
3.49 + val rewrite_set_inst: Token.T list -> ((string * string) * string) * Token.T list
3.50 + val exec_substitute: (string * string) * string -> string
3.51 + val substitute: Token.T list -> ((string * string) * string) * Token.T list
3.52 +
3.53 + (*Problem*)
3.54 + val exec_step_term: string * (string * string) -> string
3.55 + (* TODO for mutual recursion Problem .. steps
3.56 + val subproblem_msg:
3.57 + val exec_subproblem *)
3.58 +
3.59 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.60 +end
3.61 +
3.62 +(**)
3.63 +structure ParseC(**): PARSE_C(**) =
3.64 +struct
3.65 +(**)
3.66 +
3.67 +(*** tools ***)
3.68 +
3.69 +fun tokenize str =
3.70 + filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
3.71 +
3.72 +fun parse parser toks = Scan.finite Token.stopper (Scan.error parser) toks
3.73 +
3.74 +fun string_of_toks toks = fold (curry op ^) (map Token.unparse toks |> rev |> separate ", ") "";
3.75 +
3.76 +
3.77 +(*** Problem headline ***)
3.78 +
3.79 +type problem_headline = (((((string * string) * string) * string) * string list) * string)
3.80 +
3.81 +val problem_headline = Parse.$$$ "Problem" --
3.82 + Parse.$$$ "(" --
3.83 + Parse.string -- Parse.$$$ "," --
3.84 + (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") --
3.85 + Parse.$$$ ")"
3.86 +
3.87 +
3.88 +(*** Specification ***)
3.89 +
3.90 +(** Model **)
3.91 +
3.92 +type model =
3.93 + ((((((((((((((string * ((string * string) * string)) * string) * string) * string) *
3.94 + string list) * string) * string) * string list) * string) * string) * string) *
3.95 + string) * string) * string list);
3.96 +val model = (
3.97 + Parse.$$$ "Model" --
3.98 + (Scan.optional (*.. show, whether the Model refers to RProblem or to RMethod *)
3.99 + (Parse.$$$ "(" -- (Parse.$$$ "RProblem" || Parse.$$$ "RMethod") -- Parse.$$$ ")")
3.100 + (("", ""), "") ) --
3.101 + Parse.$$$ ":" --
3.102 + Parse.$$$ "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term --
3.103 + Parse.$$$ "Where" -- Parse.$$$ ":" -- Parse.list Parse.term --
3.104 + Parse.$$$ "Find" -- Parse.$$$ ":" -- Parse.term --
3.105 + Parse.$$$ "Relate" -- Parse.$$$ ":" -- Parse.list Parse.term
3.106 +)
3.107 +
3.108 +(** References **)
3.109 +
3.110 +type refs =
3.111 + ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)
3.112 +val refs_dummy =
3.113 + (((((((("", ""), ""), ""), ""), []), ""), ""), [])
3.114 +
3.115 +val references = (
3.116 + Parse.$$$ "References" -- Parse.$$$ ":" (**) --
3.117 + (Scan.optional
3.118 + (Parse.$$$ "RTheory" -- Parse.$$$ ":" -- Parse.string (**) --
3.119 + Parse.$$$ "RProblem" -- Parse.$$$ ":" (**) --
3.120 + (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (**) --
3.121 + Parse.$$$ "RMethod" -- Parse.$$$ ":" (**) --
3.122 + (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")
3.123 + )
3.124 + refs_dummy
3.125 + ))
3.126 +
3.127 +(** compose Specification **)
3.128 +
3.129 +type model_refs_dummy = (model * ((string * string) * refs))
3.130 +val model_refs_dummy = ((((((((((((((("", (("", ""), "")), ""), ""), ""),
3.131 + []), ""), ""), []), ""), ""), ""), ""), ""),
3.132 + []),
3.133 + (("", ""), (((((((("", ""), ""), ""), ""), []),
3.134 + ""), ""), [])))
3.135 +
3.136 +type specification = (string * string) * model_refs_dummy
3.137 +val specification = (
3.138 + (Parse.$$$ "Specification" -- Parse.$$$ ":") --
3.139 + (Scan.optional
3.140 + (model -- references)
3.141 + )
3.142 + model_refs_dummy
3.143 +)
3.144 +
3.145 +(*** Tactics ***)
3.146 +
3.147 +val substitute = Parse.reserved "Substitute" -- Parse.term -- Parse.term;
3.148 +val rewrite_set_inst = Parse.reserved "Rewrite_Set_Inst" -- Parse.term -- Parse.name;
3.149 +val check_postcond = Parse.reserved "Check_Postcond" --
3.150 + (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]");
3.151 +
3.152 +(* see test/../Test_Parsers.thy \<open>|| requires arguments of equal type *)
3.153 +fun exec_substitute ((str, tm), bdv) =
3.154 + "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*UnparseC.term*) bdv;
3.155 +fun exec_rewrite_set_inst ((str, tm), id) =
3.156 + "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*Problem.id_to_string*) id;
3.157 +fun exec_check_postcond (str, path) =
3.158 + "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*Problem.id_to_string*)fold (curry op ^) path "";
3.159 +
3.160 +val tactic = ( (* incomplete list of tactics *)
3.161 + Parse.$$$ "Tactic" --
3.162 + (substitute >> exec_substitute ||
3.163 + rewrite_set_inst >> exec_rewrite_set_inst ||
3.164 + check_postcond >> exec_check_postcond
3.165 + )
3.166 + )
3.167 +
3.168 +
3.169 +(*** Problem ***)
3.170 +
3.171 +type problem =
3.172 + (((( problem_headline *
3.173 + ((string * string) * (model *
3.174 + ((string * string) * refs)))) *
3.175 + string) * string) * string list)
3.176 +
3.177 +fun exec_step_term (tm, (tac1, tac2)) =
3.178 + "EXEC IMMEDIATELY step_term: " ^ (*UnparseC.term*) tm ^ " (" ^ tac1 ^ ", " ^ tac2 ^ ")";
3.179 +
3.180 +(** )
3.181 +fun subproblem_msg
3.182 + (((((((((s1, s2), s3), s4), strs0), s5),
3.183 + ((s6, s7),
3.184 + (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),
3.185 + s23), s24), s25), s26), strs27),
3.186 + ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))
3.187 + , s51), s61), strs71) = "EXEC IMMEDIATELY step_subproblem:\n" ^
3.188 +" (((((((((" ^ s1 ^ ", " ^ s2 ^ "), " ^ s3 ^ "), " ^ s4 ^ "), " ^ LibraryC.strs2str strs0 ^ "), " ^ s5 ^ "),\n" ^
3.189 +" ((" ^ s6 ^ ", " ^ s7 ^ "),\n" ^
3.190 +" (((((((((((((((" ^ s11 ^ ", ((" ^ s12 ^ ", " ^ s13 ^ "), " ^ s14 ^ ")), " ^ s15 ^ "), " ^ s16 ^ "), " ^ s17 ^ "), " ^ LibraryC.strs2str strs18 ^ "), " ^ s19 ^ "), " ^ s20 ^ "), " ^ LibraryC.strs2str strs21 ^ "), " ^ s22 ^ "),\n" ^
3.191 + s23 ^ "), " ^ s24 ^ "), " ^ s25 ^ "), " ^ s26 ^ "), " ^ LibraryC.strs2str strs27 ^ "),\n" ^
3.192 +" ((" ^ s31 ^ ", " ^ s32 ^ "), ((((((((" ^ s30 ^ ", " ^ s33 ^ "), " ^ s34 ^ "), " ^ s35 ^ "), " ^ s36 ^ "), " ^ LibraryC.strs2str strs37 ^ "), " ^ s38 ^ "), " ^ s39 ^ "), " ^ LibraryC.strs2str strs40 ^ ")))))\n" ^
3.193 +" , " ^ s51 ^ "), " ^ s61 ^ "), " ^ LibraryC.strs2str strs71 ^ ")";
3.194 +fun exec_subproblem
3.195 + (((((((((s1, s2), s3), s4), strs0), s5),
3.196 + ((s6, s7),
3.197 + (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),
3.198 + s23), s24), s25), s26), strs27),
3.199 + ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))
3.200 + , s51), s61), strs71) = subproblem_msg
3.201 + (((((((((s1, s2), s3), s4), strs0), s5),
3.202 + ((s6, s7),
3.203 + (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),
3.204 + s23), s24), s25), s26), strs27),
3.205 + ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))
3.206 + , s51), s61), strs71);
3.207 +( **)
3.208 +
3.209 +val problem =
3.210 + problem_headline --
3.211 + specification --
3.212 + Parse.$$$ "Solution" -- Parse.$$$ ":" --
3.213 + (*/----- this will become "and steps".. *)
3.214 + (Scan.repeat (
3.215 + ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) ||
3.216 + (problem >> exec_subproblem) ( *exec_* make types equal for both args of ||*)
3.217 + ))
3.218 + (*\----- ..this will become "and steps",
3.219 + see Test_Parse_Isac subsubsection \<open>trials on recursion stopped\<close> *)
3.220 +
3.221 +
3.222 +(**)end(**)
3.223 \ No newline at end of file
4.1 --- a/src/Tools/isac/Build_Isac.thy Sat Aug 01 13:54:53 2020 +0200
4.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Aug 02 12:32:34 2020 +0200
4.3 @@ -133,6 +133,11 @@
4.4 ML_file "interface-xml.sml"
4.5 ML_file interface.sml
4.6 *) "BridgeLibisabelle/BridgeLibisabelle"
4.7 +(*
4.8 + theory Isac imports "~~/src/Tools/isac/MathEngine/MathEngine"
4.9 + ML_file parseC.sml
4.10 + theory BridgeJEdit imports Isac
4.11 +*) "BridgeJEdit/BridgeJEdit"
4.12
4.13 "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
4.14
5.1 --- a/test/Pure/Isar/Test_Parse_Isac.thy Sat Aug 01 13:54:53 2020 +0200
5.2 +++ b/test/Pure/Isar/Test_Parse_Isac.thy Sun Aug 02 12:32:34 2020 +0200
5.3 @@ -6,7 +6,8 @@
5.4 ( * the following are without type: "minor keywords" *)
5.5 "Problem" (* root-problem + recursively in Solution *)
5.6 "Specification" "Model" "References" "Solution" (* structure only *) and
5.7 - "Given" "Find" "Relate" "Where" (* await input of term *) and
5.8 + "Given" "Find" "Relate" "Where" (* await input of term
5.9 +*) and
5.10 "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) and
5.11 "RProblem" "RMethod" (* await input of string list *) and
5.12 "Tactic" (* optionally repeated with each step 0.. end of calculation *)
5.13 @@ -284,7 +285,7 @@
5.14
5.15 subsection \<open>References\<close>
5.16 ML \<open>
5.17 -\<close> ML \<open> (*original
5.18 +\<close> ML \<open> (*original, without support for folding refs
5.19 val references = (
5.20 Parse.$$$ "References" -- Parse.$$$ ":" (**) --
5.21 Parse.$$$ "RTheory" -- Parse.$$$ ":" -- Parse.string (**) --
5.22 @@ -302,10 +303,10 @@
5.23 :
5.24 ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list) parser
5.25 \<close> ML \<open>
5.26 -type references =
5.27 +type refs =
5.28 ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)
5.29 \<close> ML \<open>
5.30 -val empty_references =
5.31 +val refs_dummy =
5.32 (((((((("", ""), ""), ""), ""), []), ""), ""), [])
5.33 \<close> ML \<open>
5.34 val references = (
5.35 @@ -317,7 +318,7 @@
5.36 Parse.$$$ "RMethod" -- Parse.$$$ ":" (**) --
5.37 (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")
5.38 )
5.39 - empty_references
5.40 + refs_dummy
5.41 ))
5.42 \<close> ML \<open>
5.43 parse references (tokenize references_collapsed_str)
5.44 @@ -432,27 +433,27 @@
5.45 ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list)) parser
5.46 *)
5.47 \<close> ML \<open>
5.48 -type model_refs = (((((((((((((((string * ((string * string) * string)) * string) * string) * string) *
5.49 +type model_refs_dummy = (((((((((((((((string * ((string * string) * string)) * string) * string) * string) *
5.50 string list) * string) * string) * string list) * string) * string) * string) * string) * string) *
5.51 string list) *
5.52 ((string * string) * ((((((((string * string) * string) * string) * string) * string list) *
5.53 string) * string) * string list)))
5.54 \<close> ML \<open>
5.55 val string = "";
5.56 -val e_model_refs = ((((((((((((((("", (("", ""), "")), ""), ""), ""),
5.57 +val model_refs_dummy = ((((((((((((((("", (("", ""), "")), ""), ""), ""),
5.58 []), ""), ""), []), ""), ""), ""), ""), ""),
5.59 []),
5.60 (("", ""), (((((((("", ""), ""), ""), ""), []),
5.61 ""), ""), [])))
5.62 \<close> ML \<open>
5.63 -e_model_refs : model_refs
5.64 +model_refs_dummy : model_refs_dummy
5.65 \<close> ML \<open>
5.66 val specification = (
5.67 - (Parse.$$$ "Specification" -- Parse.$$$ ":") (**) --
5.68 - ( (**) Scan.optional (* ML error\<^here>: Type error in function application... *)
5.69 - (model -- references) (**)
5.70 - ) (**)
5.71 - e_model_refs
5.72 + (Parse.$$$ "Specification" -- Parse.$$$ ":") --
5.73 + (Scan.optional
5.74 + (model -- references)
5.75 + )
5.76 + model_refs_dummy
5.77 )
5.78 \<close> ML \<open> (*whole Specification from above -----------------------------------------------------\*)
5.79 specification (tokenize specification_str)
5.80 @@ -490,7 +491,7 @@
5.81 ([] : Token.T list)) => () | _ => error "parse specification (expanded) changed"
5.82 *)
5.83 \<close> ML \<open>
5.84 -(specification toks) : ((string * string) * model_refs) * Token.T list
5.85 +(specification toks) : ((string * string) * model_refs_dummy) * Token.T list
5.86 \<close> ML \<open>
5.87 \<close> ML \<open> (*Specification collapsed ------------------------------------------------------------\*)
5.88 val toks = tokenize (
5.89 @@ -686,7 +687,9 @@
5.90 ML \<open>
5.91 \<close> ML \<open>
5.92 val toks = tokenize (problem_headline_str ^ specification_str ^ solution_str)
5.93 -\<close> ML \<open>
5.94 +\<close>
5.95 +declare [[ML_print_depth = 999]] (* ..for getting complete <Output> *)
5.96 +ML \<open>
5.97 val problem =
5.98 problem_headline --
5.99 specification --
5.100 @@ -701,6 +704,7 @@
5.101 \<close>
5.102 declare [[ML_print_depth = 999]] (* ..for getting complete <Output> *)
5.103 ML \<open>
5.104 +specification
5.105 \<close> ML \<open>
5.106 parse problem toks
5.107 \<close> ML \<open>
5.108 @@ -772,7 +776,7 @@
5.109 \<close> ML \<open>
5.110 \<close>
5.111
5.112 -subsubsection \<open>enter Specification TODO\<close>
5.113 +subsubsection \<open>enter Specification\<close>
5.114 text \<open>
5.115 the Model only has Descriptors and the References are empty
5.116 \<close> ML \<open>
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/test/Tools/isac/BridgeJEdit/parseC.sml Sun Aug 02 12:32:34 2020 +0200
6.3 @@ -0,0 +1,12 @@
6.4 +(* Title: "BridgeJEdit/parseC.sml"
6.5 + Author: Walther Neuper
6.6 + (c) due to copyright terms
6.7 +*)
6.8 +
6.9 +"-----------------------------------------------------------------------------------------------";
6.10 +"table of contents -----------------------------------------------------------------------------";
6.11 +"-----------------------------------------------------------------------------------------------";
6.12 +"----------- SEE test/Pure/Isar/Test_Parse_Isac.thy --------------------------------------------";
6.13 +"-----------------------------------------------------------------------------------------------";
6.14 +"-----------------------------------------------------------------------------------------------";
6.15 +"-----------------------------------------------------------------------------------------------";
7.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sat Aug 01 13:54:53 2020 +0200
7.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Aug 02 12:32:34 2020 +0200
7.3 @@ -281,6 +281,8 @@
7.4 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
7.5 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
7.6
7.7 + ML_file "BridgeJEdit/parseC.sml"
7.8 +
7.9 ML_file "Knowledge/delete.sml"
7.10 ML_file "Knowledge/descript.sml"
7.11 ML_file "Knowledge/simplify.sml"