(* Title:  Interpret/derive.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

Derive makes (term * rule * result) steps (= derivation) for term transformations,

which cannot be done by rewriting, e.g cancellation of polynomials.

*)

signature DERIVE =

sig

  (*TODO cleanup signature*)

  type der

  type deri

  type derivation

(*val make_deriv *)

  val do_one : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->

    term option -> term -> derivation

(*val reverse_deriv *)

  val steps_reverse : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->

    term option -> term -> deri list

(*val concat_deriv *)

  val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->

    bool * der list

  val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T

(* ---- 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(**): DERIVE(**) =

struct

(**)

(** the triple for a step **)

type der =        (* 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                *)

type deri = Rule.rule * (term * term list)

type derivation = der 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

(** make one triple towards the goal term **)

fun msg_1 rts =

  (tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n");

   tracing (deriv2str rts));

fun msg_2 thmid =

  if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");

fun msg_3 t' =

  if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();

fun msg_4 op_ =

  if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"");

fun msg_5 t' =

  if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')

fun do_one thy erls rs ro goal tt = 

  let 

    datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)

    fun rew_once _ rts t Noap [] = 

        (case goal of NONE => rts | SOME _ =>

          raise ERROR ("do_one: 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 (msg_1 rts; rts)

      else

        (case r of

          Rule.Thm (thmid, tm) => 

            (msg_2 thmid;

            case Rewrite.rewrite_ thy ro erls true tm t of

              NONE => rew_once lim rts t apno rs'

            | SOME (t', a') =>

              (msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))

        | Rule.Eval (c as (op_, _)) => 

            (msg_4 op_;

            case Eval.adhoc_thm thy c (TermC.uminus_to_string 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 => raise ERROR "adhoc_thm: NONE"

                val _ = msg_5 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")

        | Rule.Rls_ rls =>

          (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 => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))

    | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"

  in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end

(** concatenate several steps in revers order **)

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

fun steps_reverse thy erls rs ro goal t =

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

(** concatenate several steps **)

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

(* fo = ifo excluded already in inform *)

fun steps 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 = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE  fo

    val ifod = do_one (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

(* embed the tacis created by a '_deriv'ation; sys.form <> input.form

  tacis are in order, thus are reverted for generate *)

fun embed tacis (pt, pos as (p, Pos.Frm)) =

  (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402

    and transfer the istate (from _after_ compare_deriv) from Frm to Res*)

    let

      val (res, asm) = (State_Steps.result o last_elem) tacis

    	val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of

    	  (SOME (ist, ctxt), _) => (ist, ctxt)

      | (NONE, _) => error "Derive.embed Frm: uncovered case get_obj"

    	val form =  Ctree.get_obj  Ctree.g_form pt p

      (*val p = lev_on p; ---------------only difference to (..,Res) below*)

    	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::

    		(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),

    			(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]

    	val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))

    	val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))

    	val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))

    	val pt = Ctree.update_branch pt p Ctree.TransitiveB

    in (c, (pt, pos)) end

  | embed tacis (pt, (p, Pos.Res)) =

    (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?

      and transfer the istate (from _after_ compare_deriv) from Res to new Res*)

    let

      val (res, asm) = (State_Steps.result o last_elem) tacis

    	val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of

    	  (_, SOME (ist, ctxt)) => (ist, ctxt)

      | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"

    	val (f, _) = Ctree.get_obj Ctree.g_result pt p

    	val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);

    	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::

    		(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), 

    			(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];

    	val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))

    	val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))

    	val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))

    	val pt = Ctree.update_branch pt p Ctree.TransitiveB

    in (c, (pt, pos)) end

  | embed _ _ = error "Derive.embed: uncovered definition"

(**)end(**)