(* title: Interpret/error-pattern.sml

    author: Walther Neuper

    0603

    (c) due to copyright terms

 In case a term is input, which contains an "error pattern" (provided by a mathauthor),

 several "fill patterns" can be presented as help for the next step.)

 *)

 signature ERROR_PATTERN =

 sig

   type id = Error_Pattern_Def.id

   type T = Error_Pattern_Def.T

   val s_to_string : T list -> string

   val empty: T

   type fill_in_id = Error_Pattern_Def.fill_in_id

   type fill_in = Error_Pattern_Def.fill_in

   val fill_in_empty: fill_in

   type record

   val from_store: Tactic.input -> Error_Pattern_Def.id list

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

   val check_for: Proof.context -> term * term -> term * Env.T -> T list * Rule_Set.T -> id option

   val find_fill_patterns: Calc.T -> id -> record list

 \<^isac_test>\<open>

   val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id option

   val fill_from_store: Subst.input option * Subst.T -> term -> id -> thm ->

     record list

   val fill_form: Subst.input option * Subst.T -> thm * term -> id -> fill_in ->

     record option

 \<close>

 end

 (**)

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

 struct

 (**)

 type id = Error_Pattern_Def.id;

 type T = Error_Pattern_Def.T;

 val s_to_string = Error_Pattern_Def.s_to_string;

 val empty = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}])

 type fill_in_id = Error_Pattern_Def.fill_in_id;

 type fill_in = Error_Pattern_Def.fill_in;

 val fill_in_empty = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")

 type record = (fill_in_id * term * thm * Subst.input option);

 (*

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

 *)

 fun check_for' ctxt (res, inf) subst (id, pat) rls =

   let

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

       Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty

         Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;

   in

     if rewritten then 

       let

         val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls  res' of

             NONE => res'

           | SOME (norm_res, _) => norm_res

         val norm_inf = case Rewrite.rewrite_set_inst_ ctxt false subst rls inf of

             NONE => inf

           | SOME (norm_inf, _) => norm_inf

       in

         if norm_res = norm_inf then SOME id 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 ctxt (res, inf) (prog, env) (errpats, rls) =

   let

     val (_, subst) = Subst.for_bdv prog env

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

       | scan (id, T :: errpats, _) =

           case check_for' ctxt (res, inf) subst (id, T) rls of

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

           | SOME id => SOME id

     fun scans [] = NONE

       | scans (group :: groups) =

           case scan group of

             NONE => scans groups

           | SOME id => SOME id

   in scans errpats end;

 (* fill-in patterns an forms.

   returns thm required by "fun in_fillform *)

 fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =

   let

     val ctxt = Proof_Context.init_global ((ThyC.Isac()))

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

       Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;

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

     if id = erpaID andalso rewritten then

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

     else NONE

   end

 fun fill_from_store subst form id thm =

   let

     val thmDeriv = Thm.get_name_hint thm

     val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv

     val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]

     val fillpats = case Thy_Read.from_store theID of

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

     | _ => raise ERROR "fill_from_store: uncovered case of get_the"

     val some = map (fill_form subst (thm, form) id) fillpats

   in some |> filter is_some |> map the end

 fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =

   let 

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

     val pp = Ctree.par_pblobj pt p

     val (errpats, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of

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

     | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"

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

     val subst = Subst.for_bdv prog env

     val errpatthms = errpats

       |> filter ((curry op = id) o (#1: Error_Pattern_Def.T -> Error_Pattern_Def.id))

       |> map (#3: Error_Pattern_Def.T -> thm list)

       |> flat

   in map (fill_from_store subst f_curr id) errpatthms |> flat end

 (*

   Check input on a fill-pattern:

   check if input is exactly equal to the rewrite from a rule

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

 *)

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

   case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) 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 Solve_Step.check tac (pt, pos) of

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

         | Applicable.Yes rew =>

             let

               val res = case rew of

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

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

               | t => raise ERROR ("filled_exactly: 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 from_store tac =

   let

     val rlsID =

       case tac of

        Tactic.Rewrite_Set rlsID => rlsID

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

       | _ => "empty"

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

     val rls = case Thy_Read.from_store [part, thyID, "Rulesets", rlsID] of

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

     | _ => raise ERROR "from_store: uncovered case of get_the"

   in case rls of

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

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

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

   | Rule_Set.Empty => []

   end

 (**)end(**)