added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
authorwenzelm
Sat Mar 26 12:01:40 2011 +0100 (2011-03-26)
changeset 4208674bf78db0d87
parent 42085 2ba15af46cb7
child 42122 524bb42442dc
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
recovered printing of Hoare assign statements from 45d090186bbe;
src/HOL/Hoare_Parallel/OG_Syntax.thy
src/HOL/Hoare_Parallel/RG_Syntax.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Tools/record.ML
src/Pure/Syntax/syn_trans.ML
     1.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat Mar 26 10:52:29 2011 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat Mar 26 12:01:40 2011 +0100
     1.3 @@ -93,20 +93,14 @@
     1.4            annquote_tr' (Syntax.const name) (r :: t :: ts)
     1.5        | annbexp_tr' _ _ = raise Match;
     1.6  
     1.7 -    fun K_tr' (Abs (_, _, t)) =
     1.8 -          if null (loose_bnos t) then t else raise Match
     1.9 -      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
    1.10 -          if null (loose_bnos t) then t else raise Match
    1.11 -      | K_tr' _ = raise Match;
    1.12 -
    1.13      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
    1.14            quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
    1.15 -            (Abs (x, dummyT, K_tr' k) :: ts)
    1.16 +            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
    1.17        | assign_tr' _ = raise Match;
    1.18  
    1.19      fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
    1.20            quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
    1.21 -            (Abs (x, dummyT, K_tr' k) :: ts)
    1.22 +            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
    1.23        | annassign_tr' _ = raise Match;
    1.24  
    1.25      fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
     2.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Mar 26 10:52:29 2011 +0100
     2.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Mar 26 12:01:40 2011 +0100
     2.3 @@ -67,15 +67,9 @@
     2.4            quote_tr' (Syntax.const name) (t :: ts)
     2.5        | bexp_tr' _ _ = raise Match;
     2.6  
     2.7 -    fun K_tr' (Abs (_, _, t)) =
     2.8 -          if null (loose_bnos t) then t else raise Match
     2.9 -      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
    2.10 -          if null (loose_bnos t) then t else raise Match
    2.11 -      | K_tr' _ = raise Match;
    2.12 -
    2.13      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
    2.14            quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
    2.15 -            (Abs (x, dummyT, K_tr' k) :: ts)
    2.16 +            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
    2.17        | assign_tr' _ = raise Match;
    2.18    in
    2.19     [(@{const_syntax Collect}, assert_tr'),
     3.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Sat Mar 26 10:52:29 2011 +0100
     3.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Sat Mar 26 12:01:40 2011 +0100
     3.3 @@ -237,15 +237,9 @@
     3.4            quote_tr' (Syntax.const name) (t :: ts)
     3.5        | bexp_tr' _ _ = raise Match;
     3.6  
     3.7 -    fun K_tr' (Abs (_, _, t)) =
     3.8 -          if null (loose_bnos t) then t else raise Match
     3.9 -      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
    3.10 -          if null (loose_bnos t) then t else raise Match
    3.11 -      | K_tr' _ = raise Match;
    3.12 -
    3.13      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
    3.14            quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
    3.15 -            (Abs (x, dummyT, K_tr' k) :: ts)
    3.16 +            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
    3.17        | assign_tr' _ = raise Match;
    3.18    in
    3.19     [(@{const_syntax Collect}, assert_tr'),
     4.1 --- a/src/HOL/Tools/record.ML	Sat Mar 26 10:52:29 2011 +0100
     4.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 26 12:01:40 2011 +0100
     4.3 @@ -961,21 +961,11 @@
     4.4  fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
     4.5        (case dest_update ctxt c of
     4.6          SOME name =>
     4.7 -          let
     4.8 -            val opt_t =
     4.9 -              (case k of
    4.10 -                Abs (_, _, Abs (_, _, t) $ Bound 0) =>
    4.11 -                  if null (loose_bnos t) then SOME t else NONE
    4.12 -              | Abs (_, _, t) =>
    4.13 -                  if null (loose_bnos t) then SOME t else NONE
    4.14 -              | _ => NONE);
    4.15 -          in
    4.16 -            (case opt_t of
    4.17 -              SOME t =>
    4.18 -                apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
    4.19 -                  (field_updates_tr' ctxt u)
    4.20 -            | NONE => ([], tm))
    4.21 -          end
    4.22 +          (case try Syntax.const_abs_tr' k of
    4.23 +            SOME t =>
    4.24 +              apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
    4.25 +                (field_updates_tr' ctxt u)
    4.26 +          | NONE => ([], tm))
    4.27        | NONE => ([], tm))
    4.28    | field_updates_tr' _ tm = ([], tm);
    4.29  
     5.1 --- a/src/Pure/Syntax/syn_trans.ML	Sat Mar 26 10:52:29 2011 +0100
     5.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sat Mar 26 12:01:40 2011 +0100
     5.3 @@ -10,6 +10,7 @@
     5.4    val eta_contract_raw: Config.raw
     5.5    val eta_contract: bool Config.T
     5.6    val atomic_abs_tr': string * typ * term -> term * term
     5.7 +  val const_abs_tr': term -> term
     5.8    val mk_binder_tr: string * string -> string * (term list -> term)
     5.9    val mk_binder_tr': string * string -> string * (term list -> term)
    5.10    val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
    5.11 @@ -316,6 +317,13 @@
    5.12      ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
    5.13    | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
    5.14  
    5.15 +fun const_abs_tr' t =
    5.16 +  (case eta_abs t of
    5.17 +    Abs (_, _, t') =>
    5.18 +      if Term.is_dependent t' then raise Match
    5.19 +      else incr_boundvars ~1 t'
    5.20 +  | _ => raise Match);
    5.21 +
    5.22  
    5.23  (* binders *)
    5.24