# HG changeset patch # User wneuper # Date 1674658353 -3600 # Node ID b7a2ad3b3d458f99e28607d27647070048e91bb2 # Parent 06ec8abfd3bc6fbdb09ee4cfa267a6b6aca988e7 ContextC.build_while_parsing, improves O_Model.init_PIDE diff -r 06ec8abfd3bc -r b7a2ad3b3d45 src/Tools/isac/BaseDefinitions/contextC.sml --- a/src/Tools/isac/BaseDefinitions/contextC.sml Wed Jan 11 11:38:01 2023 +0100 +++ b/src/Tools/isac/BaseDefinitions/contextC.sml Wed Jan 25 15:52:33 2023 +0100 @@ -10,6 +10,7 @@ val isac_ctxt : 'a -> Proof.context val declare_constraints: term -> Proof.context -> Proof.context val add_constraints: term list -> Proof.context -> Proof.context + val build_while_parsing: Formalise.model -> theory -> term list * Proof.context val initialise : Proof.context -> term list -> Proof.context val initialise' : theory -> TermC.as_string list -> Proof.context val get_assumptions : Proof.context -> term list @@ -37,7 +38,20 @@ fun add_constraints ts ctxt = fold Variable.declare_constraints (TermC.vars' ts) ctxt +fun build_while_parsing_ [] (ts, ctxt) = (ts, ctxt) + | build_while_parsing_ (str :: strs) (ts, ctxt) = + let + val t as (_ $ tm) = Syntax.read_term ctxt str + handle ERROR msg => raise ERROR ("ContextC.build_while_parsing " ^ quote str ^ " " ^ msg) + val vars = TermC.vars tm + val ctxt' = add_constraints vars ctxt + in build_while_parsing_ strs (ts @ [t], ctxt') end +(* shouldn't that be done by fold ? + fn: string * Proof.context -> term list * Proof.context -> term list * Proof.context *) +fun build_while_parsing strs thy = build_while_parsing_ strs ([], Proof_Context.init_global thy) + (* in Subproblem take respective actual arguments from program *) +(* FIXME: should be replaced by build_while_parsing *) fun initialise ctxt ts = let val frees = TermC.vars' ts diff -r 06ec8abfd3bc -r b7a2ad3b3d45 src/Tools/isac/BaseDefinitions/termC.sml --- a/src/Tools/isac/BaseDefinitions/termC.sml Wed Jan 11 11:38:01 2023 +0100 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed Jan 25 15:52:33 2023 +0100 @@ -103,13 +103,14 @@ val sym_trm : term -> term (* unused code, kept as hints to design ideas *) val string_of_detail: Proof.context -> term -> string +(*from isac_test for Minisubpbl*) + val atom_typ: Proof.context -> typ -> unit \<^isac_test>\ val mk_negative: typ -> term -> term val mk_Var: term -> term val scala_of_term: term -> string - val atom_typ: Proof.context -> typ -> unit val atom_write: Proof.context -> term -> unit val atom_trace: Proof.context -> term -> unit @@ -190,6 +191,7 @@ scala_of_term t) | scala_of_term (t1 $ t2) = enclose "App(" ")" (scala_of_term t1 ^ ", " ^ scala_of_term t2) +\ (* see structure's bare bones. for Isabelle standard output compare 2017 "structure ML_PP" *) @@ -204,6 +206,8 @@ | atol n (T :: Ts) = (ato n T ^ atol n Ts) in tracing (ato 0 t ^ "\n") end; + +\<^isac_test>\ local fun ato (Const (a, _)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)" | ato (Free (a, _)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)" @@ -525,7 +529,7 @@ | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) (*\----- old versions to be eliminated -------------------------------------------------------/*) -(* to be replaced by parse..*) +(* to be replaced by Syntax.read_term..*) fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str; (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *) fun parse_patt thy str = (thy, str) diff -r 06ec8abfd3bc -r b7a2ad3b3d45 src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Wed Jan 11 11:38:01 2023 +0100 +++ b/src/Tools/isac/Build_Isac.thy Wed Jan 25 15:52:33 2023 +0100 @@ -178,6 +178,117 @@ \ ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml" ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml" +ML \ +\ ML \ +(* Title: 100-init-rootpbl.sml + Author: Walther Neuper 1105 + (c) copyright due to lincense terms. +*) + +"----------- Minisubplb/100-init-rootpbl.sml ---------------------"; +"----------- Minisubplb/100-init-rootpbl.sml ---------------------"; +"----------- Minisubplb/100-init-rootpbl.sml ---------------------"; +val (_(*example text*), + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: + "Extremum (A = 2 * u * v - u \ 2)" :: + "SideConditions [((u::real) / 2) \ 2 + (2 / v) \ 2 = r \ 2]" :: + "SideConditions [((u::real) / 2) \ 2 + (2 / v) \ 2 = r \ 2]" :: + "SideConditions [(u::real) / 2 = r * sin \, 2 / v = r * cos \]" :: + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \" :: + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \ / 2}" :: + "ErrorBound (\ = (0::real))" :: []), + refs as ("Diff_App", + ["univariate_calculus", "Optimisation"], + ["Optimisation", "by_univariate_calculus"]))) + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"]; + + Test_Code.init_calc @{context} [(model, refs)]; +"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) + = (@{context}, [(model, refs)]); +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*) + +(**)val return_nxt_specify_init_calc_PIDE =(**) +Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs); +"~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs)); + +Step_Specify.initialise_PIDE thy (model, refs); +"~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs)); +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*) + val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *) + val (pI, (pors, pctxt), mI) = + if mI = ["no_met"] + then raise error "else not covered by test" + else + let +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) +(*old*) in (pI, (pors, pctxt), mI) end; +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; + in (pI, (pors, pctxt), mI) end; + +(*/------------------- check result of O_Model.init_PIDE ------------------------------------\*) +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r"; +(*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u"; +(*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*) + +val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *); +"~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis) + = ((pt, p), tacis); + val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis; + + Test_Code.TESTg_form ctxt (pt,p); +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p)); + val (form, _, _) = ME_Misc.pt_extract ctxt ptp; +val Ctree.ModSpec (_, p_, _, gfr, where_, _) = + (*case*) form (*of*); +val Pos.Pbl = + (*case*) p_ (*of*); + Test_Out.Problem []; + Test_Out.MethodC []; + +(*val return =*) + Test_Out.PpcKF (Test_Out.Problem [], + P_Model.from (Proof_Context.theory_of ctxt) gfr where_); +"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_); + +(*//------------------ inserted hidden code ------------------------------------------------\\*) +fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))) + | item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c + | item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c + | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))) + | item_from_feedback thy (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))) + | item_from_feedback thy (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid) + | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition" +fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x = + case sel of + "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re} + | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re} + | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re} + | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]} + | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*) + | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"") +fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh = + {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re} +fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term_in_ctxt ctxt term) + | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term_in_ctxt ctxt term); +(*\\------------------ inserted hidden code ------------------------------------------------//*) + + fun coll model [] = model + | coll model ((_, _, _, field, itm_)::itms) = + coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms; + val gfr = coll P_Model.empty itms; + +(*val return =*) + add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_); +"~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh) + = (gfr, (map + (boolterm2item ctxt) where_)); +"~~~~~ fun boolterm2item , args:"; val () = (); +(*\\------------------ step into nxt_specify_init_calc -------------------------------------//*) +\ ML \ +\ ML \ +\ ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml" ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml" ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml" diff -r 06ec8abfd3bc -r b7a2ad3b3d45 src/Tools/isac/Specify/o-model.sml --- a/src/Tools/isac/Specify/o-model.sml Wed Jan 11 11:38:01 2023 +0100 +++ b/src/Tools/isac/Specify/o-model.sml Wed Jan 25 15:52:33 2023 +0100 @@ -32,6 +32,7 @@ val single_empty: single val init: theory -> Formalise.model -> Model_Pattern.T -> T + val init_PIDE: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context val values : T -> term list val values': Proof.context -> T -> Formalise.model * term list val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context @@ -179,7 +180,23 @@ |> add_enumerate |> map flattup; in model' end; - +fun init_PIDE _ [] _ = ([], ContextC.empty) + | init_PIDE thy fmz pbt = + let + val (ts, ctxt) = ContextC.build_while_parsing fmz thy + val model = + (map (fn t => t + |> Input_Descript.split + |> add_field thy pbt) ts) + |> add_variants; + val maxv = model |> map fst |> max_variant; + val maxv = if maxv = 0 then 1 else maxv; + val model' = model + |> collect_variants + |> map (replace_0 maxv |> apfst) + |> add_enumerate + |> map flattup + in (model', ctxt) end (** get the values **) diff -r 06ec8abfd3bc -r b7a2ad3b3d45 src/Tools/isac/Specify/step-specify.sml --- a/src/Tools/isac/Specify/step-specify.sml Wed Jan 11 11:38:01 2023 +0100 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Jan 25 15:52:33 2023 +0100 @@ -11,7 +11,10 @@ val initialise: Proof.context -> Formalise.T -> term * term * References.T * O_Model.T * Proof.context + val initialise_PIDE: theory -> Formalise.T -> + term * term * References.T * O_Model.T * Proof.context val nxt_specify_init_calc: Proof.context -> Formalise.T -> Calc.T * State_Steps.T + val nxt_specify_init_calc_PIDE: theory -> Formalise.T -> Calc.T * State_Steps.T end (**) @@ -246,6 +249,40 @@ in (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt) end; +(* initialise <-?-> nxt_specify_init_calc *) +fun initialise_PIDE thy (fmz, (_, pI, mI)) = + let +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*) + val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *) + val (pI, (pors, pctxt), mI) = + if mI = ["no_met"] + then + let +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; + val pI' = Refine.refine_ori' pctxt pors pI; + in (pI', (pors (*refinement over models with diff.precond only*), pctxt), + (hd o #solve_mets o Problem.from_store ctxt) pI') + end + else + let +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) +(*old*) in (pI, (pors, pctxt), mI) end; +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; + in (pI, (pors, pctxt), mI) end; + val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*) + val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy')) + val hdl = case cas of + NONE => Auto_Prog.pblterm dI pI + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t + val hdlPIDE = case cas of + NONE => Auto_Prog.pblterm dI pI + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t + in + (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt) + end; (*TODO: HOW RELATES nxt_specify_init_calc \ initialise *) fun nxt_specify_init_calc ctxt ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*) if pI <> [] @@ -286,5 +323,44 @@ in ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl)))) end - +fun nxt_specify_init_calc_PIDE thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*) + if pI <> [] + then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *) + let + val {cas, solve_mets, model, thy, ...} = Problem.from_store (Proof_Context.init_global thy) pI + val dI = if dI = "" then Context.theory_name thy else dI + val mI = if mI = [] then hd solve_mets else mI + val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI)) + ([], (dI,pI,mI), hdl, ContextC.empty) + val pt = update_spec pt [] (dI, pI, mI) + val pits = I_Model.init model + val pt = update_pbl pt [] pits + in ((pt, ([] , Pbl)), []) end + else + if mI <> [] + then (* from met-browser *) + let + val {model, ...} = MethodC.from_store (Proof_Context.init_global thy) mI + val dI = if dI = "" then "Isac_Knowledge" else dI + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) + ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty) + val pt = update_spec pt [] (dI, pI, mI) + val mits = I_Model.init model + val pt = update_met pt [] mits + in ((pt, ([], Met)), []) end + else (* new example, pepare for interactive modeling *) + let + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) + ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty) + in ((pt, ([], Pbl)), []) end + | nxt_specify_init_calc_PIDE thy (model, refs) = + let (* both ^^^^^ ^^^^^^^^^^^^ are either empty or complete *) + val (_, hdl, refs, pors, pctxt) = initialise_PIDE thy (model, refs) + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) + (model, refs) (pors, refs, hdl, pctxt) + in + ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl)))) + end + (**)end(**) diff -r 06ec8abfd3bc -r b7a2ad3b3d45 src/Tools/isac/Test_Code/test-code.sml --- a/src/Tools/isac/Test_Code/test-code.sml Wed Jan 11 11:38:01 2023 +0100 +++ b/src/Tools/isac/Test_Code/test-code.sml Wed Jan 25 15:52:33 2023 +0100 @@ -57,8 +57,9 @@ (* create a calc-tree *) fun init_calc ctxt [(model, refs as (thy_id, _, _))] = let - val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global - val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (model, refs) +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*) + val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs) val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis val f = TESTg_form ctxt (pt,p) in (p, []:NEW, f, tac, Celem.Sundef, pt) end diff -r 06ec8abfd3bc -r b7a2ad3b3d45 test/Tools/isac/Knowledge/eqsystem-1.sml --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Jan 11 11:38:01 2023 +0100 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Jan 25 15:52:33 2023 +0100 @@ -301,7 +301,7 @@ ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node)); val {thy, model, where_, where_rls, ...} = py ; "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model); - val ctxt = Proof_Context.init_global thy; + val (ts, ctxt) = ContextC.build_while_parsing fmz thy; "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt); fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of (_, _::_) => (Free (v,T)::get_vars vs) diff -r 06ec8abfd3bc -r b7a2ad3b3d45 test/Tools/isac/MathEngine/mathengine-stateless.sml --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Jan 11 11:38:01 2023 +0100 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Jan 25 15:52:33 2023 +0100 @@ -122,8 +122,7 @@ val thy = ThyC.get_theory dI val ctxt = Proof_Context.init_global thy; (*if*) mI = ["no_met"](*else*); - val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; - val pctxt = ContextC.initialise' thy fmz; + val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*) "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*) val dI = Context.theory_name (ThyC.parent_of thy thy'); diff -r 06ec8abfd3bc -r b7a2ad3b3d45 test/Tools/isac/Minisubpbl/100-init-rootpbl.sml --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Jan 11 11:38:01 2023 +0100 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Jan 25 15:52:33 2023 +0100 @@ -23,28 +23,35 @@ Test_Code.init_calc @{context} [(model, refs)]; "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) = (@{context}, [(model, refs)]); - val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global - val ((pt''', p'''), tacis''') = (* keep for continuation *) +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*) -Step_Specify.nxt_specify_init_calc ctxt (model, refs); +(**)val return_nxt_specify_init_calc_PIDE =(**) +Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs); "~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs)); -Step_Specify.initialise ctxt (model, refs); +Step_Specify.initialise_PIDE thy (model, refs); "~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs)); - val thy = ThyC.get_theory_PIDE ctxt dI - val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *) +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*) + val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *) val (pI, (pors, pctxt), mI) = - if mI = ["no_met"] - then raise error "else not covered by test" - else - let - val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) - val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) - in (pI, (pors, pctxt), mI) end; + if mI = ["no_met"] + then raise error "else not covered by test" + else + let +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) +(*old*) in (pI, (pors, pctxt), mI) end; +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; + in (pI, (pors, pctxt), mI) end; +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r"; +(*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u"; (*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*) + +val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *); "~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis) - = ((pt''', p'''), tacis'''); + = ((pt, p), tacis); val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis; Test_Code.TESTg_form ctxt (pt,p); diff -r 06ec8abfd3bc -r b7a2ad3b3d45 test/Tools/isac/Test_Theory.thy --- a/test/Tools/isac/Test_Theory.thy Wed Jan 11 11:38:01 2023 +0100 +++ b/test/Tools/isac/Test_Theory.thy Wed Jan 25 15:52:33 2023 +0100 @@ -77,7 +77,7 @@ \ ML \ \ -section \=================================================================\ +section \=========="Minisubpbl/100-init-rootpbl.sml"========================================\ ML \ \ ML \ \ ML \