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