1.1 --- a/TODO.md Mon Sep 26 10:57:53 2022 +0200
1.2 +++ b/TODO.md Thu Sep 29 18:02:10 2022 +0200
1.3 @@ -62,9 +62,7 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 -* WN: follow up 3: MethodC.adapt_to_typ on loading by CalcTree, CalcTreeTEST
1.8 - follow up 4: CAS_Cmd.adapt_to_typ on loading by CalcTree, CalcTreeTEST
1.9 - follow up 5: cleanup
1.10 +* WN: follow up 5: cleanup
1.11 follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context}
1.12 Thus eliminate use of Thy_Info.get_theory
1.13 follow up 7: ANSWER ?How represent items, which have not yet been input? IN VSCode_Example.thy WITH "__"
2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Sep 26 10:57:53 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Thu Sep 29 18:02:10 2022 +0200
2.3 @@ -27,16 +27,16 @@
2.4 ML_file unparseC.sml
2.5 ML_file "rule-def.sml"
2.6 ML_file "thmC-def.sml"
2.7 -ML_file "eval-def.sml" (*rename identifiers by use of struct.id*)
2.8 +ML_file "eval-def.sml"
2.9 ML_file "rewrite-order.sml"
2.10 ML_file rule.sml
2.11 +ML_file "model-pattern.sml"
2.12 ML_file "error-pattern-def.sml"
2.13 ML_file "rule-set.sml"
2.14
2.15 ML_file "store.sml"
2.16 ML_file "check-unique.sml"
2.17 ML_file "references-def.sml"
2.18 -ML_file "model-pattern.sml"
2.19 ML_file "problem-def.sml"
2.20 ML_file "method-def.sml"
2.21 ML_file "cas-def.sml"
3.1 --- a/src/Tools/isac/BaseDefinitions/error-pattern-def.sml Mon Sep 26 10:57:53 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/error-pattern-def.sml Thu Sep 29 18:02:10 2022 +0200
3.3 @@ -10,6 +10,7 @@
3.4 eqtype id
3.5 type T = id * term list * thm list
3.6 val s_to_string : T list -> string
3.7 + val adapt_to_type: Proof.context -> T -> T
3.8
3.9 type fill_in_id
3.10 type fill_in
3.11 @@ -32,6 +33,9 @@
3.12 "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms
3.13 fun s_to_string errpats = (strs2str' o (map errpat2str)) errpats
3.14
3.15 +fun adapt_to_type ctxt (id, terms, thms) =
3.16 + (id, map (Model_Pattern.adapt_term_to_type ctxt) terms, thms)
3.17 +
3.18 (* for (at least) 2 kinds of access:
3.19 (1) given an id, find the respective fill_in's (e.g. in fun find_fill_patterns)
3.20 (2) given a thm, find respective fill_in's *)
4.1 --- a/src/Tools/isac/BaseDefinitions/references-def.sml Mon Sep 26 10:57:53 2022 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/references-def.sml Thu Sep 29 18:02:10 2022 +0200
4.3 @@ -15,7 +15,7 @@
4.4
4.5 type T
4.6 val empty: T
4.7 - val to_string: string * string list * string list -> string
4.8 + val to_string: string * (*Problem.*)id * (*MethodC.*)id -> string
4.9
4.10 val select_input : T -> T -> T
4.11 end
5.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Mon Sep 26 10:57:53 2022 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Thu Sep 29 18:02:10 2022 +0200
5.3 @@ -8,6 +8,8 @@
5.4 sig
5.5 eqtype id
5.6 val cut_id: string -> id
5.7 + val id_of: theory -> id
5.8 + val curried_equal: theory -> theory -> bool
5.9
5.10 val last_isabelle_thy: theory
5.11 val session_specify_names: id list
5.12 @@ -32,6 +34,8 @@
5.13 type id = string;
5.14 val id_empty = "empty_thy_id";
5.15 fun cut_id dn = hd (space_explode "." dn);
5.16 +fun id_of thy = thy |> Context.theory_id |> Context.theory_id_name
5.17 +fun curried_equal thy1 thy2 = id_of thy1 = id_of thy2
5.18
5.19 val last_isabelle_thy = @{theory Complex_Main}
5.20 val session_specify_names = ["Specify", "MathEngBasic", "Input_Descript",
6.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Sep 26 10:57:53 2022 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Sep 29 18:02:10 2022 +0200
6.3 @@ -75,10 +75,11 @@
6.4 fun IteratorTEST cI = States.add_user cI;
6.5
6.6 (* create a calc-tree; compare "fun CalcTreeTEST" *)
6.7 -fun CalcTree [(fmz, sp)] (*for several variants lateron*) =
6.8 +fun CalcTree [(model, refs as (thy_id, _, _))] (*for several variants lateron*) =
6.9 (case \<^try>\<open>
6.10 let
6.11 - val cs = Step_Specify.nxt_specify_init_calc (fmz, sp)
6.12 + val ctxt = thy_id |> ThyC.get_theory |> Proof_Context.init_global; (*will become an argument*)
6.13 + val cs = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
6.14 val cI = States.add_calc cs (*FIXME.WN.8.03: error-handling missing*)
6.15 in calctreeOK2xml cI end
6.16 \<close> of
7.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Mon Sep 26 10:57:53 2022 +0200
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Thu Sep 29 18:02:10 2022 +0200
7.3 @@ -14,7 +14,7 @@
7.4 type xml
7.5 val pbl_hierarchy2file : filepath -> filepath * string
7.6 val met_hierarchy2file : filepath -> filepath * string
7.7 - val update_metpair: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id
7.8 + val update_metpair_PIDE: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id
7.9 end
7.10
7.11 (**)
7.12 @@ -100,8 +100,8 @@
7.13 ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: MethodC.T
7.14
7.15 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
7.16 -fun update_metpair thy metID errpats = let
7.17 - val ret = (update_metdata (MethodC.from_store' thy metID) errpats, metID)
7.18 +fun update_metpair_PIDE thy metID errpats = let
7.19 + val ret = (update_metdata (MethodC.from_store'_PIDE thy metID) errpats, metID)
7.20 handle ERROR _ => raise ERROR ("update_metpair: " ^ (strs2str metID) ^ " must address a method");
7.21 in ret end;
7.22
8.1 --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml Mon Sep 26 10:57:53 2022 +0200
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml Thu Sep 29 18:02:10 2022 +0200
8.3 @@ -76,7 +76,7 @@
8.4 EXCEPT theory hierarchy ... compare 'fun keref2xml' *)
8.5 fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store_PIDE ctxt)) pblID)
8.6 handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
8.7 -fun metID2guh metID = (((#guh o MethodC.from_store) metID)
8.8 +fun metID2guh metID = (((#guh o MethodC.from_store_PIDE ("Isac_Knowledge" |> ThyC.get_theory |> Proof_Context.init_global)) metID)
8.9 handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
8.10 fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID
8.11 | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID
9.1 --- a/src/Tools/isac/Build_Isac.thy Mon Sep 26 10:57:53 2022 +0200
9.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Sep 29 18:02:10 2022 +0200
9.3 @@ -2871,7 +2871,7 @@
9.4 ML \<open>Eval.adhoc_thm; (*from "ProgLang/evaluate.sml" *)\<close>
9.5 ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
9.6 ML \<open>Input_Descript.for_real_list; (*from "Input_Descript.thy" *)\<close>
9.7 -ML \<open>Test_Code.me;\<close>
9.8 +ML \<open>(*Test_Code.me;*)\<close>
9.9 text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
9.10 ML \<open>prog_expr\<close>
9.11
10.1 --- a/src/Tools/isac/Interpret/derive.sml Mon Sep 26 10:57:53 2022 +0200
10.2 +++ b/src/Tools/isac/Interpret/derive.sml Thu Sep 29 18:02:10 2022 +0200
10.3 @@ -151,7 +151,7 @@
10.4 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
10.5 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
10.6 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
10.7 - val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
10.8 + val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
10.9 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
10.10 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
10.11 val pt = Ctree.update_branch pt p Ctree.TransitiveB
10.12 @@ -169,7 +169,7 @@
10.13 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
10.14 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
10.15 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
10.16 - val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
10.17 + val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
10.18 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
10.19 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
10.20 val pt = Ctree.update_branch pt p Ctree.TransitiveB
11.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Mon Sep 26 10:57:53 2022 +0200
11.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Thu Sep 29 18:02:10 2022 +0200
11.3 @@ -119,8 +119,9 @@
11.4 fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =
11.5 let
11.6 val f_curr = Ctree.get_curr_formula (pt, pos);
11.7 - val pp = Ctree.par_pblobj pt p
11.8 - val (errpats, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
11.9 + val (_, _, _, ctxt) = LItool.parent_node_PIDE pt pos (*--------------- double code*)
11.10 + val pp = Ctree.par_pblobj pt p (*by ^^^^^^^ replace with extension --- double code*)
11.11 + val (errpats, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
11.12 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
11.13 | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
11.14 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
11.15 @@ -178,4 +179,4 @@
11.16 | Rule_Set.Empty => []
11.17 end
11.18
11.19 -(**)end(**)
11.20 \ No newline at end of file
11.21 +(**)end(**)
12.1 --- a/src/Tools/isac/Interpret/li-tool.sml Mon Sep 26 10:57:53 2022 +0200
12.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Thu Sep 29 18:02:10 2022 +0200
12.3 @@ -13,10 +13,10 @@
12.4 | Not_Associated;
12.5 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
12.6
12.7 - val parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T
12.8 + val parent_node_PIDE: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T * Proof.context
12.9 val init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> MethodC.id ->
12.10 Istate.T * Proof.context * Program.T
12.11 - val resume_prog: ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree ->
12.12 + val resume_prog_PIDE: Pos.pos' -> Ctree.ctree ->
12.13 (Istate.T * Proof.context) * Program.T
12.14
12.15 val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
12.16 @@ -27,7 +27,7 @@
12.17 val tac_from_prog: Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
12.18
12.19 \<^isac_test>\<open>
12.20 - val arguments_from_model : MethodC.id -> I_Model.T -> term list
12.21 + val arguments_from_model : Proof.context -> MethodC.id -> I_Model.T -> term list
12.22 \<close>
12.23 end
12.24
12.25 @@ -51,7 +51,7 @@
12.26 fun error_msg_2 d itms = ("arguments_from_model: '" ^ UnparseC.term d ^ "' not in itms:\n" ^
12.27 "itms:\n" ^ I_Model.to_string @{context} itms)
12.28 (* turn Model-items into arguments for a program *)
12.29 -fun arguments_from_model mI itms =
12.30 +fun arguments_from_model ctxt mI itms =
12.31 let
12.32 val mvat = I_Model.max_variant itms
12.33 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
12.34 @@ -61,7 +61,7 @@
12.35 case find_first (test_dsc d) itms of
12.36 NONE => raise ERROR (error_msg_2 d itms)
12.37 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
12.38 - val pats = (#ppc o MethodC.from_store) mI
12.39 + val pats = (#ppc o MethodC.from_store_PIDE ctxt) mI
12.40 val _ = if pats = [] then raise ERROR error_msg_1 else ()
12.41 in (flat o (map (itm2arg itms))) pats end;
12.42
12.43 @@ -203,21 +203,21 @@
12.44 | associate _ ctxt (tac, _) =
12.45 (trace_msg_3 ctxt tac; Not_Associated);
12.46
12.47 -(* find the next parent, which is either a PblObj or a PrfObj *)
12.48 -fun parent_node _ ([], _) = (true, [], Rule_Set.Empty)
12.49 - | parent_node pt (pos as (p, _)) =
12.50 +(* find the next parent, which is either a PblObj xor a PrfObj in case of detail step*)
12.51 +fun parent_node_PIDE _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
12.52 + | parent_node_PIDE pt (pos as (p, _)) =
12.53 let
12.54 - fun par _ [] = (true, [], Rule_Set.Empty)
12.55 + fun par _ [] = (true, [], Rule_Set.Empty, ContextC.empty)
12.56 | par pt p =
12.57 if Ctree.is_pblobj (Ctree.get_obj I pt p)
12.58 - then (true, p, Rule_Set.Empty)
12.59 + then (true, p, Rule_Set.Empty, ContextC.empty)
12.60 else
12.61 let
12.62 val ctxt = Ctree.get_ctxt pt pos
12.63 in
12.64 case Ctree.get_obj Ctree.g_tac pt p of
12.65 - Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
12.66 - | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
12.67 + Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls', ctxt)
12.68 + | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls', ctxt)
12.69 | _ => par pt (Pos.lev_up p)
12.70 end
12.71 in par pt (Pos.lev_up p) end;
12.72 @@ -269,11 +269,11 @@
12.73 then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
12.74 else ();
12.75 in
12.76 -fun init_pstate srls ctxt itms metID =
12.77 +fun init_pstate (srls: Rule_Def.rule_set) (ctxt: Proof.context) (itms) (metID) =
12.78 let
12.79 - val actuals = arguments_from_model metID itms
12.80 + val actuals = arguments_from_model ctxt metID itms
12.81 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
12.82 - val (scr, sc) = (case (#scr o MethodC.from_store) metID of
12.83 + val (scr, sc) = (case (#scr o MethodC.from_store_PIDE ctxt) metID of
12.84 scr as Rule.Prog sc => (trace_init ctxt metID; (scr, sc))
12.85 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string metID))
12.86 val formals = Program.formal_args sc
12.87 @@ -290,7 +290,7 @@
12.88 else
12.89 let val (f, a) = assoc_by_type f aas
12.90 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
12.91 - val {pre, prls, ...} = MethodC.from_store metID;
12.92 + val {pre, prls, ...} = MethodC.from_store_PIDE ctxt metID;
12.93 val pres = Pre_Conds.check prls pre itms 0 |> snd |> map snd;
12.94 val ctxt = ctxt |> ContextC.insert_assumptions pres;
12.95 val ist = Istate.e_pstate
12.96 @@ -302,35 +302,35 @@
12.97 end (*local*)
12.98
12.99 (* get the simplifier of the current method *)
12.100 -fun get_simplifier (pt, (p, _)) =
12.101 +fun get_simplifier (pt, pos as (p, _)) =
12.102 let
12.103 val p' = Ctree.par_pblobj pt p
12.104 val metID = Ctree.get_obj Ctree.g_metID pt p'
12.105 - val {srls, ...} = MethodC.from_store metID
12.106 + val ctxt = Ctree.get_ctxt pt pos
12.107 + val {srls, ...} = MethodC.from_store_PIDE ctxt metID
12.108 in srls end
12.109
12.110 (* resume program interpretation at the beginning of a step *)
12.111 -fun resume_prog thy (pos as (p, p_)) pt =
12.112 +fun resume_prog_PIDE pos pt =
12.113 let
12.114 - val (is_problem, p', rls') = parent_node pt pos
12.115 + val (is_problem, p', rls', ctxt) = parent_node_PIDE pt pos (*is Ctree.PrfObj in case of detail step*)
12.116 in
12.117 if is_problem then
12.118 let
12.119 val metID = get_obj g_metID pt p'
12.120 - val {srls, ...} = MethodC.from_store metID
12.121 + val {srls, ...} = MethodC.from_store_PIDE ctxt metID
12.122 val (is, ctxt) =
12.123 - case get_loc pt (p, p_) of
12.124 + case get_loc pt pos of
12.125 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
12.126 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
12.127 in
12.128 - ((is, ctxt), (#scr o MethodC.from_store) metID)
12.129 + ((is, ctxt), (#scr o MethodC.from_store_PIDE ctxt) metID)
12.130 end
12.131 else
12.132 - (get_loc pt (p, p_),
12.133 - Rule.Prog (Auto_Prog.gen (ThyC.get_theory thy) (get_last_formula (pt, (p, p_))) rls'))
12.134 + (get_loc pt pos,
12.135 + Rule.Prog (Auto_Prog.gen (Proof_Context.theory_of ctxt) (get_last_formula (pt, pos)) rls'))
12.136 end
12.137
12.138 -
12.139 fun trace_msg_1 ctxt call t stac =
12.140 if Config.get ctxt LI_trace then
12.141 tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term t ^ "\" \<longrightarrow> Tac \"" ^ UnparseC.term stac ^ "\"")
13.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Sep 26 10:57:53 2022 +0200
13.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Sep 29 18:02:10 2022 +0200
13.3 @@ -271,8 +271,8 @@
13.4 Accept_Tac (tac, ist, ctxt) =>
13.5 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
13.6 | Term_Val prog_result =>
13.7 - (case LItool.parent_node pt pos of
13.8 - (true, p', _) =>
13.9 + (case LItool.parent_node_PIDE pt pos of
13.10 + (true, p', _, _) =>
13.11 let
13.12 val (_, pblID, _) = get_obj g_spec pt p';
13.13 in
13.14 @@ -498,10 +498,10 @@
13.15
13.16 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
13.17 let
13.18 - val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
13.19 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
13.20 + val (itms, oris, probl, ctxt) = case get_obj I pt p of
13.21 + PblObj {meth = itms, origin = (oris, _, _), probl, ctxt, ...} => (itms, oris, probl, ctxt)
13.22 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
13.23 - val {ppc, ...} = MethodC.from_store mI;
13.24 + val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
13.25 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
13.26 val srls = LItool.get_simplifier (pt, pos)
13.27 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
13.28 @@ -547,7 +547,8 @@
13.29 | by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) =
13.30 let
13.31 val parent_pos = par_pblobj pt p
13.32 - val {scr, ...} = MethodC.from_store (get_obj g_metID pt parent_pos);
13.33 + val ctxt = Ctree.get_ctxt pt pos
13.34 + val {scr, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt parent_pos);
13.35 val prog_res =
13.36 case find_next_step scr (pt, pos) sub_ist sub_ctxt of
13.37 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
13.38 @@ -590,7 +591,7 @@
13.39 else
13.40 let
13.41 val thy' = get_obj g_domID pt (par_pblobj pt p);
13.42 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
13.43 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
13.44 in
13.45 case find_next_step sc (pt, pos) ist ctxt of
13.46 Next_Step (ist, ctxt, tac) =>
13.47 @@ -615,7 +616,8 @@
13.48 fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo =
13.49 let
13.50 val fo = Calc.current_formula ptp
13.51 - val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
13.52 + val ctxt = Ctree.get_ctxt pt pos
13.53 + val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
13.54 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
13.55 val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)
13.56 in
14.1 --- a/src/Tools/isac/Interpret/solve-step.sml Mon Sep 26 10:57:53 2022 +0200
14.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Thu Sep 29 18:02:10 2022 +0200
14.3 @@ -43,13 +43,13 @@
14.4
14.5 fun get_ruleset _ (pos as (p, _)) pt =
14.6 let
14.7 - val (pbl, p', rls') = LItool.parent_node pt pos
14.8 + val (pbl, p', rls', ctxt) = LItool.parent_node_PIDE pt pos
14.9 in
14.10 if pbl
14.11 then
14.12 let
14.13 val thy' = Ctree.get_obj Ctree.g_domID pt p'
14.14 - val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p')
14.15 + val {rew_ord', erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt p')
14.16 in ("OK", thy', rew_ord', erls, false) end
14.17 else
14.18 let
14.19 @@ -60,13 +60,13 @@
14.20
14.21 fun get_eval scrop (pos as (p, _)) pt =
14.22 let
14.23 - val (pbl, p', rls') = LItool.parent_node pt pos
14.24 + val (pbl, p', rls', ctxt) = LItool.parent_node_PIDE pt pos
14.25 in
14.26 if pbl
14.27 then
14.28 let
14.29 val thy' = Ctree.get_obj Ctree.g_domID pt p'
14.30 - val {calc = scr_isa_fns, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p')
14.31 + val {calc = scr_isa_fns, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt p')
14.32 val opt = assoc (scr_isa_fns, scrop)
14.33 in
14.34 case opt of
14.35 @@ -152,7 +152,7 @@
14.36 val pp = Ctree.par_pblobj pt p;
14.37 val ctxt = Ctree.get_loc pt pos |> snd
14.38 val thy = Proof_Context.theory_of ctxt
14.39 - val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp);
14.40 + val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp);
14.41 val f = Calc.current_formula cs;
14.42 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
14.43 in
14.44 @@ -195,7 +195,7 @@
14.45 val ctxt = Ctree.get_loc pt pos |> snd
14.46 val thy = Proof_Context.theory_of ctxt
14.47 val f = Calc.current_formula cs;
14.48 - val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
14.49 + val {rew_ord', erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp)
14.50 val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*)
14.51 val ro = get_rew_ord ctxt rew_ord'
14.52 in
15.1 --- a/src/Tools/isac/Interpret/step-solve.sml Mon Sep 26 10:57:53 2022 +0200
15.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Thu Sep 29 18:02:10 2022 +0200
15.3 @@ -46,8 +46,7 @@
15.4 end
15.5 else
15.6 let
15.7 - val thy' = get_obj g_domID pt (par_pblobj pt p);
15.8 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
15.9 + val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
15.10 in
15.11 case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
15.12 LI.Safe_Step (istate, ctxt, tac) =>
15.13 @@ -107,8 +106,9 @@
15.14 ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
15.15 | LI.Not_Derivable =>
15.16 let
15.17 - val pp = Ctree.par_pblobj pt p
15.18 - val (errpats, nrls, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
15.19 + val (_, _, _, ctxt) = LItool.parent_node_PIDE pt pos (*--------------- double code*)
15.20 + val pp = Ctree.par_pblobj pt p (*by ^^^^^^^ replace with extension --- double code*)
15.21 + val (errpats, nrls, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
15.22 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
15.23 | _ => raise ERROR "inform: uncovered case of get_met"
15.24 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
16.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Mon Sep 26 10:57:53 2022 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Sep 29 18:02:10 2022 +0200
16.3 @@ -137,7 +137,7 @@
16.4 subsubsection \<open>Error patterns for differentiation\<close>
16.5
16.6 setup \<open>KEStore_Elems.add_mets @{context}
16.7 - [Pbl_Met_Hierarchy.update_metpair @{theory Diff} ["diff", "differentiate_on_R"]
16.8 + [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Diff} ["diff", "differentiate_on_R"]
16.9 [("chain-rule-diff-both",
16.10 [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
16.11 TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
16.12 @@ -167,7 +167,7 @@
16.13 subsubsection \<open>Error patterns for calculation with rationals\<close>
16.14
16.15 setup \<open>KEStore_Elems.add_mets @{context}
16.16 - [Pbl_Met_Hierarchy.update_metpair @{theory Rational} ["simplification", "of_rationals"]
16.17 + [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Rational} ["simplification", "of_rationals"]
16.18 [("addition-of-fractions",
16.19 [TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
16.20 TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
17.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Mon Sep 26 10:57:53 2022 +0200
17.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Sep 29 18:02:10 2022 +0200
17.3 @@ -146,7 +146,6 @@
17.4 Find: "solutions v_v'i'"
17.5
17.6 ML \<open>
17.7 - MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];
17.8 \<close> ML \<open>
17.9 \<close> ML \<open>
17.10 \<close>
18.1 --- a/src/Tools/isac/MathEngBasic/method.sml Mon Sep 26 10:57:53 2022 +0200
18.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Thu Sep 29 18:02:10 2022 +0200
18.3 @@ -20,14 +20,14 @@
18.4
18.5 type input
18.6 (* TODO: ------------- remove always empty --- vvvvvvvvvvv -- vvv*)
18.7 - val prep_input : theory -> Check_Unique.id -> string list -> id ->
18.8 + val prep_input_PIDE: theory -> Check_Unique.id -> string list -> id ->
18.9 id * Problem.model_input * input * thm -> T * id
18.10
18.11 val set_data: input -> theory -> theory
18.12 val the_data: theory -> input
18.13
18.14 - val from_store: id -> T
18.15 - val from_store': theory -> id -> T
18.16 + val from_store'_PIDE: theory -> id -> T
18.17 + val from_store_PIDE: Proof.context -> id -> T
18.18 end
18.19
18.20 (**)
18.21 @@ -50,7 +50,7 @@
18.22 {calc: Rule_Def.eval_ml_from_prog list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
18.23 prls: Rule_Set.T, rew_ord': Rewrite_Ord.id, rls': Rule_Set.T, srls: Rule_Set.T}
18.24
18.25 -fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
18.26 +fun prep_input_PIDE thy guh (mathauthors: string list) (init: References_Def.id)
18.27 (metID, ppc,
18.28 {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
18.29 errpats = ep, nrls = nr}, scr) =
18.30 @@ -60,9 +60,9 @@
18.31 val gi = (case gi of
18.32 [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
18.33 | ((_, gi') :: []) =>
18.34 - (case \<^try>\<open> map (Problem.split_did_PIDE o (TermC.parseNEW'' thy)) gi'\<close> of
18.35 + (*(case \<^try>\<open> *)map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) gi'(*\<close> of
18.36 SOME x => x
18.37 - | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
18.38 + | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))*)
18.39 | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
18.40 val gi = map (pair "#Given") gi;
18.41
18.42 @@ -70,9 +70,9 @@
18.43 val fi = (case fi of
18.44 [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
18.45 | ((_, fi') :: []) =>
18.46 - (case \<^try>\<open> map (Problem.split_did_PIDE o (TermC.parseNEW'' thy)) fi'\<close> of
18.47 + (*(case \<^try>\<open> *)map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) fi'(*\<close> of
18.48 SOME x => x
18.49 - | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
18.50 + | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))*)
18.51 | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
18.52 val fi = map (pair "#Find") fi;
18.53
18.54 @@ -80,9 +80,9 @@
18.55 val re = (case re of
18.56 [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
18.57 | ((_,re') :: []) =>
18.58 - (case \<^try>\<open> map (Problem.split_did_PIDE o (TermC.parseNEW'' thy)) re'\<close> of
18.59 + (*(case \<^try>\<open> *) map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) re'(*\<close> of
18.60 SOME x => x
18.61 - | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
18.62 + | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))*)
18.63 | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
18.64 val re = map (pair "#Relate") re;
18.65
18.66 @@ -90,9 +90,9 @@
18.67 val wh = (case wh of
18.68 [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
18.69 | ((_, wh') :: []) =>
18.70 - (case \<^try>\<open> map (TermC.parse_patt thy) wh'\<close> of
18.71 + (*(case \<^try>\<open> *)map (TermC.parse_patt_PIDE thy) wh'(*\<close> of
18.72 SOME x => x
18.73 - | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
18.74 + | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))*)
18.75 | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
18.76 val sc = Program.prep_program scr
18.77 val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
18.78 @@ -141,22 +141,36 @@
18.79 (case program of
18.80 NONE => @{thm refl}
18.81 | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
18.82 - val arg = prep_input thy name maa id_empty (metID, model_input, input, thm);
18.83 + val arg = prep_input_PIDE thy name maa id_empty (metID, model_input, input, thm);
18.84 in KEStore_Elems.add_mets @{context} [arg] thy end)))
18.85
18.86 in end;
18.87
18.88 (** get MethodC from Store **)
18.89
18.90 +fun adapt_to_type ctxt {guh, mathauthors, init, rew_ord', erls, srls, crls, nrls, errpats, calc,
18.91 + scr, prls, ppc, pre} =
18.92 + let
18.93 + val where_ = map (Model_Pattern.adapt_term_to_type ctxt) pre
18.94 + val model = map (Model_Pattern.adapt_to_type ctxt) ppc
18.95 + val errpats = map (Error_Pattern_Def.adapt_to_type ctxt) errpats
18.96 + in
18.97 + {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls,
18.98 + srls = srls, crls = crls, nrls = nrls, errpats = errpats, calc = calc, scr = scr, prls = prls,
18.99 + ppc = model, pre = where_}
18.100 + end
18.101 +
18.102 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
18.103 -fun from_store id =
18.104 - (Store.get (get_mets ()) id id)
18.105 - handle ERROR _ =>
18.106 - raise error ("*** ERROR MethodC.from_store " ^ strs2str id ^ " not found");
18.107 -
18.108 -fun from_store' thy id =
18.109 +fun from_store'_PIDE thy id =
18.110 (Store.get (KEStore_Elems.get_mets thy) id id)
18.111 handle ERROR _ =>
18.112 raise error ("*** ERROR MethodC.from_store thy " ^ strs2str id ^ " not found");
18.113
18.114 +fun from_store_PIDE ctxt id =
18.115 + let
18.116 + val pbl = Store.get (get_mets ()) id (rev id)
18.117 + in adapt_to_type ctxt pbl end
18.118 + handle ERROR _ =>
18.119 + raise error ("*** ERROR MethodC.from_store thy " ^ strs2str id ^ " not found");
18.120 +
18.121 (**)end(**)
19.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Mon Sep 26 10:57:53 2022 +0200
19.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Thu Sep 29 18:02:10 2022 +0200
19.3 @@ -29,9 +29,10 @@
19.4 val pp = par_pblobj pt p;
19.5 val thy' = get_obj g_domID pt pp;
19.6 val thy = ThyC.get_theory thy';
19.7 + val ctxt = Ctree.get_ctxt pt pos
19.8 val metID = get_obj g_metID pt pp;
19.9 val metID' = if metID = MethodC.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
19.10 - val (sc, srls) = (case MethodC.from_store metID' of
19.11 + val (sc, srls) = (case MethodC.from_store_PIDE ctxt metID' of
19.12 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1")
19.13 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
19.14 val ctxt = get_ctxt pt (p, p_)
19.15 @@ -57,7 +58,7 @@
19.16 if metID = MethodC.id_empty
19.17 then (get_obj g_origin pt pp) |> #2 |> #3
19.18 else metID
19.19 - val (sc, srls, erls, ro) = (case MethodC.from_store metID' of
19.20 + val (sc, srls, erls, ro) = (case MethodC.from_store_PIDE ctxt metID' of
19.21 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
19.22 | _ => raise ERROR "specific_from_prog 1")
19.23 val (env, (a, v)) = (case get_istate_LI pt pos of
19.24 @@ -80,4 +81,4 @@
19.25 |> distinct Tactic.eq_tac
19.26 end;
19.27
19.28 -(**)end(**)
19.29 \ No newline at end of file
19.30 +(**)end(**)
20.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Sep 26 10:57:53 2022 +0200
20.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Sep 29 18:02:10 2022 +0200
20.3 @@ -129,7 +129,7 @@
20.4
20.5 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
20.6 if no pbl has been specified, take the init from origin.*)
20.7 -fun initcontext_pbl pt (pos as (p, _)) =
20.8 +fun initcontext_pbl pt (p, _) =
20.9 let
20.10 val (probl, os, pI, hdl, pI', ctxt) =
20.11 case Ctree.get_obj I pt p of
20.12 @@ -148,14 +148,15 @@
20.13
20.14 fun initcontext_met pt (p,_) =
20.15 let
20.16 - val (meth, os, mI, mI') =
20.17 + val (meth, os, mI, mI', ctxt) =
20.18 case Ctree.get_obj I pt p of
20.19 - Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
20.20 + Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ctxt, ...} =>
20.21 + (meth, os, mI, mI', ctxt)
20.22 | Ctree.PrfObj _ => raise ERROR "initcontext_met: uncovered case"
20.23 val metID = if mI' = MethodC.id_empty
20.24 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
20.25 else mI'
20.26 - val {ppc, pre, prls, scr, ...} = MethodC.from_store metID
20.27 + val {ppc, pre, prls, scr, ...} = MethodC.from_store_PIDE ctxt metID
20.28 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
20.29 in
20.30 (model_ok, metID, scr, pbl, pre)
20.31 @@ -177,11 +178,11 @@
20.32
20.33 fun context_met mI pt p =
20.34 let
20.35 - val (meth, os) =
20.36 + val (meth, os, ctxt) =
20.37 case Ctree.get_obj I pt p of
20.38 - Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
20.39 + Ctree.PblObj {meth, origin = (os, _, _), ctxt, ...} => (meth, os, ctxt)
20.40 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
20.41 - val {ppc,pre,prls,scr,...} = MethodC.from_store mI
20.42 + val {ppc,pre,prls,scr,...} = MethodC.from_store_PIDE ctxt mI
20.43 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
20.44 in
20.45 (model_ok, mI, scr, pbl, pre)
21.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Mon Sep 26 10:57:53 2022 +0200
21.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Thu Sep 29 18:02:10 2022 +0200
21.3 @@ -15,13 +15,13 @@
21.4 struct
21.5 (**)
21.6
21.7 -fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ...}) Pos.Met =
21.8 +fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ctxt, ...}) Pos.Met =
21.9 let
21.10 val (_, _, metID) = Ctree.get_somespec' spec spec'
21.11 val pre = if metID = MethodC.id_empty then []
21.12 else
21.13 let
21.14 - val {prls, pre= where_, ...} = MethodC.from_store metID
21.15 + val {prls, pre = where_, ...} = MethodC.from_store_PIDE ctxt metID
21.16 val (_, pre) = Pre_Conds.check prls where_ meth 0
21.17 in pre end
21.18 val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 pre))
22.1 --- a/src/Tools/isac/Specify/cas-command.sml Mon Sep 26 10:57:53 2022 +0200
22.2 +++ b/src/Tools/isac/Specify/cas-command.sml Thu Sep 29 18:02:10 2022 +0200
22.3 @@ -54,7 +54,7 @@
22.4 case Refine.problem thy pI pits of
22.5 SOME (pI,_) => (pI, (hd o #met o Problem.from_store_PIDE ctxt) pI)
22.6 | NONE => (pI, (hd o #met o Problem.from_store_PIDE ctxt) pI)
22.7 - val {ppc, pre, prls, ...} = MethodC.from_store mI
22.8 + val {ppc, pre, prls, ...} = MethodC.from_store_PIDE ctxt mI
22.9 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
22.10 val its = O_Model.add_enumerate its_
22.11 val mits = map flattup2 its
23.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Sep 26 10:57:53 2022 +0200
23.2 +++ b/src/Tools/isac/Specify/p-spec.sml Thu Sep 29 18:02:10 2022 +0200
23.3 @@ -242,26 +242,33 @@
23.4 in (Pos.Pbl, appl_adds dI' oris probl pbt
23.5 (map itms2fstr probl), meth) end
23.6 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
23.7 - then let val met = (#ppc o MethodC.from_store) mI
23.8 + then let val met = (#ppc o MethodC.from_store_PIDE ctxt) mI
23.9 val mits = I_Model.complete oris probl meth met
23.10 in if foldl and_ (true, map #3 mits)
23.11 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
23.12 end
23.13 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
23.14 - ((#ppc o Problem.from_store_PIDE ctxt) (#2 (References.select_input ospec spec)))
23.15 - (imodel2fstr imodel), meth)
23.16 + ((#ppc o Problem.from_store_PIDE ctxt)
23.17 + (#2 (References.select_input ospec spec)))
23.18 + (imodel2fstr imodel), meth)
23.19 val pt = Ctree.update_spec pt p spec;
23.20 in if pos_ = Pos.Pbl
23.21 - then let val {prls,where_,...} = Problem.from_store_PIDE ctxt (#2 (References.select_input ospec spec))
23.22 - val (_, pre) = Pre_Conds.check prls where_ pits 0
23.23 - in (Ctree.update_pbl pt p pits,
23.24 - (SpecificationC.is_complete' pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T)
23.25 - end
23.26 - else let val {prls,pre,...} = MethodC.from_store (#3 (References.select_input ospec spec))
23.27 - val (_, pre) = Pre_Conds.check prls pre mits 0
23.28 - in (Ctree.update_met pt p mits,
23.29 - (SpecificationC.is_complete' mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)
23.30 - end
23.31 + then
23.32 + let
23.33 + val {prls, where_,...} = Problem.from_store_PIDE ctxt
23.34 + (#2 (References.select_input ospec spec))
23.35 + val (_, pre) = Pre_Conds.check prls where_ pits 0
23.36 + in (Ctree.update_pbl pt p pits,
23.37 + (SpecificationC.is_complete' pits pre spec, Pos.Pbl, hdf', pits, pre, spec))
23.38 + end
23.39 + else
23.40 + let
23.41 + val {prls,pre,...} = MethodC.from_store_PIDE ctxt
23.42 + (#3 (References.select_input ospec spec))
23.43 + val (_, pre) = Pre_Conds.check prls pre mits 0
23.44 + in (Ctree.update_met pt p mits,
23.45 + (SpecificationC.is_complete' mits pre spec, Pos.Met, hdf', mits, pre, spec))
23.46 + end
23.47 end
23.48 end
23.49 | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."
24.1 --- a/src/Tools/isac/Specify/specification.sml Mon Sep 26 10:57:53 2022 +0200
24.2 +++ b/src/Tools/isac/Specify/specification.sml Thu Sep 29 18:02:10 2022 +0200
24.3 @@ -114,8 +114,8 @@
24.4 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
24.5 fun get (pt, pos as (p, Pos.Pbl)) =
24.6 let
24.7 - val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
24.8 - Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
24.9 + val (ospec, hdf', spec, probl, ctxt) = case Ctree.get_obj I pt p of
24.10 + Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} => (ospec, hdf', spec, probl, ctxt)
24.11 | _ => raise ERROR "get Pbl: uncovered case get_obj"
24.12 val {prls, where_, ...} =
24.13 Problem.from_store_PIDE (Ctree.get_ctxt pt pos) (#2 (References.select_input ospec spec))
24.14 @@ -125,10 +125,10 @@
24.15 end
24.16 | get (pt, (p, Pos.Met)) =
24.17 let
24.18 - val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
24.19 - Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
24.20 + val (ospec, hdf', spec, meth, ctxt) = case Ctree.get_obj I pt p of
24.21 + Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ctxt, ...} => (ospec, hdf', spec, meth, ctxt)
24.22 | _ => raise ERROR "get Met: uncovered case get_obj"
24.23 - val {prls, pre, ...} = MethodC.from_store (#3 (References.select_input ospec spec))
24.24 + val {prls, pre, ...} = MethodC.from_store_PIDE ctxt (#3 (References.select_input ospec spec))
24.25 val (_, pre) = Pre_Conds.check prls pre meth 0
24.26 in
24.27 (is_complete' meth pre spec, Pos.Met, hdf', meth, pre, spec)
24.28 @@ -148,4 +148,4 @@
24.29 val pt = Ctree.update_spec pt p References.empty
24.30 in (pt, (p, Pos.Pbl)) end
24.31
24.32 -(**)end(**)
24.33 \ No newline at end of file
24.34 +(**)end(**)
25.1 --- a/src/Tools/isac/Specify/specify-step.sml Mon Sep 26 10:57:53 2022 +0200
25.2 +++ b/src/Tools/isac/Specify/specify-step.sml Thu Sep 29 18:02:10 2022 +0200
25.3 @@ -22,8 +22,9 @@
25.4 let
25.5 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
25.6 ...} = Calc.specify_data (ctree, pos);
25.7 + val ctxt = Ctree.get_ctxt ctree pos
25.8 val (dI, _, _) = References.select_input o_refs refs;
25.9 - val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
25.10 + val {ppc = m_patt, pre, prls, ...} = MethodC.from_store_PIDE ctxt mID
25.11 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
25.12 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
25.13 val thy = ThyC.get_theory dI
26.1 --- a/src/Tools/isac/Specify/specify.sml Mon Sep 26 10:57:53 2022 +0200
26.2 +++ b/src/Tools/isac/Specify/specify.sml Thu Sep 29 18:02:10 2022 +0200
26.3 @@ -10,9 +10,9 @@
26.4 (Model_Def.m_field * TermC.as_string) option
26.5 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
26.6 \<^isac_test>\<open>
26.7 - val for_problem: O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
26.8 + val for_problem_PIDE: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
26.9 string * (Pos.pos_ * Tactic.input)
26.10 - val for_method: O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
26.11 + val for_method_PIDE: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
26.12 string * (Pos.pos_ * Tactic.input)
26.13 \<close>
26.14 end
26.15 @@ -73,16 +73,15 @@
26.16
26.17 (** find a next step in the specify-phase **)
26.18 (*
26.19 - there should be mutual recursion between for_problem and for_method
26.20 + here should be mutual recursion between for_problem and for_method
26.21 *)
26.22 -fun for_problem oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
26.23 +fun for_problem_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
26.24 let
26.25 val cdI = if dI = ThyC.id_empty then dI' else dI;
26.26 - val ctxt = Proof_Context.init_global (ThyC.get_theory cdI)
26.27 val cpI = if pI = Problem.id_empty then pI' else pI;
26.28 val cmI = if mI = MethodC.id_empty then mI' else mI;
26.29 val {ppc = pbt, prls, where_, ...} = Problem.from_store_PIDE ctxt cpI;
26.30 - val {ppc = mpc, ...} = MethodC.from_store cmI
26.31 + val {ppc = mpc, ...} = MethodC.from_store_PIDE ctxt cmI
26.32 val (preok, _) = Pre_Conds.check prls where_ pbl 0;
26.33 in
26.34 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
26.35 @@ -113,10 +112,10 @@
26.36 | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
26.37 end
26.38
26.39 -fun for_method oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
26.40 +fun for_method_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
26.41 let
26.42 val cmI = if mI = MethodC.id_empty then mI' else mI;
26.43 - val {ppc = mpc, prls, pre, ...} = MethodC.from_store cmI; (*..MethodC ?*)
26.44 + val {ppc = mpc, prls, pre, ...} = MethodC.from_store_PIDE ctxt cmI; (*..MethodC ?*)
26.45 val (preok, _) = Pre_Conds.check prls pre pbl 0;
26.46 in
26.47 (case find_first (I_Model.is_error o #5) met of
26.48 @@ -151,9 +150,9 @@
26.49 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
26.50 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
26.51 else if p_ = Pos.Pbl then
26.52 - for_problem oris (o_refs, refs) (pbl, met)
26.53 + for_problem_PIDE ctxt oris (o_refs, refs) (pbl, met)
26.54 else
26.55 - for_method oris (o_refs, refs) (pbl, met)
26.56 + for_method_PIDE ctxt oris (o_refs, refs) (pbl, met)
26.57 end
26.58
26.59
26.60 @@ -165,7 +164,7 @@
26.61 val (i_model, m_patt) =
26.62 if p_ = Pos.Met then
26.63 (met,
26.64 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
26.65 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store_PIDE ctxt |> #ppc)
26.66 else
26.67 (pbl,
26.68 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store_PIDE ctxt |> #ppc)
26.69 @@ -195,7 +194,7 @@
26.70 | _ => raise ERROR "finish_phase: unvered case get_obj"
26.71 val (_, pI, mI) = References.select_input ospec spec
26.72 val ctxt = Ctree.get_ctxt pt pos
26.73 - val mpc = (#ppc o MethodC.from_store) mI
26.74 + val mpc = (#ppc o MethodC.from_store_PIDE ctxt) mI
26.75 val ppc = (#ppc o Problem.from_store_PIDE ctxt) pI
26.76 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
26.77 val pt = Ctree.update_pblppc pt p pits
26.78 @@ -206,7 +205,7 @@
26.79 fun finish_phase_PIDEnote ctxt (o_model, o_refs) (problem_model, refs) =
26.80 let
26.81 val (_, pI, mI) = References.select_input o_refs refs
26.82 - val method_pattern = (#ppc o MethodC.from_store) mI
26.83 + val method_pattern = (#ppc o MethodC.from_store_PIDE ctxt) mI
26.84 val problem_pattern = (#ppc o Problem.from_store_PIDE ctxt) pI
26.85 val (problem_model, method_model) =
26.86 I_Model.complete_method (o_model, method_pattern, problem_pattern, problem_model)
26.87 @@ -216,13 +215,14 @@
26.88 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
26.89 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
26.90 *)
26.91 -fun do_all (pt, (p, _)) =
26.92 +fun do_all (pt, pos as (p, _)) =
26.93 let
26.94 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of
26.95 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
26.96 => (pors, dI, pI, mI)
26.97 | _ => raise ERROR "do_all: uncovered case get_obj"
26.98 - val {ppc, ...} = MethodC.from_store mI
26.99 + val ctxt = Ctree.get_ctxt pt pos
26.100 + val {ppc, ...} = MethodC.from_store_PIDE ctxt mI
26.101 val (_, vals) = O_Model.values' pors
26.102 val ctxt = ContextC.initialise dI vals
26.103 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
27.1 --- a/src/Tools/isac/Specify/step-specify.sml Mon Sep 26 10:57:53 2022 +0200
27.2 +++ b/src/Tools/isac/Specify/step-specify.sml Thu Sep 29 18:02:10 2022 +0200
27.3 @@ -11,7 +11,7 @@
27.4
27.5 val initialise_PIDE: Formalise.T ->
27.6 term * term * References.T * O_Model.T * Proof.context
27.7 - val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
27.8 + val nxt_specify_init_calc: Proof.context -> Formalise.T -> Calc.T * State_Steps.T
27.9 end
27.10
27.11 (**)
27.12 @@ -28,7 +28,7 @@
27.13 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
27.14 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
27.15 val (_, pI, mI) = References.select_input ospec spec
27.16 - val mpc = (#ppc o MethodC.from_store) mI (* just for reuse I_Model.complete_method *)
27.17 + val mpc = (#ppc o MethodC.from_store_PIDE ctxt) mI (* just for reuse I_Model.complete_method *)
27.18 val {cas, ppc, ...} = Problem.from_store_PIDE (Ctree.get_ctxt pt pos) pI
27.19 val pbl = I_Model.init ppc (* fill in descriptions *)
27.20 (*----------------if you think, this should be done by the Dialog
27.21 @@ -52,7 +52,6 @@
27.22 val (oris, dI, ctxt) = case get_obj I pt p of
27.23 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
27.24 | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"
27.25 - val ctxt = Ctree.get_ctxt pt pos
27.26 val opt = Refine.refine_ori_PIDE ctxt oris pI
27.27 in
27.28 case opt of
27.29 @@ -242,11 +241,10 @@
27.30 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
27.31 end;
27.32 (* nxt_specify_init_calc \<rightarrow> initialise *)
27.33 -fun nxt_specify_init_calc ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
27.34 - if pI <> []
27.35 +fun nxt_specify_init_calc ctxt ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
27.36 + if pI <> []
27.37 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
27.38 let
27.39 - val ctxt = Proof_Context.init_global (ThyC.get_theory dI)
27.40 val {cas, met, ppc, thy, ...} = Problem.from_store_PIDE ctxt pI
27.41 val dI = if dI = "" then Context.theory_name thy else dI
27.42 val mI = if mI = [] then hd met else mI
27.43 @@ -260,8 +258,8 @@
27.44 else
27.45 if mI <> []
27.46 then (* from met-browser *)
27.47 - let
27.48 - val {ppc, ...} = MethodC.from_store mI
27.49 + let
27.50 + val {ppc, ...} = MethodC.from_store_PIDE ctxt mI
27.51 val dI = if dI = "" then "Isac_Knowledge" else dI
27.52 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
27.53 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
27.54 @@ -274,7 +272,7 @@
27.55 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
27.56 ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)
27.57 in ((pt, ([], Pbl)), []) end
27.58 - | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
27.59 + | nxt_specify_init_calc _ (fmz, (dI, pI, mI)) =
27.60 let (* both ^^^ ^^^^^^^^^^^^ are either empty or complete *)
27.61 val (_, hdl, (dI, pI, mI), pors, pctxt) = initialise_PIDE (fmz, (dI, pI, mI))
27.62 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
28.1 --- a/src/Tools/isac/Test_Code/test-code.sml Mon Sep 26 10:57:53 2022 +0200
28.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Thu Sep 29 18:02:10 2022 +0200
28.3 @@ -54,11 +54,11 @@
28.4 fun f2str (Test_Out.FormKF cterm') = cterm'
28.5 | f2str _ = raise ERROR "f2str: uncovered case in fun.def.";
28.6
28.7 -(* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
28.8 - compare "fun CalcTree" which DOES decode *)
28.9 -fun CalcTreeTEST [(fmz, sp)] =
28.10 +(* create a calc-tree *)
28.11 +fun CalcTreeTEST [(model, refs as (thy_id, _, _))] =
28.12 let
28.13 - val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc (fmz, sp)
28.14 + val ctxt = thy_id |> ThyC.get_theory |> Proof_Context.init_global; (*will become an argument*)
28.15 + val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
28.16 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
28.17 val f = TESTg_form (pt,p)
28.18 in (p, []:NEW, f, tac, Celem.Sundef, pt) end
28.19 @@ -171,10 +171,10 @@
28.20
28.21
28.22 (** me' for |> **)
28.23 -
28.24 -fun CalcTreeTEST' [(fmz, sp)] =
28.25 +fun CalcTreeTEST' [(model, refs as (thy_id, _, _))] =
28.26 let
28.27 - val ((pt, p), _) = Step_Specify.nxt_specify_init_calc (fmz, sp)
28.28 + val ctxt = thy_id |> ThyC.get_theory |> Proof_Context.init_global; (*will become an argument*)
28.29 + val ((pt, p), _) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
28.30 in
28.31 (Tactic.Model_Problem, (pt, p)) (* thus <Output> shows Tactic on top *)
28.32 end