# HG changeset patch # User Walther Neuper # Date 1587478571 -7200 # Node ID a3d65f3b495f160e454481411ee86430bb6bf658 # Parent 68883c04696302825498dc76d480de7bb6c66b22 remove unused code from Celem diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/BaseDefinitions/calcelems.sml --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 16:16:11 2020 +0200 @@ -10,121 +10,30 @@ signature CALC_ELEMENT = sig -(*/------- to Celem7 -------\* ) - type cas_elem - val cas_eq: cas_elem * cas_elem -> bool -( *\------- to Celem7 -------/*) -(*/------- to Celem5 -------\* ) - type pbt = Probl_Def.T - val e_pbt: pbt; - val e_Ptyp: pbt Store.node - type ptyps = Probl_Def.store - val pbts2str: pbt list -> string -( *\------- to Celem5 -------/*) - -(*/------- to Spec -------\* ) - type metID - type pblID - type spec - val spec2str: string * string list * string list -> string - val metID2str: string list -> string - val e_pblID: pblID - val e_metID: metID - val empty_spec: spec - val e_spec: spec -( *\------- to Spec -------/*) - -(*/------- to Store -------\* ) -(*datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list\*) - val merge_ptyps: 'a Store.T * 'a Store.T -> 'a Store.T - val insrt: Spec.pblID -> 'a -> string list -> 'a Store.T -> 'a Store.T - val get_py: 'a Store.T -> Spec.pblID -> string list -> 'a - val update_ptyps: string list -> string list -> 'a -> 'a Store.T -> 'a Store.T - val app_py: 'a Store.T -> ('a Store.node -> 'b) -> Spec.pblID -> string list -> 'b -( *\------- to Store -------/*) - -(*/------- to Celem2 -------\* ) - type guh -( *\------- to Celem2 -------/*) - -(*/------- to Celem8 -------\* ) - type authors = Thy_Html.authors - datatype thydata = datatype Thy_Html.thydata - type theID = Thy_Html.theID - val theID2str: string list -> string - val the2str: thydata -> string - val thes2str: thydata list -> string - val theID2thyID: theID -> ThyC.id - - val part2guh: theID -> Check_Unique.guh - val thy2guh: theID -> Check_Unique.guh - val thypart2guh: theID -> Check_Unique.guh - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.guh - val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.guh - val cal2guh: string * ThyC.id -> string -> Check_Unique.guh - val ord2guh: string * ThyC.id -> string -> string - val theID2guh: theID -> Check_Unique.guh - - val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T - val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata -( *\------- to Celem8 -------/*) - -(*/------- to Celem6 -------\* ) - type met = Meth_Def.T - type mets = Meth_Def.store - val e_Mets: met Store.node -( *\------- to Celem6 -------/*) - -(*/------- to Celem91 -------\* ) - val check_guhs_unique: bool Unsynchronized.ref - val coll_pblguhs: Probl_Def.T Store.T -> Check_Unique.guh list - val check_pblguh_unique: Check_Unique.guh -> Probl_Def.T Store.T -> unit - val coll_metguhs: Meth_Def.T Store.T -> Check_Unique.guh list - val check_metguh_unique: Check_Unique.guh -> Meth_Def.T Store.T -> unit -( *\------- to Celem91 -------/*) - - val linefeed: string -> string - val trace_calc: bool Unsynchronized.ref - val trace_rewrite: bool Unsynchronized.ref - val depth: int Unsynchronized.ref - datatype ketype = Exp_ | Met_ | Pbl_ | Thy_ - type kestoreID - val ketype2str: ketype -> string - -(*/------- to Celem4 -------\* ) - type pat = Celem4.pat - val pats2str: pat list -> string - val pats2str' : Celem4.pat list -> string -( *\------- to Celem4 -------/*) - - val maxthy: theory -> theory -> theory - eqtype filename - val lim_deriv: int Unsynchronized.ref - val isabthys: unit -> theory list - val partID': ThyC.id -> string - type pbt_ = string * (term * term) - eqtype xml - val ketype2str': ketype -> string - val str2ketype': string -> ketype - eqtype filepath - val update_hrls: Thy_Html.thydata -> Error_Fill_Def.errpatID list -> Thy_Html.thydata eqtype iterID eqtype calcID -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) - val insert_fillpats: Thy_Html.thydata Store.T -> (Spec.pblID * Error_Fill_Def.fillpat list) list -> Thy_Html.thydata Store.T -> - Thy_Html.thydata Store.T -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - val knowthys: unit -> theory list -(*/------- to Celem6 -------\*) - val e_met: Meth_Def.T -(*\------- to Celem6 -------/*) -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) + eqtype xml -(*----- unused code, kept as hints to design ideas ---------------------------------------------*) - val overwritelthy: theory -> (Rule_Set.id * (string * Rule_Set.T)) list * (Rule_Set.id * Rule_Set.T) list -> - (Rule_Set.id * (string * Rule_Set.T)) list + type kestoreID + + datatype ketype = Exp_ | Met_ | Pbl_ | Thy_ + val ketype2str: ketype -> string + val ketype2str': ketype -> string + val str2ketype': string -> ketype + + eqtype filename + eqtype filepath + + val maxthy: theory -> theory -> theory + + type pbt_ = string * (term * term) + val update_hrls: Thy_Html.thydata -> Error_Fill_Def.errpatID list -> Thy_Html.thydata + + val isabthys: unit -> theory list + val partID': ThyC.id -> string + end (**) @@ -132,62 +41,11 @@ struct (**) -val linefeed = curry op ^ "\n"; (* ?\ libraryC ?*) - type iterID = int; type calcID = int; -(*/------- to Celem2 -------\*) -type guh = Check_Unique.guh; -(*\------- to Celem2 -------/*) type xml = string; (* rm together with old code replaced by XML.tree *) - -(* WN0509 discussion: -############################################################################# -# How to manage theorys in subproblems wrt. the requirement, # -# that scripts should be re-usable ? # -############################################################################# - - eg. 'Program Solve_rat_equation' calls 'SubProblem (RatEq',..' - which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script - because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b - is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard - (see match_ags). - - Preliminary solution: - # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically, - # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl - # however, a thy specified by the user in the rootpbl may lead to - errors in far-off subpbls (which are not yet reported properly !!!) - and interactively specifiying thys in subpbl is not very relevant. - - Other solutions possible: - # always parse and type-check with Thy_Info_get_theory "Isac_Knowledge" - (rejected due to the vague idea eg. to re-use equations for R in C etc.) - # regard the subthy-relation in specifying thys of subpbls - # specifically handle 'SubProblem (undefined, pbl, arglist)' - # ??? -*) - -(*/------- to Spec -------\*) -(*the key into the hierarchy ob problems*) -type pblID = Spec.pblID; -val e_pblID = Spec.e_pblID; -type metID = Spec.metID; -type spec = Spec.spec; -val spec2str = Spec.spec2str; -val e_metID = Spec.e_metID; -val metID2str = Spec.metID2str; -val empty_spec = Spec.empty_spec; -val e_spec = Spec.e_spec; -(*\------- to Spec -------/*) - -(*/------- to Celem7 -------\*) -type cas_elem = CAS_Def.T; -val cas_eq = CAS_Def.equal; -(*\------- to Celem7 -------/*) - (*either theID or pblID or metID*) type kestoreID = string list; @@ -208,133 +66,20 @@ | str2ketype' "met" = Met_ | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str) -(*/------- to Store -------\*) -val merge_ptyps = Store.merge; -val insrt = Store.insert; -val app_py = Store.apply; -val get_py = Store.get; -val update_ptyps = Store.update; -(*\------- to Store -------/*) - -(*/------- to Celem8 -------\*) -type authors = Thy_Html.authors; -datatype thydata = datatype Thy_Html.thydata; -type theID = Thy_Html.theID; -val theID2str = Thy_Html.theID2str; -val the2str = Thy_Html.the2str; -val thes2str = Thy_Html.thes2str; -val theID2thyID = Thy_Html.theID2thyID; - -val part2guh = Thy_Html.part2guh; -val thy2guh = Thy_Html.thy2guh; -val thypart2guh = Thy_Html.thypart2guh; -val thm2guh = Thy_Html.thm2guh; -val rls2guh = Thy_Html.rls2guh; -val cal2guh = Thy_Html.cal2guh; -val ord2guh = Thy_Html.ord2guh; -val theID2guh = Thy_Html.theID2guh; - -val add_thydata = Thy_Html.add_thydata; -val update_hthm = Thy_Html.update_hthm; -(*\------- to Celem8 -------/*) - type filepath = string; type filename = string; -(* overwrite an element in an association list and pair it with a thyID - in order to create the thy_hierarchy; - overwrites existing rls' even if they are defined in a different thy; - this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc *) -(* WN060120 ...these are NOT compatible to "fun assoc_thm'" in that - they do NOT handle overlays by re-using an identifier in different thys; - "thyID.rlsID" would be a good solution, if the "." would be possible - in scripts... - actually a hack to get alltogether run again with minimal effort *) -fun insthy thy' (rls', rls) = (rls', (thy', rls)); -fun overwritelthy thy (al, bl: (Rule_Set.id * Rule_Set.T) list) = - let val bl' = map (insthy ((get_thy o Context.theory_name) thy)) bl - in overwritel (al, bl') end; - fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; -(*/------- to Trace from Celem -------\*) -(* trace internal steps of isac's numeral calculations *) -val trace_calc = Unsynchronized.ref false; -(* trace internal steps of isac's rewriter *) -val trace_rewrite = Unsynchronized.ref false; -(* depth of recursion in traces of the rewriter, if trace_rewrite:=true *) -val depth = Unsynchronized.ref 99999; -(* no of rewrites exceeding this int -> NO rewrite *) -val lim_deriv = Unsynchronized.ref 100; -(*\------- to Trace from Celem --------/*) - -(*/------- to Celem4 -------\*) -(* the pattern for an item of a problems model or a methods guard *) -type pat = Celem4.pat; -val pats2str = Celem4.pats2str; -val pats2str' = Celem4.pats2str'; -(*\------- to Celem4 -------/*) - (* types for problems models (TODO rename to specification models) *) type pbt_ = (string * (* field "#Given",..*)(*deprecated due to 'type pat'*) (term * (* description *) term)); (* id | struct-var *) -(*/------- to Celem5 -------\*) -type pbt = Probl_Def.T; -val e_pbt = Probl_Def.empty; -val e_Ptyp = Probl_Def.empty_store; -val pbts2str = Probl_Def.s_to_string; -type ptyps = Probl_Def.store; -(*\------- to Celem5 -------/*) - -(*/------- to Celem6 -------\*) -type met = Meth_Def.T; -val e_met = Meth_Def.empty; -val e_Mets = Meth_Def.empty_store; -type mets = (met Store.node) list; -(*\------- to Celem6 -------/*) - -(*/------- to Celem91 -------\*) -val check_guhs_unique = Check_Unique.check_guhs_unique; -val coll_pblguhs = Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh); -val check_pblguh_unique = Probl_Def.check_unique; -val coll_metguhs = Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh); -val check_metguh_unique = Meth_Def.check_unique; -(*\------- to Celem91 -------/*) - -(*/------- to Celem8 -------\*) -fun Html_default exist = (Html {guh = theID2guh exist, - coursedesign = ["isac team 2006"], mathauthors = [], html = ""}) - -fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], []) - | fill_parents (exist, i :: is) thydata = - Store.Node (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata]) - | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive" - -fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata] - | add_thydata (exist, [i]) data (pys as (py as Store.Node (key, _, _)) :: pyss) = - if i = key - then pys (* preserve existing thydata *) - else py :: add_thydata (exist, [i]) data pyss - | add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) = - if i = key - then - if length pys = 0 - then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss - else Store.Node (key, d, add_thydata (exist @ [i], is) data pys) :: pyss - else py :: add_thydata (exist, iss) data pyss - | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive" - -fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' = - Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors, - fillpats = fillpats', thm = thm} - | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments"; -(*\------- to Celem8 -------/*) (* for dialog-authoring *) -fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs = +fun update_hrls (Thy_Html.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs = let val rls' = case rls of @@ -349,20 +94,11 @@ scr = scr, errpatts = errpatIDs} | Erls => Erls in - Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors, + Thy_Html.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors, thy_rls = (thyID, rls')} end | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments"; -fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *) - let - fun update_elem th (theID, fillpats) = - let - val hthm = get_py th theID theID - val hthm' = update_hthm hthm fillpats - handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") - in update_ptyps theID theID hthm' end - in fold (update_elem th) fis end (* group the theories defined in Isac, compare Build_Thydata: section "Get and group the theories defined in Isac" *) @@ -389,7 +125,6 @@ in take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys') end - fun progthys () = (*["Isac_Knowledge", .., "Descript"]*) let fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *) @@ -407,7 +142,6 @@ in drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys') end - fun partID thy = if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge" else if member Context.eq_thy (progthys ()) thy then "IsacScripts" diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/BaseDefinitions/environment.sml --- a/src/Tools/isac/BaseDefinitions/environment.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/BaseDefinitions/environment.sml Tue Apr 21 16:16:11 2020 +0200 @@ -27,7 +27,7 @@ fun subst2str s = (strs2str o (map ( - Celem.linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s; + linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s; fun subst2str' s = (strs2str' o (map ( diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/BaseDefinitions/tracing.sml --- a/src/Tools/isac/BaseDefinitions/tracing.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/BaseDefinitions/tracing.sml Tue Apr 21 16:16:11 2020 +0200 @@ -8,8 +8,10 @@ signature TRACING = sig (*/------- to Trace from Celem -------\*) - val trace_calc: bool Unsynchronized.ref - val trace_rewrite: bool Unsynchronized.ref + val trace_calc: bool Unsynchronized.ref + val trace_rewrite: bool Unsynchronized.ref + val depth: int Unsynchronized.ref + val lim_deriv: int Unsynchronized.ref (*\------- to Trace from Celem --------/*) (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) (*NONE*) diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/Interpret/rewtools.sml --- a/src/Tools/isac/Interpret/rewtools.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Apr 21 16:16:11 2020 +0200 @@ -137,20 +137,20 @@ | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs') and rew_or_calc lim rts t apno (rrs' as (r :: rs')) = if lim < 0 - then (tracing ("make_deriv exceeds " ^ int2str (! Celem.lim_deriv) ^ "with deriv =\n"); + then (tracing ("make_deriv exceeds " ^ int2str (! Trace.lim_deriv) ^ "with deriv =\n"); tracing (deriv2str rts); rts) else (case r of Rule.Thm (thmid, tm) => - (if not (! Celem.trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\""); + (if not (! Trace.trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\""); case Rewrite.rewrite_ thy ro erls true tm t of NONE => rew_once lim rts t apno rs' | SOME (t', a') => - (if ! Celem.trace_rewrite then tracing ("=== rewrites to: " ^ UnparseC.term t') else (); + (if ! Trace.trace_rewrite then tracing ("=== rewrites to: " ^ UnparseC.term t') else (); rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')) | Rule.Eval (c as (op_, _)) => let - val _ = if not (! Celem.trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"") + val _ = if not (! Trace.trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"") val t = TermC.uminus_to_string t in case Eval.adhoc_thm thy c t of @@ -160,7 +160,7 @@ val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of SOME ta => ta | NONE => error "adhoc_thm: NONE" - val _ = if not (! Celem.trace_rewrite) then () else tracing("=== calc. to: " ^ UnparseC.term t') + val _ = if not (! Trace.trace_rewrite) then () else tracing("=== calc. to: " ^ UnparseC.term t') val r' = Rule.Thm (thmid, tm) in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end) handle _ => error "derive_norm, Eval: no rewrite" @@ -172,7 +172,7 @@ | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs') | rule => error ("rew_once: uncovered case " ^ Rule.to_string rule)) | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []" - in rew_once (! Celem.lim_deriv) [] tt Noap rs end + in rew_once (! Trace.lim_deriv) [] tt Noap rs end (*version for reverse rewrite used before 040214*) fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a)); diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/MathEngBasic/MathEngBasic.thy --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Apr 21 16:16:11 2020 +0200 @@ -13,7 +13,7 @@ ML_file method.sml ML_file "cas-command.sml" -ML_file rewrite.sml + ML_file rewrite.sml ML_file "calc-tree-elem.sml" ML_file model.sml ML_file mstools.sml diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/MathEngBasic/ctree-basic.sml --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Apr 21 16:16:11 2020 +0200 @@ -540,7 +540,7 @@ (*extract a formula or model from ctree for itms2itemppc or model2xml*) fun preconds2str bts = - (strs2str o (map (Celem.linefeed o pair2str o + (strs2str o (map (linefeed o pair2str o (apsnd UnparseC.term) o (apfst bool2str)))) bts; fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *) diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/MathEngBasic/model.sml --- a/src/Tools/isac/MathEngBasic/model.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/model.sml Tue Apr 21 16:16:11 2020 +0200 @@ -327,14 +327,14 @@ fun ori2str (i, vs, fi, t, ts) = "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^ UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; -val oris2str = strs2str' o (map (Celem.linefeed o ori2str)); +val oris2str = strs2str' o (map (linefeed o ori2str)); (* an or without leading integer *) type preori = (vats * string * term * term list); fun preori2str (vs, fi, t, ts) = "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^ UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; -val preoris2str = (strs2str' o (map (Celem.linefeed o preori2str))); +val preoris2str = (strs2str' o (map (linefeed o preori2str))); (* 9.5.03 penv postponed: pbl_ids' *) fun pbl_ids' d vs = [comp_ts (d, vs)]; @@ -404,7 +404,7 @@ fun itm2str_ ctxt ((i, is, b, s, itm_):itm) = "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^ s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")"; -fun itms2str_ ctxt itms = strs2str' (map (Celem.linefeed o (itm2str_ ctxt)) itms); +fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms); fun init_item str = SyntaxE str; type 'a ppc = @@ -463,7 +463,7 @@ term (* the precondition (for map) *) *) fun pre2str (b, t) = pair2str(bool2str b, UnparseC.term t); -fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres); +fun pres2str pres = strs2str' (map (linefeed o pre2str) pres); fun vars_of itms = itms |> mk_env |> map snd diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/MathEngBasic/mstools.sml --- a/src/Tools/isac/MathEngBasic/mstools.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/mstools.sml Tue Apr 21 16:16:11 2020 +0200 @@ -78,7 +78,7 @@ else (false , pre); fun pre2str (b, t) = pair2str (bool2str b, UnparseC.term t); -fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres); +fun pres2str pres = strs2str' (map (linefeed o pre2str) pres); (* check preconditions, return true if all true *) fun check_preconds' _ [] _ _ = [] (* empty preconditions are true *) diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/MathEngBasic/rewrite.sml --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 21 16:16:11 2020 +0200 @@ -40,9 +40,9 @@ exception STOP_REW_SUB; (*WN050820 quick and dirty*) fun trace i str = - if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else () + if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" i ^ str) else () fun trace1 i str = - if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else () + if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" (i + 1) ^ str) else () fun rewrite__ thy i bdv tless rls put_asm thm ct = let @@ -58,7 +58,7 @@ val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r')) val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r' - val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> [] + val _ = if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> [] then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else () val (t'', p'') = (*conditional rewriting*) let @@ -66,20 +66,20 @@ in if nofalse then - (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> [] + (if ! Trace.trace_rewrite andalso i < ! Trace.depth andalso p' <> [] then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^ " stored: " ^ UnparseC.terms_in_thy thy simpl_p') else(); (t',simpl_p')) (* uncond.rew. from above*) else - (if ! Celem.trace_rewrite andalso i < ! Celem.depth + (if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p') else(); raise STOP_REW_SUB (* don't go into subterms of cond *)) end in if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*) - then (if ! Celem.trace_rewrite andalso i < ! Celem.depth + then (if ! Trace.trace_rewrite andalso i < ! Trace.depth then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"") else (); raise NO_REWRITE) diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/MathEngBasic/specification-elems.sml --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Tue Apr 21 16:16:11 2020 +0200 @@ -48,7 +48,7 @@ fun subst2str s = (strs2str o (map ( - Celem.linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s; + linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s; type fmz_ = TermC.as_string list; (* a formalization of an example contains data sufficient for mechanically finding the solution for the example. diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/ProgLang/calculate.sml --- a/src/Tools/isac/ProgLang/calculate.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/ProgLang/calculate.sml Tue Apr 21 16:16:11 2020 +0200 @@ -94,15 +94,15 @@ ^^^^^^... the selecting operator op_ (variable for eval_binop) *) fun trace_calc0 str = - if ! Celem.trace_calc then writeln ("### " ^ str) else () + if ! Trace.trace_calc then writeln ("### " ^ str) else () fun trace_calc1 str1 str2 = - if ! Celem.trace_calc then writeln (str1 ^ str2) else () + if ! Trace.trace_calc then writeln (str1 ^ str2) else () fun trace_calc2 str term popt = - if ! Celem.trace_calc then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else () + if ! Trace.trace_calc then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else () fun trace_calc3 str term = - if ! Celem.trace_calc then writeln ("### " ^ str ^ UnparseC.term term) else () + if ! Trace.trace_calc then writeln ("### " ^ str ^ UnparseC.term term) else () fun trace_calc4 str t1 t2 = - if ! Celem.trace_calc then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else () + if ! Trace.trace_calc then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else () fun get_pair thy op_ (ef: Exec_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *) if op_ = op0 then diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/Specify/generate.sml --- a/src/Tools/isac/Specify/generate.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/Specify/generate.sml Tue Apr 21 16:16:11 2020 +0200 @@ -83,7 +83,7 @@ fun taci2str ((tac, tac_, (pos', (istate, _))):taci) = "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^ Istate_Def.string_of istate ^ " ))" -fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis +fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis datatype pblmet = (*%^%*) Upblmet (*undefined*) diff -r 68883c046963 -r a3d65f3b495f src/Tools/isac/Specify/ptyps.sml --- a/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 15:42:50 2020 +0200 +++ b/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 16:16:11 2020 +0200 @@ -718,18 +718,18 @@ error ("kestoreID2guh: \"" ^ Celem.ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\""); fun show_pblguhs () = (* for tests *) - (tracing o strs2str o (map Celem.linefeed)) + (tracing o strs2str o (map linefeed)) (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh) (get_ptyps ())) fun sort_pblguhs () = (* for tests *) - (tracing o strs2str o (map Celem.linefeed)) + (tracing o strs2str o (map linefeed)) (((sort string_ord) o (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh))) (get_ptyps ())) fun show_metguhs () = (* for tests *) - (tracing o strs2str o (map Celem.linefeed)) + (tracing o strs2str o (map linefeed)) (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh) (get_mets ())) fun sort_metguhs () = (* for tests *) - (tracing o strs2str o (map Celem.linefeed)) + (tracing o strs2str o (map linefeed)) (((sort string_ord) o (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh))) (get_mets ()))