1.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Wed Sep 07 10:58:12 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Wed Sep 07 14:51:58 2022 +0200
     1.3 @@ -11,10 +11,10 @@
     1.4    ML_file istate.sml
     1.5    ML_file "sub-problem.sml"
     1.6    ML_file "thy-read.sml"
     1.7 +  ML_file "li-tool.sml"
     1.8    ML_file "solve-step.sml"
     1.9    ML_file "error-pattern.sml"
    1.10    ML_file derive.sml
    1.11 -  ML_file "li-tool.sml"
    1.12    ML_file "lucas-interpreter.sml"
    1.13    ML_file "step-solve.sml"
    1.14  
    1.15 @@ -32,5 +32,28 @@
    1.16  end
    1.17  \<close> ML \<open>
    1.18  \<close> ML \<open>
    1.19 +\<close> text \<open> (*postpone after successful test*)
    1.20 +fun parent_node _ ([], _) = (true, [], Rule_Set.Empty)
    1.21 +  | parent_node pt (pos as (p, _)) =
    1.22 +    let
    1.23 +      fun par _ [] = (true, [], Rule_Set.Empty)
    1.24 +        | par pt p =
    1.25 +            if Ctree.is_pblobj (Ctree.get_obj I pt p)
    1.26 +            then (true, p, Rule_Set.Empty)
    1.27 +  		      else 
    1.28 +              let
    1.29 +                val ctxt = Ctree.get_ctxt pt pos
    1.30 +              in
    1.31 +                case Ctree.get_obj Ctree.g_tac pt p of
    1.32 +      				    Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
    1.33 +      			    | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
    1.34 +      			    | _ => par pt (Pos.lev_up p)
    1.35 +              end
    1.36 +    in par pt (Pos.lev_up p) end; 
    1.37 +\<close> text \<open>
    1.38 +parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T
    1.39 +\<close> ML \<open>
    1.40 +Ctree.get_ctxt
    1.41 +\<close> ML \<open>
    1.42  \<close>
    1.43  end

     2.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Wed Sep 07 10:58:12 2022 +0200
     2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Wed Sep 07 14:51:58 2022 +0200
     2.3 @@ -13,6 +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 init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> MethodC.id ->
     2.9      Istate.T * Proof.context * Program.T
    2.10    val resume_prog: ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree -> 
    2.11 @@ -202,6 +203,25 @@
    2.12    | associate _ ctxt (tac, _) = 
    2.13      (trace_msg_3 ctxt tac; Not_Associated);
    2.14  
    2.15 +(* find the next parent, which is either a PblObj or a PrfObj *)
    2.16 +fun parent_node _ ([], _) = (true, [], Rule_Set.Empty)
    2.17 +  | parent_node pt (pos as (p, _)) =
    2.18 +    let
    2.19 +      fun par _ [] = (true, [], Rule_Set.Empty)
    2.20 +        | par pt p =
    2.21 +            if Ctree.is_pblobj (Ctree.get_obj I pt p)
    2.22 +            then (true, p, Rule_Set.Empty)
    2.23 +  		      else 
    2.24 +              let
    2.25 +                val ctxt = Ctree.get_ctxt pt pos
    2.26 +              in
    2.27 +                case Ctree.get_obj Ctree.g_tac pt p of
    2.28 +      				    Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
    2.29 +      			    | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
    2.30 +      			    | _ => par pt (Pos.lev_up p)
    2.31 +              end
    2.32 +    in par pt (Pos.lev_up p) end; 
    2.33 +
    2.34  (* create the initial interpreter state
    2.35    from the items of the guard and the formal arguments of the program.
    2.36  Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
    2.37 @@ -290,9 +310,9 @@
    2.38    in srls end
    2.39  
    2.40  (* resume program interpretation at the beginning of a step *)
    2.41 -fun resume_prog thy (p, p_) pt =
    2.42 +fun resume_prog thy (pos as (p, p_)) pt =
    2.43    let
    2.44 -    val (is_problem, p', rls') = parent_node pt p
    2.45 +    val (is_problem, p', rls') = parent_node pt pos
    2.46    in
    2.47      if is_problem then
    2.48        let

     3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Sep 07 10:58:12 2022 +0200
     3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Sep 07 14:51:58 2022 +0200
     3.3 @@ -266,12 +266,12 @@
     3.4  | scan_to_tactic _ _ = raise ERROR "scan_to_tactic: uncovered pattern";
     3.5  
     3.6  (* find the next applicable Prog_Tac in a prog *)
     3.7 -fun find_next_step (Rule.Prog prog) (ptp as(pt, (p, _))) (Pstate ist) ctxt =
     3.8 +fun find_next_step (Rule.Prog prog) (ptp as (pt, pos as (p, _))) (Pstate ist) ctxt =
     3.9     (case scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) of
    3.10        Accept_Tac (tac, ist, ctxt) =>
    3.11          Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
    3.12      | Term_Val prog_result =>
    3.13 -        (case parent_node pt p of
    3.14 +        (case LItool.parent_node pt pos of
    3.15            (true, p', _) => 
    3.16              let
    3.17                val (_, pblID, _) = get_obj g_spec pt p';

     4.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Wed Sep 07 10:58:12 2022 +0200
     4.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Wed Sep 07 14:51:58 2022 +0200
     4.3 @@ -16,9 +16,9 @@
     4.4    val add_hard:
     4.5      theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T
     4.6  
     4.7 -  val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
     4.8 +  val get_ruleset: 'a -> Pos.pos' -> Ctree.ctree ->
     4.9      string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool
    4.10 -  val get_eval: string -> Pos.pos -> Ctree.ctree -> string * ThyC.id * Eval.ml
    4.11 +  val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml
    4.12  
    4.13  \<^isac_test>\<open>
    4.14    val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list
    4.15 @@ -41,9 +41,9 @@
    4.16      (rew_ord', erls, ca)
    4.17    | rew_info rls = raise ERROR ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
    4.18  
    4.19 -fun get_ruleset _ p pt = 
    4.20 +fun get_ruleset _ (pos as (p, _)) pt = 
    4.21    let 
    4.22 -    val (pbl, p', rls') = Ctree.parent_node pt p
    4.23 +    val (pbl, p', rls') = LItool.parent_node pt pos
    4.24    in                                                      
    4.25      if pbl
    4.26      then 
    4.27 @@ -58,9 +58,9 @@
    4.28  		  in ("OK", thy', rew_ord', erls, false) end
    4.29    end;
    4.30  
    4.31 -fun get_eval scrop p pt = 
    4.32 +fun get_eval scrop (pos as (p, _)) pt = 
    4.33    let
    4.34 -    val (pbl, p', rls') =  Ctree.parent_node pt p
    4.35 +    val (pbl, p', rls') =  LItool.parent_node pt pos
    4.36    in
    4.37      if pbl
    4.38      then
    4.39 @@ -103,9 +103,9 @@
    4.40        in
    4.41          Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
    4.42        end
    4.43 -  | check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
    4.44 +  | check (Tactic.Calculate op_) (cs as (pt, pos as (p, _))) =
    4.45        let 
    4.46 -        val (msg, thy', isa_fn) = get_eval op_ p pt;
    4.47 +        val (msg, thy', isa_fn) = get_eval op_ pos pt;
    4.48          val f = Calc.current_formula cs;
    4.49        in
    4.50          if msg = "OK"
    4.51 @@ -133,9 +133,9 @@
    4.52        in
    4.53          Applicable.Yes (Tactic.Or_to_List' (f, ls))
    4.54        end
    4.55 -  | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) = 
    4.56 +  | check (Tactic.Rewrite thm) (cs as (pt, pos as (p, _))) = 
    4.57        let
    4.58 -        val (msg, thy', ro, rls', _) = get_ruleset thm p pt;
    4.59 +        val (msg, thy', ro, rls', _) = get_ruleset thm pos pt;
    4.60          val thy = ThyC.get_theory thy';
    4.61          val ctxt = Proof_Context.init_global thy;
    4.62          val f = Calc.current_formula cs;

     5.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Wed Sep 07 10:58:12 2022 +0200
     5.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Wed Sep 07 14:51:58 2022 +0200
     5.3 @@ -46,13 +46,16 @@
     5.4    ML_file calculation.sml
     5.5  
     5.6  ML \<open>
     5.7 -\<close> ML \<open>
     5.8 +\<close> text \<open>
     5.9  fun lev_up [] = raise Ctree.PTREE "lev_up []"
    5.10    | lev_up p = (drop_last p);
    5.11 -\<close> ML \<open>
    5.12 -\<close> ML \<open>
    5.13 +\<close> text \<open>
    5.14 +lev_up: 'a list -> 'a list
    5.15 +\<close> text \<open>
    5.16 +lev_up: 'a list -> 'a list
    5.17 +\<close> text \<open>
    5.18  open Ctree
    5.19 -\<close> ML \<open> (*postpone after successful test*)
    5.20 +\<close> text \<open> (*postpone after successful test*)
    5.21  fun parent_node _ [] = (true, [], Rule_Set.Empty)
    5.22    | parent_node pt p =
    5.23      let
    5.24 @@ -62,7 +65,7 @@
    5.25              then (true, p, Rule_Set.Empty)
    5.26    		      else 
    5.27                let
    5.28 -                val ctxt = p |> get_obj g_loc pt |> snd |> the |> snd (*???*)
    5.29 +                val ctxt = p |> get_obj g_loc pt |> snd |> the |> snd (*parent_node goes lev_up*)
    5.30                in
    5.31                  case get_obj g_tac pt p of
    5.32        				    Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')

     6.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Wed Sep 07 10:58:12 2022 +0200
     6.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Wed Sep 07 14:51:58 2022 +0200
     6.3 @@ -64,7 +64,7 @@
     6.4    val get_somespec' : References_Def.T -> References_Def.T -> References_Def.T
     6.5    exception PTREE of string;
     6.6    
     6.7 -  val parent_node : ctree -> Pos.pos -> bool * Pos.pos * Rule_Set.T
     6.8 +(*val parent_node : ctree -> Pos.pos -> bool * Pos.pos * Rule_Set.T*)
     6.9    val rootthy : ctree -> theory
    6.10  (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
    6.11    val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree
    6.12 @@ -386,7 +386,7 @@
    6.13  \<close>
    6.14  (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*)
    6.15  
    6.16 -(* find the next parent, which is either a PblObj or a PrfObj *)
    6.17 +(* find the next parent, which is either a PblObj or a PrfObj * )
    6.18  fun parent_node _ [] = (true, [], Rule_Set.Empty)
    6.19    | parent_node pt p =
    6.20      let
    6.21 @@ -400,6 +400,25 @@
    6.22  			    | _ => par pt (lev_up p)
    6.23      in par pt (lev_up p) end; 
    6.24  
    6.25 +fun parent_node _ [] = (true, [], Rule_Set.Empty)
    6.26 +  | parent_node pt p =
    6.27 +    let
    6.28 +      fun par _ [] = (true, [], Rule_Set.Empty)
    6.29 +        | par pt p =
    6.30 +            if is_pblobj (get_obj I pt p)
    6.31 +            then (true, p, Rule_Set.Empty)
    6.32 +  		      else 
    6.33 +              let
    6.34 +                val ctxt = p |> get_obj g_loc pt |> snd |> the |> snd (*parent_node goes lev_up*)
    6.35 +              in
    6.36 +                case get_obj g_tac pt p of
    6.37 +      				    Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
    6.38 +      			    | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
    6.39 +      			    | _ => par pt (lev_up p)
    6.40 +              end
    6.41 +    in par pt (lev_up p) end; 
    6.42 + *)
    6.43 +
    6.44  (* insert obj b into ctree at pos, ev.overwriting this pos *)
    6.45  fun insert_pt b EmptyPtree [] = Nd (b, [])
    6.46    | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _"

     7.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Sep 07 10:58:12 2022 +0200
     7.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Sep 07 14:51:58 2022 +0200
     7.3 @@ -458,7 +458,7 @@
     7.4  
     7.5      Term_Val prog_result  (*return from scan_to_tactic*);
     7.6  "~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
     7.7 -    val (true, p', _) = (*case*) parent_node pt p (*of*);
     7.8 +    val (true, p', _) = (*case*) parent_node pt pos (*of*);
     7.9                val (_, pblID, _) = get_obj g_spec pt p';
    7.10  
    7.11       End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))

     8.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml	Wed Sep 07 10:58:12 2022 +0200
     8.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml	Wed Sep 07 14:51:58 2022 +0200
     8.3 @@ -344,7 +344,7 @@
     8.4      LItool.resume_prog thy' (p,p_) pt;
     8.5  "~~~~~ fun resume_prog , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
     8.6    (*if*) Pos.on_specification (p, p_) (*else*);
     8.7 -    val (pbl, p', rls') = parent_node pt p
     8.8 +    val (pbl, p', rls') = parent_node pt pos
     8.9      (*if*) pbl (*then*);
    8.10  	         val metID = get_obj g_metID pt p'
    8.11  (*["RootEq", "solve_sq_root_equation"] found for correction, which caused ERROR 2*)