1 (* Title: Specify/specification.sml
2 Author: Walther Neuper, Mathias Lehnfeld
3 (c) due to copyright terms
5 (* Survey on type fmz_ .. type ori .. type itm (in probl, meth) .. formal args of root-/SubProblem
6 and relations between respective list elements: #1#
7 fmz = [ dsc $ v......................................(dsc $ v)..]
8 root problem on pos = ([], _)
9 fmz_ = [(dsc, v).......................................(dsc, v)..]
11 oris = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)...........(dsc, v)..]
12 \<down> #Given,..,#Relate #Find #undef............#undef \<down>
13 \<down> \<down> \<down> \<down>
14 Specify_Problem + pbl.ppc= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
15 \<down> \<down> \<down> \<down>
16 itms = [(dsc, v)..(dsc, v),(dsc, v)] \<down> \<down> \<down>
17 int.modelling +Cor ++++++++++Cor +Cor \<down> \<down> \<down>
18 \<down> \<down> \<down> \<down>
19 Specify_Method + met.ppc= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
20 \<down> \<down> \<down> \<down>
21 itms = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)..(dsc, v)] \<down> \<down>
22 int.modelling +Cor ++++++Cor \<down> \<down>
23 form.args= [ id ..... id , /////// id ....... id ] \<down> \<down>
24 env = [(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
25 interpret code env = [(id, v)..(id, v),(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
26 ..extends env ^^^^^^^^^^^^^^^^ \<down> \<down> \<down> \<down> \<down>
27 \<down> \<down> \<down> \<down> \<down> \<down>
28 SubProblem on pos = ([2], _) \<down> \<down> \<down> \<down> \<down> \<down>
29 form.args= [id ................................ id ]\<down> \<down> \<down>
30 \<down> REAL..BOOL.. \<down> \<down> \<down>
31 \<down> \<down> \<down> \<down>
32 + met.ppc= [(dsc,id).......................(dsc,id)]\<down> \<down> \<down>
33 \<down> \<down> \<down> \<down> \<down>
34 oris = [(dsc, v)...................... (dsc, v) ........... (dsc, v)]\<down>
35 Specify_Problem, int.modelling, Specify_Method, interpret code as above #1# \<down>
37 SubProblem on pos = ([3, 4], _) \<down>
38 form.args= [id ...................... id ] \<down>
39 \<down> REAL..BOOL.. \<down>
40 + met.ppc= [(dsc,id).............(dsc,id)] \<down>
41 oris = [(dsc, v).............(dsc, v)...................(dsc, v)]
42 Specify_Problem, int.modelling, Specify_Method, interpret code as above #1#
45 (1) SubProblem implements sub-function calls such, that the arguments (+ pre- + post-condition)
46 of the functions become concern of interactive modelling.
47 (2) In Isac-terms, the above concerns the phases of modelling and
48 and of specifying (Specify_Problem, Specify_Method),
49 while stepwise construction of solutions is called solving.
50 The latter is supported by Lucas-Interpretation of the functions' body.
51 (3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem;
52 it is as complete as possible (this has been different up to now).
53 (4) itm list is initialised by pbl-ppc | met-pps and completed (Cor) by stepwise user input.
54 (5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,
55 add them to the model-pattern of met and let this input be done automatically;
56 respective items must be in fmz.
58 signature SPECIFICATION =
61 type T = Specification_Def.T
63 (*val reset: Calc.T -> Calc.T*)
64 val reset_calchead: Calc.T -> Calc.T
65 (*val get: Calc.T -> T*)
66 val get_ocalhd: Calc.T -> T
67 (*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
68 val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
69 (*val is_complete: Calc.T -> bool*)
70 val is_complete_mod: Calc.T -> bool
72 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
74 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
75 val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
76 val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
77 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
79 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
80 val variants_in: term list -> int
81 val is_untouched: I_Model.single -> bool
82 val is_list_type: typ -> bool
83 val parse_ok: I_Model.feedback list -> bool
84 val all_dsc_in: I_Model.feedback list -> term list
85 val chktyps: theory -> term list * term list -> term list (* only in old tests*)
86 val is_complete_modspec: Calc.T -> bool
87 val get_formress: (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
88 (string * Pos.pos' * term) list
89 val get_forms: (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
90 (string * Pos.pos' * term) list
94 structure Specification(** ): SPECIFICATION( **) =
98 type T = Specification_Def.T;
100 (* is the calchead complete ? *)
101 fun ocalhd_complete its pre (dI, pI, mI) =
102 foldl and_ (true, map #3 (its: I_Model.T)) andalso
103 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
104 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
106 (* get the number of variants in a problem in 'original',
107 assumes equal descriptions in immediate sequence *)
110 fun eq (x, y) = head_of x = head_of y
111 fun cnt _ [] _ n = ([n], [])
112 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
113 fun coll _ xs [] = xs
114 | coll eq xs (y :: ys) =
115 let val (n, ys') = cnt eq (y :: ys) y 0
116 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
117 val vts = subtract op = [1] (distinct (coll eq [] ts))
122 | _ => raise ERROR "different variants in formalization"
125 fun is_list_type (Type ("List.list", _)) = true
126 | is_list_type _ = false
127 fun is_parsed (I_Model.Syn _) = false
129 fun parse_ok its = foldl and_ (true, map is_parsed its)
131 fun all_dsc_in itm_s =
133 fun d_in (I_Model.Cor ((d, _), _)) = [d]
134 | d_in (I_Model.Syn _) = []
135 | d_in (I_Model.Typ _) = []
136 | d_in (I_Model.Inc ((d,_),_)) = [d]
137 | d_in (I_Model.Sup (d,_)) = [d]
138 | d_in (I_Model.Mis (d,_)) = [d]
139 | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
140 in (flat o (map d_in)) itm_s end;
142 (* get the first term in ts from ori *)
143 fun getr_ct thy (_, _, fd, d, ts) =
144 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
146 (* get a term from ori, notyet input in itm.
147 the term from ori is thrown back to a string in order to reuse
148 machinery for immediate input by the user. *)
149 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
150 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
152 (* in FE dsc, not dat: this is in itms ...*)
153 fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
154 | is_untouched _ = false
156 (* output the headline to a ppc *)
157 fun header p_ pI mI =
159 Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI)
160 | Pos.Met => Test_Out.Method mI
161 | pos => raise ERROR ("header called with "^ Pos.pos_2str pos)
163 fun make m_field (term_as_string, i_model) =
165 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
166 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
167 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
168 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
169 fun get (pt, (p, _)) =
170 case Ctree.get_obj I pt p of
171 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
172 => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
173 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
175 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
176 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
177 fun tag_form thy (formal, given) =
179 val gf = (head_of given) $ formal;
180 val _ = Thm.global_cterm_of thy gf
182 handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
183 " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
185 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
187 fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
188 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
189 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
190 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
191 | is_complete_mod (pt, pos as (p, Pos.Met)) =
192 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
193 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
194 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
195 | is_complete_mod (_, pos) =
196 raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
198 fun is_complete_modspec ptp = is_complete_mod ptp andalso References.are_complete ptp
201 (** get the formula from a ctree-node **)
203 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
204 take res from all other PrfObj's
205 Designed for interSteps, outcommented 04 in favour of calcChangedEvent
207 fun formres p (Ctree.Nd (Ctree.PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
208 [("headline", (p, Pos.Frm), h), ("stepform", (p, Pos.Res), r)]
209 | formres p (Ctree.Nd (Ctree.PrfObj {form, result = (r, _), ...}, _)) =
210 [("stepform", (p, Pos.Frm), form), ("stepform", (p, Pos.Res), r)]
211 | formres _ _ = raise ERROR "formres: uncovered definition"
212 fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) =
213 [("stepform", (p, Pos.Res), r)]
214 | form _ _ = raise ERROR "form: uncovered definition"
216 (* assumes to take whole level, in particular hd -- for use in interSteps *)
217 fun get_formress fs _ [] = flat fs
218 | get_formress fs p (nd::nds) =
219 (* start with 'form+res' and continue with trying 'res' only*)
220 get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
221 and get_forms fs _ [] = flat fs
222 | get_forms fs p (nd::nds) =
224 (* start again with 'form+res' ///ugly repeat with Check_elementwise
225 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
226 then get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
227 (* continue with trying 'res' only*)
228 else get_forms (fs @ [form p nd]) (Pos.lev_on p) nds;
231 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
232 fun get_ocalhd (pt, (p, Pos.Pbl)) =
234 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
235 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
236 | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"
237 val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))
238 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
240 (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
242 | get_ocalhd (pt, (p, Pos.Met)) =
244 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
245 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
246 | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"
247 val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))
248 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
250 (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
252 | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"
254 (* at the activeFormula set the Specification
255 to empty and return a CalcHead;
256 the 'origin' remains (for reconstructing all that) *)
257 fun reset_calchead (pt, (p,_)) =
259 val () = case Ctree.get_obj I pt p of
261 | _ => raise ERROR "reset_calchead: uncovered case get_obj"
262 val pt = Ctree.update_pbl pt p []
263 val pt = Ctree.update_met pt p []
264 val pt = Ctree.update_spec pt p References.empty
265 in (pt, (p, Pos.Pbl)) end