wneuper/isa: test/Tools/isac/BridgeJEdit/calculation.sml@18b933a12ab8

     1 (* Title:  BridgeJEdit/calculation.sml

     2    Author: Walther Neuper

     3 *)

     5 "-----------------------------------------------------------------------------------------------";

     6 "table of contents -----------------------------------------------------------------------------";

     7 "-----------------------------------------------------------------------------------------------";

     8 "----------- build Outer_Syntax Example_TEST 1: parse errors shown at the spot -----------------";

     9 "----------- build Outer_Syntax Example_TEST 2: handle empty input -----------------------------";

    10 "----------- build Outer_Syntax Example_TEST 3: Pre_Conds.check_TEST I_Model.is_complete_OLD ---";

    11 "-----------------------------------------------------------------------------------------------";

    12 "-----------------------------------------------------------------------------------------------";

    13 "-----------------------------------------------------------------------------------------------";

    16 "----------- build Outer_Syntax Example_TEST 1: parse errors shown at the spot -----------------";

    17 "----------- build Outer_Syntax Example_TEST 1: parse errors shown at the spot -----------------";

    18 "----------- build Outer_Syntax Example_TEST 1: parse errors shown at the spot -----------------";

    19 (*/-------------------- state of src/../preliminary.sml at that time --------------------------\*)

    20 fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*)))

    21 fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*)))

    22 fun re_eval_met ((*dummyarg*)) = ("re_eval_met"; ((*dummyarg*)))

    23 ;

    24 re_eval_all: unit -> unit;

    25 (*

    26   switch_pbl_met IS MISSING! Greater changes are to expect with respective introduction.

    27   In the meanwhile we just \<open>re_eval\<close> the \<open>I_Model\<close> of \<open>Problem\<close>;

    28   in case this is complete, we automatically complete the \<open>I_Model\<close> of \<open>MethodC\<close>

    29   without displaying the respective \<open>P_Model\<close> and immediately start solve-phase by \<open>Apply_Method\<close>;

    30 *)

    31 fun re_eval (input_thy, input_pbl, input_met) (spec_thy, spec_pbl, spec_met) =

    32   if spec_thy <> input_thy

    33     then re_eval_all ()

    34     else if spec_pbl <> input_pbl

    35       then re_eval_pbl ()

    36       else if spec_met <> input_met

    37         then re_eval_met ()

    38         else ("nothing to re-evaluate"; ((*dummyarg*)))

    39 ;

    40 re_eval: References.T -> References.T -> unit;

    41 (*\-------------------- state of src/../preliminary.sml at that time --------------------------/*)

    42 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)

    43 (* Example_TEST "Diff_App-No.123a" (*complete Model, empty References*) *)

    44 val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")

    45 val thy = @{theory Calculation}

    46 val model_input = (*type Position.T is hidden, thus redefinition*)

    47  [("#Given", [("Constants [r = 7]", Position.none)]),

    48   ("#Where", [("0 < r", Position.none)]),

    49   ("#Find",

    50    [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),

    51   ("#Relate",

    52    [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),

    53     ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]

    54 : (Model_Pattern.m_field * (string * Position.T) list) list

    55 val example_id = "Diff_App-No.123a";

    56 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)

    57 (*/---------------------------------------- adapt to Test_Isac/_Short.thy ---------------------\*)

    58 (**)val ctree = Preliminary.init_ctree thy example_id;

    59 (** ) --- why does this not work? ( **)

    60 set_data ctree thy;

    61 the_data thy;

    62 (** )-- why does this not work? Note (**)ctree(** )(the_data thy)( **) below.*)

    63 (*\---------------------------------------- adapt to Test_Isac/_Short.thy ---------------------/*)

    64             val state =

    65               case the_data thy of

    66                   CTbasic_TEST.EmptyPtree => Preliminary.init_ctree thy example_id

    67                 | _ => the_data thy

    68                 (*let*)

    69                     val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =

    70                       CTbasic_TEST.get_obj I (**)ctree(** )(the_data thy)( **) [] |> CTbasic_TEST.rep_specify_data

    71                     val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)

    72                     val (model, where_) = Model_Pattern.parse_pos ctxt model_input

    73 (**)

    74                     val _ = re_eval References.empty References.empty;

    75 (**)

    76             (*in*) Preliminary.update_state thy

    77                       (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)

    78             (*end*);

    81 "----------- build Outer_Syntax Example_TEST 2: handle empty input -----------------------------";

    82 "----------- build Outer_Syntax Example_TEST 2: handle empty input -----------------------------";

    83 "----------- build Outer_Syntax Example_TEST 2: handle empty input -----------------------------";

    84 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)

    85 (* Example_TEST "Diff_App-No.123a" (*complete Model, empty References*) *)

    86 val thy = @{theory}

    87 val model_input = (*type Position.T is hidden, thus redefinition*)

    88  [("#Given", [("Constants [r = 7]", Position.none)]),

    89   ("#Where", [("0 < r", Position.none)]),

    90   ("#Find",

    91    [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),

    92   ("#Relate",

    93    [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),

    94     ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]

    95 : (Model_Pattern.m_field * (string * Position.T) list) list

    96 (**)

    97 val ((thy_id, thy_id_pos), (probl_id, probl_id_pos), (meth_id, meth_id_pos)) =

    98   (("__", Position.none), ( "__/__", Position.none), ("__/__", Position.none))

    99 (**)

   100 val example_id = "Diff_App-No.123a";

   101 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)

   102 open Model_Pattern

   104             val state =

   105               case the_data thy of

   106                   CTbasic_TEST.EmptyPtree => Preliminary.init_ctree thy example_id

   107                 | _ => the_data thy

   108                   (*let*)

   109                     val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =

   110                       CTbasic_TEST.get_obj I state [(*Pos will become variable*)] |> CTbasic_TEST.rep_specify_data

   112 (*knows variables from origin + notation (input) undefined ^^^^^ from BaseDefinitions.thy*)

   113 (*test*)val Const ("Input_Descript.Constants", _) $

   114      (Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ Const ("HOL.undefined", _) $ Const ("HOL.undefined", _)) $

   115        (Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ Const ("HOL.undefined", _) $ Const ("HOL.undefined", _)) $

   116          Const ("List.list.Nil", _))) = Syntax.read_term ctxt "Constants [__=__, __=__]"

   118                     val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)

   119 (* here we assume:

   120   (1) thy_id did not provide an update

   121   (2) \<Otimes>\<Odot> is set to Problem_Ref

   122   (3) the probl : I_Model is complete with descriptors from Preliminary.init_ctree

   123 *)

   124                     val (model, where_) =

   125 Model_Pattern.parse_pos_empty ctxt model_input;

   126 "~~~~~ fun parse_pos_empty , args:"; val (ctxt, model_input) = (ctxt, model_input);

   127     val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;

   128     val model = items

   129       |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")

   130 (*    |> map (parse_term ctxt) *)

   131 (*val model =

   132    [("#Given", ("Constants [r = 7]", {})), ("#Find", ("Maximum A", {})), ("#Find", ("AdditionalValues [u, v]", {})), ("#Relate", ("Extremum (A = 2 * u * v - u \<up> 2)", {})),

   133     ("#Relate", ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", {}))]:

   134    (string * (string * Position.T)) list*);

   136 "~~~~~ fun parse_empty_input , args:"; val (ctxt, (m_field, (str, pos))) = (ctxt, hd model);

   137     val (m_field, term, pos) = parse_term ctxt (m_field, (str, pos));

   139 (*+*)if is_undefined @{term "Constants [__=__, __=__]"}

   140 (*+*)  then () else error "is_undefined 1 CHANGED";

   141 (*+*)if is_undefined @{term "Maximum __"}

   142 (*+*)  then () else error "is_undefined 2 CHANGED";

   143 (*+*)if is_undefined @{term "AdditionalValues [__, __]"}

   144 (*+*)  then () else error "is_undefined 3 CHANGED";

   145 (*+*)if is_undefined @{term "Constants [r = 7]"}

   146 (*+*)  then error "is_undefined 4 CHANGED" else ();

   148 (*+*)val (m_field, (descr, arg), pos) = split_descriptor ctxt (m_field, term, pos);

   149 (*+*)if is_undefined arg

   150 (*+*)then Empty (m_field, (descr, descr |> empty_for), pos)

   151 (*+*)else Proper (m_field, (descr, arg), pos);

   153                     val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input (*+check syntax*)

   154 (*+*)val [Proper

   155 (*+*)  ("#Given", (Const ("Input_Descript.Constants", _),

   156 (*+*)    Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ Free ("r", _) $

   157 (*+*)      (Const ("Num.numeral_class.numeral", _) $ _)) $ Const ("List.list.Nil", _)), _),

   158 (*+*) Proper _, Proper _, Proper _, Proper _] = model

   160 (**)

   161                     val _ = re_eval References.empty References.empty;

   162 (**)

   163             (*in*) Preliminary.update_state thy

   164                       (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)

   165             (*end*);

   168 "----------- build Outer_Syntax Example_TEST 3: Pre_Conds.check_TEST I_Model.is_complete_OLD ---";

   169 "----------- build Outer_Syntax Example_TEST 3: Pre_Conds.check_TEST I_Model.is_complete_OLD ---";

   170 "----------- build Outer_Syntax Example_TEST 3: Pre_Conds.check_TEST I_Model.is_complete_OLD ---";

   171 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)

   172 (* Example_TEST "Diff_App-No.123a" (*complete Model, empty References*) *)

   173 val thy = @{theory Calculation}

   174 val model_input = (*type Position.T is hidden, thus redefinition*)

   175  [("#Given", [("Constants [r = 7]", Position.none)]),

   176   ("#Where", [("0 < r", Position.none)]),

   177   ("#Find",

   178    [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),

   179   ("#Relate",

   180    [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),

   181     ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]

   182 : (Model_Pattern.m_field * (string * Position.T) list) list

   183 (**)

   184 val ((thy_id, thy_id_pos), (probl_id, probl_id_pos), (meth_id, meth_id_pos)) =

   185   (("__", Position.none), ( "__/__", Position.none), ("__/__", Position.none))

   186 (**)

   187 val example_id = "Diff_App-No.123a";

   188 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)

   189 open Model_Pattern

   190 open Pre_Conds

   191 open I_Model

   193             val state =

   194               case the_data thy of

   195                   CTbasic_TEST.EmptyPtree => Preliminary.init_ctree thy example_id

   196                 | _(*state (*FOR TEST*)*) => (**)the_data thy(**)

   197                   (*let*)

   198                     val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =

   199                       CTbasic_TEST.get_obj I state [(*Pos will become variable*)] |> CTbasic_TEST.rep_specify_data

   200                     val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)

   201                     val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input (*+check syntax*);

   203 (*+*)(o_model |> O_Model.to_string ctxt) = "[\n" ^

   204   "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^

   205   "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^

   206   "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^

   207   "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^

   208   "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^

   209   "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^

   210   "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^

   211   "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^

   212   "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^

   213   "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^

   214   "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^

   215   "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]";

   217 (*//------------------ code under construction relate_to_input etc -------------------------\\*)

   218 (* \<longrightarrow> calculation.sml (? preliminary.sml ?) *)

   219 (*

   220   each item of I_Model is related to input (NOT vice versa),

   221   where the input-items might be less in number than the I_Model-items

   222   due to error (msg ^ Position.here pos) in ParseC.term_position.

   223 *)

   224 fun relate_to_input o_model i_model input = 123

   225 (*is known, which input -----------------------------(str, pos) is new ???*)

   226 fun check_single ctxt m_field o_model i_model m_patt (str, pos) = 123;

   227 (*\\------------------ code under construction relate_to_input etc -------------------------//*)

   229 (*//------------------ test under construction relate_to_input etc -------------------------\\*)

   230 "~~~~~ fun relate_to_input , args:"; val (o_model, i_model, input) = (o_model, probl, model);

   233 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, (str, pos)) =

   234   (ctxt, "#Given", o_model, i_model, (str, Position.none));

   237 (*\\------------------ test under construction relate_to_input etc -------------------------//*)

   239 (*reminder for Template.show ----------------------------------------------------------------\*)

   240                     val ((_, true, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =

   241                       References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref

   242                     val {model = model_patt, where_ = where_ctree, where_rls, ...} =

   243                       Problem.from_store ctxt pbl_id;

   245 (*/----- ERROR: mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"-------------\

   246   ------------------------------------------------vvvvvvvvvvvvvvvvvvvvv-----------------------* )

   247                     val (_, env_eval) = Pre_Conds.sep_variants_envs_OLD model_patt probl

   248                     (*------------------- must be completed first ---^^^^^*)

   249                     val _ =

   250                       case I_Model.is_complete_OLD ctxt model_patt where_rls where_ctree probl of

   251                         NONE => writeln "I_Model.is_complete_OLD --> NONE"

   252                       | SOME variants =>

   253                         writeln ("I_Model.is_complete_OLD --> SOME " ^ LibraryC.ints2str' variants)

   254 ( *\----- ERROR: mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"-------------/*)

   255 (*reminder for Template.show ----------------------------------------------------------------/*)

   257 (*reminder for Pre_Conds.check_TEST ---------------------------------------------------------\* )

   258 val (true, [(true, (Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

   259   Free ("r", _), _))]) = Pre_Conds.check_TEST ctxt where_rls where_ env_eval;

   260 ( *reminder for Pre_Conds.check_TEST ---------------------------------------------------------/*)

   261 (**)

   262                     val ((_, true, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =

   263                         References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref

   264                     val _ = re_eval References.empty References.empty;

   265 (**)

   266             (*in*)

   267                     Preliminary.update_state thy

   268                       (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)

   269             (*end*)

author	wneuper <Walther.Neuper@jku.at>
	Thu, 17 Aug 2023 08:01:45 +0200
changeset 60732	18b933a12ab8
parent 60717	4c8c9ef90da9
child 60771	1b072aab8f4e
permissions	-rw-r--r--