1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Apr 28 17:50:18 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Apr 28 19:39:06 2020 +0200
1.3 @@ -6,7 +6,6 @@
1.4 *)
1.5 theory BaseDefinitions imports Know_Store
1.6 begin
1.7 - ML_file calcelems.sml
1.8 ML_file termC.sml
1.9 ML_file substitution.sml
1.10 ML_file contextC.sml
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 28 17:50:18 2020 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,63 +0,0 @@
2.4 -(* ~~/src/Tools/isac/calcelems.sml
2.5 - elements of calculations.
2.6 - they are partially held in association lists as ref's for
2.7 - switching language levels (meta-string, object-values).
2.8 - in order to keep these ref's during re-evaluation of code,
2.9 - they are defined here at the beginning of the code.
2.10 - Author: Walther Neuper 2003
2.11 - (c) copyright due to lincense terms
2.12 -*)
2.13 -
2.14 -signature CALC_ELEMENT =
2.15 -sig
2.16 -
2.17 - eqtype filename
2.18 - eqtype filepath
2.19 -
2.20 - val maxthy: theory -> theory -> theory
2.21 -
2.22 - type pbt_ = string * (term * term)
2.23 - val update_hrls: Thy_Write.thydata -> Error_Pattern_Def.id list -> Thy_Write.thydata
2.24 -
2.25 -end
2.26 -
2.27 -(**)
2.28 -structure Celem(**): CALC_ELEMENT(**) =
2.29 -struct
2.30 -(**)
2.31 -
2.32 -type filepath = string;
2.33 -type filename = string;
2.34 -
2.35 -fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
2.36 -
2.37 -
2.38 -(* types for problems models (TODO rename to specification models) *)
2.39 -type pbt_ =
2.40 - (string * (* field "#Given",..*)(*deprecated due to 'type pat'*)
2.41 - (term * (* description *)
2.42 - term)); (* id | struct-var *)
2.43 -
2.44 -(* for dialog-authoring *)
2.45 -fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
2.46 - let
2.47 - val rls' =
2.48 - case rls of
2.49 - Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
2.50 - => Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
2.51 - calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
2.52 - | Rule_Set.Sequence {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
2.53 - => Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
2.54 - calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
2.55 - | Rule_Set.Rrls {id, prepat, rew_ord, erls, calc, scr, ...}
2.56 - => Rule_Set.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
2.57 - scr = scr, errpatts = errpatIDs}
2.58 - | Erls => Erls
2.59 - in
2.60 - Thy_Write.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
2.61 - thy_rls = (thyID, rls')}
2.62 - end
2.63 - | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
2.64 -
2.65 -end (*struct*)
2.66 -
3.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Tue Apr 28 17:50:18 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Tue Apr 28 19:39:06 2020 +0200
3.3 @@ -15,6 +15,8 @@
3.4
3.5 val id_empty: id
3.6 val Isac: 'a -> theory
3.7 + val parent_of: theory -> theory -> theory
3.8 +
3.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.10 (*NONE*)
3.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.12 @@ -43,4 +45,6 @@
3.13 val id_empty = "empty_thy_id";
3.14 fun Isac _ = Proof_Context.theory_of (id_to_ctxt "Isac_Knowledge");
3.15
3.16 +fun parent_of thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
3.17 +
3.18 (**)end(**)
4.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 17:50:18 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 19:39:06 2020 +0200
4.3 @@ -2,14 +2,46 @@
4.4 author: Walther Neuper 2004
4.5 (c) isac-team
4.6 *)
4.7 +signature PROBLEM_METHOD_HIERARCHY =
4.8 +sig
4.9 + eqtype filepath
4.10 + val file2str: filepath -> Thy_Present.filename -> string
4.11 + val hierarchy: string -> 'a Store.node list -> string
4.12 + val hierarchy_met: Method.T Store.node list -> xml
4.13 + val hierarchy_pbl: Problem.T Store.node list -> xml
4.14 + val i: int
4.15 + val id2filename: string list -> string
4.16 + val met2file: filepath -> Pos.pos -> Method.id -> Method.T -> unit
4.17 + val met2xml: Method.id -> Method.T -> xml
4.18 + val met_hierarchy2file: filepath -> unit
4.19 + val mets2file: filepath -> unit
4.20 + val node: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node -> unit
4.21 + val nodes: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node list -> unit
4.22 + val pbl2file: filepath -> Pos.pos -> Method.id -> Problem.T -> unit
4.23 + val pbl2term: theory -> Specify.pblRD -> term
4.24 + val pbl2xml: Problem.id -> Problem.T -> xml
4.25 + val pbl_hierarchy2file: filepath -> unit
4.26 + val pbls2file: filepath -> unit
4.27 + val pos2filename: int list -> string
4.28 + val str2file: Thy_Present.filename -> string -> unit
4.29 + val update_metdata: Method.T -> Error_Pattern_Def.T list -> Method.T
4.30 + val update_metpair: theory -> Method.id -> Error_Pattern_Def.T list -> Method.T * Method.id
4.31 +end
4.32
4.33 -fun file2str (path : Celem.filepath) (fnm : Celem.filename) =
4.34 +(**)
4.35 +structure Pbl_Met_Hierarchy(**): PROBLEM_METHOD_HIERARCHY(**) =
4.36 +struct
4.37 +(**)
4.38 +
4.39 +type filepath = string;
4.40 +
4.41 +fun file2str path fnm =
4.42 let
4.43 val file = TextIO.openIn (path ^ fnm)
4.44 val str = TextIO.inputAll file
4.45 in TextIO.closeIn file; str end
4.46
4.47 -fun str2file (fnm : Celem.filename) (str : string) =
4.48 +fun str2file (fnm : Thy_Present.filename) (str : string) =
4.49 let val file = TextIO.openOut fnm
4.50 in
4.51 TextIO.output (file, str);
4.52 @@ -83,7 +115,7 @@
4.53 (* (writeln o hierarchy_pbl) (!ptyps);
4.54 *)
4.55
4.56 -fun pbl_hierarchy2file (path : Celem.filepath) =
4.57 +fun pbl_hierarchy2file path =
4.58 str2file (path ^ "pbl_hierarchy.xml")
4.59 ("<NODE>\n" ^
4.60 " <ID> problem hierarchy </ID>\n" ^
4.61 @@ -92,7 +124,7 @@
4.62 (hierarchy_pbl (get_ptyps ())) ^
4.63 "</NODE>");
4.64
4.65 -fun met_hierarchy2file (path : Celem.filepath) =
4.66 +fun met_hierarchy2file path =
4.67 str2file (path ^ "met_hierarchy.xml")
4.68 ("<NODE>\n" ^
4.69 " <ID> method hierarchy </ID>\n" ^
4.70 @@ -181,7 +213,7 @@
4.71
4.72
4.73 (**. write pbls from hierarchy to files.**)
4.74 -fun pbl2file (path: Celem.filepath) (pos: Pos.pos) (id:Method.id) (pbl as {guh,...}) =
4.75 +fun pbl2file path (pos: Pos.pos) (id: Method.id) (pbl as {guh, ...}) =
4.76 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos);
4.77 ((str2file (path ^ Thy_Present.guh2filename guh)) o (pbl2xml id)) pbl
4.78 );
4.79 @@ -254,17 +286,17 @@
4.80 *)
4.81
4.82 (*.write the files using an int-key (pos') as filename.*)
4.83 -fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Method.id) met =
4.84 +fun met2file path (pos: Pos.pos) (id: Method.id) met =
4.85 (writeln ("### met2file: id = " ^ strs2str id);
4.86 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
4.87
4.88 (*.write the files using the guh as filename.*)
4.89 -fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Method.id) (met as {guh,...}) =
4.90 +fun met2file path (pos: Pos.pos) (id: Method.id) (met as {guh,...}) =
4.91 (writeln ("### met2file: id = " ^ strs2str id);
4.92 ((str2file (path ^ Thy_Present.guh2filename guh)) o (met2xml id)) met);
4.93
4.94 (*.scan the mtree Ptyp and print the nodes using wfn.*)
4.95 -fun node (pa: Celem.filepath) ids po wfn (Store.Node (id,[n],ns)) =
4.96 +fun node pa ids po wfn (Store.Node (id, [n], ns)) =
4.97 let val po' = Pos.lev_on po
4.98 in
4.99 wfn pa po' (ids@[id]) n;
4.100 @@ -274,8 +306,8 @@
4.101 | nodes pa ids po wfn (n::ns) =
4.102 (node pa ids po wfn n; nodes pa ids (Pos.lev_on po) wfn ns);
4.103
4.104 -fun pbls2file (p: Celem.filepath) = nodes p [] [0] pbl2file (get_ptyps ());
4.105 -fun mets2file (p: Celem.filepath) = nodes p [] [0] met2file (get_mets ());
4.106 +fun pbls2file path = nodes path [] [0] pbl2file (get_ptyps ());
4.107 +fun mets2file path = nodes path [] [0] met2file (get_mets ());
4.108 (*
4.109 val path = "/home/neuper/proto2/isac/xmldata/";
4.110 val path = "/home/neuper/tmp/";
4.111 @@ -302,3 +334,5 @@
4.112 val ret = (update_metdata (Specify.get_met' thy metID) errpats, metID)
4.113 handle ERROR _ => error ("update_metpair: " ^ (strs2str metID) ^ " must address a method");
4.114 in ret end;
4.115 +
4.116 +(**)end(**)
5.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 17:50:18 2020 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 19:39:06 2020 +0200
5.3 @@ -17,6 +17,7 @@
5.4 val hierarchy_guh: 'a Store.T -> string
5.5 val insert_errpatIDs: 'a -> Thy_Write.theID -> Error_Pattern_Def.id list ->
5.6 Thy_Write.thydata * Thy_Write.theID
5.7 + val update_hrls: Thy_Write.thydata -> Error_Pattern_Def.id list -> Thy_Write.thydata
5.8
5.9 val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Thy_Write.theID * Thy_Write.thydata
5.10 val makeHord: string * ThyC.id -> string * Rule_Def.rew_ord_ ->
5.11 @@ -35,19 +36,19 @@
5.12
5.13 val show_thes: unit -> unit
5.14
5.15 - val thes2file: Celem.filepath -> unit
5.16 + val thes2file: Pbl_Met_Hierarchy.filepath -> unit
5.17 val thms_of: theory -> thm list
5.18 val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->
5.19 (string * thm) list
5.20 - val thy_hierarchy2file: Celem.filepath -> unit
5.21 - val thydata2file: Celem.filepath -> Pos.pos -> Thy_Write.theID -> Thy_Write.thydata -> unit
5.22 + val thy_hierarchy2file: Pbl_Met_Hierarchy.filepath -> unit
5.23 + val thydata2file: Pbl_Met_Hierarchy.filepath -> Pos.pos -> Thy_Write.theID -> Thy_Write.thydata -> unit
5.24 val thydata2xml: Thy_Write.theID * Thy_Write.thydata -> xml
5.25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.26 (*NONE*)
5.27 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.28 - val thenode: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->
5.29 + val thenode: Pbl_Met_Hierarchy.filepath -> string list -> Pos.pos -> (Pbl_Met_Hierarchy.filepath -> Pos.pos ->
5.30 string list -> 'a -> 'b) -> 'a Store.node -> unit
5.31 - val thenodes: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->
5.32 + val thenodes: Pbl_Met_Hierarchy.filepath -> string list -> Pos.pos -> (Pbl_Met_Hierarchy.filepath -> Pos.pos ->
5.33 string list -> 'a -> 'b) -> 'a Store.T -> unit
5.34 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.35 end
5.36 @@ -161,8 +162,8 @@
5.37 | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Pos.lev_on p) theID ns);
5.38 in nodes j [0] [] h end;
5.39
5.40 -fun thy_hierarchy2file (path: Celem.filepath) =
5.41 - str2file (path ^ "thy_hierarchy.xml")
5.42 +fun thy_hierarchy2file (path: Pbl_Met_Hierarchy.filepath) =
5.43 + Pbl_Met_Hierarchy.str2file (path ^ "thy_hierarchy.xml")
5.44 ("<NODE>\n" ^
5.45 " <ID> theory hierarchy </ID>\n" ^
5.46 " <NO> 1 </NO>\n" ^
5.47 @@ -217,12 +218,12 @@
5.48 error ("thydata2xml: not implemented for "^ strs2str' theID);
5.49
5.50 (* analoguous to 'fun met2file' *)
5.51 -fun thydata2file (path : Celem.filepath) (pos : Pos.pos) (theID : Thy_Write.theID) thydata =
5.52 +fun thydata2file (path : Pbl_Met_Hierarchy.filepath) (pos : Pos.pos) (theID : Thy_Write.theID) thydata =
5.53 (writeln ("### thes2file: id = " ^ strs2str theID);
5.54 - str2file (path ^ Thy_Present.theID2filename theID) (thydata2xml (theID, thydata)));
5.55 + Pbl_Met_Hierarchy.str2file (path ^ Thy_Present.theID2filename theID) (thydata2xml (theID, thydata)));
5.56
5.57 (* analoguous to 'fun node' *)
5.58 -fun thenode (pa : Celem.filepath) ids po wfn (Store.Node (id, [n], ns)) =
5.59 +fun thenode (pa : Pbl_Met_Hierarchy.filepath) ids po wfn (Store.Node (id, [n], ns)) =
5.60 let val po' = Pos.lev_on po
5.61 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Pos.lev_dn po') wfn ns end
5.62 and thenodes _ _ _ _ [] = ()
5.63 @@ -230,7 +231,7 @@
5.64 (thenode pa ids po wfn n; thenodes pa ids (Pos.lev_on po) wfn ns);
5.65
5.66 (* analoguous to 'fun mets2file' *)
5.67 -fun thes2file (p : Celem.filepath) = thenodes p [] [0] thydata2file (get_thes ());
5.68 +fun thes2file (p : Pbl_Met_Hierarchy.filepath) = thenodes p [] [0] thydata2file (get_thes ());
5.69
5.70
5.71 (***.store a single theory element in the hierarchy.***)
5.72 @@ -284,10 +285,31 @@
5.73 val the = Thy_Write.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
5.74 in (the, theID) end
5.75
5.76 +(* for dialog-authoring *)
5.77 +fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
5.78 + let
5.79 + val rls' =
5.80 + case rls of
5.81 + Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
5.82 + => Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
5.83 + calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
5.84 + | Rule_Set.Sequence {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
5.85 + => Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
5.86 + calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
5.87 + | Rule_Set.Rrls {id, prepat, rew_ord, erls, calc, scr, ...}
5.88 + => Rule_Set.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
5.89 + scr = scr, errpatts = errpatIDs}
5.90 + | Erls => Erls
5.91 + in
5.92 + Thy_Write.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
5.93 + thy_rls = (thyID, rls')}
5.94 + end
5.95 + | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
5.96 +
5.97 fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)
5.98 let
5.99 val hrls = Specify.get_the theID
5.100 - val hrls' = Celem.update_hrls hrls errpatIDs
5.101 + val hrls' = update_hrls hrls errpatIDs
5.102 handle ERROR _ => error ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
5.103 in (hrls', theID) end
5.104
6.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-present.sml Tue Apr 28 17:50:18 2020 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-present.sml Tue Apr 28 19:39:06 2020 +0200
6.3 @@ -8,6 +8,8 @@
6.4 signature THEORY_DATA_PRESENTATION =
6.5 sig
6.6
6.7 + eqtype filename
6.8 +
6.9 datatype contthy
6.10 = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
6.11 | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
6.12 @@ -20,9 +22,9 @@
6.13 bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
6.14 rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}
6.15 | EContThy
6.16 - val guh2filename : Check_Unique.id -> Celem.filename
6.17 + val guh2filename : Check_Unique.id -> filename
6.18 val thms_of_rls : Rule_Set.T -> Rule.rule list
6.19 - val theID2filename : Thy_Write.theID -> Celem.filename
6.20 + val theID2filename : Thy_Write.theID -> filename
6.21 val no_thycontext : Check_Unique.id -> bool
6.22 val subs_from : Istate.T -> 'a -> Check_Unique.id -> Subst.input
6.23 val guh2rewtac : Check_Unique.id -> Subst.input -> Tactic.input
6.24 @@ -41,6 +43,8 @@
6.25 struct
6.26 (**)
6.27
6.28 +type filename = string;
6.29 +
6.30 (* packing return-values to matchTheory, contextToThy for xml-generation *)
6.31 datatype contthy = (*also an item from Know_Store on Browser ...........#*)
6.32 EContThy (* not from Know_Store ..............................*)
7.1 --- a/src/Tools/isac/Build_Isac.thy Tue Apr 28 17:50:18 2020 +0200
7.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Apr 28 19:39:06 2020 +0200
7.3 @@ -24,7 +24,6 @@
7.4 ML_file rule.sml
7.5 ML_file "error-fill-def.sml"
7.6 ML_file "rule-set.sml"
7.7 - ML_file calcelems.sml
7.8 theory BaseDefinitions imports Know_Store
7.9 ML_file termC.sml
7.10 ML_file contextC.sml
8.1 --- a/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy Tue Apr 28 17:50:18 2020 +0200
8.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy Tue Apr 28 19:39:06 2020 +0200
8.3 @@ -445,7 +445,6 @@
8.4 certain location:
8.5 \<close>
8.6 (*<*)ML \<open>
8.7 -open Celem
8.8 open LI
8.9 \<close>
8.10 ML(*>*) \<open>
9.1 --- a/src/Tools/isac/Interpret/istate.sml Tue Apr 28 17:50:18 2020 +0200
9.2 +++ b/src/Tools/isac/Interpret/istate.sml Tue Apr 28 19:39:06 2020 +0200
9.3 @@ -60,8 +60,6 @@
9.4 struct
9.5 (**)
9.6
9.7 -open Celem
9.8 -
9.9 datatype asap = datatype Istate_Def.asap
9.10 val asap2str = Istate_Def.asap2str
9.11
10.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Tue Apr 28 17:50:18 2020 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Tue Apr 28 19:39:06 2020 +0200
10.3 @@ -112,7 +112,7 @@
10.4 subsubsection \<open>Error patterns for differentiation\<close>
10.5
10.6 setup \<open>KEStore_Elems.add_mets
10.7 - [update_metpair @{theory Diff} ["diff","differentiate_on_R"]
10.8 + [Pbl_Met_Hierarchy.update_metpair @{theory Diff} ["diff","differentiate_on_R"]
10.9 [("chain-rule-diff-both",
10.10 [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
10.11 TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
10.12 @@ -142,7 +142,7 @@
10.13 subsubsection \<open>Error patterns for calculation with rationals\<close>
10.14
10.15 setup \<open>KEStore_Elems.add_mets
10.16 - [update_metpair @{theory Rational} ["simplification", "of_rationals"]
10.17 + [Pbl_Met_Hierarchy.update_metpair @{theory Rational} ["simplification", "of_rationals"]
10.18 [("addition-of-fractions",
10.19 [TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
10.20 TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
11.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Tue Apr 28 17:50:18 2020 +0200
11.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Tue Apr 28 19:39:06 2020 +0200
11.3 @@ -31,8 +31,6 @@
11.4 struct
11.5 (**)
11.6
11.7 -open Celem
11.8 -
11.9 datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or *)
11.10 ORundef (* undefined: set only by (topmost) Or *)
11.11 | AssOnly (* do not execute applicable Prog_Tac - there could be an associated
12.1 --- a/src/Tools/isac/Specify/input-calchead.sml Tue Apr 28 17:50:18 2020 +0200
12.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Tue Apr 28 19:39:06 2020 +0200
12.3 @@ -5,6 +5,8 @@
12.4
12.5 signature INPUT_CALCHEAD =
12.6 sig
12.7 + type pbt_ = string * (term * term)
12.8 +
12.9 datatype iitem = Find of TermC.as_string list | Given of TermC.as_string list | Relate of TermC.as_string list
12.10 type imodel = iitem list
12.11 type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * Spec.T
12.12 @@ -25,13 +27,19 @@
12.13 structure In_Chead(**): INPUT_CALCHEAD(**) =
12.14 struct
12.15
12.16 +(* types for problems models (TODO rename to specification models) *)
12.17 +type pbt_ =
12.18 + (string * (* field "#Given",..*)(*deprecated due to 'type pat'*)
12.19 + (term * (* description *)
12.20 + term)); (* id | struct-var *)
12.21 +
12.22 (*** handle an input by CAS-command ***)
12.23
12.24 fun dtss2itm_ ppc (d, ts) =
12.25 let
12.26 val (f, (d, id)) = the (find_first ((curry op= d) o
12.27 (#1: (term * term) -> term) o
12.28 - (#2: Celem.pbt_ -> (term * term))) ppc)
12.29 + (#2: pbt_ -> (term * term))) ppc)
12.30 in
12.31 ([1], true, f, Model.Cor ((d, ts), (id, ts)))
12.32 end
13.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 17:50:18 2020 +0200
13.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 19:39:06 2020 +0200
13.3 @@ -39,7 +39,7 @@
13.4 Exception- OPTION raised
13.5 *)
13.6
13.7 -if pbl2xml ["Biegelinien"] (get_pbt ["Biegelinien"]) =
13.8 +if Pbl_Met_Hierarchy.pbl2xml ["Biegelinien"] (get_pbt ["Biegelinien"]) =
13.9 "<NODECONTENT>\n"^
13.10 " <GUH> pbl_bieg </GUH>\n"^
13.11 " <STRINGLIST>\n"^
13.12 @@ -120,14 +120,14 @@
13.13 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";
13.14 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";
13.15 val path = "/tmp/";
13.16 -"~~~~~ fun pbls2file, args:"; val (p:filepath) = (path ^ "pbl/");
13.17 +"~~~~~ fun pbls2file, args:"; val (p: Pbl_Met_Hierarchy.filepath) = (path ^ "pbl/");
13.18 get_ptyps (); (*not = []*)
13.19 "~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
13.20 - (p, []: string list, [0], pbl2file, (get_ptyps ()));
13.21 -"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Store.Node (id,[n],ns)) = (pa, ids, po, wfn, n);
13.22 + (p, []: string list, [0], Pbl_Met_Hierarchy.pbl2file, (get_ptyps ()));
13.23 +"~~~~~ fun node, args:"; val (pa: Pbl_Met_Hierarchy.filepath, ids, po, wfn, Store.Node (id,[n],ns)) = (pa, ids, po, wfn, n);
13.24 val po' = lev_on po;
13.25 wfn (*= pbl2file*)
13.26 -"~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id: Method.id), (pbl as {guh,...})) =
13.27 +"~~~~~ fun pbl2file, args:"; val ((path:Pbl_Met_Hierarchy.filepath), (pos:pos), (id: Method.id), (pbl as {guh,...})) =
13.28 (pa, po', (ids@[id]), n);
13.29 strs2str id = "[\"e_pblID\"]"; (*true*)
13.30 pos2str pos = "[1]"; (*true*)
13.31 @@ -144,7 +144,7 @@
13.32 "----- fun pbl2term ----------------------------------------------";
13.33 "----- fun pbl2term ----------------------------------------------";
13.34 (*see WN120405a.TODO.txt*)
13.35 -if UnparseC.term (pbl2term (ThyC.get_theory "Isac_Knowledge") ["equations","univariate","normalise"]) =
13.36 +if UnparseC.term (Pbl_Met_Hierarchy.pbl2term (ThyC.get_theory "Isac_Knowledge") ["equations","univariate","normalise"]) =
13.37 "Problem (Isac_Knowledge', [normalise, univariate, equations])"
13.38 then () else error "fun pbl2term changed";
13.39
14.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 17:50:18 2020 +0200
14.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 19:39:06 2020 +0200
14.3 @@ -90,9 +90,9 @@
14.4 "----------- search for data error in thes2file ------------------";
14.5 "----------- search for data error in thes2file ------------------";
14.6 val TESTdump = Unsynchronized.ref
14.7 - ("path": filepath, ["ids"]: Thy_Write.theID, []: pos, thydata2file, Store.Node ("xxx", [], []): Thy_Write.thydata Store.node);
14.8 + ("path": Pbl_Met_Hierarchy.filepath, ["ids"]: Thy_Write.theID, []: pos, thydata2file, Store.Node ("xxx", [], []): Thy_Write.thydata Store.node);
14.9
14.10 -fun TESTthenode (pa:filepath) ids po wfn (Store.Node (id, [n], ns)) TESTids =
14.11 +fun TESTthenode (pa:Pbl_Met_Hierarchy.filepath) ids po wfn (Store.Node (id, [n], ns)) TESTids =
14.12 let val po' = lev_on po
14.13 in
14.14 if (ids@[id]) = TESTids
14.15 @@ -111,7 +111,7 @@
14.16 val j = indentation;
14.17 (* \--- side effects from previous test files ---/*)
14.18
14.19 -"~~~~~ fun thes2file, args:"; val (p : filepath) = ("/tmp/");
14.20 +"~~~~~ fun thes2file, args:"; val (p : Pbl_Met_Hierarchy.filepath) = ("/tmp/");
14.21 (* recursively descend into thehier just before the error
14.22 by setting TESTids according to the last line in ouput
14.23 ### thes2file: id = : *)
14.24 @@ -122,7 +122,7 @@
14.25 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
14.26 val (pa, ids, po', wfn, (Store.Node (id, [n], ns))) = ! TESTdump;
14.27 ;
14.28 -"~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:Thy_Write.theID), thydata) =
14.29 +"~~~~~ fun thydata2file, args:"; val ((xmldata:Pbl_Met_Hierarchy.filepath), (pos:pos), (theID:Thy_Write.theID), thydata) =
14.30 (pa, po', (ids@[id]), n);
14.31 "~~~~~ fun thydata2xml, args:"; val (theID, Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
14.32 (theID:Thy_Write.theID, thydata);
14.33 @@ -331,15 +331,15 @@
14.34 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
14.35 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
14.36 fun MINIget_the (theID : Thy_Write.theID) = Store.get MINIthehier theID theID (*see ptyps.sml*)
14.37 -fun MINIthy_hierarchy2file (path:filepath) =
14.38 - str2file (path ^ "thy_hierarchy.xml")
14.39 +fun MINIthy_hierarchy2file (path:Pbl_Met_Hierarchy.filepath) =
14.40 + Pbl_Met_Hierarchy.str2file (path ^ "thy_hierarchy.xml")
14.41 ("<NODE>\n" ^
14.42 " <ID> theory hierarchy </ID>\n" ^
14.43 " <NO> 1 </NO>\n" ^
14.44 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
14.45 (hierarchy_guh MINIthehier) ^
14.46 "</NODE>");
14.47 -fun MINIthes2file (p : filepath) = thenodes p [] [0] thydata2file MINIthehier;
14.48 +fun MINIthes2file (p : Pbl_Met_Hierarchy.filepath) = thenodes p [] [0] thydata2file MINIthehier;
14.49
14.50 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
14.51 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
14.52 @@ -351,7 +351,7 @@
14.53 val path = "/tmp/"
14.54 ;
14.55 MINIthy_hierarchy2file path (* ---> /tmp/thy_hierarchy.xml *);
14.56 -writeln (file2str path "thy_hierarchy.xml") (* better check in editor *)
14.57 +writeln (Pbl_Met_Hierarchy.file2str path "thy_hierarchy.xml") (* better check in editor *)
14.58 ;
14.59 MINIthes2file path (* ---> /tmp/thy_... *);
14.60
14.61 @@ -361,7 +361,7 @@
14.62 "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
14.63 "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
14.64 (path, [], [0], thydata2file, MINIthehier);
14.65 -"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Store.Node (id, [n], ns))) =
14.66 +"~~~~~ fun thenode, args:"; val ((pa : Pbl_Met_Hierarchy.filepath), ids, po, wfn, (Store.Node (id, [n], ns))) =
14.67 (pa, ids, po, wfn, n);
14.68 val po' = lev_on po;
14.69 (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *)
14.70 @@ -372,7 +372,7 @@
14.71 Thy_Write.Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()
14.72 | _ => error "a change inhibits successful continuation of this test";
14.73 val (theID, thydata) = hd thydata_list;
14.74 -"~~~~~ fun thydata2file, args:"; val ((path : filepath), (pos : pos), (theID : Thy_Write.theID), thydata) =
14.75 +"~~~~~ fun thydata2file, args:"; val ((path : Pbl_Met_Hierarchy.filepath), (pos : pos), (theID : Thy_Write.theID), thydata) =
14.76 (pa, po', (*ids @ [id]*)theID, (*n*)thydata);
14.77 "~~~~~ fun thydata2xml, args:"; val ((theID, Thy_Write.Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=
14.78 ((theID, thydata));
15.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Apr 28 17:50:18 2020 +0200
15.2 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Apr 28 19:39:06 2020 +0200
15.3 @@ -440,7 +440,7 @@
15.4
15.5 Rewrite.trace_on := false;
15.6 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
15.7 -Celem.Rewrite.trace_on := false;
15.8 +Rewrite.trace_on := false;
15.9 (* Rewrite.trace_on:
15.10 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
15.11 (* |||||||||||||||||||||||||||||||||||| *)
15.12 @@ -481,9 +481,9 @@
15.13 (*AA :: real*)
15.14 (* we get details from here..*)
15.15
15.16 -Celem.Rewrite.trace_on := false;
15.17 +Rewrite.trace_on := false;
15.18 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
15.19 -Celem.Rewrite.trace_on := false;
15.20 +Rewrite.trace_on := false;
15.21 (* Rewrite.trace_on:
15.22 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
15.23 (* |||||||||||||||||||||||||||||||||||| *)
16.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Apr 28 17:50:18 2020 +0200
16.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Apr 28 19:39:06 2020 +0200
16.3 @@ -151,7 +151,7 @@
16.4 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
16.5 val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
16.6 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
16.7 - val dI = Context.theory_name (maxthy thy thy');
16.8 + val dI = Context.theory_name (ThyC.parent_of thy thy');
16.9 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
16.10 cas = NONE; (*true*)
16.11 val hdl = pblterm dI pI;
17.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Tue Apr 28 17:50:18 2020 +0200
17.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Tue Apr 28 19:39:06 2020 +0200
17.3 @@ -16,7 +16,7 @@
17.4 (*if*) mI = ["no_met"]; (*else*)
17.5 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
17.6 val {cas, ppc, thy=thy',...} = get_pbt pI
17.7 - val dI = Context.theory_name (maxthy thy thy');
17.8 + val dI = Context.theory_name (ThyC.parent_of thy thy');
17.9 val hdl =
17.10 case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
17.11 | _ => error "Minisubplb/100-init-rootpbl.sml no headline"