author | haftmann |
Wed, 10 Jun 2009 15:04:33 +0200 | |
changeset 31604 | eb2f9d709296 |
parent 29623 | src/HOL/Tools/datatype_case.ML@1219985d24b5 |
child 31737 | b3f63611784e |
permissions | -rw-r--r-- |
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 | 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 | 17 |
val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option) |
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 | 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 | 61 |
fun add_row_used ((prfx, pats), (tm, tag)) = |
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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 422 |
fun strip_case'' dest (pat, rhs) = |
29281 | 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 | 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 | 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 | 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 | 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 | 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 | 458 |
(fn x as Free (s, T) => |
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; |