1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Jan 25 17:51:52 2023 +0100
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Jan 25 18:35:02 2023 +0100
1.3 @@ -101,9 +101,8 @@
1.4 val example_id' = References_Def.explode_id example_id
1.5 val (_, (fmz as (model, refs as (_(*thy_id*), probl_id, _)))) =
1.6 Store.get (Know_Store.get_expls @{theory}) example_id' example_id'
1.7 - val ctxt = ContextC.initialise' thy model;
1.8 -
1.9 - val o_model = Problem.from_store ctxt probl_id |> #model |> O_Model.init thy model
1.10 + val (o_model, ctxt) = Problem.from_store (Proof_Context.init_global thy) probl_id
1.11 + |> #model |> O_Model.init thy model
1.12 in
1.13 Ctree.Nd (Ctree.PblObj {
1.14 fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)),
2.1 --- a/src/Tools/isac/Specify/m-match.sml Wed Jan 25 17:51:52 2023 +0100
2.2 +++ b/src/Tools/isac/Specify/m-match.sml Wed Jan 25 18:35:02 2023 +0100
2.3 @@ -141,7 +141,7 @@
2.4 (* match a formalization with a problem type, for tests *)
2.5 fun match_pbl fmz ({thy = thy, where_ = where_, model, where_rls = er, ...}: Problem.T) =
2.6 let
2.7 - val oris = O_Model.init thy fmz model(* |> #1*);
2.8 + val (oris, _) = O_Model.init thy fmz model(* |> #1*);
2.9 val (bool, (itms, where_')) = match_oris' thy oris (model, where_, er);
2.10 in
2.11 if bool
3.1 --- a/src/Tools/isac/Specify/o-model.sml Wed Jan 25 17:51:52 2023 +0100
3.2 +++ b/src/Tools/isac/Specify/o-model.sml Wed Jan 25 18:35:02 2023 +0100
3.3 @@ -31,8 +31,7 @@
3.4 val single_to_string: single -> string
3.5 val single_empty: single
3.6
3.7 - val init: theory -> Formalise.model -> Model_Pattern.T -> T
3.8 - val init_PIDE: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context
3.9 + val init: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context
3.10 val values : T -> term list
3.11 val values': Proof.context -> T -> Formalise.model * term list
3.12 val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context
3.13 @@ -163,26 +162,9 @@
3.14
3.15 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
3.16
3.17 -fun init _ [] _ = []
3.18 +fun init _ [] _ = ([], ContextC.empty)
3.19 | init thy fmz pbt =
3.20 let
3.21 - val model =
3.22 - (map (fn str => str
3.23 - |> TermC.parseNEW'' thy
3.24 - |> Input_Descript.split
3.25 - |> add_field thy pbt) fmz)
3.26 - |> add_variants;
3.27 - val maxv = model |> map fst |> max_variant;
3.28 - val maxv = if maxv = 0 then 1 else maxv;
3.29 - val model' = model
3.30 - |> collect_variants
3.31 - |> map (replace_0 maxv |> apfst)
3.32 - |> add_enumerate
3.33 - |> map flattup;
3.34 - in model' end;
3.35 -fun init_PIDE _ [] _ = ([], ContextC.empty)
3.36 - | init_PIDE thy fmz pbt =
3.37 - let
3.38 val (ts, ctxt) = ContextC.build_while_parsing fmz thy
3.39 val model =
3.40 (map (fn t => t
4.1 --- a/src/Tools/isac/Specify/p-spec.sml Wed Jan 25 17:51:52 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Jan 25 18:35:02 2023 +0100
4.3 @@ -220,52 +220,54 @@
4.4 spec = sspec as (sdI, spI, smI), probl, meth, ...}
4.5 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
4.6 | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
4.7 - val ctxt = Proof_Context.init_global (ThyC.get_theory sdI)
4.8 - in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.parse ctxt hdf))
4.9 - else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
4.10 + val thy = Know_Store.get_via_last_thy dI
4.11 +(** ) val ctxt = Proof_Context.init_global (ThyC.get_theory sdI)( **)
4.12 + in if CAS_Cmd.is_from hdf fmz
4.13 + then the (CAS_Cmd.input (TermC.parse (Proof_Context.init_global thy) hdf))
4.14 + else
4.15 let val (pos_, pits, mits) =
4.16 if dI <> sdI
4.17 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
4.18 val (its, trms) = filter_sep is_Par its;
4.19 - val pbt =
4.20 - (#model o Problem.from_store ctxt) (#2 (References.select_input ospec sspec))
4.21 + val pbt = (#model o Problem.from_store (Proof_Context.init_global thy))
4.22 + (#2 (References.select_input ospec sspec))
4.23 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
4.24 else
4.25 if pI <> spI
4.26 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
4.27 else
4.28 - let val pbt = (#model o Problem.from_store ctxt) pI
4.29 + let val pbt = (#model o Problem.from_store (Proof_Context.init_global thy)) pI
4.30 val dI' = #1 (References.select_input ospec spec)
4.31 val oris =
4.32 if pI = #2 ospec then oris
4.33 - else O_Model.init (ThyC.get_theory "Isac_Knowledge") fmz_ pbt(* |> #1*);
4.34 + else O_Model.init thy fmz_ pbt |> #1;
4.35 in (Pos.Pbl, appl_adds dI' oris probl pbt
4.36 (map itms2fstr probl), meth) end
4.37 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
4.38 - then let val met = (#model o MethodC.from_store ctxt) mI
4.39 + then let val met = (#model o MethodC.from_store (Proof_Context.init_global thy)) mI
4.40 val mits = I_Model.complete oris probl meth met
4.41 in if foldl and_ (true, map #3 mits)
4.42 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
4.43 end
4.44 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
4.45 - ((#model o Problem.from_store ctxt)
4.46 + ((#model o Problem.from_store (Proof_Context.init_global thy))
4.47 (#2 (References.select_input ospec spec)))
4.48 (imodel2fstr imodel), meth)
4.49 val pt = Ctree.update_spec pt p spec;
4.50 in if pos_ = Pos.Pbl
4.51 then
4.52 let
4.53 - val {where_rls, where_,...} = Problem.from_store ctxt
4.54 + val {where_rls, where_,...} = Problem.from_store (Proof_Context.init_global thy)
4.55 (#2 (References.select_input ospec spec))
4.56 - val (_, where_) = Pre_Conds.check ctxt where_rls where_ pits 0
4.57 + val (_, where_) = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ pits 0
4.58 in (Ctree.update_pbl pt p pits,
4.59 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec))
4.60 end
4.61 else
4.62 let
4.63 - val {where_rls,where_,...} = MethodC.from_store ctxt
4.64 + val {where_rls,where_,...} = MethodC.from_store (Proof_Context.init_global thy)
4.65 (#3 (References.select_input ospec spec))
4.66 - val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
4.67 + val (_, where_) = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ mits 0
4.68 in (Ctree.update_met pt p mits,
4.69 (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
4.70 end
5.1 --- a/src/Tools/isac/Specify/refine.sml Wed Jan 25 17:51:52 2023 +0100
5.2 +++ b/src/Tools/isac/Specify/refine.sml Wed Jan 25 18:35:02 2023 +0100
5.3 @@ -221,44 +221,6 @@
5.4
5.5 \<^isac_test>\<open>
5.6 (* refine a problem; version providing output for math-experts *)
5.7 -(*
5.8 -fun refin' pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
5.9 - let
5.10 - val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
5.11 - val {thy, model, where_, where_rls, ...} = py
5.12 - val oris = O_Model.init thy fmz model(* |> #1*);
5.13 - (* WN020803: itms!: oris might _not_ be complete here *)
5.14 - val (b, (itms, where_')) = M_Match.match_oris' thy oris (model, where_, where_rls)
5.15 - in
5.16 - if b
5.17 - then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
5.18 - else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
5.19 - end
5.20 - | refin' pblRD fmz pbls (Store.Node (pI, [py], pys)) =
5.21 - let
5.22 - val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
5.23 - val {thy, model, where_, where_rls, ...} = py
5.24 - val oris = O_Model.init thy fmz model(* |> #1*);
5.25 - (* WN020803: itms!: oris might _not_ be complete here *)
5.26 - val(b, (itms, where_')) = M_Match.match_oris' thy oris (model,where_,where_rls);
5.27 - in
5.28 - if b
5.29 - then
5.30 - let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')
5.31 - in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
5.32 - else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')])
5.33 - end
5.34 - | refin' _ _ _ _ = raise ERROR "refin': uncovered fun def."
5.35 -and refins' _ _ pbls [] = pbls
5.36 - | refins' pblRD fmz pbls ((p as Store.Node _) :: pts) =
5.37 - let
5.38 - val pbls' = refin' pblRD fmz pbls p
5.39 - in
5.40 - case last_elem pbls' of
5.41 - M_Match.Matches _ => pbls'
5.42 - | M_Match.NoMatch _ => refins' pblRD fmz pbls' pts
5.43 - end;
5.44 -*)
5.45 (*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list ->
5.46 Probl_Def.T Store.node -> M_Match.T list*)
5.47 fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
5.48 @@ -267,10 +229,10 @@
5.49 val {thy, model, where_, where_rls, ...} = py
5.50 val model = map (Model_Pattern.adapt_to_type ctxt) model
5.51 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
5.52 - val oris = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
5.53 + val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
5.54 val (b, (itms, where_')) =
5.55 M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
5.56 - in
5.57 + in
5.58 if b
5.59 then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
5.60 else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
5.61 @@ -281,7 +243,7 @@
5.62 val {thy, model, where_, where_rls, ...} = py
5.63 val model = map (Model_Pattern.adapt_to_type ctxt) model
5.64 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
5.65 - val oris = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
5.66 + val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
5.67 val (b, (itms, where_')) =
5.68 M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
5.69 in
6.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Jan 25 17:51:52 2023 +0100
6.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Jan 25 18:35:02 2023 +0100
6.3 @@ -223,14 +223,14 @@
6.4 if mI = ["no_met"]
6.5 then
6.6 let
6.7 - val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
6.8 + val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
6.9 val pI' = Refine.refine_ori' pctxt pors pI;
6.10 in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
6.11 (hd o #solve_mets o Problem.from_store ctxt) pI')
6.12 end
6.13 else
6.14 let
6.15 - val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
6.16 + val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
6.17 in (pI, (pors, pctxt), mI) end;
6.18 val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
6.19 val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy'))
7.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Jan 25 17:51:52 2023 +0100
7.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Jan 25 18:35:02 2023 +0100
7.3 @@ -124,7 +124,7 @@
7.4 val thy = ThyC.get_theory dI
7.5 val ctxt = Proof_Context.init_global thy;
7.6 (*if*) mI = ["no_met"](*else*);
7.7 - val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
7.8 + val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
7.9 val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*)
7.10 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
7.11 val dI = Context.theory_name (ThyC.parent_of thy thy');
8.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Jan 25 17:51:52 2023 +0100
8.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Jan 25 18:35:02 2023 +0100
8.3 @@ -42,7 +42,7 @@
8.4 (*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
8.5 (*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
8.6 (*old*) in (pI, (pors, pctxt), mI) end;
8.7 -( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
8.8 +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
8.9 in (pI, (pors, pctxt), mI) end;
8.10
8.11 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
9.1 --- a/test/Tools/isac/Specify/m-match.sml Wed Jan 25 17:51:52 2023 +0100
9.2 +++ b/test/Tools/isac/Specify/m-match.sml Wed Jan 25 18:35:02 2023 +0100
9.3 @@ -43,7 +43,7 @@
9.4 "solveFor x", "errorBound (eps=0)", "solutions L"];
9.5 val pbt as {model = model,...} =
9.6 Problem.from_store @{context} ["univariate", "equation"];
9.7 -val o_model = O_Model.init @{theory} fmz model
9.8 +val (o_model, ctxt) = O_Model.init @{theory} fmz model
9.9 val py = Problem.from_store @{context} ["equation"];
9.10 val py = Problem.from_store @{context} ["univariate", "equation"];
9.11 val py = Problem.from_store @{context} ["sq", "rootX", "univariate", "equation"];
10.1 --- a/test/Tools/isac/Specify/o-model.sml Wed Jan 25 17:51:52 2023 +0100
10.2 +++ b/test/Tools/isac/Specify/o-model.sml Wed Jan 25 18:35:02 2023 +0100
10.3 @@ -41,11 +41,11 @@
10.4 "~~~~~ fun initialise , args:"; val (thy, (fmz, (_, pI, mI))) = (thy, (model, refs));
10.5 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *);
10.6 (*if*) mI = ["no_met"] (*else*);
10.7 - val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
10.8 + val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
10.9 (*+*)Problem.from_store ctxt pI: Problem.T;
10.10 (*+*)(Problem.from_store ctxt pI |> #model): Model_Pattern.T;
10.11
10.12 -(*+*)val o_model = (Problem.from_store ctxt pI |> #model |>
10.13 +(*+*)val (o_model, ctxt) = (Problem.from_store ctxt pI |> #model |>
10.14 O_Model.init thy fmz);
10.15 "~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store ctxt pI |> #model);
10.16 val ori = (map (fn str => str
10.17 @@ -178,7 +178,7 @@
10.18 "errorBound (eps=(0::real))"]
10.19 val pbt as {model = model,...} =
10.20 Problem.from_store @{context} ["maximum_of", "function"];
10.21 -val o_model = O_Model.init @{theory} formalise model;
10.22 +val (o_model, ctxt) = O_Model.init @{theory} formalise model;
10.23
10.24 case o_model of
10.25 [