1.1 --- a/src/Tools/isac/Interpret/derive.sml Thu Apr 23 09:29:56 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/derive.sml Thu Apr 23 12:34:54 2020 +0200
1.3 @@ -2,18 +2,25 @@
1.4 Author: Walther Neuper 2019
1.5 (c) due to copyright terms
1.6
1.7 -
1.8 +Derive makes (term * rule * result) steps (= derivation) for term transformations,
1.9 +which cannot be done by rewriting, e.g cancellation of polynomials.
1.10 *)
1.11
1.12 -signature DERIVATION =
1.13 +signature DERIVE =
1.14 sig
1.15 - type deriv
1.16 - val make_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
1.17 - term option -> term -> deriv
1.18 - val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
1.19 - Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
1.20 - val reverse_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
1.21 - term option -> term -> (Rule.rule * (term * term list)) list
1.22 + (*TODO cleanup signature*)
1.23 + type der
1.24 + type deri
1.25 + type derivation
1.26 +(*val make_deriv *)
1.27 + val do_one : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
1.28 + term option -> term -> derivation
1.29 +(*val reverse_deriv *)
1.30 + val steps_reverse : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
1.31 + term option -> term -> deri list
1.32 +(*val concat_deriv *)
1.33 + val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
1.34 + bool * der list
1.35 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.36 (* NONE *)
1.37 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.38 @@ -24,70 +31,45 @@
1.39 end
1.40
1.41 (**)
1.42 -structure Derive(**): DERIVATION(**) =
1.43 +structure Derive(**): DERIVE(**) =
1.44 struct
1.45 (**)
1.46 -(*/------- to Derive from Rtools -------\*)
1.47 -(*** reverse rewriting ***)
1.48 -(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
1.49 - * of for connecting a user-input formula with the current calc-state. *
1.50 - *# It is somewhat incompatible with the rest of the math-engine: *
1.51 - * (1) it is not created by a script *
1.52 - * (2) thus there cannot be another user-input within a derivation *
1.53 - *# It suffers particularily from the not-well-foundedness of the math-engine*
1.54 - * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
1.55 - * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
1.56 - * (3) FIXME and eventually 'lev_back' *
1.57 - *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
1.58 - * (1) FIXME nest Rls_ in 'make_deriv' *
1.59 - * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
1.60 - * user-input will become possible in this part of a derivation *
1.61 - * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
1.62 - * while a non-derivable inform requires to step until End_Proof' *
1.63 - * (4) FIXME find criteria on when _not_ to step until End_Proof' *
1.64 - * (5) FIXME
1.65 -.*)
1.66 -type deriv = (* derivation for inserting one level of nodes into the Ctree *)
1.67 +
1.68 +(** the triple for a step **)
1.69 +
1.70 +type der = (* derivation for inserting one level of nodes into the Ctree *)
1.71 ( term * (* where the rule is applied to *)
1.72 Rule.rule * (* rule to be applied *)
1.73 ( term * (* resulting from rule application *)
1.74 - term list)) (* assumptions resulting from rule application *)
1.75 - list
1.76 + term list));(* assumptions resulting from rule application *)
1.77 +type deri = Rule.rule * (term * term list)
1.78 +type derivation = der list
1.79
1.80 fun trta2str (t, r, (t', a)) =
1.81 "\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))"
1.82 fun trtas2str trtas = (strs2str o (map trta2str)) trtas
1.83 val deriv2str = trtas2str
1.84 -(*\------- to Derive from Rtools -------/*)
1.85 -(*/------- to Derive from Rtools -------\*)
1.86 -(* derive normalform of a rls, or derive until SOME goal,
1.87 - and record rules applied and rewrites.
1.88 -val it = fn
1.89 - : theory
1.90 - -> rls
1.91 - -> rule list
1.92 - -> rew_ord : the order of this rls, which 1 theorem of is used
1.93 - for rewriting 1 single step (?14.4.03)
1.94 - -> term option : 040214 ??? use for "derive until SOME goal" ???
1.95 - -> term
1.96 - -> (term * : to this term ...
1.97 - rule * : ... this rule is applied yielding ...
1.98 - (term * : ... this term ...
1.99 - term list)) : ... under these assumptions.
1.100 - list :
1.101 -returns empty list for a normal form
1.102 -FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
1.103
1.104 -WN060825 too complicated for the intended use by cancel_, common_nominator_
1.105 -and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..
1.106 - -- replaced below *)
1.107 +(** make one triple towards the goal term **)
1.108
1.109 +fun msg_1 rts =
1.110 + (tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n");
1.111 + tracing (deriv2str rts));
1.112 +fun msg_2 thmid =
1.113 + if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
1.114 +fun msg_3 t' =
1.115 + if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
1.116 +fun msg_4 op_ =
1.117 + if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"");
1.118 +fun msg_5 t' =
1.119 + if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
1.120
1.121 -fun make_deriv thy erls rs ro goal tt =
1.122 +fun do_one thy erls rs ro goal tt =
1.123 let
1.124 - datatype switch = Appl | Noap (* unify with version in rewrite.sml *)
1.125 + datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
1.126 fun rew_once _ rts t Noap [] =
1.127 - (case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ UnparseC.term t))
1.128 + (case goal of NONE => rts | SOME _ =>
1.129 + raise ERROR ("do_one: no derivation for " ^ UnparseC.term t))
1.130 | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
1.131 (*| Seq _ => rts) FIXXXXXME 14.3.03*)
1.132 | rew_once lim rts t apno rs' =
1.133 @@ -96,60 +78,56 @@
1.134 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
1.135 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
1.136 if lim < 0
1.137 - then (tracing ("make_deriv exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with deriv =\n");
1.138 - tracing (deriv2str rts); rts)
1.139 + then (msg_1 rts; rts)
1.140 else
1.141 (case r of
1.142 Rule.Thm (thmid, tm) =>
1.143 - (if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
1.144 + (msg_2 thmid;
1.145 case Rewrite.rewrite_ thy ro erls true tm t of
1.146 NONE => rew_once lim rts t apno rs'
1.147 | SOME (t', a') =>
1.148 - (if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
1.149 - rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
1.150 + (msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
1.151 | Rule.Eval (c as (op_, _)) =>
1.152 - let
1.153 - val _ = if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"")
1.154 - val t = TermC.uminus_to_string t
1.155 - in
1.156 - case Eval.adhoc_thm thy c t of
1.157 + (msg_4 op_;
1.158 + case Eval.adhoc_thm thy c (TermC.uminus_to_string t) of
1.159 NONE => rew_once lim rts t apno rs'
1.160 | SOME (thmid, tm) =>
1.161 (let
1.162 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
1.163 SOME ta => ta
1.164 - | NONE => error "adhoc_thm: NONE"
1.165 - val _ = if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
1.166 + | NONE => raise ERROR "adhoc_thm: NONE"
1.167 + val _ = msg_5 t'
1.168 val r' = Rule.Thm (thmid, tm)
1.169 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
1.170 - handle _ => raise ERROR "derive_norm, Eval: no rewrite"
1.171 - end
1.172 - | Rule.Rls_ rls => (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)
1.173 + handle _ => raise ERROR "derive_norm, Eval: no rewrite")
1.174 + | Rule.Rls_ rls =>
1.175 (case Rewrite.rewrite_set_ thy true rls t of
1.176 NONE => rew_once lim rts t apno rs'
1.177 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
1.178 - | rule => error ("rew_once: uncovered case " ^ Rule.to_string rule))
1.179 - | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
1.180 + | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))
1.181 + | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
1.182 in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
1.183
1.184 -(*version for reverse rewrite used before 040214*)
1.185 +
1.186 +(** concatenate several steps in revers order **)
1.187 +
1.188 fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
1.189 -fun reverse_deriv thy erls rs ro goal t =
1.190 - (rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)
1.191 -(*\------- to Derive from Rtools -------/*)
1.192 +fun steps_reverse thy erls rs ro goal t =
1.193 + (rev o (map rev_deriv)) (do_one thy erls rs ro goal t)
1.194
1.195 -(*/------- to NEW Derive from Error_Fill_Pattern -------\*)
1.196 -(* 040214: version for concat_deriv *)
1.197 +
1.198 +(** concatenate several steps **)
1.199 +
1.200 fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
1.201
1.202 (* fo = ifo excluded already in inform *)
1.203 -fun concat_deriv rew_ord erls rules fo ifo =
1.204 +fun steps rew_ord erls rules fo ifo =
1.205 let
1.206 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
1.207 | derivat dt = (#1 o #3 o last_elem) dt
1.208 - fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
1.209 - val fod = make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
1.210 - val ifod = make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
1.211 + fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
1.212 + val fod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
1.213 + val ifod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
1.214 in
1.215 case (fod, ifod) of
1.216 ([], []) => if fo = ifo then (true, []) else (false, [])
1.217 @@ -162,6 +140,5 @@
1.218 in (true, fod' @ (map rev_deriv' rifod')) end
1.219 else (false, [])
1.220 end
1.221 -(*\------- to NEW Derive from Error_Fill_Pattern-------/*)
1.222
1.223 (**)end(**)