1.1 --- a/src/Tools/isac/BaseDefinitions/contextC.sml Wed Jan 11 11:38:01 2023 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/contextC.sml Wed Jan 25 15:52:33 2023 +0100
1.3 @@ -10,6 +10,7 @@
1.4 val isac_ctxt : 'a -> Proof.context
1.5 val declare_constraints: term -> Proof.context -> Proof.context
1.6 val add_constraints: term list -> Proof.context -> Proof.context
1.7 + val build_while_parsing: Formalise.model -> theory -> term list * Proof.context
1.8 val initialise : Proof.context -> term list -> Proof.context
1.9 val initialise' : theory -> TermC.as_string list -> Proof.context
1.10 val get_assumptions : Proof.context -> term list
1.11 @@ -37,7 +38,20 @@
1.12 fun add_constraints ts ctxt =
1.13 fold Variable.declare_constraints (TermC.vars' ts) ctxt
1.14
1.15 +fun build_while_parsing_ [] (ts, ctxt) = (ts, ctxt)
1.16 + | build_while_parsing_ (str :: strs) (ts, ctxt) =
1.17 + let
1.18 + val t as (_ $ tm) = Syntax.read_term ctxt str
1.19 + handle ERROR msg => raise ERROR ("ContextC.build_while_parsing " ^ quote str ^ " " ^ msg)
1.20 + val vars = TermC.vars tm
1.21 + val ctxt' = add_constraints vars ctxt
1.22 + in build_while_parsing_ strs (ts @ [t], ctxt') end
1.23 +(* shouldn't that be done by fold ?
1.24 + fn: string * Proof.context -> term list * Proof.context -> term list * Proof.context *)
1.25 +fun build_while_parsing strs thy = build_while_parsing_ strs ([], Proof_Context.init_global thy)
1.26 +
1.27 (* in Subproblem take respective actual arguments from program *)
1.28 +(* FIXME: should be replaced by build_while_parsing *)
1.29 fun initialise ctxt ts =
1.30 let
1.31 val frees = TermC.vars' ts
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Wed Jan 11 11:38:01 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed Jan 25 15:52:33 2023 +0100
2.3 @@ -103,13 +103,14 @@
2.4 val sym_trm : term -> term (* unused code, kept as hints to design ideas *)
2.5
2.6 val string_of_detail: Proof.context -> term -> string
2.7 +(*from isac_test for Minisubpbl*)
2.8 + val atom_typ: Proof.context -> typ -> unit
2.9
2.10 \<^isac_test>\<open>
2.11 val mk_negative: typ -> term -> term
2.12 val mk_Var: term -> term
2.13 val scala_of_term: term -> string
2.14
2.15 - val atom_typ: Proof.context -> typ -> unit
2.16 val atom_write: Proof.context -> term -> unit
2.17 val atom_trace: Proof.context -> term -> unit
2.18
2.19 @@ -190,6 +191,7 @@
2.20 scala_of_term t)
2.21 | scala_of_term (t1 $ t2) =
2.22 enclose "App(" ")" (scala_of_term t1 ^ ", " ^ scala_of_term t2)
2.23 +\<close>
2.24
2.25 (* see structure's bare bones.
2.26 for Isabelle standard output compare 2017 "structure ML_PP" *)
2.27 @@ -204,6 +206,8 @@
2.28 | atol n (T :: Ts) = (ato n T ^ atol n Ts)
2.29 in tracing (ato 0 t ^ "\n") end;
2.30
2.31 +
2.32 +\<^isac_test>\<open>
2.33 local
2.34 fun ato (Const (a, _)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)"
2.35 | ato (Free (a, _)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)"
2.36 @@ -525,7 +529,7 @@
2.37 | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
2.38 (*\----- old versions to be eliminated -------------------------------------------------------/*)
2.39
2.40 -(* to be replaced by parse..*)
2.41 +(* to be replaced by Syntax.read_term..*)
2.42 fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
2.43 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
2.44 fun parse_patt thy str = (thy, str)
3.1 --- a/src/Tools/isac/Build_Isac.thy Wed Jan 11 11:38:01 2023 +0100
3.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Jan 25 15:52:33 2023 +0100
3.3 @@ -178,6 +178,117 @@
3.4 \<close>
3.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
3.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
3.7 +ML \<open>
3.8 +\<close> ML \<open>
3.9 +(* Title: 100-init-rootpbl.sml
3.10 + Author: Walther Neuper 1105
3.11 + (c) copyright due to lincense terms.
3.12 +*)
3.13 +
3.14 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
3.15 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
3.16 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
3.17 +val (_(*example text*),
3.18 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
3.19 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
3.20 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
3.21 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
3.22 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
3.23 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
3.24 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
3.25 + "ErrorBound (\<epsilon> = (0::real))" :: []),
3.26 + refs as ("Diff_App",
3.27 + ["univariate_calculus", "Optimisation"],
3.28 + ["Optimisation", "by_univariate_calculus"])))
3.29 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
3.30 +
3.31 + Test_Code.init_calc @{context} [(model, refs)];
3.32 +"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
3.33 + = (@{context}, [(model, refs)]);
3.34 +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
3.35 +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
3.36 +
3.37 +(**)val return_nxt_specify_init_calc_PIDE =(**)
3.38 +Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs);
3.39 +"~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
3.40 +
3.41 +Step_Specify.initialise_PIDE thy (model, refs);
3.42 +"~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
3.43 +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
3.44 + val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)
3.45 + val (pI, (pors, pctxt), mI) =
3.46 + if mI = ["no_met"]
3.47 + then raise error "else not covered by test"
3.48 + else
3.49 + let
3.50 +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
3.51 +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
3.52 +(*old*) in (pI, (pors, pctxt), mI) end;
3.53 +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
3.54 + in (pI, (pors, pctxt), mI) end;
3.55 +
3.56 +(*/------------------- check result of O_Model.init_PIDE ------------------------------------\*)
3.57 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
3.58 +(*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";
3.59 +(*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*)
3.60 +
3.61 +val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *);
3.62 +"~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
3.63 + = ((pt, p), tacis);
3.64 + val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
3.65 +
3.66 + Test_Code.TESTg_form ctxt (pt,p);
3.67 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
3.68 + val (form, _, _) = ME_Misc.pt_extract ctxt ptp;
3.69 +val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
3.70 + (*case*) form (*of*);
3.71 +val Pos.Pbl =
3.72 + (*case*) p_ (*of*);
3.73 + Test_Out.Problem [];
3.74 + Test_Out.MethodC [];
3.75 +
3.76 +(*val return =*)
3.77 + Test_Out.PpcKF (Test_Out.Problem [],
3.78 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_);
3.79 +"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
3.80 +
3.81 +(*//------------------ inserted hidden code ------------------------------------------------\\*)
3.82 +fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
3.83 + | item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c
3.84 + | item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c
3.85 + | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
3.86 + | item_from_feedback thy (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
3.87 + | item_from_feedback thy (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid)
3.88 + | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
3.89 +fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
3.90 + case sel of
3.91 + "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
3.92 + | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
3.93 + | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
3.94 + | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
3.95 + | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
3.96 + | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
3.97 +fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
3.98 + {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
3.99 +fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term_in_ctxt ctxt term)
3.100 + | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term_in_ctxt ctxt term);
3.101 +(*\\------------------ inserted hidden code ------------------------------------------------//*)
3.102 +
3.103 + fun coll model [] = model
3.104 + | coll model ((_, _, _, field, itm_)::itms) =
3.105 + coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
3.106 + val gfr = coll P_Model.empty itms;
3.107 +
3.108 +(*val return =*)
3.109 + add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_);
3.110 +"~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh)
3.111 + = (gfr, (map
3.112 + (boolterm2item ctxt) where_));
3.113 +"~~~~~ fun boolterm2item , args:"; val () = ();
3.114 +(*\\------------------ step into nxt_specify_init_calc -------------------------------------//*)
3.115 +\<close> ML \<open>
3.116 +\<close> ML \<open>
3.117 +\<close>
3.118 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
3.119 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
3.120 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
4.1 --- a/src/Tools/isac/Specify/o-model.sml Wed Jan 11 11:38:01 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/o-model.sml Wed Jan 25 15:52:33 2023 +0100
4.3 @@ -32,6 +32,7 @@
4.4 val single_empty: single
4.5
4.6 val init: theory -> Formalise.model -> Model_Pattern.T -> T
4.7 + val init_PIDE: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context
4.8 val values : T -> term list
4.9 val values': Proof.context -> T -> Formalise.model * term list
4.10 val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context
4.11 @@ -179,7 +180,23 @@
4.12 |> add_enumerate
4.13 |> map flattup;
4.14 in model' end;
4.15 -
4.16 +fun init_PIDE _ [] _ = ([], ContextC.empty)
4.17 + | init_PIDE thy fmz pbt =
4.18 + let
4.19 + val (ts, ctxt) = ContextC.build_while_parsing fmz thy
4.20 + val model =
4.21 + (map (fn t => t
4.22 + |> Input_Descript.split
4.23 + |> add_field thy pbt) ts)
4.24 + |> add_variants;
4.25 + val maxv = model |> map fst |> max_variant;
4.26 + val maxv = if maxv = 0 then 1 else maxv;
4.27 + val model' = model
4.28 + |> collect_variants
4.29 + |> map (replace_0 maxv |> apfst)
4.30 + |> add_enumerate
4.31 + |> map flattup
4.32 + in (model', ctxt) end
4.33
4.34 (** get the values **)
4.35
5.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Jan 11 11:38:01 2023 +0100
5.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Jan 25 15:52:33 2023 +0100
5.3 @@ -11,7 +11,10 @@
5.4
5.5 val initialise: Proof.context -> Formalise.T ->
5.6 term * term * References.T * O_Model.T * Proof.context
5.7 + val initialise_PIDE: theory -> Formalise.T ->
5.8 + term * term * References.T * O_Model.T * Proof.context
5.9 val nxt_specify_init_calc: Proof.context -> Formalise.T -> Calc.T * State_Steps.T
5.10 + val nxt_specify_init_calc_PIDE: theory -> Formalise.T -> Calc.T * State_Steps.T
5.11 end
5.12
5.13 (**)
5.14 @@ -246,6 +249,40 @@
5.15 in
5.16 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
5.17 end;
5.18 +(* initialise <-?-> nxt_specify_init_calc *)
5.19 +fun initialise_PIDE thy (fmz, (_, pI, mI)) =
5.20 + let
5.21 +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
5.22 + val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)
5.23 + val (pI, (pors, pctxt), mI) =
5.24 + if mI = ["no_met"]
5.25 + then
5.26 + let
5.27 +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
5.28 +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
5.29 +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
5.30 + val pI' = Refine.refine_ori' pctxt pors pI;
5.31 + in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
5.32 + (hd o #solve_mets o Problem.from_store ctxt) pI')
5.33 + end
5.34 + else
5.35 + let
5.36 +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
5.37 +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
5.38 +(*old*) in (pI, (pors, pctxt), mI) end;
5.39 +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
5.40 + in (pI, (pors, pctxt), mI) end;
5.41 + val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
5.42 + val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy'))
5.43 + val hdl = case cas of
5.44 + NONE => Auto_Prog.pblterm dI pI
5.45 + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
5.46 + val hdlPIDE = case cas of
5.47 + NONE => Auto_Prog.pblterm dI pI
5.48 + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
5.49 + in
5.50 + (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
5.51 + end;
5.52 (*TODO: HOW RELATES nxt_specify_init_calc \<longleftrightarrow> initialise *)
5.53 fun nxt_specify_init_calc ctxt ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
5.54 if pI <> []
5.55 @@ -286,5 +323,44 @@
5.56 in
5.57 ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
5.58 end
5.59 -
5.60 +fun nxt_specify_init_calc_PIDE thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
5.61 + if pI <> []
5.62 + then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
5.63 + let
5.64 + val {cas, solve_mets, model, thy, ...} = Problem.from_store (Proof_Context.init_global thy) pI
5.65 + val dI = if dI = "" then Context.theory_name thy else dI
5.66 + val mI = if mI = [] then hd solve_mets else mI
5.67 + val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
5.68 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
5.69 + ([], (dI,pI,mI), hdl, ContextC.empty)
5.70 + val pt = update_spec pt [] (dI, pI, mI)
5.71 + val pits = I_Model.init model
5.72 + val pt = update_pbl pt [] pits
5.73 + in ((pt, ([] , Pbl)), []) end
5.74 + else
5.75 + if mI <> []
5.76 + then (* from met-browser *)
5.77 + let
5.78 + val {model, ...} = MethodC.from_store (Proof_Context.init_global thy) mI
5.79 + val dI = if dI = "" then "Isac_Knowledge" else dI
5.80 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
5.81 + ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
5.82 + val pt = update_spec pt [] (dI, pI, mI)
5.83 + val mits = I_Model.init model
5.84 + val pt = update_met pt [] mits
5.85 + in ((pt, ([], Met)), []) end
5.86 + else (* new example, pepare for interactive modeling *)
5.87 + let
5.88 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
5.89 + ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)
5.90 + in ((pt, ([], Pbl)), []) end
5.91 + | nxt_specify_init_calc_PIDE thy (model, refs) =
5.92 + let (* both ^^^^^ ^^^^^^^^^^^^ are either empty or complete *)
5.93 + val (_, hdl, refs, pors, pctxt) = initialise_PIDE thy (model, refs)
5.94 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
5.95 + (model, refs) (pors, refs, hdl, pctxt)
5.96 + in
5.97 + ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
5.98 + end
5.99 +
5.100 (**)end(**)
6.1 --- a/src/Tools/isac/Test_Code/test-code.sml Wed Jan 11 11:38:01 2023 +0100
6.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Wed Jan 25 15:52:33 2023 +0100
6.3 @@ -57,8 +57,9 @@
6.4 (* create a calc-tree *)
6.5 fun init_calc ctxt [(model, refs as (thy_id, _, _))] =
6.6 let
6.7 - val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
6.8 - val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
6.9 +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
6.10 +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
6.11 + val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs)
6.12 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
6.13 val f = TESTg_form ctxt (pt,p)
6.14 in (p, []:NEW, f, tac, Celem.Sundef, pt) end
7.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Jan 11 11:38:01 2023 +0100
7.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Jan 25 15:52:33 2023 +0100
7.3 @@ -301,7 +301,7 @@
7.4 ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
7.5 val {thy, model, where_, where_rls, ...} = py ;
7.6 "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);
7.7 - val ctxt = Proof_Context.init_global thy;
7.8 + val (ts, ctxt) = ContextC.build_while_parsing fmz thy;
7.9 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
7.10 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
7.11 (_, _::_) => (Free (v,T)::get_vars vs)
8.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Jan 11 11:38:01 2023 +0100
8.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Jan 25 15:52:33 2023 +0100
8.3 @@ -122,8 +122,7 @@
8.4 val thy = ThyC.get_theory dI
8.5 val ctxt = Proof_Context.init_global thy;
8.6 (*if*) mI = ["no_met"](*else*);
8.7 - val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
8.8 - val pctxt = ContextC.initialise' thy fmz;
8.9 + val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
8.10 val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*)
8.11 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
8.12 val dI = Context.theory_name (ThyC.parent_of thy thy');
9.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Jan 11 11:38:01 2023 +0100
9.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Jan 25 15:52:33 2023 +0100
9.3 @@ -23,28 +23,35 @@
9.4 Test_Code.init_calc @{context} [(model, refs)];
9.5 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
9.6 = (@{context}, [(model, refs)]);
9.7 - val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
9.8 - val ((pt''', p'''), tacis''') = (* keep for continuation *)
9.9 +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
9.10 +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
9.11
9.12 -Step_Specify.nxt_specify_init_calc ctxt (model, refs);
9.13 +(**)val return_nxt_specify_init_calc_PIDE =(**)
9.14 +Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs);
9.15 "~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
9.16
9.17 -Step_Specify.initialise ctxt (model, refs);
9.18 +Step_Specify.initialise_PIDE thy (model, refs);
9.19 "~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
9.20 - val thy = ThyC.get_theory_PIDE ctxt dI
9.21 - val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)
9.22 +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
9.23 + val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)
9.24 val (pI, (pors, pctxt), mI) =
9.25 - if mI = ["no_met"]
9.26 - then raise error "else not covered by test"
9.27 - else
9.28 - let
9.29 - val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
9.30 - val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
9.31 - in (pI, (pors, pctxt), mI) end;
9.32 + if mI = ["no_met"]
9.33 + then raise error "else not covered by test"
9.34 + else
9.35 + let
9.36 +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
9.37 +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
9.38 +(*old*) in (pI, (pors, pctxt), mI) end;
9.39 +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
9.40 + in (pI, (pors, pctxt), mI) end;
9.41
9.42 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
9.43 +(*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";
9.44 (*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*)
9.45 +
9.46 +val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *);
9.47 "~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
9.48 - = ((pt''', p'''), tacis''');
9.49 + = ((pt, p), tacis);
9.50 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
9.51
9.52 Test_Code.TESTg_form ctxt (pt,p);
10.1 --- a/test/Tools/isac/Test_Theory.thy Wed Jan 11 11:38:01 2023 +0100
10.2 +++ b/test/Tools/isac/Test_Theory.thy Wed Jan 25 15:52:33 2023 +0100
10.3 @@ -77,7 +77,7 @@
10.4 \<close> ML \<open>
10.5 \<close>
10.6
10.7 -section \<open>=================================================================\<close>
10.8 +section \<open>=========="Minisubpbl/100-init-rootpbl.sml"========================================\<close>
10.9 ML \<open>
10.10 \<close> ML \<open>
10.11 \<close> ML \<open>