1 (* Title: Specify/input-calchead.sml
3 (c) due to copyright terms
5 This will be dropped at switch to Isabelle/PIDE.
8 signature INPUT_SPECIFICATION =
11 Find of TermC.as_string list
12 | Given of TermC.as_string list
13 | Relate of TermC.as_string list
14 type imodel = iitem list
15 type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
16 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
20 val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
21 string * TermC.as_string -> I_Model.single
22 val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
23 (string * TermC.as_string) list -> I_Model.T
25 val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
26 val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list
27 val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
28 int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
29 val imodel2fstr: iitem list -> (string * TermC.as_string) list
30 val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
31 val is_e_ts: term list -> bool
32 val itms2fstr: I_Model.single -> string * string
33 val par2fstr: I_Model.single -> string * TermC.as_string
34 val parsitm: theory -> I_Model.single -> I_Model.single
35 val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
36 (''a * string) list ->
37 (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
42 structure P_Specific(**): INPUT_SPECIFICATION(**) =
46 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
48 (** handle an input P_Specific'action **)
51 Given of TermC.as_string list
52 (*Where is still not input*)
53 | Find of TermC.as_string list
54 | Relate of TermC.as_string list
56 type imodel = iitem list
59 Pos.pos' * (* the position in Ctree *)
60 TermC.as_string * (* the headline shown on Calc.T *)
61 imodel * (* the model *)
62 Pos.pos_ * (* model belongs to Problem or Method *)
63 References.T; (* into Know_Store *)
64 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
66 (* re-parse itms with a new thy and prepare for checking with ori list *)
67 fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
68 (let val t = Input_Descript.join (d, ts)
69 val _ = (UnparseC.term_in_thy dI t)
70 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
72 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
73 | parsitm dI (i, v, b, f, I_Model.Syn str) =
74 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
75 in (i, v, b ,f, I_Model.Par str) end
76 handle _ => (i, v, b, f, I_Model.Syn str))
77 | parsitm dI (i, v, b, f, I_Model.Typ str) =
78 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
79 in (i, v, b, f, I_Model.Par str) end
80 handle _ => (i, v, b, f, I_Model.Syn str))
81 | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
82 (let val t = Input_Descript.join (d,ts);
83 val _ = UnparseC.term_in_thy dI t;
84 (*this ^ should raise the exn on unability of re-parsing dts*)
86 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
87 | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
88 (let val t = Input_Descript.join (d,ts);
89 val _ = UnparseC.term_in_thy dI t;
90 (*this ^ should raise the exn on unability of re-parsing dts*)
92 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
93 | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
95 val _ = UnparseC.term_in_thy dI t;
96 (*this ^ should raise the exn on unability of re-parsing dts*)
98 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
99 | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) =
100 raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
102 (*separate a list to a pair of elements that do NOT satisfy the predicate,
103 and of elements that satisfy the predicate, i.e. (false, true)*)
104 fun filter_sep pred xs =
107 | filt (a, b) (x :: xs) =
109 then filt (a, b @ [x]) xs
110 else filt (a @ [x], b) xs
111 in filt ([], []) xs end;
112 fun is_Par (_, _, _, _, I_Model.Par _) = true
115 fun is_e_ts [] = true
116 | is_e_ts [Const ("List.list.Nil", _)] = true
119 (* WN.9.11.03 copied from fun appl_add *)
120 fun appl_add' dI oris ppc pbt (sel, ct) =
122 val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;
124 case TermC.parseNEW ctxt ct of
125 NONE => (0, [], false, sel, I_Model.Syn ct)
127 (case I_Model.is_known ctxt sel oris t of
129 (case I_Model.is_notyet_input ctxt ppc all ori' pbt of
131 | (msg,_) => raise ERROR ("appl_add': " ^ msg))
132 | (_, (i, v, _, d, ts), _) =>
134 then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
135 else (i, v, false, sel, I_Model.Sup (d, ts)))
138 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
139 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
140 fun fstr2itm_ thy pbt (f, str) =
142 val topt = TermC.parse thy str
145 NONE => ([], false, f, I_Model.Syn str)
148 val (d, ts) = (Input_Descript.split o Thm.term_of) ct
149 val popt = find_first (eq7 (f, d)) pbt
152 NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
153 | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
157 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
158 fun unknown_expl dI pbt selcts =
160 val thy = ThyC.get_theory dI
161 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
162 val its = O_Model.add_id its_
163 in map flattup2 its end
165 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
166 appl_add': generate 1 item
167 appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
168 appl_add' . is_notyet_input: compare with items in model already input
169 insert_ppc': insert this 1 item*)
170 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
171 (*already present itms in model are being overwritten*)
172 | appl_adds _ _ ppc _ [] = ppc
173 | appl_adds dI oris ppc pbt (selct :: ss) =
174 let val itm = appl_add' dI oris ppc pbt selct;
175 in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end
177 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
178 | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
179 fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
180 | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
181 | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
182 | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
183 | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
184 | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
185 | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =
186 raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
188 fun imodel2fstr iitems =
191 | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
192 | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
193 | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
194 in xxx [] iitems end;
196 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
197 fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
199 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
200 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
201 spec = sspec as (sdI, spI, smI), probl, meth, ...}
202 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
203 | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
204 in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf))
205 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
206 let val (pos_, pits, mits) =
208 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
209 val (its, trms) = filter_sep is_Par its;
210 val pbt = (#ppc o Problem.from_store) (#2 (References.select ospec sspec))
211 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
214 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
216 let val pbt = (#ppc o Problem.from_store) pI
217 val dI' = #1 (References.select ospec spec)
218 val oris = if pI = #2 ospec then oris
219 else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
220 in (Pos.Pbl, appl_adds dI' oris probl pbt
221 (map itms2fstr probl), meth) end
222 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
223 then let val met = (#ppc o Method.from_store) mI
224 val mits = Specification.complete_metitms oris probl meth met
225 in if foldl and_ (true, map #3 mits)
226 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
228 else (Pos.Pbl, appl_adds (#1 (References.select ospec spec)) oris [(*!!!*)]
229 ((#ppc o Problem.from_store) (#2 (References.select ospec spec)))
230 (imodel2fstr imodel), meth)
231 val pt = Ctree.update_spec pt p spec;
233 then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))
234 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
235 in (Ctree.update_pbl pt p pits,
236 (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
238 else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec))
239 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
240 in (Ctree.update_met pt p mits,
241 (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
245 | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."