(* 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(**)