1 (* Title: Specify/specification.sml
2 Author: Walther Neuper, Mathias Lehnfeld
3 (c) due to copyright terms
6 (* Survey on type fmz_ .. type ori .. type itm (in probl, meth) .. formal args of root-/SubProblem
7 and relations between respective list elements: #1#
8 fmz = [ dsc $ v......................................(dsc $ v)..]
9 root problem on pos = ([], _)
10 fmz_ = [(dsc, v).......................................(dsc, v)..]
12 oris = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)...........(dsc, v)..]
13 \<down> #Given,..,#Relate #Find #undef............#undef \<down>
14 \<down> \<down> \<down> \<down>
15 Specify_Problem + pbl.ppc= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
16 \<down> \<down> \<down> \<down>
17 itms = [(dsc, v)..(dsc, v),(dsc, v)] \<down> \<down> \<down>
18 int.modelling +Cor ++++++++++Cor +Cor \<down> \<down> \<down>
19 \<down> \<down> \<down> \<down>
20 Specify_Method + met.ppc= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
21 \<down> \<down> \<down> \<down>
22 itms = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)..(dsc, v)] \<down> \<down>
23 int.modelling +Cor ++++++Cor \<down> \<down>
24 form.args= [ id ..... id , /////// id ....... id ] \<down> \<down>
25 env = [(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
26 interpret code env = [(id, v)..(id, v), (id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
27 ..extends env ^^^^^^^^^^^^^^^^ \<down> \<down> \<down> \<down> \<down>
28 \<down> \<down> \<down> \<down> \<down> \<down>
29 SubProblem on pos = ([2], _) \<down> \<down> \<down> \<down> \<down> \<down>
30 form.args= [id ................................ id ]\<down> \<down> \<down>
31 \<down> REAL..BOOL.. \<down> \<down> \<down>
32 \<down> \<down> \<down> \<down>
33 + met.ppc= [(dsc,id).......................(dsc,id)]\<down> \<down> \<down>
34 \<down> \<down> \<down> \<down> \<down>
35 oris = [(dsc, v)...................... (dsc, v) ........... (dsc, v)]\<down>
36 Specify_Problem, int.modelling, Specify_Method, interpret code as above #1# \<down>
38 SubProblem on pos = ([3, 4], _) \<down>
39 form.args= [id ...................... id ] \<down>
40 \<down> REAL..BOOL.. \<down>
41 + met.ppc= [(dsc,id).............(dsc,id)] \<down>
42 oris = [(dsc, v).............(dsc, v)...................(dsc, v)]
43 Specify_Problem, int.modelling, Specify_Method, interpret code as above #1#
46 (1) SubProblem implements sub-function calls such, that the arguments(in/output + pre- + post-cond.)
47 of the functions become concern of interactive modelling.
48 (2) In Isac-terms, the above concerns the phases of modelling and
49 and of specifying (Specify_Problem, Specify_Method),
50 while stepwise construction of Solution is called solving.
51 The latter is supported by Lucas-Interpretation of the functions' body.
52 (3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem;
53 it is as complete as possible (this has been different up to now).
54 (4) itm list is initialised by pbl-ppc | met-ppc and completed (Cor) by stepwise user input.
55 (5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,
56 add them to the model-pattern of met and let this input be done automatically;
57 respective items must be in fmz.
59 signature SPECIFICATION =
62 type T = Specification_Def.T (*see NOTES AT START PIDE-ADAPTION in Specification_Def*)
64 val get_data: Calc.T ->
65 I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
66 val reset: Calc.T -> Calc.T
68 val is_complete': I_Model.T -> Pre_Conds.T -> References.T -> bool(*TODO:see I_Model.is_complete*)
69 val is_complete: Calc.T -> bool (*TODO:see I_Model.is_complete*)
73 structure SpecificationC(**): SPECIFICATION(**) =
77 type T = Specification_Def.T;
79 (** is SpecificationC complete? **)
81 (* check i_model either for Problem or MethodC *)
83 (1) singles are all I_Model.Cor
84 (2) Pre_Conds are true
86 * replace (1..2) by I_Model.is_complete
89 fun is_complete' its pre (dI, pI, mI) =
90 foldl and_ (true, map #3 (its: I_Model.T)) andalso
91 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
92 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> MethodC.id_empty
94 (* check I_Model.is_complete either for Problem or MethodC *)
95 fun is_complete (pt, pos as (p, Pos.Pbl)) =
96 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
97 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
98 else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
99 | is_complete (pt, pos as (p, Pos.Met)) =
100 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
101 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
102 else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
103 | is_complete (_, pos) =
104 raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
106 (** handle acces to Ctree **)
108 fun get_data (pt, (p, _)) =
109 case Ctree.get_obj I pt p of
110 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
111 => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
112 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
114 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
115 fun get (pt, pos as (p, Pos.Pbl)) =
117 val (ospec, hdf', spec, probl, ctxt) = case Ctree.get_obj I pt p of
118 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} => (ospec, hdf', spec, probl, ctxt)
119 | _ => raise ERROR "get Pbl: uncovered case get_obj"
120 val {where_rls, where_, ...} =
121 Problem.from_store (Ctree.get_ctxt pt pos) (#2 (References.select_input ospec spec))
122 val (_, pre) = Pre_Conds.check where_rls where_ probl 0
124 (is_complete' probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
126 | get (pt, (p, Pos.Met)) =
128 val (ospec, hdf', spec, meth, ctxt) = case Ctree.get_obj I pt p of
129 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ctxt, ...} => (ospec, hdf', spec, meth, ctxt)
130 | _ => raise ERROR "get Met: uncovered case get_obj"
131 val {prls, pre, ...} = MethodC.from_store ctxt (#3 (References.select_input ospec spec))
132 val (_, pre) = Pre_Conds.check prls pre meth 0
134 (is_complete' meth pre spec, Pos.Met, hdf', meth, pre, spec)
136 | get _ = raise ERROR "get: uncovered definition"
138 (* at the activeFormula set the Specification
139 to empty and return a CalcHead;
140 the 'origin' remains (for reconstructing all that) *)
141 fun reset (pt, (p,_)) =
143 val () = case Ctree.get_obj I pt p of
145 | _ => raise ERROR "reset: uncovered case get_obj"
146 val pt = Ctree.update_pbl pt p []
147 val pt = Ctree.update_met pt p []
148 val pt = Ctree.update_spec pt p References.empty
149 in (pt, (p, Pos.Pbl)) end