(* Title:  Interpret/derive.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 *)

 signature DERIVATION =

 sig

   type deriv

   val make_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->

     term option -> term -> deriv

   val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->

     Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list

   val reverse_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->

     term option -> term -> (Rule.rule * (term * term list)) list

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*  NONE *)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   val trtas2str : (term * Rule.rule * (term * term list)) list -> string

   val deriv2str : (term * Rule.rule * (term * term list)) list -> string

   val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 (**)

 structure Derive(**): DERIVATION(**) =

 struct

 (**)

 (*/------- to Derive from Rtools -------\*)

 (*** reverse rewriting ***)

 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls       *

  *  of for connecting a user-input formula with the current calc-state.	     *

  *# It is somewhat incompatible with the rest of the math-engine:	     *

  *  (1) it is not created by a script					     *

  *  (2) thus there cannot be another user-input within a derivation	     *

  *# It suffers particularily from the not-well-foundedness of the math-engine*

  *  (1) FIXME other branchtyptes than Transitive will change 'embed_deriv'   *

  *  (2) FIXME and eventually 'compare_step' (ie. the script interpreter)     *

  *  (3) FIXME and eventually 'lev_back'                                      *

  *# SOME improvements are evident FIXME.040215 '_deriv'ation:	             *

  *  (1) FIXME nest Rls_ in 'make_deriv'					     *

  *  (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus    *

  *	user-input will become possible in this part of a derivation	     *

  *  (3) FIXME do (2) only if a derivation has been found -- for efficiency,  *

  *	while a non-derivable inform requires to step until End_Proof'	     *

  *  (4) FIXME find criteria on when _not_ to step until End_Proof'           *

  *  (5) FIXME 

 .*)

 type deriv =      (* derivation for inserting one level of nodes into the Ctree *) 

   ( term *        (* where the rule is applied to                               *)

     Rule.rule *   (* rule to be applied                                         *)

     ( term *      (* resulting from rule application                            *)

       term list)) (* assumptions resulting from rule application                *)

   list

 fun trta2str (t, r, (t', a)) =

   "\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))"

 fun trtas2str trtas = (strs2str o (map trta2str)) trtas

 val deriv2str = trtas2str

 (*\------- to Derive from Rtools -------/*)

 (*/------- to Derive from Rtools -------\*)

 (* derive normalform of a rls, or derive until SOME goal,

    and record rules applied and rewrites.

 val it = fn

   : theory

     -> rls

     -> rule list

     -> rew_ord       : the order of this rls, which 1 theorem of is used 

                        for rewriting 1 single step (?14.4.03)

     -> term option   : 040214 ??? use for "derive until SOME goal" ??? 

     -> term 

     -> (term *       : to this term ...

         rule * 	     : ... this rule is applied yielding ...

         (term *      : ... this term ...

          term list)) : ... under these assumptions.

        list          :

 returns empty list for a normal form

 FIXME.WN040214: treats rules as in Rls, _not_ as in Seq

 WN060825 too complicated for the intended use by cancel_, common_nominator_

 and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..

  -- replaced below *)

 fun make_deriv thy erls rs ro goal tt = 

   let 

     datatype switch = Appl | Noap (* unify with version in rewrite.sml *)

     fun rew_once _ rts t Noap [] = 

         (case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ UnparseC.term t))

       | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs

         (*| Seq _ => rts) FIXXXXXME 14.3.03*)

       | rew_once lim rts t apno rs' =

         (case goal of 

           NONE => rew_or_calc lim rts t apno rs'

         | 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 (! Rewrite.lim_deriv) ^ "with deriv =\n");

         tracing (deriv2str rts); rts)

       else

         (case r of

           Rule.Thm (thmid, tm) => 

             (if not (! Rewrite.trace_on) 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 ! Rewrite.trace_on 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 (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"")

             val t = TermC.uminus_to_string t

           in 

             case Eval.adhoc_thm thy c t of

               NONE => rew_once lim rts t apno rs'

             | SOME (thmid, tm) => 

               (let

                 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of

                   SOME ta => ta

                 | NONE => error "adhoc_thm: NONE"

                 val _ = if not (! Rewrite.trace_on) 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 _ => raise ERROR "derive_norm, Eval: no rewrite"

           end

         | Rule.Rls_ rls => (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)

           (case Rewrite.rewrite_set_ thy true rls t of

             NONE => rew_once lim rts t apno rs'

           | 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 (! Rewrite.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));

 fun reverse_deriv thy erls rs ro goal t =

     (rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)

 (*\------- to Derive from Rtools -------/*)

 (*/------- to NEW Derive from Error_Fill_Pattern -------\*)

 (* 040214: version for concat_deriv *)

 fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));

 (* fo = ifo excluded already in inform *)

 fun concat_deriv rew_ord erls rules fo ifo =

   let 

     fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty

       | derivat dt = (#1 o #3 o last_elem) dt

     fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2

     val  fod = make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE  fo

     val ifod = make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo

   in 

     case (fod, ifod) of

       ([], []) => if fo = ifo then (true, []) else (false, [])

     | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])

     | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])

     | (fod, ifod) =>

       if derivat fod = derivat ifod (*common normal form found*) then

         let 

           val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)

         in (true, fod' @ (map rev_deriv' rifod')) end

       else (false, [])

   end

 (*\------- to NEW Derive from Error_Fill_Pattern-------/*)

 (**)end(**)