1.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Sat Nov 30 15:43:14 2019 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Sat Nov 30 17:03:49 2019 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4  sig
     1.5    val dest_spec : term -> Celem.spec
     1.6    val get_stac : 'a -> term -> term option (*rename get_first*)
     1.7 -  val eval_leaf: (term * term) list -> term option -> term -> term -> term option * Program.leaf
     1.8 +  val eval_leaf: (term * term) list -> term option -> term -> term -> Program.leaf * term option
     1.9    val is: term -> bool
    1.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.11    (*NONE*)
    1.12 @@ -129,60 +129,68 @@
    1.13  	       (3) non-matching patterns become an Program.Expr by fall-through.
    1.14  WN060906 quick and dirty fix: due to (2) a is returned, too *)
    1.15  fun eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
    1.16 -    (NONE, Program.Tac (subst_atomic E t))
    1.17 +    (Program.Tac (subst_atomic E t), NONE)
    1.18    | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
    1.19 -    (a, Program.Tac (
    1.20 +    (Program.Tac (
    1.21        case a of SOME a' => (subst_atomic E (t $ a'))
    1.22 -		          | NONE => ((subst_atomic E t) $ v)))
    1.23 +		          | NONE => ((subst_atomic E t) $ v)),
    1.24 +    a)
    1.25    | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) =
    1.26 -    (NONE, Program.Tac (subst_atomic E t))
    1.27 +    (Program.Tac (subst_atomic E t), NONE)
    1.28    | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Inst"(*2*), _) $ _ $ _)) =
    1.29 -    (a, Program.Tac (
    1.30 +    (Program.Tac (
    1.31        case a of SOME a' => subst_atomic E (t $ a')
    1.32 -	            | NONE => ((subst_atomic E t) $ v)))
    1.33 +	            | NONE => ((subst_atomic E t) $ v)),
    1.34 +    a)
    1.35    | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set"(*1*), _) $ _ $ _)) =
    1.36 -    (NONE, Program.Tac (subst_atomic E t))
    1.37 +    (Program.Tac (subst_atomic E t), NONE)
    1.38    | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set"(*2*), _) $ _)) =
    1.39 -    (a, Program.Tac (
    1.40 +    (Program.Tac (
    1.41        case a of SOME a' => subst_atomic E (t $ a')
    1.42 -	            | NONE => ((subst_atomic E t) $ v)))
    1.43 +	            | NONE => ((subst_atomic E t) $ v)),
    1.44 +    a)
    1.45    | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*1*), _) $ _ $ _ $ _)) =
    1.46 -    (NONE, Program.Tac (subst_atomic E t))
    1.47 +    (Program.Tac (subst_atomic E t), NONE)
    1.48    | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*2*), _) $ _ $ _)) =
    1.49 -    (a, Program.Tac (
    1.50 +    (Program.Tac (
    1.51        case a of SOME a' => subst_atomic E (t $ a')
    1.52 -	            | NONE => ((subst_atomic E t) $ v)))
    1.53 +	            | NONE => ((subst_atomic E t) $ v)),
    1.54 +    a)
    1.55    | eval_leaf E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =
    1.56 -    (NONE, Program.Tac (subst_atomic E t))
    1.57 +    (Program.Tac (subst_atomic E t), NONE)
    1.58    | eval_leaf E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =
    1.59 -    (a, Program.Tac (
    1.60 +    (Program.Tac (
    1.61        case a of SOME a' => subst_atomic E (t $ a')
    1.62 -	            | NONE => ((subst_atomic E t) $ v)))
    1.63 +	            | NONE => ((subst_atomic E t) $ v)),
    1.64 +    a)
    1.65    | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check'_elementwise"(*1*),_) $ _ $ _)) = 
    1.66 -    (NONE, Program.Tac (subst_atomic E t))
    1.67 +    (Program.Tac (subst_atomic E t), NONE)
    1.68    | eval_leaf E a v (t as (Const ("Prog_Tac.Check'_elementwise"(*2*), _) $ _)) = 
    1.69 -    (a, Program.Tac (
    1.70 +    (Program.Tac (
    1.71        case a of SOME a' => subst_atomic E (t $ a')
    1.72 -		          | NONE => ((subst_atomic E t) $ v)))
    1.73 +		          | NONE => ((subst_atomic E t) $ v)),
    1.74 +    a)
    1.75    | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or'_to'_List"(*1*), _) $ _)) = 
    1.76 -    (NONE, Program.Tac (subst_atomic E t))
    1.77 +    (Program.Tac (subst_atomic E t), NONE)
    1.78    | eval_leaf E a v (t as (Const ("Prog_Tac.Or'_to'_List"(*2*), _))) = (*t $ v*)
    1.79 -    (a, Program.Tac (
    1.80 +    (Program.Tac (
    1.81        case a of SOME a' => subst_atomic E (t $ a')
    1.82 -		          | NONE => ((subst_atomic E t) $ v)))
    1.83 +		          | NONE => ((subst_atomic E t) $ v)),
    1.84 +    a)
    1.85    | eval_leaf E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
    1.86 -    (NONE, Program.Tac (subst_atomic E t))
    1.87 +    (Program.Tac (subst_atomic E t), NONE)
    1.88    | eval_leaf E _ _ (t as (Const ("Prog_Tac.Take", _) $ _)) =
    1.89 -    (NONE, Program.Tac (subst_atomic E t))
    1.90 +    (Program.Tac (subst_atomic E t), NONE)
    1.91    | eval_leaf E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
    1.92 -    (NONE, Program.Tac (subst_atomic E t))
    1.93 +    (Program.Tac (subst_atomic E t), NONE)
    1.94    | eval_leaf E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =
    1.95 -    (a, Program.Tac (
    1.96 +    (Program.Tac (
    1.97        case a of SOME a' => subst_atomic E (t $ a')
    1.98 -		          | NONE => ((subst_atomic E t) $ v)))
    1.99 +		          | NONE => ((subst_atomic E t) $ v)),
   1.100 +    a)
   1.101    (*now all tactics are matched out and this leaf must be without a tactic*)
   1.102    | eval_leaf E a v t = 
   1.103 -    (a, Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t));
   1.104 +    (Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t), a);
   1.105  
   1.106  
   1.107  (* check if a term is a Prog_Tac *)