1.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 15:42:50 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 16:16:11 2020 +0200
1.3 @@ -10,121 +10,30 @@
1.4
1.5 signature CALC_ELEMENT =
1.6 sig
1.7 -(*/------- to Celem7 -------\* )
1.8 - type cas_elem
1.9 - val cas_eq: cas_elem * cas_elem -> bool
1.10 -( *\------- to Celem7 -------/*)
1.11
1.12 -(*/------- to Celem5 -------\* )
1.13 - type pbt = Probl_Def.T
1.14 - val e_pbt: pbt;
1.15 - val e_Ptyp: pbt Store.node
1.16 - type ptyps = Probl_Def.store
1.17 - val pbts2str: pbt list -> string
1.18 -( *\------- to Celem5 -------/*)
1.19 -
1.20 -(*/------- to Spec -------\* )
1.21 - type metID
1.22 - type pblID
1.23 - type spec
1.24 - val spec2str: string * string list * string list -> string
1.25 - val metID2str: string list -> string
1.26 - val e_pblID: pblID
1.27 - val e_metID: metID
1.28 - val empty_spec: spec
1.29 - val e_spec: spec
1.30 -( *\------- to Spec -------/*)
1.31 -
1.32 -(*/------- to Store -------\* )
1.33 -(*datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list\*)
1.34 - val merge_ptyps: 'a Store.T * 'a Store.T -> 'a Store.T
1.35 - val insrt: Spec.pblID -> 'a -> string list -> 'a Store.T -> 'a Store.T
1.36 - val get_py: 'a Store.T -> Spec.pblID -> string list -> 'a
1.37 - val update_ptyps: string list -> string list -> 'a -> 'a Store.T -> 'a Store.T
1.38 - val app_py: 'a Store.T -> ('a Store.node -> 'b) -> Spec.pblID -> string list -> 'b
1.39 -( *\------- to Store -------/*)
1.40 -
1.41 -(*/------- to Celem2 -------\* )
1.42 - type guh
1.43 -( *\------- to Celem2 -------/*)
1.44 -
1.45 -(*/------- to Celem8 -------\* )
1.46 - type authors = Thy_Html.authors
1.47 - datatype thydata = datatype Thy_Html.thydata
1.48 - type theID = Thy_Html.theID
1.49 - val theID2str: string list -> string
1.50 - val the2str: thydata -> string
1.51 - val thes2str: thydata list -> string
1.52 - val theID2thyID: theID -> ThyC.id
1.53 -
1.54 - val part2guh: theID -> Check_Unique.guh
1.55 - val thy2guh: theID -> Check_Unique.guh
1.56 - val thypart2guh: theID -> Check_Unique.guh
1.57 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.guh
1.58 - val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.guh
1.59 - val cal2guh: string * ThyC.id -> string -> Check_Unique.guh
1.60 - val ord2guh: string * ThyC.id -> string -> string
1.61 - val theID2guh: theID -> Check_Unique.guh
1.62 -
1.63 - val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
1.64 - val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
1.65 -( *\------- to Celem8 -------/*)
1.66 -
1.67 -(*/------- to Celem6 -------\* )
1.68 - type met = Meth_Def.T
1.69 - type mets = Meth_Def.store
1.70 - val e_Mets: met Store.node
1.71 -( *\------- to Celem6 -------/*)
1.72 -
1.73 -(*/------- to Celem91 -------\* )
1.74 - val check_guhs_unique: bool Unsynchronized.ref
1.75 - val coll_pblguhs: Probl_Def.T Store.T -> Check_Unique.guh list
1.76 - val check_pblguh_unique: Check_Unique.guh -> Probl_Def.T Store.T -> unit
1.77 - val coll_metguhs: Meth_Def.T Store.T -> Check_Unique.guh list
1.78 - val check_metguh_unique: Check_Unique.guh -> Meth_Def.T Store.T -> unit
1.79 -( *\------- to Celem91 -------/*)
1.80 -
1.81 - val linefeed: string -> string
1.82 - val trace_calc: bool Unsynchronized.ref
1.83 - val trace_rewrite: bool Unsynchronized.ref
1.84 - val depth: int Unsynchronized.ref
1.85 - datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
1.86 - type kestoreID
1.87 - val ketype2str: ketype -> string
1.88 -
1.89 -(*/------- to Celem4 -------\* )
1.90 - type pat = Celem4.pat
1.91 - val pats2str: pat list -> string
1.92 - val pats2str' : Celem4.pat list -> string
1.93 -( *\------- to Celem4 -------/*)
1.94 -
1.95 - val maxthy: theory -> theory -> theory
1.96 - eqtype filename
1.97 - val lim_deriv: int Unsynchronized.ref
1.98 - val isabthys: unit -> theory list
1.99 - val partID': ThyC.id -> string
1.100 - type pbt_ = string * (term * term)
1.101 - eqtype xml
1.102 - val ketype2str': ketype -> string
1.103 - val str2ketype': string -> ketype
1.104 - eqtype filepath
1.105 - val update_hrls: Thy_Html.thydata -> Error_Fill_Def.errpatID list -> Thy_Html.thydata
1.106 eqtype iterID
1.107 eqtype calcID
1.108
1.109 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.110 - val insert_fillpats: Thy_Html.thydata Store.T -> (Spec.pblID * Error_Fill_Def.fillpat list) list -> Thy_Html.thydata Store.T ->
1.111 - Thy_Html.thydata Store.T
1.112 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.113 - val knowthys: unit -> theory list
1.114 -(*/------- to Celem6 -------\*)
1.115 - val e_met: Meth_Def.T
1.116 -(*\------- to Celem6 -------/*)
1.117 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.118 + eqtype xml
1.119
1.120 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.121 - val overwritelthy: theory -> (Rule_Set.id * (string * Rule_Set.T)) list * (Rule_Set.id * Rule_Set.T) list ->
1.122 - (Rule_Set.id * (string * Rule_Set.T)) list
1.123 + type kestoreID
1.124 +
1.125 + datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
1.126 + val ketype2str: ketype -> string
1.127 + val ketype2str': ketype -> string
1.128 + val str2ketype': string -> ketype
1.129 +
1.130 + eqtype filename
1.131 + eqtype filepath
1.132 +
1.133 + val maxthy: theory -> theory -> theory
1.134 +
1.135 + type pbt_ = string * (term * term)
1.136 + val update_hrls: Thy_Html.thydata -> Error_Fill_Def.errpatID list -> Thy_Html.thydata
1.137 +
1.138 + val isabthys: unit -> theory list
1.139 + val partID': ThyC.id -> string
1.140 +
1.141 end
1.142
1.143 (**)
1.144 @@ -132,62 +41,11 @@
1.145 struct
1.146 (**)
1.147
1.148 -val linefeed = curry op ^ "\n"; (* ?\<longrightarrow> libraryC ?*)
1.149 -
1.150 type iterID = int;
1.151 type calcID = int;
1.152
1.153 -(*/------- to Celem2 -------\*)
1.154 -type guh = Check_Unique.guh;
1.155 -(*\------- to Celem2 -------/*)
1.156 type xml = string; (* rm together with old code replaced by XML.tree *)
1.157
1.158 -
1.159 -(* WN0509 discussion:
1.160 -#############################################################################
1.161 -# How to manage theorys in subproblems wrt. the requirement, #
1.162 -# that scripts should be re-usable ? #
1.163 -#############################################################################
1.164 -
1.165 - eg. 'Program Solve_rat_equation' calls 'SubProblem (RatEq',..'
1.166 - which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
1.167 - because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
1.168 - is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
1.169 - (see match_ags).
1.170 -
1.171 - Preliminary solution:
1.172 - # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
1.173 - # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
1.174 - # however, a thy specified by the user in the rootpbl may lead to
1.175 - errors in far-off subpbls (which are not yet reported properly !!!)
1.176 - and interactively specifiying thys in subpbl is not very relevant.
1.177 -
1.178 - Other solutions possible:
1.179 - # always parse and type-check with Thy_Info_get_theory "Isac_Knowledge"
1.180 - (rejected due to the vague idea eg. to re-use equations for R in C etc.)
1.181 - # regard the subthy-relation in specifying thys of subpbls
1.182 - # specifically handle 'SubProblem (undefined, pbl, arglist)'
1.183 - # ???
1.184 -*)
1.185 -
1.186 -(*/------- to Spec -------\*)
1.187 -(*the key into the hierarchy ob problems*)
1.188 -type pblID = Spec.pblID;
1.189 -val e_pblID = Spec.e_pblID;
1.190 -type metID = Spec.metID;
1.191 -type spec = Spec.spec;
1.192 -val spec2str = Spec.spec2str;
1.193 -val e_metID = Spec.e_metID;
1.194 -val metID2str = Spec.metID2str;
1.195 -val empty_spec = Spec.empty_spec;
1.196 -val e_spec = Spec.e_spec;
1.197 -(*\------- to Spec -------/*)
1.198 -
1.199 -(*/------- to Celem7 -------\*)
1.200 -type cas_elem = CAS_Def.T;
1.201 -val cas_eq = CAS_Def.equal;
1.202 -(*\------- to Celem7 -------/*)
1.203 -
1.204 (*either theID or pblID or metID*)
1.205 type kestoreID = string list;
1.206
1.207 @@ -208,133 +66,20 @@
1.208 | str2ketype' "met" = Met_
1.209 | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
1.210
1.211 -(*/------- to Store -------\*)
1.212 -val merge_ptyps = Store.merge;
1.213 -val insrt = Store.insert;
1.214 -val app_py = Store.apply;
1.215 -val get_py = Store.get;
1.216 -val update_ptyps = Store.update;
1.217 -(*\------- to Store -------/*)
1.218 -
1.219 -(*/------- to Celem8 -------\*)
1.220 -type authors = Thy_Html.authors;
1.221 -datatype thydata = datatype Thy_Html.thydata;
1.222 -type theID = Thy_Html.theID;
1.223 -val theID2str = Thy_Html.theID2str;
1.224 -val the2str = Thy_Html.the2str;
1.225 -val thes2str = Thy_Html.thes2str;
1.226 -val theID2thyID = Thy_Html.theID2thyID;
1.227 -
1.228 -val part2guh = Thy_Html.part2guh;
1.229 -val thy2guh = Thy_Html.thy2guh;
1.230 -val thypart2guh = Thy_Html.thypart2guh;
1.231 -val thm2guh = Thy_Html.thm2guh;
1.232 -val rls2guh = Thy_Html.rls2guh;
1.233 -val cal2guh = Thy_Html.cal2guh;
1.234 -val ord2guh = Thy_Html.ord2guh;
1.235 -val theID2guh = Thy_Html.theID2guh;
1.236 -
1.237 -val add_thydata = Thy_Html.add_thydata;
1.238 -val update_hthm = Thy_Html.update_hthm;
1.239 -(*\------- to Celem8 -------/*)
1.240 -
1.241 type filepath = string;
1.242 type filename = string;
1.243
1.244 -(* overwrite an element in an association list and pair it with a thyID
1.245 - in order to create the thy_hierarchy;
1.246 - overwrites existing rls' even if they are defined in a different thy;
1.247 - this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc *)
1.248 -(* WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
1.249 - they do NOT handle overlays by re-using an identifier in different thys;
1.250 - "thyID.rlsID" would be a good solution, if the "." would be possible
1.251 - in scripts...
1.252 - actually a hack to get alltogether run again with minimal effort *)
1.253 -fun insthy thy' (rls', rls) = (rls', (thy', rls));
1.254 -fun overwritelthy thy (al, bl: (Rule_Set.id * Rule_Set.T) list) =
1.255 - let val bl' = map (insthy ((get_thy o Context.theory_name) thy)) bl
1.256 - in overwritel (al, bl') end;
1.257 -
1.258 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
1.259
1.260
1.261 -(*/------- to Trace from Celem -------\*)
1.262 -(* trace internal steps of isac's numeral calculations *)
1.263 -val trace_calc = Unsynchronized.ref false;
1.264 -(* trace internal steps of isac's rewriter *)
1.265 -val trace_rewrite = Unsynchronized.ref false;
1.266 -(* depth of recursion in traces of the rewriter, if trace_rewrite:=true *)
1.267 -val depth = Unsynchronized.ref 99999;
1.268 -(* no of rewrites exceeding this int -> NO rewrite *)
1.269 -val lim_deriv = Unsynchronized.ref 100;
1.270 -(*\------- to Trace from Celem --------/*)
1.271 -
1.272 -(*/------- to Celem4 -------\*)
1.273 -(* the pattern for an item of a problems model or a methods guard *)
1.274 -type pat = Celem4.pat;
1.275 -val pats2str = Celem4.pats2str;
1.276 -val pats2str' = Celem4.pats2str';
1.277 -(*\------- to Celem4 -------/*)
1.278 -
1.279 (* types for problems models (TODO rename to specification models) *)
1.280 type pbt_ =
1.281 (string * (* field "#Given",..*)(*deprecated due to 'type pat'*)
1.282 (term * (* description *)
1.283 term)); (* id | struct-var *)
1.284 -(*/------- to Celem5 -------\*)
1.285 -type pbt = Probl_Def.T;
1.286 -val e_pbt = Probl_Def.empty;
1.287 -val e_Ptyp = Probl_Def.empty_store;
1.288 -val pbts2str = Probl_Def.s_to_string;
1.289 -type ptyps = Probl_Def.store;
1.290 -(*\------- to Celem5 -------/*)
1.291 -
1.292 -(*/------- to Celem6 -------\*)
1.293 -type met = Meth_Def.T;
1.294 -val e_met = Meth_Def.empty;
1.295 -val e_Mets = Meth_Def.empty_store;
1.296 -type mets = (met Store.node) list;
1.297 -(*\------- to Celem6 -------/*)
1.298 -
1.299 -(*/------- to Celem91 -------\*)
1.300 -val check_guhs_unique = Check_Unique.check_guhs_unique;
1.301 -val coll_pblguhs = Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh);
1.302 -val check_pblguh_unique = Probl_Def.check_unique;
1.303 -val coll_metguhs = Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh);
1.304 -val check_metguh_unique = Meth_Def.check_unique;
1.305 -(*\------- to Celem91 -------/*)
1.306 -
1.307 -(*/------- to Celem8 -------\*)
1.308 -fun Html_default exist = (Html {guh = theID2guh exist,
1.309 - coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
1.310 -
1.311 -fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], [])
1.312 - | fill_parents (exist, i :: is) thydata =
1.313 - Store.Node (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
1.314 - | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
1.315 -
1.316 -fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
1.317 - | add_thydata (exist, [i]) data (pys as (py as Store.Node (key, _, _)) :: pyss) =
1.318 - if i = key
1.319 - then pys (* preserve existing thydata *)
1.320 - else py :: add_thydata (exist, [i]) data pyss
1.321 - | add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) =
1.322 - if i = key
1.323 - then
1.324 - if length pys = 0
1.325 - then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
1.326 - else Store.Node (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
1.327 - else py :: add_thydata (exist, iss) data pyss
1.328 - | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
1.329 -
1.330 -fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
1.331 - Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1.332 - fillpats = fillpats', thm = thm}
1.333 - | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
1.334 -(*\------- to Celem8 -------/*)
1.335
1.336 (* for dialog-authoring *)
1.337 -fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
1.338 +fun update_hrls (Thy_Html.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
1.339 let
1.340 val rls' =
1.341 case rls of
1.342 @@ -349,20 +94,11 @@
1.343 scr = scr, errpatts = errpatIDs}
1.344 | Erls => Erls
1.345 in
1.346 - Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1.347 + Thy_Html.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1.348 thy_rls = (thyID, rls')}
1.349 end
1.350 | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
1.351
1.352 -fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *)
1.353 - let
1.354 - fun update_elem th (theID, fillpats) =
1.355 - let
1.356 - val hthm = get_py th theID theID
1.357 - val hthm' = update_hthm hthm fillpats
1.358 - handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.359 - in update_ptyps theID theID hthm' end
1.360 - in fold (update_elem th) fis end
1.361
1.362 (* group the theories defined in Isac, compare Build_Thydata:
1.363 section "Get and group the theories defined in Isac" *)
1.364 @@ -389,7 +125,6 @@
1.365 in
1.366 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
1.367 end
1.368 -
1.369 fun progthys () = (*["Isac_Knowledge", .., "Descript"]*)
1.370 let
1.371 fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
1.372 @@ -407,7 +142,6 @@
1.373 in
1.374 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
1.375 end
1.376 -
1.377 fun partID thy =
1.378 if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"
1.379 else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
2.1 --- a/src/Tools/isac/BaseDefinitions/environment.sml Tue Apr 21 15:42:50 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/environment.sml Tue Apr 21 16:16:11 2020 +0200
2.3 @@ -27,7 +27,7 @@
2.4 fun subst2str s =
2.5 (strs2str o
2.6 (map (
2.7 - Celem.linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;
2.8 + linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;
2.9 fun subst2str' s =
2.10 (strs2str' o
2.11 (map (
3.1 --- a/src/Tools/isac/BaseDefinitions/tracing.sml Tue Apr 21 15:42:50 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/tracing.sml Tue Apr 21 16:16:11 2020 +0200
3.3 @@ -8,8 +8,10 @@
3.4 signature TRACING =
3.5 sig
3.6 (*/------- to Trace from Celem -------\*)
3.7 - val trace_calc: bool Unsynchronized.ref
3.8 - val trace_rewrite: bool Unsynchronized.ref
3.9 + val trace_calc: bool Unsynchronized.ref
3.10 + val trace_rewrite: bool Unsynchronized.ref
3.11 + val depth: int Unsynchronized.ref
3.12 + val lim_deriv: int Unsynchronized.ref
3.13 (*\------- to Trace from Celem --------/*)
3.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.15 (*NONE*)
4.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Apr 21 15:42:50 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Apr 21 16:16:11 2020 +0200
4.3 @@ -137,20 +137,20 @@
4.4 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
4.5 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
4.6 if lim < 0
4.7 - then (tracing ("make_deriv exceeds " ^ int2str (! Celem.lim_deriv) ^ "with deriv =\n");
4.8 + then (tracing ("make_deriv exceeds " ^ int2str (! Trace.lim_deriv) ^ "with deriv =\n");
4.9 tracing (deriv2str rts); rts)
4.10 else
4.11 (case r of
4.12 Rule.Thm (thmid, tm) =>
4.13 - (if not (! Celem.trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
4.14 + (if not (! Trace.trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
4.15 case Rewrite.rewrite_ thy ro erls true tm t of
4.16 NONE => rew_once lim rts t apno rs'
4.17 | SOME (t', a') =>
4.18 - (if ! Celem.trace_rewrite then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
4.19 + (if ! Trace.trace_rewrite then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
4.20 rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
4.21 | Rule.Eval (c as (op_, _)) =>
4.22 let
4.23 - val _ = if not (! Celem.trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")
4.24 + val _ = if not (! Trace.trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")
4.25 val t = TermC.uminus_to_string t
4.26 in
4.27 case Eval.adhoc_thm thy c t of
4.28 @@ -160,7 +160,7 @@
4.29 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
4.30 SOME ta => ta
4.31 | NONE => error "adhoc_thm: NONE"
4.32 - val _ = if not (! Celem.trace_rewrite) then () else tracing("=== calc. to: " ^ UnparseC.term t')
4.33 + val _ = if not (! Trace.trace_rewrite) then () else tracing("=== calc. to: " ^ UnparseC.term t')
4.34 val r' = Rule.Thm (thmid, tm)
4.35 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
4.36 handle _ => error "derive_norm, Eval: no rewrite"
4.37 @@ -172,7 +172,7 @@
4.38 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
4.39 | rule => error ("rew_once: uncovered case " ^ Rule.to_string rule))
4.40 | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
4.41 - in rew_once (! Celem.lim_deriv) [] tt Noap rs end
4.42 + in rew_once (! Trace.lim_deriv) [] tt Noap rs end
4.43
4.44 (*version for reverse rewrite used before 040214*)
4.45 fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
5.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Apr 21 15:42:50 2020 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Apr 21 16:16:11 2020 +0200
5.3 @@ -13,7 +13,7 @@
5.4 ML_file method.sml
5.5 ML_file "cas-command.sml"
5.6
5.7 -ML_file rewrite.sml
5.8 + ML_file rewrite.sml
5.9 ML_file "calc-tree-elem.sml"
5.10 ML_file model.sml
5.11 ML_file mstools.sml
6.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Apr 21 15:42:50 2020 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Apr 21 16:16:11 2020 +0200
6.3 @@ -540,7 +540,7 @@
6.4
6.5 (*extract a formula or model from ctree for itms2itemppc or model2xml*)
6.6 fun preconds2str bts =
6.7 - (strs2str o (map (Celem.linefeed o pair2str o
6.8 + (strs2str o (map (linefeed o pair2str o
6.9 (apsnd UnparseC.term) o
6.10 (apfst bool2str)))) bts;
6.11 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
7.1 --- a/src/Tools/isac/MathEngBasic/model.sml Tue Apr 21 15:42:50 2020 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Tue Apr 21 16:16:11 2020 +0200
7.3 @@ -327,14 +327,14 @@
7.4 fun ori2str (i, vs, fi, t, ts) =
7.5 "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^
7.6 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
7.7 -val oris2str = strs2str' o (map (Celem.linefeed o ori2str));
7.8 +val oris2str = strs2str' o (map (linefeed o ori2str));
7.9
7.10 (* an or without leading integer *)
7.11 type preori = (vats * string * term * term list);
7.12 fun preori2str (vs, fi, t, ts) =
7.13 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
7.14 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
7.15 -val preoris2str = (strs2str' o (map (Celem.linefeed o preori2str)));
7.16 +val preoris2str = (strs2str' o (map (linefeed o preori2str)));
7.17
7.18 (* 9.5.03 penv postponed: pbl_ids' *)
7.19 fun pbl_ids' d vs = [comp_ts (d, vs)];
7.20 @@ -404,7 +404,7 @@
7.21 fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
7.22 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
7.23 s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
7.24 -fun itms2str_ ctxt itms = strs2str' (map (Celem.linefeed o (itm2str_ ctxt)) itms);
7.25 +fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
7.26 fun init_item str = SyntaxE str;
7.27
7.28 type 'a ppc =
7.29 @@ -463,7 +463,7 @@
7.30 term (* the precondition (for map) *)
7.31 *)
7.32 fun pre2str (b, t) = pair2str(bool2str b, UnparseC.term t);
7.33 -fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);
7.34 +fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
7.35
7.36 fun vars_of itms = itms |> mk_env |> map snd
7.37
8.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml Tue Apr 21 15:42:50 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/mstools.sml Tue Apr 21 16:16:11 2020 +0200
8.3 @@ -78,7 +78,7 @@
8.4 else (false , pre);
8.5
8.6 fun pre2str (b, t) = pair2str (bool2str b, UnparseC.term t);
8.7 -fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);
8.8 +fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
8.9
8.10 (* check preconditions, return true if all true *)
8.11 fun check_preconds' _ [] _ _ = [] (* empty preconditions are true *)
9.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 21 15:42:50 2020 +0200
9.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 21 16:16:11 2020 +0200
9.3 @@ -40,9 +40,9 @@
9.4 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
9.5
9.6 fun trace i str =
9.7 - if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()
9.8 + if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" i ^ str) else ()
9.9 fun trace1 i str =
9.10 - if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else ()
9.11 + if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" (i + 1) ^ str) else ()
9.12
9.13 fun rewrite__ thy i bdv tless rls put_asm thm ct =
9.14 let
9.15 @@ -58,7 +58,7 @@
9.16 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
9.17 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
9.18 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
9.19 - val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
9.20 + val _ = if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
9.21 then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
9.22 val (t'', p'') = (*conditional rewriting*)
9.23 let
9.24 @@ -66,20 +66,20 @@
9.25 in
9.26 if nofalse
9.27 then
9.28 - (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
9.29 + (if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> []
9.30 then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
9.31 " stored: " ^ UnparseC.terms_in_thy thy simpl_p')
9.32 else();
9.33 (t',simpl_p')) (* uncond.rew. from above*)
9.34 else
9.35 - (if ! Celem.trace_rewrite andalso i < ! Celem.depth
9.36 + (if ! Trace.trace_rewrite andalso i < ! Trace.depth
9.37 then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
9.38 else();
9.39 raise STOP_REW_SUB (* don't go into subterms of cond *))
9.40 end
9.41 in
9.42 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
9.43 - then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
9.44 + then (if ! Trace.trace_rewrite andalso i < ! Trace.depth
9.45 then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
9.46 else ();
9.47 raise NO_REWRITE)
10.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Tue Apr 21 15:42:50 2020 +0200
10.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Tue Apr 21 16:16:11 2020 +0200
10.3 @@ -48,7 +48,7 @@
10.4 fun subst2str s =
10.5 (strs2str o
10.6 (map (
10.7 - Celem.linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;
10.8 + linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;
10.9 type fmz_ = TermC.as_string list;
10.10 (* a formalization of an example contains data
10.11 sufficient for mechanically finding the solution for the example.
11.1 --- a/src/Tools/isac/ProgLang/calculate.sml Tue Apr 21 15:42:50 2020 +0200
11.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Tue Apr 21 16:16:11 2020 +0200
11.3 @@ -94,15 +94,15 @@
11.4 ^^^^^^... the selecting operator op_ (variable for eval_binop)
11.5 *)
11.6 fun trace_calc0 str =
11.7 - if ! Celem.trace_calc then writeln ("### " ^ str) else ()
11.8 + if ! Trace.trace_calc then writeln ("### " ^ str) else ()
11.9 fun trace_calc1 str1 str2 =
11.10 - if ! Celem.trace_calc then writeln (str1 ^ str2) else ()
11.11 + if ! Trace.trace_calc then writeln (str1 ^ str2) else ()
11.12 fun trace_calc2 str term popt =
11.13 - if ! Celem.trace_calc then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
11.14 + if ! Trace.trace_calc then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
11.15 fun trace_calc3 str term =
11.16 - if ! Celem.trace_calc then writeln ("### " ^ str ^ UnparseC.term term) else ()
11.17 + if ! Trace.trace_calc then writeln ("### " ^ str ^ UnparseC.term term) else ()
11.18 fun trace_calc4 str t1 t2 =
11.19 - if ! Celem.trace_calc then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
11.20 + if ! Trace.trace_calc then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
11.21
11.22 fun get_pair thy op_ (ef: Exec_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
11.23 if op_ = op0 then
12.1 --- a/src/Tools/isac/Specify/generate.sml Tue Apr 21 15:42:50 2020 +0200
12.2 +++ b/src/Tools/isac/Specify/generate.sml Tue Apr 21 16:16:11 2020 +0200
12.3 @@ -83,7 +83,7 @@
12.4 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
12.5 "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
12.6 Istate_Def.string_of istate ^ " ))"
12.7 -fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis
12.8 +fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis
12.9
12.10 datatype pblmet = (*%^%*)
12.11 Upblmet (*undefined*)
13.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 15:42:50 2020 +0200
13.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 16:16:11 2020 +0200
13.3 @@ -718,18 +718,18 @@
13.4 error ("kestoreID2guh: \"" ^ Celem.ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");
13.5
13.6 fun show_pblguhs () = (* for tests *)
13.7 - (tracing o strs2str o (map Celem.linefeed))
13.8 + (tracing o strs2str o (map linefeed))
13.9 (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh) (get_ptyps ()))
13.10 fun sort_pblguhs () = (* for tests *)
13.11 - (tracing o strs2str o (map Celem.linefeed))
13.12 + (tracing o strs2str o (map linefeed))
13.13 (((sort string_ord) o (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh)))
13.14 (get_ptyps ()))
13.15
13.16 fun show_metguhs () = (* for tests *)
13.17 - (tracing o strs2str o (map Celem.linefeed))
13.18 + (tracing o strs2str o (map linefeed))
13.19 (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh) (get_mets ()))
13.20 fun sort_metguhs () = (* for tests *)
13.21 - (tracing o strs2str o (map Celem.linefeed))
13.22 + (tracing o strs2str o (map linefeed))
13.23 (((sort string_ord) o (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh)))
13.24 (get_mets ()))
13.25