clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
authorwenzelm
Thu Dec 15 18:08:40 2011 +0100 (2011-12-15)
changeset 45891d73605c829cc
parent 45890 5f70aaecae26
child 45894 629d123b7dbe
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
src/HOL/Inductive.thy
src/HOL/List.thy
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Inductive.thy	Thu Dec 15 17:37:14 2011 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Thu Dec 15 18:08:40 2011 +0100
     1.3 @@ -11,9 +11,9 @@
     1.4    "Tools/dseq.ML"
     1.5    "Tools/Datatype/datatype_aux.ML"
     1.6    "Tools/Datatype/datatype_prop.ML"
     1.7 -  "Tools/Datatype/datatype_case.ML"
     1.8    ("Tools/Datatype/datatype_abs_proofs.ML")
     1.9    ("Tools/Datatype/datatype_data.ML")
    1.10 +  ("Tools/Datatype/datatype_case.ML")
    1.11    ("Tools/Datatype/rep_datatype.ML")
    1.12    ("Tools/primrec.ML")
    1.13    ("Tools/Datatype/datatype_codegen.ML")
    1.14 @@ -277,9 +277,8 @@
    1.15  text {* Package setup. *}
    1.16  
    1.17  use "Tools/Datatype/datatype_abs_proofs.ML"
    1.18 -use "Tools/Datatype/datatype_data.ML"
    1.19 -setup Datatype_Data.setup
    1.20 -
    1.21 +use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
    1.22 +use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.23  use "Tools/Datatype/rep_datatype.ML"
    1.24  
    1.25  use "Tools/Datatype/datatype_codegen.ML"
    1.26 @@ -300,7 +299,7 @@
    1.27      let
    1.28        (* FIXME proper name context!? *)
    1.29        val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
    1.30 -      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs];
    1.31 +      val ft = Datatype_Case.case_tr true ctxt [x, cs];
    1.32      in lambda x ft end
    1.33  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.34  *}
     2.1 --- a/src/HOL/List.thy	Thu Dec 15 17:37:14 2011 +0100
     2.2 +++ b/src/HOL/List.thy	Thu Dec 15 18:08:40 2011 +0100
     2.3 @@ -391,7 +391,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 -      val ft = Datatype_Case.case_tr false Datatype.info_of_constr_permissive ctxt [x, cs];
     2.8 +      val ft = Datatype_Case.case_tr false ctxt [x, cs];
     2.9      in lambda x ft end;
    2.10  
    2.11    fun abs_tr ctxt (p as Free (s, T)) e opti =
     3.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Dec 15 17:37:14 2011 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Dec 15 18:08:40 2011 +0100
     3.3 @@ -9,17 +9,12 @@
     3.4  sig
     3.5    datatype config = Error | Warning | Quiet
     3.6    type info = Datatype_Aux.info
     3.7 -  val make_case: (string * typ -> info option) ->
     3.8 -    Proof.context -> config -> string list -> term -> (term * term) list ->
     3.9 -    term
    3.10 -  val dest_case: (string -> info option) -> bool ->
    3.11 -    string list -> term -> (term * (term * term) list) option
    3.12 -  val strip_case: (string -> info option) -> bool ->
    3.13 -    term -> (term * (term * term) list) option
    3.14 -  val case_tr: bool -> (theory -> string * typ -> info option) ->
    3.15 -    Proof.context -> term list -> term
    3.16 -  val case_tr': (theory -> string -> info option) ->
    3.17 -    string -> Proof.context -> term list -> term
    3.18 +  val make_case :  Proof.context -> config -> string list -> term -> (term * term) list -> term
    3.19 +  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    3.20 +  val case_tr: bool -> Proof.context -> term list -> term
    3.21 +  val case_tr': string -> Proof.context -> term list -> term
    3.22 +  val add_case_tr' : string list -> theory -> theory
    3.23 +  val setup: theory -> theory
    3.24  end;
    3.25  
    3.26  structure Datatype_Case : DATATYPE_CASE =
    3.27 @@ -147,8 +142,10 @@
    3.28  
    3.29  (* Translation of pattern terms into nested case expressions. *)
    3.30  
    3.31 -fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
    3.32 +fun mk_case ctxt ty_match ty_inst type_of used range_ty =
    3.33    let
    3.34 +    val tab = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt);
    3.35 +
    3.36      val name = singleton (Name.variant_list used) "a";
    3.37      fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand_var_row", ~1)
    3.38        | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
    3.39 @@ -215,7 +212,7 @@
    3.40          else x :: xs)
    3.41      | _ => I) pat [];
    3.42  
    3.43 -fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses =
    3.44 +fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses =
    3.45    let
    3.46      fun string_of_clause (pat, rhs) =
    3.47        Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
    3.48 @@ -228,7 +225,7 @@
    3.49        | _ => case_error "all cases must have the same result type");
    3.50      val used' = fold add_row_used rows used;
    3.51      val (tags, case_tm) =
    3.52 -      mk_case tab ctxt ty_match ty_inst type_of used' rangeT [x] rows
    3.53 +      mk_case ctxt ty_match ty_inst type_of used' rangeT [x] rows
    3.54          handle CASE_ERROR (msg, i) =>
    3.55            case_error
    3.56              (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
    3.57 @@ -245,9 +242,9 @@
    3.58  
    3.59  in
    3.60  
    3.61 -fun make_case tab ctxt =
    3.62 +fun make_case ctxt =
    3.63    gen_make_case (match_type (Proof_Context.theory_of ctxt))
    3.64 -    Envir.subst_term_types fastype_of tab ctxt;
    3.65 +    Envir.subst_term_types fastype_of ctxt;
    3.66  
    3.67  val make_case_untyped =
    3.68    gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT);
    3.69 @@ -257,7 +254,7 @@
    3.70  
    3.71  (* parse translation *)
    3.72  
    3.73 -fun case_tr err tab_of ctxt [t, u] =
    3.74 +fun case_tr err ctxt [t, u] =
    3.75        let
    3.76          val thy = Proof_Context.theory_of ctxt;
    3.77          val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt);
    3.78 @@ -291,12 +288,17 @@
    3.79            | dest_case2 t = [t];
    3.80          val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
    3.81          val case_tm =
    3.82 -          make_case_untyped (tab_of thy) ctxt
    3.83 +          make_case_untyped ctxt
    3.84              (if err then Error else Warning) []
    3.85              (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
    3.86                 (flat cnstrts) t) cases;
    3.87        in case_tm end
    3.88 -  | case_tr _ _ _ ts = case_error "case_tr";
    3.89 +  | case_tr _ _ ts = case_error "case_tr";
    3.90 +
    3.91 +val trfun_setup =
    3.92 +  Sign.add_advanced_trfuns ([],
    3.93 +    [(@{syntax_const "_case_syntax"}, case_tr true)],
    3.94 +    [], []);
    3.95  
    3.96  
    3.97  (* Pretty printing of nested case expressions *)
    3.98 @@ -306,7 +308,7 @@
    3.99  local
   3.100  
   3.101  (* FIXME proper name context!? *)
   3.102 -fun gen_dest_case name_of type_of tab d used t =
   3.103 +fun gen_dest_case name_of type_of ctxt d used t =
   3.104    (case apfst name_of (strip_comb t) of
   3.105      (SOME cname, ts as _ :: _) =>
   3.106        let
   3.107 @@ -328,6 +330,7 @@
   3.108            | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c);
   3.109          val is_undefined = name_of #> equal (SOME @{const_name undefined});
   3.110          fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body);
   3.111 +        val tab = Datatype_Data.info_of_case (Proof_Context.theory_of ctxt);
   3.112        in
   3.113          (case ty_info tab cname of
   3.114            SOME {constructors, case_name} =>
   3.115 @@ -409,9 +412,10 @@
   3.116  
   3.117  (* print translation *)
   3.118  
   3.119 -fun case_tr' tab_of cname ctxt ts =
   3.120 +fun case_tr' cname ctxt ts =
   3.121    let
   3.122      val thy = Proof_Context.theory_of ctxt;
   3.123 +
   3.124      fun mk_clause (pat, rhs) =
   3.125        let val xs = Term.add_frees pat [] in
   3.126          Syntax.const @{syntax_const "_case1"} $
   3.127 @@ -424,7 +428,7 @@
   3.128                | t => t) rhs
   3.129        end;
   3.130    in
   3.131 -    (case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
   3.132 +    (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
   3.133        SOME (x, clauses) =>
   3.134          Syntax.const @{syntax_const "_case_syntax"} $ x $
   3.135            foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
   3.136 @@ -432,4 +436,15 @@
   3.137      | NONE => raise Match)
   3.138    end;
   3.139  
   3.140 +fun add_case_tr' case_names thy =
   3.141 +  Sign.add_advanced_trfuns ([], [],
   3.142 +    map (fn case_name =>
   3.143 +      let val case_name' = Lexicon.mark_const case_name
   3.144 +      in (case_name', case_tr' case_name') end) case_names, []) thy;
   3.145 +
   3.146 +
   3.147 +(* theory setup *)
   3.148 +
   3.149 +val setup = trfun_setup;
   3.150 +
   3.151  end;
     4.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Dec 15 17:37:14 2011 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Dec 15 18:08:40 2011 +0100
     4.3 @@ -24,10 +24,6 @@
     4.4    val mk_case_names_exhausts: descr -> string list -> attribute list
     4.5    val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
     4.6    val interpretation_data : config * string list -> theory -> theory
     4.7 -  val make_case :  Proof.context -> Datatype_Case.config -> string list -> term ->
     4.8 -    (term * term) list -> term
     4.9 -  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    4.10 -  val add_case_tr' : string list -> theory -> theory
    4.11    val setup: theory -> theory
    4.12  end;
    4.13  
    4.14 @@ -198,27 +194,6 @@
    4.15  end;
    4.16  
    4.17  
    4.18 -(* translation rules for case *)
    4.19 -
    4.20 -fun make_case ctxt =
    4.21 -  Datatype_Case.make_case (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt;
    4.22 -
    4.23 -fun strip_case ctxt =
    4.24 -  Datatype_Case.strip_case (info_of_case (Proof_Context.theory_of ctxt));
    4.25 -
    4.26 -fun add_case_tr' case_names thy =
    4.27 -  Sign.add_advanced_trfuns ([], [],
    4.28 -    map (fn case_name =>
    4.29 -      let val case_name' = Lexicon.mark_const case_name in
    4.30 -        (case_name', Datatype_Case.case_tr' info_of_case case_name')
    4.31 -      end) case_names, []) thy;
    4.32 -
    4.33 -val trfun_setup =
    4.34 -  Sign.add_advanced_trfuns ([],
    4.35 -    [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr_permissive)],
    4.36 -    [], []);
    4.37 -
    4.38 -
    4.39  
    4.40  (** document antiquotation **)
    4.41  
    4.42 @@ -262,7 +237,6 @@
    4.43  (** setup theory **)
    4.44  
    4.45  val setup =
    4.46 -  trfun_setup #>
    4.47    antiq_setup #>
    4.48    Datatype_Interpretation.init;
    4.49  
     5.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Dec 15 17:37:14 2011 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Dec 15 18:08:40 2011 +0100
     5.3 @@ -99,9 +99,9 @@
     5.4          ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
     5.5            named_rules @ unnamed_rules)
     5.6      |> snd
     5.7 -    |> Datatype_Data.add_case_tr' case_names
     5.8      |> Datatype_Data.register dt_infos
     5.9      |> Datatype_Data.interpretation_data (config, dt_names)
    5.10 +    |> Datatype_Case.add_case_tr' case_names
    5.11      |> pair dt_names
    5.12    end;
    5.13  
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Dec 15 17:37:14 2011 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Dec 15 18:08:40 2011 +0100
     6.3 @@ -663,7 +663,7 @@
     6.4      val v = Free (name, T);
     6.5      val v' = Free (name', T);
     6.6    in
     6.7 -    lambda v (Datatype.make_case ctxt Datatype_Case.Quiet [] v
     6.8 +    lambda v (Datatype_Case.make_case ctxt Datatype_Case.Quiet [] v
     6.9        [(HOLogic.mk_tuple out_ts,
    6.10          if null eqs'' then success_t
    6.11          else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
    6.12 @@ -949,7 +949,7 @@
    6.13          in
    6.14            (pattern, compilation)
    6.15          end
    6.16 -        val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
    6.17 +        val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet [] inp_var
    6.18            ((map compile_single_case switched_clauses) @
    6.19              [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
    6.20        in
     7.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 15 17:37:14 2011 +0100
     7.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 15 18:08:40 2011 +0100
     7.3 @@ -412,7 +412,7 @@
     7.4    end
     7.5  
     7.6  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
     7.7 -    Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
     7.8 +    Datatype_Case.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
     7.9        (t, mk_case_term ctxt (p - 1) qs' c)) cs)
    7.10    | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
    7.11      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c