1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Apr 22 16:21:23 2021 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Apr 22 16:49:41 2021 +0200
1.3 @@ -17,6 +17,8 @@
1.4 ML_file "thy-hierarchy.sml"
1.5 ML_file "interface-xml.sml"
1.6 ML_file interface.sml
1.7 +(*
1.8 +*)
1.9
1.10 ML \<open>
1.11 \<close> ML \<open>
2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 22 16:21:23 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 22 16:49:41 2021 +0200
2.3 @@ -284,39 +284,47 @@
2.4 (** general types: lists, **)
2.5
2.6 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
2.7 +(*
2.8 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
2.9 | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
2.10
2.11 fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = Ptool.str2ketype' str
2.12 | xml_to_ketype tree = raise ERROR ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)
2.13 +*)
2.14
2.15 fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
2.16 fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
2.17
2.18 +(*
2.19 fun xml_to_str (XML.Elem (("STRING", []), [XML.Text str])) = str
2.20 | xml_to_str tree = raise ERROR ("xml_to_str: wrong XML.tree \n" ^ xmlstr 0 tree)
2.21 fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
2.22 | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
2.23 +*)
2.24
2.25 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
2.26 fun xml_of_ints is =
2.27 XML.Elem (("INTLIST", []), map xml_of_int is)
2.28
2.29 +(*
2.30 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
2.31 (case TermC.int_opt_of_string i of SOME i => i | _ => raise ERROR "xml_to_int: int_of_str \<Rightarrow> NONE")
2.32 | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)
2.33 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
2.34 | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
2.35 +*)
2.36
2.37 (** isac datatypes **)
2.38 fun xml_of_pos tag (is, pp) =
2.39 XML.Elem ((tag, []), [
2.40 xml_of_ints is,
2.41 XML.Elem (("POS", []), [XML.Text (Pos.pos_2str pp)])])
2.42 +(*
2.43 fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = Pos.str2pos_ pp
2.44 | xml_to_pos_ tree = raise ERROR ("xml_to_pos_: wrong XML.tree \n" ^ xmlstr 0 tree)
2.45 fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
2.46 | xml_to_pos tree = raise ERROR ("xml_to_pos: wrong XML.tree \n" ^ xmlstr 0 tree)
2.47 +*)
2.48
2.49 fun xml_of_auto (Solve.Steps i) =
2.50 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
2.51 @@ -325,6 +333,7 @@
2.52 | xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
2.53 | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
2.54 | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
2.55 +(*
2.56 fun xml_to_auto (XML.Elem (("AUTO", []), [
2.57 XML.Elem (("STEP", []), [XML.Text i])])) = Solve.Steps (TermC.int_opt_of_string i |> the)
2.58 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = Solve.CompleteModel
2.59 @@ -333,6 +342,7 @@
2.60 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = Solve.CompleteSubpbl
2.61 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = Solve.CompleteCalc
2.62 | xml_to_auto tree = raise ERROR ("xml_to_auto: wrong XML.tree \n" ^ xmlstr 0 tree)
2.63 +*)
2.64
2.65 fun filterpbl str =
2.66 let fun filt [] = []
2.67 @@ -384,22 +394,28 @@
2.68 XML.Elem (("THEORYID", []), [XML.Text thyID]),
2.69 XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
2.70 XML.Elem (("METHODID", []), [xml_of_strs metID])])
2.71 +(*
2.72 fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [
2.73 XML.Elem (("THEORYID", []), [XML.Text thyID]),
2.74 XML.Elem (("PROBLEMID", []), [ps]),
2.75 XML.Elem (("METHODID", []), [ms])])) = (thyID, xml_to_strs ps, xml_to_strs ms)
2.76 | xml_to_spec tree = raise ERROR ("xml_to_spec: wrong XML.tree \n" ^ xmlstr 0 tree)
2.77 +*)
2.78
2.79 fun xml_of_variant (items, spec) =
2.80 XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])
2.81 +(*
2.82 fun xml_to_variant (XML.Elem (("VARIANT", []), [items, spec])) =
2.83 (xml_to_strs items, xml_to_spec spec)
2.84 | xml_to_variant tree = raise ERROR ("xml_to_variant: wrong XML.tree \n" ^ xmlstr 0 tree)
2.85 +*)
2.86
2.87 fun xml_of_fmz [] = xml_of_fmz [Formalise.empty]
2.88 | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
2.89 +(*
2.90 fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
2.91 | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
2.92 +*)
2.93
2.94 fun xml_of_modspec ((b, p_, head, gfr, pre, spec): SpecificationC.T) =
2.95 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
2.96 @@ -417,6 +433,7 @@
2.97 XML.Elem (("BELONGSTO", []), [
2.98 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
2.99 xml_of_spec spec])
2.100 +(*
2.101 fun xml_to_imodel
2.102 (XML.Elem (("IMODEL", []), [
2.103 XML.Elem (("GIVEN", []), givens),
2.104 @@ -437,28 +454,35 @@
2.105 (xml_to_pos pos, xml_to_term_NEW form |> UnparseC.term, xml_to_imodel imodel,
2.106 Pos.str2pos_ belongsto, xml_to_spec spec) : P_Spec.icalhd
2.107 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
2.108 +*)
2.109
2.110 fun xml_of_sub (id, value) =
2.111 XML.Elem (("PAIR", []), [
2.112 XML.Elem (("VARIABLE", []), [xml_of_term id]),
2.113 XML.Elem (("VALUE", []), [xml_of_term value])])
2.114 +(*
2.115 fun xml_to_sub
2.116 (XML.Elem (("PAIR", []), [
2.117 XML.Elem (("VARIABLE", []), [id]),
2.118 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
2.119 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
2.120 +*)
2.121 fun xml_of_subs (subs : Subst.input) =
2.122 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs))
2.123 +(*
2.124 fun xml_to_subs
2.125 (XML.Elem (("SUBSTITUTION", []),
2.126 subs)) = Subst.T_to_input (map xml_to_sub subs)
2.127 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
2.128 +*)
2.129 fun xml_of_sube sube =
2.130 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))
2.131 +(*
2.132 fun xml_to_sube
2.133 (XML.Elem (("SUBSTITUTION", []),
2.134 xml_var_val_pairs)) = Subst.T_to_string_eqs (map xml_to_sub xml_var_val_pairs)
2.135 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
2.136 +*)
2.137
2.138 fun thm''2xml j (thm : thm) =
2.139 indt j ^ "<THEOREM>\n" ^
2.140 @@ -482,6 +506,7 @@
2.141 XML.Elem (("FORMULA", []), [
2.142 XML.Text ((UnparseC.term o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *)
2.143
2.144 +(*
2.145 fun xml_to_thm'
2.146 (XML.Elem (("THEOREM", []), [
2.147 XML.Elem (("ID", []), [XML.Text ID]),
2.148 @@ -502,6 +527,7 @@
2.149 XML.Elem (("FORMULA", []), [
2.150 XML.Text term])])) = (ID, ThmC.thm_from_thy (ThyC.Isac ()) ID)
2.151 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
2.152 +*)
2.153
2.154 fun xml_of_src Rule.Empty_Prog =
2.155 XML.Elem (("NOCODE", []), [XML.Text "empty"])
2.156 @@ -566,6 +592,7 @@
2.157 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
2.158 | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac);
2.159
2.160 +(*
2.161 fun xml_to_tac
2.162 (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
2.163 XML.Elem (("THEORY", []), [XML.Text dI]),
2.164 @@ -635,6 +662,7 @@
2.165 (XML.Elem (("STRINGLISTTACTIC", [
2.166 ("name", "Specify_Problem")]), [ct])) = Tactic.Specify_Problem (xml_to_strs ct)
2.167 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
2.168 +*)
2.169
2.170 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
2.171 ("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")");
2.172 @@ -705,9 +733,11 @@
2.173 xml_of_pos "UNCHANGED" old,
2.174 xml_of_pos "DELETED" del,
2.175 xml_of_pos "GENERATED" new])])
2.176 +(*
2.177 fun xml_to_calcchanged (XML.Elem (("CALCCHANGED", []), [old, del, new])) =
2.178 (xml_to_pos old, xml_to_pos del, xml_to_pos new)
2.179 | xml_to_calcchanged x = raise ERROR ("xml_to_calcchanged: WRONG arg = " ^ xmlstr 0 x)
2.180 +*)
2.181
2.182 (* for checking output at Frontend *)
2.183 fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode
3.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Thu Apr 22 16:21:23 2021 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Thu Apr 22 16:49:41 2021 +0200
3.3 @@ -86,6 +86,7 @@
3.4 XML.Elem (("MATHML", []),
3.5 [XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)])])
3.6 fun xml_of_terms ts = map xml_of_term ts
3.7 +(*
3.8 fun xml_to_term
3.9 ((XML.Elem (("MATHML", []), [
3.10 XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term
3.11 @@ -96,6 +97,7 @@
3.12 | xml_to_term_NEW xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
3.13 fun xml_to_terms ts = map xml_to_term ts
3.14 fun xml_to_terms_NEW ts = map xml_to_term_NEW ts
3.15 +*)
3.16
3.17 (* intermediate replacements while introducing transfer of terms by libisabelle *)
3.18 fun xml_of_term_NEW (t : term) =
3.19 @@ -108,6 +110,7 @@
3.20 (*\\---------------------------------- rm libisabelle ---------------------------------------//*)
3.21 ])
3.22
3.23 +(*
3.24 (* unused: formulas come as strings from frontend and are parsed by Isabelle *)
3.25 fun xml_to_term_UNUSED
3.26 ((XML.Elem (("FORMULA", []), [
3.27 @@ -119,6 +122,7 @@
3.28 Const ("rm libisabelle: xt NOT DECODED", HOLogic.realT)
3.29 (*\\---------------------------------- rm libisabelle ---------------------------------------//*)
3.30 | xml_to_term_UNUSED xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
3.31 +*)
3.32
3.33 (*version for TextIO*)
3.34 fun terms2xml j [] = ""
3.35 @@ -136,10 +140,12 @@
3.36 fun xml_of_cterm ct =
3.37 XML.Elem (("MATHML", []),
3.38 [XML.Elem (("ISA", []), [XML.Text ct])])
3.39 +(*
3.40 fun xml_to_cterm
3.41 (XML.Elem (("MATHML", []),
3.42 [XML.Elem (("ISA", []), [XML.Text ct])])) = ct
3.43 | xml_to_cterm x = raise ERROR ("xml_to_cterm wrong arg: " ^ xmlstr 0 x)
3.44 +*)
3.45
3.46 (*version for TextIO*)
3.47 fun cterms2xml j [] = ""
4.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml Thu Apr 22 16:21:23 2021 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,247 +0,0 @@
4.4 -(* Title: tests for libisabelle
4.5 - https://github.com/wneuper/libisabelle cloned from ...
4.6 - https://github.com/larsrh/libisabelle
4.7 - Author: Walther Neuper 2015
4.8 - Use is subject to license terms.
4.9 -*)
4.10 -
4.11 -"-----------------------------------------------------------------------------";
4.12 -"-----------------------------------------------------------------------------";
4.13 -"table of contents -----------------------------------------------------------";
4.14 -"-----------------------------------------------------------------------------";
4.15 -"-------- mini-test ----------------------------------------------------------";
4.16 -"-----------------------------------------------------------------------------";
4.17 -"-----------------------------------------------------------------------------";
4.18 -
4.19 -
4.20 -"-------- mini-test ----------------------------------------------------------";
4.21 -"-------- mini-test ----------------------------------------------------------";
4.22 -"-------- mini-test ----------------------------------------------------------";
4.23 -(* see
4.24 -https://github.com/wneuper/libisabelle/blob/master/doc/test--isac-Java--isac-kernel.txt*)
4.25 -reset_states (); (*resets all state information in Kernel *)
4.26 -
4.27 -"----------- step 1: operation_setup calctree --------------------------------------------------";
4.28 -val items = ["equality (x+1=(2::real))", "solveFor x", "solutions L"]
4.29 -val spec = ("Test", ["sqroot-test", "univariate", "equation", "test"], ["Test", "squ-equ-test-subpbl1"])
4.30 -val intree = xml_of_fmz [(items, spec)]
4.31 -(* --- VARIANT was missing:
4.32 -val intree =
4.33 -<FORMALIZATION>
4.34 - <VARIANT>
4.35 - <STRINGLIST>
4.36 - <STRING>equality (x+1=(2::real))</STRING>
4.37 - <STRING>solveFor x</STRING>
4.38 - <STRING>solutions L</STRING>
4.39 - </STRINGLIST>
4.40 - <SPECIFICATION>
4.41 - <THEORYID>Test</THEORYID>
4.42 - <PROBLEMID>
4.43 - <STRINGLIST>
4.44 - <STRING>sqroot-test</STRING>
4.45 - <STRING>univariate</STRING>
4.46 - <STRING>equation</STRING>
4.47 - <STRING>test</STRING>
4.48 - </STRINGLIST>
4.49 - </PROBLEMID>
4.50 - <METHODID>
4.51 - <STRINGLIST>
4.52 - <STRING>Test</STRING>
4.53 - <STRING>squ-equ-test-subpbl1</STRING>
4.54 - </STRINGLIST>
4.55 - </METHODID>
4.56 - </SPECIFICATION>
4.57 - </VARIANT>
4.58 -</FORMALIZATION>:
4.59 -*)
4.60 -;
4.61 -"~~~~~ operation_setup calctree, args:"; val intree =
4.62 - (xml_of_fmz [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
4.63 - ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))])
4.64 - val fmz = case intree of
4.65 - tree as XML.Elem (("FORMALIZATION", []), _) => xml_to_fmz tree
4.66 - | tree => error ("calctree: intree =" ^ xmlstr 0 tree)
4.67 -
4.68 - val result = CalcTree fmz (* <--------------------------------- *)
4.69 -;
4.70 -val calcid = case result of
4.71 - XML.Elem (("CALCTREE", []), [
4.72 - XML.Elem (("CALCID", []), [XML.Text calcid])]) => int_of_str calcid
4.73 -| tree => error ("test--isac-java--isac-kernel step 1: operation_setup calctree changed, out = \n" ^
4.74 - xmlstr 0 tree);
4.75 -result |> xmlstr 0 |> writeln (*
4.76 -<CALCTREE>
4.77 -. <CALCID>
4.78 -. . 1
4.79 -. </CALCID>
4.80 -</CALCTREE>
4.81 -*)
4.82 -;
4.83 -"----------- step 2: operation_setup iterator --------------------------------------------------";
4.84 -"~~~~~ operation_setup iterator, args:"; val calcid = calcid
4.85 -val out = Iterator calcid (* <--------------------------------- *)
4.86 -val XML.Elem (("ADDUSER", []),
4.87 - [XML.Elem (("CALCID", []), [XML.Text calcid]),
4.88 - XML.Elem (("USERID", []), [XML.Text userid])]) = out;
4.89 -"~~~~~ operation_setup iterator";
4.90 -"calcid = "; calcid;
4.91 -"userid = "; userid;
4.92 -if calcid = "1" andalso userid = "1" then ()
4.93 -else error "test--isac-java--isac-kernel step 2: operation_setup iterator changed"
4.94 -out |> xmlstr 0 |> writeln (*
4.95 -<ADDUSER>
4.96 -. <CALCID>
4.97 -. . 1
4.98 -. </CALCID>
4.99 -. <USERID>
4.100 -. . 1
4.101 -. </USERID>
4.102 -</ADDUSER>
4.103 -*)
4.104 -;
4.105 -"----------- step 3: operation_setup moveactiveroot --------------------------------------------";
4.106 -"~~~~~ operation_setup moveactiveroot, args:"; val calcid = calcid
4.107 -val out = moveActiveRoot (int_of_str calcid) (* <--------------------------------- *)
4.108 -val XML.Elem (("CALCITERATOR", []), [
4.109 - XML.Elem (("CALCID", []), [XML.Text calcid]),
4.110 - XML.Elem (("POSITION", []), [
4.111 - XML.Elem (("INTLIST", []), is),
4.112 - XML.Elem (("POS", []), [XML.Text kind])])]) = out;
4.113 -if calcid = "1" andalso is = [] andalso kind = "Pbl" then ()
4.114 -else error "test--isac-java--isac-kernel step 3: operation_setup moveactiveroot changed";
4.115 -out |> xmlstr 0 |> writeln (*
4.116 -<CALCITERATOR>
4.117 -. <CALCID>
4.118 -. . 1
4.119 -. </CALCID>
4.120 -. <POSITION>
4.121 -. . <INTLIST>
4.122 -. . </INTLIST>
4.123 -. . <POS>
4.124 -. . . Pbl
4.125 -. . </POS>
4.126 -. </POSITION>
4.127 -</CALCITERATOR>
4.128 -*)
4.129 -;
4.130 -"----------- step 4: operation_setup getformulaefromto -----------------------------------------";
4.131 -val pos as (is, kind) = ([], Pbl)
4.132 -val calcformula as (pos, formula) = (pos, "solve (x + 1 = 2, x)")
4.133 -val formheads = [calcformula (*, calchead .. see below*)]
4.134 -val intree = (* CREATE THIS IN Mini_Test.java *)
4.135 - XML.Elem (("GETFORMULAEFROMTO", []), [
4.136 - XML.Elem (("CALCID", []),
4.137 - [XML.Text calcid]),
4.138 - xml_of_pos "POSITION" (is, kind),
4.139 - xml_of_pos "POSITION" (is, kind),
4.140 - xml_of_int 0,
4.141 - xml_of_bool false]);
4.142 -"~~~~~ operation_setup getformulaefromto, args:"; val calcid = calcid
4.143 - val (ci, from, to, level, rules) = case intree of
4.144 - XML.Elem (("GETFORMULAEFROMTO", []), [
4.145 - XML.Elem (("CALCID", []), [XML.Text calcid]),
4.146 - from as XML.Elem (("POSITION", []), [
4.147 - XML.Elem (("INTLIST", []), _),
4.148 - XML.Elem (("POS", []), [XML.Text _])]),
4.149 - to as XML.Elem (("POSITION", []), [
4.150 - XML.Elem (("INTLIST", []), _),
4.151 - XML.Elem (("POS", []), [XML.Text _])]),
4.152 - XML.Elem (("INT", []), [XML.Text level]),
4.153 - XML.Elem (("BOOL", []), [XML.Text rules])]) => (calcid, from, to, level, rules)
4.154 - | tree => error ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
4.155 - val SOME calcid = ThmC_Def.int_opt_of_string calcid
4.156 - val from = xml_to_pos from
4.157 - val to = xml_to_pos to
4.158 - val SOME level = (*xml_to_int*) ThmC_Def.int_opt_of_string level
4.159 - val rules = (*xml_to_bool*) string_to_bool rules
4.160 - val out = getFormulaeFromTo calcid from to level rules (* <-------------------- *)
4.161 -;
4.162 -(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
4.163 -if xmlstr 0 out =
4.164 -"(GETELEMENTSFROMTO)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (FORMHEADS)\n. . (CALCFORMULA)\n. . . (POSITION)\n. . . . (INTLIST)\n. . . . (/INTLIST)\n. . . . (POS)\n. . . . . Pbl\n. . . . (/POS)\n. . . (/POSITION)\n. . . (FORMULA)\n. . . . (ISA)\n. . . . . solve (x + 1 = 2, x)\n. . . . (/ISA)\n. . . . (TERM)\n. . . . . solve (x + 1 = 2, x)\n. . . . (/TERM)\n. . . (/FORMULA)\n. . (/CALCFORMULA)\n. (/FORMHEADS)\n(/GETELEMENTSFROMTO)\n"
4.165 -then () else error "test--isac-java--isac-kernel step 4: operation_setup getformulaefromto CHANGED";
4.166 -out |> xmlstr 0 |> writeln (*
4.167 -( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
4.168 -<GETELEMENTSFROMTO>
4.169 -. <CALCID>
4.170 -. . 1
4.171 -. </CALCID>
4.172 -. <FORMHEADS>
4.173 -. . <CALCFORMULA>
4.174 -. . . <POSITION>
4.175 -. . . . <INTLIST>
4.176 -. . . . </INTLIST>
4.177 -. . . . <POS>
4.178 -. . . . . Pbl
4.179 -. . . . </POS>
4.180 -. . . </POSITION>
4.181 -. . . <FORMULA>
4.182 -. . . . <MATHML>
4.183 -. . . . . <ISA>
4.184 -. . . . . . solve (x + 1 = 2, x)
4.185 -. . . . . </ISA>
4.186 -. . . . </MATHML>
4.187 -. . . </FORMULA>
4.188 -. . </CALCFORMULA>
4.189 -. </FORMHEADS>
4.190 -</GETELEMENTSFROMTO>
4.191 -*)
4.192 -;
4.193 -(* TODO ...*)
4.194 -"----------- step 5: operation_setup refformula ------------------------------------------------";
4.195 -"~~~~~ operation_setup getformulaefromto, args:"; val () = ()
4.196 -;
4.197 -"----------- step 6: operation_setup refformula ------------------------------------------------";
4.198 -(* intree von TestPIDE.java:
4.199 -<REFFORMULA>
4.200 - <CALCID>1</CALCID>
4.201 - <POSITION>
4.202 - <INTLIST/>
4.203 - <POS>Pbl</POS>
4.204 - </POSITION>
4.205 -</REFFORMULA>*)
4.206 -if ci = "1" then () else error "--- step 6: ci <> 1";
4.207 -val intree =
4.208 - XML.Elem (("REFFORMULA", []), [
4.209 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.210 - XML.Elem (("POSITION", []), [
4.211 - XML.Elem (("INTLIST", []), []),
4.212 - XML.Elem (("POS", []), [XML.Text "Pbl"])])])
4.213 -;
4.214 -"~~~~~ operation_setup refformula, args:"; val intree = intree;
4.215 - val (ci, p) =
4.216 - case intree of
4.217 - XML.Elem (("REFFORMULA", []), [
4.218 - XML.Elem (("CALCID", []), [XML.Text ci]),
4.219 - p]) => (ci, p)
4.220 - | _ => error "operation_setup refformula intree changed"
4.221 - val SOME calcid = ThmC_Def.int_opt_of_string ci
4.222 - val pos = xml_to_pos p
4.223 -;
4.224 -if calcid = 1 andalso pos = ([], Pbl) then () else error "--- step 6: intree changed";
4.225 - val result = refFormula calcid pos
4.226 -;
4.227 -(*this vanished by now..*)
4.228 -xmlstr 0 result = "<REFFORMULA>\n. <CALCID>\n. . 1\n. </CALCID>\n. <ERROR>\n. . pos does not exist \n. </ERROR>\n</REFFORMULA>\n"
4.229 -;
4.230 -"----------- step 7: operation_setup autocalculate ---------------------------------------------";
4.231 -"~~~~~ operation_setup autocalculate, args:"; val () = ()
4.232 -;
4.233 -"----------- step 8: operation_setup getformulaefromto -----------------------------------------";
4.234 -"~~~~~ operation_setup getformulaefromto, args:"; val () = ()
4.235 -;
4.236 -"----------- step 9: operation_setup getformulaefromto -----------------------------------------";
4.237 -"~~~~~ operation_setup getformulaefromto, args:"; val () = ()
4.238 -;
4.239 -"----------- step 10: operation_setup refformula -----------------------------------------------";
4.240 -"~~~~~ operation_setup refformula, args:"; val () = ()
4.241 -;
4.242 -"----------- step 11: operation_setup refformula -----------------------------------------------";
4.243 -"~~~~~ operation_setup refformula, args:"; val () = ()
4.244 -;
4.245 -"----------- step 12: operation_setup refFormula -----------------------------------------------";
4.246 -"~~~~~ operation_setup refformula, args:"; val () = ()
4.247 -;
4.248 -"----------- step 13: operation_setup deconstrcalctree -----------------------------------------";
4.249 -"~~~~~ operation_setup deconstrcalctree, args:"; val () = ()
4.250 -
5.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml Thu Apr 22 16:21:23 2021 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,111 +0,0 @@
5.4 -(* Title: tests for libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy
5.5 - Author: Walther Neuper 2015
5.6 - (c) due to copyright terms
5.7 -
5.8 -theory Test_Some imports Isac.Build_Thydata begin
5.9 -ML {* KEStore_Elems.set_ref_thy @{theory};
5.10 - fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}
5.11 -ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
5.12 -*)
5.13 -
5.14 -(* NOTE: Protocol.thy still belongs to a different development at
5.15 - https://github.com/wneuper/libisabelle
5.16 -but Protocol.thy is enclosed in isabisac for testing synchronisation,
5.17 -see Build_Isac.thy *)
5.18 -
5.19 -"-----------------------------------------------------------------------------";
5.20 -"table of contents -----------------------------------------------------------";
5.21 -"-----------------------------------------------------------------------------";
5.22 -"----------- fun initContext, fun initcontext_pbl, fun initcontext_met -------";
5.23 -"-----------------------------------------------------------------------------";
5.24 -"-----------------------------------------------------------------------------";
5.25 -"-----------------------------------------------------------------------------";
5.26 -
5.27 -"----------- fun initContext, fun initcontext_pbl, fun initcontext_met -------";
5.28 -"----------- fun initContext, fun initcontext_pbl, fun initcontext_met -------";
5.29 -"----------- fun initContext, fun initcontext_pbl, fun initcontext_met -------";
5.30 -(* compare isac-java/src/java-tests/isac/bridge/TestContext#testContext *)
5.31 -reset_states ();
5.32 -CalcTree [(["equality (x + 1 = (2::real))", "solveFor x", "solutions L"],
5.33 - ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))];
5.34 -moveActiveRoot 1;
5.35 -autoCalculate 1 CompleteCalc;
5.36 -
5.37 -(*/----- BROKEN WITH CHILD OF 33913fe24685, dropped as irrelevant for PIDE --\* )
5.38 -(*-->ISA: initContext 1 Ptool.Thy_ ([1],Frm); *)
5.39 -val out = initContext 1 Ptool.Thy_ ([1],Frm);
5.40 -if cut_xml out 105 =
5.41 -"(CONTEXTTHY)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . thy_isac_Test-rls-norm_equation"
5.42 -then () else error "initContext 1 Ptool.Thy_ ([1],Frm); CHANGED";
5.43 -
5.44 -(*-->ISA: initContext 1 Ptool.Thy_ ([1],Res); *)
5.45 -val out = initContext 1 Ptool.Thy_ ([1],Res);
5.46 -if cut_xml out 105 =
5.47 -"(CONTEXTTHY)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . thy_isac_Test-rls-Test_simplify"
5.48 -then () else error "initContext 1 Ptool.Thy_ ([1],Res); CHANGED";
5.49 -
5.50 -val ((pt, _), _) = get_calc 1;
5.51 -
5.52 -(*-->ISA: initContext 1 Pbl_ ([1],Res); *)
5.53 -val (p, p_) = ([1], Res)
5.54 -val pp = par_pblobj pt p
5.55 -val chd = initcontext_pbl pt (pp,p_)
5.56 -val out = contextpblOK2xml 1 chd;
5.57 -if cut_xml out 100 = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_test_uni_roottest\n. . "
5.58 -then () else error "initContext 1 Pbl_ ([1],Res); CHANGED";
5.59 -
5.60 -(*-->ISA: initContext 1 Pbl_ ([3,1],Res); *)
5.61 -val (p, p_) = ([3, 1], Res)
5.62 -val pp = par_pblobj pt p
5.63 -val chd = initcontext_pbl pt (pp,p_)
5.64 -val out = contextpblOK2xml 1 chd;
5.65 -if cut_xml out 90 =
5.66 -"(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_test_uni_lin"
5.67 -then () else error "initContext 1 Pbl_ ([3,1],Res); CHANGED";
5.68 -
5.69 -(*-->ISA: initContext 1 Met_ ([1],Res); *)
5.70 -val (p, p_) = ([1], Res)
5.71 -(*interface.sml*)val pp = par_pblobj pt p
5.72 -(*interface.sml*)val chd = initcontext_met pt (pp, p_);
5.73 -val out = contextmetOK2xml 1 chd; (*ERROR was pblID2guh: not for '[Test,squ-equ-test-subpbl1]'*)
5.74 -"~~~~~ fun contextmetOK2xml, args:"; val (calcid, contmet) = (1, chd);
5.75 -"~~~~~ fun xml_of_matchmet, args:"; val (model_ok, pI, scr, pbl, pre) = (contmet);
5.76 -if metID2guh pI =
5.77 -"met_test_squ_sub" then () else error "xml_of_matchmet CHANGED";
5.78 -if cut_xml out 90 = "(CONTEXTMET)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . met_test_squ_sub"
5.79 -then () else error "initContext 1 Met_ ([1],Res); CHANGED";
5.80 -
5.81 -(*-->ISA: initContext 1 Met_ ([3,1],Res); *)
5.82 -val (p, p_) = ([3,1],Res)
5.83 -(*interface.sml*)val pp = par_pblobj pt p
5.84 -(*interface.sml*)val chd = initcontext_met pt (pp, p_);
5.85 -val out = contextmetOK2xml 1 chd;
5.86 -if cut_xml out 91 = "(CONTEXTMET)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . met_test_solvelin"
5.87 -then () else error "initContext 1 Met_ ([3,1],Res); CHANGED";
5.88 -"~~~~~ fun operation_setup init_ctxt, args:"; val (intree) =
5.89 - XML.Elem (("INITCONTEXT", []), [
5.90 - XML.Elem (("CALCID", []), [XML.Text "1"]),
5.91 - XML.Elem (("KETYPE", []), [XML.Text "met"]),
5.92 - XML.Elem (("POSITION", []), [
5.93 - XML.Elem (("INTLIST", []), [
5.94 - XML.Elem (("INT", []), [XML.Text "3"]),
5.95 - XML.Elem (("INT", []), [XML.Text "1"])]),
5.96 - XML.Elem (("POS", []), [XML.Text "Res"])])])
5.97 -fun xxxxx () = (fn intree =>
5.98 - ((let
5.99 - val (ci, ketype, pos) = case intree of
5.100 - XML.Elem (("INITCONTEXT", []), [
5.101 - XML.Elem (("CALCID", []), [XML.Text ci]),
5.102 - ketype as XML.Elem (("KETYPE", []), _),
5.103 - pos as XML.Elem (("POSITION", []), _)])
5.104 - => (int_of_str ci, xml_to_ketype ketype, xml_to_pos pos)
5.105 - | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
5.106 - val result = initContext ci ketype pos
5.107 - in result end)
5.108 - handle ERROR msg => sysERROR2xml 4711 msg)
5.109 - handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")
5.110 -val out = xxxxx () intree;
5.111 -if cut_xml out 91 = "(CONTEXTMET)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . met_test_solvelin"
5.112 -then () else error "operation_setup initContext 1 Met_ ([3,1],Res); CHANGED";
5.113 -( *\----- BROKEN WITH CHILD OF 33913fe24685 ---------------------------------------------------/*)
5.114 -
6.1 --- a/test/Tools/isac/Test_Isac.thy Thu Apr 22 16:21:23 2021 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Apr 22 16:49:41 2021 +0200
6.3 @@ -347,8 +347,6 @@
6.4
6.5 section \<open>further tests additional to src/.. files\<close>
6.6 ML_file "BridgeLibisabelle/use-cases.sml"
6.7 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
6.8 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
6.9
6.10 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
6.11 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
7.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Apr 22 16:21:23 2021 +0200
7.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Apr 22 16:49:41 2021 +0200
7.3 @@ -316,14 +316,11 @@
7.4
7.5 section \<open>further tests additional to src/.. files\<close>
7.6 ML_file "BridgeLibisabelle/use-cases.sml"
7.7 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
7.8 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
7.9
7.10 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
7.11 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
7.12 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
7.13 -ML \<open>
7.14 -\<close> ML \<open>
7.15 +ML \<open>\<close> ML \<open>
7.16 \<close> ML \<open>
7.17 \<close> ML \<open>
7.18 \<close> ML \<open>