(* Handle user-input during the specify- and the solve-phase. 

    author: Walther Neuper

    0603

    (c) due to copyright terms

 *)

 signature ERROR_PATTERN =

 sig

   val find_fillpatterns : Calc.T -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list

   val is_exactly_equal : Calc.T -> string -> string * Tactic.input

   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 mk_tacis: Rule_Def.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))

   val fetchErrorpatterns : Tactic.input -> Rule.errpatID list

   val check_for :

     term * term ->

     term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule_Set.T -> Rule.errpatID option

   val rule2thm'' : Rule.rule -> Celem.thm''

   val rule2rls' : Rule.rule -> string

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

   (*  NONE *)

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

   val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list

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

   val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule_Set.T -> Rule.errpatID option

   val get_fillform :

      'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option

   val get_fillpats :

      'a * (term * term) list -> term -> Rule.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list

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

 end

 (**)

 structure Error_Pattern(**): ERROR_PATTERN(**) =

 struct

 (**)

 fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)

   | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule_Set.rule2str r);

 fun rule2rls' (Rule.Rls_ rls) = Rule_Set.id_rls rls

   | rule2rls' r = error ("rule2rls': not defined for " ^ Rule_Set.rule2str r);

 (*the lists contain eq-al elem-pairs at the beginning;

   return first list reverted (again) - ie. in order as required subsequently*)

 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =

     if equal f1 i1 then

       if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)

       else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)

     else error "dropwhile': did not start with equal elements"

   | dropwhile' equal (f::fs) [i] =

     if equal f i then

       (rev (f::fs), [i])

     else error "dropwhile': did not start with equal elements"

   | dropwhile' equal [f] (i::is) =

     if equal f i then

       ([f], i::is)

     else error "dropwhile': did not start with equal elements"

   | dropwhile' _ _ _ = error "dropwhile': uncovered case"

 (* 040214: version for concat_deriv *)

 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));

 fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) = 

       (Tactic.Rewrite (id, thm), 

         Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, rule2thm'' r, t, (t', a)),

        (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))

   | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) = 

       (Tactic.Rewrite_Set (rule2rls' r), 

         Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),

        (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))

   | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule_Set.rule2str r ^ " at " ^ Rule.term2str t)

 (* 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) = Rule.e_term

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

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

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

     val ifod = Rtools.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

 (*** handle an error pattern ***)

 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)

 fun check_err_patt (res, inf) subst (errpatID, pat) rls =

   let 

     val (res', _, _, rewritten) =

       Rewrite.rew_sub (ThyC.Isac()) 1 subst Rule.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;

   in

     if rewritten then 

       let

         val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls  res' of

           NONE => res'

         | SOME (norm_res, _) => norm_res

         val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of

           NONE => inf

         | SOME (norm_inf, _) => norm_inf

       in if norm_res = norm_inf then SOME errpatID else NONE

       end

     else NONE

   end;

 (* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;

    (prog, env) for retrieval of casual substitution for bdv in the pattern. *)

 fun check_for (res, inf) (prog, env) (errpats, rls) =

   let

     val (_, subst) = Rtools.get_bdv_subst prog env

     fun scan (_, [], _) = NONE

       | scan (errpatID, errpat :: errpats, _) =

           case check_err_patt (res, inf) subst (errpatID, errpat) rls of

             NONE => scan (errpatID, errpats, [])

           | SOME errpatID => SOME errpatID

     fun scans [] = NONE

       | scans (group :: groups) =

           case scan group of

             NONE => scans groups

           | SOME errpatID => SOME errpatID

   in scans errpats end;

 (* fill-in patterns an forms.

   returns thm required by "fun in_fillform *)

 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =

   let

     val (form', _, _, rewritten) =

       Rewrite.rew_sub (ThyC.Isac()) 1 subst Rule.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;

   in (*the fillpat of the thm must be dedicated to errpatID*)

     if errpatID = erpaID andalso rewritten then

       SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) 

     else NONE

   end

 fun get_fillpats subst form errpatID thm =

   let

     val thmDeriv = Thm.get_name_hint thm

     val (part, thyID) = Rtools.thy_containing_thm thmDeriv

     val theID = [part, thyID, "Theorems", Celem.thmID_of_derivation_name thmDeriv]

     val fillpats = case Specify.get_the theID of

       Celem.Hthm {fillpats, ...} => fillpats

     | _ => error "get_fillpats: uncovered case of get_the"

     val some = map (get_fillform subst (thm, form) errpatID) fillpats

   in some |> filter is_some |> map the end

 fun find_fillpatterns (pt, pos as (p, _): Pos.pos') errpatID =

   let 

     val f_curr = Ctree.get_curr_formula (pt, pos);

     val pp = Ctree.par_pblobj pt p

     val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of

       {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)

     | _ => error "find_fillpatterns: uncovered case of get_met"

     val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate

     val subst = Rtools.get_bdv_subst prog env

     val errpatthms = errpats

       |> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID))

       |> map (#3: Rule.errpat -> thm list)

       |> flat

   in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end

 (* check if an input formula is exactly equal the rewrite from a rule

    which is stored at the pos where the input is stored of "ok". *)

 fun is_exactly_equal (pt, pos as (p, _)) istr =

   case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> ThyC.thy2ctxt) istr of

     NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")

   | SOME ifo => 

       let

         val p' = Pos.lev_on p;

         val tac = Ctree.get_obj Ctree.g_tac pt p';

       in 

         case Applicable.applicable_in pos pt tac of

           Applicable.Notappl msg => (msg, Tactic.Tac "")

         | Applicable.Appl rew =>

             let

               val res = case rew of

                Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res

               |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res

               | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t)

             in 

               if not (ifo = res) then

                 ("input does not exactly fill the gaps", Tactic.Tac "")

               else ("ok", tac)

             end

       end

 (* fetch errpatIDs from an arbitrary tactic *)

 fun fetchErrorpatterns tac =

   let

     val rlsID =

       case tac of

        Tactic.Rewrite_Set rlsID => rlsID

       |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID

       | _ => "empty"

     val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;

     val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of

       Celem.Hrls {thy_rls = (_, rls), ...} => rls

     | _ => error "fetchErrorpatterns: uncovered case of get_the"

   in case rls of

     Rule_Def.Repeat {errpatts, ...} => errpatts

   | Rule_Set.Seqence {errpatts, ...} => errpatts

   | Rule_Set.Rrls {errpatts, ...} => errpatts

   | Rule_Set.Empty => []

   end

 (**)

 end

 (**)