1 (* Title: Specify/input-calchead.sml
3 (c) due to copyright terms
5 This will be dropped at switch to Isabelle/PIDE .
8 signature PRESENTATION_SPECIFICATION =
11 (*/------- rename -------\*)
13 Find of TermC.as_string list
14 | Given of TermC.as_string list
15 | Relate of TermC.as_string list
16 type imodel = iitem list
17 type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
19 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * SpecificationC.T
21 val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
22 string * TermC.as_string -> I_Model.single
23 val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
24 (string * TermC.as_string) list -> I_Model.T
25 val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
26 val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
27 int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
28 val imodel2fstr: iitem list -> (string * TermC.as_string) list
29 val is_e_ts: term list -> bool
30 val itms2fstr: Proof.context -> I_Model.single -> string * string
31 val par2fstr: I_Model.single -> string * TermC.as_string
32 val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T*)
33 (''a * string) list ->
34 (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T*)
36 (*\------- rename -------/*)
40 structure P_Spec(**): PRESENTATION_SPECIFICATION(**) =
44 type record = {thy_id: ThyC.id, pbl_id: Problem.id, (* headline of Problem *)
45 givens: TermC.as_string list, wheres: TermC.as_string list, (* Model.T *)
46 find: TermC.as_string, relates: TermC.as_string list,
47 rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: MethodC.id} (* References.T *)
49 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
51 (** handle an input P_Specific'action **)
54 Given of TermC.as_string list
55 (*Where is still not input*)
56 | Find of TermC.as_string list
57 | Relate of TermC.as_string list
59 type imodel = iitem list
62 Pos.pos' * (* the position in Ctree *)
63 TermC.as_string * (* the headline shown on Calc.T *)
64 imodel * (* the model *)
65 Pos.pos_ * (* model belongs to Problem or MethodC *)
66 References.T; (* into Know_Store *)
67 val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
70 | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true
73 (* WN.9.11.03 copied from fun appl_add *)
74 fun appl_add' dI oris model pbt (sel, ct) =
76 val ctxt = Know_Store.get_via_last_thy dI |> Proof_Context.init_global;
78 (*/------------ replace by ParseC.term_position ------------------\*)
79 case ParseC.term_opt ctxt ct of
80 (*\------------ replace by ParseC.term_position ------------------/*)
81 NONE => (0, [], false, sel, I_Model.Syn ct)
83 (case O_Model.contains ctxt sel oris t of
85 (case I_Model.is_notyet_input ctxt model all ori' pbt of
87 | (msg,_) => raise ERROR ("appl_add': " ^ msg))
88 | (_, (i, v, _, d, ts), _) =>
90 then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
91 else (i, v, false, sel, I_Model.Sup (d, ts)))
94 (* generate preliminary itm_ from a string (with field "#Given" etc.) *)
95 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
96 fun fstr2itm_ thy pbt (f, str) =
98 (*/------------ replace by ParseC.term_position ? ------------\*)
99 val topt = ParseC.term_opt (Proof_Context.init_global thy) str
100 (*\------------ replace by ParseC.term_position ? ------------/*)
103 NONE => ([], false, f, I_Model.Syn str)
106 val (d, ts) = Input_Descript.split ct
107 val popt = find_first (eq7 (f, d)) pbt
110 NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
111 | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
115 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
116 fun unknown_expl dI pbt selcts =
118 val thy = Know_Store.get_via_last_thy dI
119 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
120 val its = O_Model.add_enumerate its_
121 in map flattup2 its end
123 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
124 appl_add': generate 1 item
125 appl_add' . contains: parse, get data from oris (vats, all (elems if list)..)
126 appl_add' . is_notyet_input: compare with items in model already input
127 insert_ppc': insert this 1 item*)
128 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
129 (*already present itms in model are being overwritten*)
130 | appl_adds _ _ model _ [] = model
131 | appl_adds dI oris model pbt (selct :: ss) =
132 let val itm = appl_add' dI oris model pbt selct;
133 in appl_adds dI oris (I_Model.add itm model) pbt ss end
135 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
136 | par2fstr itm = raise ERROR ("par2fstr: called with " ^
137 I_Model.single_to_string (ContextC.for_ERROR ()) itm)
138 fun itms2fstr _ (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
139 | itms2fstr _ (_, _, _, f, I_Model.Syn str) = (f, str)
140 | itms2fstr _ (_, _, _, f, I_Model.Typ str) = (f, str)
141 | itms2fstr _ (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
142 | itms2fstr _ (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
143 | itms2fstr ctxt (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term ctxt (d $ t))
144 | itms2fstr ctxt (itm as (_, _, _, _, I_Model.Par _)) =
145 raise ERROR ("itms2fstr (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
147 fun imodel2fstr iitems =
150 | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
151 | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
152 | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
153 in xxx [] iitems end;
155 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
156 fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
158 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
159 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
160 spec = sspec as (sdI, spI, smI), probl, meth, ...}
161 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
162 | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
163 val thy = Know_Store.get_via_last_thy dI
164 val ctxt = Proof_Context.init_global thy
165 in if CAS_Cmd.is_from hdf fmz
166 then the (CAS_Cmd.input (ParseC.term_opt ctxt hdf |> the))
168 let val (pos_, pits, mits) =
170 then let (* eliminated for PIDE turn 11: take Position into I_Model
171 val its = map (parsitm thy) probl;
172 val (its, trms) = filter_sep is_Par its;*)
173 val pbt = (#model o Problem.from_store ctxt)
174 (#2 (References.select_input ospec sspec))
175 in (Pos.Pbl, appl_adds dI oris [](*its*) pbt (map par2fstr [](*trms*)), meth) end
178 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
180 val pbt = (#model o Problem.from_store ctxt) pI
181 val dI' = #1 (References.select_input ospec spec)
183 if pI = #2 ospec then oris
184 else O_Model.init thy fmz_ pbt |> #1;
185 in (Pos.Pbl, appl_adds dI' oris probl pbt
186 (map (itms2fstr ctxt) probl), meth) end
187 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
189 val (_, mits) = I_Model.s_make_complete ctxt oris
190 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (pI, mI)
191 in if foldl and_ (true, map #3 mits)
192 then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)
193 else (Pos.Met, probl, I_Model.TEST_to_OLD mits)
195 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
196 ((#model o Problem.from_store ctxt)
197 (#2 (References.select_input ospec spec)))
198 (imodel2fstr imodel), meth)
199 val pt = Ctree.update_spec pt p spec;
203 val {where_rls, where_, model, ...} = Problem.from_store ctxt
204 (#2 (References.select_input ospec spec))
205 val (_, where_) = Pre_Conds.check ctxt where_rls where_
206 (model, I_Model.OLD_to_TEST pits)
207 in (Ctree.update_pbl pt p pits,
208 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec))
212 val {where_rls,where_, model, ...} = MethodC.from_store ctxt
213 (#3 (References.select_input ospec spec))
214 val (_, where_) = Pre_Conds.check ctxt where_rls where_
215 (model, I_Model.OLD_to_TEST mits)
216 in (Ctree.update_met pt p mits,
217 (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
221 | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."