1.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue May 05 13:33:23 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue May 05 15:39:20 2020 +0200
1.3 @@ -33,7 +33,7 @@
1.4 type pblRD = string list (* for pbl-met-hierarchy.sml *)
1.5 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
1.6 val scan : string list -> 'a Store.T -> string list list (* for thy-hierarchy.sml *)
1.7 - val itm_out : theory -> Model.itm_ -> string
1.8 + val itm_out : theory -> I_Model.feedback -> string
1.9 val dsc_unknown : term
1.10
1.11 (*/------- from Celem to Specify -------\*)
1.12 @@ -93,11 +93,11 @@
1.13 fun hack_until_review_Specify_1 metID itms =
1.14 if metID = ["Biegelinien", "ausBelastung"]
1.15 then itms @
1.16 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
1.17 + [(4, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
1.18 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1.19 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1.20 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
1.21 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
1.22 + (5, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
1.23 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1.24 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1.25 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
1.26 @@ -105,11 +105,11 @@
1.27 fun hack_until_review_Specify_2 metID itms =
1.28 if metID = ["IntegrierenUndKonstanteBestimmen2"]
1.29 then itms @
1.30 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
1.31 + [(4, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
1.32 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1.33 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1.34 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
1.35 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
1.36 + (5, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
1.37 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1.38 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1.39 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
1.40 @@ -151,12 +151,12 @@
1.41 type field = string * (term * term)
1.42 val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
1.43
1.44 -fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (I_Model.comp_dts (d, ts)))
1.45 - | itm_2item _ (Model.Syn c) = Model.SyntaxE c
1.46 - | itm_2item _ (Model.Typ c) = Model.TypeE c
1.47 - | itm_2item _ (Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (I_Model.comp_dts (d, ts)))
1.48 - | itm_2item _ (Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (I_Model.comp_dts (d, ts)))
1.49 - | itm_2item _ (Model.Mis (d, pid)) = Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)
1.50 +fun itm_2item (_: theory) (I_Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (I_Model.comp_dts (d, ts)))
1.51 + | itm_2item _ (I_Model.Syn c) = Model.SyntaxE c
1.52 + | itm_2item _ (I_Model.Typ c) = Model.TypeE c
1.53 + | itm_2item _ (I_Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (I_Model.comp_dts (d, ts)))
1.54 + | itm_2item _ (I_Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (I_Model.comp_dts (d, ts)))
1.55 + | itm_2item _ (I_Model.Mis (d, pid)) = Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)
1.56 | itm_2item _ _ = error "itm_2item: uncovered definition"
1.57
1.58 fun mappc f {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} =
1.59 @@ -184,12 +184,12 @@
1.60 in (hd, arg) end
1.61
1.62 (*create output-string for itm_*)
1.63 -fun itm_out _ (Model.Cor ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
1.64 - | itm_out _ (Model.Syn c) = c
1.65 - | itm_out _ (Model.Typ c) = c
1.66 - | itm_out _ (Model.Inc ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
1.67 - | itm_out _ (Model.Sup (d, ts)) = UnparseC.term (I_Model.comp_dts (d, ts))
1.68 - | itm_out _ (Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
1.69 +fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
1.70 + | itm_out _ (I_Model.Syn c) = c
1.71 + | itm_out _ (I_Model.Typ c) = c
1.72 + | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
1.73 + | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (I_Model.comp_dts (d, ts))
1.74 + | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
1.75 | itm_out _ _ = error "itm_out: uncovered definition"
1.76
1.77 fun boolterm2item (true, term) = Model.Correct (UnparseC.term term)
1.78 @@ -447,34 +447,34 @@
1.79 (** check a problem (ie. itm list) for matching a problemtype **)
1.80
1.81 fun eq1 d (_, (d', _)) = (d = d');
1.82 -fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", Model.Sup (d, ts));
1.83 +fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts));
1.84 (*see + add_sel_ppc ~~~~~~~*)
1.85
1.86 fun field_eq f (_, _, f', _, _) = f = f';
1.87
1.88 (* check an item (with arbitrary itm_ from previous matchings)
1.89 for matching a problemtype; returns true only for itms found in pbt *)
1.90 -fun chk_ (_: theory) pbt (i, vats, b, f, Model.Cor ((d, vs), _)) =
1.91 +fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
1.92 (case find_first (eq1 d) pbt of
1.93 - SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
1.94 - | NONE => (i, vats, false, f, Model.Sup (d, vs)))
1.95 - | chk_ _ pbt (i, vats, b, f, Model.Inc ((d, vs), _)) =
1.96 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
1.97 + | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
1.98 + | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
1.99 (case find_first (eq1 d) pbt of
1.100 - SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
1.101 - | NONE => (i, vats, false, f, Model.Sup (d, vs)))
1.102 - | chk_ _ _ (itm as (_, _, _, _, Model.Syn _)) = itm
1.103 - | chk_ _ _ (itm as (_, _, _, _, Model.Typ _)) = itm
1.104 - | chk_ _ pbt (i, vats, b, f, Model.Sup (d, vs)) =
1.105 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
1.106 + | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
1.107 + | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
1.108 + | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
1.109 + | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
1.110 (case find_first (eq1 d) pbt of
1.111 - SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d,vs), (id, Model.pbl_ids' d vs)))
1.112 - | NONE => (i, vats, false, f, Model.Sup (d, vs)))
1.113 - | chk_ _ pbt (i, vats, _, f, Model.Mis (d, vs)) =
1.114 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, Model.pbl_ids' d vs)))
1.115 + | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
1.116 + | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
1.117 (case find_first (eq1 d) pbt of
1.118 - SOME (_, _) => error "chk_: ((i,vats,b,f,Model.Cor ((d,vs),(id, Model.pbl_ids' d vs))):itm)"
1.119 - | NONE => (i, vats, false, f, Model.Sup (d, [vs])))
1.120 + SOME (_, _) => error "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Model.pbl_ids' d vs))):itm)"
1.121 + | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
1.122 | chk_ _ _ _ = error "chk_: uncovered fun def.";
1.123
1.124 -fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = Model.d_in itm_;
1.125 +fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
1.126 fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
1.127 fun eq0 (0, _, _, _, _) = true
1.128 | eq0 _ = false;
1.129 @@ -495,7 +495,7 @@
1.130 | NONE =>
1.131 (case find_first (eq2 p) untouched of
1.132 SOME itm => [itm]
1.133 - | NONE => [(0, [], false, f, Model.Mis (d, id))]);
1.134 + | NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
1.135
1.136 fun chk_mis mvat itms untouched pbt =
1.137 let val mis = (flat o (map (chk_m itms untouched))) pbt;
1.138 @@ -503,12 +503,12 @@
1.139 in add_idvat [] (mid + 1) mvat mis end;
1.140
1.141 (* check a problem (ie. itm list) for matching a problemtype,
1.142 - takes the Model.max_vt for concluding completeness (could be another!) *)
1.143 + takes the I_Model.max_vt for concluding completeness (could be another!) *)
1.144 fun match_itms thy itms (pbt, pre, prls) =
1.145 let
1.146 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
1.147 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
1.148 - val mvat = Model.max_vt itms';
1.149 + val mvat = I_Model.max_vt itms';
1.150 val itms'' = filter (okv mvat) itms';
1.151 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
1.152 val mis = chk_mis mvat itms'' untouched pbt;
1.153 @@ -518,7 +518,7 @@
1.154
1.155 (* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
1.156 for missing items get data from formalization (ie. ori list);
1.157 - takes the Model.max_vt for concluding completeness (could be another!)
1.158 + takes the I_Model.vars_of for concluding completeness (could be another!)
1.159
1.160 (0) determine the most frequent variant mv in pbl
1.161 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
1.162 @@ -527,15 +527,15 @@
1.163 (4) pbt @ newitms *)
1.164 fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
1.165 let
1.166 - (*0*)val mv = Model.max_vt pbl;
1.167 + (*0*)val mv = I_Model.max_vt pbl;
1.168
1.169 - fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = Model.d_in itm_;
1.170 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
1.171 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
1.172 SOME _ => false | NONE => true;
1.173 (*1*)val mis = (filter (notmem pbl)) pbt;
1.174
1.175 fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
1.176 - fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, Model.Mis (d, pid));
1.177 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
1.178 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
1.179 val news = (flat o (map (oris2itms oris))) mis;
1.180 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
1.181 @@ -552,7 +552,7 @@
1.182 returns true only for itms found in pbt *)
1.183 fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
1.184 case find_first (eq1 d) pbt of
1.185 - SOME (_, (_, id)) => [(i, vats, true, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))]
1.186 + SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))]
1.187 | NONE => [];
1.188
1.189 (* elem 'p' of pbt contained in itms ? *)
1.190 @@ -560,18 +560,18 @@
1.191 fun chk1_m' oris (p as (f, (d, t))) =
1.192 case find_first (eq2' p) oris of
1.193 SOME _ => []
1.194 - | NONE => [(f, Model.Mis (d, t))];
1.195 + | NONE => [(f, I_Model.Mis (d, t))];
1.196 fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
1.197
1.198 fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
1.199 fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
1.200
1.201 (* check a problem (ie. ori list) for matching a problemtype,
1.202 - takes the Model.max_vt for concluding completeness (FIXME could be another!) *)
1.203 + takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *)
1.204 fun match_oris thy prls oris (pbt,pre) =
1.205 let
1.206 val itms = (flat o (map (chk1_ thy pbt))) oris;
1.207 - val mvat = Model.max_vt itms;
1.208 + val mvat = I_Model.vars_of itms;
1.209 val complete = chk1_mis mvat itms pbt;
1.210 val pre' = Stool.check_preconds' prls pre itms mvat;
1.211 val pb = foldl and_ (true, map fst pre');
1.212 @@ -583,7 +583,7 @@
1.213 let
1.214 val itms = (flat o (map (chk1_ thy ppc))) oris;
1.215 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
1.216 - val mvat = Model.max_vt itms;
1.217 + val mvat = I_Model.vars_of itms;
1.218 val miss = chk1_mis' oris ppc;
1.219 val pre' = Stool.check_preconds' prls pre itms mvat;
1.220 val pb = foldl and_ (true, map fst pre');