1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Dec 11 09:24:02 2023 +0100
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Dec 11 12:14:28 2023 +0100
1.3 @@ -33,14 +33,14 @@
1.4 (**)
1.5 structure Data = Theory_Data
1.6 (
1.7 - type T = CTbasic_POS.ctree option;
1.8 + type T = CTbasic.ctree option;
1.9 val empty = NONE;
1.10 fun merge _ = NONE;
1.11 );
1.12
1.13 val set_data = Data.put o SOME;
1.14 fun the_data thy =
1.15 - case Data.get thy of NONE => CTbasic_POS.EmptyPtree
1.16 + case Data.get thy of NONE => CTbasic.EmptyPtree
1.17 | SOME ctree => ctree;
1.18 \<close> ML \<open>
1.19 \<close>
1.20 @@ -60,11 +60,11 @@
1.21 let
1.22 val state =
1.23 case the_data thy of
1.24 - CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id
1.25 + CTbasic.EmptyPtree => Preliminary.init_ctree thy example_id
1.26 | state =>
1.27 let
1.28 val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
1.29 - CTbasic_POS.get_obj I state [(*Pos will become variable*)] |> CTbasic_POS.rep_specify_data
1.30 + CTbasic.get_obj I state [(*Pos will become variable*)] |> CTbasic.rep_specify_data
1.31 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
1.32 val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input (*+check syntax*)
1.33 (** )
1.34 @@ -96,7 +96,7 @@
1.35 (* ---------- ^^^ values for arguments of the fn below in order to determine signature -------*)
1.36 (fn thy =>
1.37 let
1.38 - val store = CTbasic_POS.EmptyPtree;
1.39 + val store = CTbasic.EmptyPtree;
1.40 in set_data store thy end)
1.41 : theory -> theory
1.42 (*\---------------------------------------- mimic input from PIDE ----------------------------/*)
2.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Mon Dec 11 09:24:02 2023 +0100
2.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Mon Dec 11 12:14:28 2023 +0100
2.3 @@ -21,7 +21,7 @@
2.4 Below there are different versions of Example "Diff_App-No.123a" for reference;
2.5 the versions refer to different situations in educational settings.
2.6
2.7 - The actual development is done in test/../Test_VSCode_Example.thy on \<open>Example_POS\<close>.
2.8 + The actual development is done in test/../Test_VSCode_Example.thy on \<open>\<close>.
2.9 According to successful results of development the versions below will be updated.
2.10 \<close>
2.11
3.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml Mon Dec 11 09:24:02 2023 +0100
3.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml Mon Dec 11 12:14:28 2023 +0100
3.3 @@ -8,9 +8,9 @@
3.4 signature PRELIMINARY =
3.5 sig
3.6 val check_input: Model_Pattern.model_input_pos -> I_Model.T_POS
3.7 - val init_ctree: theory -> string -> CTbasic_POS.ctree
3.8 + val init_ctree: theory -> string -> CTbasic.ctree
3.9 val update_state: theory -> string * (Model_Pattern.model_input_pos * References.input) ->
3.10 - CTbasic_POS.ctree -> CTbasic_POS.ctree
3.11 + CTbasic.ctree -> CTbasic.ctree
3.12
3.13 end
3.14
3.15 @@ -46,20 +46,20 @@
3.16 val (o_model, ctxt) = O_Model.init thy model model_patt
3.17 val i_model_empty = I_Model.init_POS ctxt o_model model_patt
3.18 in
3.19 - CTbasic_POS.Nd (CTbasic_POS.PblObj {
3.20 + CTbasic.Nd (CTbasic.PblObj {
3.21 fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)),
3.22 spec = References.empty, probl = i_model_empty, meth = I_Model.empty_POS,
3.23 ctxt = ctxt, loc = (NONE, NONE),
3.24 - branch = CTbasic_POS.NoBranch, ostate = CTbasic_POS.Incomplete, result = (TermC.empty, [])}, [])
3.25 + branch = CTbasic.NoBranch, ostate = CTbasic.Incomplete, result = (TermC.empty, [])}, [])
3.26 end
3.27
3.28
3.29 (** update state **)
3.30
3.31 -fun update_state thy (example_id, (model, refs)) CTbasic_POS.EmptyPtree =
3.32 +fun update_state thy (example_id, (model, refs)) CTbasic.EmptyPtree =
3.33 (init_ctree thy example_id) |> update_state thy (example_id, (model, refs))
3.34 | update_state _ (_, (model, refs_input))
3.35 - (CTbasic_POS.Nd (CTbasic_POS.PblObj {fmz, origin = origin as (o_model, refs_orig, _),
3.36 + (CTbasic.Nd (CTbasic.PblObj {fmz, origin = origin as (o_model, refs_orig, _),
3.37 spec, probl, meth, ctxt, loc, branch, ostate, result}, children)) =
3.38 let
3.39 val (thy_id, pbl_id, met_id) = References.select_from_input refs_input refs_orig spec
3.40 @@ -71,7 +71,7 @@
3.41 val complete_model = I_Model.complete o_model probl meth model
3.42 ( **)
3.43 in
3.44 - CTbasic_POS.Nd (CTbasic_POS.PblObj {
3.45 + CTbasic.Nd (CTbasic.PblObj {
3.46 fmz = fmz, origin = origin, spec = (thy_id, pbl_id, met_id),
3.47 probl = probl, meth = meth, (*TODO P_Model.switch_pbl_met*)
3.48 ctxt = ctxt, loc = loc,
4.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Dec 11 09:24:02 2023 +0100
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Dec 11 12:14:28 2023 +0100
4.3 @@ -84,23 +84,17 @@
4.4 in filt end;
4.5
4.6 (*T_POSold*)
4.7 -fun xml_of_itm_ (I_Model.Cor (dts, _)) =
4.8 +fun xml_of_itm_ (I_Model.Cor_POS (dts)) =
4.9 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
4.10 - | xml_of_itm_ (I_Model.Syn c) =
4.11 + | xml_of_itm_ (I_Model.Syn_POS c) =
4.12 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
4.13 - | xml_of_itm_ (I_Model.Typ c) =
4.14 - XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
4.15 - (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
4.16 - | xml_of_itm_ (I_Model.Inc (dts, _)) =
4.17 + | xml_of_itm_ (I_Model.Inc_POS (dts)) =
4.18 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
4.19 - | xml_of_itm_ (I_Model.Sup dts) =
4.20 + | xml_of_itm_ (I_Model.Sup_POS dts) =
4.21 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])
4.22 - | xml_of_itm_ (I_Model.Mis (d, pid)) =
4.23 - XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
4.24 - | xml_of_itm_ _ = raise ERROR "xml_of_itm_: wrong argument"
4.25 -fun xml_of_itms itms =
4.26 +fun xml_of_itms (itms: I_Model.T_POS) =
4.27 let
4.28 - fun extract (_, _, _, _, itm_) = itm_
4.29 + fun extract (_, _, _, _, (itm_, _)) = itm_
4.30 in map (xml_of_itm_ o extract) itms end
4.31 (*T_POS*)
4.32 fun xml_of_itm_POS (I_Model.Cor_POS dts) =
4.33 @@ -121,7 +115,7 @@
4.34 XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])
4.35 fun xml_of_preconds ps = map xml_of_precond ps
4.36
4.37 -fun xml_of_model itms where_ =
4.38 +fun xml_of_model (itms: I_Model.T_POS) where_ =
4.39 let
4.40 fun eq str (_, _, _,field, _) = str = field
4.41 in
4.42 @@ -151,7 +145,7 @@
4.43 fun xml_of_modspec ((b, p_, head, gfr, where_, spec): SpecificationC.T) =
4.44 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
4.45 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
4.46 - xml_of_model (I_Model.TEST_to_OLD gfr) where_,
4.47 + xml_of_model gfr where_,
4.48 XML.Elem (("BELONGSTO", []), [
4.49 XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),
4.50 xml_of_spec spec])
4.51 @@ -160,7 +154,7 @@
4.52 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
4.53 xml_of_pos "POSITION" p,
4.54 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
4.55 - xml_of_model (I_Model.TEST_to_OLD gfr) where_,
4.56 + xml_of_model gfr where_,
4.57 XML.Elem (("BELONGSTO", []), [
4.58 XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),
4.59 xml_of_spec spec])
4.60 @@ -287,7 +281,7 @@
4.61 XML.Elem (("STATUS", []), [
4.62 XML.Text ((if model_ok then "correct" else "incorrect"))]),
4.63 XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]),
4.64 - xml_of_model (I_Model.TEST_to_OLD pbl) where_])
4.65 + xml_of_model pbl where_])
4.66
4.67 fun xml_of_matchmet (model_ok, pI, program, pbl, where_) =
4.68 XML.Elem (("CONTEXTDATA", []), [
5.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 11 09:24:02 2023 +0100
5.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 11 12:14:28 2023 +0100
5.3 @@ -507,8 +507,7 @@
5.4 => (itms, oris, probl, o_spec, spec)
5.5 | _ => raise ERROR "LI.by_tactic: no PblObj"
5.6 val (_, pI', _) = References.select_input o_spec spec
5.7 - val (_, itms) = I_Model.s_make_complete ctxt oris
5.8 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
5.9 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
5.10 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt itms mI of
5.11 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
5.12 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
6.1 --- a/src/Tools/isac/Interpret/solve-step.sml Mon Dec 11 09:24:02 2023 +0100
6.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Mon Dec 11 12:14:28 2023 +0100
6.3 @@ -121,7 +121,7 @@
6.4 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
6.5 | _ => raise ERROR "Solve_Step.check Apply_Method: uncovered case Ctree.get_obj"
6.6 val {model, where_rls, where_, ...} = Problem.from_store ctxt pI
6.7 - val checked = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_POS probl)
6.8 + val checked = Pre_Conds.check ctxt where_rls where_ (model, probl)
6.9 val true_only = checked
6.10 |> snd
6.11 |> map (fn (true, prec) => [prec] | (false, _) => [])
7.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Mon Dec 11 09:24:02 2023 +0100
7.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Mon Dec 11 12:14:28 2023 +0100
7.3 @@ -35,7 +35,6 @@
7.4 ML_file position.sml
7.5 ML_file "specification-def.sml"
7.6
7.7 - ML_file "ctree-basic-TEST.sml"
7.8 ML_file "ctree-basic.sml"
7.9 ML_file "ctree-access.sml"
7.10 ML_file "ctree-navi.sml"
8.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Mon Dec 11 09:24:02 2023 +0100
8.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Mon Dec 11 12:14:28 2023 +0100
8.3 @@ -8,11 +8,11 @@
8.4 val get_last_formula: CTbasic.state -> term
8.5 val update_branch : CTbasic.ctree -> Pos.pos -> CTbasic.branch -> CTbasic.ctree
8.6 val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.id -> CTbasic.ctree
8.7 - val update_met : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =vvv= ? *)
8.8 - val update_metppc : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =^^^= ? *)
8.9 + val update_met : CTbasic.ctree -> Pos.pos -> Model_Def.i_model_POS -> CTbasic.ctree (* =vvv= ? *)
8.10 + val update_metppc : CTbasic.ctree -> Pos.pos -> Model_Def.i_model_POS -> CTbasic.ctree (* =^^^= ? *)
8.11 val update_metID : CTbasic.ctree -> Pos.pos -> MethodC.id -> CTbasic.ctree
8.12 - val update_pbl : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =vvv= ? *)
8.13 - val update_pblppc : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =^^^= ? *)
8.14 + val update_pbl : CTbasic.ctree -> Pos.pos -> Model_Def.i_model_POS -> CTbasic.ctree (* =vvv= ? *)
8.15 + val update_pblppc : CTbasic.ctree -> Pos.pos -> Model_Def.i_model_POS -> CTbasic.ctree (* =^^^= ? *)
8.16 val update_pblID : CTbasic.ctree -> Pos.pos -> Problem.id -> CTbasic.ctree
8.17 val update_oris : CTbasic.ctree -> Pos.pos -> Model_Def.o_model -> CTbasic.ctree
8.18 val update_orispec : CTbasic.ctree -> Pos.pos -> References_Def.T -> CTbasic.ctree
8.19 @@ -25,7 +25,7 @@
8.20 val cappend_problem : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->
8.21 Model_Def.form_T -> Model_Def.o_model * References_Def.T * term * Proof.context
8.22 -> CTbasic.ctree * Pos.pos' list
8.23 - val cupdate_problem: CTbasic.ctree -> Pos.pos -> References_Def.T * Model_Def.i_model * Model_Def.i_model * Proof.context
8.24 + val cupdate_problem: CTbasic.ctree -> Pos.pos -> References_Def.T * Model_Def.i_model_POS * Model_Def.i_model_POS * Proof.context
8.25 -> CTbasic.ctree * Pos.pos' list
8.26 val append_atomic : (* for solve.sml *)
8.27 Pos.pos -> ((Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context)) ->
8.28 @@ -37,13 +37,15 @@
8.29
8.30 val update_loc' : CTbasic.ctree -> Pos.pos ->
8.31 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree
8.32 +
8.33 \<^isac_test>\<open>
8.34 val append_form: Pos.pos -> Istate_Def.T * Proof.context -> term -> CTbasic.ctree -> CTbasic.ctree
8.35 val append_problem : Pos.pos -> Istate_Def.T * Proof.context -> Model_Def.form_T ->
8.36 Model_Def.o_model * References_Def.T * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree
8.37 - val update_problem: Pos.pos -> References_Def.T * Model_Def.i_model * Model_Def.i_model * Proof.context
8.38 + val update_problem: Pos.pos -> References_Def.T * Model_Def.i_model_POS * Model_Def.i_model_POS * Proof.context
8.39 -> CTbasic.ctree -> CTbasic.ctree
8.40 \<close>
8.41 +
8.42 end
8.43 (**)
8.44 structure CTaccess(**): CALC_TREE_ACCESS(**) =
9.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon Dec 11 09:24:02 2023 +0100
9.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon Dec 11 12:14:28 2023 +0100
9.3 @@ -44,8 +44,8 @@
9.4 val g_spec : ppobj -> References_Def.T
9.5 val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
9.6 val g_form : ppobj -> term
9.7 - val g_pbl : ppobj -> Model_Def.i_model
9.8 - val g_met : ppobj -> Model_Def.i_model
9.9 + val g_pbl : ppobj -> Model_Def.i_model_POS
9.10 + val g_met : ppobj -> Model_Def.i_model_POS
9.11 val g_metID : ppobj -> MethodC.id
9.12 val g_result : ppobj -> Celem.result
9.13 val g_tac : ppobj -> Tactic.input
9.14 @@ -181,8 +181,8 @@
9.15 References_Def.T * (* updated by Refine_Tacitly *)
9.16 term, (* headline of calc-head, as calculated initially(!) *)
9.17 spec : References_Def.T, (* explicitly input *)
9.18 - probl : Model_Def.i_model,(* = I_Model.T for interactive input to a Problem *)
9.19 - meth : Model_Def.i_model,(* = I_Model.T for interactive input to a MethodC *)
9.20 + probl : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a Problem *)
9.21 + meth : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a MethodC *)
9.22 ctxt : Proof.context, (* used while specifying this (Sub-)Problem and MethodC *)
9.23 loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *)
9.24 * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
10.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 11 09:24:02 2023 +0100
10.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 11 12:14:28 2023 +0100
10.3 @@ -139,8 +139,8 @@
10.4 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
10.5 else pI'
10.6 val {model, where_, where_rls, ...} = Problem.from_store ctxt pblID
10.7 - val (model_ok, (pbl, where_)) = M_Match.by_i_models ctxt os
10.8 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
10.9 + val (model_ok, (pbl, where_)) = M_Match.by_i_models ctxt os (probl, meth)
10.10 + (model, where_, where_rls)
10.11 in
10.12 (model_ok, pblID, hdl, pbl, where_)
10.13 end
10.14 @@ -156,8 +156,8 @@
10.15 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
10.16 else mI'
10.17 val {model, where_, where_rls, program, ...} = MethodC.from_store ctxt metID
10.18 - val (model_ok, (pbl, where_)) = M_Match.by_i_models ctxt os
10.19 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
10.20 + val (model_ok, (pbl, where_)) = M_Match.by_i_models ctxt os (probl, meth)
10.21 + (model, where_, where_rls)
10.22 in
10.23 (model_ok, metID, program, pbl, where_)
10.24 end
10.25 @@ -174,12 +174,12 @@
10.26 |> Know_Store.get_via_last_thy
10.27 |> Proof_Context.init_global
10.28 in
10.29 - case Refine.problem (Know_Store.get_via_last_thy "Isac_Knowledge") pI (I_Model.OLD_to_POS probl) of
10.30 + case Refine.problem (Know_Store.get_via_last_thy "Isac_Knowledge") pI probl of
10.31 NONE => (*copy from context_pbl*)
10.32 let
10.33 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI
10.34 - val (_, (pbl, where_)) = M_Match.by_i_models ctxt os
10.35 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
10.36 + val (_, (pbl, where_)) = M_Match.by_i_models ctxt os (probl, meth)
10.37 + (model, where_, where_rls)
10.38 in
10.39 (false, pI, hdl, pbl, where_)
10.40 end
11.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Mon Dec 11 09:24:02 2023 +0100
11.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Mon Dec 11 12:14:28 2023 +0100
11.3 @@ -24,16 +24,16 @@
11.4 fun pt_model (Ctree.PblObj {meth, spec, origin = (_, o_spec, hdl), ctxt, ...}) Pos.Met =
11.5 let
11.6 val (_, _, met_id) = References.select_input o_spec spec
11.7 - val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_POS meth) (Pos.Met, met_id)
11.8 + val (allcorr, _) = Pre_Conds.check_internal ctxt meth (Pos.Met, met_id)
11.9 in
11.10 - Ctree.ModSpec (allcorr, Pos.Met, hdl, (I_Model.OLD_to_POS meth), (*where_*)[(*MethodC.from_store in check*)], spec)
11.11 + Ctree.ModSpec (allcorr, Pos.Met, hdl, meth, (*where_*)[(*MethodC.from_store in check*)], spec)
11.12 end
11.13 | pt_model (Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}) _(*Frm,Pbl*) =
11.14 let
11.15 val (_, _, met_id) = References.select_input o_spec spec
11.16 - val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_POS probl) (Pos.Met, met_id)
11.17 + val (allcorr, _) = Pre_Conds.check_internal ctxt probl (Pos.Met, met_id)
11.18 in
11.19 - Ctree.ModSpec (allcorr, Pos.Pbl, hdl, (I_Model.OLD_to_POS probl), (*where_*)[(*Problem.from_store in check*)], spec)
11.20 + Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec)
11.21 end
11.22 | pt_model _ _ = raise ERROR "pt_model: uncovered definition"
11.23
11.24 @@ -42,7 +42,7 @@
11.25 let
11.26 val (dI, pI, _) = Ctree.get_somespec' spec spec'
11.27 val {cas, model, ...} = Problem.from_store ctxt pI
11.28 - val env_model = Pre_Conds.environment_POS model (I_Model.OLD_to_POS probl)
11.29 + val env_model = Pre_Conds.environment_POS model probl
11.30 in case cas of
11.31 NONE => Ctree.Form (Auto_Prog.pblterm dI pI)
11.32 | SOME t => Ctree.Form (subst_atomic env_model t)
12.1 --- a/src/Tools/isac/Specify/cas-command.sml Mon Dec 11 09:24:02 2023 +0100
12.2 +++ b/src/Tools/isac/Specify/cas-command.sml Mon Dec 11 12:14:28 2023 +0100
12.3 @@ -82,8 +82,8 @@
12.4 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
12.5 ([], References.empty) ([], References.empty, hdt, ctxt)
12.6 val pt = Ctree.update_spec pt [] spec
12.7 - val pt = Ctree.update_pbl pt [] (I_Model.TEST_to_OLD pits)
12.8 - val pt = Ctree.update_met pt [] (I_Model.TEST_to_OLD mits)
12.9 + val pt = Ctree.update_pbl pt [] pits
12.10 + val pt = Ctree.update_met pt [] mits
12.11 in
12.12 SOME (pt, (true, Pos.Met, hdt, mits, where_, spec) : SpecificationC.T)
12.13 end
13.1 --- a/src/Tools/isac/Specify/i-model.sml Mon Dec 11 09:24:02 2023 +0100
13.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon Dec 11 12:14:28 2023 +0100
13.3 @@ -10,8 +10,12 @@
13.4
13.5 type T
13.6 type T_POS
13.7 - val OLD_to_POS: T -> T_POS
13.8 +(*OLD* )
13.9 + val OLD_to_POS: T -> T_POS .. already Test_Isac ok
13.10 + val OLD_to_POS: T_POS -> T_POS
13.11 val TEST_to_OLD: T_POS -> T
13.12 +( *---*)
13.13 +(*NEW*)
13.14 val empty: T
13.15 val empty_POS: T_POS
13.16
13.17 @@ -43,8 +47,11 @@
13.18 val TEST_to_OLD_single: single_POS -> single
13.19
13.20 datatype add_single = Add of single_POS | Err of string
13.21 +(*OLD* )
13.22 val init: Model_Pattern.T -> T
13.23 +( *---*)
13.24 val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
13.25 +(*NEW*)
13.26 val check_single: Proof.context -> m_field -> O_Model.T -> T_POS -> Model_Pattern.T ->
13.27 TermC.as_string -> add_single
13.28 val add_single: theory -> single_POS -> T_POS -> T_POS
13.29 @@ -137,7 +144,11 @@
13.30 (UnparseC.term (ContextC.for_ERROR ()) pid))
13.31 | feedback_OLD_to_POS (Par s) = (Model_Def.Syn_POS s)
13.32 fun OLD_to_POS_single (a, b, c, d, e) = (a, b, c, d, (feedback_OLD_to_POS e, Position.none))
13.33 +(*OLD* )
13.34 fun OLD_to_POS i_old = map OLD_to_POS_single i_old
13.35 +fun OLD_to_POS i_old = I i_old
13.36 +( *---*)
13.37 +(*NEW*)
13.38
13.39 fun feedback_POS_to_OLD (Model_Def.Cor_POS (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
13.40 | feedback_POS_to_OLD (Model_Def.Syn_POS c) = (Syn c)
14.1 --- a/src/Tools/isac/Specify/specification.sml Mon Dec 11 09:24:02 2023 +0100
14.2 +++ b/src/Tools/isac/Specify/specification.sml Mon Dec 11 12:14:28 2023 +0100
14.3 @@ -100,8 +100,7 @@
14.4 | _ => raise ERROR "SpecificationC.is_complete only with PblObj"
14.5 val (_, pbl_id, met_id) = References.select_input o_spec spec
14.6 in
14.7 - I_Model.s_are_complete ctxt oris
14.8 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pbl_id, met_id)
14.9 + I_Model.s_are_complete ctxt oris (probl, itms) (pbl_id, met_id)
14.10 end
14.11
14.12 (** handle acces to Ctree **)
14.13 @@ -109,7 +108,7 @@
14.14 fun get_data (pt, (p, _)) =
14.15 case Ctree.get_obj I pt p of
14.16 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
14.17 - => (I_Model.OLD_to_POS meth, oris, (dI', pI', mI'), I_Model.OLD_to_POS probl, (dI, pI, mI), ctxt)
14.18 + => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
14.19 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
14.20
14.21 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
14.22 @@ -117,7 +116,7 @@
14.23 let
14.24 val (ospec, hdf', spec, probl, ctxt) = case Ctree.get_obj I pt p of
14.25 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} =>
14.26 - (ospec, hdf', spec, I_Model.OLD_to_POS probl, ctxt)
14.27 + (ospec, hdf', spec, probl, ctxt)
14.28 | _ => raise ERROR "get Pbl: uncovered case get_obj"
14.29 val {where_rls, where_, model, ...} =
14.30 Problem.from_store ctxt (#2 (References.select_input ospec spec))
14.31 @@ -130,7 +129,7 @@
14.32 let
14.33 val (ospec, hdf', spec, meth, ctxt) = case Ctree.get_obj I pt p of
14.34 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ctxt, ...} =>
14.35 - (ospec, hdf', spec, I_Model.OLD_to_POS meth, ctxt)
14.36 + (ospec, hdf', spec, meth, ctxt)
14.37 | _ => raise ERROR "get Met: uncovered case get_obj"
14.38 val {where_rls, where_, model, ...} =
14.39 MethodC.from_store ctxt (#3 (References.select_input ospec spec))
15.1 --- a/src/Tools/isac/Specify/specify-step.sml Mon Dec 11 09:24:02 2023 +0100
15.2 +++ b/src/Tools/isac/Specify/specify-step.sml Mon Dec 11 12:14:28 2023 +0100
15.3 @@ -26,8 +26,8 @@
15.4 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
15.5 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
15.6 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
15.7 - val (_, (i_model, _)) = M_Match.by_i_models ctxt o_model' (I_Model.OLD_to_POS i_prob,
15.8 - I_Model.OLD_to_POS i_prob) (m_patt, where_, where_rls);
15.9 + val (_, (i_model, _)) = M_Match.by_i_models ctxt o_model' (i_prob, i_prob)
15.10 + (m_patt, where_, where_rls);
15.11 in
15.12 (o_model', ctxt', i_model)
15.13 end
15.14 @@ -60,7 +60,7 @@
15.15 | _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
15.16 val thy = if dI' = ThyC.id_empty then dI else dI';
15.17 in
15.18 - case Refine.problem (ThyC.get_theory ctxt thy) pI (I_Model.OLD_to_POS itms) of
15.19 + case Refine.problem (ThyC.get_theory ctxt thy) pI itms of
15.20 NONE => Applicable.No
15.21 (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
15.22 | SOME (pI', (i_model, prec)) =>
15.23 @@ -95,9 +95,8 @@
15.24 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
15.25 val {model, where_, where_rls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
15.26 val (check, (i_model, preconds)) = if pI' = Problem.id_empty andalso pI = Problem.id_empty
15.27 - then (false, (I_Model.OLD_to_POS (I_Model.init model), []))
15.28 - else M_Match.by_i_models ctxt oris
15.29 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
15.30 + then (false, (I_Model.init_POS ctxt oris model, []: (bool * term) list))
15.31 + else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
15.32 in
15.33 Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (i_model, preconds))))
15.34 end
15.35 @@ -114,35 +113,35 @@
15.36 (* exceed line length, because result type will change *)
15.37 fun add (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =
15.38 let
15.39 - val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD itms)
15.40 - val pt = Ctree.update_met pt p (I_Model.TEST_to_OLD met)
15.41 + val pt = Ctree.update_pbl pt p itms
15.42 + val pt = Ctree.update_met pt p met
15.43 in
15.44 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
15.45 end
15.46 | add (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
15.47 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet,P_Model.from (Proof_Context.theory_of ctxt) [][]),
15.48 case p_ of
15.49 - Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
15.50 - | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
15.51 + Pos.Pbl => Ctree.update_pbl pt p itmlist
15.52 + | Pos.Met => Ctree.update_met pt p itmlist
15.53 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
15.54 | add (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
15.55 (pos, [], (Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] [])),
15.56 case p_ of
15.57 - Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
15.58 - | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
15.59 + Pos.Pbl => Ctree.update_pbl pt p itmlist
15.60 + | Pos.Met => Ctree.update_met pt p itmlist
15.61 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
15.62 | add (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
15.63 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
15.64 case p_ of
15.65 - Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
15.66 - | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
15.67 + Pos.Pbl => Ctree.update_pbl pt p itmlist
15.68 + | Pos.Met => Ctree.update_met pt p itmlist
15.69 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
15.70 | add (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) =
15.71 (pos, [] , Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
15.72 Ctree.update_domID pt p domID)
15.73 | add (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =
15.74 let
15.75 - val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD itms)
15.76 + val pt = Ctree.update_pbl pt p itms
15.77 val pt = Ctree.update_pblID pt p pI
15.78 in
15.79 ((p, Pos.Pbl), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
15.80 @@ -150,14 +149,14 @@
15.81 | add (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
15.82 let
15.83 val pt = Ctree.update_oris pt p oris
15.84 - val pt = Ctree.update_met pt p (I_Model.TEST_to_OLD itms)
15.85 + val pt = Ctree.update_met pt p itms
15.86 val pt = Ctree.update_metID pt p mID
15.87 in
15.88 ((p, Pos.Met), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
15.89 end
15.90 | add (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) =
15.91 let
15.92 - val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD pbl)
15.93 + val pt = Ctree.update_pbl pt p pbl
15.94 val pt = Ctree.update_orispec pt p (domID, pIre, metID)
15.95 in
15.96 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
16.1 --- a/src/Tools/isac/Specify/specify.sml Mon Dec 11 09:24:02 2023 +0100
16.2 +++ b/src/Tools/isac/Specify/specify.sml Mon Dec 11 12:14:28 2023 +0100
16.3 @@ -134,9 +134,9 @@
16.4 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
16.5 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
16.6 else if p_ = Pos.Pbl then
16.7 - for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met)
16.8 + for_problem ctxt oris (o_refs, refs) (pbl, met)
16.9 else
16.10 - for_method ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met)
16.11 + for_method ctxt oris (o_refs, refs) (pbl, met)
16.12 end
16.13
16.14
16.15 @@ -178,10 +178,9 @@
16.16 | _ => raise ERROR "finish_phase: unvered case get_obj"
16.17 val (_, pI, mI) = References.select_input ospec spec
16.18 val ctxt = Ctree.get_ctxt pt pos
16.19 - val (pits, mits) = I_Model.s_make_complete ctxt oris
16.20 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (pI, mI)
16.21 - val pt = Ctree.update_pblppc pt p (I_Model.TEST_to_OLD pits)
16.22 - val pt = Ctree.update_metppc pt p (I_Model.TEST_to_OLD mits)
16.23 + val (pits, mits) = I_Model.s_make_complete ctxt oris (probl, meth) (pI, mI)
16.24 + val pt = Ctree.update_pblppc pt p pits
16.25 + val pt = Ctree.update_metppc pt p mits
16.26 in (pt, (p, Pos.Met)) end
16.27
16.28 (*
16.29 @@ -195,10 +194,8 @@
16.30 => (itms, oris, probl, o_spec, spec, ctxt)
16.31 | _ => raise ERROR "Specify.do_all: no PblObj"
16.32 val (_, pbl_id', met_id') = References.select_input o_refs spec
16.33 - val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris
16.34 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pbl_id', met_id')
16.35 - val (pt, _) = Ctree.cupdate_problem pt p
16.36 - (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)
16.37 + val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris (probl, itms) (pbl_id', met_id')
16.38 + val (pt, _) = Ctree.cupdate_problem pt p (o_refs, pbl_imod, met_imod, ctxt)
16.39 in
16.40 (pt, (p, Pos.Met))
16.41 end
17.1 --- a/src/Tools/isac/Specify/step-specify.sml Mon Dec 11 09:24:02 2023 +0100
17.2 +++ b/src/Tools/isac/Specify/step-specify.sml Mon Dec 11 12:14:28 2023 +0100
17.3 @@ -32,7 +32,7 @@
17.4 val pbl = I_Model.init_POS ctxt oris model (* fill in descriptions *)
17.5 val (pbl, met) = case cas of
17.6 NONE => (pbl, [])
17.7 - | _ => I_Model.s_make_complete ctxt oris (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (pI, mI)
17.8 + | _ => I_Model.s_make_complete ctxt oris (probl, meth) (pI, mI)
17.9 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
17.10 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
17.11 in
17.12 @@ -72,7 +72,7 @@
17.13 | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"
17.14 val thy = if dI' = ThyC.id_empty then dI else dI'
17.15 in
17.16 - case Refine.problem (ThyC.get_theory ctxt thy) pI (I_Model.OLD_to_POS probl) of
17.17 + case Refine.problem (ThyC.get_theory ctxt thy) pI probl of
17.18 NONE => ("failure", ([], [], ptp))
17.19 | SOME (pI, (i_model, prec)) =>
17.20 let
17.21 @@ -92,9 +92,8 @@
17.22 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
17.23 val (check, (i_model, preconds)) =
17.24 if pI' = Problem.id_empty andalso pI = Problem.id_empty
17.25 - then (false, (I_Model.OLD_to_POS (I_Model.init model), []))
17.26 - else M_Match.by_i_models ctxt oris
17.27 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
17.28 + then (false, (I_Model.init_POS ctxt oris model, []))
17.29 + else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
17.30 val (c, pt) =
17.31 case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
17.32 ((_, Pbl), c, _, pt) => (c, pt)
17.33 @@ -252,7 +251,7 @@
17.34 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
17.35 ([], (dI,pI,mI), hdl, ContextC.empty)
17.36 val pt = update_spec pt [] (dI, pI, mI)
17.37 - val pits = I_Model.init (*Proof_Context.init_global thy*) model
17.38 + val pits = I_Model.init_POS (Proof_Context.init_global thy) [(*o_model*)] model
17.39 val pt = update_pbl pt [] pits
17.40 in ((pt, ([] , Pbl)), []) end
17.41 else
17.42 @@ -264,7 +263,7 @@
17.43 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
17.44 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
17.45 val pt = update_spec pt [] (dI, pI, mI)
17.46 - val mits = I_Model.init (*Proof_Context.init_global thy*) model
17.47 + val mits = I_Model.init_POS (Proof_Context.init_global thy) [(*o_model*)] model
17.48 val pt = update_met pt [] mits
17.49 in ((pt, ([], Met)), []) end
17.50 else (* new example, pepare for interactive modeling *)
18.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Dec 11 09:24:02 2023 +0100
18.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Dec 11 12:14:28 2023 +0100
18.3 @@ -1,6 +1,6 @@
18.4 theory Test_VSCode_Example
18.5 imports "Isac.Build_Isac" (*"Isac.Calculation"*)
18.6 - keywords "Example_POS" :: thy_decl
18.7 + keywords "Example" :: thy_decl
18.8 begin
18.9
18.10 text \<open>
18.11 @@ -10,12 +10,12 @@
18.12
18.13 subsection \<open>Development\<close>
18.14 text \<open>
18.15 - Here we develop the semantics of \<open>Example_POS\<close> as test
18.16 - --- build Outer_Syntax Example_POS n:
18.17 + Here we develop the semantics of \<open>Example\<close> as test
18.18 + --- build Outer_Syntax Example n:
18.19 and save intermediate states as separate tests in test/../preliminary.sml
18.20 as soon as some stable state is achieved.
18.21
18.22 - This way we make all \<open>Example\<close> to \<open>Example_POS\<close> step by step
18.23 + This way we make all \<open>Example\<close> to \<open>Example\<close> step by step
18.24 and finally rename all again to \<open>Example\<close>.
18.25 \<close> ML \<open>
18.26 val ((in_thy, thy_id_pos), (in_pbl, probl_id_pos), (in_met, meth_id_pos)) =
18.27 @@ -51,11 +51,11 @@
18.28 re_eval: References.T -> References.T -> unit;
18.29 (*\-------------------- state of src/../preliminary.sml at that time -------------------------/*)
18.30 \<close> ML \<open> (*for building code copy here
18.31 - calculation.sml --- build Outer_Syntax Example_POS 3 ff*)
18.32 + calculation.sml --- build Outer_Syntax Example 3 ff*)
18.33 \<close> ML \<open>
18.34 \<close> ML \<open>
18.35 val _ =
18.36 - Outer_Syntax.command \<^command_keyword>\<open>Example_POS\<close>
18.37 + Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
18.38 "prepare ISAC problem type and register it to Knowledge Store"
18.39 (Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
18.40 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_pos_model_input --
18.41 @@ -67,11 +67,11 @@
18.42 let
18.43 val state =
18.44 case the_data thy of
18.45 - CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id
18.46 + CTbasic.EmptyPtree => Preliminary.init_ctree thy example_id
18.47 | state =>
18.48 let
18.49 val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
18.50 - CTbasic_POS.get_obj I state [(*Pos todo*)] |> CTbasic_POS.rep_specify_data
18.51 + CTbasic.get_obj I state [(*Pos todo*)] |> CTbasic.rep_specify_data
18.52 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
18.53 val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input (*+check syntax*)
18.54 (*reminder for Template.show ----------------------------------------------------------------\*)
18.55 @@ -80,7 +80,7 @@
18.56 val {model = model_patt, where_ = where_ctree, where_rls, ...} =
18.57 Problem.from_store ctxt pbl_id;
18.58
18.59 -(*/----- ERROR: mk_env not reasonable for "Inc_POS Constants [] [__=__, __=__]"-------------\
18.60 +(*/----- ERROR: mk_env not reasonable for "Inc Constants [] [__=__, __=__]"-------------\
18.61 ------------------------------------------------vvvvvvvvvvvvvvvvvvvvv-----------------------* )
18.62 val (_, env_eval) = Pre_Conds.sep_variants_envs_OLD model_patt probl
18.63 (*------------------- must be completed first -----------------^^^^^*)
18.64 @@ -90,13 +90,13 @@
18.65 NONE => writeln "I_Model.is_complete_OLD --> NONE"
18.66 | SOME variants =>
18.67 writeln ("I_Model.is_complete_OLD --> SOME " ^ LibraryC.ints2str' variants)
18.68 -( *\----- ERROR: mk_env not reasonable for "Inc_POS Constants [] [__=__, __=__]"-------------/*)
18.69 +( *\----- ERROR: mk_env not reasonable for "Inc Constants [] [__=__, __=__]"-------------/*)
18.70 (*reminder for Template.show ----------------------------------------------------------------/*)
18.71
18.72 -(*reminder for Pre_Conds.check_POS ---------------------------------------------------------\* )
18.73 +(*reminder for Pre_Conds.check ---------------------------------------------------------\* )
18.74 val (true, [(true, (Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
18.75 - Free ("r", _), _))]) = Pre_Conds.check_POS ctxt where_rls where_ env_eval;
18.76 -( *reminder for Pre_Conds.check_POS ---------------------------------------------------------/*)
18.77 + Free ("r", _), _))]) = Pre_Conds.check ctxt where_rls where_ env_eval;
18.78 +( *reminder for Pre_Conds.check ---------------------------------------------------------/*)
18.79 (**)
18.80 val ((_, _, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =
18.81 References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref
18.82 @@ -108,7 +108,7 @@
18.83 end
18.84 in set_data state thy end)));
18.85 \<close> ML \<open>
18.86 -\<close> ML \<open> (*Example_POS below*)
18.87 +\<close> ML \<open> (*Example below*)
18.88 \<close>
18.89
18.90 subsection \<open>Mirror from src/../VSCode_Example.thy for testing purposes\<close>
18.91 @@ -116,9 +116,9 @@
18.92 subsubsection \<open>Complete Specification at once\<close>
18.93
18.94 text \<open>
18.95 - Just a test, that this works also in $ISABELLE_ISAC_POS
18.96 + Just a test, that this works also in $ISABELLE_ISAC
18.97 \<close>
18.98 -Example_POS "Diff_App-No.123a" (*complete Specification*)
18.99 +Example "Diff_App-No.123a" (*complete Specification*)
18.100 Specification:
18.101 Model:
18.102 Given: \<open>Constants [r = 7]\<close>
18.103 @@ -137,10 +137,10 @@
18.104 \<close>
18.105 (*
18.106 Example: no syntax check of terms, thus OK.
18.107 -Example_POS: proper syntax check of terms with Model_Pattern.parse_pos,
18.108 +Example: proper syntax check of terms with Model_Pattern.parse_pos,
18.109 *)
18.110 (** )Example
18.111 -( **)Example_POS(**) "Diff_App-No.123a" (*complete Model, empty References*)
18.112 +( **)Example(**) "Diff_App-No.123a" (*complete Model, empty References*)
18.113 Specification:
18.114 Model:
18.115 Given: \<open>Constants [r = 7]\<close>
18.116 @@ -166,7 +166,7 @@
18.117 \<close>
18.118 (*all empty*)
18.119
18.120 -Example_POS "Diff_App-No.123a"
18.121 +Example "Diff_App-No.123a"
18.122 Specification:
18.123 Model:
18.124 Given: \<open>Constants [__=__, __=__]\<close>
18.125 @@ -267,10 +267,10 @@
18.126 ],
18.127 ("Diff_App", "univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus")
18.128 )
18.129 -) CTbasic_POS.EmptyPtree;
18.130 +) CTbasic.EmptyPtree;
18.131 val ptp = (pt, p);
18.132 \<close>
18.133 -Example_POS "Diff_App-No.123a" (*all empty step 0*)
18.134 +Example "Diff_App-No.123a" (*all empty step 0*)
18.135 Specification:
18.136 Model:
18.137 Given: \<open>Constants [__=__, __=__]\<close>
18.138 @@ -295,7 +295,7 @@
18.139 = Step.specify_do_next ptp;
18.140 ( *\---Step.specify_do_next still works with Ctree, not Ctree_POS-------------------*)
18.141 \<close>
18.142 -Example_POS "Diff_App-No.123a" (*step 1: <Constants [r = 7]>*)
18.143 +Example "Diff_App-No.123a" (*step 1: <Constants [r = 7]>*)
18.144 Specification:
18.145 Model:
18.146 Given: \<open>Constants [r = 7]\<close>
18.147 @@ -318,7 +318,7 @@
18.148 = Step.specify_do_next ptp;
18.149 ( *\---Step.specify_do_next still works with Ctree, not Ctree_POS-------------------*)
18.150 \<close>
18.151 -Example_POS "Diff_App-No.123a" (*step 2: AdditionalValues [u]*)
18.152 +Example "Diff_App-No.123a" (*step 2: AdditionalValues [u]*)
18.153 Specification:
18.154 Model:
18.155 Given: \<open>Constants [r = 7]\<close>
18.156 @@ -341,7 +341,7 @@
18.157 ( *\---Step.specify_do_next still works with Ctree, not Ctree_POS-------------------*)
18.158 \<close>
18.159
18.160 -Example_POS "Diff_App-No.123a" (*step 3: A.Values [u, v]*)
18.161 +Example "Diff_App-No.123a" (*step 3: A.Values [u, v]*)
18.162 Specification:
18.163 Model:
18.164 Given: \<open>Constants [r = 7]\<close>
18.165 @@ -359,7 +359,7 @@
18.166 \<close>
18.167 ML \<open> (* # 5: Input to \<open>Problem_Ref\<close> might change the \<open>Model\<close> *)
18.168 \<close>
18.169 -Example_POS "Diff_App-No.123a" (*step 4: (wrong) Problem_Ref input*)
18.170 +Example "Diff_App-No.123a" (*step 4: (wrong) Problem_Ref input*)
18.171 Specification:
18.172 Model:
18.173 Given: \<open>Constants [r = 7]\<close>
18.174 @@ -379,7 +379,7 @@
18.175 \<close>
18.176 ML \<open> (* # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close> *)
18.177 \<close>
18.178 -Example_POS "Diff_App-No.123a" (*step 5: Method_Ref updated*)
18.179 +Example "Diff_App-No.123a" (*step 5: Method_Ref updated*)
18.180 Specification:
18.181 Model: (* FIXME: lookup model of method *)
18.182 Given: \<open>Constants [r = 7]\<close>
18.183 @@ -403,7 +403,7 @@
18.184 text \<open>
18.185 Observe the (still outcommented) toggles \<Odot>\<Otimes> changed according to the Reference
18.186 \<close>
18.187 -Example_POS "Diff_App-No.123a" (*Specification of the Method_Ref*)
18.188 +Example "Diff_App-No.123a" (*Specification of the Method_Ref*)
18.189 Specification:
18.190 Model:
18.191 Given: \<open>Constants [r = 7]\<close> \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>
19.1 --- a/test/Tools/isac/BridgeJEdit/calculation.sml Mon Dec 11 09:24:02 2023 +0100
19.2 +++ b/test/Tools/isac/BridgeJEdit/calculation.sml Mon Dec 11 12:14:28 2023 +0100
19.3 @@ -5,17 +5,17 @@
19.4 "-----------------------------------------------------------------------------------------------";
19.5 "table of contents -----------------------------------------------------------------------------";
19.6 "-----------------------------------------------------------------------------------------------";
19.7 -"----------- build Outer_Syntax Example_POS 1: parse errors shown at the spot -----------------";
19.8 -"----------- build Outer_Syntax Example_POS 2: handle empty input -----------------------------";
19.9 -"----------- build Outer_Syntax Example_POS 3: Pre_Conds.check_POS I_Model.is_complete_OLD ---";
19.10 +"----------- build Outer_Syntax Example 1: parse errors shown at the spot -----------------";
19.11 +"----------- build Outer_Syntax Example 2: handle empty input -----------------------------";
19.12 +"----------- build Outer_Syntax Example 3: Pre_Conds.check_POS I_Model.is_complete_OLD ---";
19.13 "-----------------------------------------------------------------------------------------------";
19.14 "-----------------------------------------------------------------------------------------------";
19.15 "-----------------------------------------------------------------------------------------------";
19.16
19.17
19.18 -"----------- build Outer_Syntax Example_POS 1: parse errors shown at the spot -----------------";
19.19 -"----------- build Outer_Syntax Example_POS 1: parse errors shown at the spot -----------------";
19.20 -"----------- build Outer_Syntax Example_POS 1: parse errors shown at the spot -----------------";
19.21 +"----------- build Outer_Syntax Example 1: parse errors shown at the spot -----------------";
19.22 +"----------- build Outer_Syntax Example 1: parse errors shown at the spot -----------------";
19.23 +"----------- build Outer_Syntax Example 1: parse errors shown at the spot -----------------";
19.24 (*/-------------------- state of src/../preliminary.sml at that time --------------------------\*)
19.25 fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*)))
19.26 fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*)))
19.27 @@ -40,7 +40,7 @@
19.28 re_eval: References.T -> References.T -> unit;
19.29 (*\-------------------- state of src/../preliminary.sml at that time --------------------------/*)
19.30 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
19.31 -(* Example_POS "Diff_App-No.123a" (*complete Model, empty References*) *)
19.32 +(* Example "Diff_App-No.123a" (*complete Model, empty References*) *)
19.33 val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
19.34 val thy = @{theory Calculation}
19.35 val model_input = (*type Position.T is hidden, thus redefinition*)
19.36 @@ -63,11 +63,11 @@
19.37 (*\---------------------------------------- adapt to Test_Isac/_Short.thy ---------------------/*)
19.38 val state =
19.39 case the_data thy of
19.40 - CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id
19.41 + CTbasic.EmptyPtree => Preliminary.init_ctree thy example_id
19.42 | _ => the_data thy
19.43 (*let*)
19.44 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
19.45 - CTbasic_POS.get_obj I (**)ctree(** )(the_data thy)( **) [] |> CTbasic_POS.rep_specify_data
19.46 + CTbasic.get_obj I (**)ctree(** )(the_data thy)( **) [] |> CTbasic.rep_specify_data
19.47 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
19.48 val (model, where_) = Model_Pattern.parse_pos ctxt model_input
19.49 (**)
19.50 @@ -78,11 +78,11 @@
19.51 (*end*);
19.52
19.53
19.54 -"----------- build Outer_Syntax Example_POS 2: handle empty input -----------------------------";
19.55 -"----------- build Outer_Syntax Example_POS 2: handle empty input -----------------------------";
19.56 -"----------- build Outer_Syntax Example_POS 2: handle empty input -----------------------------";
19.57 +"----------- build Outer_Syntax Example 2: handle empty input -----------------------------";
19.58 +"----------- build Outer_Syntax Example 2: handle empty input -----------------------------";
19.59 +"----------- build Outer_Syntax Example 2: handle empty input -----------------------------";
19.60 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
19.61 -(* Example_POS "Diff_App-No.123a" (*complete Model, empty References*) *)
19.62 +(* Example "Diff_App-No.123a" (*complete Model, empty References*) *)
19.63 val thy = @{theory}
19.64 val model_input = (*type Position.T is hidden, thus redefinition*)
19.65 [("#Given", [("Constants [r = 7]", Position.none)]),
19.66 @@ -103,11 +103,11 @@
19.67
19.68 val state =
19.69 case the_data thy of
19.70 - CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id
19.71 + CTbasic.EmptyPtree => Preliminary.init_ctree thy example_id
19.72 | _ => the_data thy
19.73 (*let*)
19.74 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
19.75 - CTbasic_POS.get_obj I state [(*Pos will become variable*)] |> CTbasic_POS.rep_specify_data
19.76 + CTbasic.get_obj I state [(*Pos will become variable*)] |> CTbasic.rep_specify_data
19.77
19.78 (*knows variables from origin + notation (input) undefined ^^^^^ from BaseDefinitions.thy*)
19.79 (*test*)val Const ("Input_Descript.Constants", _) $
19.80 @@ -165,11 +165,11 @@
19.81 (*end*);
19.82
19.83
19.84 -"----------- build Outer_Syntax Example_POS 3: Pre_Conds.check_POS I_Model.is_complete_OLD ---";
19.85 -"----------- build Outer_Syntax Example_POS 3: Pre_Conds.check_POS I_Model.is_complete_OLD ---";
19.86 -"----------- build Outer_Syntax Example_POS 3: Pre_Conds.check_POS I_Model.is_complete_OLD ---";
19.87 +"----------- build Outer_Syntax Example 3: Pre_Conds.check_POS I_Model.is_complete_OLD ---";
19.88 +"----------- build Outer_Syntax Example 3: Pre_Conds.check_POS I_Model.is_complete_OLD ---";
19.89 +"----------- build Outer_Syntax Example 3: Pre_Conds.check_POS I_Model.is_complete_OLD ---";
19.90 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
19.91 -(* Example_POS "Diff_App-No.123a" (*complete Model, empty References*) *)
19.92 +(* Example "Diff_App-No.123a" (*complete Model, empty References*) *)
19.93 val thy = @{theory Calculation}
19.94 val model_input = (*type Position.T is hidden, thus redefinition*)
19.95 [("#Given", [("Constants [r = 7]", Position.none)]),
19.96 @@ -192,11 +192,11 @@
19.97
19.98 val state =
19.99 case the_data thy of
19.100 - CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id
19.101 + CTbasic.EmptyPtree => Preliminary.init_ctree thy example_id
19.102 | _(*state (*FOR TEST*)*) => (**)the_data thy(**)
19.103 (*let*)
19.104 val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
19.105 - CTbasic_POS.get_obj I state [(*Pos will become variable*)] |> CTbasic_POS.rep_specify_data
19.106 + CTbasic.get_obj I state [(*Pos will become variable*)] |> CTbasic.rep_specify_data
19.107 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
19.108 val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input (*+check syntax*);
19.109
20.1 --- a/test/Tools/isac/BridgeJEdit/template.sml Mon Dec 11 09:24:02 2023 +0100
20.2 +++ b/test/Tools/isac/BridgeJEdit/template.sml Mon Dec 11 12:14:28 2023 +0100
20.3 @@ -30,10 +30,10 @@
20.4 : (Model_Pattern.m_field * (string * Position.T) list) list
20.5 val example_id = "Diff_App-No.123a";
20.6 (*----------------------------------------- init state -----------------------------------------*)
20.7 -set_data CTbasic_POS.EmptyPtree @{theory Calculation};
20.8 +set_data CTbasic.EmptyPtree @{theory Calculation};
20.9 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)
20.10
20.11 -val CTbasic_POS.EmptyPtree =
20.12 +val CTbasic.EmptyPtree =
20.13 (*case*) the_data @{theory Calculation} (*of*);
20.14
20.15 (* Calculation.thy..*)
21.1 --- a/test/Tools/isac/BridgeJEdit/vscode-example.sml Mon Dec 11 09:24:02 2023 +0100
21.2 +++ b/test/Tools/isac/BridgeJEdit/vscode-example.sml Mon Dec 11 12:14:28 2023 +0100
21.3 @@ -57,7 +57,7 @@
21.4 ("Diff_App", "univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus")
21.5 (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
21.6 )
21.7 -) CTbasic_POS.EmptyPtree;
21.8 +) CTbasic.EmptyPtree;
21.9 val ptp = (pt, p);
21.10 (*\------- start example as required in VSCode_Example.thy -----------------------------------*)
21.11
22.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Dec 11 09:24:02 2023 +0100
22.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Dec 11 12:14:28 2023 +0100
22.3 @@ -74,8 +74,8 @@
22.4 "~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
22.5 (nxt, p, c, pt);
22.6 val ctxt = Ctree.get_ctxt pt p
22.7 -(*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc
22.8 - ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
22.9 +(*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given",
22.10 + (Inc_POS (Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
22.11 (*-------------------------------------------^^--*)
22.12 val return_step_by_tactic = (*case*)
22.13 Step.by_tactic tac (pt, p) (*of*);
22.14 @@ -645,7 +645,7 @@
22.15 fill_method o_model (pbl_imod, met_imod) m_patt;
22.16 (*////--------------- step into fill_method -----------------------------------------------\\*)
22.17 "~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =
22.18 - (o_model, (pbl_imod, met_imod), m_patt);
22.19 + (o_model, (pbl_imod, met_imod), m_patt);
22.20
22.21 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
22.22 = pbl_imod |> I_Model.to_string_POS ctxt
23.1 --- a/test/Tools/isac/Specify/i-model.sml Mon Dec 11 09:24:02 2023 +0100
23.2 +++ b/test/Tools/isac/Specify/i-model.sml Mon Dec 11 12:14:28 2023 +0100
23.3 @@ -152,7 +152,7 @@
23.4 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
23.5 (*//------------------ step into check_single ----------------------------------------------\\*)
23.6 "~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)
23.7 - = (ctxt, m_field, oris, (I_Model.TEST_to_OLD i_model), m_patt, ct);
23.8 + = (ctxt, m_field, oris, i_model, m_patt, ct);
23.9 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
23.10 handle ERROR msg => error (msg (*^ Position.here pp*))
23.11
23.12 @@ -167,7 +167,7 @@
23.13 (*+*)val [Free ("q_0", _)] = all;
23.14
23.15 (**)val ("", itm) =(**)
23.16 - (*case*) is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt (*of*);
23.17 + (*case*) is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt (*of*);
23.18
23.19 (*+*)val (2, [1], true, "#Given", (Cor_POS (Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), _)) = itm
23.20 (*\\------------------ step into check_single ----------------------------------------------//*)
23.21 @@ -216,10 +216,10 @@
23.22 : (Model_Pattern.m_field * (string * Position.T) list) list
23.23 val example_id = "Diff_App-No.123a";
23.24 (*----------------------------------------- init state -----------------------------------------*)
23.25 -set_data CTbasic_POS.EmptyPtree @{theory Calculation};
23.26 +set_data CTbasic.EmptyPtree @{theory Calculation};
23.27 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)
23.28
23.29 -val CTbasic_POS.EmptyPtree =
23.30 +val CTbasic.EmptyPtree =
23.31 (*case*) the_data @{theory Calculation} (*of*);
23.32
23.33 (* Calculation..*)
24.1 --- a/test/Tools/isac/Specify/pre-conditions.sml Mon Dec 11 09:24:02 2023 +0100
24.2 +++ b/test/Tools/isac/Specify/pre-conditions.sml Mon Dec 11 12:14:28 2023 +0100
24.3 @@ -23,11 +23,11 @@
24.4
24.5 val state =
24.6 case the_data thy of
24.7 - CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id
24.8 + CTbasic.EmptyPtree => Preliminary.init_ctree thy example_id
24.9 | _(*state (*FOR TEST*)*) => (**)the_data thy(**)
24.10 (*let*)
24.11 val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
24.12 - CTbasic_POS.get_obj I state [(*Pos will become variable*)] |> CTbasic_POS.rep_specify_data
24.13 + CTbasic.get_obj I state [(*Pos will become variable*)] |> CTbasic.rep_specify_data
24.14 ;
24.15 (*+*)if (probl |> I_Model.to_string_POS @{context}) = "[\n" ^
24.16 "(1, [1, 2, 3], false ,#Given, (Inc_POS Constants [] [__=__, __=__], Position.T)), \n" ^