1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Thu Apr 23 09:29:56 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Thu Apr 23 12:34:54 2020 +0200
1.3 @@ -17,6 +17,8 @@
1.4 val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
1.5 val merge: string -> T -> T -> T
1.6 val get_rules: T -> Rule_Def.rule list
1.7 +(*val rule2rls' : Rule.rule -> string*)
1.8 + val id_from_rule : Rule.rule -> string
1.9
1.10 type for_kestore
1.11 val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
1.12 @@ -151,11 +153,14 @@
1.13 | get_rules (Rule_Def.Sequence {rules, ...}) = rules
1.14 | get_rules (Rule_Def.Rrls _) = [];
1.15
1.16 +fun id_from_rule (Rule.Rls_ rls) = id rls
1.17 + | id_from_rule r = raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string r);
1.18 +
1.19 (*/------- this will disappear eventually -----------\*)
1.20 type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
1.21 (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
1.22 val e_rrlsstate = (UnparseC.term_empty, UnparseC.term_empty, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.term_empty, []))]) : rrlsstate;
1.23 -local
1.24 +local
1.25 fun ii (_: term) = e_rrlsstate;
1.26 fun no (_: term) = SOME (UnparseC.term_empty, [UnparseC.term_empty]);
1.27 fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
2.1 --- a/src/Tools/isac/BaseDefinitions/thy-html.sml Thu Apr 23 09:29:56 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/thy-html.sml Thu Apr 23 12:34:54 2020 +0200
2.3 @@ -9,7 +9,7 @@
2.4 type authors
2.5 datatype thydata
2.6 = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
2.7 - | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
2.8 + | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}
2.9 | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
2.10 | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
2.11 | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
3.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 23 09:29:56 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 23 12:34:54 2020 +0200
3.3 @@ -19,7 +19,7 @@
3.4 Thy_Html.thydata * Thy_Html.theID
3.5
3.6 val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Thy_Html.theID * Thy_Html.thydata
3.7 - val makeHord: string * ThyC.id -> string * ((term * term) list -> term * term -> bool) ->
3.8 + val makeHord: string * ThyC.id -> string * Rule_Def.rew_ord_ ->
3.9 Thy_Html.theID * Thy_Html.thydata
3.10 val makeHrls: string -> Rule_Set.id * (ThyC.id * Rule_Def.rule_set) ->
3.11 Thy_Html.theID * Thy_Html.thydata
3.12 @@ -27,7 +27,7 @@
3.13 val make_cal: theory -> Rule_Def.calc -> Thy_Html.authors -> Thy_Html.thydata * Thy_Html.theID
3.14 val make_isa: theory -> ThyC.id * ThyC.id -> Thy_Html.authors ->
3.15 Thy_Html.thydata * Thy_Html.theID
3.16 - val make_ord: theory -> ((term * term) list -> term * term -> bool) -> Thy_Html.authors ->
3.17 + val make_ord: theory -> Rule_Def.rew_ord_ -> Thy_Html.authors ->
3.18 Thy_Html.thydata * Thy_Html.theID
3.19 val make_rls: theory -> Rule_Def.rule_set -> Thy_Html.authors -> Thy_Html.thydata * Thy_Html.theID
3.20 val make_thm: theory -> string -> string * thm -> Thy_Html.authors -> Thy_Html.thydata * Thy_Html.theID
4.1 --- a/src/Tools/isac/Interpret/derive.sml Thu Apr 23 09:29:56 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/derive.sml Thu Apr 23 12:34:54 2020 +0200
4.3 @@ -2,18 +2,25 @@
4.4 Author: Walther Neuper 2019
4.5 (c) due to copyright terms
4.6
4.7 -
4.8 +Derive makes (term * rule * result) steps (= derivation) for term transformations,
4.9 +which cannot be done by rewriting, e.g cancellation of polynomials.
4.10 *)
4.11
4.12 -signature DERIVATION =
4.13 +signature DERIVE =
4.14 sig
4.15 - type deriv
4.16 - val make_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
4.17 - term option -> term -> deriv
4.18 - val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
4.19 - Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
4.20 - val reverse_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
4.21 - term option -> term -> (Rule.rule * (term * term list)) list
4.22 + (*TODO cleanup signature*)
4.23 + type der
4.24 + type deri
4.25 + type derivation
4.26 +(*val make_deriv *)
4.27 + val do_one : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
4.28 + term option -> term -> derivation
4.29 +(*val reverse_deriv *)
4.30 + val steps_reverse : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
4.31 + term option -> term -> deri list
4.32 +(*val concat_deriv *)
4.33 + val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
4.34 + bool * der list
4.35 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.36 (* NONE *)
4.37 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.38 @@ -24,70 +31,45 @@
4.39 end
4.40
4.41 (**)
4.42 -structure Derive(**): DERIVATION(**) =
4.43 +structure Derive(**): DERIVE(**) =
4.44 struct
4.45 (**)
4.46 -(*/------- to Derive from Rtools -------\*)
4.47 -(*** reverse rewriting ***)
4.48 -(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
4.49 - * of for connecting a user-input formula with the current calc-state. *
4.50 - *# It is somewhat incompatible with the rest of the math-engine: *
4.51 - * (1) it is not created by a script *
4.52 - * (2) thus there cannot be another user-input within a derivation *
4.53 - *# It suffers particularily from the not-well-foundedness of the math-engine*
4.54 - * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
4.55 - * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
4.56 - * (3) FIXME and eventually 'lev_back' *
4.57 - *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
4.58 - * (1) FIXME nest Rls_ in 'make_deriv' *
4.59 - * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
4.60 - * user-input will become possible in this part of a derivation *
4.61 - * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
4.62 - * while a non-derivable inform requires to step until End_Proof' *
4.63 - * (4) FIXME find criteria on when _not_ to step until End_Proof' *
4.64 - * (5) FIXME
4.65 -.*)
4.66 -type deriv = (* derivation for inserting one level of nodes into the Ctree *)
4.67 +
4.68 +(** the triple for a step **)
4.69 +
4.70 +type der = (* derivation for inserting one level of nodes into the Ctree *)
4.71 ( term * (* where the rule is applied to *)
4.72 Rule.rule * (* rule to be applied *)
4.73 ( term * (* resulting from rule application *)
4.74 - term list)) (* assumptions resulting from rule application *)
4.75 - list
4.76 + term list));(* assumptions resulting from rule application *)
4.77 +type deri = Rule.rule * (term * term list)
4.78 +type derivation = der list
4.79
4.80 fun trta2str (t, r, (t', a)) =
4.81 "\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))"
4.82 fun trtas2str trtas = (strs2str o (map trta2str)) trtas
4.83 val deriv2str = trtas2str
4.84 -(*\------- to Derive from Rtools -------/*)
4.85 -(*/------- to Derive from Rtools -------\*)
4.86 -(* derive normalform of a rls, or derive until SOME goal,
4.87 - and record rules applied and rewrites.
4.88 -val it = fn
4.89 - : theory
4.90 - -> rls
4.91 - -> rule list
4.92 - -> rew_ord : the order of this rls, which 1 theorem of is used
4.93 - for rewriting 1 single step (?14.4.03)
4.94 - -> term option : 040214 ??? use for "derive until SOME goal" ???
4.95 - -> term
4.96 - -> (term * : to this term ...
4.97 - rule * : ... this rule is applied yielding ...
4.98 - (term * : ... this term ...
4.99 - term list)) : ... under these assumptions.
4.100 - list :
4.101 -returns empty list for a normal form
4.102 -FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
4.103
4.104 -WN060825 too complicated for the intended use by cancel_, common_nominator_
4.105 -and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..
4.106 - -- replaced below *)
4.107 +(** make one triple towards the goal term **)
4.108
4.109 +fun msg_1 rts =
4.110 + (tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n");
4.111 + tracing (deriv2str rts));
4.112 +fun msg_2 thmid =
4.113 + if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
4.114 +fun msg_3 t' =
4.115 + if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
4.116 +fun msg_4 op_ =
4.117 + if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"");
4.118 +fun msg_5 t' =
4.119 + if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
4.120
4.121 -fun make_deriv thy erls rs ro goal tt =
4.122 +fun do_one thy erls rs ro goal tt =
4.123 let
4.124 - datatype switch = Appl | Noap (* unify with version in rewrite.sml *)
4.125 + datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
4.126 fun rew_once _ rts t Noap [] =
4.127 - (case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ UnparseC.term t))
4.128 + (case goal of NONE => rts | SOME _ =>
4.129 + raise ERROR ("do_one: no derivation for " ^ UnparseC.term t))
4.130 | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
4.131 (*| Seq _ => rts) FIXXXXXME 14.3.03*)
4.132 | rew_once lim rts t apno rs' =
4.133 @@ -96,60 +78,56 @@
4.134 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
4.135 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
4.136 if lim < 0
4.137 - then (tracing ("make_deriv exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with deriv =\n");
4.138 - tracing (deriv2str rts); rts)
4.139 + then (msg_1 rts; rts)
4.140 else
4.141 (case r of
4.142 Rule.Thm (thmid, tm) =>
4.143 - (if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
4.144 + (msg_2 thmid;
4.145 case Rewrite.rewrite_ thy ro erls true tm t of
4.146 NONE => rew_once lim rts t apno rs'
4.147 | SOME (t', a') =>
4.148 - (if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
4.149 - rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
4.150 + (msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
4.151 | Rule.Eval (c as (op_, _)) =>
4.152 - let
4.153 - val _ = if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"")
4.154 - val t = TermC.uminus_to_string t
4.155 - in
4.156 - case Eval.adhoc_thm thy c t of
4.157 + (msg_4 op_;
4.158 + case Eval.adhoc_thm thy c (TermC.uminus_to_string t) of
4.159 NONE => rew_once lim rts t apno rs'
4.160 | SOME (thmid, tm) =>
4.161 (let
4.162 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
4.163 SOME ta => ta
4.164 - | NONE => error "adhoc_thm: NONE"
4.165 - val _ = if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
4.166 + | NONE => raise ERROR "adhoc_thm: NONE"
4.167 + val _ = msg_5 t'
4.168 val r' = Rule.Thm (thmid, tm)
4.169 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
4.170 - handle _ => raise ERROR "derive_norm, Eval: no rewrite"
4.171 - end
4.172 - | Rule.Rls_ rls => (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)
4.173 + handle _ => raise ERROR "derive_norm, Eval: no rewrite")
4.174 + | Rule.Rls_ rls =>
4.175 (case Rewrite.rewrite_set_ thy true rls t of
4.176 NONE => rew_once lim rts t apno rs'
4.177 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
4.178 - | rule => error ("rew_once: uncovered case " ^ Rule.to_string rule))
4.179 - | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
4.180 + | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))
4.181 + | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
4.182 in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
4.183
4.184 -(*version for reverse rewrite used before 040214*)
4.185 +
4.186 +(** concatenate several steps in revers order **)
4.187 +
4.188 fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
4.189 -fun reverse_deriv thy erls rs ro goal t =
4.190 - (rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)
4.191 -(*\------- to Derive from Rtools -------/*)
4.192 +fun steps_reverse thy erls rs ro goal t =
4.193 + (rev o (map rev_deriv)) (do_one thy erls rs ro goal t)
4.194
4.195 -(*/------- to NEW Derive from Error_Fill_Pattern -------\*)
4.196 -(* 040214: version for concat_deriv *)
4.197 +
4.198 +(** concatenate several steps **)
4.199 +
4.200 fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
4.201
4.202 (* fo = ifo excluded already in inform *)
4.203 -fun concat_deriv rew_ord erls rules fo ifo =
4.204 +fun steps rew_ord erls rules fo ifo =
4.205 let
4.206 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
4.207 | derivat dt = (#1 o #3 o last_elem) dt
4.208 - fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
4.209 - val fod = make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
4.210 - val ifod = make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
4.211 + fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
4.212 + val fod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
4.213 + val ifod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
4.214 in
4.215 case (fod, ifod) of
4.216 ([], []) => if fo = ifo then (true, []) else (false, [])
4.217 @@ -162,6 +140,5 @@
4.218 in (true, fod' @ (map rev_deriv' rifod')) end
4.219 else (false, [])
4.220 end
4.221 -(*\------- to NEW Derive from Error_Fill_Pattern-------/*)
4.222
4.223 (**)end(**)
5.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 09:29:56 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 12:34:54 2020 +0200
5.3 @@ -18,11 +18,6 @@
5.4 val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
5.5 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
5.6
5.7 -(*/------- to ThmC -------\*)
5.8 - val rule2thm'' : Rule.rule -> ThmC.T
5.9 - val rule2rls' : Rule.rule -> string
5.10 -(*\------- to ThmC -------/*)
5.11 -
5.12 (*/------- to LItool -------\*)
5.13 val mk_tacis: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
5.14 Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
5.15 @@ -49,17 +44,12 @@
5.16
5.17 type errpatID = Rule_Def.errpatID
5.18
5.19 -fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
5.20 - | rule2thm'' r = raise ERROR ("rule2thm': not defined for " ^ Rule.to_string r);
5.21 -fun rule2rls' (Rule.Rls_ rls) = Rule_Set.id rls
5.22 - | rule2rls' r = raise ERROR ("rule2rls': not defined for " ^ Rule.to_string r);
5.23 -
5.24 fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
5.25 (Tactic.Rewrite (id, thm),
5.26 - Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, rule2thm'' r, t, (t', a)),
5.27 + Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)),
5.28 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
5.29 | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
5.30 - (Tactic.Rewrite_Set (rule2rls' r),
5.31 + (Tactic.Rewrite_Set (Rule_Set.id_from_rule r),
5.32 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
5.33 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
5.34 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
6.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Apr 23 09:29:56 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Apr 23 12:34:54 2020 +0200
6.3 @@ -622,7 +622,7 @@
6.4 val fo = Calc.get_current_formula ptp
6.5 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
6.6 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
6.7 - val (found, der) = Derive.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
6.8 + val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
6.9 in
6.10 if found
6.11 then
7.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Apr 23 09:29:56 2020 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Apr 23 12:34:54 2020 +0200
7.3 @@ -476,7 +476,7 @@
7.4 let
7.5 val SOME (t', _) = factout_p_ thy t;
7.6 val SOME (t'', asm) = cancel_p_ thy t;
7.7 - val der = Derive.reverse_deriv thy eval_rls rules ro NONE t';
7.8 + val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
7.9 val der = der @
7.10 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
7.11 val rs = (Rtools.distinct_Thm o (map #1)) der
7.12 @@ -498,7 +498,7 @@
7.13
7.14 fun next_rule thy eval_rls ro [rs] t =
7.15 let
7.16 - val der = Derive.make_deriv thy eval_rls rs ro NONE t;
7.17 + val der = Derive.do_one thy eval_rls rs ro NONE t;
7.18 in case der of (_, r, _) :: _ => SOME r | _ => NONE end
7.19 | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate");
7.20
7.21 @@ -537,7 +537,7 @@
7.22 let
7.23 val SOME (t',_) = common_nominator_p_ thy t;
7.24 val SOME (t'', asm) = add_fraction_p_ thy t;
7.25 - val der = Derive.reverse_deriv thy eval_rls rules ro NONE t';
7.26 + val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
7.27 val der = der @
7.28 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
7.29 val rs = (Rtools.distinct_Thm o (map #1)) der;
7.30 @@ -559,7 +559,7 @@
7.31 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
7.32
7.33 fun next_rule thy eval_rls ro [rs] t =
7.34 - let val der = Derive.make_deriv thy eval_rls rs ro NONE t;
7.35 + let val der = Derive.do_one thy eval_rls rs ro NONE t;
7.36 in
7.37 case der of
7.38 (_,r,_)::_ => SOME r
8.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Thu Apr 23 09:29:56 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Thu Apr 23 12:34:54 2020 +0200
8.3 @@ -9,15 +9,15 @@
8.4 val eval_prog_expr: theory -> Rule_Set.T -> term -> term
8.5 val eval_true_: theory -> Rule_Set.T -> term -> bool
8.6 val eval_true: theory -> term list -> Rule_Set.T -> bool
8.7 - val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
8.8 + val rew_sub: theory -> int -> (term * term) list -> Rule_Def.rew_ord_
8.9 -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
8.10 - val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
8.11 + val rewrite_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
8.12 term -> (term * term list) option
8.13 - val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
8.14 + val rewrite_inst_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
8.15 -> (term * term) list -> thm -> term -> (term * term list) option
8.16 val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
8.17 val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
8.18 - val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
8.19 + val rewrite_terms_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
8.20 -> term -> (term * term list) option
8.21
8.22 val trace_on: bool Unsynchronized.ref
8.23 @@ -27,7 +27,7 @@
8.24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.25 (* NONE *)
8.26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.27 - val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
8.28 + val rewrite__: theory -> int -> (term * term) list -> Rule_Def.rew_ord_ ->
8.29 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
8.30 val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
8.31 val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
9.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Thu Apr 23 09:29:56 2020 +0200
9.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Thu Apr 23 12:34:54 2020 +0200
9.3 @@ -19,10 +19,12 @@
9.4 val cut_id: string -> string
9.5 val id_of_thm: thm -> string
9.6 val of_thm: thm -> T
9.7 + val from_rule : Rule.rule -> T
9.8
9.9 val is_sym: id -> bool
9.10 val revert_sym_rule: theory -> Rule.rule -> Rule.rule
9.11
9.12 +
9.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.14 val string_of_thm_in_thy: theory -> thm -> string
9.15 val id_drop_sym: id -> id
9.16 @@ -84,7 +86,7 @@
9.17 (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
9.18 fun sym_thm thm =
9.19 let
9.20 - val (deriv,
9.21 + val (derivation,
9.22 {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs,
9.23 prop = prop}) = Thm.rep_thm_G thm
9.24 val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop
9.25 @@ -92,7 +94,7 @@
9.26 NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))
9.27 | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
9.28 in
9.29 - Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop'
9.30 + Thm.assbl_thm derivation cert tags maxidx shyps hyps tpairs prop'
9.31 end
9.32
9.33 fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty
9.34 @@ -129,4 +131,7 @@
9.35 else Rule.Thm (Thm.get_name_hint thm, thm)
9.36 | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)
9.37
9.38 +fun from_rule (Rule.Thm (id, thm)) = (id, thm)
9.39 + | from_rule r = raise ERROR ("rule2thm': not defined for " ^ Rule.to_string r);
9.40 +
9.41 (**)end(**)
10.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 09:29:56 2020 +0200
10.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 12:34:54 2020 +0200
10.3 @@ -117,13 +117,13 @@
10.4 *)
10.5 "----------------------------------------------------------";
10.6
10.7 - val fod = Derive.make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
10.8 + val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
10.9 ((#rules o Rule_Set.rep) Test_simplify)
10.10 (sqrt_right false (@{theory "Pure"})) NONE
10.11 (str2term "x + 1 + -1 * 2 = 0");
10.12 (writeln o Derive.trtas2str) fod;
10.13
10.14 - val ifod = Derive.make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
10.15 + val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
10.16 ((#rules o Rule_Set.rep) Test_simplify)
10.17 (sqrt_right false (@{theory "Pure"})) NONE
10.18 (str2term "-2 * 1 + (1 + x) = 0");
11.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Apr 23 09:29:56 2020 +0200
11.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Apr 23 12:34:54 2020 +0200
11.3 @@ -348,12 +348,12 @@
11.4 | _ => TermC.empty (*on PblObj is fo <> ifo*);
11.5 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
11.6 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
11.7 - (*val (found, der) = *)Derive.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
11.8 + (*val (found, der) = *)Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
11.9 "~~~~~ fun .concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
11.10 (rew_ord, erls, rules, fo, ifo);
11.11 fun derivat ([]:(term * rule * (term * term list)) list) = TermC.empty
11.12 | derivat dt = (#1 o #3 o last_elem) dt
11.13 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
11.14 - (*val fod = *)Derive.make_deriv (Isac"") erls rules (snd rew_ord) NONE fo;
11.15 - (*val ifod = *)Derive.make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo;
11.16 + (*val fod = *)Derive.do_one (Isac"") erls rules (snd rew_ord) NONE fo;
11.17 + (*val ifod = *)Derive.do_one (Isac"") erls rules (snd rew_ord) NONE ifo;
11.18