1.1 --- a/TODO.md Thu Apr 22 21:34:20 2021 +0200
1.2 +++ b/TODO.md Sat Apr 24 15:59:54 2021 +0200
1.3 @@ -3,11 +3,9 @@
1.4 - or more basic try/can combinators;
1.5 - or more direct ML of intention;
1.6
1.7 -* WN: purge BridgeLibisabelle: eliminate unused code;
1.8 -
1.9 -
1.10 * reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
1.11 -
1.12 + + consider in Build_Thydata: Thy_Hierarchy.insert_errpatIDs
1.13 + + consider in Biegelinie.thy: KEStore_Elems.add_thes,
1.14
1.15 * MW: ML antiqutation @{rule_thm NAME} to produce (Rule.Thm ("NAME", ThmC.numerals_to_Free "NAME"));
1.16
2.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Apr 22 21:34:20 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Sat Apr 24 15:59:54 2021 +0200
2.3 @@ -3,29 +3,27 @@
2.4 (c) due to copyright terms
2.5
2.6 Since libisabelle has been discontinued, this directory will disappear eventually.
2.7 -Remaining code will be located elsewhere.
2.8 +Respective code will be deleted or located elsewhere.
2.9 *)
2.10
2.11 theory BridgeLibisabelle
2.12 imports "$ISABELLE_ISAC/Test_Code/Test_Code"
2.13 begin
2.14 - ML_file "present-tool.sml"
2.15 - ML_file "thy-present.sml"
2.16 - ML_file mathml.sml
2.17 - ML_file datatypes.sml
2.18 - ML_file "pbl-met-hierarchy.sml"
2.19 - ML_file "thy-hierarchy.sml"
2.20 - ML_file "interface-xml.sml"
2.21 - ML_file interface.sml
2.22 -(*
2.23 -*)
2.24 + ML_file "pbl-met-hierarchy.sml" (*keep as a model for browsing pbl and met hierarchies*)
2.25 + ML_file "thy-hierarchy.sml" (*replace by Isabelle/PIDE*)
2.26 + ML_file "present-tool.sml" (*keep tests of interaction Java-frontend <-> Kernel running*)
2.27 + ML_file mathml.sml (*keep tests of interaction Java-frontend <-> Kernel running*)
2.28 + ML_file datatypes.sml (*keep tests of interaction Java-frontend <-> Kernel running*)
2.29 + ML_file "interface-xml.sml" (*keep tests of interaction Java-frontend <-> Kernel running*)
2.30 + ML_file interface.sml (*keep tests of interaction Java-frontend <-> Kernel running*)
2.31
2.32 ML \<open>
2.33 \<close> ML \<open>
2.34 +\<close> ML \<open>
2.35 (*
2.36 - The only code kept for generation of XML (required by Isac's old Java frontend)
2.37 + The only code kept for generation of XML (required by the deprecated Java-frontend)
2.38 is called below.
2.39 - The hierarchies below will still be required in addition to PIDE functionality.
2.40 + The hierarchies will still be required in addition to PIDE functionality.
2.41 *)
2.42 val path = "/home/wneuper/tmp/"; (*~/tmp/pbl/ and ~/tmp/met must be created manyally*)
2.43 \<close> text \<open>(* ATTENTION: outcomment before commits, because the directories must exist *)
3.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 22 21:34:20 2021 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Sat Apr 24 15:59:54 2021 +0200
3.3 @@ -2,20 +2,12 @@
3.4 authors: Walther Neuper 2003, 2016
3.5 (c) due to copyright terms
3.6
3.7 -This code remains for the purpose of running tests
3.8 -which imitate interaction via libisabelle.
3.9 +This code remains in order to
3.10 +keep tests of interaction Java-frontend <-> Kernel running.
3.11 *)
3.12
3.13 -(*------------------------------------------------------------------
3.14 -structure datatypes: DATATYPES =
3.15 -(*structure datatypes =*)
3.16 -struct
3.17 -------------------------------------------------------------------*)
3.18 -
3.19 (*** convert sml-datatypes to xml for kbase ***)
3.20
3.21 -val i = indentation;
3.22 -
3.23 fun calc2xml j (thyID, (scrop, (rewop, _))) =
3.24 indt j ^ "<CALC>\n" ^
3.25 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
3.26 @@ -77,7 +69,7 @@
3.27
3.28 (*** convert sml-datatypes to xml for libisabelle ***)
3.29
3.30 -(** general types: lists, **)
3.31 +(** general types: lists, etc **)
3.32
3.33 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
3.34
3.35 @@ -89,6 +81,7 @@
3.36 XML.Elem (("INTLIST", []), map xml_of_int is)
3.37
3.38 (** isac datatypes **)
3.39 +
3.40 fun xml_of_pos tag (is, pp) =
3.41 XML.Elem ((tag, []), [
3.42 xml_of_ints is,
3.43 @@ -96,11 +89,11 @@
3.44
3.45 fun xml_of_auto (Solve.Steps i) =
3.46 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
3.47 - | xml_of_auto CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
3.48 - | xml_of_auto CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
3.49 - | xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
3.50 - | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
3.51 - | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
3.52 + | xml_of_auto Solve.CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
3.53 + | xml_of_auto Solve.CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
3.54 + | xml_of_auto Solve.CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
3.55 + | xml_of_auto Solve.CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
3.56 + | xml_of_auto Solve.CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
3.57
3.58 fun filterpbl str =
3.59 let fun filt [] = []
3.60 @@ -125,7 +118,6 @@
3.61 fun xml_of_itms itms =
3.62 let
3.63 fun extract (_, _, _, _, itm_) = itm_
3.64 - | extract _ = raise ERROR "xml_of_itms.extract: wrong argument"
3.65 in map (xml_of_itm_ o extract) itms end
3.66
3.67 fun xml_of_precond (status, term) =
3.68 @@ -164,7 +156,7 @@
3.69 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
3.70 xml_of_model gfr pre,
3.71 XML.Elem (("BELONGSTO", []), [
3.72 - XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
3.73 + XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),
3.74 xml_of_spec spec])
3.75
3.76 fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): SpecificationC.T)) =
3.77 @@ -173,7 +165,7 @@
3.78 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
3.79 xml_of_model gfr pre,
3.80 XML.Elem (("BELONGSTO", []), [
3.81 - XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
3.82 + XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),
3.83 xml_of_spec spec])
3.84
3.85 fun xml_of_sub (id, value) =
3.86 @@ -255,7 +247,7 @@
3.87 XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
3.88 | xml_of_tac (Tactic.Check_Postcond pI) =
3.89 XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
3.90 - | xml_of_tac Model_Problem =
3.91 + | xml_of_tac Tactic.Model_Problem =
3.92 XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
3.93 | xml_of_tac (Tactic.Refine_Tacitly pI) =
3.94 XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
3.95 @@ -331,9 +323,3 @@
3.96
3.97 (* for checking output at Frontend *)
3.98 fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode
3.99 -(*------------------------------------------------------------------
3.100 -end
3.101 -open datatypes;
3.102 -------------------------------------------------------------------*)
3.103 -
3.104 -
4.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Thu Apr 22 21:34:20 2021 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Sat Apr 24 15:59:54 2021 +0200
4.3 @@ -2,11 +2,10 @@
4.4 authors: Walther Neuper 2002
4.5 (c) due to copyright terms
4.6
4.7 -This code remains for the purpose of running tests
4.8 -which imitate interaction via libisabelle.
4.9 +This code remains in order to
4.10 +keep tests of interaction Java-frontend <-> Kernel running.
4.11 *)
4.12
4.13 -(**FIXXME.8.03 addUser: clear code, because only CalcTrees distinguished**)
4.14 fun adduserOK2xml (calcid : calcID) (userid : iterID) =
4.15 XML.Elem (("ADDUSER", []),
4.16 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
4.17 @@ -64,24 +63,6 @@
4.18 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
4.19 XML.Elem (("ASMLIST", []), (map xml_of_term_NEW terms))])
4.20
4.21 -(*WN0502 getaccuasmsOK2xml @see ME/ctree: type asms: illdesigned, thus not used*)
4.22 -fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)
4.23 - indt j ^ "<FORMULA>\n"^
4.24 - term2xml j term ^"\n"^
4.25 - indt j ^ "</FORMULA>\n" : xml;
4.26 -fun formulae2xml j [] = ("": xml)
4.27 - | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
4.28 -
4.29 -fun getaccuasmsOK2xml cI asms =
4.30 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
4.31 - "<GETACCUMULATEDASMS>\n" ^
4.32 - " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
4.33 - " <ASMLIST>\n"^
4.34 - formulae2xml (i+i) asms^
4.35 - " </ASMLIST>\n" ^
4.36 - "</GETACCUMULATEDASMS>\n" ^
4.37 - "@@@@@end@@@@@");
4.38 -
4.39 fun getintervalOK (calcid : calcID) fs =
4.40 XML.Elem (("GETELEMENTSFROMTO", []),
4.41 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
4.42 @@ -122,10 +103,6 @@
4.43 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
4.44 XML.Elem (("ERROR", []), [XML.Text e])])
4.45
4.46 -(*. UNCHANGED: the pos' of the active formula autocalculate has been applied at
4.47 - DELETED: last pos' of the succesional sequence of formulae prob. deleted
4.48 - GENERATED: the pos' of the new active formula
4.49 -.*)
4.50 fun autocalculateOK2xml (calcid : calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
4.51 xml_of_calcchanged calcid "AUTOCALC" old del new
4.52 fun autocalculateERROR2xml (calcid : calcID) e =
4.53 @@ -145,7 +122,7 @@
4.54 " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
4.55 "@@@@@end@@@@@");
4.56
4.57 -fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : SpecificationC.T) =
4.58 +fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, _ ,_ ,_ ,_ ,_) : SpecificationC.T) =
4.59 XML.Elem (("MODIFYCALCHEAD", []), [
4.60 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
4.61 XML.Elem (("STATUS", []), [
5.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Apr 22 21:34:20 2021 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Sat Apr 24 15:59:54 2021 +0200
5.3 @@ -12,9 +12,6 @@
5.4 val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)
5.5 val applyTactic : calcID -> Pos.pos' -> Tactic.input -> XML.tree
5.6 val CalcTree : Formalise.T list -> XML.tree
5.7 -(** )
5.8 - val checkContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
5.9 -( **)
5.10 val DEconstrCalcTree : calcID -> XML.tree
5.11 val fetchApplicableTactics : calcID -> int -> Pos.pos' -> XML.tree
5.12 val fetchProposedTactic : calcID -> XML.tree
5.13 @@ -24,9 +21,6 @@
5.14 val getAssumptions : calcID -> Pos.pos' -> XML.tree
5.15 val getFormulaeFromTo : calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree
5.16 val getTactic : calcID -> Pos.pos' -> XML.tree
5.17 -(** )
5.18 - val initContext : calcID -> Ptool.ketype -> Pos.pos' -> XML.tree
5.19 -( **)
5.20 val inputFillFormula: calcID -> string -> XML.tree
5.21 val interSteps : calcID -> Pos.pos' -> XML.tree
5.22 val Iterator : calcID -> XML.tree
5.23 @@ -52,9 +46,6 @@
5.24 val replaceFormula : calcID -> TermC.as_string -> XML.tree
5.25 val requestFillformula : calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
5.26 val resetCalcHead : calcID -> XML.tree
5.27 -(** )
5.28 - val setContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
5.29 -( **)
5.30 val setMethod : calcID -> MethodC.id -> XML.tree
5.31 val setNextTactic : calcID -> Tactic.input -> XML.tree
5.32 val setProblem : calcID -> Problem.id -> XML.tree
6.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Thu Apr 22 21:34:20 2021 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Sat Apr 24 15:59:54 2021 +0200
6.3 @@ -1,10 +1,12 @@
6.4 (* translate formulae from Isabelle-string format to xml-format.
6.5 - TODO implement MathML
6.6 author: Walther Neuper 030701
6.7 (c) isac-team 2003
6.8 +
6.9 +This code remains in order to
6.10 +keep tests of interaction Java-frontend <-> Kernel running.
6.11 *)
6.12
6.13 -type xml = string; (* rm together with old code replaced by XML.tree *)
6.14 +val indentation = 2;
6.15
6.16 (*
6.17 EXCEPT xml-coding issues (2).
6.18 @@ -39,11 +41,11 @@
6.19 | enc (c :: cs) = c :: (enc cs)
6.20 in str |> Symbol.explode |> rm_doublets "^" [] |> enc |> implode end;
6.21
6.22 -val indentation = 2;
6.23 +val i = indentation;
6.24
6.25 (* proper <> is translated to html; however, () creates readable output.. *)
6.26 fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
6.27 - | xmlstr i (XML.Elem (("TERM", []), [xt])) =
6.28 + | xmlstr i (XML.Elem (("TERM", []), [_])) =
6.29 indent i ^ "(" ^ "TERM" ^ ")" ^ "\n" ^
6.30 indent (i + 1) ^ "rm libisabelle: xt NOT DECODED" ^ "\n" ^
6.31 indent i ^ "(/" ^ "TERM" ^ ")" ^ "\n"
6.32 @@ -60,9 +62,6 @@
6.33
6.34 fun strs2xml strs = foldl (op ^) ("", strs);
6.35
6.36 -val indentation = 2;
6.37 -val i = indentation;
6.38 -
6.39 (*WN071016 checked that _all_ Frontend/interface.sml uses this*)
6.40 fun term2xml j t =
6.41 indt (j+i) ^ "<MATHML>\n" ^
6.42 @@ -86,10 +85,10 @@
6.43 ])
6.44
6.45 (*version for TextIO*)
6.46 -fun terms2xml j [] = ""
6.47 +fun terms2xml _ [] = ""
6.48 | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;
6.49 (*version for writeln: extra \n*)
6.50 -fun terms2xml' j [] = ""
6.51 +fun terms2xml' _ [] = ""
6.52 | terms2xml' j [t] = term2xml j t
6.53 | terms2xml' j (t::ts) = term2xml j t ^"\n"^ terms2xml' j ts;
6.54
6.55 @@ -103,8 +102,8 @@
6.56 [XML.Elem (("ISA", []), [XML.Text ct])])
6.57
6.58 (*version for TextIO*)
6.59 -fun cterms2xml j [] = ""
6.60 +fun cterms2xml _ [] = ""
6.61 | cterms2xml j (t::ts) = cterm2xml j t ^ cterms2xml j ts;
6.62 (*version for writeln: extra \n*)
6.63 -fun cterms2xml' j [] = ""
6.64 +fun cterms2xml' _ [] = ""
6.65 | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;
7.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Thu Apr 22 21:34:20 2021 +0200
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sat Apr 24 15:59:54 2021 +0200
7.3 @@ -9,83 +9,72 @@
7.4 *)
7.5 signature PROBLEM_METHOD_HIERARCHY =
7.6 sig
7.7 - val format_pblIDl : string list list -> string
7.8 eqtype filepath
7.9 - val file2str: filepath -> Thy_Present.filename -> string
7.10 - val hierarchy_met: MethodC.T Store.node list -> xml
7.11 - val hierarchy_pbl: Problem.T Store.node list -> xml
7.12 - val i: int
7.13 -
7.14 + eqtype filename
7.15 + type xml
7.16 val pbl_hierarchy2file: filepath -> unit
7.17 val met_hierarchy2file: filepath -> unit
7.18 -
7.19 - val str2file: Thy_Present.filename -> string -> unit
7.20 - val update_metdata: MethodC.T -> Error_Pattern_Def.T list -> MethodC.T
7.21 val update_metpair: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id
7.22 +\<^isac_test>\<open>
7.23 + val str2file: filename -> string -> unit
7.24 +\<close>
7.25 end
7.26
7.27 (**)
7.28 -structure Pbl_Met_Hierarchy(**): PROBLEM_METHOD_HIERARCHY(**) =
7.29 +structure Pbl_Met_Hierarchy(**): PROBLEM_METHOD_HIERARCHY(*AUTHOR*) =
7.30 struct
7.31 (**)
7.32
7.33 -fun format_pblID strl = enclose " [" "]" (commas_quote strl);
7.34 -fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
7.35 +type filepath = string;
7.36 +type filename = string;
7.37
7.38 -type filepath = string;
7.39 +type xml = string; (* rm together with old code replaced by XML.tree *)
7.40 +val indentation = 2;
7.41 +fun hierarchy_pbl h =
7.42 + let
7.43 + val j = indentation
7.44 + fun nd i p (Store.Node (id,[{guh,...} : Problem.T],ns)) =
7.45 + let val p' = Pos.lev_on p
7.46 + in (indt i) ^ "<NODE>\n" ^
7.47 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
7.48 + (indt (i+j)) ^ "<NO> " (*on this level*) ^
7.49 + (string_of_int o last_elem) p' ^ " </NO>\n" ^
7.50 + (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
7.51 + " </CONTENTREF>\n" ^
7.52 + (nds (i+j) (Pos.lev_dn p') ns) ^
7.53 + (indt i) ^ "</NODE>\n"
7.54 + end
7.55 + | nd _ _ _ = raise ERROR "hierarchy_pbl"
7.56 + and nds _ _ [] = ""
7.57 + | nds i p (n::ns) = (nd i p n) ^ (nds i (Pos.lev_on p) ns);
7.58 + in nds j [0] h : xml end;
7.59
7.60 -fun file2str path fnm =
7.61 - let
7.62 - val file = TextIO.openIn (path ^ fnm)
7.63 - val str = TextIO.inputAll file
7.64 - in TextIO.closeIn file; str end
7.65 +fun hierarchy_met h =
7.66 + let
7.67 + val j = indentation
7.68 + fun nd i p (Store.Node (id,[{guh,...} : MethodC.T],ns)) =
7.69 + let val p' = Pos.lev_on p
7.70 + in (indt i) ^ "<NODE>\n" ^
7.71 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
7.72 + (indt (i+j)) ^ "<NO> " (*on this level*) ^
7.73 + (string_of_int o last_elem) p' ^ " </NO>\n" ^
7.74 + (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
7.75 + " </CONTENTREF>\n" ^
7.76 + (nds (i+j) (Pos.lev_dn p') ns) ^
7.77 + (indt i) ^ "</NODE>\n"
7.78 + end
7.79 + | nd _ _ _ = raise ERROR "hierarchy_met"
7.80 + and nds _ _ [] = ""
7.81 + | nds i p (n::ns) = (nd i p n) ^ (nds i (Pos.lev_on p) ns);
7.82 + in nds j [0] h : xml end;
7.83
7.84 -fun str2file (fnm : Thy_Present.filename) (str : string) =
7.85 +fun str2file (fnm : filename) (str : string) =
7.86 let val file = TextIO.openOut fnm
7.87 in
7.88 TextIO.output (file, str);
7.89 TextIO.flushOut file;
7.90 TextIO.closeOut file
7.91 end
7.92 -
7.93 -(*
7.94 - create XML for the tree structure of problem-patterns.
7.95 -*)
7.96 -fun hierarchy_pbl h =
7.97 - let val j = indentation
7.98 - fun nd i p (Store.Node (id,[n as {guh,...} : Problem.T],ns)) =
7.99 - let val p' = Pos.lev_on p
7.100 - in (indt i) ^ "<NODE>\n" ^
7.101 - (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
7.102 - (indt (i+j)) ^ "<NO> " (*on this level*) ^
7.103 - (string_of_int o last_elem) p' ^ " </NO>\n" ^
7.104 - (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
7.105 - " </CONTENTREF>\n" ^
7.106 - (nds (i+j) (Pos.lev_dn p') ns) ^
7.107 - (indt i) ^ "</NODE>\n"
7.108 - end
7.109 - and nds _ _ [] = ""
7.110 - | nds i p (n::ns) = (nd i p n) ^ (nds i (Pos.lev_on p) ns);
7.111 - in nds j [0] h : xml end;
7.112 -fun hierarchy_met h =
7.113 - let val j = indentation
7.114 - fun nd i p (Store.Node (id,[n as {guh,...} : MethodC.T],ns)) =
7.115 - let val p' = Pos.lev_on p
7.116 - in (indt i) ^ "<NODE>\n" ^
7.117 - (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
7.118 - (indt (i+j)) ^ "<NO> " (*on this level*) ^
7.119 - (string_of_int o last_elem) p' ^ " </NO>\n" ^
7.120 - (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
7.121 - " </CONTENTREF>\n" ^
7.122 - (nds (i+j) (Pos.lev_dn p') ns) ^
7.123 - (indt i) ^ "</NODE>\n"
7.124 - end
7.125 - and nds _ _ [] = ""
7.126 - | nds i p (n::ns) = (nd i p n) ^ (nds i (Pos.lev_on p) ns);
7.127 - in nds j [0] h : xml end;
7.128 -(* (writeln o hierarchy_pbl) (!ptyps);
7.129 - *)
7.130 -
7.131 fun pbl_hierarchy2file path =
7.132 str2file (path ^ "pbl_hierarchy.xml")
7.133 ("<NODE>\n" ^
7.134 @@ -94,7 +83,6 @@
7.135 " <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^
7.136 (hierarchy_pbl (get_ptyps ())) ^
7.137 "</NODE>");
7.138 -
7.139 fun met_hierarchy2file path =
7.140 str2file (path ^ "met_hierarchy.xml")
7.141 ("<NODE>\n" ^
7.142 @@ -104,18 +92,6 @@
7.143 (hierarchy_met (get_mets ())) ^
7.144 "</NODE>");
7.145
7.146 -(**.create the xml-files for the pbls, mets from the hierarchy.**)
7.147 -
7.148 -(*.format a problem in xml for presentation on the problem browser;
7.149 - new version with <KESTOREREF>s -- not used because linking
7.150 - requires elements (rls, calc, ...) to be reorganized.*)
7.151 -(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
7.152 -fun pbl2term thy (pblRD: Problem.id) = (*WN120405.TODO.txt*)
7.153 - TermC.str2term ("Problem (" ^ (get_thy o Context.theory_name) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
7.154 -(* term2str (pbl2term (Thy_Info_get_theory "Isac_Knowledge") ["equations", "univariate", "normalise"]);
7.155 -val it = "Problem (Isac, [normalise, univariate, equations])" : string
7.156 -*)
7.157 -val i = indentation;
7.158
7.159 fun update_metdata
7.160 ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: MethodC.T)
8.1 --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml Thu Apr 22 21:34:20 2021 +0200
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml Sat Apr 24 15:59:54 2021 +0200
8.3 @@ -1,20 +1,23 @@
8.4 (* Title: BridgeLibisabelle/present-tool.sml
8.5 Author: Walther Neuper
8.6 (c) due to copyright terms
8.7 +
8.8 +This code remains in order to
8.9 +keep tests of interaction Java-frontend <-> Kernel running.
8.10 *)
8.11
8.12 signature PRESENTATION_TOOL =
8.13 sig
8.14 - datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
8.15 +
8.16 + type ketype
8.17 val ketype2str: ketype -> string
8.18 - val ketype2str': ketype -> string
8.19 val str2ketype': string -> ketype
8.20
8.21 type kestoreID
8.22 val pblID2guh : Problem.id -> Check_Unique.id
8.23 val metID2guh : MethodC.id -> Check_Unique.id
8.24 val kestoreID2guh : ketype -> kestoreID -> Check_Unique.id
8.25 - val guh2kestoreID : Check_Unique.id -> string list (* for interface.sml *)
8.26 + val guh2kestoreID : Check_Unique.id -> string list
8.27 end
8.28
8.29 (**)
8.30 @@ -59,10 +62,6 @@
8.31 | ketype2str Thy_ = "Thy_"
8.32 | ketype2str Pbl_ = "Pbl_"
8.33 | ketype2str Met_ = "Met_";
8.34 -fun ketype2str' Exp_ = "Example"
8.35 - | ketype2str' Thy_ = "Theory"
8.36 - | ketype2str' Pbl_ = "Problem"
8.37 - | ketype2str' Met_ = "MethodC";
8.38 (* for conversion from XML *)
8.39 fun str2ketype' "exp" = Exp_
8.40 | str2ketype' "thy" = Thy_
8.41 @@ -81,7 +80,7 @@
8.42 handle _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
8.43 fun kestoreID2guh Pbl_ kestoreID = pblID2guh kestoreID
8.44 | kestoreID2guh Met_ kestoreID = metID2guh kestoreID
8.45 - | kestoreID2guh ketype kestoreID =
8.46 - raise ERROR ("kestoreID2guh: \"" ^ ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");
8.47 + | kestoreID2guh ketyp kestoreID =
8.48 + raise ERROR ("kestoreID2guh: \"" ^ ketype2str ketyp ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");
8.49
8.50 (**)end(**);
9.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 22 21:34:20 2021 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sat Apr 24 15:59:54 2021 +0200
9.3 @@ -2,7 +2,7 @@
9.4 Author: Walther Neuper 0601
9.5 (c) due to copyright terms
9.6
9.7 -Tools for Build_Thydata of theorems and rule-sets defined in Knowledge/ and ProgLang/
9.8 +Tools to Build_Thydata of theorems and rule-sets defined in Knowledge/ and ProgLang/
9.9 *)
9.10
9.11 signature THEORY_HIERARCHY =
9.12 @@ -15,15 +15,15 @@
9.13 (Thy_Write.theID * Thy_Write.thydata) list
9.14 val collect_thms: string -> theory -> (Thy_Write.theID * Thy_Write.thydata) list
9.15
9.16 - val hierarchy_guh: 'a Store.T -> string
9.17 val insert_errpatIDs: 'a -> Thy_Write.theID -> Error_Pattern_Def.id list ->
9.18 Thy_Write.thydata * Thy_Write.theID
9.19 - val update_hrls: Thy_Write.thydata -> Error_Pattern_Def.id list -> Thy_Write.thydata
9.20
9.21 + val thms_of_rls : Rule_Set.T -> Rule.rule list
9.22 val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->
9.23 (string * thm) list
9.24
9.25 \<^isac_test>\<open>
9.26 + val hierarchy_guh: 'a Store.T -> string
9.27 val get_fun_ids: theory -> (string * typ) list
9.28 \<close>
9.29 end
9.30 @@ -70,7 +70,7 @@
9.31 in (theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID, coursedesign = [],
9.32 mathauthors = ["isac-team"], fillpats = [], thm = thm})
9.33 end;
9.34 -fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.id * Rule_Set.T) =
9.35 +fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, _): ThyC.id * Rule_Set.T) =
9.36 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Thy_Write.theID
9.37 in (theID, Thy_Write.Hrls {guh = Thy_Write.theID2guh theID, coursedesign = [],
9.38 mathauthors = ["isac-team"], thy_rls = thy_rls})
9.39 @@ -80,15 +80,21 @@
9.40 in (theID, Thy_Write.Hcal {guh = Thy_Write.theID2guh theID, coursedesign=[],
9.41 mathauthors = ["isac-team"], calc = cal})
9.42 end;
9.43 -fun makeHord (part : string, thyID : ThyC.id) (ordID, ord) =
9.44 - let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Thy_Write.theID
9.45 - in (theID, Thy_Write.Hord {guh = Thy_Write.theID2guh theID, coursedesign=[],
9.46 - mathauthors = ["isac-team"], ord = ord})
9.47 - end;
9.48 +
9.49 +(* get all theorems in a rule set (recursivley containing rule sets) *)
9.50 +fun thm_of_rule Rule.Erule = []
9.51 + | thm_of_rule (thm as Rule.Thm _) = [thm]
9.52 + | thm_of_rule (Rule.Eval _) = []
9.53 + | thm_of_rule (Rule.Cal1 _) = []
9.54 + | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls
9.55 +and thms_of_rls Rule_Set.Empty = []
9.56 + | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map thm_of_rule)) rules
9.57 + | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules
9.58 + | thms_of_rls (Rule_Set.Rrls _) = []
9.59
9.60 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
9.61 fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
9.62 - |> map (Thy_Present.thms_of_rls o #2 o #2)
9.63 + |> map (thms_of_rls o #2 o #2)
9.64 |> flat
9.65 |> map (ThmC.revert_sym_rule thy)
9.66 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
9.67 @@ -105,9 +111,8 @@
9.68 fun collect_cals (part, thy') =
9.69 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
9.70 in map (makeHcal (part, thy')) cals end;
9.71 -fun collect_ords (part, thy') =
9.72 - let val thy = ThyC.get_theory thy'
9.73 - in [(*TODO.WN060120 rew_ord, Eval*)]:(Thy_Write.theID * Thy_Write.thydata) list end;
9.74 +fun collect_ords (_, _) =
9.75 + [(*TODO.WN060120 rew_ord, Eval*)]:(Thy_Write.theID * Thy_Write.thydata) list
9.76
9.77 (* parts are: Isabelle | IsacKnowledge | IsacScripts, see Know_Store.thy *)
9.78 fun collect_part part parent thys =
9.79 @@ -128,39 +133,6 @@
9.80 end
9.81
9.82
9.83 -(** create an xml representation for thehier: hierarchy of entries + files per entry **)
9.84 -
9.85 -(* create an xml-hierarchy where the filname is created from the guh;
9.86 - ad DTD: a NODE contains an ID and zero or more NODEs*)
9.87 -fun hierarchy_guh h =
9.88 - let
9.89 - val i = indentation
9.90 - val j = indentation
9.91 - fun node i p theID (Store.Node (id, _, ns)) =
9.92 - let
9.93 - val p' = Pos.lev_on p
9.94 - val theID' = theID @ [id]
9.95 - in
9.96 - (indt i) ^ "<NODE>\n" ^
9.97 - (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
9.98 - (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
9.99 - (indt (i+j)) ^ "<CONTENTREF> " ^ Thy_Write.theID2guh theID' ^ " </CONTENTREF>\n" ^
9.100 - (nodes (i+j) (Pos.lev_dn p') theID' ns) ^
9.101 - (indt i) ^ "</NODE>\n"
9.102 - end
9.103 - and nodes _ _ _ [] = ""
9.104 - | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Pos.lev_on p) theID ns);
9.105 - in nodes j [0] [] h end;
9.106 -
9.107 -fun thy_hierarchy2file (path: Pbl_Met_Hierarchy.filepath) =
9.108 - Pbl_Met_Hierarchy.str2file (path ^ "thy_hierarchy.xml")
9.109 - ("<NODE>\n" ^
9.110 - " <ID> theory hierarchy </ID>\n" ^
9.111 - " <NO> 1 </NO>\n" ^
9.112 - " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
9.113 - (hierarchy_guh (get_thes ())) ^
9.114 - "</NODE>");
9.115 -
9.116 (* for dialog-authoring *)
9.117 fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
9.118 let
9.119 @@ -182,11 +154,35 @@
9.120 end
9.121 | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
9.122
9.123 -fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)
9.124 +fun insert_errpatIDs _(*thy*) theID errpatIDs = (* TODO: redo like insert_fillpatts *)
9.125 let
9.126 val hrls = Thy_Read.from_store theID
9.127 val hrls' = update_hrls hrls errpatIDs
9.128 handle ERROR _ => raise ERROR ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
9.129 in (hrls', theID) end
9.130
9.131 +(*keep tests of interaction Java-frontend <-> Kernel running*)
9.132 +\<^isac_test>\<open>
9.133 +(* create an xml-hierarchy where the filname is created from the guh *)
9.134 +val indentation = 2;
9.135 +fun hierarchy_guh h =
9.136 + let
9.137 + val j = indentation
9.138 + fun node i p theID (Store.Node (id, _, ns)) =
9.139 + let
9.140 + val p' = Pos.lev_on p
9.141 + val theID' = theID @ [id]
9.142 + in
9.143 + (indt i) ^ "<NODE>\n" ^
9.144 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
9.145 + (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
9.146 + (indt (i+j)) ^ "<CONTENTREF> " ^ Thy_Write.theID2guh theID' ^ " </CONTENTREF>\n" ^
9.147 + (nodes (i+j) (Pos.lev_dn p') theID' ns) ^
9.148 + (indt i) ^ "</NODE>\n"
9.149 + end
9.150 + and nodes _ _ _ [] = ""
9.151 + | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Pos.lev_on p) theID ns);
9.152 + in nodes j [0] [] h end;
9.153 +\<close>
9.154 +
9.155 (**)end(**)
10.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-present.sml Thu Apr 22 21:34:20 2021 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,35 +0,0 @@
10.4 -(*
10.5 - authors: Walther Neuper 2002, 2006
10.6 - (c) due to copyright terms
10.7 -
10.8 -tools for rewriting, reverse rewriting, context to thy concerning rewriting
10.9 -*)
10.10 -
10.11 -signature THEORY_DATA_PRESENTATION =
10.12 -sig
10.13 - eqtype filename
10.14 -
10.15 - val guh2filename : Check_Unique.id -> filename
10.16 - val thms_of_rls : Rule_Set.T -> Rule.rule list
10.17 -end
10.18 -(**)
10.19 -structure Thy_Present(**): THEORY_DATA_PRESENTATION(**) =
10.20 -struct
10.21 -(**)
10.22 -
10.23 -type filename = string;
10.24 -
10.25 -(* get all theorems in a rule set (recursivley containing rule sets) *)
10.26 -fun thm_of_rule Rule.Erule = []
10.27 - | thm_of_rule (thm as Rule.Thm _) = [thm]
10.28 - | thm_of_rule (Rule.Eval _) = []
10.29 - | thm_of_rule (Rule.Cal1 _) = []
10.30 - | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls
10.31 -and thms_of_rls Rule_Set.Empty = []
10.32 - | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map thm_of_rule)) rules
10.33 - | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules
10.34 - | thms_of_rls (Rule_Set.Rrls _) = []
10.35 -
10.36 -fun guh2filename guh = guh ^ ".xml";
10.37 -
10.38 -(**)end(**)
11.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Apr 22 21:34:20 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sat Apr 24 15:59:54 2021 +0200
11.3 @@ -227,16 +227,6 @@
11.4 TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)
11.5 \<close>
11.6
11.7 -subsection \<open>Generate XML representation from SML (data in Know_Store)\<close>
11.8 -text \<open>
11.9 - See the wiki
11.10 - http://www.ist.tugraz.at/isac/Generate_representations_for_ISAC_Knowledge#Step_1:_Generate_XML_representation_from_SML
11.11 -
11.12 - val path = "/tmp/xmldata/";
11.13 - pbl_hierarchy2file (path ^ "pbl/");
11.14 - met_hierarchy2file (path ^ "met/");
11.15 -\<close>
11.16 -
11.17 section \<open>Link KEStore_Elems to completed IsacKnowledge\<close>
11.18 ML \<open>KEStore_Elems.set_ref_thy @{theory}\<close>
11.19
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Apr 22 21:34:20 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sat Apr 24 15:59:54 2021 +0200
12.3 @@ -770,13 +770,7 @@
12.4 (Context.theory_name @{theory}, d2_polyeq_abcFormula_simplify)),
12.5 ("d3_polyeq_simplify", (Context.theory_name @{theory}, d3_polyeq_simplify)),
12.6 ("d4_polyeq_simplify", (Context.theory_name @{theory}, d4_polyeq_simplify))]\<close>
12.7 -ML\<open>
12.8 -(*------------------------problems------------------------*)
12.9 -(*
12.10 -(get_pbt ["degree_2", "polynomial", "univariate", "equation"]);
12.11 -show_ptyps();
12.12 -*)
12.13 -\<close>
12.14 +
12.15 setup \<open>KEStore_Elems.add_pbts
12.16 [(Problem.prep_input thy "pbl_equ_univ_poly" [] Problem.id_empty
12.17 (["polynomial", "univariate", "equation"],
13.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Apr 22 21:34:20 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sat Apr 24 15:59:54 2021 +0200
13.3 @@ -122,12 +122,7 @@
13.4 ("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))]\<close>
13.5
13.6 subsection \<open>problems\<close>
13.7 -ML \<open>
13.8 -(*
13.9 -(get_pbt ["rat", "rootX", "univariate", "equation"]);
13.10 -show_ptyps();
13.11 -*)
13.12 -\<close>
13.13 +
13.14 setup \<open>KEStore_Elems.add_pbts
13.15 [(Problem.prep_input thy "pbl_equ_univ_root_sq_rat" [] Problem.id_empty
13.16 (["rat", "sq", "rootX", "univariate", "equation"],
14.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 22 21:34:20 2021 +0200
14.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sat Apr 24 15:59:54 2021 +0200
14.3 @@ -38,7 +38,7 @@
14.4
14.5 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
14.6 val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
14.7 - |> map (Thy_Present.thms_of_rls o #2 o #2)
14.8 + |> map (Thy_Hierarchy.thms_of_rls o #2 o #2)
14.9 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
14.10 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
14.11 |> flat
15.1 --- a/test/Tools/isac/Test_Some.thy Thu Apr 22 21:34:20 2021 +0200
15.2 +++ b/test/Tools/isac/Test_Some.thy Sat Apr 24 15:59:54 2021 +0200
15.3 @@ -180,7 +180,7 @@
15.4 \<close> ML \<open>
15.5 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
15.6 val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
15.7 - |> map (Thy_Present.thms_of_rls o #2 o #2)
15.8 + |> map (Thy_Hierarchy.thms_of_rls o #2 o #2)
15.9 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
15.10 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
15.11 |> flat