1.1 --- a/src/Tools/isac/Specify/m-match.sml Sat May 16 12:40:09 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/m-match.sml Sat May 16 14:04:35 2020 +0200
1.3 @@ -7,11 +7,11 @@
1.4
1.5 signature MODEL_MATCH =
1.6 sig
1.7 +(*/------- rename -------\*)
1.8 datatype T =
1.9 Matches of Problem.id * P_Model.T
1.10 | NoMatch of Problem.id * P_Model.T
1.11 val matchs2str : T list -> string
1.12 -
1.13 val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool
1.14 (*unify ^^^^^^^^^^ vvvvvvvvvv
1.15 vvvvvvvvv ^^^^^^^^^*)
1.16 @@ -19,17 +19,23 @@
1.17 bool * (I_Model.T * Pre_Conds.T)
1.18 val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
1.19 O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
1.20 +(*\------- rename -------/*)
1.21 +
1.22 + val arguments: theory -> Model_Pattern.T -> term list -> T
1.23 + val arguments_msg: Problem.id -> term -> term list -> unit
1.24
1.25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.26 +(*/------- rename -------\*)
1.27 datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T
1.28 val match_pbl : Formalise.model -> Problem.T -> match'
1.29 +(*\------- rename -------/*)
1.30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.31 (*NONE*)
1.32 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.33 end
1.34
1.35 (**)
1.36 -structure M_Match(**) : MODEL_MATCH(**) =
1.37 +structure M_Match(** ) : MODEL_MATCH( **) =
1.38 struct
1.39 (**)
1.40
1.41 @@ -140,4 +146,70 @@
1.42 else NoMatch' (P_Model.from thy itms pre')
1.43 end;
1.44
1.45 +(* split type-wrapper from scr-arg and build part of an ori;
1.46 + an type-error is reported immediately, raises an exn,
1.47 + subsequent handling of exn provides 2nd part of error message *)
1.48 +fun mtc thy (str, (dsc, _)) (ty $ var) =
1.49 + ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
1.50 + SOME (([1], str, dsc, (*[var]*)
1.51 + Input_Descript.split' (dsc, var))) (*:ori without leading #*))
1.52 + handle e as TYPE _ =>
1.53 + (tracing (dashs 70 ^ "\n"
1.54 + ^ "*** ERROR while creating the items for the model of the ->problem\n"
1.55 + ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
1.56 + ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
1.57 + ^ "*** description: " ^ TermC.term_detail2str dsc
1.58 + ^ "*** value: " ^ TermC.term_detail2str var
1.59 + ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
1.60 + ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
1.61 + ^ "*** " ^ dots 66);
1.62 + writeln (@{make_string} e);
1.63 + Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
1.64 + NONE))
1.65 + | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)
1.66 +
1.67 +(* match each pat of the model-pattern with an actual argument;
1.68 + precondition: copy-named vars are filtered out *)
1.69 +fun matc _ [] _ oris = oris
1.70 + | matc _ pbt [] _ =
1.71 + (tracing (dashs 70);
1.72 + raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
1.73 + | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
1.74 + (*del?..*)if (O_Model.is_copy_named_idstr o TermC.free2str) t then oris
1.75 + else(*..del?*)
1.76 + let val opt = mtc thy p a
1.77 + in
1.78 + case opt of
1.79 + SOME ori => matc thy pbt ags (oris @ [ori])
1.80 + | NONE => [](*WN050903 skipped by exn handled in arguments*)
1.81 + end
1.82 +
1.83 +(* match the actual arguments of a SubProblem with a model-pattern
1.84 + and create an ori list (in root-pbl created from formalization).
1.85 + expects ags:pats = 1:1, while copy-named are filtered out of pats;
1.86 + if no 1:1 then exn raised by matc/mtc and handled at call.
1.87 + copy-named pats are appended in order to get them into the model-items *)
1.88 +fun arguments thy pbt ags =
1.89 + let
1.90 + fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
1.91 + val pbt' = filter_out O_Model.is_copy_named pbt
1.92 + val cy = filter O_Model.is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
1.93 + val oris' = matc thy pbt' ags []
1.94 + val cy' = map (O_Model.cpy_nam pbt' oris') cy
1.95 + val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
1.96 + in (map flattup ors) end
1.97 +
1.98 +(* report part of the error-msg which is not available in match_args *)
1.99 +fun arguments_msg pI stac ags =
1.100 + let
1.101 + val pats = (#ppc o Problem.from_store) pI
1.102 + val msg = (dots 70 ^ "\n"
1.103 + ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
1.104 + ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
1.105 + ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
1.106 + ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
1.107 + ^ dashs 70)
1.108 + (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
1.109 + in tracing msg end
1.110 +
1.111 (**)end(**)