(* Title:  Specify/m-match.sml

   Author: Walther Neuper 110226

   (c) due to copyright terms

Operations on models.

*)

signature MODEL_MATCH =

sig

  datatype T =

      Matches of Problem.id * P_Model.T

    | NoMatch of Problem.id * P_Model.T  

  val matchs2str : T list -> string

  val data_by_o: Proof.context -> O_Model.T ->

    Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set ->

      bool * (I_Model.T * Pre_Conds.T)

  val by_o_model: Proof.context -> O_Model.T ->

    Model_Pattern.single list * Pre_Conds.unchecked * Rule_Def.rule_set -> bool

  val by_i_model: Proof.context -> I_Model.T ->

    Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set -> bool * Pre_Conds.T

  val by_i_models: Proof.context -> O_Model.T -> I_Model.T * I_Model.T ->

    Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set ->

      bool * (I_Model.T * Pre_Conds.T)

  val arguments: theory -> Model_Pattern.T -> term list -> O_Model.T

  val arguments_msg: Problem.id -> term -> term list -> unit

  datatype match' =  (* constructors for tests only *)

    Matches' of P_Model.T | NoMatch' of P_Model.T

  val by_formalise : Formalise.model -> Problem.T -> match'

(*from isac_test for Minisubpbl*)

  val contains_o: Model_Def.descriptor -> O_Model.T -> bool

\<^isac_test>\<open>

  val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T

\<close>

(*\------- rename -------/*)

end

(**)

structure M_Match(** ) : MODEL_MATCH( **) =

struct

(**)

datatype T = 

  Matches of Problem.id *  P_Model.T

| NoMatch of Problem.id *  P_Model.T;

fun match2str (Matches (pI, model)) = "Matches (" ^ strs2str pI ^ ", " ^  P_Model.to_string model ^ ")"

  | match2str (NoMatch (pI, model)) = "NoMatch (" ^ strs2str pI ^ ", " ^  P_Model.to_string model ^ ")";

fun matchs2str ms = (strs2str o (map match2str)) ms;

fun contains_o descr o_model =

  case find_first (fn (_, _, _, descr', _) => descr' = descr) o_model of

     SOME _ => true | NONE => false

fun data_by_o ctxt o_model (model_patt, where_, where_rls) =

  let

    val o_model_vnt = o_model

      |> map (fn o_single as (_, variants, _, _, _)

        => if member_swap op = 1 (*variant 1 is mandatory*) variants then [o_single] else [])

      |> flat

    val is_complete = model_patt

      |> map (fn (_, (descr, _)) => contains_o descr o_model_vnt) 

      |> curry (foldl and_) true

    val i_model = (*in order to match sig of Pre_Conds.check*)

      map (fn (a, b, c, d, e) => (a, b, true, c, (I_Model.Cor (d, e), Position.none))) o_model_vnt

    val (pre_conds_check, pre_conds) = Pre_Conds.check ctxt where_rls where_ (model_patt, i_model)

  in

    (is_complete andalso pre_conds_check, (i_model, pre_conds))

  end

fun by_o_model ctxt o_model (model_patt, where_, where_rls) = 

  (data_by_o ctxt o_model (model_patt, where_, where_rls)) |> #1

fun by_i_models ctxt o_model (pbl_imod, met_imod) (met_patt, where_, where_rls) =

  let

    val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt

    val (check, preconds) = Pre_Conds.check ctxt where_rls where_ (met_patt, met_imod)

  in    

   (check, (met_imod, preconds))

  end

(*contains_i: descriptor -> I_Model.T -> bool*)

fun contains_i descr i_model =

  case find_first (fn (_, _, _, _, (feedb, _)) => Model_Def.get_descr feedb = descr) i_model of

     SOME _ => true | NONE => false

fun by_i_model ctxt i_model (model_patt, where_, where_rls) =

  let

    val max_vnt = last_elem (Model_Def.max_variants'' i_model)

    val i_model_vnt = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) i_model

    val is_complete = model_patt

      |> map (fn (_, (descr, _)) => contains_i descr i_model_vnt)

      |> curry (foldl and_) true

    val (env_model, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model_vnt;

    val (prec_check, precs)

      = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))

  in

    (is_complete andalso prec_check, precs)

  end

(** for use by math-authors **)

datatype match' = (* for the user *)

  Matches' of P_Model.T

| NoMatch' of P_Model.T;

(* match a formalization with a problem type, for tests *)

fun by_formalise fmz ({thy, where_, model, where_rls, ...}: Problem.T) =

  let

    val ctxt = Proof_Context.init_global thy

    val (oris, _) = O_Model.init thy fmz model

    val (bool, (itms, where_')) = data_by_o ctxt oris (model, where_, where_rls);

  in

    if bool

    then Matches' (P_Model.from thy itms where_')

    else NoMatch' (P_Model.from thy itms where_')

  end;

(* split type-wrapper from program-arg and build part of an ori;

   an type-error is reported immediately, raises an exn, 

   subsequent handling of exn provides 2nd part of error message *)

fun mtc thy (str, (dsc, _)) (ty $ var) =

    let val ctxt = Proof_Context.init_global thy

    in

    ((Thm.global_cterm_of thy (dsc $ var);(*type check*)

      SOME (([1], str, dsc, (*[var]*)

	    Input_Descript.split' (dsc, var))) (*:ori without leading #*))

      handle e as TYPE _ => 

	      (tracing (dashs 70 ^ "\n"

	        ^ "*** ERROR while creating the items for the model of the ->problem\n"

	        ^ "*** from the ->stac with ->typeconstructor in arglist:\n"

	        ^ "*** item (->description ->value): " ^ UnparseC.term ctxt dsc ^ " " ^ UnparseC.term ctxt var ^ "\n"

	        ^ "*** description: " ^ TermC.string_of_detail ctxt dsc

	        ^ "*** value: " ^ TermC.string_of_detail ctxt var

	        ^ "*** typeconstructor in script: " ^ TermC.string_of_detail ctxt ty

	        ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"

	        ^ "*** " ^ dots 66);

          writeln (@{make_string} e);

          Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)

      NONE))

    end

  | mtc thy _ t =

    let val ctxt = Proof_Context.init_global thy

    in raise ERROR ("mtc: uncovered case with" ^ UnparseC.term ctxt t) end

(* match each pat of the model-pattern with an actual argument;

   precondition: copy-named vars are filtered out            *)

fun matc _ [] _ oris = oris

  | matc thy pbt [] _ =

    (tracing (dashs 70);

     raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string

       (Proof_Context.init_global thy) pbt ^ "' i.e. should be 'copy-named' by '*_._'"))

  | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =

    (*del?..*)if (O_Model.is_copy_named' o TermC.free2str) t then oris

    else(*..del?*)

      let val opt = mtc thy p a

      in

        case opt of

          SOME ori => matc thy pbt ags (oris @ [ori])

	      | NONE => [](*WN050903 skipped by exn handled in arguments*)

	 end

(* match the actual arguments of a SubProblem with a model-pattern

   and create an O_Model (in root-pbl created from Formalise.model).

   expects ags:pats = 1:1, while copy-named are filtered out of pats;

   if no 1:1 then exn raised by matc/mtc and handled at call.

   copy-named pats are appended in order to get them into the Model-items *)

fun arguments thy pbt ags =

  let

    fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)

    val pbt' = filter_out O_Model.is_copy_named pbt

    val cy = filter O_Model.is_copy_named pbt  (* cy is NOT a (formal) argument, but the fun's result *)

    val oris' = matc thy pbt' ags []

    val cy' = map (O_Model.copy_name pbt' oris') cy

    val ors = O_Model.add_enumerate (oris' @ cy') (*...appended in order to get into the Model-items *)

  in (map flattup ors) end

(* report part of the error-msg which is not available in match_args *)

fun arguments_msg ctxt pI stac ags =

  let

    val pats = (#model o Problem.from_store ctxt) pI

    val msg = (dots 70 ^ "\n"

       ^ "*** problem " ^ strs2str pI ^ " has the ...\n"

       ^ "*** model-pattern " ^ Model_Pattern.to_string ctxt pats ^ "\n"

       ^ "*** stac   '" ^ UnparseC.term ctxt stac ^ "' has the ...\n"

       ^ "*** arg-list " ^ UnparseC.terms ctxt ags ^ "\n"

       ^ dashs 70)

  in tracing msg end

(**)end(**)