(* 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_ins" 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 : Proof.context -> 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

  val from_store: Proof.context -> Tactic.input -> 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 get_fill_ins: theory -> fill_in_id -> fill_in list

  val store_fill_ins: (fill_in_id * fill_in list) list -> theory -> theory

  type record

(*val find_fill_ins: Calc.T -> id -> record list*)

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

(*from isac_test for Minisubpbl*)

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

    record list

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

    record option

\<^isac_test>\<open>

  val get_fill_inss: theory -> (fill_in_id * fill_in list) list

  val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id 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", [ParseC.patt_opt @{theory} "?a = ?b" |> the], [@{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", ParseC.patt_opt @{theory} "?a = _" |> the, "e_errpatID")

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

structure Data = Theory_Data (

  type T = (fill_in_id * fill_in list) list;

  val empty = [];

  val merge = merge op=;

  );                                                              

fun get_fill_inss thy = Data.get thy

fun store_fill_ins fill_in = Data.map (curry (Library.merge op=) fill_in)

fun get_fill_ins thy fill_in_id =

  case AList.lookup (op =) (get_fill_inss thy) fill_in_id of

    SOME fill_ins => fill_ins

  | NONE => raise ERROR ("fill_ins for thm \"" ^ fill_in_id ^ "\" missing in theory \"" ^ 

    (thy |> ThyC.id_of) ^ "\" (and ancestors)" ^

    "\nTODO exception hierarchy needs to be established.")

(*

  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 ctxt 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 ctxt (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =

  let

    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 ctxt subst form errpat_id thm =

  let

    val thm_id_long = Thm.get_name_hint thm

    val thm_id = ThmC.cut_longid thm_id_long

    val fill_ins = get_fill_ins (Proof_Context.theory_of ctxt) thm_id;

    val some = map (fill_form ctxt subst (thm, form) errpat_id) fill_ins;

  in some |> filter is_some |> map the end

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

  let 

    val ctxt = Ctree.get_ctxt pt pos

    val f_curr = Ctree.get_curr_formula (pt, pos)

    val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)

    val (errpats, prog) = (* after shift to Diff.thy -------vvvvvvvvvvvvvvv ctxt should be sufficient*)

      case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of

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

      | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"

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

    val subst = Subst.for_bdv ctxt prog env

    val errpat_thms = 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 (Ctree.get_ctxt pt pos) subst f_curr id) errpat_thms |> 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".

*)

(*will come directly from PIDE --------vvvvvvvvvvv*)

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

  let

    val ctxt = (Ctree.get_ctxt pt pos)

    val ifo = Syntax.read_term ctxt istr

      handle ERROR msg => error (msg (*^ Position.here pp*))

    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 ctxt 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 ctxt tac =

  let

    val rls_id =

      case tac of

       Tactic.Rewrite_Set rls_id => rls_id

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

      | _ => "empty"

  in case get_rls ctxt rls_id of

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

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

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

  | Rule_Set.Empty => []

  end

(**)end(**)