1.1 --- a/src/Tools/isac/CalcElements/rule.sml Wed Apr 08 15:50:03 2020 +0200
1.2 +++ b/src/Tools/isac/CalcElements/rule.sml Wed Apr 08 16:56:47 2020 +0200
1.3 @@ -2,11 +2,6 @@
1.4 Author: Walther Neuper 2018
1.5 (c) copyright due to lincense terms
1.6
1.7 -TODO: this theory should vanish; vaious stuff awaits separation.
1.8 -* rew_ord: this also needs to
1.9 -* ThmC
1.10 -* TheoryC
1.11 -* ...
1.12 Some stuff waits for later rounds of restructuring, e.g. Rule.e_term
1.13 *)
1.14
1.15 @@ -18,16 +13,7 @@
1.16 eqtype cterm'
1.17 type subst = (term * term) list
1.18
1.19 -(*/------- to rewrite-ord.sml ---------------------\*)
1.20 - val dummy_ord: Rule_Def.rew_ord_
1.21 - val e_rew_ord_: Rule_Def.rew_ord_
1.22 - val e_rew_ord: Rule_Def.rew_ord_
1.23 - val e_rew_ordX: Rule_Def.rew_ord
1.24 - val rew_ord': (Rule_Def.rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
1.25 - val assoc_rew_ord: string -> subst -> term * term -> bool
1.26 -(*\------- to rewrite-ord.sml ---------------------/*)
1.27 -
1.28 - eqtype errpatID (*..from Rule_Def*)
1.29 + eqtype errpatID
1.30 type errpat = errpatID * term list * thm list
1.31
1.32 val scr2str: program -> string
1.33 @@ -40,12 +26,12 @@
1.34 val termopt2str: term option -> string (* shift up to Unparse *)
1.35 val terms2str: term list -> string (* shift up to Unparse *)
1.36 val terms2strs: term list -> string list
1.37 - val term_to_string'': ThyC.thyID -> term -> string (* shift up to Unparse *)
1.38 + val term_to_string'': ThyC.thyID -> term -> string (* shift up to Unparse *)
1.39 val term_to_string''': theory -> term -> string (* shift up to Unparse *)
1.40 val t2str: theory -> term -> string
1.41 val ts2str: theory -> term list -> string (* shift up to Unparse *)
1.42 val string_of_typ: typ -> string (* shift up to Unparse *)
1.43 - val string_of_typ_thy: ThyC.thyID -> typ -> string (* shift up to Unparse *)
1.44 + val string_of_typ_thy: ThyC.thyID -> typ -> string (* shift up to Unparse *)
1.45
1.46 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.47 val terms2str': term list -> string (* shift up to Unparse *)
1.48 @@ -80,29 +66,6 @@
1.49 type cterm' = string;
1.50 type subst = (term * term) list;
1.51
1.52 -val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
1.53 -type rew_ord_ = Rule_Def.rew_ord_;
1.54 -fun dummy_ord (_: subst) (_: term, _: term) = true;
1.55 -val e_rew_ord_ = dummy_ord;
1.56 -type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord (*..from Rule_Def*)
1.57 -val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
1.58 -val e_rew_ordX = (e_rew_ord', e_rew_ord_);
1.59 -
1.60 -(* rewrite orders, also stored in 'type met' and type 'and rls'
1.61 - The association list is required for 'rewrite.."rew_ord"..' *)
1.62 -val rew_ord' = Unsynchronized.ref
1.63 - ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
1.64 - : (Rule_Def.rew_ord' * (* the key for the association list *)
1.65 - (subst (* the bound variables - they get high order*)
1.66 - -> (term * term) (* (t1, t2) to be compared *)
1.67 - -> bool)) (* if t1 <= t2 then true else false *)
1.68 - list); (* association list *)
1.69 -fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
1.70 - | assoc' ((keyi, xi) :: pairs, key) =
1.71 - if key = keyi then SOME xi else assoc' (pairs, key);
1.72 -fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
1.73 - handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
1.74 -
1.75 fun term_to_string' ctxt t =
1.76 let
1.77 val ctxt' = Config.put show_markup false ctxt