special constant to prevent eta-contraction of the check-phase syntax of case translations
authortraytel
Fri Apr 05 22:08:42 2013 +0200 (2013-04-05)
changeset 516742b1498a2ce85
parent 51673 4dfa00e264d8
child 51675 18bbc78888aa
special constant to prevent eta-contraction of the check-phase syntax of case translations
src/HOL/Inductive.thy
src/HOL/Tools/case_translation.ML
     1.1 --- a/src/HOL/Inductive.thy	Tue Jan 22 14:33:45 2013 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Fri Apr 05 22:08:42 2013 +0200
     1.3 @@ -275,6 +275,7 @@
     1.4  ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
     1.5  
     1.6  consts
     1.7 +  case_guard :: "'a \<Rightarrow> 'a"
     1.8    case_nil :: "'a \<Rightarrow> 'b"
     1.9    case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.10    case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
     2.1 --- a/src/HOL/Tools/case_translation.ML	Tue Jan 22 14:33:45 2013 +0100
     2.2 +++ b/src/HOL/Tools/case_translation.ML	Fri Apr 05 22:08:42 2013 +0200
     2.3 @@ -123,11 +123,11 @@
     2.4          fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
     2.5            | dest_case2 t = [t];
     2.6        in
     2.7 -        fold_rev
     2.8 +        Syntax.const @{const_syntax case_guard} $ (fold_rev
     2.9            (fn t => fn u =>
    2.10               Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
    2.11            (dest_case2 u)
    2.12 -          (Syntax.const @{const_syntax case_nil}) $ t
    2.13 +          (Syntax.const @{const_syntax case_nil}) $ t)
    2.14        end
    2.15    | case_tr _ _ = case_error "case_tr";
    2.16  
    2.17 @@ -139,8 +139,9 @@
    2.18  
    2.19  (* print translation *)
    2.20  
    2.21 -fun case_tr' [t, u, x] =
    2.22 +fun case_tr' [tx] =
    2.23        let
    2.24 +        val (t, x) = Term.dest_comb tx;
    2.25          fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used =
    2.26                let val (s', used') = Name.variant s used
    2.27                in mk_clause t ((s', T) :: xs) used' end
    2.28 @@ -151,18 +152,16 @@
    2.29  
    2.30          fun mk_clauses (Const (@{const_syntax case_nil}, _)) = []
    2.31            | mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) =
    2.32 -              mk_clauses' t u
    2.33 -        and mk_clauses' t u =
    2.34                mk_clause t [] (Term.declare_term_frees t Name.context) ::
    2.35                mk_clauses u
    2.36        in
    2.37          Syntax.const @{syntax_const "_case_syntax"} $ x $
    2.38            foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
    2.39 -            (mk_clauses' t u)
    2.40 +            (mk_clauses t)
    2.41        end;
    2.42  
    2.43  val trfun_setup' = Sign.add_trfuns
    2.44 -  ([], [], [(@{const_syntax "case_cons"}, case_tr')], []);
    2.45 +  ([], [], [(@{const_syntax "case_guard"}, case_tr')], []);
    2.46  
    2.47  
    2.48  (* declarations *)
    2.49 @@ -413,7 +412,7 @@
    2.50  
    2.51  fun check_case ctxt =
    2.52    let
    2.53 -    fun decode_case ((t as Const (@{const_name case_cons}, _) $ _ $ _) $ u) =
    2.54 +    fun decode_case (Const (@{const_name case_guard}, _) $ (t $ u)) =
    2.55          make_case ctxt Error Name.context (decode_case u) (decode_cases t)
    2.56      | decode_case (t $ u) = decode_case t $ decode_case u
    2.57      | decode_case (Abs (x, T, u)) =
    2.58 @@ -517,7 +516,12 @@
    2.59          encode_clause S T p $ encode_cases S T ps;
    2.60  
    2.61  fun encode_case (t, ps as (pat, rhs) :: _) =
    2.62 -      encode_cases (fastype_of pat) (fastype_of rhs) ps $ t
    2.63 +    let
    2.64 +      val T = fastype_of rhs;
    2.65 +    in
    2.66 +      Const (@{const_name case_guard}, T --> T) $
    2.67 +        (encode_cases (fastype_of pat) (fastype_of rhs) ps $ t)
    2.68 +    end
    2.69    | encode_case _ = case_error "encode_case";
    2.70  
    2.71  fun strip_case' ctxt d (pat, rhs) =