(* Title:  Specify/model.sml

   Author: Walther Neuper 110226

   (c) due to copyright terms

Operations on models.

*)

signature MODEL_MATCH =

sig

  datatype T = (* ------------vvvvvvvvv--- adapt to PIDE *)

      Matches of Problem.id * P_Model.T

    | NoMatch of Problem.id * P_Model.T  

  val matchs2str : T list -> string

(*/------- rename: TODO 220917 review -------\*)

(*val o_model: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool*)

  val match_oris: Proof.context -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool

(*unify                     ^^^^^^^^^^                                  vvvvvvvvvv 

                             vvvvvvvvv    ^^^^^^^^^*)

(*val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->

    bool * (I_Model.T * Pre_Conds.T)*)

  val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list(*Pre_Cond.unchecked*) * Rule_Set.T ->

    bool * (I_Model.T * Pre_Conds.T)    (*^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v--- type*)

(*val o_i_model: O_Model.T * I_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> theory ->

    bool * (I_Model.T * Pre_Conds.T)             (*?values--^^^^^^^^^?*)*)

  val match_itms_oris: theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->

    O_Model.T -> bool * (I_Model.T * Pre_Conds.T)

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

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

(*val arguments_msg: Problem.id -> term -> term list -> unit*)

  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 match_pbl : Formalise.model -> Problem.T -> match'

\<^isac_test>\<open>

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

  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 field_eq f (_, _, f', _, _) = f = f';

fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';

fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;

fun eq1 d (_, (d', _)) = (d = d');

fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts));

(* check an ori for matching a problemtype by description; 

   returns true only for itms found in pbt              *)

fun chk1_ pbt (i, vats, f, d, vs) =

  case find_first (eq1 d) pbt of 

	  SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))]

  | NONE => [];

(* elem 'p' of pbt contained in itms ? *)

fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;

fun chk1_m' oris (p as (f, (d, t))) = 

  case find_first (eq2' p) oris of

	  SOME _ => []

  | NONE => [(f, I_Model.Mis (d, t))];

fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);

fun chk1_mis _(*mvat*) itms model = foldl and_ (true, map (chk1_m itms) model);

fun chk1_mis' oris model = map pair0vatsfalse ((flat o (map (chk1_m' oris))) model);

(* check a problem (ie. ori list) for matching a problemtype, 

   takes the I_Model.variables for concluding completeness (FIXME could be another!) *)

fun match_oris ctxt where_rls oris (pbt,where_) = 

  let

    val itms = (flat o (map (chk1_ pbt))) oris;

    val mvat = I_Model.variables itms;

    val complete = chk1_mis mvat itms pbt;

    val (pb, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_ itms mvat;

  in if complete andalso pb then true else false end;

(* check a problem (ie. ori list) for matching a problemtype, 

   returns items for output to math-experts *)

fun match_oris' thy oris (model, where_, where_rls) =

  let

    val itms = (flat o (map (chk1_ model))) oris;

    val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;

    val mvat = I_Model.variables itms;

    val miss = chk1_mis' oris model;

    val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms mvat;

  in (miss = [] andalso pb, (itms @ miss @ sups, where_')) end;

(** check a problem (ie. itm list) for matching a problemtype **)

(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,

   for missing items get data from formalization (ie. ori list); 

   takes the I_Model.variables for concluding completeness (could be another!)

  (0) determine the most frequent variant mv in pbl

   ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>

            (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;

            (3) newitms = filter (mv mem vat(news)) news 

   (4) pbt @ newitms                                           *)

fun match_itms_oris ctxt pbl (pbt, where_, where_rls) oris =

  let 

 (*0*)val mv = I_Model.max_variant pbl;

      fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;

      fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of

				SOME _ => false | NONE => true;

 (*1*)val mis = (filter (notmem pbl)) pbt;

      fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';

      fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));

 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;

      val news = (flat o (map (oris2itms oris))) mis;

 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;

      val newitms = filter mem_vat news;

 (*4*)val itms' = pbl @ newitms;

      val (pb, where_') = Pre_Conds.check ctxt where_rls where_ itms' mv;

  in (length mis = 0 andalso pb, (itms', where_')) 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 match_pbl fmz ({thy = thy, where_ = where_, model, where_rls = er, ...}: Problem.T) =

  let

    val oris = O_Model.init thy fmz model(* |> #1*);

    val (bool, (itms, where_')) = match_oris' thy oris (model, where_, er);

  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_in_ctxt ctxt dsc ^ " " ^ UnparseC.term_in_ctxt 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_in_ctxt 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 _ pbt [] _ =

    (tracing (dashs 70);

     raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string 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 pats ^ "\n"

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

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

       ^ dashs 70)

  in tracing msg end

(**)end(**)