1.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Wed Jun 22 17:33:45 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Wed Jun 22 19:26:18 2022 +0200
1.3 @@ -184,13 +184,9 @@
1.4 ]: TermC.as_string list;
1.5 val refs =
1.6 ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
1.7 -\<close> ML \<open>
1.8 -\<close> ML \<open>
1.9 -\<close> ML \<open>
1.10 \<close> ML \<open>
1.11 \<close>
1.12
1.13 -
1.14 subsection \<open>Specification Phase\<close>
1.15 text \<open>
1.16 Stepwise development of \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> begins with
2.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Wed Jun 22 17:33:45 2022 +0200
2.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Wed Jun 22 19:26:18 2022 +0200
2.3 @@ -90,7 +90,7 @@
2.4
2.5 type i_model_single =
2.6 int * (* sequence of input, 0 = untouched, drop with PIDE ? *)
2.7 - variants * (* pointers to variants given in Formalise.T *)
2.8 + variants * (* pointers to variants given in Formalise.T TODOrevise*)
2.9 bool * (* input on this item is not/complete *)
2.10 m_field * (* #Given | #Find | #Relate *)
2.11 i_model_feedback; (* variables and values, see above *)
3.1 --- a/src/Tools/isac/MathEngBasic/specification-def.sml Wed Jun 22 17:33:45 2022 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/specification-def.sml Wed Jun 22 19:26:18 2022 +0200
3.3 @@ -15,13 +15,13 @@
3.4 struct
3.5 (**)
3.6
3.7 -type T =
3.8 - bool * (* I_Model.T andalso Pre_Conds.T *)
3.9 +type T = (* NOTES AT START PIDE-ADAPTION*)
3.10 + bool * (* I_Model.T andalso Pre_Conds.T ELIMINATE*)
3.11 Pos.pos_ * (* model belongs to Problem or MethodC *)
3.12 - term * (* the headline shown on Calc.T *)
3.13 - Model_Def.i_model * (* used by I_Model.T *)
3.14 - Pre_Conds_Def.T * (* used by Pre_Conds.T *)
3.15 - References_Def.T; (* into Know_Store *)
3.16 + term * (* the headline shown on Calc.T NOT SPECIFIC FOR Pbl | Met*)
3.17 + Model_Def.i_model * (* used by I_Model.T *)
3.18 + Pre_Conds_Def.T * (* used by Pre_Conds.T *)
3.19 + References_Def.T; (* into Know_Store NOT SPECIFIC FOR Pbl | Met*)
3.20 val empty =
3.21 (false, Pos.Und, TermC.empty, [Model_Def.i_model_empty], [(false, TermC.empty)], References_Def.empty);
3.22
4.1 --- a/src/Tools/isac/Specify/i-model.sml Wed Jun 22 17:33:45 2022 +0200
4.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Jun 22 19:26:18 2022 +0200
4.3 @@ -401,7 +401,7 @@
4.4 val mits = complete oris pits [] mpc
4.5 in (pits, mits) end
4.6
4.7 -(* WN0312: use in nxt_spec, too ? what about variants ??? *)
4.8 +(* TODO: also check if all elements are I_Model.Cor *)
4.9 fun is_complete ([]: T) = false
4.10 | is_complete itms = foldl and_ (true, (map #3 itms))
4.11
5.1 --- a/src/Tools/isac/Specify/p-spec.sml Wed Jun 22 17:33:45 2022 +0200
5.2 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Jun 22 19:26:18 2022 +0200
5.3 @@ -253,12 +253,12 @@
5.4 then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))
5.5 val (_, pre) = Pre_Conds.check prls where_ pits 0
5.6 in (Ctree.update_pbl pt p pits,
5.7 - (SpecificationC.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T)
5.8 + (SpecificationC.is_complete' pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T)
5.9 end
5.10 else let val {prls,pre,...} = MethodC.from_store (#3 (References.select ospec spec))
5.11 val (_, pre) = Pre_Conds.check prls pre mits 0
5.12 in (Ctree.update_met pt p mits,
5.13 - (SpecificationC.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)
5.14 + (SpecificationC.is_complete' mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)
5.15 end
5.16 end
5.17 end
6.1 --- a/src/Tools/isac/Specify/specification.sml Wed Jun 22 17:33:45 2022 +0200
6.2 +++ b/src/Tools/isac/Specify/specification.sml Wed Jun 22 19:26:18 2022 +0200
6.3 @@ -58,14 +58,14 @@
6.4 signature SPECIFICATION =
6.5 sig
6.6
6.7 - type T = Specification_Def.T
6.8 + type T = Specification_Def.T (*see NOTES AT START PIDE-ADAPTION in Specification_Def*)
6.9 val get: Calc.T -> T
6.10 val get_data: Calc.T ->
6.11 I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
6.12 val reset: Calc.T -> Calc.T
6.13
6.14 - val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * MethodC.id -> bool
6.15 - val is_complete: Calc.T -> bool
6.16 + val is_complete': I_Model.T -> Pre_Conds.T -> References.T -> bool(*TODO: see I_Mode.is_complete*)
6.17 + val is_complete: Calc.T -> bool (*TODO: see I_Mode.is_complete*)
6.18 end
6.19
6.20 (**)
6.21 @@ -75,18 +75,22 @@
6.22
6.23 type T = Specification_Def.T;
6.24
6.25 -(* is the calchead complete ? *)
6.26 -fun complete its pre (dI, pI, mI) =
6.27 +(** is SpecificationC complete? **)
6.28 +
6.29 +(* check i_model either for Problem or MethodC *)
6.30 +(*whether
6.31 +(1) singles are all I_Model.Cor
6.32 +(2) Pre_Conds are true
6.33 + * TODO-PIDE:
6.34 + * replace (1..2) by I_Model.is_complete
6.35 + * sort out References
6.36 + *)
6.37 +fun is_complete' its pre (dI, pI, mI) =
6.38 foldl and_ (true, map #3 (its: I_Model.T)) andalso
6.39 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
6.40 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> MethodC.id_empty
6.41
6.42 -fun get_data (pt, (p, _)) =
6.43 - case Ctree.get_obj I pt p of
6.44 - (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
6.45 - => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
6.46 - | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
6.47 -
6.48 +(* check I_Model.is_complete either for Problem or MethodC *)
6.49 fun is_complete (pt, pos as (p, Pos.Pbl)) =
6.50 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
6.51 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
6.52 @@ -98,6 +102,14 @@
6.53 | is_complete (_, pos) =
6.54 raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
6.55
6.56 +(** handle acces to Ctree **)
6.57 +
6.58 +fun get_data (pt, (p, _)) =
6.59 + case Ctree.get_obj I pt p of
6.60 + (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
6.61 + => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
6.62 + | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
6.63 +
6.64 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
6.65 fun get (pt, (p, Pos.Pbl)) =
6.66 let
6.67 @@ -107,7 +119,7 @@
6.68 val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))
6.69 val (_, pre) = Pre_Conds.check prls where_ probl 0
6.70 in
6.71 - (complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
6.72 + (is_complete' probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
6.73 end
6.74 | get (pt, (p, Pos.Met)) =
6.75 let
6.76 @@ -117,7 +129,7 @@
6.77 val {prls, pre, ...} = MethodC.from_store (#3 (References.select ospec spec))
6.78 val (_, pre) = Pre_Conds.check prls pre meth 0
6.79 in
6.80 - (complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
6.81 + (is_complete' meth pre spec, Pos.Met, hdf', meth, pre, spec)
6.82 end
6.83 | get _ = raise ERROR "get: uncovered definition"
6.84