(* Title:  Interpret/derive.sml

    Author: Walther Neuper

    (c) due to copyright terms

 Try to make (term * rule * result) steps (= derivation) by use of a Rule_Set.T.

 Two purposes:

 (1) derive steps from a given term towards another give term

 (2) term transformations, which cannot be done by rewriting, e.g cancellation of polynomials.

 *)

 signature DERIVE =

 sig

   type rule_result

   type step

   type derivation

   val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->

     term option -> term -> derivation

   val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->

     term option -> term -> rule_result list

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

     bool * derivation

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

 \<^isac_test>\<open>

   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)

 \<close>

 end

 (**)

 structure Derive(**): DERIVE(**) =

 struct

 (**)

 (** the triple for a step **)

 type rule_result = Rule.rule * Calc.result;

 type step = term * Rule.rule * Calc.result;

 type derivation = step 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 ctxt rts =

   (tracing ("do_one exceeds " ^ int2str (Config.get ctxt rewrite_limit) ^ "with derivation =\n");

    tracing (deriv2str rts));

 fun msg_2 ctxt thmid =

   if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");

 fun msg_3 ctxt t' =

   if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();

 fun msg_4 ctxt op_ =

   if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying calc. \"" ^ op_^"\"");

 fun msg_5 ctxt t' =

   if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term t')

 fun do_one ctxt 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 ("Derive.do_one: no derivation for " ^ UnparseC.term t))

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

       | 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 ctxt rts; rts)

       else

         (case r of

           Rule.Thm (thmid, tm) => 

             (msg_2 ctxt thmid;

             case Rewrite.rewrite_ ctxt ro erls true tm t of

               NONE => rew_once lim rts t apno rs'

             | SOME (t', a') =>

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

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

             (msg_4 ctxt op_;

             case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c t of

               NONE => rew_once lim rts t apno rs'

             | SOME (thmid, tm) => 

               (let

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

                   SOME ta => ta

                 | NONE => raise ERROR "adhoc_thm: NONE"

                 val _ = msg_5 ctxt t'

                 val r' = Rule.Thm (thmid, tm)

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

                 handle Rewrite.NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite")

         | Rule.Rls_ rls =>

           (case Rewrite.rewrite_set_ ctxt 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 (Config.get ctxt rewrite_limit) [] 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 (Proof_Context.init_global (ThyC.Isac())) erls rules (snd rew_ord) NONE  fo

     val ifod = do_one (Proof_Context.init_global (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 a derivation into the Ctree **)

 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, _) => raise 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, ...} = MethodC.from_store (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) => raise 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, ...} = MethodC.from_store (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 _ _ = raise ERROR "Derive.embed: uncovered definition"

 (**)end(**)