1.1 --- a/src/Tools/isac/Interpret/Interpret.thy Wed Sep 07 14:51:58 2022 +0200
1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Wed Sep 07 15:01:17 2022 +0200
1.3 @@ -32,28 +32,5 @@
1.4 end
1.5 \<close> ML \<open>
1.6 \<close> ML \<open>
1.7 -\<close> text \<open> (*postpone after successful test*)
1.8 -fun parent_node _ ([], _) = (true, [], Rule_Set.Empty)
1.9 - | parent_node pt (pos as (p, _)) =
1.10 - let
1.11 - fun par _ [] = (true, [], Rule_Set.Empty)
1.12 - | par pt p =
1.13 - if Ctree.is_pblobj (Ctree.get_obj I pt p)
1.14 - then (true, p, Rule_Set.Empty)
1.15 - else
1.16 - let
1.17 - val ctxt = Ctree.get_ctxt pt pos
1.18 - in
1.19 - case Ctree.get_obj Ctree.g_tac pt p of
1.20 - Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
1.21 - | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
1.22 - | _ => par pt (Pos.lev_up p)
1.23 - end
1.24 - in par pt (Pos.lev_up p) end;
1.25 -\<close> text \<open>
1.26 -parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T
1.27 -\<close> ML \<open>
1.28 -Ctree.get_ctxt
1.29 -\<close> ML \<open>
1.30 \<close>
1.31 end
2.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Sep 07 14:51:58 2022 +0200
2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Sep 07 15:01:17 2022 +0200
2.3 @@ -13,7 +13,7 @@
2.4 | Not_Associated;
2.5 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
2.6
2.7 - val parent_node : Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T
2.8 + val parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T
2.9 val init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> MethodC.id ->
2.10 Istate.T * Proof.context * Program.T
2.11 val resume_prog: ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree ->
3.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Sep 07 14:51:58 2022 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Sep 07 15:01:17 2022 +0200
3.3 @@ -46,33 +46,7 @@
3.4 ML_file calculation.sml
3.5
3.6 ML \<open>
3.7 -\<close> text \<open>
3.8 -fun lev_up [] = raise Ctree.PTREE "lev_up []"
3.9 - | lev_up p = (drop_last p);
3.10 -\<close> text \<open>
3.11 -lev_up: 'a list -> 'a list
3.12 -\<close> text \<open>
3.13 -lev_up: 'a list -> 'a list
3.14 -\<close> text \<open>
3.15 -open Ctree
3.16 -\<close> text \<open> (*postpone after successful test*)
3.17 -fun parent_node _ [] = (true, [], Rule_Set.Empty)
3.18 - | parent_node pt p =
3.19 - let
3.20 - fun par _ [] = (true, [], Rule_Set.Empty)
3.21 - | par pt p =
3.22 - if is_pblobj (get_obj I pt p)
3.23 - then (true, p, Rule_Set.Empty)
3.24 - else
3.25 - let
3.26 - val ctxt = p |> get_obj g_loc pt |> snd |> the |> snd (*parent_node goes lev_up*)
3.27 - in
3.28 - case get_obj g_tac pt p of
3.29 - Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
3.30 - | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
3.31 - | _ => par pt (lev_up p)
3.32 - end
3.33 - in par pt (lev_up p) end;
3.34 +\<close> ML \<open>
3.35 \<close> ML \<open>
3.36 \<close>
3.37 end
4.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Sep 07 14:51:58 2022 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Sep 07 15:01:17 2022 +0200
4.3 @@ -64,7 +64,6 @@
4.4 val get_somespec' : References_Def.T -> References_Def.T -> References_Def.T
4.5 exception PTREE of string;
4.6
4.7 -(*val parent_node : ctree -> Pos.pos -> bool * Pos.pos * Rule_Set.T*)
4.8 val rootthy : ctree -> theory
4.9 (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
4.10 val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree
4.11 @@ -386,39 +385,6 @@
4.12 \<close>
4.13 (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*)
4.14
4.15 -(* find the next parent, which is either a PblObj or a PrfObj * )
4.16 -fun parent_node _ [] = (true, [], Rule_Set.Empty)
4.17 - | parent_node pt p =
4.18 - let
4.19 - fun par _ [] = (true, [], Rule_Set.Empty)
4.20 - | par pt p =
4.21 - if is_pblobj (get_obj I pt p)
4.22 - then (true, p, Rule_Set.Empty)
4.23 - else case get_obj g_tac pt p of
4.24 - Tactic.Rewrite_Set rls' => (false, p, assoc_rls rls')
4.25 - | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
4.26 - | _ => par pt (lev_up p)
4.27 - in par pt (lev_up p) end;
4.28 -
4.29 -fun parent_node _ [] = (true, [], Rule_Set.Empty)
4.30 - | parent_node pt p =
4.31 - let
4.32 - fun par _ [] = (true, [], Rule_Set.Empty)
4.33 - | par pt p =
4.34 - if is_pblobj (get_obj I pt p)
4.35 - then (true, p, Rule_Set.Empty)
4.36 - else
4.37 - let
4.38 - val ctxt = p |> get_obj g_loc pt |> snd |> the |> snd (*parent_node goes lev_up*)
4.39 - in
4.40 - case get_obj g_tac pt p of
4.41 - Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
4.42 - | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
4.43 - | _ => par pt (lev_up p)
4.44 - end
4.45 - in par pt (lev_up p) end;
4.46 - *)
4.47 -
4.48 (* insert obj b into ctree at pos, ev.overwriting this pos *)
4.49 fun insert_pt b EmptyPtree [] = Nd (b, [])
4.50 | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _"