(* 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_TEST * 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_TEST ->

     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_TEST * I_Model.T_TEST ->

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

       bool * (I_Model.T_TEST * 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 chk1_: Model_Pattern.T -> O_Model.single -> I_Model.T

   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_TEST (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_TEST -> 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 (I_Model.TEST_to_OLD itms) where_')

     else NoMatch' (P_Model.from thy (I_Model.TEST_to_OLD 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(**)