1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Apr 22 12:53:26 2021 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Apr 22 16:21:23 2021 +0200
1.3 @@ -11,8 +11,8 @@
1.4 begin
1.5 ML_file "present-tool.sml"
1.6 ML_file "thy-present.sml"
1.7 - ML_file mathml.sml
1.8 - ML_file datatypes.sml
1.9 +(**)ML_file mathml.sml(**)
1.10 +(**)ML_file datatypes.sml(**)
1.11 ML_file "pbl-met-hierarchy.sml"
1.12 ML_file "thy-hierarchy.sml"
1.13 ML_file "interface-xml.sml"
2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 22 12:53:26 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 22 16:21:23 2021 +0200
2.3 @@ -8,7 +8,6 @@
2.4 val authors2xml : int -> string -> string list -> xml
2.5 val calc2xml : int -> ThyC.id * Rule_Def.calc -> xml
2.6 val calcrefs2xml : int -> ThyC.id * Rule_Def.calc list -> xml
2.7 - val contthy2xml : int -> Thy_Present.contthy -> xml
2.8 val extref2xml : int -> string -> string -> xml
2.9 val filterpbl :
2.10 ''a -> (''a * (Term.term * Term.term)) list -> Term.term list
2.11 @@ -681,75 +680,6 @@
2.12 XML.Elem (("GUH", []), [XML.Text guh])])
2.13 end
2.14
2.15 -fun xml_of_contthy Thy_Present.EContThy =
2.16 - raise ERROR "contthy2xml called with EContThy"
2.17 -
2.18 - | xml_of_contthy (Thy_Present.ContThm {thyID, thm, applto, applat, reword,
2.19 - asms,lhs, rhs, result, resasms, asmrls}) =
2.20 - XML.Elem (("CONTEXTDATA", []), [
2.21 - XML.Elem (("GUH", []), [XML.Text thm]),
2.22 - XML.Elem (("APPLTO", []), [xml_of_term applto]),
2.23 - XML.Elem (("APPLAT", []), [xml_of_term applat]),
2.24 - XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
2.25 - XML.Elem (("ID", []), [XML.Text reword])]),
2.26 - XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
2.27 - XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
2.28 - XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
2.29 - XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
2.30 - XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
2.31 - XML.Elem (("RESULT", []), [xml_of_term result]),
2.32 - XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
2.33 - XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
2.34 -
2.35 - | xml_of_contthy (Thy_Present.ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
2.36 - reword, asms, lhs, rhs, result, resasms, asmrls}) =
2.37 - XML.Elem (("CONTEXTDATA", []), [
2.38 - XML.Elem (("GUH", []), [XML.Text thm]),
2.39 - XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
2.40 - xml_of_cterm (Env.subst2str' bdvs)]),
2.41 - XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
2.42 - XML.Elem (("APPLTO", []), [xml_of_term applto]),
2.43 - XML.Elem (("APPLAT", []), [xml_of_term applat]),
2.44 - XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
2.45 - XML.Elem (("ID", []), [XML.Text reword])]),
2.46 - XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
2.47 - XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
2.48 - XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
2.49 - XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
2.50 - XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
2.51 - XML.Elem (("RESULT", []), [xml_of_term result]),
2.52 - XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
2.53 - XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
2.54 -
2.55 - | xml_of_contthy (Thy_Present.ContRls {thyID = _, rls, applto, result, asms}) =
2.56 - XML.Elem (("CONTEXTDATA", []), [
2.57 - XML.Elem (("GUH", []), [XML.Text rls]),
2.58 - XML.Elem (("APPLTO", []), [xml_of_term applto]),
2.59 - XML.Elem (("RESULT", []), [xml_of_term result]),
2.60 - XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
2.61 -
2.62 - | xml_of_contthy (Thy_Present.ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
2.63 - XML.Elem (("CONTEXTDATA", []), [
2.64 - XML.Elem (("GUH", []), [XML.Text rls]),
2.65 - XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
2.66 - xml_of_cterm (Env.subst2str' bdvs)]),
2.67 - XML.Elem (("INSTANTIATED", []), [xml_of_cterm (Env.subst2str' bdvs)]),
2.68 - XML.Elem (("APPLTO", []), [xml_of_term applto]),
2.69 - XML.Elem (("RESULT", []), [xml_of_term result]),
2.70 - XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
2.71 -
2.72 - | xml_of_contthy (Thy_Present.ContNOrew {thyID = _, thm_rls, applto}) =
2.73 - XML.Elem (("CONTEXTDATA", []), [
2.74 - XML.Elem (("GUH", []), [XML.Text thm_rls]),
2.75 - XML.Elem (("APPLTO", []), [xml_of_term applto])])
2.76 -
2.77 - | xml_of_contthy (Thy_Present.ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
2.78 - XML.Elem (("CONTEXTDATA", []), [
2.79 - XML.Elem (("GUH", []), [XML.Text thm_rls]),
2.80 - XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
2.81 - xml_of_cterm (Env.subst2str' bdvs)]),
2.82 - XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
2.83 - XML.Elem (("APPLTO", []), [xml_of_term applto])])
2.84
2.85 fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =
2.86 XML.Elem (("CONTEXTDATA", []), [
3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Thu Apr 22 12:53:26 2021 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Thu Apr 22 16:21:23 2021 +0200
3.3 @@ -165,11 +165,6 @@
3.4 XML.Text (if complete then "complete" else "incomplete")]),
3.5 xml_of_modspec chd])
3.6
3.7 -fun contextthyOK2xml calcid contthy =
3.8 - XML.Elem (("CONTEXTTHY", []), [
3.9 - XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.10 - xml_of_contthy contthy])
3.11 -
3.12 fun contextpblOK2xml calcid contpbl =
3.13 XML.Elem (("CONTEXTPBL", []), [
3.14 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
4.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Apr 22 12:53:26 2021 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Apr 22 16:21:23 2021 +0200
4.3 @@ -12,7 +12,9 @@
4.4 val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)
4.5 val applyTactic : calcID -> Pos.pos' -> Tactic.input -> XML.tree
4.6 val CalcTree : Formalise.T list -> XML.tree
4.7 +(** )
4.8 val checkContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
4.9 +( **)
4.10 val DEconstrCalcTree : calcID -> XML.tree
4.11 val fetchApplicableTactics : calcID -> int -> Pos.pos' -> XML.tree
4.12 val fetchProposedTactic : calcID -> XML.tree
4.13 @@ -22,7 +24,9 @@
4.14 val getAssumptions : calcID -> Pos.pos' -> XML.tree
4.15 val getFormulaeFromTo : calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree
4.16 val getTactic : calcID -> Pos.pos' -> XML.tree
4.17 +(** )
4.18 val initContext : calcID -> Ptool.ketype -> Pos.pos' -> XML.tree
4.19 +( **)
4.20 val inputFillFormula: calcID -> string -> XML.tree
4.21 val interSteps : calcID -> Pos.pos' -> XML.tree
4.22 val Iterator : calcID -> XML.tree
4.23 @@ -48,7 +52,9 @@
4.24 val replaceFormula : calcID -> TermC.as_string -> XML.tree
4.25 val requestFillformula : calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
4.26 val resetCalcHead : calcID -> XML.tree
4.27 +(** )
4.28 val setContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
4.29 +( **)
4.30 val setMethod : calcID -> MethodC.id -> XML.tree
4.31 val setNextTactic : calcID -> Tactic.input -> XML.tree
4.32 val setProblem : calcID -> Problem.id -> XML.tree
4.33 @@ -293,6 +299,7 @@
4.34 in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end)
4.35 handle _ => sysERROR2xml cI "error in kernel 11";
4.36
4.37 +(** )
4.38 (* set the UContext determined on a knowledgebrowser to the current calc
4.39 WN0825: not implemented in isac-java.
4.40 Recalling the state of development after summer-term 2006 (Robert Koenishofer et.al.):
4.41 @@ -363,6 +370,7 @@
4.42 else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"
4.43 end
4.44 ) handle _ => sysERROR2xml cI "setContext: met_ ???")
4.45 +( **)
4.46
4.47
4.48 (* specify the MethodC at the activeFormula and return a CalcHead containing the Guard.
4.49 @@ -549,6 +557,7 @@
4.50 in iteratorOK2xml cI ip' end)
4.51 handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 30"
4.52
4.53 +(** )
4.54 (*.initContext Thy_ is conceptually impossible at [Pbl,Met]
4.55 and at positions with Check_Postcond and End_Trans;
4.56 at possible pos's there can be NO rewrite (returned as a context, too).*)
4.57 @@ -636,6 +645,7 @@
4.58 in contextmetOK2xml cI chd end
4.59 ) handle _ => sysERROR2xml cI "error in kernel 36")
4.60 | str => sysERROR2xml cI ("checkContext: str = " ^ str)
4.61 +( **)
4.62
4.63 (*
4.64 for an Error_Pattern.id find "(fill_in_id * fill_in) list"
5.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 22 12:53:26 2021 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 22 16:21:23 2021 +0200
5.3 @@ -2,7 +2,7 @@
5.4 Author: Walther Neuper 0601
5.5 (c) due to copyright terms
5.6
5.7 -Export theory-data "thehier" to xml.
5.8 +Tools for Build_Thydata of theorems and rule-sets defined in Knowledge/ and ProgLang/
5.9 *)
5.10
5.11 signature THEORY_HIERARCHY =
5.12 @@ -20,36 +20,11 @@
5.13 Thy_Write.thydata * Thy_Write.theID
5.14 val update_hrls: Thy_Write.thydata -> Error_Pattern_Def.id list -> Thy_Write.thydata
5.15
5.16 - val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Thy_Write.theID * Thy_Write.thydata
5.17 - val makeHord: string * ThyC.id -> string * Rule_Def.rew_ord_ ->
5.18 - Thy_Write.theID * Thy_Write.thydata
5.19 - val makeHrls: string -> Rule_Set.id * (ThyC.id * Rule_Def.rule_set) ->
5.20 - Thy_Write.theID * Thy_Write.thydata
5.21 - val makeHthm: string * ThyC.id -> thm -> Thy_Write.theID * Thy_Write.thydata
5.22 - val make_cal: theory -> Rule_Def.calc -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
5.23 - val make_isa: theory -> ThyC.id * ThyC.id -> Thy_Write.authors ->
5.24 - Thy_Write.thydata * Thy_Write.theID
5.25 - val make_ord: theory -> Rule_Def.rew_ord_ -> Thy_Write.authors ->
5.26 - Thy_Write.thydata * Thy_Write.theID
5.27 - val make_rls: theory -> Rule_Def.rule_set -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
5.28 - val make_thm: theory -> string -> string * thm -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
5.29 - val make_thy: theory -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
5.30 -
5.31 - val show_thes: unit -> unit
5.32 -
5.33 - val thes2file: Pbl_Met_Hierarchy.filepath -> unit
5.34 - val thms_of: theory -> thm list
5.35 val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->
5.36 (string * thm) list
5.37 - val thy_hierarchy2file: Pbl_Met_Hierarchy.filepath -> unit
5.38 - val thydata2file: Pbl_Met_Hierarchy.filepath -> Pos.pos -> Thy_Write.theID -> Thy_Write.thydata -> unit
5.39 - val thydata2xml: Thy_Write.theID * Thy_Write.thydata -> xml
5.40 +
5.41 \<^isac_test>\<open>
5.42 val get_fun_ids: theory -> (string * typ) list
5.43 - val thenode: Pbl_Met_Hierarchy.filepath -> string list -> Pos.pos -> (Pbl_Met_Hierarchy.filepath -> Pos.pos ->
5.44 - string list -> 'a -> 'b) -> 'a Store.node -> unit
5.45 - val thenodes: Pbl_Met_Hierarchy.filepath -> string list -> Pos.pos -> (Pbl_Met_Hierarchy.filepath -> Pos.pos ->
5.46 - string list -> 'a -> 'b) -> 'a Store.T -> unit
5.47 \<close>
5.48 end
5.49
5.50 @@ -152,8 +127,6 @@
5.51 thm = thm})
5.52 end
5.53
5.54 -fun show_thes () = (writeln o Pbl_Met_Hierarchy.format_pblIDl o (Store.scan [])) (get_thes ());
5.55 -
5.56
5.57 (** create an xml representation for thehier: hierarchy of entries + files per entry **)
5.58
5.59 @@ -188,120 +161,6 @@
5.60 (hierarchy_guh (get_thes ())) ^
5.61 "</NODE>");
5.62
5.63 -(* create the xml-files for the thydata in the hierarchy *)
5.64 -val i = indentation;
5.65 -(* analoguous to 'fun met2xml' *)
5.66 -fun thydata2xml (theID: Thy_Write.theID, Thy_Write.Html {guh, coursedesign, mathauthors, html}) =
5.67 - "<HTMLDATA>\n" ^
5.68 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
5.69 - id2xml i theID ^
5.70 - indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
5.71 - authors2xml i "MATHAUTHORS" mathauthors ^
5.72 - authors2xml i "COURSEDESIGNS" coursedesign ^
5.73 - "</HTMLDATA>\n" : xml
5.74 - | thydata2xml (theID, Thy_Write.Hthm {guh, coursedesign, mathauthors, fillpats(*TODO?*), thm}) =
5.75 - "<THEOREMDATA>\n" ^
5.76 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
5.77 - id2xml i theID ^
5.78 - thm''2xml i thm ^
5.79 - indt i ^ "<PROOF>\n" ^
5.80 - extref2xml (i+i) "Proof of the theorem" (* TODO "Unsorted"vvv: distinguish Isabelle | Isac *)
5.81 - ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
5.82 - nth 2 theID ^ ".html") ^
5.83 - indt i ^ "</PROOF>\n" ^
5.84 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
5.85 - authors2xml i "MATHAUTHORS" mathauthors ^
5.86 - authors2xml i "COURSEDESIGNS" coursedesign ^
5.87 - "</THEOREMDATA>\n"
5.88 - | thydata2xml (theID, Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
5.89 - "<RULESETDATA>\n" ^
5.90 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
5.91 - id2xml i theID ^
5.92 - rls2xml i thy_rls ^
5.93 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
5.94 - authors2xml i "MATHAUTHORS" mathauthors ^
5.95 - authors2xml i "COURSEDESIGNS" coursedesign ^
5.96 - "</RULESETDATA>\n"
5.97 - | thydata2xml (theID, Thy_Write.Hcal {guh, coursedesign, mathauthors, calc}) =
5.98 - "<RULESETDATA>\n" ^
5.99 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
5.100 - id2xml i theID ^
5.101 - calc2xml i (Thy_Write.theID2thyID theID, calc) ^
5.102 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
5.103 - authors2xml i "MATHAUTHORS" mathauthors ^
5.104 - authors2xml i "COURSEDESIGNS" coursedesign ^
5.105 - "</RULESETDATA>\n"
5.106 - | thydata2xml (theID, _) =
5.107 - raise ERROR ("thydata2xml: not implemented for "^ strs2str' theID);
5.108 -
5.109 -(* analoguous to 'fun met2file' *)
5.110 -fun thydata2file (path : Pbl_Met_Hierarchy.filepath) (pos : Pos.pos) (theID : Thy_Write.theID) thydata =
5.111 - (writeln ("### thes2file: id = " ^ strs2str theID);
5.112 - Pbl_Met_Hierarchy.str2file (path ^ Thy_Present.theID2filename theID) (thydata2xml (theID, thydata)));
5.113 -
5.114 -(* analoguous to 'fun node' *)
5.115 -fun thenode (pa : Pbl_Met_Hierarchy.filepath) ids po wfn (Store.Node (id, [n], ns)) =
5.116 - let val po' = Pos.lev_on po
5.117 - in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Pos.lev_dn po') wfn ns end
5.118 -and thenodes _ _ _ _ [] = ()
5.119 - | thenodes pa ids po wfn (n::ns) =
5.120 - (thenode pa ids po wfn n; thenodes pa ids (Pos.lev_on po) wfn ns);
5.121 -
5.122 -(* analoguous to 'fun mets2file' *)
5.123 -fun thes2file (p : Pbl_Met_Hierarchy.filepath) = thenodes p [] [0] thydata2file (get_thes ());
5.124 -
5.125 -
5.126 -(***.store a single theory element in the hierarchy.***)
5.127 -
5.128 -(*.for mathauthors only, other html is added to xml exported from here.*)
5.129 -fun make_isa thy (part, thypart) (mathauthors : Thy_Write.authors) =
5.130 - let
5.131 - val theID = [part, Context.theory_name thy, thypart]
5.132 - val guh = case theID of
5.133 - [part] => Thy_Write.part2guh theID
5.134 - | [part, thyID, thypart] => Thy_Write.thypart2guh theID
5.135 - val theID = Thy_Present.guh2theID guh
5.136 - val the = Thy_Write.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
5.137 - in (the, theID) end
5.138 -
5.139 -fun make_thy thy (mathauthors : Thy_Write.authors) =
5.140 - let
5.141 - val guh = Thy_Write.thy2guh ["IsacKnowledge", Context.theory_name thy]
5.142 - val theID = Thy_Present.guh2theID guh
5.143 - val the = Thy_Write.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
5.144 - in (the, theID) end
5.145 -
5.146 -fun make_thm thy part (thmID : ThmC.id, thm) (mathauthors : Thy_Write.authors) =
5.147 - let
5.148 - val guh = Thy_Write.thm2guh (part, Context.theory_name thy) thmID
5.149 - val theID = Thy_Present.guh2theID guh
5.150 - val the = Thy_Write.Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)],
5.151 - mathauthors = mathauthors, fillpats = [], thm = thm}
5.152 - in (the, theID) end
5.153 -
5.154 -fun make_rls thy rls (mathauthors : Thy_Write.authors) =
5.155 - let
5.156 - val guh = Thy_Write.rls2guh ("IsacKnowledge", Context.theory_name thy) ((#id o Rule_Set.rep) rls)
5.157 - val theID = Thy_Present.guh2theID guh
5.158 - val the = Thy_Write.Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
5.159 - thy_rls = (Context.theory_name thy, rls)}
5.160 - (*needs no (!check_guhs_unique) because guh is generated automatically*)
5.161 - in (the, theID) end
5.162 -
5.163 -fun make_cal thy cal (mathauthors : Thy_Write.authors) =
5.164 - let
5.165 - val guh = Thy_Write.cal2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_cal")
5.166 - val theID = Thy_Present.guh2theID guh
5.167 - val the = Thy_Write.Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}
5.168 - in (the, theID) end
5.169 -
5.170 -fun make_ord thy ord (mathauthors : Thy_Write.authors) =
5.171 - let
5.172 - val guh = Thy_Write.ord2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_ord")
5.173 - val theID = Thy_Present.guh2theID guh
5.174 - val the = Thy_Write.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
5.175 - in (the, theID) end
5.176 -
5.177 (* for dialog-authoring *)
5.178 fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
5.179 let
5.180 @@ -331,4 +190,4 @@
5.181 in (hrls', theID) end
5.182
5.183 (**)end(**)
5.184 -open Thy_Hierarchy
5.185 +(** )open Thy_Hierarchy( **)
6.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-present.sml Thu Apr 22 12:53:26 2021 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-present.sml Thu Apr 22 16:21:23 2021 +0200
6.3 @@ -7,30 +7,10 @@
6.4
6.5 signature THEORY_DATA_PRESENTATION =
6.6 sig
6.7 -
6.8 eqtype filename
6.9
6.10 - datatype contthy
6.11 - = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
6.12 - | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
6.13 - | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id}
6.14 - | ContRlsInst of {applto: term, asms: term list, bdvs: subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}
6.15 - | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
6.16 - lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
6.17 - thm: Check_Unique.id, thyID: ThyC.id}
6.18 - | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
6.19 - bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
6.20 - rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}
6.21 - | EContThy
6.22 val guh2filename : Check_Unique.id -> filename
6.23 val thms_of_rls : Rule_Set.T -> Rule.rule list
6.24 - val theID2filename : Thy_Write.theID -> filename
6.25 - val no_thycontext : Check_Unique.id -> bool
6.26 - val subs_from : Istate.T -> 'a -> Check_Unique.id -> Subst.input
6.27 - val guh2rewtac : Check_Unique.id -> Subst.input -> Tactic.input
6.28 - val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input
6.29 - val context_thy : Calc.T -> Tactic.input -> contthy
6.30 - val guh2theID : Check_Unique.id -> Thy_Write.theID
6.31 end
6.32 (**)
6.33 structure Thy_Present(**): THEORY_DATA_PRESENTATION(**) =
6.34 @@ -39,161 +19,6 @@
6.35
6.36 type filename = string;
6.37
6.38 -(* packing return-values to matchTheory, contextToThy for xml-generation *)
6.39 -datatype contthy = (*also an item from Know_Store on Browser ...........#*)
6.40 - EContThy (* not from Know_Store ..............................*)
6.41 - | ContThm of (* a theorem in contex ===========================*)
6.42 - {thyID : ThyC.id, (* for *2guh in sub-elems here .*)
6.43 - thm : Check_Unique.id, (* theorem in the context .*)
6.44 - applto : term, (* applied to formula ... .*)
6.45 - applat : term, (* ... with lhs inserted .*)
6.46 - reword : Rewrite_Ord.rew_ord', (* order used for rewrite .*)
6.47 - asms : (term (* asumption instantiated .*)
6.48 - * term) list, (* asumption evaluated .*)
6.49 - lhs : term (* lhs of the theorem ... #*)
6.50 - * term, (* ... instantiated .*)
6.51 - rhs : term (* rhs of the theorem ... #*)
6.52 - * term, (* ... instantiated .*)
6.53 - result : term, (* resulting from the rewrite .*)
6.54 - resasms : term list, (* ... with asms stored .*)
6.55 - asmrls : Rule_Set.id (* ruleset for evaluating asms .*)
6.56 - }
6.57 - | ContThmInst of (* a theorem with bdvs in contex ============ *)
6.58 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
6.59 - thm : Check_Unique.id, (*theorem in the context .*)
6.60 - bdvs : subst, (*bound variables to modify... .*)
6.61 - thminst : term, (*... theorem instantiated .*)
6.62 - applto : term, (*applied to formula ... .*)
6.63 - applat : term, (*... with lhs inserted .*)
6.64 - reword : Rewrite_Ord.rew_ord', (*order used for rewrite .*)
6.65 - asms : (term (*asumption instantiated .*)
6.66 - * term) list, (*asumption evaluated .*)
6.67 - lhs : term (*lhs of the theorem ... #*)
6.68 - * term, (*... instantiated .*)
6.69 - rhs : term (*rhs of the theorem ... #*)
6.70 - * term, (*... instantiated .*)
6.71 - result : term, (*resulting from the rewrite .*)
6.72 - resasms : term list, (*... with asms stored .*)
6.73 - asmrls : Rule_Set.id (*ruleset for evaluating asms .*)
6.74 - }
6.75 - | ContRls of (* a rule set in contex ========================= *)
6.76 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
6.77 - rls : Check_Unique.id, (*rule set in the context .*)
6.78 - applto : term, (*rewrite this formula .*)
6.79 - result : term, (*resulting from the rewrite .*)
6.80 - asms : term list (*... with asms stored .*)
6.81 - }
6.82 - | ContRlsInst of (* a rule set with bdvs in contex =========== *)
6.83 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
6.84 - rls : Check_Unique.id, (*rule set in the context .*)
6.85 - bdvs : subst, (*for bound variables in thms .*)
6.86 - applto : term, (*rewrite this formula .*)
6.87 - result : term, (*resulting from the rewrite .*)
6.88 - asms : term list (*... with asms stored .*)
6.89 - }
6.90 - | ContNOrew of (* no rewrite for thm or rls ================== *)
6.91 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
6.92 - thm_rls : Check_Unique.id, (*thm or rls in the context .*)
6.93 - applto : term (*rewrite this formula .*)
6.94 - }
6.95 - | ContNOrewInst of (* no rewrite for some instantiation ====== *)
6.96 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
6.97 - thm_rls : Check_Unique.id, (*thm or rls in the context .*)
6.98 - bdvs : subst, (*for bound variables in thms .*)
6.99 - thminst : term, (*... theorem instantiated .*)
6.100 - applto : term (*rewrite this formula .*)
6.101 - }
6.102 -
6.103 -(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
6.104 - pass other tacs unchanged.*)
6.105 -fun get_tac_checked pt ((p, _) : Pos.pos') = Ctree.get_obj Ctree.g_tac pt p;
6.106 -
6.107 -(* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
6.108 -fun context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite thm'') =
6.109 - let
6.110 - val thm_deriv = ThmC.long_id thm''
6.111 - in
6.112 - (case Step.check tac (pt, pos) of
6.113 - Applicable.Yes (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>
6.114 - ContThm
6.115 - {thyID = thy',
6.116 - thm = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
6.117 - applto = f, applat = TermC.empty, reword = ord',
6.118 - asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
6.119 - result = res, resasms = asm, asmrls = Rule_Set.id erls}
6.120 - | Applicable.No _ =>
6.121 - let
6.122 - val pp = Ctree.par_pblobj pt p
6.123 - val thy' = Ctree.get_obj Ctree.g_domID pt pp
6.124 - val f = case p_ of
6.125 - Pos.Frm => Ctree.get_obj Ctree.g_form pt p
6.126 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
6.127 - | _ => raise ERROR "context_thy: uncovered position"
6.128 - in
6.129 - ContNOrew
6.130 - {thyID = thy',
6.131 - thm_rls =
6.132 - Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
6.133 - applto = f}
6.134 - end
6.135 - | _ => raise ERROR "context_thy..Rewrite: uncovered case 2")
6.136 - end
6.137 - | context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite_Inst (subs, (thmID, _))) =
6.138 - let val thm = Global_Theory.get_thm (ThyC.Isac ()) thmID
6.139 - in
6.140 - (case Step.check tac (pt, pos) of
6.141 - Applicable.Yes (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
6.142 - let
6.143 - val thm_deriv = Thm.get_name_hint thm
6.144 - val thminst = TermC.inst_bdv subst (Eval.norm (Thm.prop_of thm))
6.145 - in
6.146 - ContThmInst
6.147 - {thyID = thy',
6.148 - thm =
6.149 - Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
6.150 - bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
6.151 - asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
6.152 - result = res, resasms = asm, asmrls = Rule_Set.id erls}
6.153 - end
6.154 - | Applicable.No _ =>
6.155 - let
6.156 - val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
6.157 - val thm_deriv = Thm.get_name_hint thm
6.158 - val pp = Ctree.par_pblobj pt p
6.159 - val thy' = Ctree.get_obj Ctree.g_domID pt pp
6.160 - val subst = Subst.T_from_input (ThyC.get_theory thy') subs
6.161 - val thminst = TermC.inst_bdv subst (Eval.norm (Thm.prop_of thm))
6.162 - val f = case p_ of
6.163 - Pos.Frm => Ctree.get_obj Ctree.g_form pt p
6.164 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
6.165 - | _ => raise ERROR "context_thy: uncovered case 3"
6.166 - in
6.167 - ContNOrewInst
6.168 - {thyID = thy',
6.169 - thm_rls = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
6.170 - bdvs = subst, thminst = thminst, applto = f}
6.171 - end
6.172 - | _ => raise ERROR "context_thy..Rewrite_Inst: uncovered case 4")
6.173 - end
6.174 - | context_thy (pt, p) (tac as Tactic.Rewrite_Set rls') =
6.175 - (case Step.check tac (pt, p) of
6.176 - Applicable.Yes (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
6.177 - ContRls
6.178 - {thyID = thy',
6.179 - rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
6.180 - applto = f, result = res, asms = asm}
6.181 - | _ => raise ERROR ("context_thy Rewrite_Set: not for Applicable.No"))
6.182 - | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) =
6.183 - (case Step.check tac (pt, p) of
6.184 - Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
6.185 - ContRlsInst
6.186 - {thyID = thy',
6.187 - rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
6.188 - bdvs = subst, applto = f, result = res, asms = asm}
6.189 - | _ => raise ERROR ("context_thy Rewrite_Set_Inst: not for Applicable.No"))
6.190 - | context_thy (_, p) tac =
6.191 - raise ERROR ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p)
6.192 -
6.193 (* get all theorems in a rule set (recursivley containing rule sets) *)
6.194 fun thm_of_rule Rule.Erule = []
6.195 | thm_of_rule (thm as Rule.Thm _) = [thm]
6.196 @@ -205,118 +30,6 @@
6.197 | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules
6.198 | thms_of_rls (Rule_Set.Rrls _) = []
6.199
6.200 -
6.201 -(* filenames not only for thydata, but also for thy's etc *)
6.202 -fun theID2filename theID = Thy_Write.theID2guh theID ^ ".xml"
6.203 -
6.204 -fun guh2theID guh =
6.205 - let
6.206 - val guh' = Symbol.explode guh
6.207 - val part = implode (take_fromto 1 4 guh')
6.208 - val isa = implode (take_fromto 5 9 guh')
6.209 - in
6.210 - if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
6.211 - then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_")
6.212 - else
6.213 - let
6.214 - val chap = case isa of
6.215 - "isab_" => "Isabelle"
6.216 - | "scri_" => "IsacScripts"
6.217 - | "isac_" => "IsacKnowledge"
6.218 - | _ =>
6.219 - raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9")
6.220 - val rest = takerest (9, guh')
6.221 - val thyID = takewhile [] (not o (curry op= "-")) rest
6.222 - val rest' = dropuntil (curry op = "-") rest
6.223 - in case implode rest' of
6.224 - "-part" => [chap] : Thy_Write.theID
6.225 - | "" => [chap, implode thyID]
6.226 - | "-Theorems" => [chap, implode thyID, "Theorems"]
6.227 - | "-Rulesets" => [chap, implode thyID, "Rulesets"]
6.228 - | "-Operations" => [chap, implode thyID, "Operations"]
6.229 - | "-Orders" => [chap, implode thyID, "Orders"]
6.230 - | _ =>
6.231 - let val sect = implode (take_fromto 1 5 rest')
6.232 - val sect' = case sect of
6.233 - "-thm-" => "Theorems"
6.234 - | "-rls-" => "Rulesets"
6.235 - | "-cal-" => "Operations"
6.236 - | "-ord-" => "Orders"
6.237 - | _ =>
6.238 - raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-")
6.239 - in
6.240 - [chap, implode thyID, sect', implode (takerest (5, rest'))]
6.241 - end
6.242 - end
6.243 - end
6.244 -
6.245 fun guh2filename guh = guh ^ ".xml";
6.246
6.247 -fun guh2rewtac guh [] =
6.248 - let
6.249 - val (_, thy, sect, xstr) = case guh2theID guh of
6.250 - [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
6.251 - | _ => raise ERROR "guh2rewtac: uncovered case"
6.252 - in case sect of
6.253 - "Theorems" => Tactic.Rewrite (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr)
6.254 - | "Rulesets" => Tactic.Rewrite_Set xstr
6.255 - | _ => raise ERROR ("guh2rewtac: not impl. for '"^xstr^"'")
6.256 - end
6.257 - | guh2rewtac guh subs =
6.258 - let
6.259 - val (_, thy, sect, xstr) = case guh2theID guh of
6.260 - [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
6.261 - | _ => raise ERROR "guh2rewtac: uncovered case"
6.262 - in case sect of
6.263 - "Theorems" =>
6.264 - Tactic.Rewrite_Inst (subs, (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr))
6.265 - | "Rulesets" => Tactic.Rewrite_Set_Inst (subs, xstr)
6.266 - | str => raise ERROR ("guh2rewtac: not impl. for '" ^ str ^ "'")
6.267 - end
6.268 -
6.269 -(* the front-end may request a context for any element of the hierarchy *)
6.270 -fun no_thycontext guh = (guh2theID guh; false)
6.271 - handle ERROR _ => true;
6.272 -
6.273 -(* get the substitution of bound variables for matchTheory:
6.274 - # lookup the thm|rls' in the script
6.275 - # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
6.276 - # instantiate this subs with the istates env to [(bdv, x),..]
6.277 - # otherwise []
6.278 - WN060617 hack assuming that all scripts use only one bound variable
6.279 - and use 'v_' as the formal argument for this bound variable*)
6.280 -fun subs_from (Istate.Pstate ({env, ...})) _ guh =
6.281 - let
6.282 - val (_, _, thyID, sect, xstr) = case guh2theID guh of
6.283 - theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
6.284 - | _ => raise ERROR "subs_from: uncovered case"
6.285 - in
6.286 - case sect of
6.287 - "Theorems" =>
6.288 - let val thm = Global_Theory.get_thm (ThyC.get_theory thyID) xstr
6.289 - in
6.290 - if Auto_Prog.contains_bdv thm
6.291 - then
6.292 - let
6.293 - val formal_arg = TermC.str2term "v_"
6.294 - val value = subst_atomic env formal_arg
6.295 - in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end
6.296 - else []
6.297 - end
6.298 - | "Rulesets" =>
6.299 - let
6.300 - val rules = (Rule_Set.get_rules o assoc_rls) xstr
6.301 - in
6.302 - if Auto_Prog.contain_bdv rules
6.303 - then
6.304 - let
6.305 - val formal_arg = TermC.str2term "v_"
6.306 - val value = subst_atomic env formal_arg
6.307 - in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end
6.308 - else []
6.309 - end
6.310 - | str => raise ERROR ("subs_from: uncovered case with " ^ str)
6.311 - end
6.312 - | subs_from _ _ guh = raise ERROR ("subs_from: uncovered case with " ^ guh)
6.313 -
6.314 (**)end(**)
7.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Apr 22 12:53:26 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Thu Apr 22 16:21:23 2021 +0200
7.3 @@ -76,6 +76,7 @@
7.4
7.5 section \<open>Acknowledgements shown in browsers of Isac_Knowledge\<close>
7.6
7.7 +(* there will be other ways in Isabelle/PIDE * )
7.8 setup \<open>
7.9 KEStore_Elems.add_thes
7.10 [Thy_Hierarchy.make_thy @{theory}
7.11 @@ -97,6 +98,7 @@
7.12 Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})
7.13 ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
7.14 \<close>
7.15 +( **)
7.16
7.17 section \<open>Problems\<close>
7.18
8.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 22 12:53:26 2021 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,371 +0,0 @@
8.4 -(* Title: test for sml/xmlsrc/datatypes.sml
8.5 - Authors: Walther Neuper 2003
8.6 - (c) due to copyright terms
8.7 -
8.8 -use"../smltest/xmlsrc/datatypes.sml";
8.9 -use"datatypes.sml";
8.10 -*)
8.11 -
8.12 -"-----------------------------------------------------------------";
8.13 -"table of contents -----------------------------------------------";
8.14 -"-----------------------------------------------------------------";
8.15 -"----------- fun rules2xml ---------------------------------------";
8.16 -"----------- fun thm''2xml ---------------------------------------";
8.17 -"----------- fun xml_of_model ------------------------------------------------------------------";
8.18 -"----------- fun xml_of_tac --------------------------------------------------------------------";
8.19 -"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
8.20 -"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
8.21 -"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
8.22 -"-----------------------------------------------------------------";
8.23 -"-----------------------------------------------------------------";
8.24 -"-----------------------------------------------------------------";
8.25 -
8.26 -
8.27 -
8.28 -"----------- fun rules2xml ---------------------------------------";
8.29 -"----------- fun rules2xml ---------------------------------------";
8.30 -"----------- fun rules2xml ---------------------------------------";
8.31 -
8.32 -show_thes();
8.33 -val thyID = "Test";
8.34 -
8.35 -(*========== inhibit exn AK110725 ================================================
8.36 -val thydata = Thy_Read.from_store ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
8.37 -(*AK110725
8.38 -(*val thydata = Thy_Read.from_store ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
8.39 - (* ERROR: Problem.from_store not found: ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"] *)*)
8.40 -"~~~~~ fun Thy_Read.from_store, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
8.41 -(*get_py (ThyC.get_theory "Pure") theID theID (get_thes ());
8.42 - (* ERROR: Problem.from_store not found: ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"] *)*)
8.43 -(*default_print_depth 3; 999*)
8.44 -(get_thes ());
8.45 -
8.46 -(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));*)
8.47 -"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));
8.48 -error ("Problem.from_store not found: "^(strs2str d));
8.49 -(*AK110725 To be continued...s*)
8.50 -*)
8.51 -
8.52 -val Hrls {thy_rls = (_,Rule_Set.Repeat {rules = rules as rule::_,...}),...} = thydata;
8.53 -
8.54 -(*for rule2xml...*)
8.55 -val (j, thyID, Thm (thmID, thm)) = (2, thyID, rule);
8.56 -val (isa, thyID') = thy_containing_thm thyID thmID;
8.57 -val guh = thm2guh (isa, thyID') thmID;
8.58 -writeln (rules2xml 2 "Test" rules);
8.59 -
8.60 -
8.61 -"----------- fun thm''2xml ---------------------------------------";
8.62 -"----------- fun thm''2xml ---------------------------------------";
8.63 -"----------- fun thm''2xml ---------------------------------------";
8.64 -
8.65 -show_thes();
8.66 -val theID = ["IsacKnowledge", "Diff", "Theorems", "frac_conv"];
8.67 -val thydata = Thy_Read.from_store theID;
8.68 -val Hthm {guh=guh, thm=thm, mathauthors=ma, coursedesign=co} = thydata;
8.69 -writeln(thydata2xml (theID, thydata));
8.70 -"----- check 'manually' ...0 < ?n |] ==> ?a... -----";
8.71 -"---------------------------- \<up> --------- \<up> ------------";
8.72 -
8.73 -
8.74 -
8.75 -(* use"../smltest/xmlsrc/datatypes.sml";
8.76 - *)
8.77 -============ inhibit exn AK110725 ==============================================*)
8.78 -
8.79 -"----------- fun xml_of_model ------------------------------------------------------------------";
8.80 -"----------- fun xml_of_model ------------------------------------------------------------------";
8.81 -"----------- fun xml_of_model ------------------------------------------------------------------";
8.82 -(*create testdata: see --- tryrefine ---
8.83 - xml_of_model used via refineProblem \<longrightarrow> matchpbl2xml \<longrightarrow> model2xml*)
8.84 -reset_states ();
8.85 -CalcTree [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
8.86 - "solveFor x", "solutions L"],
8.87 - ("RatEq",["univariate", "equation"],["no_met"]))];
8.88 -Iterator 1;
8.89 -moveActiveRoot 1; autoCalculate 1 CompleteCalc;
8.90 -refineProblem 1 ([1],Res) "pbl_equ_univ";
8.91 -"~~~~~ fun refineProblem, args:"; val (cI, ((p,p_) : pos'), (guh : Check_Unique.id)) =
8.92 - (1, ([1],Res), "pbl_equ_univ");
8.93 -val pblID = Ptool.guh2kestoreID guh
8.94 - val ((pt,_),_) = get_calc cI
8.95 - val pp = par_pblobj pt p
8.96 - val chd = tryrefine pblID pt (pp, p_);
8.97 -"~~~~~ fun matchpbl2xml, args:"; val ((cI:calcID), (model_ok, pI, hdl, pbl, pre)) = (cI, chd);
8.98 -"~~~~~ fun model2xml, args:"; val (j, (itms:I_Model.T), where_) = (i, pbl, pre);
8.99 -"~~~~~ fun xml_of_model, args:"; val (itms, where_) = (pbl, pre);
8.100 -val xxx = xml_of_model itms where_;
8.101 -(xmlstr 0 xxx);
8.102 -writeln(xmlstr 0 xxx);
8.103 -if xmlstr 0 xxx = "(MODEL)\n. (GIVEN)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . equality (x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) = 1 / x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solveFor x\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/GIVEN)\n. (WHERE)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/WHERE)\n. (FIND)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solutions L\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/FIND)\n. (RELATE)\n. (/RELATE)\n(/MODEL)\n"
8.104 -then () else error ("xml_of_model changed = " ^ xmlstr 0 xxx);
8.105 -
8.106 -"----------- fun xml_of_tac --------------------------------------------------------------------";
8.107 -"----------- fun xml_of_tac --------------------------------------------------------------------";
8.108 -"----------- fun xml_of_tac --------------------------------------------------------------------";
8.109 -(* WN150814 these are the Java objects.
8.110 -import isac.util.tactics.RewriteInst
8.111 -import isac.util.tactics.RewriteSet
8.112 -import isac.util.tactics.RewriteSetInst
8.113 -import isac.util.tactics.SimpleTactic ...not appropriately abstracted
8.114 -import isac.util.tactics.StringListTactic ...not appropriately abstracted
8.115 -import isac.util.tactics.SubProblemTactic
8.116 -import isac.util.tactics.Tactic
8.117 -*)
8.118 -Rewrite: ThmC.T -> Tactic.input;
8.119 -val tac = Rewrite("refl", @{thm refl});
8.120 -if xmlstr 0 (xml_of_tac tac) =
8.121 -(*---xml_of_tac------------------------------------------thm'_to_thm''--------------
8.122 -"(REWRITETACTIC name=Rewrite)\n" ^
8.123 -". (THEOREM)\n" ^
8.124 -". . (ID)\n" ^
8.125 -". . . refl\n" ^
8.126 -". . (/ID)\n" ^
8.127 -". . (FORMULA)\n" ^
8.128 -". . . (ISA)\n" ^
8.129 -". . . . a = a\n" ^
8.130 -". . . (/ISA)\n" ^
8.131 -". . . (TERM)\n" ^
8.132 -". . . . ?t = ?t\n" ^
8.133 -". . . (/TERM)\n" ^
8.134 -". . (/FORMULA)\n" ^
8.135 -". (/THEOREM)\n" ^
8.136 ------xml_of_tac------------------------------------------thm'_to_thm''------------*)
8.137 -"(REWRITETACTIC name=Rewrite)\n" ^
8.138 -". (THEOREM)\n" ^
8.139 -". . (ID)\n" ^
8.140 -". . . refl\n" ^
8.141 -". . (/ID)\n" ^
8.142 -". . (FORMULA)\n" ^
8.143 -". . . ?t = ?t\n" ^
8.144 -". . (/FORMULA)\n" ^
8.145 -". (/THEOREM)\n" ^
8.146 -"(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";
8.147 -
8.148 -Rewrite_Inst: Subst.input * ThmC.T -> Tactic.input;
8.149 -val tac = Rewrite_Inst(["(''bdv'', x)"], ("refl", @{thm refl}));
8.150 -if xmlstr 0 (xml_of_tac tac) =
8.151 -"(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^
8.152 -". (SUBSTITUTION)\n" ^
8.153 -". . (PAIR)\n" ^
8.154 -". . . (VARIABLE)\n" ^
8.155 -". . . . (MATHML)\n" ^ (* TODO *)
8.156 -". . . . . (ISA)\n" ^
8.157 -". . . . . . bdv\n" ^
8.158 -". . . . . (/ISA)\n" ^
8.159 -". . . . (/MATHML)\n" ^
8.160 -". . . (/VARIABLE)\n" ^
8.161 -". . . (VALUE)\n" ^
8.162 -". . . . (MATHML)\n" ^
8.163 -". . . . . (ISA)\n" ^
8.164 -". . . . . . x\n" ^
8.165 -". . . . . (/ISA)\n" ^
8.166 -". . . . (/MATHML)\n" ^
8.167 -". . . (/VALUE)\n" ^
8.168 -". . (/PAIR)\n" ^
8.169 -". (/SUBSTITUTION)\n" ^
8.170 -(*---xml_of_tac------------------------------------------thm'_to_thm''--------------
8.171 -". (THEOREM)\n" ^
8.172 -". . (ID)\n" ^
8.173 -". . . refl\n" ^
8.174 -". . (/ID)\n" ^
8.175 -". . (FORMULA)\n" ^ (* OK *)
8.176 -". . . (ISA)\n" ^
8.177 -". . . . a = a\n" ^
8.178 -". . . (/ISA)\n" ^
8.179 -". . . (TERM)\n" ^
8.180 -". . . ?t = ?t\n" ^
8.181 -". . . (/TERM)\n" ^
8.182 -". . (/FORMULA)\n" ^
8.183 -". (/THEOREM)\n" ^
8.184 ------xml_of_tac------------------------------------------thm'_to_thm''------------*)
8.185 -". (THEOREM)\n" ^
8.186 -". . (ID)\n" ^
8.187 -". . . refl\n" ^
8.188 -". . (/ID)\n" ^
8.189 -". . (FORMULA)\n" ^
8.190 -". . . ?t = ?t\n" ^
8.191 -". . (/FORMULA)\n" ^
8.192 -". (/THEOREM)\n" ^
8.193 -"(/REWRITEINSTTACTIC)\n" then () else error "xml_of_tac Rewrite_Inst CHANGED";
8.194 -
8.195 -Rewrite_Set: Rule_Set.id -> Tactic.input;
8.196 -val tac = Rewrite_Set("simplify");
8.197 -if xmlstr 0 (xml_of_tac tac) = "(REWRITESETTACTIC name=Rewrite_Set)\n" ^
8.198 -". simplify\n" ^
8.199 -"(/REWRITESETTACTIC)\n" then () else error "xml_of_tac Rewrite_Set CHANGED";
8.200 -
8.201 -Rewrite_Set_Inst: Subst.input * Rule_Set.id -> Tactic.input;
8.202 -val tac = Rewrite_Set_Inst(["(''bdv'', x)"], "simplify");
8.203 -if xmlstr 0 (xml_of_tac tac) =
8.204 -"(REWRITESETINSTTACTIC name=Rewrite_Set_Inst)\n" ^
8.205 -". (SUBSTITUTION)\n" ^
8.206 -". . (PAIR)\n" ^
8.207 -". . . (VARIABLE)\n" ^
8.208 -". . . . (MATHML)\n" ^ (* TODO *)
8.209 -". . . . . (ISA)\n" ^
8.210 -". . . . . . bdv\n" ^
8.211 -". . . . . (/ISA)\n" ^
8.212 -". . . . (/MATHML)\n" ^
8.213 -". . . (/VARIABLE)\n" ^
8.214 -". . . (VALUE)\n" ^
8.215 -". . . . (MATHML)\n" ^
8.216 -". . . . . (ISA)\n" ^
8.217 -". . . . . . x\n" ^
8.218 -". . . . . (/ISA)\n" ^
8.219 -". . . . (/MATHML)\n" ^
8.220 -". . . (/VALUE)\n" ^
8.221 -". . (/PAIR)\n" ^
8.222 -". (/SUBSTITUTION)\n" ^
8.223 -". (RULESET)\n" ^
8.224 -". . simplify\n" ^
8.225 -". (/RULESET)\n" ^
8.226 -"(/REWRITESETINSTTACTIC)\n"then () else error "xml_of_tac Rewrite_Set_Inst CHANGED";
8.227 -
8.228 -
8.229 -"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
8.230 -"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
8.231 -"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
8.232 -
8.233 -"----------- these are : TermC.as_string -> tac: WN150814 THESE WELL BECOME TermTactic TERMTACTIC";
8.234 -Add_Given: TermC.as_string -> Tactic.input;
8.235 -Add_Find: TermC.as_string -> Tactic.input;
8.236 -Add_Relation: TermC.as_string -> Tactic.input;
8.237 -Check_elementwise: TermC.as_string -> Tactic.input;
8.238 -Take: TermC.as_string -> Tactic.input;
8.239 -
8.240 -Add_Given: TermC.as_string -> Tactic.input;
8.241 -val tac = Add_Given("equality (x + 1 = 2)");
8.242 -xml_of_tac tac;(*
8.243 -<FORMTACTIC name="Add_Given">
8.244 - <MATHML>
8.245 - <ISA>equality (x + 1 = 2)</ISA>
8.246 - </MATHML>
8.247 -</FORMTACTIC>*)
8.248 -if xmlstr 0 (xml_of_tac tac) = "(FORMTACTIC name=Add_Given)\n. (MATHML)\n. . (ISA)\n. . . equality (x + 1 = 2)\n. . (/ISA)\n. (/MATHML)\n(/FORMTACTIC)\n"
8.249 -then () else error "xml_of_tac Add_Given CHANGED";
8.250 -
8.251 -"----------- these are : string -> tac: ";
8.252 -Calculate: string -> Tactic.input;; (* should be the operator*)
8.253 -Specify_Theory: ThyC.id -> Tactic.input;;
8.254 -val tac = Specify_Theory("Differentiate");
8.255 -xml_of_tac tac;(*
8.256 -<SIMPLETACTIC name="Specify_Theory">
8.257 - <MATHML> NONSENSE
8.258 - <ISA>Differentiate</ISA>
8.259 - </MATHML>
8.260 -</SIMPLETACTIC>*)
8.261 -if xmlstr 0 (xml_of_tac tac) = "(SIMPLETACTIC name=Specify_Theory)\n. Differentiate\n(/SIMPLETACTIC)\n"
8.262 -then () else error "xml_of_tac Specify_Theory CHANGED";
8.263 -
8.264 -"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
8.265 -"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
8.266 -"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
8.267 -Model_Problem: Tactic.input;
8.268 -Or_to_List: Tactic.input;
8.269 -
8.270 -Apply_Method: MethodC.id -> Tactic.input;
8.271 -Refine_Tacitly: Problem.id -> Tactic.input;
8.272 -Specify_Problem: Problem.id -> Tactic.input;
8.273 -Specify_Method: MethodC.id -> Tactic.input;
8.274 -Substitute: Subst.input -> Tactic.input;; (* Substitute: sube -> tac; Subst.string_eqs_empty: TermC.as_string list; UNCLEAR HOW TO INPUT *)
8.275 -Check_Postcond: Problem.id -> Tactic.input;
8.276 -
8.277 -Apply_Method: MethodC.id -> Tactic.input;
8.278 -val tac = Apply_Method(["test", "equation", "simplify"]);
8.279 -xml_of_tac tac;(*
8.280 -<STRINGLISTTACTIC name="Apply_Method">
8.281 - <STRINGLIST>
8.282 - <STRING>test</STRING>
8.283 - <STRING>equation</STRING>
8.284 - <STRING>simplify</STRING>
8.285 - </STRINGLIST>
8.286 -</STRINGLISTTACTIC>*)
8.287 -if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Apply_Method)\n. (STRINGLIST)\n. . (STRING)\n. . . test\n. . (/STRING)\n. . (STRING)\n. . . equation\n. . (/STRING)\n. . (STRING)\n. . . simplify\n. . (/STRING)\n. (/STRINGLIST)\n(/STRINGLISTTACTIC)\n"
8.288 -then () else error "xml_of_tac Apply_Method CHANGED";
8.289 -
8.290 -"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
8.291 -"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
8.292 -"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
8.293 -(* Note: tacs Substitute, Rewrite_Inst* have different substitutions,
8.294 -while input in frontend is not yet clear: *)
8.295 -Rewrite_Inst: Subst.input * ThmC.T -> Tactic.input;
8.296 -Substitute : Subst.input -> Tactic.input;
8.297 -
8.298 -Subst.input_empty: Subst.input;
8.299 -Subst.input_empty: Subst.input;
8.300 -val subs = ["(''bdv_1'', xxx)", "(''bdv_2'', yyy)"]: TermC.as_string list;
8.301 -xml_of_subs subs;(*
8.302 -<SUBSTITUTION>
8.303 - <PAIR>
8.304 - <VARIABLE>
8.305 - <MATHML>
8.306 - <ISA>bdv_1</ISA>
8.307 - </MATHML>
8.308 - </VARIABLE>
8.309 - <VALUE><
8.310 - MATHML>
8.311 - <ISA>xxx</ISA>
8.312 - </MATHML>
8.313 - </VALUE>
8.314 - </PAIR>
8.315 - <PAIR>
8.316 - <VARIABLE>
8.317 - <MATHML>
8.318 - <ISA>bdv_2</ISA>
8.319 - </MATHML>
8.320 - </VARIABLE>
8.321 - <VALUE>
8.322 - <MATHML>
8.323 - <ISA>yyy</ISA>
8.324 - </MATHML>
8.325 - </VALUE>
8.326 - </PAIR>
8.327 -</SUBSTITUTION>:*)
8.328 -val tac = Rewrite_Inst (subs, ("diff_sin_chain", @{thm diff_sin_chain}));
8.329 -val xml = xml_of_tac tac;
8.330 -
8.331 -if xmlstr 0 (xml_of_tac tac) = "(REWRITEINSTTACTIC name=Rewrite_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (THEOREM)\n. . (ID)\n. . . diff_sin_chain\n. . (/ID)\n. . (FORMULA)\n. . . d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITEINSTTACTIC)\n"
8.332 -then () else error "xml_of_tac Rewrite_Inst CHANGED";
8.333 -
8.334 -val Rewrite_Inst (["(''bdv_1'', xxx)", "(''bdv_2'', yyy)"], ("diff_sin_chain", term)) = xml_to_tac xml;
8.335 -if (UnparseC.term o Thm.prop_of) term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"
8.336 -then () else error "xml_to_tac Rewrite_Inst CHANGED";
8.337 -
8.338 -val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: Subst.input;
8.339 -Subst.string_eqs_empty: TermC.as_string list;
8.340 -Subst.string_eqs_empty: Subst.input;
8.341 -xml_of_sube sube;(*
8.342 -<SUBSTITUTION>
8.343 - <PAIR>
8.344 - <VARIABLE>
8.345 - <MATHML>
8.346 - <ISA>bdv_1</ISA>
8.347 - </MATHML>
8.348 - </VARIABLE>
8.349 - <VALUE>
8.350 - <MATHML>
8.351 - <ISA>xxx</ISA>
8.352 - </MATHML>
8.353 - </VALUE>
8.354 - </PAIR>
8.355 - <PAIR>
8.356 - <VARIABLE>
8.357 - <MATHML>
8.358 - <ISA>bdv_2</ISA>
8.359 - </MATHML>
8.360 - </VARIABLE>
8.361 - <VALUE>
8.362 - <MATHML>
8.363 - <ISA>yyy</ISA>
8.364 - </MATHML>
8.365 - </VALUE>
8.366 - </PAIR>
8.367 -</SUBSTITUTION>:*)
8.368 -val tac = Substitute sube;
8.369 -val xml = xml_of_tac tac;
8.370 -
8.371 -if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Substitute)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n(/STRINGLISTTACTIC)\n"
8.372 -then () else error "xml_of_tac Substitute CHANGED";
8.373 -case xml_to_tac xml of Substitute ["bdv_1 = xxx", "bdv_2 = yyy"] => ()
8.374 -| _ => error "xml_to_tac Substitute CHANGED";
8.375 \ No newline at end of file
9.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 22 12:53:26 2021 +0200
9.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 22 16:21:23 2021 +0200
9.3 @@ -14,160 +14,15 @@
9.4 "-----------------------------------------------------------------------------------------------";
9.5 "table of contents -----------------------------------------------";
9.6 "-----------------------------------------------------------------";
9.7 -"----------- fun thms_of -----------------------------------------";
9.8 -"----------- ### thes2file ... Exception- Match raised -----------";
9.9 -"----------- search for data error in thes2file ------------------";
9.10 -"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
9.11 -"----------- fun Thm.make_thm ------------------------------------";
9.12 -"----------- correct theIDs for Rule_Set.empty -------------------";
9.13 "----------- fun thms_of_rlss ------------------------------------";
9.14 -"----------- repair thydata2xml for rls --------------------------";
9.15 "----------- fun get_fun_ids -------------------------------------------------------------------";
9.16 "-----------------------------------------------------------------";
9.17 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
9.18 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
9.19 -"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
9.20 -"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
9.21 "-----------------------------------------------------------------";
9.22 "-----------------------------------------------------------------";
9.23 "-----------------------------------------------------------------";
9.24
9.25 -
9.26 -"----------- fun thms_of -----------------------------------------";
9.27 -"----------- fun thms_of -----------------------------------------";
9.28 -"----------- fun thms_of -----------------------------------------";
9.29 -(*WN160112 WE REPLACED vvv BY "fun thms_of" in src/../thy-hierarchy.sml
9.30 -val ths = MutabelleExtra.thms_of false @{theory Biegelinie};
9.31 -(*val it =
9.32 - ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",
9.33 - "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)
9.34 -map ThmC.id_of_thm (thms_of thy) =
9.35 - ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit",
9.36 - "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]
9.37 -*)
9.38 -val thy = @{theory Biegelinie};
9.39 -val thms = thms_of thy;
9.40 -if map ThmC.id_of_thm thms =
9.41 - ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment",
9.42 - "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
9.43 -else error "fun thms_of ...changed";
9.44 -
9.45 -val without_partial_functions = thms_of @{theory Biegelinie};
9.46 -if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";
9.47 -
9.48 -"----------- ### thes2file ... Exception- Match raised -----------";
9.49 -"----------- ### thes2file ... Exception- Match raised -----------";
9.50 -"----------- ### thes2file ... Exception- Match raised -----------";
9.51 -writeln "what to do when you get, e.g. \n\
9.52 -\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\
9.53 -\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\
9.54 -\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\
9.55 -\Exception- Match raised\n";
9.56 -;
9.57 -val theID = ["IsacKnowledge", "Integrate", "Rulesets", "add_new_c"];
9.58 -val thydata = Thy_Read.from_store theID;
9.59 -;
9.60 -(* HERE WE DO NOT create a file ...
9.61 -thydata2file "/tmp/" [] theID thydata (*reports Exception- Match in question*);
9.62 -*)
9.63 -;
9.64 -thydata2xml (theID, thydata) (*reported Exception- Match in question*);
9.65 -val i = 2;
9.66 -;
9.67 -val (theID: Thy_Write.theID, Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);
9.68 -rls2xml i thy_rls (*reported Exception- Match in question*);
9.69 -;
9.70 -val (j, (thyID, Rule_Set.Sequence data)) = (i, thy_rls);
9.71 -rls2xml j (thyID, Rule_Set.Sequence data) (*reported Exception- Match in question*);
9.72 -;
9.73 -val (j, (thyID, Rule_Set.Sequence {id, preconds, rew_ord=(ord,_), erls, errpatts, srls, calc, rules, scr})) =
9.74 - (j, (thyID, Rule_Set.Sequence data));
9.75 -;
9.76 -rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);
9.77 -(*TODO: Eval + Cal1 in datatypes.sml *)
9.78 -
9.79 -"----------- search for data error in thes2file ------------------";
9.80 -"----------- search for data error in thes2file ------------------";
9.81 -"----------- search for data error in thes2file ------------------";
9.82 -val TESTdump = Unsynchronized.ref
9.83 - ("path": Pbl_Met_Hierarchy.filepath, ["ids"]: Thy_Write.theID, []: pos, thydata2file, Store.Node ("xxx", [], []): Thy_Write.thydata Store.node);
9.84 -
9.85 -fun TESTthenode (pa:Pbl_Met_Hierarchy.filepath) ids po wfn (Store.Node (id, [n], ns)) TESTids =
9.86 - let val po' = lev_on po
9.87 - in
9.88 - if (ids@[id]) = TESTids
9.89 - then
9.90 - (TESTdump := (pa, ids, po', wfn, (Store.Node (id, [n], ns)));
9.91 - error "stopped before error, created TESTdump") (* this exn creates right signature*)
9.92 - else
9.93 - wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
9.94 - end
9.95 -and TESTthenodes _ _ _ _ [] _ = ()
9.96 - | TESTthenodes pa ids po wfn (n::ns) TESTids =
9.97 - (TESTthenode pa ids po wfn n TESTids; TESTthenodes pa ids (lev_on po) wfn ns TESTids);
9.98 -
9.99 -(* /--- side effects from previous test files ---\*)
9.100 - val i = indentation;
9.101 - val j = indentation;
9.102 -(* \--- side effects from previous test files ---/*)
9.103 -
9.104 -"~~~~~ fun thes2file, args:"; val (p : Pbl_Met_Hierarchy.filepath) = ("/tmp/");
9.105 -(* recursively descend into thehier just before the error
9.106 - by setting TESTids according to the last line in ouput
9.107 - ### thes2file: id = : *)
9.108 -(TESTthenodes p [] [0] thydata2file (get_thes ())
9.109 - ["IsacKnowledge", "Rational", "Rulesets", "norm_Rational_parenthesized"]
9.110 -handle _(* "stopped before error, created TESTdump" *) => ());
9.111 -;
9.112 -(* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
9.113 -val (pa, ids, po', wfn, (Store.Node (id, [n], ns))) = ! TESTdump;
9.114 -;
9.115 -"~~~~~ fun thydata2file, args:"; val ((xmldata:Pbl_Met_Hierarchy.filepath), (pos:pos), (theID:Thy_Write.theID), thydata) =
9.116 - (pa, po', (ids@[id]), n);
9.117 -"~~~~~ fun thydata2xml, args:"; val (theID, Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
9.118 - (theID:Thy_Write.theID, thydata);
9.119 -"~~~~~ fun rls2xml, args:"; val (j, (thyID, Rule_Set.Sequence data)) = (i, thy_rls);
9.120 -"~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
9.121 - srls, calc, errpatts, rules, scr})) = (j, (thyID, "Rule_Set.Sequence", data));
9.122 -"~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);
9.123 -"~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);
9.124 -val rls' = (#id o Rule_Set.rep) rls;
9.125 -(* \----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----/
9.126 - another way to tackle this kind of error is shown in
9.127 -"----------- thes2file: thy_containing_rls : rls '...' not in ! --"; ------------------------*)
9.128 -
9.129 -"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
9.130 -"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
9.131 -"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
9.132 -val theID = ["IsacKnowledge", "Rational", "Rulesets", "norm_Rational_parenthesized"]
9.133 -val thydata = Thy_Read.from_store theID
9.134 -;
9.135 -thydata2xml (theID, thydata);
9.136 -
9.137 -"----------- fun ThmC_Def.make_thm ------------------------------------";
9.138 -"----------- fun ThmC_Def.make_thm ------------------------------------";
9.139 -"----------- fun ThmC_Def.make_thm ------------------------------------";
9.140 -"~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : Thy_Write.authors)) =
9.141 - (@{theory "Biegelinie"}, "IsacKnowledge",
9.142 - ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
9.143 - ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
9.144 - val guh = Thy_Write.thm2guh (part, Context.theory_name thy) thmID
9.145 - val theID = Thy_Present.guh2theID guh;
9.146 -if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso
9.147 - theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]
9.148 -then () else error "store_thm: guh | theID changed";
9.149 -
9.150 -"----------- correct theIDs for Rule_Set.empty ----------------------------";
9.151 -"----------- correct theIDs for Rule_Set.empty ----------------------------";
9.152 -"----------- correct theIDs for Rule_Set.empty ----------------------------";
9.153 -if Thy_Read.thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "Know_Store") then ()
9.154 -else error "Thy_Read.thy_containing_rls Rule_Set.empty changed";
9.155 -show_thes ();
9.156 -(*shows different assignment for "empty"...
9.157 - :
9.158 - ["IsacScripts", "Know_Store", "Rulesets", "empty"],
9.159 - :*)
9.160 -
9.161 "----------- fun thms_of_rlss ------------------------------------";
9.162 "----------- fun thms_of_rlss ------------------------------------";
9.163 "----------- fun thms_of_rlss ------------------------------------";
9.164 @@ -176,7 +31,7 @@
9.165 [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),
9.166 ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))];
9.167
9.168 -val [_, (thmID, term)] = thms_of_rlss thy rlss;
9.169 +val [_, (thmID, term)] = Thy_Hierarchy.thms_of_rlss thy rlss;
9.170
9.171 if thmID = "Poly.real_mult_minus1" (* WAS "??.unknown" from Pure/more_thm.ML *)
9.172 then () else error "thms_of_rlss changed";
9.173 @@ -198,74 +53,11 @@
9.174 |> distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
9.175
9.176
9.177 -"----------- repair thydata2xml for rls --------------------------";
9.178 -"----------- repair thydata2xml for rls --------------------------";
9.179 -"----------- repair thydata2xml for rls --------------------------";
9.180 -val theID = ["IsacKnowledge", "Poly", "Rulesets", "expand"]
9.181 -val hrls = Thy_Read.from_store theID
9.182 -;
9.183 -if thydata2xml (theID, hrls) = (
9.184 -"<RULESETDATA>\n" ^
9.185 -" <GUH> thy_isac_Poly-rls-expand </GUH>\n" ^
9.186 -" <STRINGLIST>\n" ^
9.187 -" <STRING> IsacKnowledge </STRING>\n" ^
9.188 -" <STRING> Poly </STRING>\n" ^
9.189 -" <STRING> Rulesets </STRING>\n" ^
9.190 -" <STRING> expand </STRING>\n" ^
9.191 -" </STRINGLIST>\n <RULESET>\n" ^
9.192 -" <ID> expand </ID>\n" ^
9.193 -" <TYPE> Rls </TYPE>\n" ^
9.194 -" <RULES>\n" ^
9.195 -" <RULE>\n" ^
9.196 -" <TAG> Theorem </TAG>\n" ^
9.197 -" <STRING> distrib_right </STRING>\n" ^
9.198 -" <GUH> thy_isac_distrib_right-thm-distrib_right </GUH>\n" ^
9.199 -" </RULE>\n" ^
9.200 -" <RULE>\n" ^
9.201 -" <TAG> Theorem </TAG>\n" ^
9.202 -" <STRING> distrib_left </STRING>\n" ^
9.203 -" <GUH> thy_isac_distrib_left-thm-distrib_left </GUH>\n" ^
9.204 -" </RULE>\n" ^
9.205 -" </RULES>\n" ^
9.206 -" <PRECONDS>" ^
9.207 -" </PRECONDS>\n" ^
9.208 -" <ORDER>\n" ^
9.209 -" <STRING> dummy_ord </STRING>\n" ^
9.210 -" </ORDER>\n" ^
9.211 -" <ERLS>\n" ^
9.212 -" <TAG> Ruleset </TAG>\n" ^
9.213 -" <STRING> empty </STRING>\n" ^
9.214 -" <GUH> thy_isac_Poly-rls-empty </GUH>\n" ^
9.215 -" </ERLS>\n" ^
9.216 -" <SRLS>\n" ^
9.217 -" <TAG> Ruleset </TAG>\n" ^
9.218 -" <STRING> empty </STRING>\n" ^
9.219 -" <GUH> thy_isac_Poly-rls-empty </GUH>\n" ^
9.220 -" </SRLS>\n" ^
9.221 -" <SCRIPT> </SCRIPT>\n" ^
9.222 -(*
9.223 -" <SCRIPT>\n" ^
9.224 -" <MATHML>\n" ^
9.225 -" <ISA> auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''distrib_right'')) #>\n Try (Repeat (Rewrite ''distrib_left'')))\n ??.empty) </ISA>\n" ^
9.226 -" </MATHML>\n" ^
9.227 -" </SCRIPT>\n" ^
9.228 -*)
9.229 -" </RULESET>\n" ^
9.230 -" <EXPLANATIONS> </EXPLANATIONS>\n" ^
9.231 -" <MATHAUTHORS>\n" ^
9.232 -" <STRING> isac-team </STRING>\n" ^
9.233 -" </MATHAUTHORS>\n" ^
9.234 -" <COURSEDESIGNS>\n" ^
9.235 -" </COURSEDESIGNS>\n" ^
9.236 -"</RULESETDATA>\n") then ()
9.237 -else error "thydata2xml for rls changed";
9.238 -
9.239 -
9.240 "----------- fun get_fun_ids -------------------------------------------------------------------";
9.241 "----------- fun get_fun_ids -------------------------------------------------------------------";
9.242 "----------- fun get_fun_ids -------------------------------------------------------------------";
9.243 -val met_fun_ids = get_fun_ids @{theory Biegelinie};
9.244 -if map fst (get_fun_ids @{theory Biegelinie}) =
9.245 +val met_fun_ids = Thy_Hierarchy.get_fun_ids @{theory Biegelinie};
9.246 +if map fst (Thy_Hierarchy.get_fun_ids @{theory Biegelinie}) =
9.247 ["Biegelinie.function_to_equality", "Biegelinie.biegelinie", "Biegelinie.belastung_zu_biegelinie",
9.248 "Biegelinie.setzte_randbedingungen"] then () else error "get_fun_ids changed"
9.249
9.250 @@ -278,7 +70,7 @@
9.251 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "prog_expr" (*unpleasant in test*)
9.252 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rrls" (*unpleasant in test*)
9.253 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "empty" (*unpleasant in test*)
9.254 - |> thms_of_rlss @{theory} (*length = 4*)
9.255 + |> Thy_Hierarchy.thms_of_rlss @{theory} (*length = 4*)
9.256
9.257 val rlsthmsNOTisac = isacrlsthms (*length = 2*)
9.258 |> filter (fn (deriv, _) =>
9.259 @@ -287,9 +79,9 @@
9.260 val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
9.261 ;
9.262 val thydata_list =
9.263 - collect_part "IsacKnowledge" knowledge_parent knowthys' @
9.264 - (map (collect_isab "Isabelle") rlsthmsNOTisac) @
9.265 - collect_part "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)
9.266 + Thy_Hierarchy.collect_part "IsacKnowledge" knowledge_parent knowthys' @
9.267 + (map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac) @
9.268 + Thy_Hierarchy.collect_part "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)
9.269 ;
9.270 case thydata_list of (*length = 8*)
9.271 [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
9.272 @@ -332,85 +124,6 @@
9.273 " <ID> theory hierarchy </ID>\n" ^
9.274 " <NO> 1 </NO>\n" ^
9.275 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
9.276 - (hierarchy_guh MINIthehier) ^
9.277 + (Thy_Hierarchy.hierarchy_guh MINIthehier) ^
9.278 "</NODE>");
9.279 -fun MINIthes2file (p : Pbl_Met_Hierarchy.filepath) = thenodes p [] [0] thydata2file MINIthehier;
9.280
9.281 -"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
9.282 -"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
9.283 -"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
9.284 -case MINIget_the ["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"] of
9.285 - Thy_Write.Hthm {guh = "thy_scri_Test_Build_Thydata-thm-thm111", ...} => ()
9.286 -| _ => error "MINIget_the thm111 changed"
9.287 -;
9.288 -val path = "/tmp/"
9.289 -;
9.290 -MINIthy_hierarchy2file path (* ---> /tmp/thy_hierarchy.xml *);
9.291 -writeln (Pbl_Met_Hierarchy.file2str path "thy_hierarchy.xml") (* better check in editor *)
9.292 -;
9.293 -MINIthes2file path (* ---> /tmp/thy_... *);
9.294 -
9.295 -"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
9.296 -"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
9.297 -"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
9.298 -"~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
9.299 -"~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
9.300 - (path, [], [0], thydata2file, MINIthehier);
9.301 -"~~~~~ fun thenode, args:"; val ((pa : Pbl_Met_Hierarchy.filepath), ids, po, wfn, (Store.Node (id, [n], ns))) =
9.302 - (pa, ids, po, wfn, n);
9.303 -val po' = lev_on po;
9.304 -(*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *)
9.305 -
9.306 -(* we take (theID, thydata) from thydata_list ABOVE: *)
9.307 -case hd thydata_list of
9.308 - (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
9.309 - Thy_Write.Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()
9.310 -| _ => error "a change inhibits successful continuation of this test";
9.311 -val (theID, thydata) = hd thydata_list;
9.312 -"~~~~~ fun thydata2file, args:"; val ((path : Pbl_Met_Hierarchy.filepath), (pos : pos), (theID : Thy_Write.theID), thydata) =
9.313 - (pa, po', (*ids @ [id]*)theID, (*n*)thydata);
9.314 -"~~~~~ fun thydata2xml, args:"; val ((theID, Thy_Write.Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=
9.315 - ((theID, thydata));
9.316 -"~~~~~ to str2file return val:"; val (xml) =
9.317 - "<THEOREMDATA>\n" ^
9.318 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
9.319 - id2xml i theID ^
9.320 - thm''2xml i thm ^
9.321 - indt i ^ "<PROOF>\n" ^
9.322 - extref2xml (i+i) "Proof of the theorem"
9.323 - ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
9.324 - nth 2 theID ^ ".html") ^
9.325 - indt i ^ "</PROOF>\n" ^
9.326 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
9.327 - authors2xml i "MATHAUTHORS" mathauthors ^
9.328 - authors2xml i "COURSEDESIGNS" coursedesign ^
9.329 - "</THEOREMDATA>\n"
9.330 -;
9.331 -if xml = ("<THEOREMDATA>\n" ^
9.332 -" <GUH> thy_isac_Test_Build_Thydata-thm-thm111 </GUH>\n" ^
9.333 -" <STRINGLIST>\n" ^
9.334 -" <STRING> IsacKnowledge </STRING>\n" ^
9.335 -" <STRING> Test_Build_Thydata </STRING>\n" ^
9.336 -" <STRING> Theorems </STRING>\n" ^
9.337 -" <STRING> thm111 </STRING>\n" ^
9.338 -" </STRINGLIST>\n" ^
9.339 -" <THEOREM>\n" ^
9.340 -" <ID> thm111 </ID>\n" ^
9.341 -" <MATHML>\n" ^
9.342 -" <ISA> ?thm111.0 = ?thm111.0 + 111 </ISA>\n" ^
9.343 -" </MATHML>\n" ^
9.344 -" </THEOREM>\n" ^
9.345 -" <PROOF>\n" ^
9.346 -" <EXTREF>\n" ^
9.347 -" <TEXT> Proof of the theorem </TEXT>\n" ^
9.348 -" <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Test_Build_Thydata.html </URL>\n" ^
9.349 -" </EXTREF>\n" ^
9.350 -" </PROOF>\n" ^
9.351 -" <EXPLANATIONS> </EXPLANATIONS>\n" ^
9.352 -" <MATHAUTHORS>\n" ^
9.353 -" <STRING> isac-team </STRING>\n" ^
9.354 -" </MATHAUTHORS>\n" ^
9.355 -" <COURSEDESIGNS>\n" ^
9.356 -" </COURSEDESIGNS>\n" ^
9.357 -"</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed"
9.358 -
10.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-present.sml Thu Apr 22 12:53:26 2021 +0200
10.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-present.sml Thu Apr 22 16:21:23 2021 +0200
10.3 @@ -10,13 +10,6 @@
10.4 "----------- fun thy_containing_rls ---------------------";
10.5 "----------- apply thy_containing_rls -------------------";
10.6 "----------- fun thy_containing_cal ---------------------";
10.7 -"----------- initContext Ptool.Thy_ Integration-demo ----------";
10.8 -"----------- initContext..Ptool.Thy_, fun context_thm ---------";
10.9 -"----------- initContext..Ptool.Thy_, fun context_rls ---------";
10.10 -"----------- checkContext..Ptool.Thy_, fun context_thy --------";
10.11 -"----------- checkContext..Ptool.Thy_, fun context_rls --------";
10.12 -"----------- checkContext..Ptool.Thy_ on last formula ---------";
10.13 -"----------- fun guh2theID ------------------------------";
10.14 "----------- debugging on Tests/solve_linear_as_rootpbl -";
10.15 "--------------------------------------------------------";
10.16 (*============ inhibit exn WN120321 ==============================================
10.17 @@ -81,219 +74,6 @@
10.18 if Thy_Read.thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Base_Tools")
10.19 then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"
10.20
10.21 -"----------- initContext Ptool.Thy_ Integration-demo ----------";
10.22 -"----------- initContext Ptool.Thy_ Integration-demo ----------";
10.23 -"----------- initContext Ptool.Thy_ Integration-demo ----------";
10.24 -reset_states ();
10.25 -CalcTree
10.26 -[(["functionTerm (2 * x)", "integrateBy x", "antiDerivative FF"],
10.27 - ("Integrate",["integrate", "function"],
10.28 - ["diff", "integration"]))];
10.29 -Iterator 1;
10.30 -moveActiveRoot 1;
10.31 -autoCalculate 1 CompleteCalc;
10.32 -interSteps 1 ([1],Res);
10.33 -interSteps 1 ([1,1],Res);
10.34 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
10.35 -if existpt' ([1,1,1], Frm) pt then ()
10.36 -else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
10.37 -Kernel.initContext 1 Ptool.Thy_ ([1,1,1], Frm);
10.38 -
10.39 -"----------- initContext..Ptool.Thy_, fun context_thm ---------";
10.40 -"----------- initContext..Ptool.Thy_, fun context_thm ---------";
10.41 -"----------- initContext..Ptool.Thy_, fun context_thm ---------";
10.42 -reset_states (); (*start of calculation, return No.1*)
10.43 -CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
10.44 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
10.45 - ["Test", "squ-equ-test-subpbl1"]))];
10.46 -Iterator 1; moveActiveRoot 1;
10.47 -autoCalculate 1 CompleteCalc;
10.48 -
10.49 -"----- no thy-context at result -----";
10.50 -val p = ([], Res);
10.51 -initContext 1 Ptool.Thy_ p;
10.52 -val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt; (* 11 lines with subpbl *)
10.53 -
10.54 -interSteps 1 ([2], Res);
10.55 -val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt; (* added [2,1]..[2,6] *)
10.56 -interSteps 1 ([3,1], Res);
10.57 -val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt; (* added [3,1,1] Frm + Res *)
10.58 -
10.59 -val p = ([2,4], Res);
10.60 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Ptool.Thy_, (pos as (p,p_):pos')) = (1, Ptool.Thy_, p);
10.61 - member op = [Pbl,Met] p_ = false;
10.62 - pos = ([],Res) = false;
10.63 - val cs as (ptp as (pt,_),_) = get_calc cI;
10.64 - exist_lev_on' pt pos = true;
10.65 - val pos' = lev_on' pt pos
10.66 - val tac = Thy_Present.get_tac_checked pt pos';
10.67 - is_rewtac tac = true;
10.68 -"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite (thmID,_))) =
10.69 - ((pt, pos), tac);
10.70 - val Applicable.Yes (Rewrite' (thy', ord', erls, _, (thmID, thm), f, (res,asm))) = Step.check tac (pt, pos)
10.71 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
10.72 - val thm_deriv = Thm.get_name_hint thm;
10.73 -
10.74 -if Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
10.75 - = "thy_isac_Test-thm-radd_left_commute" then ()
10.76 -else error "context_thy mini-subpbl ([2,4], Res) changed";
10.77 -(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
10.78 --rw-rw-r-- 1 wneuper wneuper 638 Aug 8 16:04 thy_isac_Test-thm-radd_left_commute.html*)
10.79 -
10.80 -
10.81 -val p = ([3,1,1], Frm);
10.82 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Ptool.Thy_, (pos as (p,p_):pos')) = (1, Ptool.Thy_, p);
10.83 - member op = [Pbl,Met] p_ = false;
10.84 - pos = ([],Res) = false;
10.85 - val cs as (ptp as (pt,_),_) = get_calc cI;
10.86 - exist_lev_on' pt pos = true;
10.87 - val pos' = lev_on' pt pos
10.88 - val tac = Thy_Present.get_tac_checked pt pos';
10.89 - is_rewtac tac = true;
10.90 -"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite_Inst (subs, (thmID,_))))=
10.91 - ((pt, pos), tac);
10.92 -val Applicable.Yes (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =
10.93 - Step.check tac (pt, pos)
10.94 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
10.95 - val thm_deriv = Thm.get_name_hint thm;
10.96 -if Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv) =
10.97 - "thy_isac_Test-thm-risolate_bdv_add" then ()
10.98 -else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
10.99 -(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*
10.100 --rw-rw-r-- 1 wneuper wneuper 646 Aug 8 16:04 thy_isac_Test-thm-risolate_bdv_add.html*)
10.101 -
10.102 -
10.103 -val p = ([2,5], Res);
10.104 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Ptool.Thy_, (pos as (p,p_):pos')) = (1, Ptool.Thy_, p);
10.105 - member op = [Pbl,Met] p_ = false;
10.106 - pos = ([],Res) = false;
10.107 - val cs as (ptp as (pt,_),_) = get_calc cI;
10.108 - exist_lev_on' pt pos = true;
10.109 - val pos' = lev_on' pt pos
10.110 - val tac = Thy_Present.get_tac_checked pt pos';
10.111 -if is_rewtac tac = false then ()
10.112 -else error "initContext: context_thy .. Calculate PLUS .. TO BE IMPLEMENTED"
10.113 -
10.114 -"----------- initContext..Ptool.Thy_, fun context_rls ---------";
10.115 -"----------- initContext..Ptool.Thy_, fun context_rls ---------";
10.116 -"----------- initContext..Ptool.Thy_, fun context_rls ---------";
10.117 -(*using pt from above*)
10.118 -val p = ([1], Res);
10.119 -val tac = Rewrite_Set "Test_simplify";
10.120 -initContext 1 Ptool.Thy_ p;
10.121 -(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
10.122 - --- in initContext..Ptool.Thy_ ---*)
10.123 -val Thy_Present.ContRls {rls,result,...} = Thy_Present.context_thy (pt,p) tac;
10.124 -if rls = "thy_isac_Test-rls-Test_simplify"
10.125 - andalso UnparseC.term result = "-1 + x = 0" then ()
10.126 -else error "rewtools.sml initContext..Th_ thy_isac_Test-rls-Test_simplify";
10.127 -
10.128 -val p = ([3,1], Frm);
10.129 -val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
10.130 -initContext 1 Ptool.Thy_ p;
10.131 -(*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
10.132 - --- in initContext..Ptool.Thy_ ---*)
10.133 -val Thy_Present.ContRlsInst {rls,result,...} = Thy_Present.context_thy (pt,p) tac;
10.134 -if rls = "thy_isac_Test-rls-isolate_bdv"
10.135 - andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
10.136 -else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
10.137 -
10.138 -"----------- checkContext..Ptool.Thy_, fun context_thy --------";
10.139 -"----------- checkContext..Ptool.Thy_, fun context_thy --------";
10.140 -"----------- checkContext..Ptool.Thy_, fun context_thy --------";
10.141 -(*using pt from above*)
10.142 -val p = ([2,4], Res);
10.143 -val tac = Rewrite ("radd_left_commute", @{thm radd_left_commute});
10.144 -checkContext 1 p "thy_Test-thm-radd_left_commute";
10.145 -(* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
10.146 - --- in checkContext..Ptool.Thy_ ---*)
10.147 -val Thy_Present.ContThm {thm,result,...} = Thy_Present.context_thy (pt,p) tac;
10.148 -if thm = "thy_isac_Test-thm-radd_left_commute"
10.149 - andalso UnparseC.term result = "-2 + (1 + x) = 0" then ()
10.150 -else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
10.151 -
10.152 -val p = ([3,1,1], Frm);
10.153 -val tac = Rewrite_Inst (["(''bdv'',x)"],("risolate_bdv_add", @{thm "risolate_bdv_add"}));
10.154 -checkContext 1 p "thy_Test-thm-risolate_bdv_add";
10.155 -(* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
10.156 - --- in checkContext..Ptool.Thy_ ---*)
10.157 -val Thy_Present.ContThmInst {thm,result,...} = Thy_Present.context_thy (pt,p) tac;
10.158 -if thm = "thy_isac_Test-thm-risolate_bdv_add"
10.159 - andalso UnparseC.term result = "x = 0 + - 1 * -1" then ()
10.160 -else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
10.161 -
10.162 -val p = ([2,5], Res);
10.163 -val tac = Calculate "plus";
10.164 -(*checkContext..Ptool.Thy_ 1 ([2,5], Res);*)
10.165 -(*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
10.166 -checkContext 1 p ;
10.167 -(* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
10.168 - --- in checkContext..Ptool.Thy_ ---*)
10.169 -
10.170 -"----------- checkContext..Ptool.Thy_, fun context_rls --------";
10.171 -"----------- checkContext..Ptool.Thy_, fun context_rls --------";
10.172 -"----------- checkContext..Ptool.Thy_, fun context_rls --------";
10.173 -(*using pt from above*)
10.174 -val p = ([1], Res);
10.175 -val tac = Rewrite_Set "Test_simplify";
10.176 -checkContext 1 p "thy_isac_Test-rls-Test_simplify";
10.177 -(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
10.178 - --- in checkContext..Ptool.Thy_ ---*)
10.179 -val Thy_Present.ContRls {rls,result,...} = Thy_Present.context_thy (pt,p) tac;
10.180 -if rls = "thy_isac_Test-rls-Test_simplify"
10.181 - andalso UnparseC.term result = "-1 + x = 0" then ()
10.182 -else error "rewtools.sml checkContext..Ptool.Thy_ thy_Test-rls-Test_simplify";
10.183 -
10.184 -val p = ([3,1], Frm);
10.185 -val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
10.186 -checkContext 1 p "thy_Test-rls-isolate_bdv";
10.187 -val Thy_Present.ContRlsInst {rls,result,...} = Thy_Present.context_thy (pt,p) tac;
10.188 -if rls = "thy_isac_Test-rls-isolate_bdv"
10.189 - andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
10.190 -else error "rewtools.sml checkContext..Ptool.Thy_ thy_Test-thm-isolate_bdv";
10.191 -
10.192 -"----------- checkContext..Ptool.Thy_ on last formula ---------";
10.193 -"----------- checkContext..Ptool.Thy_ on last formula ---------";
10.194 -"----------- checkContext..Ptool.Thy_ on last formula ---------";
10.195 -reset_states (); (*start of calculation, return No.1*)
10.196 -CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
10.197 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
10.198 - ["Test", "squ-equ-test-subpbl1"]))];
10.199 -Iterator 1; moveActiveRoot 1;
10.200 -
10.201 -autoCalculate 1 CompleteCalcHead;
10.202 -autoCalculate 1 (Steps 1);
10.203 -val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;
10.204 -initContext 1 Ptool.Thy_ ([1], Frm);
10.205 -checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
10.206 -
10.207 -autoCalculate 1 (Steps 1);
10.208 -val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;
10.209 -initContext 1 Ptool.Thy_ ([1], Res);
10.210 -checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
10.211 -
10.212 -"----------- fun guh2theID ------------------------------";
10.213 -"----------- fun guh2theID ------------------------------";
10.214 -"----------- fun guh2theID ------------------------------";
10.215 -val guh = "thy_scri_ListG-thm-zip_Nil";
10.216 -(*default_print_depth 3; 999*)
10.217 -take_fromto 1 4 (Symbol.explode guh);
10.218 -take_fromto 5 9 (Symbol.explode guh);
10.219 -val rest = takerest (9,(Symbol.explode guh));
10.220 -
10.221 -separate "-" rest;
10.222 -space_implode "-" rest;
10.223 -commas rest;
10.224 -
10.225 -val delim = "-";
10.226 -val thyID = takewhile [] (not o (curry op= delim)) rest;
10.227 -val rest' = dropuntil (curry op= delim) rest;
10.228 -val setc = take_fromto 1 5 rest';
10.229 -val xstr = takerest (5, rest');
10.230 -
10.231 -if Thy_Present.guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
10.232 -else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
10.233 -
10.234
10.235 "----------- debugging on Tests/solve_linear_as_rootpbl -";
10.236 "----------- debugging on Tests/solve_linear_as_rootpbl -";
10.237 @@ -319,6 +99,7 @@
10.238 if is_curr_endof_calc pt ([1],Res) then ()
10.239 else error "rewtools.sml is_curr_endof_calc ([1],Res)";
10.240
10.241 +(*//----------------- dropped with "purge code for theory-hierarchy" * )
10.242 initContext 1 Ptool.Thy_ ([1],Res);
10.243
10.244 "----- checkContext -----";
10.245 @@ -340,6 +121,7 @@
10.246
10.247 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
10.248 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
10.249 +( *//----------------- dropped with "purge code for theory-hierarchy" *)
10.250
10.251 "----------- fun is_contained_in ------------------------";
10.252 "----------- fun is_contained_in ------------------------";
11.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Apr 22 12:53:26 2021 +0200
11.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Apr 22 16:21:23 2021 +0200
11.3 @@ -569,11 +569,11 @@
11.4
11.5 setProblem 1 ["LINEAR", "univariate", "equation", "test"];
11.6 val pos = get_pos 1 1;
11.7 -setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);
11.8 +(*setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);*)
11.9 refFormula 1 (get_pos 1 1);
11.10
11.11 setMethod 1 ["Test", "solve_linear"];
11.12 -setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);
11.13 +(*setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);*)
11.14 refFormula 1 (get_pos 1 1);
11.15 val ((pt,_),_) = get_calc 1;
11.16 if get_obj g_spec pt [] = ("empty_thy_id",
11.17 @@ -612,11 +612,11 @@
11.18 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
11.19 *)
11.20 "----- \<up> ^^ and vvvvv do the same -----";
11.21 - setContext 1 p "thy_isac_Test-rls-Test_simplify";
11.22 +(*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
11.23 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
11.24
11.25 autoCalculate 1 (Steps 1);
11.26 - setContext 1 p "thy_isac_Test-rls-Test_simplify";
11.27 +(*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
11.28 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
11.29 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
11.30 if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
11.31 @@ -782,19 +782,19 @@
11.32 autoCalculate 1 (Steps 1);
11.33
11.34 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
11.35 -initContext 1 Ptool.Pbl_ ([],Pbl);
11.36 +(*initContext 1 Ptool.Pbl_ ([],Pbl);*)
11.37 (* this would break if a calculation would be inserted before: CALCID...
11.38 and pattern matching is not available in *.java.
11.39 if cut_xml xml = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_equ_univ\n. . (/GUH)\n. . (STATUS)\n. . . correct\n. . (/STATUS)\n. . (HEAD)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solve (x ^ 2 + 4 * x + 5 = 2, x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/HEAD)\n. . (MODEL)\n. . . (GIVEN)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . equality (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solveFor x\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/GIVEN)\n. . . (WHERE)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . TermC.matches (?a = ?b) (x \<up> ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/WHERE)\n. . . (FIND)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solutions L\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/FI"
11.40 then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Ptool.Pbl_ ([],Pbl); CHANGED";
11.41 *)
11.42 -initContext 1 Ptool.Met_ ([],Pbl);
11.43 +(*initContext 1 Ptool.Met_ ([],Pbl);*)
11.44 (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>*)
11.45
11.46 "--------- this match will show some incomplete items: ---------";
11.47
11.48 -checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
11.49 -checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Met_ ["LinEq", "solve_lineq_equation"]);
11.50 +(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
11.51 +checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Met_ ["LinEq", "solve_lineq_equation"]);*)
11.52
11.53
11.54 fetchProposedTactic 1;
11.55 @@ -804,9 +804,9 @@
11.56 setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Steps 1);
11.57
11.58 "--------- this is a matching model (all items correct): -------";
11.59 -checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
11.60 +(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);*)
11.61 "--------- this is a NOT matching model (some 'false': ---------";
11.62 -checkContext 1 ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR", "univariate", "equation"]);
11.63 +(*checkContext 1 ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR", "univariate", "equation"]);*)
11.64
11.65 "--------- find out a matching problem: ------------------------";
11.66 "--------- find out a matching problem (FAILING: no new pbl) ---";
12.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Thu Apr 22 12:53:26 2021 +0200
12.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Thu Apr 22 16:21:23 2021 +0200
12.3 @@ -54,7 +54,7 @@
12.4 val progthys' = (*["Program", "Tools", "ListC", "Know_Store"]*)
12.5 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
12.6 val isacrlsthms = (*length = 460*)
12.7 - thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.id * thm) list
12.8 + Thy_Hierarchy.thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.id * thm) list
12.9 val rlsthmsNOTisac = isacrlsthms (*length = 36*)
12.10 |> filter (fn (deriv, _) =>
12.11 member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
12.12 @@ -62,13 +62,13 @@
12.13 ;
12.14 (*\----- cp from Build_Thydata.thy -----------------------------------------------------------/*)
12.15 (*val thydata_list = ...*)
12.16 -(map (collect_isab "Isabelle") rlsthmsNOTisac); (* OK *)
12.17 -collect_part "IsacScripts" proglang_parent progthys'; (* OK *)
12.18 +(map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac); (* OK *)
12.19 +Thy_Hierarchy.collect_part "IsacScripts" proglang_parent progthys'; (* OK *)
12.20 (*collect_part "IsacKnowledge" knowledge_parent knowthys' (* NOT terminating *)*)
12.21
12.22 "~~~~~ fun collect_part , args:"; val (part, parent, thys) =
12.23 ("IsacKnowledge", knowledge_parent, knowthys');
12.24 -(map (collect_thms part) thys); (* OK *)
12.25 +(map (Thy_Hierarchy.collect_thms part) thys); (* OK *)
12.26 (*(collect_rlss part (KEStore_Elems.get_rlss parent) thys)(* NOT terminating *)*)
12.27 (*KEStore_Elems.get_rlss parent (* NOT terminating *)*)
12.28
13.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Apr 22 12:53:26 2021 +0200
13.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Apr 22 16:21:23 2021 +0200
13.3 @@ -11,7 +11,6 @@
13.4 "table of contents --------------------------------------";
13.5 "--------------------------------------------------------";
13.6 "----------- change to TermC.parse ctxt -----------------------";
13.7 -"----------- debugging setContext..pbl_ -----------------";
13.8 "----------- tryrefine ----------------------------------";
13.9 "----------- search for Or_to_List ----------------------";
13.10 "----------- check thy in CalcTreeTEST ------------------";
13.11 @@ -30,39 +29,6 @@
13.12 ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
13.13 (*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run =====================*)
13.14
13.15 -"----------- debugging setContext..pbl_ -----------------";
13.16 -"----------- debugging setContext..pbl_ -----------------";
13.17 -"----------- debugging setContext..pbl_ -----------------";
13.18 -reset_states ();
13.19 -CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
13.20 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
13.21 - ["Test", "squ-equ-test-subpbl1"]))];
13.22 -Iterator 1;
13.23 -moveActiveRoot 1; modelProblem 1;
13.24 -
13.25 -val pos as (p,_) = ([],Pbl);
13.26 -val guh = "pbl_equ_univ";
13.27 -(********************************)checkContext 1 pos guh;(**************************************)
13.28 -val ((pt, ([], Pbl)), []) = get_calc 1;
13.29 -val pp = par_pblobj pt p;
13.30 -val keID = Ptool.guh2kestoreID guh;
13.31 -case context_pbl keID pt pp of (true, ["univariate", "equation"], _, _, _) => ()
13.32 -| _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
13.33 -
13.34 -case get_obj g_spec pt p of (_, ["empty_probl_id"], _) => ()
13.35 -| _ => error "mathengine.sml: context_pbl .. pbl still empty";
13.36 -(********************************)setContext 1 pos guh;(***************************************)
13.37 -val ((pt, ([], Pbl)), []) = get_calc 1;
13.38 -case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
13.39 -| _ => error "mathengine.sml: context_pbl .. pbl set";
13.40 -
13.41 -
13.42 -setContext 1 pos "met_eq_lin";
13.43 -val ((pt,_),_) = get_calc 1;
13.44 -case get_obj g_spec pt p of
13.45 - ("empty_thy_id", ["univariate", "equation"], ["LinEq", "solve_lineq_equation"]) => ()
13.46 -| _ => error "mathengine.sml: context_pbl .. pbl set";
13.47 -
13.48
13.49 "----------- tryrefine ----------------------------------";
13.50 "----------- tryrefine ----------------------------------";
14.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Apr 22 12:53:26 2021 +0200
14.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Apr 22 16:21:23 2021 +0200
14.3 @@ -263,7 +263,6 @@
14.4
14.5 ML_file "BridgeLibisabelle/thy-present.sml"
14.6 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
14.7 - ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*)
14.8 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
14.9 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
14.10 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)