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