src/HOL/Tools/datatype_case.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29623 1219985d24b5
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Tools/datatype_case.ML
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
     2
    Author:     Konrad Slind, Cambridge University Computer Laboratory
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 26931
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
     4
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
     5
Nested case expressions on datatypes.
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
     6
*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
     7
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
     8
signature DATATYPE_CASE =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
     9
sig
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    10
  val make_case: (string -> DatatypeAux.datatype_info option) ->
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    11
    Proof.context -> bool -> string list -> term -> (term * term) list ->
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    12
    term * (term * (int * bool)) list
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    13
  val dest_case: (string -> DatatypeAux.datatype_info option) -> bool ->
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    14
    string list -> term -> (term * (term * term) list) option
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    15
  val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    16
    term -> (term * (term * term) list) option
24349
0dd8782fb02d Final mods for list comprehension
nipkow
parents: 22779
diff changeset
    17
  val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
0dd8782fb02d Final mods for list comprehension
nipkow
parents: 22779
diff changeset
    18
    -> Proof.context -> term list -> term
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    19
  val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    20
    string -> Proof.context -> term list -> term
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    21
end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    22
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    23
structure DatatypeCase : DATATYPE_CASE =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    24
struct
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    25
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    26
exception CASE_ERROR of string * int;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    27
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    28
fun match_type thy pat ob = Sign.typ_match thy (pat, ob) Vartab.empty;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    29
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    30
(*---------------------------------------------------------------------------
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    31
 * Get information about datatypes
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    32
 *---------------------------------------------------------------------------*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    33
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    34
fun ty_info (tab : string -> DatatypeAux.datatype_info option) s =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    35
  case tab s of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    36
    SOME {descr, case_name, index, sorts, ...} =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    37
      let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    38
        val (_, (tname, dts, constrs)) = nth descr index;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    39
        val mk_ty = DatatypeAux.typ_of_dtyp descr sorts;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    40
        val T = Type (tname, map mk_ty dts)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    41
      in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    42
        SOME {case_name = case_name,
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    43
          constructors = map (fn (cname, dts') =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    44
            Const (cname, Logic.varifyT (map mk_ty dts' ---> T))) constrs}
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    45
      end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    46
  | NONE => NONE;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    47
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    48
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    49
(*---------------------------------------------------------------------------
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    50
 * Each pattern carries with it a tag (i,b) where
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    51
 * i is the clause it came from and
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    52
 * b=true indicates that clause was given by the user
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    53
 * (or is an instantiation of a user supplied pattern)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    54
 * b=false --> i = ~1
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    55
 *---------------------------------------------------------------------------*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    56
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
    57
fun pattern_subst theta (tm, x) = (subst_free theta tm, x);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    58
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    59
fun row_of_pat x = fst (snd x);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    60
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
    61
fun add_row_used ((prfx, pats), (tm, tag)) =
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
    62
  fold Term.add_free_names (tm :: pats @ prfx);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    63
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    64
(* try to preserve names given by user *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    65
fun default_names names ts =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    66
  map (fn ("", Free (name', _)) => name' | (name, _) => name) (names ~~ ts);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    67
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    68
fun strip_constraints (Const ("_constrain", _) $ t $ tT) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    69
      strip_constraints t ||> cons tT
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    70
  | strip_constraints t = (t, []);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    71
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    72
fun mk_fun_constrain tT t = Syntax.const "_constrain" $ t $
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    73
  (Syntax.free "fun" $ tT $ Syntax.free "dummy");
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    74
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    75
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    76
(*---------------------------------------------------------------------------
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    77
 * Produce an instance of a constructor, plus genvars for its arguments.
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    78
 *---------------------------------------------------------------------------*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    79
fun fresh_constr ty_match ty_inst colty used c =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    80
  let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    81
    val (_, Ty) = dest_Const c
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    82
    val Ts = binder_types Ty;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    83
    val names = Name.variant_list used
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    84
      (DatatypeProp.make_tnames (map Logic.unvarifyT Ts));
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    85
    val ty = body_type Ty;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    86
    val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    87
      raise CASE_ERROR ("type mismatch", ~1)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    88
    val c' = ty_inst ty_theta c
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    89
    val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    90
  in (c', gvars)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    91
  end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    92
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    93
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    94
(*---------------------------------------------------------------------------
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    95
 * Goes through a list of rows and picks out the ones beginning with a
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    96
 * pattern with constructor = name.
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    97
 *---------------------------------------------------------------------------*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    98
fun mk_group (name, T) rows =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    99
  let val k = length (binder_types T)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   100
  in fold (fn (row as ((prfx, p :: rst), rhs as (_, (i, _)))) =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   101
    fn ((in_group, not_in_group), (names, cnstrts)) => (case strip_comb p of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   102
        (Const (name', _), args) =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   103
          if name = name' then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   104
            if length args = k then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   105
              let val (args', cnstrts') = split_list (map strip_constraints args)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   106
              in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   107
                ((((prfx, args' @ rst), rhs) :: in_group, not_in_group),
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   108
                 (default_names names args', map2 append cnstrts cnstrts'))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   109
              end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   110
            else raise CASE_ERROR
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   111
              ("Wrong number of arguments for constructor " ^ name, i)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   112
          else ((in_group, row :: not_in_group), (names, cnstrts))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   113
      | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   114
    rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   115
  end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   116
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   117
(*---------------------------------------------------------------------------
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   118
 * Partition the rows. Not efficient: we should use hashing.
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   119
 *---------------------------------------------------------------------------*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   120
fun partition _ _ _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   121
  | partition ty_match ty_inst type_of used constructors colty res_ty
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   122
        (rows as (((prfx, _ :: rstp), _) :: _)) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   123
      let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   124
        fun part {constrs = [], rows = [], A} = rev A
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   125
          | part {constrs = [], rows = (_, (_, (i, _))) :: _, A} =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   126
              raise CASE_ERROR ("Not a constructor pattern", i)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   127
          | part {constrs = c :: crst, rows, A} =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   128
              let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   129
                val ((in_group, not_in_group), (names, cnstrts)) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   130
                  mk_group (dest_Const c) rows;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   131
                val used' = fold add_row_used in_group used;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   132
                val (c', gvars) = fresh_constr ty_match ty_inst colty used' c;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   133
                val in_group' =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   134
                  if null in_group  (* Constructor not given *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   135
                  then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   136
                    let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   137
                      val Ts = map type_of rstp;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   138
                      val xs = Name.variant_list
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
   139
                        (fold Term.add_free_names gvars used')
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   140
                        (replicate (length rstp) "x")
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   141
                    in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   142
                      [((prfx, gvars @ map Free (xs ~~ Ts)),
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   143
                        (Const ("HOL.undefined", res_ty), (~1, false)))]
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   144
                    end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   145
                  else in_group
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   146
              in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   147
                part{constrs = crst,
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   148
                  rows = not_in_group,
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   149
                  A = {constructor = c',
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   150
                    new_formals = gvars,
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   151
                    names = names,
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   152
                    constraints = cnstrts,
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   153
                    group = in_group'} :: A}
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   154
              end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   155
      in part {constrs = constructors, rows = rows, A = []}
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   156
      end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   157
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   158
(*---------------------------------------------------------------------------
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   159
 * Misc. routines used in mk_case
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   160
 *---------------------------------------------------------------------------*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   161
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   162
fun mk_pat ((c, c'), l) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   163
  let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   164
    val L = length (binder_types (fastype_of c))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   165
    fun build (prfx, tag, plist) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   166
      let val (args, plist') = chop L plist
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   167
      in (prfx, tag, list_comb (c', args) :: plist') end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   168
  in map build l end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   169
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   170
fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   171
  | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   172
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   173
fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   174
  | v_to_pats _ = raise CASE_ERROR ("mk_case: v_to_pats", ~1);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   175
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   176
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   177
(*----------------------------------------------------------------------------
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   178
 * Translation of pattern terms into nested case expressions.
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   179
 *
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   180
 * This performs the translation and also builds the full set of patterns.
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   181
 * Thus it supports the construction of induction theorems even when an
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   182
 * incomplete set of patterns is given.
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   183
 *---------------------------------------------------------------------------*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   184
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   185
fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   186
  let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   187
    val name = Name.variant used "a";
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   188
    fun expand constructors used ty ((_, []), _) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   189
          raise CASE_ERROR ("mk_case: expand_var_row", ~1)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   190
      | expand constructors used ty (row as ((prfx, p :: rst), rhs)) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   191
          if is_Free p then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   192
            let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   193
              val used' = add_row_used row used;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   194
              fun expnd c =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   195
                let val capp =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   196
                  list_comb (fresh_constr ty_match ty_inst ty used' c)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   197
                in ((prfx, capp :: rst), pattern_subst [(p, capp)] rhs)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   198
                end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   199
            in map expnd constructors end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   200
          else [row]
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   201
    fun mk {rows = [], ...} = raise CASE_ERROR ("no rows", ~1)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   202
      | mk {path = [], rows = ((prfx, []), (tm, tag)) :: _} =  (* Done *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   203
          ([(prfx, tag, [])], tm)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   204
      | mk {path, rows as ((row as ((_, [Free _]), _)) :: _ :: _)} =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   205
          mk {path = path, rows = [row]}
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   206
      | mk {path = u :: rstp, rows as ((_, _ :: _), _) :: _} =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   207
          let val col0 = map (fn ((_, p :: _), (_, (i, _))) => (p, i)) rows
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   208
          in case Option.map (apfst head_of)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   209
            (find_first (not o is_Free o fst) col0) of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   210
              NONE =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   211
                let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   212
                  val rows' = map (fn ((v, _), row) => row ||>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   213
                    pattern_subst [(v, u)] |>> v_to_prfx) (col0 ~~ rows);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   214
                  val (pref_patl, tm) = mk {path = rstp, rows = rows'}
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   215
                in (map v_to_pats pref_patl, tm) end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   216
            | SOME (Const (cname, cT), i) => (case ty_info tab cname of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   217
                NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   218
              | SOME {case_name, constructors} =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   219
                let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   220
                  val pty = body_type cT;
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
   221
                  val used' = fold Term.add_free_names rstp used;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   222
                  val nrows = maps (expand constructors used' pty) rows;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   223
                  val subproblems = partition ty_match ty_inst type_of used'
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   224
                    constructors pty range_ty nrows;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   225
                  val new_formals = map #new_formals subproblems
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   226
                  val constructors' = map #constructor subproblems
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   227
                  val news = map (fn {new_formals, group, ...} =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   228
                    {path = new_formals @ rstp, rows = group}) subproblems;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   229
                  val (pat_rect, dtrees) = split_list (map mk news);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   230
                  val case_functions = map2
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   231
                    (fn {new_formals, names, constraints, ...} =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   232
                       fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   233
                         Abs (if s = "" then name else s, T,
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   234
                           abstract_over (x, t)) |>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   235
                         fold mk_fun_constrain cnstrts)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   236
                           (new_formals ~~ names ~~ constraints))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   237
                    subproblems dtrees;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   238
                  val types = map type_of (case_functions @ [u]);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   239
                  val case_const = Const (case_name, types ---> range_ty)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   240
                  val tree = list_comb (case_const, case_functions @ [u])
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   241
                  val pat_rect1 = flat (map mk_pat
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   242
                    (constructors ~~ constructors' ~~ pat_rect))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   243
                in (pat_rect1, tree)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   244
                end)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   245
            | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24349
diff changeset
   246
                Syntax.string_of_term ctxt t, i)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   247
          end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   248
      | mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   249
  in mk
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   250
  end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   251
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   252
fun case_error s = error ("Error in case expression:\n" ^ s);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   253
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   254
(* Repeated variable occurrences in a pattern are not allowed. *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   255
fun no_repeat_vars ctxt pat = fold_aterms
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   256
  (fn x as Free (s, _) => (fn xs =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   257
        if member op aconv xs x then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   258
          case_error (quote s ^ " occurs repeatedly in the pattern " ^
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24349
diff changeset
   259
            quote (Syntax.string_of_term ctxt pat))
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   260
        else x :: xs)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   261
    | _ => I) pat [];
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   262
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   263
fun gen_make_case ty_match ty_inst type_of tab ctxt err used x clauses =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   264
  let
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24349
diff changeset
   265
    fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   266
      (Syntax.const "_case1" $ pat $ rhs);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   267
    val _ = map (no_repeat_vars ctxt o fst) clauses;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   268
    val rows = map_index (fn (i, (pat, rhs)) =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   269
      (([], [pat]), (rhs, (i, true)))) clauses;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   270
    val rangeT = (case distinct op = (map (type_of o snd) clauses) of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   271
        [] => case_error "no clauses given"
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   272
      | [T] => T
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   273
      | _ => case_error "all cases must have the same result type");
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   274
    val used' = fold add_row_used rows used;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   275
    val (patts, case_tm) = mk_case tab ctxt ty_match ty_inst type_of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   276
        used' rangeT {path = [x], rows = rows}
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   277
      handle CASE_ERROR (msg, i) => case_error (msg ^
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   278
        (if i < 0 then ""
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   279
         else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   280
    val patts1 = map
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   281
      (fn (_, tag, [pat]) => (pat, tag)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   282
        | _ => case_error "error in pattern-match translation") patts;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   283
    val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   284
    val finals = map row_of_pat patts2
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   285
    val originals = map (row_of_pat o #2) rows
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   286
    val _ = case originals \\ finals of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   287
        [] => ()
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   288
      | is => (if err then case_error else warning)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   289
          ("The following clauses are redundant (covered by preceding clauses):\n" ^
26931
aa226d8405a8 cat_lines;
wenzelm
parents: 24920
diff changeset
   290
           cat_lines (map (string_of_clause o nth clauses) is));
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   291
  in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   292
    (case_tm, patts2)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   293
  end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   294
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   295
fun make_case tab ctxt = gen_make_case
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   296
  (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   297
val make_case_untyped = gen_make_case (K (K Vartab.empty))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   298
  (K (Term.map_types (K dummyT))) (K dummyT);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   299
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   300
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   301
(* parse translation *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   302
24349
0dd8782fb02d Final mods for list comprehension
nipkow
parents: 22779
diff changeset
   303
fun case_tr err tab_of ctxt [t, u] =
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   304
    let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   305
      val thy = ProofContext.theory_of ctxt;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   306
      (* replace occurrences of dummy_pattern by distinct variables *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   307
      (* internalize constant names                                 *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   308
      fun prep_pat ((c as Const ("_constrain", _)) $ t $ tT) used =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   309
            let val (t', used') = prep_pat t used
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   310
            in (c $ t' $ tT, used') end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   311
        | prep_pat (Const ("dummy_pattern", T)) used =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   312
            let val x = Name.variant used "x"
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   313
            in (Free (x, T), x :: used) end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   314
        | prep_pat (Const (s, T)) used =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   315
            (case try (unprefix Syntax.constN) s of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   316
               SOME c => (Const (c, T), used)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   317
             | NONE => (Const (Sign.intern_const thy s, T), used))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   318
        | prep_pat (v as Free (s, T)) used =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   319
            let val s' = Sign.intern_const thy s
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   320
            in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   321
              if Sign.declared_const thy s' then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   322
                (Const (s', T), used)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   323
              else (v, used)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   324
            end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   325
        | prep_pat (t $ u) used =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   326
            let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   327
              val (t', used') = prep_pat t used;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   328
              val (u', used'') = prep_pat u used'
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   329
            in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   330
              (t' $ u', used'')
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   331
            end
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24349
diff changeset
   332
        | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   333
      fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   334
            let val (l', cnstrts) = strip_constraints l
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
   335
            in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   336
            end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   337
        | dest_case1 t = case_error "dest_case1";
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   338
      fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   339
        | dest_case2 t = [t];
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   340
      val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
24349
0dd8782fb02d Final mods for list comprehension
nipkow
parents: 22779
diff changeset
   341
      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt err []
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   342
        (fold (fn tT => fn t => Syntax.const "_constrain" $ t $ tT)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   343
           (flat cnstrts) t) cases;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   344
    in case_tm end
24349
0dd8782fb02d Final mods for list comprehension
nipkow
parents: 22779
diff changeset
   345
  | case_tr _ _ _ ts = case_error "case_tr";
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   346
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   347
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   348
(*---------------------------------------------------------------------------
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   349
 * Pretty printing of nested case expressions
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   350
 *---------------------------------------------------------------------------*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   351
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   352
(* destruct one level of pattern matching *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   353
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   354
fun gen_dest_case name_of type_of tab d used t =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   355
  case apfst name_of (strip_comb t) of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   356
    (SOME cname, ts as _ :: _) =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   357
      let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   358
        val (fs, x) = split_last ts;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   359
        fun strip_abs i t =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   360
          let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   361
            val zs = strip_abs_vars t;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   362
            val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   363
            val (xs, ys) = chop i zs;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   364
            val u = list_abs (ys, strip_abs_body t);
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29266
diff changeset
   365
            val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   366
              (map fst xs) ~~ map snd xs)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   367
          in (xs', subst_bounds (rev xs', u)) end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   368
        fun is_dependent i t =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   369
          let val k = length (strip_abs_vars t) - i
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   370
          in k < 0 orelse exists (fn j => j >= k)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   371
            (loose_bnos (strip_abs_body t))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   372
          end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   373
        fun count_cases (_, _, true) = I
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   374
          | count_cases (c, (_, body), false) =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   375
              AList.map_default op aconv (body, []) (cons c);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   376
        val is_undefined = name_of #> equal (SOME "HOL.undefined");
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   377
        fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   378
      in case ty_info tab cname of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   379
          SOME {constructors, case_name} =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   380
            if length fs = length constructors then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   381
              let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   382
                val cases = map (fn (Const (s, U), t) =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   383
                  let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   384
                    val k = length (binder_types U);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   385
                    val p as (xs, _) = strip_abs k t
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   386
                  in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   387
                    (Const (s, map type_of xs ---> type_of x),
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   388
                     p, is_dependent k t)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   389
                  end) (constructors ~~ fs);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   390
                val cases' = sort (int_ord o swap o pairself (length o snd))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   391
                  (fold_rev count_cases cases []);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   392
                val R = type_of t;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   393
                val dummy = if d then Const ("dummy_pattern", R)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   394
                  else Free (Name.variant used "x", R)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   395
              in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   396
                SOME (x, map mk_case (case find_first (is_undefined o fst) cases' of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   397
                  SOME (_, cs) =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   398
                  if length cs = length constructors then [hd cases]
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   399
                  else filter_out (fn (_, (_, body), _) => is_undefined body) cases
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   400
                | NONE => case cases' of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   401
                  [] => cases
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   402
                | (default, cs) :: _ =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   403
                  if length cs = 1 then cases
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   404
                  else if length cs = length constructors then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   405
                    [hd cases, (dummy, ([], default), false)]
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   406
                  else
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   407
                    filter_out (fn (c, _, _) => member op aconv cs c) cases @
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   408
                    [(dummy, ([], default), false)]))
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   409
              end handle CASE_ERROR _ => NONE
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   410
            else NONE
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   411
        | _ => NONE
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   412
      end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   413
  | _ => NONE;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   414
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   415
val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   416
val dest_case' = gen_dest_case
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   417
  (try (dest_Const #> fst #> unprefix Syntax.constN)) (K dummyT);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   418
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   419
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   420
(* destruct nested patterns *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   421
29623
1219985d24b5 avoiding misleading name duplicate
haftmann
parents: 29281
diff changeset
   422
fun strip_case'' dest (pat, rhs) =
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
   423
  case dest (Term.add_free_names pat []) rhs of
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   424
    SOME (exp as Free _, clauses) =>
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 26931
diff changeset
   425
      if member op aconv (OldTerm.term_frees pat) exp andalso
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   426
        not (exists (fn (_, rhs') =>
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 26931
diff changeset
   427
          member op aconv (OldTerm.term_frees rhs') exp) clauses)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   428
      then
29623
1219985d24b5 avoiding misleading name duplicate
haftmann
parents: 29281
diff changeset
   429
        maps (strip_case'' dest) (map (fn (pat', rhs') =>
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   430
          (subst_free [(exp, pat')] pat, rhs')) clauses)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   431
      else [(pat, rhs)]
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   432
  | _ => [(pat, rhs)];
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   433
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   434
fun gen_strip_case dest t = case dest [] t of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   435
    SOME (x, clauses) =>
29623
1219985d24b5 avoiding misleading name duplicate
haftmann
parents: 29281
diff changeset
   436
      SOME (x, maps (strip_case'' dest) clauses)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   437
  | NONE => NONE;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   438
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   439
val strip_case = gen_strip_case oo dest_case;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   440
val strip_case' = gen_strip_case oo dest_case';
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   441
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   442
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   443
(* print translation *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   444
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   445
fun case_tr' tab_of cname ctxt ts =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   446
  let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   447
    val thy = ProofContext.theory_of ctxt;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   448
    val consts = ProofContext.consts_of ctxt;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   449
    fun mk_clause (pat, rhs) =
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 26931
diff changeset
   450
      let val xs = Term.add_frees pat []
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   451
      in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   452
        Syntax.const "_case1" $
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   453
          map_aterms
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   454
            (fn Free p => Syntax.mark_boundT p
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   455
              | Const (s, _) => Const (Consts.extern_early consts s, dummyT)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   456
              | t => t) pat $
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   457
          map_aterms
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 26931
diff changeset
   458
            (fn x as Free (s, T) =>
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 26931
diff changeset
   459
                  if member (op =) xs (s, T) then Syntax.mark_bound s else x
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   460
              | t => t) rhs
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   461
      end
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   462
  in case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   463
      SOME (x, clauses) => Syntax.const "_case_syntax" $ x $
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   464
        foldr1 (fn (t, u) => Syntax.const "_case2" $ t $ u)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   465
          (map mk_clause clauses)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   466
    | NONE => raise Match
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   467
  end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   468
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   469
end;