1.1 --- a/src/Tools/isac/Specify/i-model.sml Sat May 09 13:15:25 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/i-model.sml Sat May 09 15:31:15 2020 +0200
1.3 @@ -19,21 +19,45 @@
1.4 val single_to_string: Proof.context -> single -> string
1.5 val to_string: Proof.context -> T -> string
1.6
1.7 - val untouched : T -> bool
1.8 +(*/------- to I_Model from Chead -------\*)
1.9 + datatype additm = Add of single | Err of string
1.10 +(*val appl_add: m_field -> Proof.context -> O_Model.T -> Model_Pattern.T -> TermC.as_string -> T
1.11 + -> additm*)
1.12 +(*val appl_add: Proof.context -> m_field -> O_Model.T ->
1.13 + T -> Model_Pattern.T -> TermC.as_string -> additm*)
1.14 + val add_single: Proof.context -> m_field -> O_Model.T ->
1.15 + T -> Model_Pattern.T -> TermC.as_string -> additm
1.16 +(*\------- to I_Model from Chead -------/*)
1.17
1.18 - val d_in : feedback -> term
1.19 - val ts_in : feedback -> term list
1.20 - val vars_of : T -> term list
1.21 - val max_vt : T -> int
1.22 - val all_ts_in : feedback list -> term list
1.23 + val untouched: T -> bool
1.24 +
1.25 + val d_in: feedback -> term
1.26 + val ts_in: feedback -> term list
1.27 + val vars_of: T -> term list
1.28 + val max_vt: T -> int
1.29 + val all_ts_in: feedback list -> term list
1.30 val vts_in: T -> int list
1.31
1.32 - val mk_env : T -> (term * term) list
1.33 - val penvval_in : feedback -> term list
1.34 + val mk_env: T -> (term * term) list
1.35 + val penvval_in: feedback -> term list
1.36 +
1.37 +(*/------- to I_Model from Model -------\*)
1.38 + val pbl_ids': term -> term list -> term list
1.39 +(*\------- to I_Model from Model -------/*)
1.40 +
1.41 +(*/------- to I_Model from Chead -------\*)
1.42 + val is_known: Proof.context -> string -> O_Model.T -> term -> string * O_Model.single * term list
1.43 + val is_notyet_input : Proof.context -> T -> term list -> O_Model.single -> ('a * (term * term)) list
1.44 + -> string * single
1.45 + val dsc_unknown: term
1.46 +(*\------- to I_Model from Chead -------/*)
1.47 +
1.48 +
1.49 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.50 - (* NONE *)
1.51 + val dts2str: term * (term list) -> string
1.52 + val eq1: ''a -> 'b * (''a * 'c) -> bool
1.53 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.54 - (* NONE *)
1.55 + val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
1.56 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.57 end
1.58
1.59 @@ -87,7 +111,6 @@
1.60 FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
1.61 fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : single -> int)) itms);
1.62
1.63 -
1.64 (* find most frequent variant v in itms *)
1.65 fun vts_in itms = (distinct o flat o (map #2)) (itms: T);
1.66
1.67 @@ -141,25 +164,219 @@
1.68
1.69 val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
1.70 fun d_in (Cor ((d ,_), _)) = d
1.71 - | d_in (Syn c) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
1.72 - | d_in (Typ c) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
1.73 + | d_in (Syn _) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
1.74 + | d_in (Typ _) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
1.75 | d_in (Inc ((d, _), _)) = d
1.76 | d_in (Sup (d, _)) = d
1.77 | d_in (Mis (d, _)) = d
1.78 | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
1.79
1.80 fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
1.81 -(**)
1.82 -fun penvval_in (Cor ((d, _), (_, ts))) = [Input_Descript.join'''' (d,ts)]
1.83 - | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
1.84 - | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
1.85 +fun penvval_in (Cor ((d, _), (_, ts))) = [Input_Descript.join'''' (d, ts)]
1.86 + | penvval_in (Syn (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
1.87 + | penvval_in (Typ (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
1.88 | penvval_in (Inc (_, (_, ts))) = ts
1.89 - | penvval_in (Sup dts) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
1.90 - | penvval_in (Mis (d, t)) = ((*tracing ("*** penvval_in: Mis " ^
1.91 + | penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
1.92 + | penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^
1.93 pair2str(UnparseC.term d, UnparseC.term t));*) [])
1.94 | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
1.95 -(**)
1.96
1.97 fun vars_of itms = itms |> mk_env |> map snd
1.98
1.99 +
1.100 +(*/------- to I_Model from Chead -------\*)
1.101 +(* to an input (d,ts) find the according ori and insert the ts)
1.102 + WN.11.03: + dont take first inter<>[] *)
1.103 +fun seek_oridts ctxt sel (d, ts) [] =
1.104 + ("seek_oridts: input ('" ^
1.105 + (UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts))) ^ "') not found in oris (typed)",
1.106 + (0, [], sel, d, ts),
1.107 + [])
1.108 + | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
1.109 + if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
1.110 + then ("", (id, vat, sel, d, inter op = ts ts'), ts')
1.111 + else seek_oridts ctxt sel (d, ts) oris
1.112 +
1.113 +fun test_types ctxt (d,ts) =
1.114 + let
1.115 + val opt = (try Input_Descript.join) (d, ts)
1.116 + val msg = case opt of
1.117 + SOME _ => ""
1.118 + | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^
1.119 + (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts ^ " is illtyped")
1.120 + in msg end
1.121 +
1.122 +(* to an input (_,ts) find the according ori and insert the ts *)
1.123 +fun seek_orits ctxt _ ts [] =
1.124 + ("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) ts) ^
1.125 + "') not found in oris (typed)", O_Model.single_empty, [])
1.126 + | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) =
1.127 + if sel = sel' andalso (inter op = ts ts') <> []
1.128 + then
1.129 + if sel = sel'
1.130 + then ("", (id, vat, sel, d, inter op = ts ts'), ts')
1.131 + else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, O_Model.single_empty, [])
1.132 + else seek_orits ctxt sel ts oris
1.133 +
1.134 +(* make a term 'typeless' for comparing with another 'typeless' term;
1.135 + 'type-less' usually is illtyped *)
1.136 +fun typeless (Const (s, _)) = (Const (s, TermC.typ_empty))
1.137 + | typeless (Free (s, _)) = (Free (s, TermC.typ_empty))
1.138 + | typeless (Var (n, _)) = (Var (n, TermC.typ_empty))
1.139 + | typeless (Bound i) = (Bound i)
1.140 + | typeless (Abs (s, _,t)) = Abs(s, TermC.typ_empty, typeless t)
1.141 + | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
1.142 +
1.143 +(* is the term t input (or taken from fmz) known in oris ?
1.144 + give feedback on all(?) strange input;
1.145 + return _all_ terms already input to this item (e.g. valuesFor a,b) *)
1.146 +fun is_known ctxt sel ori t =
1.147 + let
1.148 + val ots = (distinct o flat o (map #5)) ori
1.149 + val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
1.150 + val (d, ts) = Input_Descript.split t
1.151 + val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
1.152 + in
1.153 + if (subtract op = oids ids) <> []
1.154 + then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", O_Model.single_empty, [])
1.155 + else
1.156 + if d = TermC.empty
1.157 + then
1.158 + if not (subset op = (map typeless ts, map typeless ots))
1.159 + then ("terms '" ^ (strs2str' o (map (UnparseC.term_in_ctxt ctxt))) ts ^
1.160 + "' not in example (typeless)", O_Model.single_empty, [])
1.161 + else
1.162 + (case seek_orits ctxt sel ts ori of
1.163 + ("", ori_ as (_,_,_,d,ts), all) =>
1.164 + (case test_types ctxt (d,ts) of
1.165 + "" => ("", ori_, all)
1.166 + | msg => (msg, O_Model.single_empty, []))
1.167 + | (msg, _, _) => (msg, O_Model.single_empty, []))
1.168 + else
1.169 + if member op = (map #4 ori) d
1.170 + then seek_oridts ctxt sel (d, ts) ori
1.171 + else (UnparseC.term_in_ctxt ctxt d ^ " not in example", (0, [], sel, d, ts), [])
1.172 + end
1.173 +(*\------- to I_Model from Chead -------/*)
1.174 +
1.175 +(*/------- to I_Model from Specify -------\*)
1.176 +val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
1.177 +(*\------- to I_Model from Specify -------/*)
1.178 +
1.179 +(*/------- to I_Model from Model -------\*)
1.180 +(* 9.5.03 penv postponed: pbl_ids' *)
1.181 +fun pbl_ids' d vs = [Input_Descript.join'''' (d, vs)];
1.182 +(*\------- to I_Model from Model -------/*)
1.183 +
1.184 +(*/------- to I_Model from Chead -------\*)
1.185 +(* update the itm_ already input, all..from ori *)
1.186 +fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
1.187 + let
1.188 + val ts' = union op = (ts_in itm_) ts;
1.189 + val pval =pbl_ids' d ts'
1.190 + (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
1.191 + val complete = if eq_set op = (ts', all) then true else false
1.192 + in
1.193 + case itm_ of
1.194 + (Cor _) =>
1.195 + (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
1.196 + else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
1.197 + | (Syn c) => error ("ori_2itm wants to overwrite " ^ c)
1.198 + | (Typ c) => error ("ori_2itm wants to overwrite " ^ c)
1.199 + | (Inc _) =>
1.200 + if complete
1.201 + then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
1.202 + else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
1.203 + | (Sup (d,ts')) => (*4.9.01 lost env*)
1.204 + (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
1.205 + (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
1.206 + (* 28.1.00: not completely clear ---^^^ etc.*)
1.207 + | (Mis _) => (* 4.9.01: Mis just copied *)
1.208 + if complete
1.209 + then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
1.210 + else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
1.211 + | i => error ("ori_2itm: uncovered case of "^ feedback_to_string' i)
1.212 + end
1.213 +
1.214 +fun eq1 d (_, (d', _)) = (d = d')
1.215 +fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_)
1.216 +
1.217 +(* 'all' ts from ori; ts is the input; (ori carries rest of info)
1.218 + 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
1.219 + pval: value for problem-environment _NOT_ checked for 'inter' --
1.220 + -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
1.221 + (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
1.222 +(*. is_input ori itms <=>
1.223 + EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
1.224 + (2) ori(ts) subset itm(ts) --- Err "already input"
1.225 + (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
1.226 + (4) -"- <> empty --- new: ori(ts) \\ inter .*)
1.227 +fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
1.228 + case find_first (eq1 d) pbt of
1.229 + SOME (_, (_, pid)) =>
1.230 + (case find_first (eq3 f d) itms of
1.231 + SOME (_,_,_,_,itm_) =>
1.232 + let val ts' = inter op = (ts_in itm_) ts
1.233 + in
1.234 + if subset op = (ts, ts')
1.235 + then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", empty) (*2*)
1.236 + else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
1.237 + end
1.238 + | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
1.239 + | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
1.240 +
1.241 +datatype additm =
1.242 + Add of single (* return-value of add_single *)
1.243 +| Err of string (* error-message *)
1.244 +
1.245 +(*
1.246 + Create feedback for input of TermC.as_string to m_field;
1.247 + check w.r.t. O_Model.T and Model_Pattern.T.
1.248 + In case of O_Model.T = [] (i.e. no data for user-guidance from Formalise.T)
1.249 + add_single is extremely permissive.
1.250 +*)
1.251 +fun add_single ctxt m_field [] i_model m_patt ct =
1.252 + let
1.253 + val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
1.254 + in
1.255 + case TermC.parseNEW ctxt ct of
1.256 + NONE => Add (i, [], false, m_field, Syn ct)
1.257 + | SOME t =>
1.258 + let
1.259 + val (d, ts) = Input_Descript.split t
1.260 + in
1.261 + if d = TermC.empty then
1.262 + Add (i, [], false, m_field, Mis (dsc_unknown, hd ts))
1.263 + else
1.264 + (case find_first (eq1 d) m_patt of
1.265 + NONE => Add (i, [], true, m_field, Sup (d,ts))
1.266 + | SOME (f, (_, id)) =>
1.267 + let
1.268 + fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0
1.269 + in
1.270 + case find_first (eq2 d) i_model of
1.271 + NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
1.272 + | SOME (i', _, _, _, itm_) =>
1.273 + if Input_Descript.for_list d then
1.274 + let
1.275 + val in_itm = ts_in itm_
1.276 + val ts' = union op = ts in_itm
1.277 + val i'' = if in_itm = [] then i else i'
1.278 + in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end
1.279 + else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))
1.280 + end)
1.281 + end
1.282 + end
1.283 + | add_single ctxt m_field o_model i_model m_patt str =
1.284 + case TermC.parseNEW ctxt str of
1.285 + NONE => Err ("add_single: syntax error in '" ^ str ^ "'")
1.286 + | SOME t =>
1.287 + case is_known ctxt m_field o_model t of
1.288 + ("", ori', all) =>
1.289 + (case is_notyet_input ctxt i_model all ori' m_patt of
1.290 + ("", itm) => Add itm
1.291 + | (msg, _) => Err ("[error] add_single: is_notyet_input: " ^ msg))
1.292 + | (msg, _, _) => Err ("[error] add_single: is_known: " ^ msg);
1.293 +(*\------- to I_Model from Chead -------/*)
1.294 +
1.295 (**)end(**);
1.296 \ No newline at end of file