1.1 --- a/src/Tools/isac/Specify/model.sml Fri May 15 11:46:43 2020 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,143 +0,0 @@
1.4 -(* Title: Specify/model.sml
1.5 - Author: Walther Neuper 110226
1.6 - (c) due to copyright terms
1.7 -
1.8 -Operations on models.
1.9 -*)
1.10 -
1.11 -signature MODEL =
1.12 -sig
1.13 - datatype match =
1.14 - Matches of Problem.id * P_Model.T
1.15 - | NoMatch of Problem.id * P_Model.T
1.16 - val matchs2str : match list -> string
1.17 -
1.18 - val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool
1.19 -(*unify ^^^^^^^^^^ vvvvvvvvvv
1.20 - vvvvvvvvv ^^^^^^^^^*)
1.21 - val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
1.22 - bool * (I_Model.T * Pre_Conds.T)
1.23 - val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
1.24 - O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
1.25 -
1.26 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
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 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.30 - (*NONE*)
1.31 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.32 -end
1.33 -
1.34 -(**)
1.35 -structure Model(** ) : MODEL( **) =
1.36 -struct
1.37 -(**)
1.38 -
1.39 -datatype match =
1.40 - Matches of Problem.id * P_Model.T
1.41 -| NoMatch of Problem.id * P_Model.T;
1.42 -fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")"
1.43 - | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")";
1.44 -fun matchs2str ms = (strs2str o (map match2str)) ms;
1.45 -
1.46 -
1.47 -fun field_eq f (_, _, f', _, _) = f = f';
1.48 -
1.49 -fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
1.50 -fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
1.51 -fun eq1 d (_, (d', _)) = (d = d');
1.52 -
1.53 -fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts));
1.54 -
1.55 -(* check an ori for matching a problemtype by description;
1.56 - returns true only for itms found in pbt *)
1.57 -fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
1.58 - case find_first (eq1 d) pbt of
1.59 - SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))]
1.60 - | NONE => [];
1.61 -
1.62 -(* elem 'p' of pbt contained in itms ? *)
1.63 -fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;
1.64 -fun chk1_m' oris (p as (f, (d, t))) =
1.65 - case find_first (eq2' p) oris of
1.66 - SOME _ => []
1.67 - | NONE => [(f, I_Model.Mis (d, t))];
1.68 -fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
1.69 -
1.70 -fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
1.71 -fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
1.72 -
1.73 -(* check a problem (ie. ori list) for matching a problemtype,
1.74 - takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *)
1.75 -fun match_oris thy prls oris (pbt,pre) =
1.76 - let
1.77 - val itms = (flat o (map (chk1_ thy pbt))) oris;
1.78 - val mvat = I_Model.vars_of itms;
1.79 - val complete = chk1_mis mvat itms pbt;
1.80 - val pre' = Pre_Conds.check prls pre itms mvat;
1.81 - val pb = foldl and_ (true, map fst pre');
1.82 - in if complete andalso pb then true else false end;
1.83 -
1.84 -(* check a problem (ie. ori list) for matching a problemtype,
1.85 - returns items for output to math-experts *)
1.86 -fun match_oris' thy oris (ppc, pre, prls) =
1.87 - let
1.88 - val itms = (flat o (map (chk1_ thy ppc))) oris;
1.89 - val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
1.90 - val mvat = I_Model.vars_of itms;
1.91 - val miss = chk1_mis' oris ppc;
1.92 - val pre' = Pre_Conds.check prls pre itms mvat;
1.93 - val pb = foldl and_ (true, map fst pre');
1.94 - in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
1.95 -
1.96 -
1.97 -(** check a problem (ie. itm list) for matching a problemtype **)
1.98 -
1.99 -(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
1.100 - for missing items get data from formalization (ie. ori list);
1.101 - takes the I_Model.vars_of for concluding completeness (could be another!)
1.102 -
1.103 - (0) determine the most frequent variant mv in pbl
1.104 - ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
1.105 - (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
1.106 - (3) newitms = filter (mv mem vat(news)) news
1.107 - (4) pbt @ newitms *)
1.108 -fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
1.109 - let
1.110 - (*0*)val mv = I_Model.max_vt pbl;
1.111 -
1.112 - fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
1.113 - fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
1.114 - SOME _ => false | NONE => true;
1.115 - (*1*)val mis = (filter (notmem pbl)) pbt;
1.116 -
1.117 - fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
1.118 - fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
1.119 - (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
1.120 - val news = (flat o (map (oris2itms oris))) mis;
1.121 - (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
1.122 - val newitms = filter mem_vat news;
1.123 - (*4*)val itms' = pbl @ newitms;
1.124 - val pre' = Pre_Conds.check prls pre itms' mv;
1.125 - val pb = foldl and_ (true, map fst pre');
1.126 - in (length mis = 0 andalso pb, (itms', pre')) end;
1.127 -
1.128 -
1.129 -(** for use by math-authors **)
1.130 -
1.131 -datatype match' = (* for the user *)
1.132 - Matches' of P_Model.T
1.133 -| NoMatch' of P_Model.T;
1.134 -
1.135 -(* match a formalization with a problem type, for tests *)
1.136 -fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) =
1.137 - let
1.138 - val oris = O_Model.init fmz thy ppc(* |> #1*);
1.139 - val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
1.140 - in
1.141 - if bool
1.142 - then Matches' (P_Model.from thy itms pre')
1.143 - else NoMatch' (P_Model.from thy itms pre')
1.144 - end;
1.145 -
1.146 -(**)end(**)