walther@59909: (* title: Interpret/error-pattern.sml
neuper@37906:    author: Walther Neuper
neuper@37906:    0603
neuper@37906:    (c) due to copyright terms
walther@59858: 
walther@59906: In case a term is input, which contains an "error pattern" (provided by a mathauthor),
walther@59906: several "fill patterns" can be presented as help for the next step.)
neuper@37906: *)
neuper@37906: 
walther@59909: signature ERROR_PATTERN =
wneuper@59262: sig
walther@59909:   type id = Error_Pattern_Def.id
walther@59909:   type T = Error_Pattern_Def.T
walther@59909:   val s_to_string : T list -> string
walther@59971:   val empty: T
walther@59858: 
walther@59909:   type fill_in_id = Error_Pattern_Def.fill_in_id
walther@59909:   type fill_in = Error_Pattern_Def.fill_in
walther@59971:   val fill_in_empty: fill_in
walther@59971: 
walther@59909:   type record
walther@59909: 
walther@59909:   val from_store: Tactic.input -> Error_Pattern_Def.id list
walther@59909:   val filled_exactly: Calc.T -> string -> string * Tactic.input
walther@59909:   val check_for: term * term -> term * Env.T -> T list * Rule_Set.T -> id option
walther@59906: 
walther@59909:   val find_fill_patterns: Calc.T -> id -> record list
wenzelm@60223: 
wenzelm@60223: \<^isac_test>\<open>
walther@59910:   val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option
Walther@60477:   val fill_from_store: Subst.input option * Subst.T -> term -> id -> thm ->
walther@59909:     record list
Walther@60477:   val fill_form: Subst.input option * Subst.T -> thm * term -> id -> fill_in ->
walther@59909:     record option
wenzelm@60223: \<close>
walther@59909: end
wneuper@59310: 
walther@59822: (**)
walther@59909: structure Error_Pattern(**): ERROR_PATTERN(**) =
walther@59822: struct
walther@59822: (**)
neuper@37906: 
walther@59909: type id = Error_Pattern_Def.id;
walther@59909: type T = Error_Pattern_Def.T;
walther@59909: val s_to_string = Error_Pattern_Def.s_to_string;
walther@59971: val empty = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}])
walther@59858: 
walther@59909: type fill_in_id = Error_Pattern_Def.fill_in_id;
walther@59909: type fill_in = Error_Pattern_Def.fill_in;
walther@59971: val fill_in_empty = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
walther@59971: 
walther@59911: type record = (fill_in_id * term * thm * Subst.input option);
walther@59822: 
walther@59909: (*
walther@59909:   check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
walther@59909: *)
walther@59909: fun check_for' (res, inf) subst (id, pat) rls =
Walther@60500:   let
Walther@60500:     val ctxt = Proof_Context.init_global ((ThyC.Isac()))
Walther@60500:     val (res', _, _, rewritten) =
Walther@60509:       Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty
Walther@60500:         Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
neuper@42423:   in
walther@59848:     if rewritten then 
neuper@42423:       let
Walther@60500:         val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls  res' of
walther@59909:             NONE => res'
walther@59909:           | SOME (norm_res, _) => norm_res
Walther@60500:         val norm_inf = case Rewrite.rewrite_set_inst_ ctxt false subst rls inf of
walther@59909:             NONE => inf
walther@59909:           | SOME (norm_inf, _) => norm_inf
walther@59909:       in
walther@59909:         if norm_res = norm_inf then SOME id else NONE
neuper@42423:       end
neuper@42423:     else NONE
neuper@42423:   end;
neuper@42423: 
walther@59908: (*
walther@59908:   check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
walther@59908:   (prog, env) for retrieval of casual substitution for bdv in the pattern.
walther@59908: *)
walther@59844: fun check_for (res, inf) (prog, env) (errpats, rls) =
neuper@42428:   let
walther@59911:     val (_, subst) = Subst.for_bdv prog env
neuper@42428:     fun scan (_, [], _) = NONE
walther@59909:       | scan (id, T :: errpats, _) =
walther@59909:           case check_for' (res, inf) subst (id, T) rls of
walther@59909:             NONE => scan (id, errpats, [])
walther@59909:           | SOME id => SOME id
neuper@42428:     fun scans [] = NONE
neuper@42428:       | scans (group :: groups) =
neuper@42428:           case scan group of
neuper@42428:             NONE => scans groups
walther@59909:           | SOME id => SOME id
neuper@42428:   in scans errpats end;
neuper@42428: 
neuper@42433: (* fill-in patterns an forms.
neuper@42433:   returns thm required by "fun in_fillform *)
walther@59909: fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =
neuper@42430:   let
Walther@60500:     val ctxt = Proof_Context.init_global ((ThyC.Isac()))
neuper@42430:     val (form', _, _, rewritten) =
Walther@60509:       Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
walther@59909:   in (*the fillpat of the thm must be dedicated to id*)
walther@59909:     if id = erpaID andalso rewritten then
walther@59848:       SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) 
wneuper@59264:     else NONE
wneuper@59264:   end
neuper@42430: 
walther@59909: fun fill_from_store subst form id thm =
wneuper@59264:   let
wneuper@59264:     val thmDeriv = Thm.get_name_hint thm
walther@59916:     val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
walther@59876:     val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
walther@59970:     val fillpats = case Thy_Read.from_store theID of
walther@59917:       Thy_Write.Hthm {fillpats, ...} => fillpats
walther@59909:     | _ => raise ERROR "fill_from_store: uncovered case of get_the"
walther@59909:     val some = map (fill_form subst (thm, form) id) fillpats
wneuper@59264:   in some |> filter is_some |> map the end
neuper@42430: 
walther@59909: fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =
neuper@42430:   let 
wneuper@59276:     val f_curr = Ctree.get_curr_formula (pt, pos);
wneuper@59276:     val pp = Ctree.par_pblobj pt p
walther@60154:     val (errpats, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
wneuper@59416:       {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
walther@59909:     | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
walther@59807:     val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
walther@59911:     val subst = Subst.for_bdv prog env
neuper@42430:     val errpatthms = errpats
walther@59909:       |> filter ((curry op = id) o (#1: Error_Pattern_Def.T -> Error_Pattern_Def.id))
walther@59909:       |> map (#3: Error_Pattern_Def.T -> thm list)
neuper@42430:       |> flat
walther@59909:   in map (fill_from_store subst f_curr id) errpatthms |> flat end
neuper@37906: 
walther@59909: (*
walther@59909:   Check input on a fill-pattern:
walther@59909:   check if input is exactly equal to the rewrite from a rule
walther@59909:   which is stored at the pos where the input is stored of "ok".
walther@59909: *)
walther@59909: fun filled_exactly (pt, pos as (p, _)) istr =
walther@60360:   case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr of
wneuper@59571:     NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
neuper@42437:   | SOME ifo => 
neuper@42437:       let
walther@59757:         val p' = Pos.lev_on p;
wneuper@59276:         val tac = Ctree.get_obj Ctree.g_tac pt p';
neuper@42437:       in 
walther@59921:         case Solve_Step.check tac (pt, pos) of
walther@59920:           Applicable.No msg => (msg, Tactic.Tac "")
walther@59920:         | Applicable.Yes rew =>
neuper@42437:             let
neuper@42437:               val res = case rew of
wneuper@59571:                Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
wneuper@59571:               |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
walther@59909:               | t => raise ERROR ("filled_exactly: uncovered case for " ^ Tactic.string_of t)
neuper@42437:             in 
walther@59848:               if not (ifo = res) then
walther@59848:                 ("input does not exactly fill the gaps", Tactic.Tac "")
neuper@42437:               else ("ok", tac)
neuper@42437:             end
neuper@42437:       end
neuper@42437: 
neuper@42458: (* fetch errpatIDs from an arbitrary tactic *)
walther@59909: fun from_store tac =
neuper@42458:   let
neuper@42458:     val rlsID =
neuper@42458:       case tac of
wneuper@59571:        Tactic.Rewrite_Set rlsID => rlsID
wneuper@59571:       |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
walther@59852:       | _ => "empty"
walther@59916:     val (part, thyID) = Thy_Read.thy_containing_rls "Isac_Knowledge" rlsID;
walther@59970:     val rls = case Thy_Read.from_store [part, thyID, "Rulesets", rlsID] of
walther@59917:       Thy_Write.Hrls {thy_rls = (_, rls), ...} => rls
walther@59909:     | _ => raise ERROR "from_store: uncovered case of get_the"
neuper@42458:   in case rls of
walther@59851:     Rule_Def.Repeat {errpatts, ...} => errpatts
walther@59878:   | Rule_Set.Sequence {errpatts, ...} => errpatts
walther@59850:   | Rule_Set.Rrls {errpatts, ...} => errpatts
walther@59851:   | Rule_Set.Empty => []
neuper@42458:   end
wneuper@59264: 
walther@59858: (**)end(**)