src/HOL/Tools/Ctr_Sugar/case_translation.ML
author wenzelm
Wed, 02 Apr 2014 13:53:32 +0200
changeset 56362 720414857a12
parent 56241 029246729dc0
child 57445 2d0cf40f6fb3
permissions -rw-r--r--
tuned whitespace;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54701
4ed7454aebde tuning -- moved ML files to subdirectory
blanchet
parents: 54398
diff changeset
     1
(*  Title:      HOL/Tools/Ctr_Sugar/case_translation.ML
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
     2
    Author:     Konrad Slind, Cambridge University Computer Laboratory
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
     4
    Author:     Dmitriy Traytel, TU Muenchen
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
     5
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
     6
Nested case expressions via a generic data slot for case combinators and constructors.
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
     7
*)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
     8
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
     9
signature CASE_TRANSLATION =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    10
sig
54398
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    11
  val indexify_names: string list -> string list
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    12
  val make_tnames: typ list -> string list
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    13
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    14
  datatype config = Error | Warning | Quiet
51678
1e33b81c328a allow redundant cases in the list comprehension translation
traytel
parents: 51677
diff changeset
    15
  val case_tr: bool -> Proof.context -> term list -> term
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    16
  val lookup_by_constr: Proof.context -> string * typ -> (term * term list) option
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    17
  val lookup_by_constr_permissive: Proof.context -> string * typ -> (term * term list) option
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    18
  val lookup_by_case: Proof.context -> string -> (term * term list) option
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    19
  val make_case:  Proof.context -> config -> Name.context -> term -> (term * term) list -> term
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    20
  val print_case_translations: Proof.context -> unit
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
    21
  val strip_case: Proof.context -> bool -> term -> (term * (term * term) list) option
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
    22
  val strip_case_full: Proof.context -> bool -> term -> term
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    23
  val show_cases: bool Config.T
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    24
  val register: term -> term list -> Context.generic -> Context.generic
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    25
end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    26
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    27
structure Case_Translation: CASE_TRANSLATION =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    28
struct
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    29
54398
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    30
(** general utilities **)
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    31
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    32
fun indexify_names names =
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    33
  let
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    34
    fun index (x :: xs) tab =
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    35
        (case AList.lookup (op =) tab x of
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    36
          NONE =>
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    37
            if member (op =) xs x
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    38
            then (x ^ "1") :: index xs ((x, 2) :: tab)
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    39
            else x :: index xs tab
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    40
        | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    41
      | index [] _ = [];
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    42
  in index names [] end;
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    43
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    44
fun make_tnames Ts =
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    45
  let
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    46
    fun type_name (TFree (name, _)) = unprefix "'" name
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    47
      | type_name (Type (name, _)) =
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    48
          let val name' = Long_Name.base_name name
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    49
          in if Symbol_Pos.is_identifier name' then name' else "x" end;
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    50
  in indexify_names (map type_name Ts) end;
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    51
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    52
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
    53
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    54
(** data management **)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    55
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    56
datatype data = Data of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    57
  {constrs: (string * (term * term list)) list Symtab.table,
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    58
   cases: (term * term list) Symtab.table};
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    59
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    60
fun make_data (constrs, cases) = Data {constrs = constrs, cases = cases};
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    61
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    62
structure Data = Generic_Data
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    63
(
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    64
  type T = data;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    65
  val empty = make_data (Symtab.empty, Symtab.empty);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    66
  val extend = I;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    67
  fun merge
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    68
    (Data {constrs = constrs1, cases = cases1},
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    69
     Data {constrs = constrs2, cases = cases2}) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    70
    make_data
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    71
      (Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    72
      Symtab.merge (K true) (cases1, cases2));
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    73
);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    74
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    75
fun map_data f =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    76
  Data.map (fn Data {constrs, cases} => make_data (f (constrs, cases)));
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    77
fun map_constrs f = map_data (fn (constrs, cases) => (f constrs, cases));
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    78
fun map_cases f = map_data (fn (constrs, cases) => (constrs, f cases));
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    79
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    80
val rep_data = (fn Data args => args) o Data.get o Context.Proof;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    81
51684
0b5497bdaddf made SML/NJ happy
traytel
parents: 51681
diff changeset
    82
fun T_of_data (comb, constrs : term list) =
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    83
  fastype_of comb
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    84
  |> funpow (length constrs) range_type
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    85
  |> domain_type;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    86
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    87
val Tname_of_data = fst o dest_Type o T_of_data;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    88
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    89
val constrs_of = #constrs o rep_data;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    90
val cases_of = #cases o rep_data;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    91
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    92
fun lookup_by_constr ctxt (c, T) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    93
  let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    94
    val tab = Symtab.lookup_list (constrs_of ctxt) c;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    95
  in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    96
    (case body_type T of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    97
      Type (tyco, _) => AList.lookup (op =) tab tyco
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    98
    | _ => NONE)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
    99
  end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   100
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   101
fun lookup_by_constr_permissive ctxt (c, T) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   102
  let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   103
    val tab = Symtab.lookup_list (constrs_of ctxt) c;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   104
    val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   105
    val default = if null tab then NONE else SOME (snd (List.last tab));
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   106
    (*conservative wrt. overloaded constructors*)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   107
  in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   108
    (case hint of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   109
      NONE => default
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   110
    | SOME tyco =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   111
        (case AList.lookup (op =) tab tyco of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   112
          NONE => default (*permissive*)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   113
        | SOME info => SOME info))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   114
  end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   115
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   116
val lookup_by_case = Symtab.lookup o cases_of;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   117
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   118
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   119
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   120
(** installation **)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   121
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   122
fun case_error s = error ("Error in case expression:\n" ^ s);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   123
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   124
val name_of = try (dest_Const #> fst);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   125
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   126
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   127
(* parse translation *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   128
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   129
fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   130
51678
1e33b81c328a allow redundant cases in the list comprehension translation
traytel
parents: 51677
diff changeset
   131
fun case_tr err ctxt [t, u] =
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   132
      let
52157
ba6b2876ef5a more uniform context;
wenzelm
parents: 52155
diff changeset
   133
        val consts = Proof_Context.consts_of ctxt;
ba6b2876ef5a more uniform context;
wenzelm
parents: 52155
diff changeset
   134
        fun is_const s = can (Consts.the_constraint consts) (Consts.intern consts s);
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   135
52158
d5fa81343322 more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents: 52157
diff changeset
   136
        fun variant_free x used =
d5fa81343322 more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents: 52157
diff changeset
   137
          let val (x', used') = Name.variant x used
d5fa81343322 more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents: 52157
diff changeset
   138
          in if is_const x' then variant_free x' used' else (x', used') end;
d5fa81343322 more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents: 52157
diff changeset
   139
52157
ba6b2876ef5a more uniform context;
wenzelm
parents: 52155
diff changeset
   140
        fun abs p tTs t =
ba6b2876ef5a more uniform context;
wenzelm
parents: 52155
diff changeset
   141
          Syntax.const @{const_syntax case_abs} $
ba6b2876ef5a more uniform context;
wenzelm
parents: 52155
diff changeset
   142
            fold constrain_Abs tTs (absfree p t);
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   143
51693
1eb533ea1480 more antiquotations;
wenzelm
parents: 51692
diff changeset
   144
        fun abs_pat (Const (@{syntax_const "_constrain"}, _) $ t $ tT) tTs =
1eb533ea1480 more antiquotations;
wenzelm
parents: 51692
diff changeset
   145
              abs_pat t (tT :: tTs)
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   146
          | abs_pat (Free (p as (x, _))) tTs =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   147
              if is_const x then I else abs p tTs
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   148
          | abs_pat (t $ u) _ = abs_pat u [] #> abs_pat t []
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   149
          | abs_pat _ _ = I;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   150
51680
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   151
        (* replace occurrences of dummy_pattern by distinct variables *)
56241
029246729dc0 more qualified names;
wenzelm
parents: 55974
diff changeset
   152
        fun replace_dummies (Const (@{const_syntax Pure.dummy_pattern}, T)) used =
52158
d5fa81343322 more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents: 52157
diff changeset
   153
              let val (x, used') = variant_free "x" used
51680
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   154
              in (Free (x, T), used') end
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   155
          | replace_dummies (t $ u) used =
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   156
              let
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   157
                val (t', used') = replace_dummies t used;
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   158
                val (u', used'') = replace_dummies u used';
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   159
              in (t' $ u', used'') end
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   160
          | replace_dummies t used = (t, used);
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   161
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   162
        fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   163
              let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context) in
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   164
                abs_pat l' []
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   165
                  (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l' $ r)
51680
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   166
              end
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   167
          | dest_case1 _ = case_error "dest_case1";
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   168
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   169
        fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   170
          | dest_case2 t = [t];
51678
1e33b81c328a allow redundant cases in the list comprehension translation
traytel
parents: 51677
diff changeset
   171
55974
c835a9379026 more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
wenzelm
parents: 55971
diff changeset
   172
        val errt = Syntax.const (if err then @{const_syntax True} else @{const_syntax False});
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   173
      in
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   174
        Syntax.const @{const_syntax case_guard} $ errt $ t $
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   175
          (fold_rev
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   176
            (fn t => fn u => Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   177
            (dest_case2 u)
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   178
            (Syntax.const @{const_syntax case_nil}))
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   179
      end
51678
1e33b81c328a allow redundant cases in the list comprehension translation
traytel
parents: 51677
diff changeset
   180
  | case_tr _ _ _ = case_error "case_tr";
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   181
55971
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   182
val _ = Theory.setup (Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)]);
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   183
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   184
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   185
(* print translation *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   186
51751
cf039b3c42a7 slightly more aggressive syntax translation for printing case expressions
traytel
parents: 51693
diff changeset
   187
fun case_tr' (_ :: x :: t :: ts) =
52159
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   188
      let
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   189
        fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used =
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   190
              let val (s', used') = Name.variant s used
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   191
              in mk_clause t ((s', T) :: xs) used' end
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   192
          | mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ =
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   193
              Syntax.const @{syntax_const "_case1"} $
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   194
                subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   195
                subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs)
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   196
          | mk_clause _ _ _ = raise Match;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   197
52159
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   198
        fun mk_clauses (Const (@{const_syntax case_nil}, _)) = []
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   199
          | mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) =
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   200
              mk_clause t [] (Term.declare_term_frees t Name.context) :: mk_clauses u
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   201
          | mk_clauses _ = raise Match;
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   202
      in
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   203
        list_comb (Syntax.const @{syntax_const "_case_syntax"} $ x $
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   204
          foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   205
            (mk_clauses t), ts)
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   206
      end
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   207
  | case_tr' _ = raise Match;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   208
55971
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   209
val _ = Theory.setup (Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')]);
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   210
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   211
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   212
(* declarations *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   213
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   214
fun register raw_case_comb raw_constrs context =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   215
  let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   216
    val ctxt = Context.proof_of context;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   217
    val case_comb = singleton (Variable.polymorphic ctxt) raw_case_comb;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   218
    val constrs = Variable.polymorphic ctxt raw_constrs;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   219
    val case_key = case_comb |> dest_Const |> fst;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   220
    val constr_keys = map (fst o dest_Const) constrs;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   221
    val data = (case_comb, constrs);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   222
    val Tname = Tname_of_data data;
55444
ec73f81e49e7 iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents: 55392
diff changeset
   223
    val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys;
ec73f81e49e7 iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents: 55392
diff changeset
   224
    val update_cases = Symtab.update (case_key, data);
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   225
  in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   226
    context
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   227
    |> map_constrs update_constrs
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   228
    |> map_cases update_cases
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   229
  end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   230
55971
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   231
val _ = Theory.setup
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   232
  (Attrib.setup @{binding case_translation}
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   233
    (Args.term -- Scan.repeat1 Args.term >>
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   234
      (fn (t, ts) => Thm.declaration_attribute (K (register t ts))))
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   235
    "declaration of case combinators and constructors");
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   236
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   237
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   238
(* (Un)check phases *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   239
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   240
datatype config = Error | Warning | Quiet;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   241
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   242
exception CASE_ERROR of string * int;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   243
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   244
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   245
(*Each pattern carries with it a tag i, which denotes the clause it
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   246
  came from. i = ~1 indicates that the clause was added by pattern
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   247
  completion.*)
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   248
52159
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   249
fun add_row_used ((prfx, pats), (tm, _)) =
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   250
  fold Term.declare_term_frees (tm :: pats @ map Free prfx);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   251
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   252
(*try to preserve names given by user*)
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   253
fun default_name "" (Free (name', _)) = name'
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   254
  | default_name name _ = name;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   255
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   256
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   257
(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
51675
18bbc78888aa Use Type.raw_match instead of Sign.typ_match
berghofe
parents: 51674
diff changeset
   258
fun fresh_constr colty used c =
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   259
  let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   260
    val (_, T) = dest_Const c;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   261
    val Ts = binder_types T;
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   262
    val (names, _) =
54398
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52705
diff changeset
   263
      fold_map Name.variant (make_tnames (map Logic.unvarifyT_global Ts)) used;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   264
    val ty = body_type T;
51675
18bbc78888aa Use Type.raw_match instead of Sign.typ_match
berghofe
parents: 51674
diff changeset
   265
    val ty_theta = Type.raw_match (ty, colty) Vartab.empty
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   266
      handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   267
    val c' = Envir.subst_term_types ty_theta c;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   268
    val gvars = map (Envir.subst_term_types ty_theta o Free) (names ~~ Ts);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   269
  in (c', gvars) end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   270
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   271
(*Go through a list of rows and pick out the ones beginning with a
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   272
  pattern with constructor = name.*)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   273
fun mk_group (name, T) rows =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   274
  let val k = length (binder_types T) in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   275
    fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   276
      fn ((in_group, not_in_group), names) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   277
        (case strip_comb p of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   278
          (Const (name', _), args) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   279
            if name = name' then
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   280
              if length args = k then
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   281
                ((((prfx, args @ ps), rhs) :: in_group, not_in_group),
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   282
                 map2 default_name names args)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   283
              else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   284
            else ((in_group, row :: not_in_group), names)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   285
        | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   286
    rows (([], []), replicate k "") |>> pairself rev
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   287
  end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   288
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   289
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   290
(* Partitioning *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   291
51675
18bbc78888aa Use Type.raw_match instead of Sign.typ_match
berghofe
parents: 51674
diff changeset
   292
fun partition _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   293
  | partition used constructors colty res_ty (rows as (((prfx, _ :: ps), _) :: _)) =
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   294
      let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   295
        fun part [] [] = []
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   296
          | part [] ((_, (_, i)) :: _) = raise CASE_ERROR ("Not a constructor pattern", i)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   297
          | part (c :: cs) rows =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   298
              let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   299
                val ((in_group, not_in_group), names) = mk_group (dest_Const c) rows;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   300
                val used' = fold add_row_used in_group used;
51675
18bbc78888aa Use Type.raw_match instead of Sign.typ_match
berghofe
parents: 51674
diff changeset
   301
                val (c', gvars) = fresh_constr colty used' c;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   302
                val in_group' =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   303
                  if null in_group  (* Constructor not given *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   304
                  then
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   305
                    let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   306
                      val Ts = map fastype_of ps;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   307
                      val (xs, _) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   308
                        fold_map Name.variant
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   309
                          (replicate (length ps) "x")
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   310
                          (fold Term.declare_term_frees gvars used');
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   311
                    in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   312
                      [((prfx, gvars @ map Free (xs ~~ Ts)),
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   313
                        (Const (@{const_name undefined}, res_ty), ~1))]
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   314
                    end
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   315
                  else in_group;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   316
              in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   317
                {constructor = c',
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   318
                 new_formals = gvars,
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   319
                 names = names,
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   320
                 group = in_group'} :: part cs not_in_group
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   321
              end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   322
      in part constructors rows end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   323
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   324
fun v_to_prfx (prfx, Free v :: pats) = (v :: prfx, pats)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   325
  | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   326
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   327
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   328
(* Translation of pattern terms into nested case expressions. *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   329
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   330
fun mk_case ctxt used range_ty =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   331
  let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   332
    val get_info = lookup_by_constr_permissive ctxt;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   333
52159
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   334
    fun expand _ _ _ ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   335
      | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   336
          if is_Free p then
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   337
            let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   338
              val used' = add_row_used row used;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   339
              fun expnd c =
51675
18bbc78888aa Use Type.raw_match instead of Sign.typ_match
berghofe
parents: 51674
diff changeset
   340
                let val capp = list_comb (fresh_constr ty used' c)
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   341
                in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   342
            in map expnd constructors end
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   343
          else [row];
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   344
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   345
    val (name, _) = Name.variant "a" used;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   346
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   347
    fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   348
      | mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
52159
432e29ff9f14 tuned -- less ML compiler warnings;
wenzelm
parents: 52158
diff changeset
   349
      | mk path ((row as ((_, [Free _]), _)) :: _ :: _) = mk path [row]
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   350
      | mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   351
          let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   352
            (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   353
              NONE =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   354
                let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   355
                  val rows' = map (fn ((v, _), row) => row ||>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   356
                    apfst (subst_free [(v, u)]) |>> v_to_prfx) (col0 ~~ rows);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   357
                in mk us rows' end
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   358
            | SOME (Const (cname, cT), i) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   359
                (case get_info (cname, cT) of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   360
                  NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ quote cname, i)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   361
                | SOME (case_comb, constructors) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   362
                    let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   363
                      val pty = body_type cT;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   364
                      val used' = fold Term.declare_term_frees us used;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   365
                      val nrows = maps (expand constructors used' pty) rows;
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   366
                      val subproblems = partition used' constructors pty range_ty nrows;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   367
                      val (pat_rect, dtrees) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   368
                        split_list (map (fn {new_formals, group, ...} =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   369
                          mk (new_formals @ us) group) subproblems);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   370
                      val case_functions =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   371
                        map2 (fn {new_formals, names, ...} =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   372
                          fold_rev (fn (x as Free (_, T), s) => fn t =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   373
                            Abs (if s = "" then name else s, T, abstract_over (x, t)))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   374
                              (new_formals ~~ names))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   375
                        subproblems dtrees;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   376
                      val types = map fastype_of (case_functions @ [u]);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   377
                      val case_const = Const (name_of case_comb |> the, types ---> range_ty);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   378
                      val tree = list_comb (case_const, case_functions @ [u]);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   379
                    in (flat pat_rect, tree) end)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   380
            | SOME (t, i) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   381
                raise CASE_ERROR ("Not a datatype constructor: " ^ Syntax.string_of_term ctxt t, i))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   382
          end
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   383
      | mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   384
  in mk end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   385
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   386
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   387
(*Repeated variable occurrences in a pattern are not allowed.*)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   388
fun no_repeat_vars ctxt pat = fold_aterms
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   389
  (fn x as Free (s, _) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   390
      (fn xs =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   391
        if member op aconv xs x then
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   392
          case_error (quote s ^ " occurs repeatedly in the pattern " ^
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   393
            quote (Syntax.string_of_term ctxt pat))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   394
        else x :: xs)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   395
    | _ => I) pat [];
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   396
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   397
fun make_case ctxt config used x clauses =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   398
  let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   399
    fun string_of_clause (pat, rhs) =
52705
c12602c1b13b do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)
traytel
parents: 52690
diff changeset
   400
      Syntax.unparse_term ctxt
c12602c1b13b do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)
traytel
parents: 52690
diff changeset
   401
        (Term.list_comb (Syntax.const @{syntax_const "_case1"},
c12602c1b13b do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)
traytel
parents: 52690
diff changeset
   402
          Syntax.uncheck_terms ctxt [pat, rhs]))
c12602c1b13b do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)
traytel
parents: 52690
diff changeset
   403
      |> Pretty.string_of;
52690
2fa3110539a5 more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);
wenzelm
parents: 52685
diff changeset
   404
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   405
    val _ = map (no_repeat_vars ctxt o fst) clauses;
51680
8b8cd5a527bc Handle dummy patterns in parse translation rather than check phase
berghofe
parents: 51679
diff changeset
   406
    val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   407
    val rangeT =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   408
      (case distinct (op =) (map (fastype_of o snd) clauses) of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   409
        [] => case_error "no clauses given"
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   410
      | [T] => T
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   411
      | _ => case_error "all cases must have the same result type");
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   412
    val used' = fold add_row_used rows used;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   413
    val (tags, case_tm) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   414
      mk_case ctxt used' rangeT [x] rows
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   415
        handle CASE_ERROR (msg, i) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   416
          case_error
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   417
            (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   418
    val _ =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   419
      (case subtract (op =) tags (map (snd o snd) rows) of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   420
        [] => ()
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   421
      | is =>
52685
554d684d8520 non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
wenzelm
parents: 52285
diff changeset
   422
          if config = Quiet then ()
554d684d8520 non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
wenzelm
parents: 52285
diff changeset
   423
          else
52690
2fa3110539a5 more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);
wenzelm
parents: 52685
diff changeset
   424
            (if config = Error then case_error else warning (*FIXME lack of syntactic context!?*))
52685
554d684d8520 non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
wenzelm
parents: 52285
diff changeset
   425
              ("The following clauses are redundant (covered by preceding clauses):\n" ^
554d684d8520 non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
wenzelm
parents: 52285
diff changeset
   426
                cat_lines (map (string_of_clause o nth clauses) is)));
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   427
  in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   428
    case_tm
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   429
  end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   430
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   431
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   432
(* term check *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   433
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   434
fun decode_clause (Const (@{const_name case_abs}, _) $ Abs (s, T, t)) xs used =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   435
      let val (s', used') = Name.variant s used
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   436
      in decode_clause t (Free (s', T) :: xs) used' end
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   437
  | decode_clause (Const (@{const_name case_elem}, _) $ t $ u) xs _ =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   438
      (subst_bounds (xs, t), subst_bounds (xs, u))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   439
  | decode_clause _ _ _ = case_error "decode_clause";
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   440
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   441
fun decode_cases (Const (@{const_name case_nil}, _)) = []
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   442
  | decode_cases (Const (@{const_name case_cons}, _) $ t $ u) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   443
      decode_clause t [] (Term.declare_term_frees t Name.context) ::
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   444
      decode_cases u
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   445
  | decode_cases _ = case_error "decode_cases";
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   446
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   447
fun check_case ctxt =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   448
  let
51679
e7316560928b disallow coercions to interfere with case translations
traytel
parents: 51678
diff changeset
   449
    fun decode_case (Const (@{const_name case_guard}, _) $ b $ u $ t) =
51678
1e33b81c328a allow redundant cases in the list comprehension translation
traytel
parents: 51677
diff changeset
   450
          make_case ctxt (if b = @{term True} then Error else Warning)
1e33b81c328a allow redundant cases in the list comprehension translation
traytel
parents: 51677
diff changeset
   451
            Name.context (decode_case u) (decode_cases t)
51676
d602caf11e48 tuned whitespace
traytel
parents: 51675
diff changeset
   452
      | decode_case (t $ u) = decode_case t $ decode_case u
d602caf11e48 tuned whitespace
traytel
parents: 51675
diff changeset
   453
      | decode_case (Abs (x, T, u)) =
d602caf11e48 tuned whitespace
traytel
parents: 51675
diff changeset
   454
          let val (x', u') = Term.dest_abs (x, T, u);
d602caf11e48 tuned whitespace
traytel
parents: 51675
diff changeset
   455
          in Term.absfree (x', T) (decode_case u') end
d602caf11e48 tuned whitespace
traytel
parents: 51675
diff changeset
   456
      | decode_case t = t;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   457
  in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   458
    map decode_case
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   459
  end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   460
55971
7644d63e8c3f modernized theory setup;
wenzelm
parents: 55444
diff changeset
   461
val _ = Context.>> (Syntax_Phases.term_check 1 "case" check_case);
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   462
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   463
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   464
(* Pretty printing of nested case expressions *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   465
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   466
(* destruct one level of pattern matching *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   467
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   468
fun dest_case ctxt d used t =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   469
  (case apfst name_of (strip_comb t) of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   470
    (SOME cname, ts as _ :: _) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   471
      let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   472
        val (fs, x) = split_last ts;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   473
        fun strip_abs i Us t =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   474
          let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   475
            val zs = strip_abs_vars t;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   476
            val j = length zs;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   477
            val (xs, ys) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   478
              if j < i then (zs @ map (pair "x") (drop j Us), [])
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   479
              else chop i zs;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   480
            val u = fold_rev Term.abs ys (strip_abs_body t);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   481
            val xs' = map Free
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   482
              ((fold_map Name.variant (map fst xs)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   483
                  (Term.declare_term_names u used) |> fst) ~~
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   484
               map snd xs);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   485
            val (xs1, xs2) = chop j xs'
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   486
          in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   487
        fun is_dependent i t =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   488
          let val k = length (strip_abs_vars t) - i
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   489
          in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   490
        fun count_cases (_, _, true) = I
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   491
          | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   492
        val is_undefined = name_of #> equal (SOME @{const_name undefined});
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   493
        fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   494
        val get_info = lookup_by_case ctxt;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   495
      in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   496
        (case get_info cname of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   497
          SOME (_, constructors) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   498
            if length fs = length constructors then
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   499
              let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   500
                val cases = map (fn (Const (s, U), t) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   501
                  let
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   502
                    val Us = binder_types U;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   503
                    val k = length Us;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   504
                    val p as (xs, _) = strip_abs k Us t;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   505
                  in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   506
                    (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   507
                  end) (constructors ~~ fs);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   508
                val cases' =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   509
                  sort (int_ord o swap o pairself (length o snd))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   510
                    (fold_rev count_cases cases []);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   511
                val R = fastype_of t;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   512
                val dummy =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   513
                  if d then Term.dummy_pattern R
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   514
                  else Free (Name.variant "x" used |> fst, R);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   515
              in
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   516
                SOME (x,
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   517
                  map mk_case
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   518
                    (case find_first (is_undefined o fst) cases' of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   519
                      SOME (_, cs) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   520
                        if length cs = length constructors then [hd cases]
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   521
                        else filter_out (fn (_, (_, body), _) => is_undefined body) cases
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   522
                    | NONE =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   523
                        (case cases' of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   524
                          [] => cases
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   525
                        | (default, cs) :: _ =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   526
                            if length cs = 1 then cases
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   527
                            else if length cs = length constructors then
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   528
                              [hd cases, (dummy, ([], default), false)]
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   529
                            else
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   530
                              filter_out (fn (c, _, _) => member op aconv cs c) cases @
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   531
                                [(dummy, ([], default), false)])))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   532
              end
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   533
            else NONE
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   534
        | _ => NONE)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   535
      end
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   536
  | _ => NONE);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   537
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   538
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   539
(* destruct nested patterns *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   540
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   541
fun encode_clause recur S T (pat, rhs) =
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   542
  fold (fn x as (_, U) => fn t =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   543
    Const (@{const_name case_abs}, (U --> T) --> T) $ Term.absfree x t)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   544
      (Term.add_frees pat [])
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   545
      (Const (@{const_name case_elem}, S --> T --> S --> T) $ pat $ recur rhs);
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   546
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   547
fun encode_cases _ S T [] = Const (@{const_name case_nil}, S --> T)
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   548
  | encode_cases recur S T (p :: ps) =
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   549
      Const (@{const_name case_cons}, (S --> T) --> (S --> T) --> S --> T) $
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   550
        encode_clause recur S T p $ encode_cases recur S T ps;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   551
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   552
fun encode_case recur (t, ps as (pat, rhs) :: _) =
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   553
      let
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   554
        val tT = fastype_of t;
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   555
        val T = fastype_of rhs;
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   556
      in
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   557
        Const (@{const_name case_guard}, @{typ bool} --> tT --> (tT --> T) --> T) $
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   558
          @{term True} $ t $ (encode_cases recur (fastype_of pat) (fastype_of rhs) ps)
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   559
      end
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   560
  | encode_case _ _ = case_error "encode_case";
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   561
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   562
fun strip_case' ctxt d (pat, rhs) =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   563
  (case dest_case ctxt d (Term.declare_term_frees pat Name.context) rhs of
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   564
    SOME (exp as Free _, clauses) =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   565
      if Term.exists_subterm (curry (op aconv) exp) pat andalso
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   566
        not (exists (fn (_, rhs') =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   567
          Term.exists_subterm (curry (op aconv) exp) rhs') clauses)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   568
      then
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   569
        maps (strip_case' ctxt d) (map (fn (pat', rhs') =>
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   570
          (subst_free [(exp, pat')] pat, rhs')) clauses)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   571
      else [(pat, rhs)]
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   572
  | _ => [(pat, rhs)]);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   573
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   574
fun strip_case ctxt d t =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   575
  (case dest_case ctxt d Name.context t of
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   576
    SOME (x, clauses) => SOME (x, maps (strip_case' ctxt d) clauses)
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   577
  | NONE => NONE);
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   578
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   579
fun strip_case_full ctxt d t =
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   580
  (case dest_case ctxt d Name.context t of
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   581
    SOME (x, clauses) =>
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   582
      encode_case (strip_case_full ctxt d)
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   583
        (strip_case_full ctxt d x, maps (strip_case' ctxt d) clauses)
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   584
  | NONE =>
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   585
      (case t of
52154
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   586
        t $ u => strip_case_full ctxt d t $ strip_case_full ctxt d u
b707a26d8fe0 tuned white-space;
wenzelm
parents: 52143
diff changeset
   587
      | Abs (x, T, u) =>
51677
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   588
          let val (x', u') = Term.dest_abs (x, T, u);
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   589
          in Term.absfree (x', T) (strip_case_full ctxt d u') end
d2b3372e6033 recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents: 51676
diff changeset
   590
      | _ => t));
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   591
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   592
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   593
(* term uncheck *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   594
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   595
val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   596
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   597
fun uncheck_case ctxt ts =
52285
da42b500a6aa permissive uncheck -- allow printing of malformed terms (e.g. in error messages);
wenzelm
parents: 52265
diff changeset
   598
  if Config.get ctxt show_cases
da42b500a6aa permissive uncheck -- allow printing of malformed terms (e.g. in error messages);
wenzelm
parents: 52265
diff changeset
   599
  then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts
da42b500a6aa permissive uncheck -- allow printing of malformed terms (e.g. in error messages);
wenzelm
parents: 52265
diff changeset
   600
  else ts;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   601
56362
720414857a12 tuned whitespace;
wenzelm
parents: 56241
diff changeset
   602
val _ = Context.>> (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   603
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   604
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   605
(* outer syntax commands *)
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   606
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   607
fun print_case_translations ctxt =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   608
  let
52155
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   609
    val cases = map snd (Symtab.dest (cases_of ctxt));
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   610
    val type_space = Proof_Context.type_space ctxt;
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   611
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   612
    val pretty_term = Syntax.pretty_term ctxt;
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   613
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   614
    fun pretty_data (data as (comb, ctrs)) =
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   615
      let
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   616
        val name = Tname_of_data data;
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   617
        val xname = Name_Space.extern ctxt type_space name;
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   618
        val markup = Name_Space.markup type_space name;
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   619
        val prt =
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   620
          (Pretty.block o Pretty.fbreaks)
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   621
           [Pretty.block [Pretty.mark_str (markup, xname), Pretty.str ":"],
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   622
            Pretty.block [Pretty.str "combinator:", Pretty.brk 1, pretty_term comb],
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   623
            Pretty.block (Pretty.str "constructors:" :: Pretty.brk 1 ::
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   624
              Pretty.commas (map pretty_term ctrs))];
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   625
      in (xname, prt) end;
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   626
  in
52155
761c325a65d4 more conventional pretty printing;
wenzelm
parents: 52154
diff changeset
   627
    Pretty.big_list "case translations:" (map #2 (sort_wrt #1 (map pretty_data cases)))
51673
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   628
    |> Pretty.writeln
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   629
  end;
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   630
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   631
val _ =
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   632
  Outer_Syntax.improper_command @{command_spec "print_case_translations"}
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   633
    "print registered case combinators and constructors"
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   634
    (Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   635
4dfa00e264d8 separate data used for case translation from the datatype package
traytel
parents:
diff changeset
   636
end;