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

   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_FILL_PATTERN =

sig

  type errpatID = Rule_Def.errpatID

  type errpat = errpatID * term list * thm list

  val errpats2str : errpat list -> string

  val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID ->

    (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list

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

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

(*/------- to ThmC -------\*)

  val rule2thm'' : Rule.rule -> ThmC.T

  val rule2rls' : Rule.rule -> string

(*\------- to ThmC -------/*)

(*/------- to LItool -------\*)

  val mk_tacis: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->

    Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))

  val check_for : term * term -> term * (term * term) list ->

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

      Error_Fill_Def.errpatID option

(*\------- to LItool -------/*)

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

  (*  NONE *)

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

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

  val get_fillform :

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

  val get_fillpats :

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

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

end

(**)

structure Error_Fill_Pattern(**): ERROR_FILL_PATTERN(**) =

struct

(**)

type errpatID = Rule_Def.errpatID

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

  | rule2thm'' r = raise ERROR ("rule2thm': not defined for " ^ Rule.to_string r);

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

  | rule2rls' r = raise ERROR ("rule2rls': not defined for " ^ Rule.to_string r);

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.to_string r ^ " at " ^ UnparseC.term t)

(*** 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 Rewrite_Ord.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 Rewrite_Ord.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", ThmC.cut_id thmDeriv]

    val fillpats = case Specify.get_the theID of

      Thy_Html.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: Error_Fill_Def.errpat -> Error_Fill_Def.errpatID))

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

      |> flat

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

(* check if an input formula is exactly equal to 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 (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) 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

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

    | _ => error "fetchErrorpatterns: 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

type errpatID = Rule_Def.errpatID

type errpat =

  errpatID    (* one identifier for a list of patterns                       

                 DESIGN ?TODO: errpatID list for hierarchy of errpats ?      *)

  * term list (* error patterns                                              *)

  * thm list  (* thms related to error patterns; note that respective lhs 

                 do not match (which reflects student's error).

                 fillpatterns are stored with these thms.                    *)

fun errpat2str (id, tms, thms) =

  "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC.string_of_thms thms

fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats

(**)end(**)