1.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Wed Feb 22 18:40:34 2023 +0100
1.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Fri Feb 24 16:14:28 2023 +0100
1.3 @@ -10,22 +10,36 @@
1.4
1.5 subsection \<open>Development\<close>
1.6 text \<open>
1.7 - Here we develop the semantics of \<open>Example\<close> intermediately within one single theory
1.8 - for \<open>Example_TEST\<close> before we transfer the development to production code in src/* .
1.9 + Here we develop the semantics of \<open>Example_TEST\<close> as test
1.10 + --- build Outer_Syntax Example_TEST n:
1.11 + and save intermediate states as separate tests in test/../preliminary.sml
1.12 + as soon as some stable state is achieved.
1.13 +
1.14 + This way we make all \<open>Example\<close> to \<open>Example_TEST\<close> step by step
1.15 + and finally rename all again to \<open>Example\<close>.
1.16 +\<close> ML \<open>
1.17 +val ((in_thy, thy_id_pos), (in_pbl, probl_id_pos), (in_met, meth_id_pos)) =
1.18 + (("__", Position.none), ( "__/__", Position.none), ("__/__", Position.none))
1.19 +val in_ = (in_thy, in_pbl, in_met)
1.20 +val spec_ as (spec_thy, spec_pbl, spec_met) = References.empty
1.21 +val o_ as (o_thy, o_pbl, o_met) =
1.22 + ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])
1.23 +\<close> ML \<open>
1.24 +\<close> ML \<open>
1.25 +\<close> ML \<open>
1.26 +\<close> ML \<open>
1.27 +\<close> ML \<open>
1.28 \<close> ML \<open>
1.29 \<close> ML \<open>
1.30 \<close> ML \<open>
1.31 \<close> ML \<open> (** preliminary handling of References **)
1.32 \<close> ML \<open> (* assumption: we read the Specfication as a whole *)
1.33 -\<close> ML \<open>
1.34 -\<close> ML \<open> (*? \<longrightarrow> ?*)
1.35 +(*/-------------------- state of src/../preliminary at that time -----------------------------\*)
1.36 fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*)))
1.37 fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*)))
1.38 fun re_eval_met ((*dummyarg*)) = ("re_eval_met"; ((*dummyarg*)))
1.39 ;
1.40 -re_eval_all: unit -> unit
1.41 -\<close> ML \<open>
1.42 -\<close> ML \<open> (*? \<longrightarrow> ?*)
1.43 +re_eval_all: unit -> unit;
1.44 (*
1.45 switch_pbl_met IS MISSING! Greater changes are to expect with respective introduction.
1.46 In the meanwhile we just \<open>re_eval\<close> the \<open>I_Model\<close> of \<open>Problem\<close>;
1.47 @@ -43,15 +57,20 @@
1.48 ;
1.49 re_eval: References.T -> References.T -> unit
1.50 \<close> ML \<open>
1.51 +\<close> ML \<open>
1.52 +\<close> ML \<open>
1.53 +\<close> ML \<open>
1.54 +\<close> ML \<open>
1.55 +(*\-------------------- state of src/../preliminary at that time -----------------------------/*)
1.56 \<close> ML \<open> (*\<longrightarrow> test/../calculation.sml*)
1.57 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
1.58 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
1.59 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
1.60 -(*################# in this intermediate verion show model's terms syntax error ################*)
1.61 +"----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";
1.62 +"----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";
1.63 +"----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";
1.64 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
1.65 -
1.66 (* Example_TEST "Diff_App-No.123a" (*complete Model, empty References*) *)
1.67 -val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
1.68 val thy = @{theory}
1.69 val model_input = (*type Position.T is hidden, thus redefinition*)
1.70 [("#Given", [("Constants [r = 7]", Position.none)]),
1.71 @@ -62,39 +81,48 @@
1.72 [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),
1.73 ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]
1.74 : (Model_Pattern.m_field * (string * Position.T) list) list
1.75 -val example_id = "Diff_App-No.123a"
1.76 +(**)
1.77 +val ((thy_id, thy_id_pos), (probl_id, probl_id_pos), (meth_id, meth_id_pos)) =
1.78 + (("__", Position.none), ( "__/__", Position.none), ("__/__", Position.none))
1.79 +(**)
1.80 +val example_id = "Diff_App-No.123a";
1.81 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)
1.82 -
1.83 +\<close> ML \<open>
1.84 val state =
1.85 case the_data thy of
1.86 Ctree.EmptyPtree => Preliminary.init_ctree_TEST thy example_id
1.87 - | _ =>
1.88 - let
1.89 + | _ => the_data thy
1.90 +\<close> ML \<open>
1.91 + (*let*)
1.92 + val ctree = the_data thy
1.93 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
1.94 - Ctree.get_obj I (the_data thy) [] |> Ctree.rep_specify_data
1.95 + Ctree.get_obj I ctree [(*Pos will become variable*)] |> Ctree.rep_specify_data
1.96 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
1.97 - val (model, where_) = Model_Pattern.parse_pos ctxt model_input
1.98 + val (model, where_) = Model_Pattern.parse_pos ctxt model_input (*+check syntax*)
1.99 +\<close> ML \<open>
1.100 +\<close> ML \<open>
1.101 +(*Specify.check_input \<longrightarrow> specify.sml*)
1.102 +fun check_input _ = 123
1.103 +\<close> ML \<open>
1.104 +\<close> ML \<open>
1.105 +\<close> ML \<open>
1.106 +\<close> ML \<open>
1.107 (**)
1.108 - val _ = re_eval References.empty References.empty
1.109 + val _ = re_eval References.empty References.empty;
1.110 (**)
1.111 - in Preliminary.update_state_TEST thy
1.112 +\<close> ML \<open>
1.113 + (*in*) Preliminary.update_state_TEST thy
1.114 (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)
1.115 - end
1.116 + (*end*)
1.117 \<close> ML \<open>
1.118 \<close> ML \<open>
1.119 \<close> ML \<open>
1.120 \<close> ML \<open>
1.121 \<close> ML \<open>
1.122 -(*----------------- after I_Model.complete ------------------------------------------------
1.123 -(* Example_TEST "Diff_App-No.123a" (*complete Model*) CAN BE TRIED *)
1.124 -val (("#Given",
1.125 - (Const ("Input_Descript.Constants", _),
1.126 - Const ("List.list.Cons", _) $
1.127 - (Const ("HOL.eq", _) $ Free ("r", Type ("Real.real", [])) $
1.128 - (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))))) $
1.129 - Const ("List.list.Nil", _)),
1.130 - _) :: _) = model: Model_Pattern.pre_model
1.131 -------------------- after I_Model.complete ------------------------------------------------*)
1.132 +\<close> ML \<open>
1.133 +\<close> ML \<open>
1.134 +\<close> ML \<open>
1.135 +\<close> ML \<open>
1.136 \<close> ML \<open>
1.137 \<close> ML \<open>
1.138 val _ =