walther@59960: (* Title: Specify/model.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@60010: datatype T = (* ------------vvvvvvvvv--- adapt to PIDE *) 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@60556: (*/------- rename: TODO 220917 review -------\*) Walther@60556: (*val o_model: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool*) Walther@60590: val match_oris: Proof.context -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool walther@59971: (*unify ^^^^^^^^^^ vvvvvvvvvv walther@59971: vvvvvvvvv ^^^^^^^^^*) walther@60010: (*val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> walther@60010: bool * (I_Model.T * Pre_Conds.T)*) Walther@60556: val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list(*Pre_Cond.unchecked*) * Rule_Set.T -> walther@60010: 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*) walther@60010: (*val o_i_model: O_Model.T * I_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> theory -> walther@60010: bool * (I_Model.T * Pre_Conds.T) (*?values--^^^^^^^^^?*)*) walther@60010: val match_itms_oris: theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> walther@59971: O_Model.T -> bool * (I_Model.T * Pre_Conds.T) walther@59987: walther@60010: (*val arguments: theory -> Model_Pattern.T -> term list -> O_Model.T*) walther@59996: val arguments: theory -> Model_Pattern.T -> term list -> O_Model.T walther@60010: (*val arguments_msg: Problem.id -> term -> term list -> unit*) 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@59971: val match_pbl : Formalise.model -> Problem.T -> match' wenzelm@60223: \<^isac_test>\ walther@60010: (*val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T*) 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@59968: walther@59968: fun field_eq f (_, _, f', _, _) = f = f'; walther@59968: walther@59968: fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d'; Walther@60477: fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_; walther@59968: fun eq1 d (_, (d', _)) = (d = d'); walther@59968: walther@59968: fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts)); walther@59968: walther@59968: (* check an ori for matching a problemtype by description; walther@59968: returns true only for itms found in pbt *) Walther@60590: fun chk1_ pbt (i, vats, f, d, vs) = walther@59968: case find_first (eq1 d) pbt of Walther@60478: SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))] walther@59968: | NONE => []; walther@59968: walther@59968: (* elem 'p' of pbt contained in itms ? *) walther@59968: fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false; walther@59968: fun chk1_m' oris (p as (f, (d, t))) = walther@59968: case find_first (eq2' p) oris of walther@59968: SOME _ => [] walther@59968: | NONE => [(f, I_Model.Mis (d, t))]; walther@59968: fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_); walther@59968: Walther@60585: fun chk1_mis _(*mvat*) itms model = foldl and_ (true, map (chk1_m itms) model); Walther@60585: fun chk1_mis' oris model = map pair0vatsfalse ((flat o (map (chk1_m' oris))) model); walther@59968: walther@59968: (* check a problem (ie. ori list) for matching a problemtype, Walther@60477: takes the I_Model.variables for concluding completeness (FIXME could be another!) *) Walther@60590: fun match_oris ctxt where_rls oris (pbt,where_) = walther@59968: let Walther@60590: val itms = (flat o (map (chk1_ pbt))) oris; Walther@60477: val mvat = I_Model.variables itms; walther@59968: val complete = chk1_mis mvat itms pbt; Walther@60590: val (pb, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_ itms mvat; walther@59968: in if complete andalso pb then true else false end; walther@59968: walther@59968: (* check a problem (ie. ori list) for matching a problemtype, walther@59968: returns items for output to math-experts *) Walther@60586: fun match_oris' thy oris (model, where_, where_rls) = walther@59968: let Walther@60590: val itms = (flat o (map (chk1_ model))) oris; walther@59968: val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris; Walther@60477: val mvat = I_Model.variables itms; Walther@60585: val miss = chk1_mis' oris model; Walther@60590: val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms mvat; Walther@60586: in (miss = [] andalso pb, (itms @ miss @ sups, where_')) end; walther@59968: walther@59971: walther@59971: (** check a problem (ie. itm list) for matching a problemtype **) walther@59971: walther@59971: (* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt, walther@59971: for missing items get data from formalization (ie. ori list); Walther@60477: takes the I_Model.variables for concluding completeness (could be another!) walther@59971: walther@59971: (0) determine the most frequent variant mv in pbl walther@59971: ALL pbt. (1) dsc(pbt) notmem dsc(pbls) => walther@59971: (2) filter (dsc(pbt) = dsc(oris)) oris; -> news; walther@59971: (3) newitms = filter (mv mem vat(news)) news walther@59971: (4) pbt @ newitms *) Walther@60590: fun match_itms_oris ctxt pbl (pbt, where_, where_rls) oris = walther@59971: let Walther@60477: (*0*)val mv = I_Model.max_variant pbl; walther@59971: Walther@60477: fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_; walther@59971: fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of walther@59971: SOME _ => false | NONE => true; walther@59971: (*1*)val mis = (filter (notmem pbl)) pbt; walther@59971: walther@59971: fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d'; walther@59971: fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid)); walther@59971: (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; walther@59971: val news = (flat o (map (oris2itms oris))) mis; walther@59971: (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv; walther@59971: val newitms = filter mem_vat news; walther@59971: (*4*)val itms' = pbl @ newitms; Walther@60590: val (pb, where_') = Pre_Conds.check ctxt where_rls where_ itms' mv; Walther@60586: in (length mis = 0 andalso pb, (itms', where_')) end; walther@59971: 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@60586: fun match_pbl fmz ({thy = thy, where_ = where_, model, where_rls = er, ...}: Problem.T) = walther@59971: let Walther@60585: val oris = O_Model.init thy fmz model(* |> #1*); Walther@60586: val (bool, (itms, where_')) = match_oris' thy oris (model, where_, er); walther@59971: in walther@59971: if bool Walther@60586: then Matches' (P_Model.from thy itms where_') Walther@60586: 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@60650: ^ "*** item (->description ->value): " ^ UnparseC.term_in_ctxt ctxt dsc ^ " " ^ UnparseC.term_in_ctxt 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@60650: in raise ERROR ("mtc: uncovered case with" ^ UnparseC.term_in_ctxt 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@59987: | matc _ pbt [] _ = walther@59987: (tracing (dashs 70); walther@59987: raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string 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@59987: ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n" walther@59987: ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n" walther@59987: ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n" walther@59987: ^ dashs 70) Walther@60556: in tracing msg end walther@59987: walther@59968: (**)end(**)