Walther@60760: (* Title: Specify/m-match.sml walther@59960: Author: Walther Neuper 110226 walther@59960: (c) due to copyright terms walther@59960: walther@59960: Operations on models. walther@59960: *) walther@59960: walther@59984: signature MODEL_MATCH = walther@59960: sig Walther@60768: datatype T = walther@59969: Matches of Problem.id * P_Model.T walther@59971: | NoMatch of Problem.id * P_Model.T walther@59984: val matchs2str : T list -> string Walther@60768: Walther@60768: val data_by_o: Proof.context -> O_Model.T -> Walther@60770: Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set -> Walther@60782: bool * (I_Model.T * Pre_Conds.T) Walther@60768: val by_o_model: Proof.context -> O_Model.T -> Walther@60768: Model_Pattern.single list * Pre_Conds.unchecked * Rule_Def.rule_set -> bool Walther@60782: val by_i_model: Proof.context -> I_Model.T -> Walther@60770: Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set -> bool * Pre_Conds.T Walther@60782: val by_i_models: Proof.context -> O_Model.T -> I_Model.T * I_Model.T -> Walther@60760: Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set -> Walther@60782: bool * (I_Model.T * Pre_Conds.T) walther@59987: walther@59996: val arguments: theory -> Model_Pattern.T -> term list -> O_Model.T walther@59987: val arguments_msg: Problem.id -> term -> term list -> unit walther@59968: walther@60251: datatype match' = (* constructors for tests only *) walther@60251: Matches' of P_Model.T | NoMatch' of P_Model.T Walther@60769: val by_formalise : Formalise.model -> Problem.T -> match' Walther@60729: Walther@60729: (*from isac_test for Minisubpbl*) Walther@60770: val contains_o: Model_Def.descriptor -> O_Model.T -> bool Walther@60729: wenzelm@60223: \<^isac_test>\ walther@60010: val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T wenzelm@60223: \ walther@59987: (*\------- rename -------/*) walther@59960: end walther@59960: walther@59968: (**) walther@59997: structure M_Match(** ) : MODEL_MATCH( **) = walther@59960: struct walther@59968: (**) walther@59960: walther@59984: datatype T = walther@59969: Matches of Problem.id * P_Model.T walther@59969: | NoMatch of Problem.id * P_Model.T; Walther@60585: fun match2str (Matches (pI, model)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string model ^ ")" Walther@60585: | match2str (NoMatch (pI, model)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string model ^ ")"; walther@59965: fun matchs2str ms = (strs2str o (map match2str)) ms; walther@59965: Walther@60770: fun contains_o descr o_model = Walther@60768: case find_first (fn (_, _, _, descr', _) => descr' = descr) o_model of Walther@60768: SOME _ => true | NONE => false Walther@60768: fun data_by_o ctxt o_model (model_patt, where_, where_rls) = Walther@60768: let Walther@60768: val o_model_vnt = o_model Walther@60768: |> map (fn o_single as (_, variants, _, _, _) Walther@60768: => if member_swap op = 1 (*variant 1 is mandatory*) variants then [o_single] else []) Walther@60768: |> flat Walther@60768: val is_complete = model_patt Walther@60770: |> map (fn (_, (descr, _)) => contains_o descr o_model_vnt) Walther@60768: |> curry (foldl and_) true Walther@60768: val i_model = (*in order to match sig of Pre_Conds.check*) Walther@60782: map (fn (a, b, c, d, e) => (a, b, true, c, (I_Model.Cor (d, e), Position.none))) o_model_vnt Walther@60768: val (pre_conds_check, pre_conds) = Pre_Conds.check ctxt where_rls where_ (model_patt, i_model) Walther@60768: in Walther@60768: (is_complete andalso pre_conds_check, (i_model, pre_conds)) Walther@60768: end walther@59968: Walther@60768: fun by_o_model ctxt o_model (model_patt, where_, where_rls) = Walther@60768: (data_by_o ctxt o_model (model_patt, where_, where_rls)) |> #1 walther@59968: Walther@60769: fun by_i_models ctxt o_model (pbl_imod, met_imod) (met_patt, where_, where_rls) = Walther@60760: let Walther@60760: val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt Walther@60760: val (check, preconds) = Pre_Conds.check ctxt where_rls where_ (met_patt, met_imod) Walther@60760: in Walther@60760: (check, (met_imod, preconds)) Walther@60760: end walther@59971: Walther@60782: (*contains_i: descriptor -> I_Model.T -> bool*) Walther@60770: fun contains_i descr i_model = Walther@60770: case find_first (fn (_, _, _, _, (feedb, _)) => Model_Def.get_descr feedb = descr) i_model of Walther@60770: SOME _ => true | NONE => false Walther@60770: fun by_i_model ctxt i_model (model_patt, where_, where_rls) = Walther@60770: let Walther@60770: val max_vnt = last_elem (Model_Def.max_variants'' i_model) Walther@60770: val i_model_vnt = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) i_model Walther@60770: val is_complete = model_patt Walther@60770: |> map (fn (_, (descr, _)) => contains_i descr i_model_vnt) Walther@60770: |> curry (foldl and_) true Walther@60770: Walther@60770: val (env_model, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model_vnt; Walther@60770: val (prec_check, precs) Walther@60770: = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval)) Walther@60770: in Walther@60770: (is_complete andalso prec_check, precs) Walther@60770: end Walther@60770: walther@59971: walther@59971: (** for use by math-authors **) walther@59971: walther@59971: datatype match' = (* for the user *) walther@59971: Matches' of P_Model.T walther@59971: | NoMatch' of P_Model.T; walther@59971: walther@59971: (* match a formalization with a problem type, for tests *) Walther@60769: fun by_formalise fmz ({thy, where_, model, where_rls, ...}: Problem.T) = walther@59971: let Walther@60768: val ctxt = Proof_Context.init_global thy Walther@60768: val (oris, _) = O_Model.init thy fmz model Walther@60768: val (bool, (itms, where_')) = data_by_o ctxt oris (model, where_, where_rls); walther@59971: in walther@59971: if bool Walther@60772: then Matches' (P_Model.from thy itms where_') Walther@60772: else NoMatch' (P_Model.from thy itms where_') walther@59971: end; walther@59971: Walther@60586: (* split type-wrapper from program-arg and build part of an ori; walther@59987: an type-error is reported immediately, raises an exn, walther@59987: subsequent handling of exn provides 2nd part of error message *) walther@59987: fun mtc thy (str, (dsc, _)) (ty $ var) = Walther@60650: let val ctxt = Proof_Context.init_global thy Walther@60650: in walther@59987: ((Thm.global_cterm_of thy (dsc $ var);(*type check*) walther@59987: SOME (([1], str, dsc, (*[var]*) walther@59987: Input_Descript.split' (dsc, var))) (*:ori without leading #*)) walther@59987: handle e as TYPE _ => walther@59987: (tracing (dashs 70 ^ "\n" walther@59987: ^ "*** ERROR while creating the items for the model of the ->problem\n" walther@59987: ^ "*** from the ->stac with ->typeconstructor in arglist:\n" Walther@60675: ^ "*** item (->description ->value): " ^ UnparseC.term ctxt dsc ^ " " ^ UnparseC.term ctxt var ^ "\n" Walther@60650: ^ "*** description: " ^ TermC.string_of_detail ctxt dsc Walther@60650: ^ "*** value: " ^ TermC.string_of_detail ctxt var Walther@60650: ^ "*** typeconstructor in script: " ^ TermC.string_of_detail ctxt ty walther@59987: ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n" walther@59987: ^ "*** " ^ dots 66); walther@59987: writeln (@{make_string} e); walther@59987: Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*) walther@59987: NONE)) Walther@60650: end Walther@60650: | mtc thy _ t = Walther@60650: let val ctxt = Proof_Context.init_global thy Walther@60675: in raise ERROR ("mtc: uncovered case with" ^ UnparseC.term ctxt t) end walther@59987: walther@59987: (* match each pat of the model-pattern with an actual argument; walther@59987: precondition: copy-named vars are filtered out *) walther@59987: fun matc _ [] _ oris = oris Walther@60655: | matc thy pbt [] _ = walther@59987: (tracing (dashs 70); Walther@60655: raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string Walther@60655: (Proof_Context.init_global thy) pbt ^ "' i.e. should be 'copy-named' by '*_._'")) walther@59987: | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris = Walther@60475: (*del?..*)if (O_Model.is_copy_named' o TermC.free2str) t then oris walther@59987: else(*..del?*) walther@59987: let val opt = mtc thy p a walther@59987: in walther@59987: case opt of walther@59987: SOME ori => matc thy pbt ags (oris @ [ori]) walther@59987: | NONE => [](*WN050903 skipped by exn handled in arguments*) walther@59987: end walther@59987: walther@59987: (* match the actual arguments of a SubProblem with a model-pattern Walther@60473: and create an O_Model (in root-pbl created from Formalise.model). walther@59987: expects ags:pats = 1:1, while copy-named are filtered out of pats; walther@59987: if no 1:1 then exn raised by matc/mtc and handled at call. walther@60152: copy-named pats are appended in order to get them into the Model-items *) walther@59987: fun arguments thy pbt ags = walther@59987: let walther@59987: fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_) walther@59987: val pbt' = filter_out O_Model.is_copy_named pbt walther@59987: val cy = filter O_Model.is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *) walther@59987: val oris' = matc thy pbt' ags [] Walther@60473: val cy' = map (O_Model.copy_name pbt' oris') cy Walther@60472: val ors = O_Model.add_enumerate (oris' @ cy') (*...appended in order to get into the Model-items *) walther@59987: in (map flattup ors) end walther@59987: walther@59987: (* report part of the error-msg which is not available in match_args *) Walther@60559: fun arguments_msg ctxt pI stac ags = walther@59987: let Walther@60585: val pats = (#model o Problem.from_store ctxt) pI walther@59987: val msg = (dots 70 ^ "\n" walther@59987: ^ "*** problem " ^ strs2str pI ^ " has the ...\n" Walther@60655: ^ "*** model-pattern " ^ Model_Pattern.to_string ctxt pats ^ "\n" Walther@60675: ^ "*** stac '" ^ UnparseC.term ctxt stac ^ "' has the ...\n" Walther@60675: ^ "*** arg-list " ^ UnparseC.terms ctxt ags ^ "\n" walther@59987: ^ dashs 70) Walther@60556: in tracing msg end walther@59987: walther@59968: (**)end(**)