walther@59978
|
1 |
(* Title: Specify/specification.sml
|
walther@59978
|
2 |
Author: Walther Neuper, Mathias Lehnfeld
|
neuper@37906
|
3 |
(c) due to copyright terms
|
wneuper@59265
|
4 |
*)
|
Walther@60547
|
5 |
|
wneuper@59540
|
6 |
(* Survey on type fmz_ .. type ori .. type itm (in probl, meth) .. formal args of root-/SubProblem
|
wneuper@59540
|
7 |
and relations between respective list elements: #1#
|
wneuper@59540
|
8 |
fmz = [ dsc $ v......................................(dsc $ v)..]
|
wneuper@59540
|
9 |
root problem on pos = ([], _)
|
wneuper@59540
|
10 |
fmz_ = [(dsc, v).......................................(dsc, v)..]
|
wneuper@59540
|
11 |
\<down>
|
wneuper@59540
|
12 |
oris = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)...........(dsc, v)..]
|
wneuper@59540
|
13 |
\<down> #Given,..,#Relate #Find #undef............#undef \<down>
|
wneuper@59540
|
14 |
\<down> \<down> \<down> \<down>
|
Walther@60586
|
15 |
Specify_Problem + pbl.model= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
|
wneuper@59540
|
16 |
\<down> \<down> \<down> \<down>
|
wneuper@59540
|
17 |
itms = [(dsc, v)..(dsc, v),(dsc, v)] \<down> \<down> \<down>
|
wneuper@59540
|
18 |
int.modelling +Cor ++++++++++Cor +Cor \<down> \<down> \<down>
|
wneuper@59540
|
19 |
\<down> \<down> \<down> \<down>
|
Walther@60586
|
20 |
Specify_Method + met.model= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
|
wneuper@59540
|
21 |
\<down> \<down> \<down> \<down>
|
wneuper@59540
|
22 |
itms = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)..(dsc, v)] \<down> \<down>
|
wneuper@59540
|
23 |
int.modelling +Cor ++++++Cor \<down> \<down>
|
wneuper@59540
|
24 |
form.args= [ id ..... id , /////// id ....... id ] \<down> \<down>
|
wneuper@59540
|
25 |
env = [(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
|
Walther@60556
|
26 |
interpret code env = [(id, v)..(id, v), (id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
|
wneuper@59540
|
27 |
..extends env ^^^^^^^^^^^^^^^^ \<down> \<down> \<down> \<down> \<down>
|
wneuper@59540
|
28 |
\<down> \<down> \<down> \<down> \<down> \<down>
|
wneuper@59540
|
29 |
SubProblem on pos = ([2], _) \<down> \<down> \<down> \<down> \<down> \<down>
|
wneuper@59540
|
30 |
form.args= [id ................................ id ]\<down> \<down> \<down>
|
wneuper@59540
|
31 |
\<down> REAL..BOOL.. \<down> \<down> \<down>
|
wneuper@59540
|
32 |
\<down> \<down> \<down> \<down>
|
Walther@60586
|
33 |
+ met.model= [(dsc,id).......................(dsc,id)]\<down> \<down> \<down>
|
wneuper@59540
|
34 |
\<down> \<down> \<down> \<down> \<down>
|
wneuper@59540
|
35 |
oris = [(dsc, v)...................... (dsc, v) ........... (dsc, v)]\<down>
|
walther@59718
|
36 |
Specify_Problem, int.modelling, Specify_Method, interpret code as above #1# \<down>
|
wneuper@59540
|
37 |
\<down>
|
wneuper@59540
|
38 |
SubProblem on pos = ([3, 4], _) \<down>
|
wneuper@59540
|
39 |
form.args= [id ...................... id ] \<down>
|
wneuper@59540
|
40 |
\<down> REAL..BOOL.. \<down>
|
Walther@60586
|
41 |
+ met.model= [(dsc,id).............(dsc,id)] \<down>
|
wneuper@59540
|
42 |
oris = [(dsc, v).............(dsc, v)...................(dsc, v)]
|
walther@59718
|
43 |
Specify_Problem, int.modelling, Specify_Method, interpret code as above #1#
|
wneuper@59540
|
44 |
|
wneuper@59540
|
45 |
Notes:
|
Walther@60586
|
46 |
(1) SubProblem implements sub-function calls such, that the arguments(in/output + where_- + post-cond.)
|
wneuper@59540
|
47 |
of the functions become concern of interactive modelling.
|
wneuper@59540
|
48 |
(2) In Isac-terms, the above concerns the phases of modelling and
|
wneuper@59540
|
49 |
and of specifying (Specify_Problem, Specify_Method),
|
Walther@60547
|
50 |
while stepwise construction of Solution is called solving.
|
wneuper@59540
|
51 |
The latter is supported by Lucas-Interpretation of the functions' body.
|
wneuper@59540
|
52 |
(3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem;
|
wneuper@59540
|
53 |
it is as complete as possible (this has been different up to now).
|
Walther@60586
|
54 |
(4) itm list is initialised by pbl-model | met-model and completed (Cor) by stepwise user input.
|
wneuper@59550
|
55 |
(5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,
|
wneuper@59550
|
56 |
add them to the model-pattern of met and let this input be done automatically;
|
wneuper@59550
|
57 |
respective items must be in fmz.
|
wneuper@59540
|
58 |
*)
|
walther@59977
|
59 |
signature SPECIFICATION =
|
wneuper@59265
|
60 |
sig
|
walther@59735
|
61 |
|
Walther@60773
|
62 |
type T = Specification_Def.T
|
walther@59992
|
63 |
val get: Calc.T -> T
|
walther@59992
|
64 |
val get_data: Calc.T ->
|
Walther@60782
|
65 |
I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
|
walther@59994
|
66 |
val reset: Calc.T -> Calc.T
|
walther@59992
|
67 |
|
Walther@60782
|
68 |
val is_complete': I_Model.T -> Pre_Conds.T -> References.T -> bool(*TODO:see I_Model.is_complete*)
|
Walther@60547
|
69 |
val is_complete: Calc.T -> bool (*TODO:see I_Model.is_complete*)
|
Walther@60773
|
70 |
|
wneuper@59265
|
71 |
end
|
neuper@37906
|
72 |
|
walther@59763
|
73 |
(**)
|
walther@60097
|
74 |
structure SpecificationC(**): SPECIFICATION(**) =
|
neuper@37906
|
75 |
struct
|
walther@59763
|
76 |
(**)
|
walther@59957
|
77 |
|
walther@59977
|
78 |
type T = Specification_Def.T;
|
walther@59977
|
79 |
|
Walther@60480
|
80 |
(** is SpecificationC complete? **)
|
Walther@60480
|
81 |
|
Walther@60480
|
82 |
(* check i_model either for Problem or MethodC *)
|
Walther@60480
|
83 |
(*whether
|
Walther@60480
|
84 |
(1) singles are all I_Model.Cor
|
Walther@60480
|
85 |
(2) Pre_Conds are true
|
Walther@60480
|
86 |
* TODO-PIDE:
|
Walther@60480
|
87 |
* replace (1..2) by I_Model.is_complete
|
Walther@60480
|
88 |
* sort out References
|
Walther@60480
|
89 |
*)
|
Walther@60586
|
90 |
fun is_complete' its where_ (dI, pI, mI) =
|
Walther@60782
|
91 |
foldl and_ (true, map #3 (its: I_Model.T)) andalso
|
Walther@60586
|
92 |
foldl and_ (true, map #1 (where_: Pre_Conds.T)) andalso
|
walther@60154
|
93 |
dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> MethodC.id_empty
|
neuper@37906
|
94 |
|
Walther@60756
|
95 |
fun is_complete (pt, (p, _)) =
|
Walther@60756
|
96 |
let
|
Walther@60756
|
97 |
val (itms, oris, probl, o_spec, spec, ctxt) = case Ctree.get_obj I pt p of
|
Walther@60756
|
98 |
Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
|
Walther@60756
|
99 |
=> (itms, oris, probl, o_spec, spec, ctxt)
|
Walther@60756
|
100 |
| _ => raise ERROR "SpecificationC.is_complete only with PblObj"
|
Walther@60756
|
101 |
val (_, pbl_id, met_id) = References.select_input o_spec spec
|
Walther@60756
|
102 |
in
|
Walther@60779
|
103 |
I_Model.s_are_complete ctxt oris (probl, itms) (pbl_id, met_id)
|
Walther@60756
|
104 |
end
|
neuper@37906
|
105 |
|
Walther@60480
|
106 |
(** handle acces to Ctree **)
|
Walther@60480
|
107 |
|
Walther@60480
|
108 |
fun get_data (pt, (p, _)) =
|
Walther@60480
|
109 |
case Ctree.get_obj I pt p of
|
Walther@60480
|
110 |
(Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
|
Walther@60779
|
111 |
=> (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
|
Walther@60480
|
112 |
| _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
|
Walther@60480
|
113 |
|
wneuper@59265
|
114 |
(* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
|
Walther@60706
|
115 |
fun get (pt, (p, Pos.Pbl)) =
|
wneuper@59265
|
116 |
let
|
Walther@60557
|
117 |
val (ospec, hdf', spec, probl, ctxt) = case Ctree.get_obj I pt p of
|
Walther@60773
|
118 |
Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} =>
|
Walther@60779
|
119 |
(ospec, hdf', spec, probl, ctxt)
|
walther@59992
|
120 |
| _ => raise ERROR "get Pbl: uncovered case get_obj"
|
Walther@60729
|
121 |
val {where_rls, where_, model, ...} =
|
Walther@60729
|
122 |
Problem.from_store ctxt (#2 (References.select_input ospec spec))
|
Walther@60741
|
123 |
val (_, where_) = Pre_Conds.check ctxt where_rls where_
|
Walther@60773
|
124 |
(model, probl)
|
wneuper@59265
|
125 |
in
|
Walther@60586
|
126 |
(is_complete' probl where_ spec, Pos.Pbl, hdf', probl, where_, spec)
|
wneuper@59265
|
127 |
end
|
walther@59992
|
128 |
| get (pt, (p, Pos.Met)) =
|
wneuper@59265
|
129 |
let
|
Walther@60557
|
130 |
val (ospec, hdf', spec, meth, ctxt) = case Ctree.get_obj I pt p of
|
Walther@60773
|
131 |
Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ctxt, ...} =>
|
Walther@60779
|
132 |
(ospec, hdf', spec, meth, ctxt)
|
walther@59992
|
133 |
| _ => raise ERROR "get Met: uncovered case get_obj"
|
Walther@60729
|
134 |
val {where_rls, where_, model, ...} =
|
Walther@60729
|
135 |
MethodC.from_store ctxt (#3 (References.select_input ospec spec))
|
Walther@60741
|
136 |
val (_, where_) = Pre_Conds.check ctxt where_rls where_
|
Walther@60773
|
137 |
(model, meth)
|
wneuper@59265
|
138 |
in
|
Walther@60586
|
139 |
(is_complete' meth where_ spec, Pos.Met, hdf', meth, where_, spec)
|
wneuper@59265
|
140 |
end
|
walther@59992
|
141 |
| get _ = raise ERROR "get: uncovered definition"
|
neuper@37906
|
142 |
|
walther@59977
|
143 |
(* at the activeFormula set the Specification
|
wneuper@59265
|
144 |
to empty and return a CalcHead;
|
wneuper@59265
|
145 |
the 'origin' remains (for reconstructing all that) *)
|
walther@59992
|
146 |
fun reset (pt, (p,_)) =
|
wneuper@59265
|
147 |
let
|
walther@59957
|
148 |
val () = case Ctree.get_obj I pt p of
|
walther@59957
|
149 |
Ctree.PblObj _ => ()
|
walther@59992
|
150 |
| _ => raise ERROR "reset: uncovered case get_obj"
|
walther@59957
|
151 |
val pt = Ctree.update_pbl pt p []
|
walther@59957
|
152 |
val pt = Ctree.update_met pt p []
|
walther@59976
|
153 |
val pt = Ctree.update_spec pt p References.empty
|
walther@59957
|
154 |
in (pt, (p, Pos.Pbl)) end
|
neuper@37906
|
155 |
|
Walther@60557
|
156 |
(**)end(**)
|