neuper@37906: (* Handle user-input during the specify- and the solve-phase. 
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@59858: signature ERROR_FILL_PATTERN =
wneuper@59262: sig
walther@59858:   type errpatID = Rule_Def.errpatID
walther@59858:   type errpat = errpatID * term list * thm list
walther@59858:   val errpats2str : errpat list -> string
walther@59858: 
walther@59906:   val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID ->
walther@59906:     (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
walther@59906:   val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
walther@59775:   val is_exactly_equal : Calc.T -> string -> string * Tactic.input
walther@59906:   val check_for : term * term -> term * (term * term) list ->
walther@59906:     (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T ->
walther@59906:       Error_Fill_Def.errpatID option
walther@59906: 
wneuper@59310: (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
wneuper@59310:   (*  NONE *)
walther@59886: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
walther@59863:   val check_err_patt : term * term -> UnparseC.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
wneuper@59262:   val get_fillform :
walther@59858:      'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
wneuper@59262:   val get_fillpats :
walther@59858:      'a * (term * term) list -> term -> Error_Fill_Def.errpatID -> thm -> (Error_Fill_Def.fillpatID * term * thm * 'a) list
walther@59886: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
wneuper@59310: 
wneuper@59262: end
walther@59822: (**)
walther@59858: structure Error_Fill_Pattern(**): ERROR_FILL_PATTERN(**) =
walther@59822: struct
walther@59822: (**)
neuper@37906: 
walther@59858: type errpatID = Rule_Def.errpatID
walther@59858: 
walther@59822: 
neuper@42428: (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
wneuper@59405: fun check_err_patt (res, inf) subst (errpatID, pat) rls =
neuper@42423:   let 
neuper@42423:     val (res', _, _, rewritten) =
walther@59857:       Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
neuper@42423:   in
walther@59848:     if rewritten then 
neuper@42423:       let
walther@59854:         val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls  res' of
neuper@42423:           NONE => res'
neuper@42423:         | SOME (norm_res, _) => norm_res
walther@59854:         val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of
neuper@42423:           NONE => inf
neuper@42423:         | SOME (norm_inf, _) => norm_inf
neuper@42423:       in if norm_res = norm_inf then SOME errpatID 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
wneuper@59263:     val (_, subst) = Rtools.get_bdv_subst prog env
neuper@42428:     fun scan (_, [], _) = NONE
neuper@42428:       | scan (errpatID, errpat :: errpats, _) =
wneuper@59405:           case check_err_patt (res, inf) subst (errpatID, errpat) rls of
neuper@42428:             NONE => scan (errpatID, errpats, [])
neuper@42428:           | SOME errpatID => SOME errpatID
neuper@42428:     fun scans [] = NONE
neuper@42428:       | scans (group :: groups) =
neuper@42428:           case scan group of
neuper@42428:             NONE => scans groups
neuper@42428:           | SOME errpatID => SOME errpatID
neuper@42428:   in scans errpats end;
neuper@42428: 
neuper@42433: (* fill-in patterns an forms.
neuper@42433:   returns thm required by "fun in_fillform *)
wneuper@59405: fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
neuper@42430:   let
neuper@42430:     val (form', _, _, rewritten) =
walther@59857:       Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
neuper@42430:   in (*the fillpat of the thm must be dedicated to errpatID*)
walther@59848:     if errpatID = 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: 
neuper@42430: fun get_fillpats subst form errpatID thm =
wneuper@59264:   let
wneuper@59264:     val thmDeriv = Thm.get_name_hint thm
wneuper@59264:     val (part, thyID) = Rtools.thy_containing_thm thmDeriv
walther@59876:     val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
wneuper@59269:     val fillpats = case Specify.get_the theID of
walther@59898:       Thy_Html.Hthm {fillpats, ...} => fillpats
wneuper@59264:     | _ => error "get_fillpats: uncovered case of get_the"
wneuper@59264:     val some = map (get_fillform subst (thm, form) errpatID) fillpats
wneuper@59264:   in some |> filter is_some |> map the end
neuper@42430: 
walther@59846: fun find_fillpatterns (pt, pos as (p, _): Pos.pos') errpatID =
neuper@42430:   let 
wneuper@59276:     val f_curr = Ctree.get_curr_formula (pt, pos);
wneuper@59276:     val pp = Ctree.par_pblobj pt p
wneuper@59276:     val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
wneuper@59416:       {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
wneuper@59264:     | _ => error "find_fillpatterns: uncovered case of get_met"
walther@59807:     val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
wneuper@59263:     val subst = Rtools.get_bdv_subst prog env
neuper@42430:     val errpatthms = errpats
walther@59858:       |> filter ((curry op = errpatID) o (#1: Error_Fill_Def.errpat -> Error_Fill_Def.errpatID))
walther@59858:       |> map (#3: Error_Fill_Def.errpat -> thm list)
neuper@42430:       |> flat
wneuper@59264:   in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
neuper@37906: 
walther@59906: (* check if an input formula is exactly equal to the rewrite from a rule
neuper@42437:    which is stored at the pos where the input is stored of "ok". *)
neuper@42437: fun is_exactly_equal (pt, pos as (p, _)) istr =
walther@59881:   case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) 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 
wneuper@59272:         case Applicable.applicable_in pos pt tac of
walther@59735:           Applicable.Notappl msg => (msg, Tactic.Tac "")
walther@59735:         | Applicable.Appl 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@59728:               | t => error ("is_exactly_equal: 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 *)
neuper@42458: fun fetchErrorpatterns 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"
wneuper@59592:     val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
wneuper@59269:     val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
walther@59898:       Thy_Html.Hrls {thy_rls = (_, rls), ...} => rls
wneuper@59264:     | _ => error "fetchErrorpatterns: 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: type errpatID = Rule_Def.errpatID
walther@59858: type errpat =
walther@59858:   errpatID    (* one identifier for a list of patterns                       
walther@59858:                  DESIGN ?TODO: errpatID list for hierarchy of errpats ?      *)
walther@59858:   * term list (* error patterns                                              *)
walther@59858:   * thm list  (* thms related to error patterns; note that respective lhs 
walther@59858:                  do not match (which reflects student's error).
walther@59858:                  fillpatterns are stored with these thms.                    *)
walther@59858: fun errpat2str (id, tms, thms) =
walther@59875:   "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC.string_of_thms thms
walther@59858: fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
walther@59858: 
walther@59858: (**)end(**)