1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 05 13:33:23 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 05 15:39:20 2020 +0200
1.3 @@ -17,8 +17,8 @@
1.4 val i : int
1.5 val id2xml : int -> string list -> string
1.6 val ints2xml : int -> int list -> string
1.7 - val itm_2xml : int -> Model.itm_ -> xml
1.8 - val itms2xml : int -> (int * Model.vats * bool * string * Model.itm_) list ->
1.9 + val itm_2xml : int -> I_Model.feedback -> xml
1.10 + val itms2xml : int -> (int * Model_Def.variants * bool * string * I_Model.feedback) list ->
1.11 string
1.12 val keref2xml : int -> Specify.ketype -> Specify.kestoreID -> xml
1.13 val model2xml :
1.14 @@ -344,18 +344,18 @@
1.15 if str = s then (t1 $ t2) :: filt ps else filt ps
1.16 in filt end;
1.17
1.18 -fun xml_of_itm_ (Model.Cor (dts, _)) =
1.19 +fun xml_of_itm_ (I_Model.Cor (dts, _)) =
1.20 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (I_Model.comp_dts' dts)])
1.21 - | xml_of_itm_ (Model.Syn c) =
1.22 + | xml_of_itm_ (I_Model.Syn c) =
1.23 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
1.24 - | xml_of_itm_ (Model.Typ c) =
1.25 + | xml_of_itm_ (I_Model.Typ c) =
1.26 XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
1.27 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
1.28 - | xml_of_itm_ (Model.Inc (dts, _)) =
1.29 + | xml_of_itm_ (I_Model.Inc (dts, _)) =
1.30 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (I_Model.comp_dts' dts)])
1.31 - | xml_of_itm_ (Model.Sup dts) =
1.32 + | xml_of_itm_ (I_Model.Sup dts) =
1.33 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (I_Model.comp_dts' dts)])
1.34 - | xml_of_itm_ (Model.Mis (d, pid)) =
1.35 + | xml_of_itm_ (I_Model.Mis (d, pid)) =
1.36 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
1.37 | xml_of_itm_ _ = error "xml_of_itm_: wrong argument"
1.38 fun xml_of_itms itms =
2.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue May 05 13:33:23 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Tue May 05 15:39:20 2020 +0200
2.3 @@ -58,14 +58,14 @@
2.4 (* turn model-items into arguments for a program *)
2.5 fun arguments_from_model mI itms =
2.6 let
2.7 - val mvat = Model.max_vt itms
2.8 + val mvat = I_Model.max_vt itms
2.9 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
2.10 val itms = filter (okv mvat) itms
2.11 - fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
2.12 + fun test_dsc d (_, _, _, _, itm_) = (d = I_Model.d_in itm_)
2.13 fun itm2arg itms (_,(d,_)) =
2.14 case find_first (test_dsc d) itms of
2.15 NONE => raise ERROR (error_msg_2 d itms)
2.16 - | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
2.17 + | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
2.18 val pats = (#ppc o Specify.get_met) mI
2.19 val _ = if pats = [] then raise ERROR error_msg_1 else ()
2.20 in (flat o (map (itm2arg itms))) pats end;
3.1 --- a/src/Tools/isac/Interpret/solve-step.sml Tue May 05 13:33:23 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Tue May 05 15:39:20 2020 +0200
3.3 @@ -99,7 +99,7 @@
3.4 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
3.5 | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
3.6 val {where_, ...} = Specify.get_pbt pI
3.7 - val pres = map (Model.mk_env probl |> subst_atomic) where_
3.8 + val pres = map (I_Model.mk_env probl |> subst_atomic) where_
3.9 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
3.10 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
3.11 else ctxt
4.1 --- a/src/Tools/isac/Specify/calchead.sml Tue May 05 13:33:23 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/calchead.sml Tue May 05 15:39:20 2020 +0200
4.3 @@ -99,10 +99,10 @@
4.4 val is_notyet_input : Proof.context -> I_Model.T -> term list -> O_Model.single -> ('a * (term * term)) list
4.5 -> string * I_Model.single
4.6 val ppc2list : 'a Model.ppc -> 'a list
4.7 - val mk_delete: theory -> string -> Model.itm_ -> Tactic.input
4.8 + val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
4.9 val mk_additem: string -> TermC.as_string -> Tactic.input
4.10 - val nxt_add: theory -> O_Model.T -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
4.11 - val is_error: Model.itm_ -> bool
4.12 + val nxt_add: theory -> O_Model.T -> (string * (term * 'a)) list -> (int * Model_Def.variants * bool * string * I_Model.feedback) list -> (string * string) option
4.13 + val is_error: I_Model.feedback -> bool
4.14 val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * I_Model.T -> I_Model.T * I_Model.T
4.15 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
4.16 val vals_of_oris : O_Model.T -> term list
4.17 @@ -131,8 +131,8 @@
4.18 val variants_in : term list -> int
4.19 val is_untouched : I_Model.single -> bool
4.20 val is_list_type : typ -> bool
4.21 - val parse_ok : Model.itm_ list -> bool
4.22 - val all_dsc_in : Model.itm_ list -> term list
4.23 + val parse_ok : I_Model.feedback list -> bool
4.24 + val all_dsc_in : I_Model.feedback list -> term list
4.25 val chktyps : theory -> term list * term list -> term list (* only in old tests*)
4.26 val chk_vars : term Model.ppc -> string * term list
4.27 val unbound_ppc : term Model.ppc -> term list
4.28 @@ -256,25 +256,25 @@
4.29
4.30 fun is_list_type (Type ("List.list", _)) = true
4.31 | is_list_type _ = false
4.32 -fun is_parsed (Model.Syn _) = false
4.33 +fun is_parsed (I_Model.Syn _) = false
4.34 | is_parsed _ = true
4.35 fun parse_ok its = foldl and_ (true, map is_parsed its)
4.36
4.37 fun all_dsc_in itm_s =
4.38 let
4.39 - fun d_in (Model.Cor ((d, _), _)) = [d]
4.40 - | d_in (Model.Syn _) = []
4.41 - | d_in (Model.Typ _) = []
4.42 - | d_in (Model.Inc ((d,_),_)) = [d]
4.43 - | d_in (Model.Sup (d,_)) = [d]
4.44 - | d_in (Model.Mis (d,_)) = [d]
4.45 + fun d_in (I_Model.Cor ((d, _), _)) = [d]
4.46 + | d_in (I_Model.Syn _) = []
4.47 + | d_in (I_Model.Typ _) = []
4.48 + | d_in (I_Model.Inc ((d,_),_)) = [d]
4.49 + | d_in (I_Model.Sup (d,_)) = [d]
4.50 + | d_in (I_Model.Mis (d,_)) = [d]
4.51 | d_in i = error ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
4.52 in (flat o (map d_in)) itm_s end;
4.53
4.54 -fun is_error (Model.Cor _) = false
4.55 - | is_error (Model.Sup _) = false
4.56 - | is_error (Model.Inc _) = false
4.57 - | is_error (Model.Mis _) = false
4.58 +fun is_error (I_Model.Cor _) = false
4.59 + | is_error (I_Model.Sup _) = false
4.60 + | is_error (I_Model.Inc _) = false
4.61 + | is_error (I_Model.Mis _) = false
4.62 | is_error _ = true
4.63
4.64 (* get the first term in ts from ori *)
4.65 @@ -285,14 +285,14 @@
4.66 the term from ori is thrown back to a string in order to reuse
4.67 machinery for immediate input by the user. *)
4.68 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
4.69 - (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (Model.ts_in itm_) ts))
4.70 + (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (I_Model.ts_in itm_) ts))
4.71
4.72 (* in FE dsc, not dat: this is in itms ...*)
4.73 -fun is_untouched (_, _, false, _, Model.Inc ((_, []), _)) = true
4.74 +fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
4.75 | is_untouched _ = false
4.76
4.77 (* select an item in oris, notyet input in itms
4.78 - (precondition: in itms are only Model.Cor, Model.Sup, Model.Inc) *)
4.79 + (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc) *)
4.80 (*args of nxt_add
4.81 thy : for?
4.82 oris: from formalization 'type fmz', structured for efficient access
4.83 @@ -301,7 +301,7 @@
4.84 *)
4.85 fun nxt_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
4.86 let
4.87 - fun test_d d (i, _, _, _, itm_) = (d = (Model.d_in itm_)) andalso i <> 0
4.88 + fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
4.89 fun is_elem itms (_, (d, _)) =
4.90 case find_first (test_d d) itms of SOME _ => true | NONE => false
4.91 in
4.92 @@ -315,11 +315,11 @@
4.93 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
4.94 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
4.95 fun test_subset itm (_, _, _, d, ts) =
4.96 - (Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (Model.ts_in (#5 itm), ts)
4.97 - fun false_and_not_Sup (_, _, false, _, Model.Sup _) = false
4.98 + (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
4.99 + fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
4.100 | false_and_not_Sup (_, _, false, _, _) = true
4.101 | false_and_not_Sup _ = false
4.102 - val v = if itms = [] then 1 else Model.max_vt itms
4.103 + val v = if itms = [] then 1 else I_Model.max_vt itms
4.104 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
4.105 val vits =
4.106 if v = 0
4.107 @@ -396,34 +396,34 @@
4.108 (* update the itm_ already input, all..from ori *)
4.109 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
4.110 let
4.111 - val ts' = union op = (Model.ts_in itm_) ts;
4.112 + val ts' = union op = (I_Model.ts_in itm_) ts;
4.113 val pval = Model.pbl_ids' d ts'
4.114 (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
4.115 val complete = if eq_set op = (ts', all) then true else false
4.116 in
4.117 case itm_ of
4.118 - (Model.Cor _) =>
4.119 - (if fd = "#undef" then (id, vt, complete, fd, Model.Sup (d, ts'))
4.120 - else (id, vt, complete, fd, Model.Cor ((d, ts'), (pid, pval))))
4.121 - | (Model.Syn c) => error ("ori_2itm wants to overwrite " ^ c)
4.122 - | (Model.Typ c) => error ("ori_2itm wants to overwrite " ^ c)
4.123 - | (Model.Inc _) =>
4.124 + (I_Model.Cor _) =>
4.125 + (if fd = "#undef" then (id, vt, complete, fd, I_Model.Sup (d, ts'))
4.126 + else (id, vt, complete, fd, I_Model.Cor ((d, ts'), (pid, pval))))
4.127 + | (I_Model.Syn c) => error ("ori_2itm wants to overwrite " ^ c)
4.128 + | (I_Model.Typ c) => error ("ori_2itm wants to overwrite " ^ c)
4.129 + | (I_Model.Inc _) =>
4.130 if complete
4.131 - then (id, vt, true, fd, Model.Cor ((d, ts'), (pid, pval)))
4.132 - else (id, vt, false, fd, Model.Inc ((d, ts'), (pid, pval)))
4.133 - | (Model.Sup (d,ts')) => (*4.9.01 lost env*)
4.134 - (*if fd = "#undef" then*) (id,vt,complete,fd,Model.Sup(d,ts'))
4.135 - (*else (id,vt,complete,fd,Model.Cor((d,ts'),e))*)
4.136 + then (id, vt, true, fd, I_Model.Cor ((d, ts'), (pid, pval)))
4.137 + else (id, vt, false, fd, I_Model.Inc ((d, ts'), (pid, pval)))
4.138 + | (I_Model.Sup (d,ts')) => (*4.9.01 lost env*)
4.139 + (*if fd = "#undef" then*) (id,vt,complete,fd,I_Model.Sup(d,ts'))
4.140 + (*else (id,vt,complete,fd,I_Model.Cor((d,ts'),e))*)
4.141 (* 28.1.00: not completely clear ---^^^ etc.*)
4.142 - | (Model.Mis _) => (* 4.9.01: Model.Mis just copied *)
4.143 + | (I_Model.Mis _) => (* 4.9.01: I_Model.Mis just copied *)
4.144 if complete
4.145 - then (id, vt, true, fd, Model.Cor ((d,ts'), (pid, pval)))
4.146 - else (id, vt, false, fd, Model.Inc ((d,ts'), (pid, pval)))
4.147 + then (id, vt, true, fd, I_Model.Cor ((d,ts'), (pid, pval)))
4.148 + else (id, vt, false, fd, I_Model.Inc ((d,ts'), (pid, pval)))
4.149 | i => error ("ori_2itm: uncovered case of "^ I_Model.feedback_to_string' i)
4.150 end
4.151
4.152 fun eq1 d (_, (d', _)) = (d = d')
4.153 -fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (Model.d_in itm_)
4.154 +fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.d_in itm_)
4.155
4.156 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
4.157 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
4.158 @@ -440,14 +440,14 @@
4.159 SOME (_, (_, pid)) =>
4.160 (case find_first (eq3 f d) itms of
4.161 SOME (_,_,_,_,itm_) =>
4.162 - let val ts' = inter op = (Model.ts_in itm_) ts
4.163 + let val ts' = inter op = (I_Model.ts_in itm_) ts
4.164 in
4.165 if subset op = (ts, ts')
4.166 then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", I_Model.empty) (*2*)
4.167 else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
4.168 end
4.169 - | NONE => ("", ori_2itm (Model.Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
4.170 - | NONE => ("", ori_2itm (Model.Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
4.171 + | NONE => ("", ori_2itm (I_Model.Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
4.172 + | NONE => ("", ori_2itm (I_Model.Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
4.173
4.174 fun test_types ctxt (d,ts) =
4.175 let
4.176 @@ -502,28 +502,28 @@
4.177 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)
4.178 in
4.179 case TermC.parseNEW ctxt ct of
4.180 - NONE => Add (i, [], false, sel, Model.Syn ct)
4.181 + NONE => Add (i, [], false, sel, I_Model.Syn ct)
4.182 | SOME t =>
4.183 let val (d, ts) = I_Model.split_dts t
4.184 in
4.185 if d = TermC.empty
4.186 - then Add (i, [], false, sel, Model.Mis (Specify.dsc_unknown, hd ts))
4.187 + then Add (i, [], false, sel, I_Model.Mis (Specify.dsc_unknown, hd ts))
4.188 else
4.189 (case find_first (eq1 d) pbt of
4.190 - NONE => Add (i, [], true, sel, Model.Sup (d,ts))
4.191 + NONE => Add (i, [], true, sel, I_Model.Sup (d,ts))
4.192 | SOME (f, (_, id)) =>
4.193 - let fun eq2 d (i, _, _, _, itm_) = d = (Model.d_in itm_) andalso i <> 0
4.194 + let fun eq2 d (i, _, _, _, itm_) = d = (I_Model.d_in itm_) andalso i <> 0
4.195 in case find_first (eq2 d) ppc of
4.196 - NONE => Add (i, [], true, f,Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
4.197 + NONE => Add (i, [], true, f,I_Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
4.198 | SOME (i', _, _, _, itm_) =>
4.199 if Input_Descript.is_list_dsc d
4.200 then
4.201 let
4.202 - val in_itm = Model.ts_in itm_
4.203 + val in_itm = I_Model.ts_in itm_
4.204 val ts' = union op = ts in_itm
4.205 val i'' = if in_itm = [] then i else i'
4.206 - in Add (i'', [], true, f, Model.Cor ((d, ts'), (id, Model.pbl_ids' d ts')))end
4.207 - else Add (i', [], true, f, Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
4.208 + in Add (i'', [], true, f, I_Model.Cor ((d, ts'), (id, Model.pbl_ids' d ts')))end
4.209 + else Add (i', [], true, f, I_Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
4.210 end)
4.211 end
4.212 end
4.213 @@ -660,14 +660,14 @@
4.214 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
4.215 fun insert_ppc thy itm ppc =
4.216 let
4.217 - fun eq_untouched d (0, _, _, _, itm_) = (d = Model.d_in itm_)
4.218 + fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.d_in itm_)
4.219 | eq_untouched _ _ = false
4.220 val ppc' = case seek_ppc (#1 itm) ppc of
4.221 SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
4.222 | NONE => (ppc @ [itm])
4.223 - in filter_out (eq_untouched ((Model.d_in o #5) itm)) ppc' end
4.224 + in filter_out (eq_untouched ((I_Model.d_in o #5) itm)) ppc' end
4.225
4.226 -fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (Model.d_in itm_ = Model.d_in iitm_)
4.227 +fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_Model.d_in iitm_)
4.228
4.229 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
4.230 handles superfluous items carelessly *)
4.231 @@ -827,15 +827,15 @@
4.232 | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
4.233
4.234 fun ori2Coritm pbt (i, v, f, d, ts) =
4.235 - (i, v, true, f, Model.Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts)))
4.236 - handle _ => (i, v, true, f, Model.Cor ((d, ts), (d, ts)))
4.237 + (i, v, true, f, I_Model.Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts)))
4.238 + handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
4.239 (*dsc in oris, but not in pbl pat list: keep this dsc*)
4.240
4.241 (* filter out oris which have same description in itms *)
4.242 fun filter_outs oris [] = oris
4.243 | filter_outs oris (i::itms) =
4.244 let
4.245 - val ors = filter_out ((curry op = ((Model.d_in o #5) i)) o (#4)) oris
4.246 + val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris
4.247 in
4.248 filter_outs ors itms
4.249 end
4.250 @@ -852,7 +852,7 @@
4.251 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
4.252 fun complete_metitms oris pits mits met =
4.253 let
4.254 - val vat = Model.max_vt pits;
4.255 + val vat = I_Model.max_vt pits;
4.256 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
4.257 val ors = filter ((member_swap op= vat) o (#2)) oris
4.258 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
4.259 @@ -864,7 +864,7 @@
4.260 fun complete_mod_ (oris, mpc, ppc, probl) =
4.261 let
4.262 val pits = filter_out ((curry op= false) o (#3)) probl
4.263 - val vat = if probl = [] then 1 else Model.max_vt probl
4.264 + val vat = if probl = [] then 1 else I_Model.max_vt probl
4.265 val pors = filter ((member_swap op = vat) o (#2)) oris
4.266 val pors = filter_outs pors pits (*which are in pbl already*)
4.267 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
4.268 @@ -1027,7 +1027,7 @@
4.269 val {cas, ...} = Specify.get_pbt pI
4.270 in case cas of
4.271 NONE => Form (Auto_Prog.pblterm dI pI)
4.272 - | SOME t => Form (subst_atomic (Model.mk_env probl) t)
4.273 + | SOME t => Form (subst_atomic (I_Model.mk_env probl) t)
4.274 end
4.275
4.276 (* pt_extract returns
5.1 --- a/src/Tools/isac/Specify/generate.sml Tue May 05 13:33:23 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/generate.sml Tue May 05 15:39:20 2020 +0200
5.3 @@ -92,13 +92,13 @@
5.4 (* init pbl with ...,dsc,empty | [] *)
5.5 fun init_pbl pbt =
5.6 let
5.7 - fun pbt2itm (f, (d, _)) = (0, [], false, f, Model.Inc ((d, []), (TermC.empty, [])))
5.8 + fun pbt2itm (f, (d, _)) = (0, [], false, f, I_Model.Inc ((d, []), (TermC.empty, [])))
5.9 in map pbt2itm pbt end
5.10
5.11 (* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)
5.12 fun init_pbl' pbt =
5.13 let
5.14 - fun pbt2itm (f, (d, t)) = (0, [], false, f, Model.Inc((d, [t]), (TermC.empty, [])))
5.15 + fun pbt2itm (f, (d, t)) = (0, [], false, f, I_Model.Inc((d, [t]), (TermC.empty, [])))
5.16 in map pbt2itm pbt end
5.17
5.18 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
6.1 --- a/src/Tools/isac/Specify/i-model.sml Tue May 05 13:33:23 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/i-model.sml Tue May 05 15:39:20 2020 +0200
6.3 @@ -38,6 +38,16 @@
6.4 val split_dts' : term * term -> term list
6.5 (*\------- to I_Model from Model 1a -------/*)
6.6
6.7 +(*/------- to I_Model from Model 4 -------\*)
6.8 + val d_in : feedback -> term
6.9 + val ts_in : feedback -> term list
6.10 + val penvval_in : feedback -> term list
6.11 + val vars_of : T -> term list
6.12 + val max_vt : T -> int
6.13 + val mk_env : T -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
6.14 + val all_ts_in : feedback list -> term list
6.15 + val vts_in: T -> int list
6.16 +(*\------- to I_Model from Model 4 -------/*)
6.17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.18 (* NONE *)
6.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.20 @@ -127,7 +137,7 @@
6.21 else (TermC.empty, TermC.dest_list' t)
6.22 end;
6.23 (* version returning ts only *)
6.24 -fun I_Model.split_dts' (d, arg) =
6.25 +fun split_dts' (d, arg) =
6.26 if Input_Descript.is_dsc d
6.27 then if Input_Descript.is_list_dsc d
6.28 then if TermC.is_list arg
6.29 @@ -138,7 +148,7 @@
6.30 else ([arg])
6.31 else (TermC.dest_list' arg)
6.32 (* WN170204: Warning "redundant"
6.33 - | I_Model.split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
6.34 + | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
6.35 let val (h,argl) = strip_comb t
6.36 in
6.37 if (not o is_dsc) h
6.38 @@ -203,4 +213,78 @@
6.39 fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : single -> int)) itms);
6.40 (*\------- to I_Model from Model 1 -------/*)
6.41
6.42 +(*/------- to I_Model from Model 4 -------\*)
6.43 +(* find most frequent variant v in itms *)
6.44 +fun vts_in itms = (distinct o flat o (map #2)) (itms: T);
6.45 +
6.46 +fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);
6.47 +fun vts_cnt vts itms = map (cnt itms) vts;
6.48 +fun max2 [] = error "max2 of []"
6.49 + | max2 (y :: ys) =
6.50 + let
6.51 + fun mx (a,x) [] = (a,x)
6.52 + | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
6.53 + in mx y ys end;
6.54 +
6.55 +(* get the constant value from a penv *)
6.56 +fun getval (id, values) =
6.57 + case values of
6.58 + [] => error ("penv_value: no values in '" ^ UnparseC.term id)
6.59 + | [v] => (id, v)
6.60 + | (v1 :: v2 :: _) => (case v1 of
6.61 + Const ("Program.Arbfix",_) => (id, v2)
6.62 + | _ => (id, v1));
6.63 +
6.64 +(* find the variant with most items already input *)
6.65 +fun max_vt itms =
6.66 + let val vts = (vts_cnt (vts_in itms)) itms;
6.67 + in if vts = [] then 0 else (fst o max2) vts end;
6.68 +
6.69 +(* TODO ev. make more efficient by avoiding flat *)
6.70 +fun mk_e (Cor (_, iv)) = [getval iv]
6.71 + | mk_e (Syn _) = []
6.72 + | mk_e (Typ _) = []
6.73 + | mk_e (Inc (_, iv)) = [getval iv]
6.74 + | mk_e (Sup _) = []
6.75 + | mk_e (Mis _) = []
6.76 + | mk_e _ = error "mk_e: uncovered case in fun.def.";
6.77 +fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
6.78 +
6.79 +(* extract the environment from an item list; takes the variant with most items *)
6.80 +fun mk_env itms =
6.81 + let val vt = max_vt itms
6.82 + in (flat o (map (mk_en vt))) itms end;
6.83 +(**)
6.84 +fun ts_in (Cor ((_, ts), _)) = ts
6.85 + | ts_in (Syn _) = []
6.86 + | ts_in (Typ _) = []
6.87 + | ts_in (Inc ((_, ts), _)) = ts
6.88 + | ts_in (Sup (_, ts)) = ts
6.89 + | ts_in (Mis _) = []
6.90 + | ts_in _ = error "ts_in: uncovered case in fun.def.";
6.91 +(*WN050629 unused*)
6.92 +fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
6.93 +
6.94 +val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
6.95 +fun d_in (Cor ((d ,_), _)) = d
6.96 + | d_in (Syn c) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
6.97 + | d_in (Typ c) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
6.98 + | d_in (Inc ((d, _), _)) = d
6.99 + | d_in (Sup (d, _)) = d
6.100 + | d_in (Mis (d, _)) = d
6.101 + | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
6.102 +
6.103 +fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
6.104 +fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
6.105 + | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
6.106 + | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
6.107 + | penvval_in (Inc (_, (_, ts))) = ts
6.108 + | penvval_in (Sup dts) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
6.109 + | penvval_in (Mis (d, t)) = ((*tracing ("*** penvval_in: Mis " ^
6.110 + pair2str(UnparseC.term d, UnparseC.term t));*) [])
6.111 + | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
6.112 +
6.113 +fun vars_of itms = itms |> mk_env |> map snd
6.114 +(*\------- to I_Model from Model 4 -------/*)
6.115 +
6.116 (**)end(**);
6.117 \ No newline at end of file
7.1 --- a/src/Tools/isac/Specify/input-calchead.sml Tue May 05 13:33:23 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Tue May 05 15:39:20 2020 +0200
7.3 @@ -21,7 +21,7 @@
7.4 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
7.5 val e_icalhd : icalhd
7.6 val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list ->
7.7 - ('c * ''b * bool * 'd * Model.itm_) list
7.8 + ('c * ''b * bool * 'd * I_Model.feedback) list
7.9 end
7.10
7.11 structure In_Chead(**): INPUT_CALCHEAD(**) =
7.12 @@ -41,7 +41,7 @@
7.13 (#1: (term * term) -> term) o
7.14 (#2: pbt_ -> (term * term))) ppc)
7.15 in
7.16 - ([1], true, f, Model.Cor ((d, ts), (id, ts)))
7.17 + ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
7.18 end
7.19
7.20 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
7.21 @@ -115,39 +115,39 @@
7.22 hdf <> "" andalso fmz_ = [] andalso spec = Spec.empty
7.23
7.24 (* re-parse itms with a new thy and prepare for checking with ori list *)
7.25 -fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =
7.26 +fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
7.27 (let val t = I_Model.comp_dts (d, ts)
7.28 val _ = (UnparseC.term_in_thy dI t)
7.29 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
7.30 in itm end
7.31 - handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
7.32 - | parsitm dI (i, v, b, f, Model.Syn str) =
7.33 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
7.34 + | parsitm dI (i, v, b, f, I_Model.Syn str) =
7.35 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
7.36 - in (i, v, b ,f, Model.Par str) end
7.37 - handle _ => (i, v, b, f, Model.Syn str))
7.38 - | parsitm dI (i, v, b, f, Model.Typ str) =
7.39 + in (i, v, b ,f, I_Model.Par str) end
7.40 + handle _ => (i, v, b, f, I_Model.Syn str))
7.41 + | parsitm dI (i, v, b, f, I_Model.Typ str) =
7.42 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
7.43 - in (i, v, b, f, Model.Par str) end
7.44 - handle _ => (i, v, b, f, Model.Syn str))
7.45 - | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) =
7.46 + in (i, v, b, f, I_Model.Par str) end
7.47 + handle _ => (i, v, b, f, I_Model.Syn str))
7.48 + | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
7.49 (let val t = I_Model.comp_dts (d,ts);
7.50 val _ = UnparseC.term_in_thy dI t;
7.51 (*this ^ should raise the exn on unability of re-parsing dts*)
7.52 in itm end
7.53 - handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
7.54 - | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) =
7.55 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
7.56 + | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
7.57 (let val t = I_Model.comp_dts (d,ts);
7.58 val _ = UnparseC.term_in_thy dI t;
7.59 (*this ^ should raise the exn on unability of re-parsing dts*)
7.60 in itm end
7.61 - handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
7.62 - | parsitm dI (itm as (i, v, _, f, Model.Mis (d, t'))) =
7.63 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
7.64 + | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
7.65 (let val t = d $ t';
7.66 val _ = UnparseC.term_in_thy dI t;
7.67 (*this ^ should raise the exn on unability of re-parsing dts*)
7.68 in itm end
7.69 - handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
7.70 - | parsitm dI (itm as (_, _, _, _, Model.Par _)) =
7.71 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
7.72 + | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) =
7.73 error ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
7.74
7.75 (*separate a list to a pair of elements that do NOT satisfy the predicate,
7.76 @@ -160,7 +160,7 @@
7.77 then filt (a, b @ [x]) xs
7.78 else filt (a @ [x], b) xs
7.79 in filt ([], []) xs end;
7.80 -fun is_Par (_, _, _, _, Model.Par _) = true
7.81 +fun is_Par (_, _, _, _, I_Model.Par _) = true
7.82 | is_Par _ = false;
7.83
7.84 fun is_e_ts [] = true
7.85 @@ -173,7 +173,7 @@
7.86 val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;
7.87 in
7.88 case TermC.parseNEW ctxt ct of
7.89 - NONE => (0, [], false, sel, Model.Syn ct)
7.90 + NONE => (0, [], false, sel, I_Model.Syn ct)
7.91 | SOME t =>
7.92 (case Chead.is_known ctxt sel oris t of
7.93 ("", ori', all) =>
7.94 @@ -182,8 +182,8 @@
7.95 | (msg,_) => error ("appl_add': " ^ msg))
7.96 | (_, (i, v, _, d, ts), _) =>
7.97 if is_e_ts ts
7.98 - then (i, v, false, sel, Model.Inc ((d, ts), (TermC.empty, [])))
7.99 - else (i, v, false, sel, Model.Sup (d, ts)))
7.100 + then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
7.101 + else (i, v, false, sel, I_Model.Sup (d, ts)))
7.102 end
7.103
7.104 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
7.105 @@ -193,15 +193,15 @@
7.106 val topt = TermC.parse thy str
7.107 in
7.108 case topt of
7.109 - NONE => ([], false, f, Model.Syn str)
7.110 + NONE => ([], false, f, I_Model.Syn str)
7.111 | SOME ct =>
7.112 let
7.113 val (d, ts) = (I_Model.split_dts o Thm.term_of) ct
7.114 val popt = find_first (eq7 (f, d)) pbt
7.115 in
7.116 case popt of
7.117 - NONE => ([1](*??*), true(*??*), f, Model.Sup (d, ts))
7.118 - | SOME (f, (d, id)) => ([1], true, f, Model.Cor ((d, ts), (id, ts)))
7.119 + NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
7.120 + | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
7.121 end
7.122 end
7.123
7.124 @@ -228,18 +228,18 @@
7.125 fun oris2itms _ _ [] = [] (* WN161130: similar in ptyps ?!? *)
7.126 | oris2itms pbt vat ((i, v, f, d, ts) :: os) =
7.127 if member op = vat v
7.128 - then (i, v, true, f, Model.Cor ((d, ts), (TermC.empty, []))) :: (oris2itms pbt vat os)
7.129 + then (i, v, true, f, I_Model.Cor ((d, ts), (TermC.empty, []))) :: (oris2itms pbt vat os)
7.130 else oris2itms pbt vat os
7.131
7.132 -fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
7.133 +fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
7.134 | par2fstr itm = error ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
7.135 -fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, I_Model.comp_dts'' (d, ts))
7.136 - | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
7.137 - | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
7.138 - | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, I_Model.comp_dts'' (d,ts))
7.139 - | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, I_Model.comp_dts'' (d, ts))
7.140 - | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
7.141 - | itms2fstr (itm as (_, _, _, _, Model.Par _)) =
7.142 +fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, I_Model.comp_dts'' (d, ts))
7.143 + | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
7.144 + | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
7.145 + | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, I_Model.comp_dts'' (d,ts))
7.146 + | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, I_Model.comp_dts'' (d, ts))
7.147 + | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
7.148 + | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =
7.149 error ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
7.150
7.151 fun imodel2fstr iitems =
8.1 --- a/src/Tools/isac/Specify/model.sml Tue May 05 13:33:23 2020 +0200
8.2 +++ b/src/Tools/isac/Specify/model.sml Tue May 05 15:39:20 2020 +0200
8.3 @@ -8,78 +8,30 @@
8.4
8.5 signature MODEL =
8.6 sig
8.7 - type vats = Model_Def.variants
8.8 -
8.9 - type ori = Model_Def.o_model_single
8.10 -(*/------- to O_Model from Model -------\* )
8.11 - val oris2str: ori list -> string
8.12 - val e_ori: ori
8.13 -( *\------- to O_Model from Model DONE -------/*)
8.14 - datatype itm_ = datatype Model_Def.i_model_feedback
8.15 - type itm = I_Model.single
8.16 -(*/------- to I_Model from Model DONE -------\* )
8.17 - val e_itm : itm
8.18 -( *\------- to I_Model from Model DONE -------/*)
8.19 -
8.20 datatype item
8.21 = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string
8.22 | SyntaxE of string | TypeE of string
8.23 -(*/------- to I_Model from Model 1 -------\* )
8.24 - val itm_2str : itm_ -> string
8.25 - val itm_2str_ : Proof.context -> itm_ -> string
8.26 - val itm2str_ : Proof.context -> itm -> string
8.27 - val itms2str_ : Proof.context -> itm list -> string
8.28 - val untouched : itm list -> bool
8.29 -( *\------- to I_Model from Model 1 -------/*)
8.30 +
8.31 type 'a ppc
8.32 val empty_ppc : item ppc
8.33 val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,
8.34 With: string list} -> string
8.35 val itemppc2str : item ppc -> string
8.36
8.37 -(*/------- to I_Model from Model 1a -------\* )
8.38 - val comp_dts : term * term list -> term
8.39 - val comp_dts' : term * term list -> term
8.40 - val comp_dts'' : term * term list -> string
8.41 - val comp_ts : term * term list -> term
8.42 - val split_dts : term -> term * term list
8.43 - val split_dts' : term * term -> term list
8.44 -( *\------- to I_Model from Model 1a -------/*)
8.45 val pbl_ids' : term -> term list -> term list
8.46 val mkval' : term list -> term
8.47
8.48 - val d_in : itm_ -> term
8.49 - val ts_in : itm_ -> term list
8.50 - val penvval_in : itm_ -> term list
8.51 - val vars_of : itm list -> term list
8.52 - val max_vt : itm list -> int
8.53 - val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
8.54 -
8.55 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.56 -(*/------- to I_Model from Model 1c -------\* )
8.57 - type penv
8.58 - val penv2str_ : Proof.context -> penv -> string (* NONE *)
8.59 -( *\------- to I_Model from Model 1c -------/*)
8.60 -(*/------- to O_Model from Model 1 -------\* )
8.61 - type preori
8.62 - val preoris2str : preori list -> string
8.63 -( *\------- to O_Model from Model 1 -------/*)
8.64 + (* NONE *)
8.65 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.66 (* NONE *)
8.67 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.68 -
8.69 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
8.70 - type envv
8.71 - val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv
8.72 - val item_ppc : string ppc -> item ppc
8.73 - val all_ts_in : itm_ list -> term list
8.74 - val pres2str : (bool * term) list -> string
8.75 end
8.76
8.77 structure Model(**) : MODEL(**) =
8.78 struct
8.79 (*==========================================================================
8.80 -23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
8.81 +23.3.02 TODO: ideas on redesign of type I_Model.feedback,type item,type ori,type item ppc
8.82 (1) kinds of itms:
8.83 (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
8.84 =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
8.85 @@ -88,7 +40,7 @@
8.86 Sup (presently) should be accepted in appl_add (instead Error')
8.87 _could_ be w.r.t current vat (and then _is_ related to vat
8.88 Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
8.89 -- dsc in itm_ is timeconsuming -- keep id for respective queries ?
8.90 +- dsc in I_Model.feedback is timeconsuming -- keep id for respective queries ?
8.91 - order of items in ppc should be stable w.r.t order of itms
8.92
8.93 - stepwise input of itms --- match_itms (in one go) ..not coordinated
8.94 @@ -97,7 +49,7 @@
8.95 (fast, for refine / slow, for modeling)
8.96
8.97 - clarify: efficiency <--> simplicity !!!
8.98 - ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
8.99 + ?: shift dsc I_Model.feedback -> itm | discard int in ori,itm | take int instead dsc
8.100 | take int for perserving order of item ppc in itms
8.101 | make all(!?) handling of itms stable against reordering(?)
8.102 | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
8.103 @@ -120,262 +72,14 @@
8.104 (b)
8.105 ==========================================================================*)
8.106
8.107 -(*/------- to I_Model from Model 1b -------\* )
8.108 -val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
8.109 -val e_listReal = script_parse "[]::(real list)";
8.110 -val e_listBool = script_parse "[]::(bool list)";
8.111 -
8.112 -(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
8.113 -fun take_apart t =
8.114 - let val elems = TermC.isalist2list t
8.115 - in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
8.116 -fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
8.117 - let val elems = (flat o (map TermC.isalist2list)) ts;
8.118 - in TermC.list2isalist (type_of (hd elems)) elems end;
8.119 -( *\------- to I_Model from Model 1b -------/*)
8.120 -
8.121 -(*/------- to I_Model from Model 1a -------\* )
8.122 -fun is_var (Free _) = true
8.123 - | is_var _ = false;
8.124 -
8.125 -(* special handling for lists. ?WN:14.5.03 ??!? *)
8.126 -fun dest_list (d, ts) =
8.127 - let fun dest t =
8.128 - if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*)
8.129 - then TermC.isalist2list t
8.130 - else [t]
8.131 - in (flat o (map dest)) ts end;
8.132 -
8.133 -(* revert split_dts only for ts; compare comp_dts *)
8.134 -fun comp_ts (d, ts) =
8.135 - if Input_Descript.is_list_dsc d
8.136 - then if TermC.is_list (hd ts)
8.137 - then if Input_Descript.is_unl d
8.138 - then (hd ts) (* e.g. someList [1,3,2] *)
8.139 - else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
8.140 - else (hd ts) (* a variable or metavariable for a list *)
8.141 - else (hd ts);
8.142 -fun comp_dts (d, []) =
8.143 - if Input_Descript.is_reall_dsc d
8.144 - then (d $ e_listReal)
8.145 - else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
8.146 - | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
8.147 - handle _ => error ("comp_dts: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
8.148 -fun comp_dts' (d, []) =
8.149 - if Input_Descript.is_reall_dsc d
8.150 - then (d $ e_listReal)
8.151 - else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
8.152 - | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
8.153 - handle _ => error ("comp_dts': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
8.154 -fun comp_dts'' (d, []) =
8.155 - if Input_Descript.is_reall_dsc d
8.156 - then UnparseC.term (d $ e_listReal)
8.157 - else if Input_Descript.is_booll_dsc d
8.158 - then UnparseC.term (d $ e_listBool)
8.159 - else UnparseC.term d
8.160 - | comp_dts'' (d, ts) = UnparseC.term (d $ (comp_ts (d, ts)))
8.161 - handle _ => error ("comp_dts'': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
8.162 -
8.163 -(* decompose an input into description, terms (ev. elems of lists),
8.164 - and the value for the problem-environment; inv to comp_dts *)
8.165 -fun split_dts (t as d $ arg) =
8.166 - if Input_Descript.is_dsc d
8.167 - then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not
8.168 - then (d, take_apart arg)
8.169 - else (d, [arg])
8.170 - else (TermC.empty, TermC.dest_list' t)
8.171 - | split_dts t =
8.172 - let val t' as (h, _) = strip_comb t;
8.173 - in
8.174 - if Input_Descript.is_dsc h
8.175 - then (h, dest_list t')
8.176 - else (TermC.empty, TermC.dest_list' t)
8.177 - end;
8.178 -(* version returning ts only *)
8.179 -fun split_dts' (d, arg) =
8.180 - if Input_Descript.is_dsc d
8.181 - then if Input_Descript.is_list_dsc d
8.182 - then if TermC.is_list arg
8.183 - then if Input_Descript.is_unl d
8.184 - then ([arg]) (* e.g. someList [1,3,2] *)
8.185 - else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
8.186 - else ([arg]) (* a variable or metavariable for a list *)
8.187 - else ([arg])
8.188 - else (TermC.dest_list' arg)
8.189 -(* WN170204: Warning "redundant"
8.190 - | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
8.191 - let val (h,argl) = strip_comb t
8.192 - in
8.193 - if (not o is_dsc) h
8.194 - then (dest_list' t)
8.195 - else (dest_list (h,argl))
8.196 - end;*)
8.197 -(* revert split_:
8.198 - WN050903 we do NOT know which is from subtheory, description or term;
8.199 - typecheck thus may lead to TYPE-error 'unknown constant';
8.200 - solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)
8.201 -(*fun comp_dts thy (d,[]) =
8.202 - Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
8.203 - (Thy_Info_get_theory "Isac_Knowledge")
8.204 - (*comp_dts:FIXXME stay with term for efficiency !!!*)
8.205 - (if is_reall_dsc d then (d $ e_listReal)
8.206 - else if is_booll_dsc d then (d $ e_listBool)
8.207 - else d)
8.208 - | comp_dts (d,ts) =
8.209 - (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
8.210 - (Thy_Info_get_theory "Isac_Knowledge")
8.211 - (*comp_dts:FIXXME stay with term for efficiency !!*)
8.212 - (d $ (comp_ts (d, ts)))
8.213 - handle _ => error ("comp_dts: "^(term2str d)^
8.214 - " $ "^(term2str (hd ts))));*)
8.215 -( *\------- to I_Model from Model 1a -------/*)
8.216 -
8.217 -(*/------- to I_Model from Model 1c -------\*)
8.218 -(* 27.8.01: problem-environment
8.219 -WN.6.5.03: FIXXME reconsider if penv is worth the effort --
8.220 - -- just rerun a whole expl with num/var may show the same ?!
8.221 -WN.9.5.03: penv-concept stalled, immediately generate script env !
8.222 - but [#0, epsilon] only outcommented for eventual reconsideration *)
8.223 -type penv = (* problem-environment *)
8.224 - (term (* err_ *)
8.225 - * (term list) (* [#0, epsilon] 9.5.03 outcommented *)
8.226 - ) list;
8.227 -fun pen2str ctxt (t, ts) =
8.228 - pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts);
8.229 -fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
8.230 -(*\------- to I_Model from Model 1c -------/*)
8.231 -
8.232 -(* get the constant value from a penv *)
8.233 -fun getval (id, values) =
8.234 - case values of
8.235 - [] => error ("penv_value: no values in '" ^ UnparseC.term id)
8.236 - | [v] => (id, v)
8.237 - | (v1 :: v2 :: _) => (case v1 of
8.238 - Const ("Program.Arbfix",_) => (id, v2)
8.239 - | _ => (id, v1));
8.240 -
8.241 -(* 9.5.03: still unused, but left for eventual future development *)
8.242 -type envv = (int * penv) list; (* over variants *)
8.243 -
8.244 -(* 14.9.01: not used after putting penv-values into itm_
8.245 - make the result of split_* a value of problem-environment *)
8.246 fun mkval _(*dsc*) [] = error "mkval called with []"
8.247 | mkval _ [t] = t
8.248 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
8.249 fun mkval' x = mkval TermC.empty x;
8.250
8.251 -(*/------- to O_Model+I_ from Mode -------\*)
8.252 -type vats = Model_Def.variants;
8.253 -(*\------- to O_Model+I_ from Model -------/*)
8.254 -
8.255 -(*/------- to I_Model from Model DONE -------\*)
8.256 -(* the internal representation of a models' item
8.257 - 4.9.01: not consistent:
8.258 - after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
8.259 - (involves 'is_error');
8.260 - bool in itm really necessary ???*)
8.261 -datatype itm_ = datatype Model_Def.i_model_feedback; (* internal state from fun parsitm *)
8.262 -
8.263 -(* data-type for working on pbl/met-ppc:
8.264 - in pbl initially holds descriptions (only) for user guidance *)
8.265 -type itm =
8.266 - int * (* id =0 .. untouched - descript (only) from init
8.267 - seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *)
8.268 - vats * (* variants - copy from ori *)
8.269 - bool * (* input on this item is not/complete *)
8.270 - string * (* #Given | #Find | #Relate *)
8.271 - itm_; (* *)
8.272 -val e_itm = (0, [], false, "e_itm", Syn "e_itm");
8.273 -(*\------- to I_Model from Model DONE -------/*)
8.274 -
8.275 -(* find most frequent variant v in itms *)
8.276 -fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
8.277 -
8.278 -fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);
8.279 -fun vts_cnt vts itms = map (cnt itms) vts;
8.280 -fun max2 [] = error "max2 of []"
8.281 - | max2 (y :: ys) =
8.282 - let
8.283 - fun mx (a,x) [] = (a,x)
8.284 - | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
8.285 - in mx y ys end;
8.286 -
8.287 -(* find the variant with most items already input *)
8.288 -fun max_vt itms =
8.289 - let val vts = (vts_cnt (vts_in itms)) itms;
8.290 - in if vts = [] then 0 else (fst o max2) vts end;
8.291 -
8.292 -(* TODO ev. make more efficient by avoiding flat *)
8.293 -fun mk_e (Cor (_, iv)) = [getval iv]
8.294 - | mk_e (Syn _) = []
8.295 - | mk_e (Typ _) = []
8.296 - | mk_e (Inc (_, iv)) = [getval iv]
8.297 - | mk_e (Sup _) = []
8.298 - | mk_e (Mis _) = []
8.299 - | mk_e _ = error "mk_e: uncovered case in fun.def.";
8.300 -fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
8.301 -
8.302 -(* extract the environment from an item list; takes the variant with most items *)
8.303 -fun mk_env itms =
8.304 - let val vt = max_vt itms
8.305 - in (flat o (map (mk_en vt))) itms end;
8.306 -
8.307 -
8.308 -
8.309 -(*/------- to O_Model from Model -------\*)
8.310 -(* example as provided by an author, complete w.r.t. pbt specified
8.311 - not touched by any user action *)
8.312 -type ori = Model_Def.o_model_single;
8.313 -val e_ori = Model_Def.o_model_empty;
8.314 -
8.315 -val oris2str = Model_Def.o_model_to_string;
8.316 -(*\------- to O_Model from Model -------/*)
8.317 -
8.318 -(*/------- to O_Model from Model 1 -------\* )
8.319 -(* an or without leading integer *)
8.320 -type preori = (vats * string * term * term list);
8.321 -fun preori2str (vs, fi, t, ts) =
8.322 - "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
8.323 - UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
8.324 -val preoris2str = (strs2str' o (map (linefeed o preori2str)));
8.325 -( *\------- to O_Model from Model 1 -------/*)
8.326 -
8.327 (* 9.5.03 penv postponed: pbl_ids' *)
8.328 fun pbl_ids' d vs = [I_Model.comp_ts (d, vs)];
8.329
8.330 -(* 14.9.01: not used after putting values for penv into itm_
8.331 - WN.5.5.03: used in upd .. upd_envv *)
8.332 -fun upd_penv ctxt penv dsc (id, vl) =
8.333 -((*tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.334 - tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
8.335 - tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";*)
8.336 - overwrite (penv, (id, Input_Descript.pbl_ids ctxt dsc vl))
8.337 -);
8.338 -
8.339 -(* WN.9.5.03: not reconsidered; looks strange !!!*)
8.340 -fun upd thy envv dsc (id, vl) i =
8.341 - let val penv = case assoc (envv, i) of
8.342 - SOME e => e
8.343 - | NONE => [];
8.344 - val penv' = upd_penv thy penv dsc (id, vl);
8.345 - in (i, penv') end;
8.346 -
8.347 -(* 14.9.01: not used after putting pre-penv into itm_*)
8.348 -fun upd_envv thy envv vats dsc id vl =
8.349 - let val vats = if length vats = 0
8.350 - then (*unknown id to _all_ variants*)
8.351 - if length envv = 0 then [1]
8.352 - else (intsto o length) envv
8.353 - else vats
8.354 - fun isin vats (i, _) = member op = vats i;
8.355 - val envs_notin_vat = filter_out (isin vats) envv;
8.356 - in (map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat end;
8.357 -
8.358 -(* update envv by folding from a list of arguments *)
8.359 -fun upds_envv _ envv [] = envv
8.360 - | upds_envv thy envv ((vs, dsc, id, vl) :: ps) =
8.361 - upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
8.362 -
8.363 (* for _output_ of the items of a Model *)
8.364 datatype item =
8.365 Correct of TermC.as_string (* labels a correct formula (type cterm') *)
8.366 @@ -393,40 +97,12 @@
8.367 | item2str (Superfl s) = "Superfl " ^ s
8.368 | item2str (Missing s) = "Missing " ^ s;
8.369
8.370 -(*/------- to I_Model from Model 1 -------\* )
8.371 -fun itm_2str_ ctxt (Cor ((d, ts), penv)) =
8.372 - "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
8.373 - | itm_2str_ _ (Syn c) = "Syn " ^ c
8.374 - | itm_2str_ _ (Typ c) = "Typ " ^ c
8.375 - | itm_2str_ ctxt (Inc ((d, ts), penv)) =
8.376 - "Inc " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
8.377 - | itm_2str_ ctxt (Sup (d, ts)) =
8.378 - "Sup " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts))
8.379 - | itm_2str_ ctxt (Mis (d, pid)) =
8.380 - "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid
8.381 - | itm_2str_ _ (Par s) = "Trm "^s;
8.382 -fun itm_2str t = itm_2str_ (ThyC.id_to_ctxt "Isac_Knowledge") t;
8.383 -
8.384 -fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
8.385 - "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
8.386 - s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
8.387 -fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
8.388 -
8.389 -(* in CalcTree/Subproblem an 'untouched' model is created
8.390 - FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
8.391 -fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms);
8.392 -( *\------- to I_Model from Model 1 -------/*)
8.393 -fun init_item str = SyntaxE str;
8.394 -
8.395 type 'a ppc =
8.396 {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
8.397 fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=
8.398 "{Given =" ^ strs2str Given ^ ",Where=" ^ strs2str Where ^ ",Find =" ^ strs2str Find ^
8.399 ",With =" ^ strs2str With ^ ",Relate=" ^ strs2str Relate ^ "}";
8.400
8.401 -fun item_ppc {Given = gi, Where= wh, Find = fi, With = wi, Relate= re} =
8.402 - {Given = map init_item gi, Where= map init_item wh, Find = map init_item fi,
8.403 - With = map init_item wi, Relate= map init_item re};
8.404 fun itemppc2str ({Given=Given,Where=Where,
8.405 Find=Find,With=With,Relate=Relate}:item ppc)=
8.406 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
8.407 @@ -437,45 +113,4 @@
8.408
8.409 val empty_ppc = {Given = [], Where= [], Find = [], With = [], Relate= []};
8.410
8.411 -fun ts_in (Cor ((_, ts), _)) = ts
8.412 - | ts_in (Syn _) = []
8.413 - | ts_in (Typ _) = []
8.414 - | ts_in (Inc ((_, ts), _)) = ts
8.415 - | ts_in (Sup (_, ts)) = ts
8.416 - | ts_in (Mis _) = []
8.417 - | ts_in _ = error "ts_in: uncovered case in fun.def.";
8.418 -(*WN050629 unused*)
8.419 -fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
8.420 -val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
8.421 -fun d_in (Cor ((d ,_), _)) = d
8.422 - | d_in (Syn c) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
8.423 - | d_in (Typ c) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
8.424 - | d_in (Inc ((d, _), _)) = d
8.425 - | d_in (Sup (d, _)) = d
8.426 - | d_in (Mis (d, _)) = d
8.427 - | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
8.428 -
8.429 -fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
8.430 -fun penvval_in (Cor ((d, _), (_, ts))) = [I_Model.comp_ts (d,ts)]
8.431 - | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
8.432 - | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
8.433 - | penvval_in (Inc (_, (_, ts))) = ts
8.434 - | penvval_in (Sup dts) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
8.435 - | penvval_in (Mis (d, t)) = ((*tracing ("*** penvval_in: Mis " ^
8.436 - pair2str(UnparseC.term d, UnparseC.term t));*) [])
8.437 - | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
8.438 -
8.439 -(* check a predicate labelled with indication of incomplete substitution;
8.440 - rls -> (* for eval_true *)
8.441 - bool * (* have _all_ variables(Free) from the model-pattern
8.442 - been substituted by a value from the pattern's environment ?*)
8.443 - term -> (* the precondition *)
8.444 - bool * (* has the precondition evaluated to true *)
8.445 - term (* the precondition (for map) *)
8.446 -*)
8.447 -fun pre2str (b, t) = pair2str(bool2str b, UnparseC.term t);
8.448 -fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
8.449 -
8.450 -fun vars_of itms = itms |> mk_env |> map snd
8.451 -
8.452 (**)end(**);
8.453 \ No newline at end of file
9.1 --- a/src/Tools/isac/Specify/mstools.sml Tue May 05 13:33:23 2020 +0200
9.2 +++ b/src/Tools/isac/Specify/mstools.sml Tue May 05 15:39:20 2020 +0200
9.3 @@ -84,10 +84,10 @@
9.4 fun check_preconds' _ [] _ _ = [] (* empty preconditions are true *)
9.5 | check_preconds' prls pres pbl _ (* FIXME.WN0308 mvat re-introduce *) =
9.6 let
9.7 - val env = Model.mk_env pbl;
9.8 + val env = I_Model.mk_env pbl;
9.9 val pres' = map (TermC.subst_atomic_all env) pres;
9.10 in map (evalprecond prls) pres' end;
9.11 -fun check_preconds _(*thy*) prls pres pbl = check_preconds' prls pres pbl (Model.max_vt pbl);
9.12 +fun check_preconds _(*thy*) prls pres pbl = check_preconds' prls pres pbl (I_Model.max_vt pbl);
9.13
9.14
9.15 fun common_subthy (thy1, thy2) =
10.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue May 05 13:33:23 2020 +0200
10.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue May 05 15:39:20 2020 +0200
10.3 @@ -33,7 +33,7 @@
10.4 type pblRD = string list (* for pbl-met-hierarchy.sml *)
10.5 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
10.6 val scan : string list -> 'a Store.T -> string list list (* for thy-hierarchy.sml *)
10.7 - val itm_out : theory -> Model.itm_ -> string
10.8 + val itm_out : theory -> I_Model.feedback -> string
10.9 val dsc_unknown : term
10.10
10.11 (*/------- from Celem to Specify -------\*)
10.12 @@ -93,11 +93,11 @@
10.13 fun hack_until_review_Specify_1 metID itms =
10.14 if metID = ["Biegelinien", "ausBelastung"]
10.15 then itms @
10.16 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
10.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", [])])),
10.18 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
10.19 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
10.20 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
10.21 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
10.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", [])])),
10.23 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
10.24 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
10.25 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
10.26 @@ -105,11 +105,11 @@
10.27 fun hack_until_review_Specify_2 metID itms =
10.28 if metID = ["IntegrierenUndKonstanteBestimmen2"]
10.29 then itms @
10.30 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
10.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", [])])),
10.32 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
10.33 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
10.34 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
10.35 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
10.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", [])])),
10.37 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
10.38 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
10.39 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
10.40 @@ -151,12 +151,12 @@
10.41 type field = string * (term * term)
10.42 val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
10.43
10.44 -fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (I_Model.comp_dts (d, ts)))
10.45 - | itm_2item _ (Model.Syn c) = Model.SyntaxE c
10.46 - | itm_2item _ (Model.Typ c) = Model.TypeE c
10.47 - | itm_2item _ (Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (I_Model.comp_dts (d, ts)))
10.48 - | itm_2item _ (Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (I_Model.comp_dts (d, ts)))
10.49 - | itm_2item _ (Model.Mis (d, pid)) = Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)
10.50 +fun itm_2item (_: theory) (I_Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (I_Model.comp_dts (d, ts)))
10.51 + | itm_2item _ (I_Model.Syn c) = Model.SyntaxE c
10.52 + | itm_2item _ (I_Model.Typ c) = Model.TypeE c
10.53 + | itm_2item _ (I_Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (I_Model.comp_dts (d, ts)))
10.54 + | itm_2item _ (I_Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (I_Model.comp_dts (d, ts)))
10.55 + | itm_2item _ (I_Model.Mis (d, pid)) = Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)
10.56 | itm_2item _ _ = error "itm_2item: uncovered definition"
10.57
10.58 fun mappc f {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} =
10.59 @@ -184,12 +184,12 @@
10.60 in (hd, arg) end
10.61
10.62 (*create output-string for itm_*)
10.63 -fun itm_out _ (Model.Cor ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
10.64 - | itm_out _ (Model.Syn c) = c
10.65 - | itm_out _ (Model.Typ c) = c
10.66 - | itm_out _ (Model.Inc ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
10.67 - | itm_out _ (Model.Sup (d, ts)) = UnparseC.term (I_Model.comp_dts (d, ts))
10.68 - | itm_out _ (Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
10.69 +fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
10.70 + | itm_out _ (I_Model.Syn c) = c
10.71 + | itm_out _ (I_Model.Typ c) = c
10.72 + | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
10.73 + | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (I_Model.comp_dts (d, ts))
10.74 + | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
10.75 | itm_out _ _ = error "itm_out: uncovered definition"
10.76
10.77 fun boolterm2item (true, term) = Model.Correct (UnparseC.term term)
10.78 @@ -447,34 +447,34 @@
10.79 (** check a problem (ie. itm list) for matching a problemtype **)
10.80
10.81 fun eq1 d (_, (d', _)) = (d = d');
10.82 -fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", Model.Sup (d, ts));
10.83 +fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts));
10.84 (*see + add_sel_ppc ~~~~~~~*)
10.85
10.86 fun field_eq f (_, _, f', _, _) = f = f';
10.87
10.88 (* check an item (with arbitrary itm_ from previous matchings)
10.89 for matching a problemtype; returns true only for itms found in pbt *)
10.90 -fun chk_ (_: theory) pbt (i, vats, b, f, Model.Cor ((d, vs), _)) =
10.91 +fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
10.92 (case find_first (eq1 d) pbt of
10.93 - SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
10.94 - | NONE => (i, vats, false, f, Model.Sup (d, vs)))
10.95 - | chk_ _ pbt (i, vats, b, f, Model.Inc ((d, vs), _)) =
10.96 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
10.97 + | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
10.98 + | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
10.99 (case find_first (eq1 d) pbt of
10.100 - SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
10.101 - | NONE => (i, vats, false, f, Model.Sup (d, vs)))
10.102 - | chk_ _ _ (itm as (_, _, _, _, Model.Syn _)) = itm
10.103 - | chk_ _ _ (itm as (_, _, _, _, Model.Typ _)) = itm
10.104 - | chk_ _ pbt (i, vats, b, f, Model.Sup (d, vs)) =
10.105 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
10.106 + | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
10.107 + | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
10.108 + | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
10.109 + | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
10.110 (case find_first (eq1 d) pbt of
10.111 - SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d,vs), (id, Model.pbl_ids' d vs)))
10.112 - | NONE => (i, vats, false, f, Model.Sup (d, vs)))
10.113 - | chk_ _ pbt (i, vats, _, f, Model.Mis (d, vs)) =
10.114 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, Model.pbl_ids' d vs)))
10.115 + | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
10.116 + | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
10.117 (case find_first (eq1 d) pbt of
10.118 - SOME (_, _) => error "chk_: ((i,vats,b,f,Model.Cor ((d,vs),(id, Model.pbl_ids' d vs))):itm)"
10.119 - | NONE => (i, vats, false, f, Model.Sup (d, [vs])))
10.120 + SOME (_, _) => error "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Model.pbl_ids' d vs))):itm)"
10.121 + | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
10.122 | chk_ _ _ _ = error "chk_: uncovered fun def.";
10.123
10.124 -fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = Model.d_in itm_;
10.125 +fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
10.126 fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
10.127 fun eq0 (0, _, _, _, _) = true
10.128 | eq0 _ = false;
10.129 @@ -495,7 +495,7 @@
10.130 | NONE =>
10.131 (case find_first (eq2 p) untouched of
10.132 SOME itm => [itm]
10.133 - | NONE => [(0, [], false, f, Model.Mis (d, id))]);
10.134 + | NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
10.135
10.136 fun chk_mis mvat itms untouched pbt =
10.137 let val mis = (flat o (map (chk_m itms untouched))) pbt;
10.138 @@ -503,12 +503,12 @@
10.139 in add_idvat [] (mid + 1) mvat mis end;
10.140
10.141 (* check a problem (ie. itm list) for matching a problemtype,
10.142 - takes the Model.max_vt for concluding completeness (could be another!) *)
10.143 + takes the I_Model.max_vt for concluding completeness (could be another!) *)
10.144 fun match_itms thy itms (pbt, pre, prls) =
10.145 let
10.146 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
10.147 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
10.148 - val mvat = Model.max_vt itms';
10.149 + val mvat = I_Model.max_vt itms';
10.150 val itms'' = filter (okv mvat) itms';
10.151 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
10.152 val mis = chk_mis mvat itms'' untouched pbt;
10.153 @@ -518,7 +518,7 @@
10.154
10.155 (* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
10.156 for missing items get data from formalization (ie. ori list);
10.157 - takes the Model.max_vt for concluding completeness (could be another!)
10.158 + takes the I_Model.vars_of for concluding completeness (could be another!)
10.159
10.160 (0) determine the most frequent variant mv in pbl
10.161 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
10.162 @@ -527,15 +527,15 @@
10.163 (4) pbt @ newitms *)
10.164 fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
10.165 let
10.166 - (*0*)val mv = Model.max_vt pbl;
10.167 + (*0*)val mv = I_Model.max_vt pbl;
10.168
10.169 - fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = Model.d_in itm_;
10.170 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
10.171 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
10.172 SOME _ => false | NONE => true;
10.173 (*1*)val mis = (filter (notmem pbl)) pbt;
10.174
10.175 fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
10.176 - fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, Model.Mis (d, pid));
10.177 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
10.178 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
10.179 val news = (flat o (map (oris2itms oris))) mis;
10.180 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
10.181 @@ -552,7 +552,7 @@
10.182 returns true only for itms found in pbt *)
10.183 fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
10.184 case find_first (eq1 d) pbt of
10.185 - SOME (_, (_, id)) => [(i, vats, true, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))]
10.186 + SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))]
10.187 | NONE => [];
10.188
10.189 (* elem 'p' of pbt contained in itms ? *)
10.190 @@ -560,18 +560,18 @@
10.191 fun chk1_m' oris (p as (f, (d, t))) =
10.192 case find_first (eq2' p) oris of
10.193 SOME _ => []
10.194 - | NONE => [(f, Model.Mis (d, t))];
10.195 + | NONE => [(f, I_Model.Mis (d, t))];
10.196 fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
10.197
10.198 fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
10.199 fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
10.200
10.201 (* check a problem (ie. ori list) for matching a problemtype,
10.202 - takes the Model.max_vt for concluding completeness (FIXME could be another!) *)
10.203 + takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *)
10.204 fun match_oris thy prls oris (pbt,pre) =
10.205 let
10.206 val itms = (flat o (map (chk1_ thy pbt))) oris;
10.207 - val mvat = Model.max_vt itms;
10.208 + val mvat = I_Model.vars_of itms;
10.209 val complete = chk1_mis mvat itms pbt;
10.210 val pre' = Stool.check_preconds' prls pre itms mvat;
10.211 val pb = foldl and_ (true, map fst pre');
10.212 @@ -583,7 +583,7 @@
10.213 let
10.214 val itms = (flat o (map (chk1_ thy ppc))) oris;
10.215 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
10.216 - val mvat = Model.max_vt itms;
10.217 + val mvat = I_Model.vars_of itms;
10.218 val miss = chk1_mis' oris ppc;
10.219 val pre' = Stool.check_preconds' prls pre itms mvat;
10.220 val pb = foldl and_ (true, map fst pre');
11.1 --- a/src/Tools/isac/TODO.thy Tue May 05 13:33:23 2020 +0200
11.2 +++ b/src/Tools/isac/TODO.thy Tue May 05 15:39:20 2020 +0200
11.3 @@ -336,7 +336,7 @@
11.4 \item xxx
11.5 \item this has been written in one go:
11.6 \begin{itemize}
11.7 - \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
11.8 + \item reconsidering I_Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
11.9 \item reconsider add_field': where is it used for what? Shift into mk_oris
11.10 \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
11.11 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
12.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 05 13:33:23 2020 +0200
12.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 05 15:39:20 2020 +0200
12.3 @@ -92,7 +92,7 @@
12.4 val pp = par_pblobj pt p
12.5 val chd = tryrefine pblID pt (pp, p_);
12.6 "~~~~~ fun matchpbl2xml, args:"; val ((cI:calcID), (model_ok, pI, hdl, pbl, pre)) = (cI, chd);
12.7 -"~~~~~ fun model2xml, args:"; val (j, (itms:itm list), where_) = (i, pbl, pre);
12.8 +"~~~~~ fun model2xml, args:"; val (j, (itms:I_Model.T), where_) = (i, pbl, pre);
12.9 "~~~~~ fun xml_of_model, args:"; val (itms, where_) = (pbl, pre);
12.10 val xxx = xml_of_model itms where_;
12.11 (xmlstr 0 xxx);
13.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue May 05 13:33:23 2020 +0200
13.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue May 05 15:39:20 2020 +0200
13.3 @@ -1250,7 +1250,7 @@
13.4 ...vvv
13.5 *)
13.6 (* val (dI, oris, ppc, pbt, (selct::ss))=
13.7 - (#1 (some_spec ospec spec), oris, []:itm list,
13.8 + (#1 (some_spec ospec spec), oris, []:I_Model.T,
13.9 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
13.10 val iii = appl_adds dI oris ppc pbt (selct::ss);
13.11 tracing(I_Model.to_string thy iii);
14.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue May 05 13:33:23 2020 +0200
14.2 +++ b/test/Tools/isac/Knowledge/poly.sml Tue May 05 15:39:20 2020 +0200
14.3 @@ -617,7 +617,7 @@
14.4
14.5 (*+*)if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
14.6 (*+*) "[\n(0 ,[] ,false ,#Find ,Inc normalform ,(??.empty, [])),\n(1 ,[1] ,true ,#Given ,Cor Term\n ((5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n (3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1)) ,(t_t, [(5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n(3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1)]))]"
14.7 -(*+*)then () else error "No.267b: itm list CHANGED";
14.8 +(*+*)then () else error "No.267b: I_Model.T CHANGED";
14.9
14.10 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
14.11 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
15.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue May 05 13:33:23 2020 +0200
15.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue May 05 15:39:20 2020 +0200
15.3 @@ -77,7 +77,7 @@
15.4 is_known ctxt sel oris t;
15.5 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
15.6 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
15.7 -val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list);
15.8 +val ots = (Library.distinct op = o flat o (map #5)) (ori:O_Model.T);
15.9 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
15.10 val (d, ts) = I_Model.split_dts t;
15.11 "~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t;
16.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Tue May 05 13:33:23 2020 +0200
16.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Tue May 05 15:39:20 2020 +0200
16.3 @@ -77,7 +77,7 @@
16.4 is_known ctxt sel oris t;
16.5 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
16.6 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
16.7 -val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list);
16.8 +val ots = (Library.distinct op = o flat o (map #5)) (ori:O_Model.T);
16.9 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
16.10 val (d, ts) = I_Model.split_dts t;
16.11 "~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t;
17.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Tue May 05 13:33:23 2020 +0200
17.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Tue May 05 15:39:20 2020 +0200
17.3 @@ -41,14 +41,14 @@
17.4 (* val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
17.5 (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
17.6 ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*)
17.7 -"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : ori list), ((dI', pI', mI') : Spec.T),
17.8 - ((pbl : itm list), (met : itm list)), (pbt, mpc), ((dI, pI, mI) : Spec.T)) =
17.9 +"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : O_Model.T), ((dI', pI', mI') : Spec.T),
17.10 + ((pbl : I_Model.T), (met : I_Model.T)), (pbt, mpc), ((dI, pI, mI) : Spec.T)) =
17.11 (p_, pb, oris, (dI',pI',mI'), (probl, meth),
17.12 (ppc, (#ppc o get_met) cmI), (dI, pI, mI));
17.13
17.14 dI' = ThyC.id_empty andalso dI = ThyC.id_empty; (* = false*)
17.15 pI' = Problem.id_empty andalso pI = Problem.id_empty; (* = false*)
17.16 -find_first (is_error o #5) (pbl:itm list); (* = NONE*)
17.17 +find_first (is_error o #5) (pbl:I_Model.T); (* = NONE*)
17.18
17.19 (* nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl;
17.20 = SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *)
17.21 @@ -58,13 +58,13 @@
17.22 fun x mem [] = false
17.23 | x mem (y :: ys) = x = y orelse x mem ys;
17.24 in
17.25 - fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
17.26 + fun testr_vt v ori = (curry (op mem) v) (#2 (ori:O_Model.single))
17.27 andalso (#3 ori) <>"#undef";
17.28 - fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
17.29 - fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
17.30 - fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
17.31 + fun testi_vt v itm = (curry (op mem) v) (#2 (itm:I_Model.single));
17.32 + fun test_id ids r = curry (op mem) (#1 (r:O_Model.single)) ids;
17.33 + fun test_subset (itm:I_Model.single) ((_,_,_,d,ts):O_Model.single) =
17.34 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
17.35 - fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
17.36 + fun false_and_not_Sup((i,v,false,f,Sup _):I_Model.single) = false
17.37 | false_and_not_Sup (i,v,false,f, _) = true
17.38 | false_and_not_Sup _ = false;
17.39 end
17.40 @@ -78,7 +78,7 @@
17.41
17.42 (* SOME (geti_ct thy ori (hd icl))
17.43 ERROR: SOME (geti_ct thy ori (hd icl))*)
17.44 -"~~~~~ fun geti_ct, args:"; val (thy, ((_, _, _, d, ts) : ori), ((_, _, _, fd, itm_) : itm)) =
17.45 +"~~~~~ fun geti_ct, args:"; val (thy, ((_, _, _, d, ts) : O_Model.single), ((_, _, _, fd, itm_) : I_Model.single)) =
17.46 (thy, ori, (hd icl));
17.47 "~~~~~ to return val:"; val xxx =
17.48 ( fd,
18.1 --- a/test/Tools/isac/Specify/calchead.sml Tue May 05 13:33:23 2020 +0200
18.2 +++ b/test/Tools/isac/Specify/calchead.sml Tue May 05 15:39:20 2020 +0200
18.3 @@ -323,7 +323,7 @@
18.4 val pI = ["LINEAR","system"];
18.5 val pats = (#ppc o get_pbt) pI;
18.6 "-a1-----------------------------------------------------";
18.7 -(*match_ags = fn : theory -> pat list -> term list -> ori list*)
18.8 +(*match_ags = fn : theory -> pat list -> term list -> O_Model.T*)
18.9 val xxx = match_ags @{theory "EqSystem"} pats ags;
18.10 "-a2-----------------------------------------------------";
18.11 case match_ags @{theory "Isac_Knowledge"} pats ags of
18.12 @@ -414,7 +414,7 @@
18.13 val pI = ["LINEAR","system"];
18.14 val pats = (#ppc o get_pbt) pI;
18.15 "-a1-----------------------------------------------------";
18.16 -(*match_ags = fn : theory -> pat list -> term list -> ori list*)
18.17 +(*match_ags = fn : theory -> pat list -> term list -> O_Model.T*)
18.18 val xxx = match_ags @{theory "EqSystem"} pats ags;
18.19 "-a2-----------------------------------------------------";
18.20 case match_ags @{theory "Isac_Knowledge"} pats ags of
19.1 --- a/test/Tools/isac/Specify/ptyps.sml Tue May 05 13:33:23 2020 +0200
19.2 +++ b/test/Tools/isac/Specify/ptyps.sml Tue May 05 15:39:20 2020 +0200
19.3 @@ -36,19 +36,19 @@
19.4 (*case 1: no refinement *)
19.5 val (d1,ts1) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");
19.6 val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)");
19.7 -val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list;
19.8 +val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;
19.9
19.10 (*case 2: refined to pbt without children *)
19.11 val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]");
19.12 -val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
19.13 +val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
19.14
19.15 (*case 3: refined to pbt with children *)
19.16 val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]");
19.17 -val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
19.18 +val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
19.19
19.20 (*case 4: refined to children (without child)*)
19.21 val (d3,ts3) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy");
19.22 -val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list;
19.23 +val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;
19.24
19.25 (*=================================================================
19.26 This test expects pbls at a certain position in the tree.
19.27 @@ -525,7 +525,7 @@
19.28 (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),
19.29 (8,[3],"#undef",Const (#,#),[Free #]),
19.30 (10,[3],"#undef",Const (#,#),[# $ #]),
19.31 - (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
19.32 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : O_Model.T list*)
19.33 "----------- fun match_pbl ---------------------------------------";
19.34 "----------- fun match_pbl ---------------------------------------";
19.35 "----------- fun match_pbl ---------------------------------------";