allow redundant cases in the list comprehension translation
authortraytel
Fri Apr 05 22:08:42 2013 +0200 (2013-04-05)
changeset 516781e33b81c328a
parent 51677 d2b3372e6033
child 51679 e7316560928b
allow redundant cases in the list comprehension translation
src/HOL/Inductive.thy
src/HOL/List.thy
src/HOL/Tools/case_translation.ML
     1.1 --- a/src/HOL/Inductive.thy	Fri Apr 05 22:08:42 2013 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Fri Apr 05 22:08:42 2013 +0200
     1.3 @@ -275,7 +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_guard :: "bool \<Rightarrow> 'a \<Rightarrow> 'a"
     1.9    case_nil :: "'a \<Rightarrow> 'b"
    1.10    case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.11    case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
    1.12 @@ -299,7 +299,7 @@
    1.13    fun fun_tr ctxt [cs] =
    1.14      let
    1.15        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    1.16 -      val ft = Case_Translation.case_tr ctxt [x, cs];
    1.17 +      val ft = Case_Translation.case_tr true ctxt [x, cs];
    1.18      in lambda x ft end
    1.19  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.20  *}
     2.1 --- a/src/HOL/List.thy	Fri Apr 05 22:08:42 2013 +0200
     2.2 +++ b/src/HOL/List.thy	Fri Apr 05 22:08:42 2013 +0200
     2.3 @@ -407,7 +407,7 @@
     2.4            Syntax.const @{syntax_const "_case1"} $
     2.5              Syntax.const @{const_syntax dummy_pattern} $ NilC;
     2.6          val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
     2.7 -      in Syntax_Trans.abs_tr [x, Case_Translation.case_tr ctxt [x, cs]] end;
     2.8 +      in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end;
     2.9  
    2.10      fun abs_tr ctxt p e opti =
    2.11        (case Term_Position.strip_positions p of
     3.1 --- a/src/HOL/Tools/case_translation.ML	Fri Apr 05 22:08:42 2013 +0200
     3.2 +++ b/src/HOL/Tools/case_translation.ML	Fri Apr 05 22:08:42 2013 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  signature CASE_TRANSLATION =
     3.5  sig
     3.6    datatype config = Error | Warning | Quiet
     3.7 -  val case_tr: Proof.context -> term list -> term
     3.8 +  val case_tr: bool -> Proof.context -> term list -> term
     3.9    val lookup_by_constr: Proof.context -> string * typ -> (term * term list) option
    3.10    val lookup_by_constr_permissive: Proof.context -> string * typ -> (term * term list) option
    3.11    val lookup_by_case: Proof.context -> string -> (term * term list) option
    3.12 @@ -100,7 +100,7 @@
    3.13  
    3.14  fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
    3.15  
    3.16 -fun case_tr ctxt [t, u] =
    3.17 +fun case_tr err ctxt [t, u] =
    3.18        let
    3.19          val thy = Proof_Context.theory_of ctxt;
    3.20  
    3.21 @@ -123,24 +123,26 @@
    3.22  
    3.23          fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
    3.24            | dest_case2 t = [t];
    3.25 +
    3.26 +        val errt = if err then @{term True} else @{term False};
    3.27        in
    3.28 -        Syntax.const @{const_syntax case_guard} $ (fold_rev
    3.29 +        Syntax.const @{const_syntax case_guard} $ errt $ (fold_rev
    3.30            (fn t => fn u =>
    3.31               Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
    3.32            (dest_case2 u)
    3.33            (Syntax.const @{const_syntax case_nil}) $ t)
    3.34        end
    3.35 -  | case_tr _ _ = case_error "case_tr";
    3.36 +  | case_tr _ _ _ = case_error "case_tr";
    3.37  
    3.38  val trfun_setup =
    3.39    Sign.add_advanced_trfuns ([],
    3.40 -    [(@{syntax_const "_case_syntax"}, case_tr)],
    3.41 +    [(@{syntax_const "_case_syntax"}, case_tr true)],
    3.42      [], []);
    3.43  
    3.44  
    3.45  (* print translation *)
    3.46  
    3.47 -fun case_tr' [tx] =
    3.48 +fun case_tr' [_, tx] =
    3.49        let
    3.50          val (t, x) = Term.dest_comb tx;
    3.51          fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used =
    3.52 @@ -410,8 +412,9 @@
    3.53  
    3.54  fun check_case ctxt =
    3.55    let
    3.56 -    fun decode_case (Const (@{const_name case_guard}, _) $ (t $ u)) =
    3.57 -          make_case ctxt Error Name.context (decode_case u) (decode_cases t)
    3.58 +    fun decode_case (Const (@{const_name case_guard}, _) $ b $ (t $ u)) =
    3.59 +          make_case ctxt (if b = @{term True} then Error else Warning)
    3.60 +            Name.context (decode_case u) (decode_cases t)
    3.61        | decode_case (t $ u) = decode_case t $ decode_case u
    3.62        | decode_case (Abs (x, T, u)) =
    3.63            let val (x', u') = Term.dest_abs (x, T, u);
    3.64 @@ -517,7 +520,7 @@
    3.65      let
    3.66        val T = fastype_of rhs;
    3.67      in
    3.68 -      Const (@{const_name case_guard}, T --> T) $
    3.69 +      Const (@{const_name case_guard}, @{typ bool} --> T --> T) $ @{term True} $
    3.70          (encode_cases recur (fastype_of pat) (fastype_of rhs) ps $ t)
    3.71      end
    3.72    | encode_case _ _ = case_error "encode_case";