src/HOL/Tools/Datatype/datatype_case.ML
author wenzelm
Wed, 11 Jan 2012 17:30:34 +0100
changeset 46188 8297006abc13
parent 46140 463b594e186a
child 46219 426ed18eba43
permissions -rw-r--r--
actually try to preserve names given by user (cf. 463b594e186a);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33968
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33040
diff changeset
     1
(*  Title:      HOL/Tools/Datatype/datatype_case.ML
22779
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
33968
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33040
diff changeset
     5
Datatype package: nested case expressions on datatypes.
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
     6
46135
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
     7
TODO:
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
     8
  * Avoid fragile operations on syntax trees (with type constraints
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
     9
    getting in the way).  Instead work with auxiliary "destructor"
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
    10
    constants in translations and introduce the actual case
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
    11
    combinators in a separate term check phase (similar to term
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
    12
    abbreviations).
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
    13
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
    14
  * Avoid hard-wiring with datatype package.  Instead provide generic
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
    15
    generic declarations of case splits based on an internal data slot.
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    16
*)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    17
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    18
signature DATATYPE_CASE =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    19
sig
33968
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33040
diff changeset
    20
  datatype config = Error | Warning | Quiet
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33040
diff changeset
    21
  type info = Datatype_Aux.info
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
    22
  val make_case :  Proof.context -> config -> string list -> term -> (term * term) list -> term
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
    23
  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
    24
  val case_tr: bool -> Proof.context -> term list -> term
46003
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
    25
  val show_cases: bool Config.T
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
    26
  val case_tr': string -> Proof.context -> term list -> term
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
    27
  val add_case_tr' : string list -> theory -> theory
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
    28
  val setup: theory -> theory
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    29
end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    30
33968
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33040
diff changeset
    31
structure Datatype_Case : DATATYPE_CASE =
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    32
struct
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    33
32671
fbd224850767 adapted configuration for DatatypeCase.make_case
bulwahn
parents: 32035
diff changeset
    34
datatype config = Error | Warning | Quiet;
33968
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33040
diff changeset
    35
type info = Datatype_Aux.info;
32671
fbd224850767 adapted configuration for DatatypeCase.make_case
bulwahn
parents: 32035
diff changeset
    36
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    37
exception CASE_ERROR of string * int;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    38
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    39
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
    40
43255
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
    41
(* Get information about datatypes *)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    42
45894
wenzelm
parents: 45891
diff changeset
    43
fun ty_info ({descr, case_name, index, ...} : info) =
wenzelm
parents: 45891
diff changeset
    44
  let
wenzelm
parents: 45891
diff changeset
    45
    val (_, (tname, dts, constrs)) = nth descr index;
wenzelm
parents: 45891
diff changeset
    46
    val mk_ty = Datatype_Aux.typ_of_dtyp descr;
wenzelm
parents: 45891
diff changeset
    47
    val T = Type (tname, map mk_ty dts);
wenzelm
parents: 45891
diff changeset
    48
  in
wenzelm
parents: 45891
diff changeset
    49
   {case_name = case_name,
wenzelm
parents: 45891
diff changeset
    50
    constructors = map (fn (cname, dts') =>
wenzelm
parents: 45891
diff changeset
    51
      Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
wenzelm
parents: 45891
diff changeset
    52
  end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    53
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    54
43255
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
    55
(*Each pattern carries with it a tag i, which denotes the clause it
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
    56
came from. i = ~1 indicates that the clause was added by pattern
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
    57
completion.*)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    58
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
    59
fun add_row_used ((prfx, pats), (tm, tag)) =
43252
b142ae3e9478 more precise type for obscure "prfx" field
krauss
parents: 42361
diff changeset
    60
  fold Term.add_free_names (tm :: pats @ map Free prfx);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    61
46140
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
    62
fun default_name name (t, cs) =
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
    63
  let
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
    64
    val name' = if name = "" then (case t of Free (name', _) => name' | _ => name) else name;
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
    65
    val cs' = if is_Free t then cs else filter_out Term_Position.is_position cs;
46188
8297006abc13 actually try to preserve names given by user (cf. 463b594e186a);
wenzelm
parents: 46140
diff changeset
    66
  in (name', cs') end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    67
35124
33976519c888 formal markup of constants;
wenzelm
parents: 33969
diff changeset
    68
fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
22779
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
46139
wenzelm
parents: 46135
diff changeset
    72
fun constrain tT t = Syntax.const @{syntax_const "_constrain"} $ t $ tT;
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    73
fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
22779
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
43255
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
    76
(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    77
fun fresh_constr ty_match ty_inst colty used c =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    78
  let
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    79
    val (_, T) = dest_Const c;
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    80
    val Ts = binder_types T;
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
    81
    val names =
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
    82
      Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    83
    val ty = body_type T;
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
    84
    val ty_theta = ty_match ty colty
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
    85
      handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
    86
    val c' = ty_inst ty_theta c;
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
    87
    val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts);
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
    88
  in (c', gvars) end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    89
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    90
fun strip_comb_positions tm =
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    91
  let
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    92
    fun result t ts = (Term_Position.strip_positions t, ts);
46139
wenzelm
parents: 46135
diff changeset
    93
    fun strip (t as Const (@{syntax_const "_constrain"}, _) $ _ $ _) ts = result t ts
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    94
      | strip (f $ t) ts = strip f (t :: ts)
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    95
      | strip t ts = result t ts;
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
    96
  in strip tm [] end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
    97
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
    98
(*Go through a list of rows and pick out the ones beginning with a
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
    99
  pattern with constructor = name.*)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   100
fun mk_group (name, T) rows =
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   101
  let val k = length (binder_types T) in
43256
375809f9afad more conventional variable naming
krauss
parents: 43255
diff changeset
   102
    fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   103
      fn ((in_group, not_in_group), (names, cnstrts)) =>
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
   104
        (case strip_comb_positions p of
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   105
          (Const (name', _), args) =>
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   106
            if name = name' then
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   107
              if length args = k then
46140
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
   108
                let
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
   109
                  val constraints' = map strip_constraints args;
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
   110
                  val (args', cnstrts') = split_list constraints';
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
   111
                  val (names', cnstrts'') = split_list (map2 default_name names constraints');
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
   112
                in
43256
375809f9afad more conventional variable naming
krauss
parents: 43255
diff changeset
   113
                  ((((prfx, args' @ ps), rhs) :: in_group, not_in_group),
46140
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
   114
                   (names', map2 append cnstrts cnstrts''))
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   115
                end
46139
wenzelm
parents: 46135
diff changeset
   116
              else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i)
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   117
            else ((in_group, row :: not_in_group), (names, cnstrts))
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   118
        | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   119
    rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   120
  end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   121
43255
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
   122
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
   123
(* Partitioning *)
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
   124
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   125
fun partition _ _ _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   126
  | partition ty_match ty_inst type_of used constructors colty res_ty
43256
375809f9afad more conventional variable naming
krauss
parents: 43255
diff changeset
   127
        (rows as (((prfx, _ :: ps), _) :: _)) =
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   128
      let
43257
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   129
        fun part [] [] = []
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   130
          | part [] ((_, (_, i)) :: _) = raise CASE_ERROR ("Not a constructor pattern", i)
43257
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   131
          | part (c :: cs) rows =
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   132
              let
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   133
                val ((in_group, not_in_group), (names, cnstrts)) = mk_group (dest_Const c) rows;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   134
                val used' = fold add_row_used in_group used;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   135
                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
   136
                val in_group' =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   137
                  if null in_group  (* Constructor not given *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   138
                  then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   139
                    let
43256
375809f9afad more conventional variable naming
krauss
parents: 43255
diff changeset
   140
                      val Ts = map type_of ps;
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   141
                      val xs =
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   142
                        Name.variant_list
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   143
                          (fold Term.add_free_names gvars used')
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   144
                          (replicate (length ps) "x");
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   145
                    in
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   146
                      [((prfx, gvars @ map Free (xs ~~ Ts)),
43254
2127c138ba3a less redundant tags
krauss
parents: 43253
diff changeset
   147
                        (Const (@{const_syntax undefined}, res_ty), ~1))]
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   148
                    end
46139
wenzelm
parents: 46135
diff changeset
   149
                  else in_group;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   150
              in
43257
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   151
                {constructor = c',
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   152
                 new_formals = gvars,
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   153
                 names = names,
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   154
                 constraints = cnstrts,
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   155
                 group = in_group'} :: part cs not_in_group
45898
wenzelm
parents: 45894
diff changeset
   156
              end;
43257
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   157
      in part constructors rows end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   158
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   159
fun v_to_prfx (prfx, Free v :: pats) = (v :: prfx, pats)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   160
  | 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
   161
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   162
43255
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
   163
(* Translation of pattern terms into nested case expressions. *)
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   164
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   165
fun mk_case ctxt ty_match ty_inst type_of used range_ty =
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   166
  let
45894
wenzelm
parents: 45891
diff changeset
   167
    val get_info = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt);
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   168
46139
wenzelm
parents: 46135
diff changeset
   169
    fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
43256
375809f9afad more conventional variable naming
krauss
parents: 43255
diff changeset
   170
      | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   171
          if is_Free p then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   172
            let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   173
              val used' = add_row_used row used;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   174
              fun expnd c =
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   175
                let val capp = list_comb (fresh_constr ty_match ty_inst ty used' c)
46140
463b594e186a refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";
wenzelm
parents: 46139
diff changeset
   176
                in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   177
            in map expnd constructors end
45898
wenzelm
parents: 45894
diff changeset
   178
          else [row];
wenzelm
parents: 45894
diff changeset
   179
wenzelm
parents: 45894
diff changeset
   180
    val name = singleton (Name.variant_list used) "a";
wenzelm
parents: 45894
diff changeset
   181
43257
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   182
    fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   183
      | mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   184
      | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
43257
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   185
      | mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
43254
2127c138ba3a less redundant tags
krauss
parents: 43253
diff changeset
   186
          let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
   187
            (case Option.map (apfst (fst o strip_comb_positions))
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
   188
                (find_first (not o is_Free o fst) col0) of
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   189
              NONE =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   190
                let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   191
                  val rows' = map (fn ((v, _), row) => row ||>
43255
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
   192
                    apfst (subst_free [(v, u)]) |>> v_to_prfx) (col0 ~~ rows);
43257
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   193
                in mk us rows' end
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   194
            | SOME (Const (cname, cT), i) =>
45894
wenzelm
parents: 45891
diff changeset
   195
                (case Option.map ty_info (get_info (cname, cT)) of
46139
wenzelm
parents: 46135
diff changeset
   196
                  NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ quote cname, i)
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   197
                | SOME {case_name, constructors} =>
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   198
                    let
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   199
                      val pty = body_type cT;
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   200
                      val used' = fold Term.add_free_names us used;
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   201
                      val nrows = maps (expand constructors used' pty) rows;
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   202
                      val subproblems =
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   203
                        partition ty_match ty_inst type_of used'
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   204
                          constructors pty range_ty nrows;
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   205
                      val (pat_rect, dtrees) =
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   206
                        split_list (map (fn {new_formals, group, ...} =>
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   207
                          mk (new_formals @ us) group) subproblems);
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   208
                      val case_functions =
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   209
                        map2 (fn {new_formals, names, constraints, ...} =>
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   210
                          fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   211
                            Abs (if s = "" then name else s, T, abstract_over (x, t))
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
   212
                            |> fold constrain_Abs cnstrts) (new_formals ~~ names ~~ constraints))
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   213
                        subproblems dtrees;
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   214
                      val types = map type_of (case_functions @ [u]);
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   215
                      val case_const = Const (case_name, types ---> range_ty);
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   216
                      val tree = list_comb (case_const, case_functions @ [u]);
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   217
                    in (flat pat_rect, tree) end)
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   218
            | SOME (t, i) =>
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   219
                raise CASE_ERROR ("Not a datatype constructor: " ^ Syntax.string_of_term ctxt t, i))
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   220
          end
43257
b81fd5c8f2dc eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
krauss
parents: 43256
diff changeset
   221
      | mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1)
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   222
  in mk end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   223
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   224
fun case_error s = error ("Error in case expression:\n" ^ s);
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   225
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   226
local
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   227
43255
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
   228
(*Repeated variable occurrences in a pattern are not allowed.*)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   229
fun no_repeat_vars ctxt pat = fold_aterms
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   230
  (fn x as Free (s, _) =>
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   231
      (fn xs =>
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   232
        if member op aconv xs x then
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   233
          case_error (quote s ^ " occurs repeatedly in the pattern " ^
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   234
            quote (Syntax.string_of_term ctxt pat))
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   235
        else x :: xs)
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
   236
    | _ => I) (Term_Position.strip_positions pat) [];
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   237
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   238
fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses =
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   239
  let
35124
33976519c888 formal markup of constants;
wenzelm
parents: 33969
diff changeset
   240
    fun string_of_clause (pat, rhs) =
33976519c888 formal markup of constants;
wenzelm
parents: 33969
diff changeset
   241
      Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   242
    val _ = map (no_repeat_vars ctxt o fst) clauses;
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   243
    val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
35124
33976519c888 formal markup of constants;
wenzelm
parents: 33969
diff changeset
   244
    val rangeT =
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   245
      (case distinct (op =) (map (type_of o snd) clauses) of
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   246
        [] => case_error "no clauses given"
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   247
      | [T] => T
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   248
      | _ => case_error "all cases must have the same result type");
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   249
    val used' = fold add_row_used rows used;
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   250
    val (tags, case_tm) =
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   251
      mk_case ctxt ty_match ty_inst type_of used' rangeT [x] rows
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   252
        handle CASE_ERROR (msg, i) =>
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   253
          case_error
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   254
            (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
35124
33976519c888 formal markup of constants;
wenzelm
parents: 33969
diff changeset
   255
    val _ =
43254
2127c138ba3a less redundant tags
krauss
parents: 43253
diff changeset
   256
      (case subtract (op =) tags (map (snd o snd) rows) of
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   257
        [] => ()
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   258
      | is =>
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   259
          (case config of Error => case_error | Warning => warning | Quiet => fn _ => ())
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   260
            ("The following clauses are redundant (covered by preceding clauses):\n" ^
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   261
              cat_lines (map (string_of_clause o nth clauses) is)));
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   262
  in
43253
fa3c61dc9f2c removed generation of instantiated pattern set, which is never actually used
krauss
parents: 43252
diff changeset
   263
    case_tm
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   264
  end;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   265
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   266
in
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   267
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   268
fun make_case ctxt =
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   269
  gen_make_case (match_type (Proof_Context.theory_of ctxt))
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   270
    Envir.subst_term_types fastype_of ctxt;
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   271
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   272
val make_case_untyped =
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   273
  gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   274
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   275
end;
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   276
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   277
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   278
(* parse translation *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   279
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   280
fun case_tr err ctxt [t, u] =
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   281
      let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   282
        val thy = Proof_Context.theory_of ctxt;
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   283
        val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt);
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35140
diff changeset
   284
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   285
        (* replace occurrences of dummy_pattern by distinct variables *)
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   286
        (* internalize constant names                                 *)
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43257
diff changeset
   287
        (* FIXME proper name context!? *)
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   288
        fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   289
              let val (t', used') = prep_pat t used
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   290
              in (c $ t' $ tT, used') end
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   291
          | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43257
diff changeset
   292
              let val x = singleton (Name.variant_list used) "x"
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   293
              in (Free (x, T), x :: used) end
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   294
          | prep_pat (Const (s, T)) used = (Const (intern_const_syntax s, T), used)
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   295
          | prep_pat (v as Free (s, T)) used =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   296
              let val s' = Proof_Context.intern_const ctxt s in
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   297
                if Sign.declared_const thy s' then (Const (s', T), used)
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   298
                else (v, used)
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   299
              end
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   300
          | prep_pat (t $ u) used =
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   301
              let
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   302
                val (t', used') = prep_pat t used;
42359
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42290
diff changeset
   303
                val (u', used'') = prep_pat u used';
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   304
              in (t' $ u', used'') end
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   305
          | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
45898
wenzelm
parents: 45894
diff changeset
   306
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   307
        fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   308
              let val (l', cnstrts) = strip_constraints l
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   309
              in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts) end
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   310
          | dest_case1 t = case_error "dest_case1";
45898
wenzelm
parents: 45894
diff changeset
   311
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   312
        fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   313
          | dest_case2 t = [t];
45898
wenzelm
parents: 45894
diff changeset
   314
42057
3eba96ff3d3e more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents: 42050
diff changeset
   315
        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
45898
wenzelm
parents: 45894
diff changeset
   316
      in
wenzelm
parents: 45894
diff changeset
   317
        make_case_untyped ctxt
wenzelm
parents: 45894
diff changeset
   318
          (if err then Error else Warning) []
46139
wenzelm
parents: 46135
diff changeset
   319
          (fold constrain (filter_out Term_Position.is_position (flat cnstrts)) t)
46135
6bff2ebaf7bb more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);
wenzelm
parents: 46125
diff changeset
   320
          cases
45898
wenzelm
parents: 45894
diff changeset
   321
      end
45894
wenzelm
parents: 45891
diff changeset
   322
  | case_tr _ _ _ = case_error "case_tr";
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   323
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   324
val trfun_setup =
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   325
  Sign.add_advanced_trfuns ([],
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   326
    [(@{syntax_const "_case_syntax"}, case_tr true)],
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   327
    [], []);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   328
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   329
43255
7df9edc6a2d6 dropped outdated/speculative historical comments;
krauss
parents: 43254
diff changeset
   330
(* Pretty printing of nested case expressions *)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   331
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   332
(* destruct one level of pattern matching *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   333
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   334
local
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   335
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   336
fun gen_dest_case name_of type_of ctxt d used t =
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   337
  (case apfst name_of (strip_comb t) of
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   338
    (SOME cname, ts as _ :: _) =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   339
      let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   340
        val (fs, x) = split_last ts;
46059
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   341
        fun strip_abs i Us t =
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   342
          let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   343
            val zs = strip_abs_vars t;
46059
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   344
            val j = length zs;
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   345
            val (xs, ys) =
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   346
              if j < i then (zs @ map (pair "x") (drop j Us), [])
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   347
              else chop i zs;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   348
            val u = list_abs (ys, strip_abs_body t);
46059
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   349
            val xs' = map Free
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   350
              ((fold_map Name.variant (map fst xs)
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   351
                  (Term.declare_term_names u used) |> fst) ~~
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   352
               map snd xs);
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   353
            val (xs1, xs2) = chop j xs'
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   354
          in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   355
        fun is_dependent i t =
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   356
          let val k = length (strip_abs_vars t) - i
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   357
          in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   358
        fun count_cases (_, _, true) = I
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   359
          | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c);
35392
5da5ac6c6b77 gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;
wenzelm
parents: 35363
diff changeset
   360
        val is_undefined = name_of #> equal (SOME @{const_name undefined});
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   361
        fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body);
45894
wenzelm
parents: 45891
diff changeset
   362
        val get_info = Datatype_Data.info_of_case (Proof_Context.theory_of ctxt);
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   363
      in
45894
wenzelm
parents: 45891
diff changeset
   364
        (case Option.map ty_info (get_info cname) of
wenzelm
parents: 45891
diff changeset
   365
          SOME {constructors, ...} =>
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   366
            if length fs = length constructors then
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   367
              let
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   368
                val cases = map (fn (Const (s, U), t) =>
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   369
                  let
46059
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   370
                    val Us = binder_types U;
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   371
                    val k = length Us;
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   372
                    val p as (xs, _) = strip_abs k Us t;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   373
                  in
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   374
                    (Const (s, map type_of xs ---> type_of x), p, is_dependent k t)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   375
                  end) (constructors ~~ fs);
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   376
                val cases' =
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   377
                  sort (int_ord o swap o pairself (length o snd))
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   378
                    (fold_rev count_cases cases []);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   379
                val R = type_of t;
35124
33976519c888 formal markup of constants;
wenzelm
parents: 33969
diff changeset
   380
                val dummy =
45156
a9b6c2ea7bec added Term.dummy_pattern conveniences;
wenzelm
parents: 44121
diff changeset
   381
                  if d then Term.dummy_pattern R
46059
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   382
                  else Free (Name.variant "x" used |> fst, R);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   383
              in
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   384
                SOME (x,
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   385
                  map mk_case
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   386
                    (case find_first (is_undefined o fst) cases' of
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   387
                      SOME (_, cs) =>
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   388
                        if length cs = length constructors then [hd cases]
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   389
                        else filter_out (fn (_, (_, body), _) => is_undefined body) cases
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   390
                    | NONE =>
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   391
                        (case cases' of
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   392
                          [] => cases
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   393
                        | (default, cs) :: _ =>
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   394
                            if length cs = 1 then cases
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   395
                            else if length cs = length constructors then
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   396
                              [hd cases, (dummy, ([], default), false)]
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   397
                            else
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   398
                              filter_out (fn (c, _, _) => member op aconv cs c) cases @
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   399
                                [(dummy, ([], default), false)])))
46059
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   400
              end
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   401
            else NONE
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   402
        | _ => NONE)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   403
      end
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   404
  | _ => NONE);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   405
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   406
in
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   407
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   408
val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42284
diff changeset
   409
val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   410
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   411
end;
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   412
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   413
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   414
(* destruct nested patterns *)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   415
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   416
local
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   417
29623
1219985d24b5 avoiding misleading name duplicate
haftmann
parents: 29281
diff changeset
   418
fun strip_case'' dest (pat, rhs) =
46059
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   419
  (case dest (Term.declare_term_frees pat Name.context) rhs of
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   420
    SOME (exp as Free _, clauses) =>
45738
0430f9123e43 eliminated some legacy operations;
wenzelm
parents: 45700
diff changeset
   421
      if Term.exists_subterm (curry (op aconv) exp) pat andalso
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   422
        not (exists (fn (_, rhs') =>
45738
0430f9123e43 eliminated some legacy operations;
wenzelm
parents: 45700
diff changeset
   423
          Term.exists_subterm (curry (op aconv) exp) rhs') clauses)
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   424
      then
29623
1219985d24b5 avoiding misleading name duplicate
haftmann
parents: 29281
diff changeset
   425
        maps (strip_case'' dest) (map (fn (pat', rhs') =>
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   426
          (subst_free [(exp, pat')] pat, rhs')) clauses)
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   427
      else [(pat, rhs)]
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   428
  | _ => [(pat, rhs)]);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   429
35124
33976519c888 formal markup of constants;
wenzelm
parents: 33969
diff changeset
   430
fun gen_strip_case dest t =
46059
f805747f8571 Made gen_dest_case more robust against eta contraction
berghofe
parents: 46003
diff changeset
   431
  (case dest Name.context t of
45700
9dcbf6a1829c misc tuning;
wenzelm
parents: 45156
diff changeset
   432
    SOME (x, clauses) => SOME (x, maps (strip_case'' dest) clauses)
42049
e945717b2b15 tuned indendation and parentheses;
wenzelm
parents: 35845
diff changeset
   433
  | NONE => NONE);
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   434
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   435
in
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   436
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   437
val strip_case = gen_strip_case oo dest_case;
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   438
val strip_case' = gen_strip_case oo dest_case';
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   439
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   440
end;
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45822
diff changeset
   441
22779
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
46003
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   445
val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   446
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   447
fun case_tr' cname ctxt ts =
46003
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   448
  if Config.get ctxt show_cases then
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   449
    let
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   450
      fun mk_clause (pat, rhs) =
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   451
        let val xs = Term.add_frees pat [] in
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   452
          Syntax.const @{syntax_const "_case1"} $
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   453
            map_aterms
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   454
              (fn Free p => Syntax_Trans.mark_boundT p
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   455
                | Const (s, _) => Syntax.const (Lexicon.mark_const s)
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   456
                | t => t) pat $
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   457
            map_aterms
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
   458
              (fn x as Free (s, T) =>
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 46059
diff changeset
   459
                  if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
46003
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   460
                | t => t) rhs
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   461
        end;
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   462
    in
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   463
      (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   464
        SOME (x, clauses) =>
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   465
          Syntax.const @{syntax_const "_case_syntax"} $ x $
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   466
            foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   467
              (map mk_clause clauses)
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   468
      | NONE => raise Match)
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   469
    end
c0fe5e8e4864 print case syntax depending on "show_cases" configuration option;
wenzelm
parents: 45898
diff changeset
   470
  else raise Match;
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   471
45891
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   472
fun add_case_tr' case_names thy =
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   473
  Sign.add_advanced_trfuns ([], [],
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   474
    map (fn case_name =>
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   475
      let val case_name' = Lexicon.mark_const case_name
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   476
      in (case_name', case_tr' case_name') end) case_names, []) thy;
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   477
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   478
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   479
(* theory setup *)
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   480
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   481
val setup = trfun_setup;
d73605c829cc clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm
parents: 45889
diff changeset
   482
22779
9ac0ca736969 Parse / print translations for nested case expressions, taken
berghofe
parents:
diff changeset
   483
end;