1 (* Title: Specify/input-calchead.sml
3 (c) due to copyright terms
6 signature INPUT_CALCHEAD =
8 datatype iitem = Find of UnparseC.cterm' list | Given of UnparseC.cterm' list | Relate of UnparseC.cterm' list
9 type imodel = iitem list
10 type icalhd = Pos.pos' * UnparseC.cterm' * imodel * Pos.pos_ * Celem.spec
11 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
12 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
17 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
19 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
21 val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list ->
22 ('c * ''b * bool * 'd * Model.itm_) list
25 structure In_Chead(**): INPUT_CALCHEAD(**) =
28 (*** handle an input by CAS-command ***)
30 fun dtss2itm_ ppc (d, ts) =
32 val (f, (d, id)) = the (find_first ((curry op= d) o
33 (#1: (term * term) -> term) o
34 (#2: Celem.pbt_ -> (term * term))) ppc)
36 ([1], true, f, Model.Cor ((d, ts), (id, ts)))
39 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
41 fun cas_input_ ((dI, pI, mI): Celem.spec) dtss = (*WN110515 reconsider thy..ctxt*)
43 val thy = Celem.assoc_thy dI
44 val {ppc, ...} = Specify.get_pbt pI
45 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
46 val its = Specify.add_id its_
47 val pits = map flattup2 its
52 case Specify.refine_pbl thy pI pits of
53 SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI)
54 | NONE => (pI, (hd o #met o Specify.get_pbt) pI)
55 val {ppc, pre, prls, ...} = Specify.get_met mI
56 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
57 val its = Specify.add_id its_
58 val mits = map flattup2 its
59 val pre = Stool.check_preconds thy prls pre mits
60 val ctxt = Proof_Context.init_global thy
61 in (pI, pits, mI, mits, pre, ctxt) end;
64 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
67 val (h, argl) = strip_comb hdt
69 case assoc_cas (Celem.assoc_thy "Isac_Knowledge") h of
71 | SOME (spec as (dI,_,_), argl2dtss) =>
73 val dtss = argl2dtss argl
74 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
75 val spec = (dI, pI, mI)
76 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
77 ([], Celem.e_spec) ([], Celem.e_spec, hdt, ctxt)
78 val pt = Ctree.update_spec pt [] spec
79 val pt = Ctree.update_pbl pt [] pits
80 val pt = Ctree.update_met pt [] mits
82 SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Ctree.ocalhd)
87 (*** handle an input calc-head ***)
90 Given of UnparseC.cterm' list
91 (*Where is never input*)
92 | Find of UnparseC.cterm' list
93 | Relate of UnparseC.cterm' list
95 type imodel = iitem list
97 (*calc-head as input*)
99 Pos.pos' * (*the position of the calc-head in the calc-tree*)
100 UnparseC.cterm' * (*the headline*)
101 imodel * (*the model (without Find) of the calc-head*)
102 Pos.pos_ * (*model belongs to Pbl or Met*)
103 Celem.spec; (*specification: domID, pblID, metID*)
104 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Celem.e_spec)
106 fun is_casinput (hdf : UnparseC.cterm') ((fmz_, spec) : Selem.fmz) =
107 hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec
109 (* re-parse itms with a new thy and prepare for checking with ori list *)
110 fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =
111 (let val t = Model.comp_dts (d, ts)
112 val _ = (UnparseC.term_to_string''' dI t)
113 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
115 handle _ => (i, v, false, f, Model.Syn (UnparseC.term2str TermC.empty (*t ..(t) has not been declared*))))
116 | parsitm dI (i, v, b, f, Model.Syn str) =
117 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
118 in (i, v, b ,f, Model.Par str) end
119 handle _ => (i, v, b, f, Model.Syn str))
120 | parsitm dI (i, v, b, f, Model.Typ str) =
121 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
122 in (i, v, b, f, Model.Par str) end
123 handle _ => (i, v, b, f, Model.Syn str))
124 | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) =
125 (let val t = Model.comp_dts (d,ts);
126 val _ = UnparseC.term_to_string''' dI t;
127 (*this ^ should raise the exn on unability of re-parsing dts*)
129 handle _ => (i, v, false, f, Model.Syn (UnparseC.term2str TermC.empty (*t ..(t) has not been declared*))))
130 | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) =
131 (let val t = Model.comp_dts (d,ts);
132 val _ = UnparseC.term_to_string''' dI t;
133 (*this ^ should raise the exn on unability of re-parsing dts*)
135 handle _ => (i, v, false, f, Model.Syn (UnparseC.term2str TermC.empty (*t ..(t) has not been declared*))))
136 | parsitm dI (itm as (i, v, _, f, Model.Mis (d, t'))) =
138 val _ = UnparseC.term_to_string''' dI t;
139 (*this ^ should raise the exn on unability of re-parsing dts*)
141 handle _ => (i, v, false, f, Model.Syn (UnparseC.term2str TermC.empty (*t ..(t) has not been declared*))))
142 | parsitm dI (itm as (_, _, _, _, Model.Par _)) =
143 error ("parsitm (" ^ Model.itm2str_ (ThyC.thy2ctxt dI) itm ^ "): Par should be internal");
145 (*separate a list to a pair of elements that do NOT satisfy the predicate,
146 and of elements that satisfy the predicate, i.e. (false, true)*)
147 fun filter_sep pred xs =
150 | filt (a, b) (x :: xs) =
152 then filt (a, b @ [x]) xs
153 else filt (a @ [x], b) xs
154 in filt ([], []) xs end;
155 fun is_Par (_, _, _, _, Model.Par _) = true
158 fun is_e_ts [] = true
159 | is_e_ts [Const ("List.list.Nil", _)] = true
162 (* WN.9.11.03 copied from fun appl_add *)
163 fun appl_add' dI oris ppc pbt (sel, ct) =
165 val ctxt = Celem.assoc_thy dI |> ThyC.thy2ctxt;
167 case TermC.parseNEW ctxt ct of
168 NONE => (0, [], false, sel, Model.Syn ct)
170 (case Chead.is_known ctxt sel oris t of
172 (case Chead.is_notyet_input ctxt ppc all ori' pbt of
174 | (msg,_) => error ("appl_add': " ^ msg))
175 | (_, (i, v, _, d, ts), _) =>
177 then (i, v, false, sel, Model.Inc ((d, ts), (TermC.empty, [])))
178 else (i, v, false, sel, Model.Sup (d, ts)))
181 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
182 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
183 fun fstr2itm_ thy pbt (f, str) =
185 val topt = TermC.parse thy str
188 NONE => ([], false, f, Model.Syn str)
191 val (d, ts) = (Model.split_dts o Thm.term_of) ct
192 val popt = find_first (eq7 (f, d)) pbt
195 NONE => ([1](*??*), true(*??*), f, Model.Sup (d, ts))
196 | SOME (f, (d, id)) => ([1], true, f, Model.Cor ((d, ts), (id, ts)))
200 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
201 fun unknown_expl dI pbt selcts =
203 val thy = Celem.assoc_thy dI
204 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
205 val its = Specify.add_id its_
206 in map flattup2 its end
208 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
209 appl_add': generate 1 item
210 appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
211 appl_add' . is_notyet_input: compare with items in model already input
212 insert_ppc': insert this 1 item*)
213 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
214 (*already present itms in model are being overwritten*)
215 | appl_adds _ _ ppc _ [] = ppc
216 | appl_adds dI oris ppc pbt (selct :: ss) =
217 let val itm = appl_add' dI oris ppc pbt selct;
218 in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end
220 fun oris2itms _ _ [] = [] (* WN161130: similar in ptyps ?!? *)
221 | oris2itms pbt vat ((i, v, f, d, ts) :: os) =
223 then (i, v, true, f, Model.Cor ((d, ts), (TermC.empty, []))) :: (oris2itms pbt vat os)
224 else oris2itms pbt vat os
226 fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
227 | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itm)
228 fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
229 | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
230 | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
231 | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, Model.comp_dts'' (d,ts))
232 | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
233 | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, UnparseC.term2str (d $ t))
234 | itms2fstr (itm as (_, _, _, _, Model.Par _)) =
235 error ("parsitm (" ^ Model.itm2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal");
237 fun imodel2fstr iitems =
240 | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
241 | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
242 | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
243 in xxx [] iitems end;
245 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
246 fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
248 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
249 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
250 spec = sspec as (sdI, spI, smI), probl, meth, ...}
251 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
252 | _ => error "input_icalhd: uncovered case of get_obj I pt p"
253 in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf))
254 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
255 let val (pos_, pits, mits) =
257 then let val its = map (parsitm (Celem.assoc_thy dI)) probl;
258 val (its, trms) = filter_sep is_Par its;
259 val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
260 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
263 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
265 let val pbt = (#ppc o Specify.get_pbt) pI
266 val dI' = #1 (Chead.some_spec ospec spec)
267 val oris = if pI = #2 ospec then oris
268 else Specify.prep_ori fmz_(Celem.assoc_thy"Isac_Knowledge") pbt |> #1;
269 in (Pos.Pbl, appl_adds dI' oris probl pbt
270 (map itms2fstr probl), meth) end
271 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
272 then let val met = (#ppc o Specify.get_met) mI
273 val mits = Chead.complete_metitms oris probl meth met
274 in if foldl and_ (true, map #3 mits)
275 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
277 else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
278 ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
279 (imodel2fstr imodel), meth)
280 val pt = Ctree.update_spec pt p spec;
282 then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
283 val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls where_ pits
284 in (Ctree.update_pbl pt p pits,
285 (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
287 else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
288 val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls pre mits
289 in (Ctree.update_met pt p mits,
290 (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
294 | input_icalhd _ (_, _, _, _(*Met*), _) = error "input_icalhd Met not impl."