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_calchead: Calc.T -> Calc.T*)
64 val reset: Calc.T -> Calc.T
65 (*val get_ocalhd: Calc.T -> T*)
68 I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context*)
69 val get_data: Calc.T ->
70 I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
72 (*val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
73 val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
74 (*val is_complete_mod: Calc.T -> bool*)
75 val is_complete: Calc.T -> bool
77 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
79 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
80 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
84 structure Specification(**): SPECIFICATION(**) =
88 type T = Specification_Def.T;
90 (* is the calchead complete ? *)
91 fun complete its pre (dI, pI, mI) =
92 foldl and_ (true, map #3 (its: I_Model.T)) andalso
93 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
94 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
97 fun make m_field (term_as_string, i_model) =
99 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
100 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
101 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
102 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
105 fun get_data (pt, (p, _)) =
106 case Ctree.get_obj I pt p of
107 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
108 => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
109 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
111 fun is_complete (pt, pos as (p, Pos.Pbl)) =
112 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
113 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
114 else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
115 | is_complete (pt, pos as (p, Pos.Met)) =
116 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
117 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
118 else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
119 | is_complete (_, pos) =
120 raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
122 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
123 fun get (pt, (p, Pos.Pbl)) =
125 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
126 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
127 | _ => raise ERROR "get Pbl: uncovered case get_obj"
128 val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))
129 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
131 (complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
133 | get (pt, (p, Pos.Met)) =
135 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
136 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
137 | _ => raise ERROR "get Met: uncovered case get_obj"
138 val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))
139 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
141 (complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
143 | get _ = raise ERROR "get: uncovered definition"
145 (* at the activeFormula set the Specification
146 to empty and return a CalcHead;
147 the 'origin' remains (for reconstructing all that) *)
148 fun reset (pt, (p,_)) =
150 val () = case Ctree.get_obj I pt p of
152 | _ => raise ERROR "reset: uncovered case get_obj"
153 val pt = Ctree.update_pbl pt p []
154 val pt = Ctree.update_met pt p []
155 val pt = Ctree.update_spec pt p References.empty
156 in (pt, (p, Pos.Pbl)) end