author | wenzelm |
Sun, 26 May 2013 19:29:15 +0200 | |
changeset 52157 | ba6b2876ef5a |
parent 52155 | 761c325a65d4 |
child 52158 | d5fa81343322 |
permissions | -rw-r--r-- |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
1 |
(* Title: Tools/case_translation.ML |
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 |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
11 |
datatype config = Error | Warning | Quiet |
51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset
|
12 |
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
|
13 |
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
|
14 |
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
|
15 |
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
|
16 |
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
|
17 |
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
|
18 |
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
|
19 |
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
|
20 |
val show_cases: bool Config.T |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
21 |
val setup: theory -> theory |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
22 |
val register: term -> term list -> Context.generic -> Context.generic |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
23 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
24 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
25 |
structure Case_Translation: CASE_TRANSLATION = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
26 |
struct |
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 |
(** data management **) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
29 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
30 |
datatype data = Data of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
31 |
{constrs: (string * (term * term list)) list Symtab.table, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
32 |
cases: (term * term list) Symtab.table}; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
33 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
34 |
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
|
35 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
36 |
structure Data = Generic_Data |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
37 |
( |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
38 |
type T = data; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
39 |
val empty = make_data (Symtab.empty, Symtab.empty); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
40 |
val extend = I; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
41 |
fun merge |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
42 |
(Data {constrs = constrs1, cases = cases1}, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
43 |
Data {constrs = constrs2, cases = cases2}) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
44 |
make_data |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
45 |
(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
|
46 |
Symtab.merge (K true) (cases1, cases2)); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
47 |
); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
48 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
49 |
fun map_data f = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
50 |
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
|
51 |
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
|
52 |
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
|
53 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
54 |
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
|
55 |
|
51684 | 56 |
fun T_of_data (comb, constrs : term list) = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
57 |
fastype_of comb |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
58 |
|> funpow (length constrs) range_type |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
59 |
|> domain_type; |
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 |
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
|
62 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
63 |
val constrs_of = #constrs o rep_data; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
64 |
val cases_of = #cases o rep_data; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
65 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
66 |
fun lookup_by_constr ctxt (c, T) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
67 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
68 |
val tab = Symtab.lookup_list (constrs_of ctxt) c; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
69 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
70 |
(case body_type T of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
71 |
Type (tyco, _) => AList.lookup (op =) tab tyco |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
72 |
| _ => NONE) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
73 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
74 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
75 |
fun lookup_by_constr_permissive ctxt (c, T) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
76 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
77 |
val tab = Symtab.lookup_list (constrs_of ctxt) c; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
(*conservative wrt. overloaded constructors*) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
81 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
82 |
(case hint of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
83 |
NONE => default |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
84 |
| SOME tyco => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
85 |
(case AList.lookup (op =) tab tyco of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
86 |
NONE => default (*permissive*) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
87 |
| SOME info => SOME info)) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
88 |
end; |
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 lookup_by_case = Symtab.lookup o cases_of; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
91 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
92 |
|
52154 | 93 |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
94 |
(** installation **) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
95 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
96 |
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
|
97 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
98 |
val name_of = try (dest_Const #> fst); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
99 |
|
52154 | 100 |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
101 |
(* parse translation *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
102 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
103 |
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
|
104 |
|
51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset
|
105 |
fun case_tr err ctxt [t, u] = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
106 |
let |
52157 | 107 |
val consts = Proof_Context.consts_of ctxt; |
108 |
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
|
109 |
|
52157 | 110 |
fun abs p tTs t = |
111 |
Syntax.const @{const_syntax case_abs} $ |
|
112 |
fold constrain_Abs tTs (absfree p t); |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
113 |
|
51693 | 114 |
fun abs_pat (Const (@{syntax_const "_constrain"}, _) $ t $ tT) tTs = |
115 |
abs_pat t (tT :: tTs) |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
116 |
| abs_pat (Free (p as (x, _))) tTs = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
117 |
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
|
118 |
| 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
|
119 |
| abs_pat _ _ = I; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
120 |
|
51680
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
121 |
(* replace occurrences of dummy_pattern by distinct variables *) |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
122 |
fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used = |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
123 |
let val (x, used') = Name.variant "x" used |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
124 |
in (Free (x, T), used') end |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
125 |
| replace_dummies (t $ u) used = |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
126 |
let |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
127 |
val (t', used') = replace_dummies t used; |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
128 |
val (u', used'') = replace_dummies u used'; |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
129 |
in (t' $ u', used'') end |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
130 |
| replace_dummies t used = (t, used); |
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
131 |
|
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset
|
132 |
fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) = |
52154 | 133 |
let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context) in |
134 |
abs_pat l' [] |
|
135 |
(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
|
136 |
end |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
137 |
| dest_case1 _ = case_error "dest_case1"; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
138 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
139 |
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
|
140 |
| dest_case2 t = [t]; |
51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset
|
141 |
|
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset
|
142 |
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
|
143 |
in |
52154 | 144 |
Syntax.const @{const_syntax case_guard} $ errt $ t $ |
145 |
(fold_rev |
|
146 |
(fn t => fn u => Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u) |
|
147 |
(dest_case2 u) |
|
148 |
(Syntax.const @{const_syntax case_nil})) |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
149 |
end |
51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset
|
150 |
| case_tr _ _ _ = case_error "case_tr"; |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
151 |
|
52143 | 152 |
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
|
153 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
154 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
155 |
(* print translation *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
156 |
|
51751
cf039b3c42a7
slightly more aggressive syntax translation for printing case expressions
traytel
parents:
51693
diff
changeset
|
157 |
fun case_tr' (_ :: x :: t :: ts) = |
52154 | 158 |
let |
159 |
fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used = |
|
160 |
let val (s', used') = Name.variant s used |
|
161 |
in mk_clause t ((s', T) :: xs) used' end |
|
162 |
| mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ = |
|
163 |
Syntax.const @{syntax_const "_case1"} $ |
|
164 |
subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $ |
|
165 |
subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs); |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
166 |
|
52154 | 167 |
fun mk_clauses (Const (@{const_syntax case_nil}, _)) = [] |
168 |
| mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) = |
|
169 |
mk_clause t [] (Term.declare_term_frees t Name.context) :: |
|
170 |
mk_clauses u |
|
171 |
in |
|
172 |
list_comb (Syntax.const @{syntax_const "_case_syntax"} $ x $ |
|
173 |
foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u) |
|
174 |
(mk_clauses t), ts) |
|
175 |
end; |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
176 |
|
52143 | 177 |
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
|
178 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
179 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
180 |
(* declarations *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
181 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
182 |
fun register raw_case_comb raw_constrs context = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
183 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
184 |
val ctxt = Context.proof_of context; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
185 |
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
|
186 |
val constrs = Variable.polymorphic ctxt raw_constrs; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
187 |
val case_key = case_comb |> dest_Const |> fst; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
188 |
val constr_keys = map (fst o dest_Const) constrs; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
189 |
val data = (case_comb, constrs); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
190 |
val Tname = Tname_of_data data; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
191 |
val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
192 |
val update_cases = Symtab.update (case_key, data); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
193 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
194 |
context |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
195 |
|> map_constrs update_constrs |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
196 |
|> map_cases update_cases |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
197 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
198 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
199 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
200 |
(* (Un)check phases *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
201 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
202 |
datatype config = Error | Warning | Quiet; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
203 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
204 |
exception CASE_ERROR of string * int; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
205 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
206 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
207 |
(*Each pattern carries with it a tag i, which denotes the clause it |
52154 | 208 |
came from. i = ~1 indicates that the clause was added by pattern |
209 |
completion.*) |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
210 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
211 |
fun add_row_used ((prfx, pats), (tm, tag)) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
212 |
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
|
213 |
|
52154 | 214 |
(*try to preserve names given by user*) |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
215 |
fun default_name "" (Free (name', _)) = name' |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
216 |
| default_name name _ = name; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
217 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
218 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
219 |
(*Produce an instance of a constructor, plus fresh variables for its arguments.*) |
51675 | 220 |
fun fresh_constr colty used c = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
221 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
222 |
val (_, T) = dest_Const c; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
223 |
val Ts = binder_types T; |
52154 | 224 |
val (names, _) = |
225 |
fold_map Name.variant |
|
226 |
(Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used; |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
227 |
val ty = body_type T; |
51675 | 228 |
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
|
229 |
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
|
230 |
val c' = Envir.subst_term_types ty_theta c; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
231 |
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
|
232 |
in (c', gvars) end; |
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 |
(*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
|
235 |
pattern with constructor = name.*) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
236 |
fun mk_group (name, T) rows = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
237 |
let val k = length (binder_types T) in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
238 |
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
|
239 |
fn ((in_group, not_in_group), names) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
240 |
(case strip_comb p of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
241 |
(Const (name', _), args) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
242 |
if name = name' then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
243 |
if length args = k then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
244 |
((((prfx, args @ ps), rhs) :: in_group, not_in_group), |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
245 |
map2 default_name names args) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
246 |
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
|
247 |
else ((in_group, row :: not_in_group), names) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
248 |
| _ => raise CASE_ERROR ("Not a constructor pattern", i))) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
249 |
rows (([], []), replicate k "") |>> pairself rev |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
250 |
end; |
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 |
(* Partitioning *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
254 |
|
51675 | 255 |
fun partition _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1) |
52154 | 256 |
| 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
|
257 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
258 |
fun part [] [] = [] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
259 |
| 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
|
260 |
| part (c :: cs) rows = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
261 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
262 |
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
|
263 |
val used' = fold add_row_used in_group used; |
51675 | 264 |
val (c', gvars) = fresh_constr colty used' c; |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
265 |
val in_group' = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
266 |
if null in_group (* Constructor not given *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
267 |
then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
268 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
269 |
val Ts = map fastype_of ps; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
270 |
val (xs, _) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
271 |
fold_map Name.variant |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
272 |
(replicate (length ps) "x") |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
273 |
(fold Term.declare_term_frees gvars used'); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
274 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
275 |
[((prfx, gvars @ map Free (xs ~~ Ts)), |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
276 |
(Const (@{const_name undefined}, res_ty), ~1))] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
277 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
278 |
else in_group; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
279 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
280 |
{constructor = c', |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
281 |
new_formals = gvars, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
282 |
names = names, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
283 |
group = in_group'} :: part cs not_in_group |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
284 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
285 |
in part constructors rows end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
286 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
287 |
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
|
288 |
| 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
|
289 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
290 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
291 |
(* Translation of pattern terms into nested case expressions. *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
292 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
293 |
fun mk_case ctxt used range_ty = |
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 get_info = lookup_by_constr_permissive ctxt; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
296 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
297 |
fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
298 |
| 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
|
299 |
if is_Free p then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
300 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
301 |
val used' = add_row_used row used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
302 |
fun expnd c = |
51675 | 303 |
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
|
304 |
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
|
305 |
in map expnd constructors end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
306 |
else [row]; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
307 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
308 |
val (name, _) = Name.variant "a" used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
309 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
310 |
fun mk _ [] = raise CASE_ERROR ("no rows", ~1) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
311 |
| mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
312 |
| mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
313 |
| mk (u :: us) (rows as ((_, _ :: _), _) :: _) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
314 |
let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in |
52154 | 315 |
(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
|
316 |
NONE => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
317 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
318 |
val rows' = map (fn ((v, _), row) => row ||> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
319 |
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
|
320 |
in mk us rows' end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
321 |
| SOME (Const (cname, cT), i) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
322 |
(case get_info (cname, cT) of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
323 |
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
|
324 |
| SOME (case_comb, constructors) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
325 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
326 |
val pty = body_type cT; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
327 |
val used' = fold Term.declare_term_frees us used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
328 |
val nrows = maps (expand constructors used' pty) rows; |
52154 | 329 |
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
|
330 |
val (pat_rect, dtrees) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
331 |
split_list (map (fn {new_formals, group, ...} => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
332 |
mk (new_formals @ us) group) subproblems); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
333 |
val case_functions = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
334 |
map2 (fn {new_formals, names, ...} => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
335 |
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
|
336 |
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
|
337 |
(new_formals ~~ names)) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
338 |
subproblems dtrees; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
339 |
val types = map fastype_of (case_functions @ [u]); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
340 |
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
|
341 |
val tree = list_comb (case_const, case_functions @ [u]); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
342 |
in (flat pat_rect, tree) end) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
343 |
| SOME (t, i) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
344 |
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
|
345 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
346 |
| mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
347 |
in mk end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
348 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
349 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
350 |
(*Repeated variable occurrences in a pattern are not allowed.*) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
351 |
fun no_repeat_vars ctxt pat = fold_aterms |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
352 |
(fn x as Free (s, _) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
353 |
(fn xs => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
354 |
if member op aconv xs x then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
355 |
case_error (quote s ^ " occurs repeatedly in the pattern " ^ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
356 |
quote (Syntax.string_of_term ctxt pat)) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
357 |
else x :: xs) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
358 |
| _ => I) pat []; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
359 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
360 |
fun make_case ctxt config used x clauses = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
361 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
362 |
fun string_of_clause (pat, rhs) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
363 |
Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
364 |
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
|
365 |
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
|
366 |
val rangeT = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
367 |
(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
|
368 |
[] => case_error "no clauses given" |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
369 |
| [T] => T |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
370 |
| _ => 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
|
371 |
val used' = fold add_row_used rows used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
372 |
val (tags, case_tm) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
373 |
mk_case ctxt used' rangeT [x] rows |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
374 |
handle CASE_ERROR (msg, i) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
375 |
case_error |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
376 |
(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
|
377 |
val _ = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
378 |
(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
|
379 |
[] => () |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
380 |
| is => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
381 |
(case config of Error => case_error | Warning => warning | Quiet => fn _ => ()) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
382 |
("The following clauses are redundant (covered by preceding clauses):\n" ^ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
383 |
cat_lines (map (string_of_clause o nth clauses) is))); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
384 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
385 |
case_tm |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
386 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
387 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
388 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
389 |
(* term check *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
390 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
391 |
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
|
392 |
let val (s', used') = Name.variant s used |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
393 |
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
|
394 |
| 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
|
395 |
(subst_bounds (xs, t), subst_bounds (xs, u)) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
396 |
| decode_clause _ _ _ = case_error "decode_clause"; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
397 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
398 |
fun decode_cases (Const (@{const_name case_nil}, _)) = [] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
399 |
| decode_cases (Const (@{const_name case_cons}, _) $ t $ u) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
400 |
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
|
401 |
decode_cases u |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
402 |
| decode_cases _ = case_error "decode_cases"; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
403 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
404 |
fun check_case ctxt = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
405 |
let |
51679
e7316560928b
disallow coercions to interfere with case translations
traytel
parents:
51678
diff
changeset
|
406 |
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
|
407 |
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
|
408 |
Name.context (decode_case u) (decode_cases t) |
51676 | 409 |
| decode_case (t $ u) = decode_case t $ decode_case u |
410 |
| decode_case (Abs (x, T, u)) = |
|
411 |
let val (x', u') = Term.dest_abs (x, T, u); |
|
412 |
in Term.absfree (x', T) (decode_case u') end |
|
413 |
| decode_case t = t; |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
414 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
415 |
map decode_case |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
416 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
417 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
418 |
val term_check_setup = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
419 |
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
|
420 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
421 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
422 |
(* Pretty printing of nested case expressions *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
423 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
424 |
(* destruct one level of pattern matching *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
425 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
426 |
fun dest_case ctxt d used t = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
427 |
(case apfst name_of (strip_comb t) of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
428 |
(SOME cname, ts as _ :: _) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
429 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
430 |
val (fs, x) = split_last ts; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
431 |
fun strip_abs i Us t = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
432 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
433 |
val zs = strip_abs_vars t; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
434 |
val j = length zs; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
435 |
val (xs, ys) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
436 |
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
|
437 |
else chop i zs; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
438 |
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
|
439 |
val xs' = map Free |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
440 |
((fold_map Name.variant (map fst xs) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
441 |
(Term.declare_term_names u used) |> fst) ~~ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
442 |
map snd xs); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
443 |
val (xs1, xs2) = chop j xs' |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
444 |
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
|
445 |
fun is_dependent i t = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
446 |
let val k = length (strip_abs_vars t) - i |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
447 |
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
|
448 |
fun count_cases (_, _, true) = I |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
449 |
| 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
|
450 |
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
|
451 |
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
|
452 |
val get_info = lookup_by_case ctxt; |
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 |
(case get_info cname of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
455 |
SOME (_, constructors) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
456 |
if length fs = length constructors then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
457 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
458 |
val cases = map (fn (Const (s, U), t) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
459 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
460 |
val Us = binder_types U; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
461 |
val k = length Us; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
462 |
val p as (xs, _) = strip_abs k Us t; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
463 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
464 |
(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
|
465 |
end) (constructors ~~ fs); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
466 |
val cases' = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
467 |
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
|
468 |
(fold_rev count_cases cases []); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
469 |
val R = fastype_of t; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
470 |
val dummy = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
471 |
if d then Term.dummy_pattern R |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
472 |
else Free (Name.variant "x" used |> fst, R); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
473 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
474 |
SOME (x, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
475 |
map mk_case |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
476 |
(case find_first (is_undefined o fst) cases' of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
477 |
SOME (_, cs) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
478 |
if length cs = length constructors then [hd cases] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
479 |
else filter_out (fn (_, (_, body), _) => is_undefined body) cases |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
480 |
| NONE => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
481 |
(case cases' of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
482 |
[] => cases |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
483 |
| (default, cs) :: _ => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
484 |
if length cs = 1 then cases |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
485 |
else if length cs = length constructors then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
486 |
[hd cases, (dummy, ([], default), false)] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
487 |
else |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
488 |
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
|
489 |
[(dummy, ([], default), false)]))) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
490 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
491 |
else NONE |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
492 |
| _ => NONE) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
493 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
494 |
| _ => NONE); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
495 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
496 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
497 |
(* destruct nested patterns *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
498 |
|
51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
499 |
fun encode_clause recur S T (pat, rhs) = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
500 |
fold (fn x as (_, U) => fn t => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
501 |
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
|
502 |
(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
|
503 |
(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
|
504 |
|
51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
505 |
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
|
506 |
| encode_cases recur S T (p :: ps) = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
507 |
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
|
508 |
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
|
509 |
|
51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
510 |
fun encode_case recur (t, ps as (pat, rhs) :: _) = |
52154 | 511 |
let |
512 |
val tT = fastype_of t; |
|
513 |
val T = fastype_of rhs; |
|
514 |
in |
|
515 |
Const (@{const_name case_guard}, @{typ bool} --> tT --> (tT --> T) --> T) $ |
|
516 |
@{term True} $ t $ (encode_cases recur (fastype_of pat) (fastype_of rhs) ps) |
|
517 |
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
|
518 |
| encode_case _ _ = case_error "encode_case"; |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
519 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
520 |
fun strip_case' ctxt d (pat, rhs) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
521 |
(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
|
522 |
SOME (exp as Free _, clauses) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
523 |
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
|
524 |
not (exists (fn (_, rhs') => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
525 |
Term.exists_subterm (curry (op aconv) exp) rhs') clauses) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
526 |
then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
527 |
maps (strip_case' ctxt d) (map (fn (pat', rhs') => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
528 |
(subst_free [(exp, pat')] pat, rhs')) clauses) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
529 |
else [(pat, rhs)] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
530 |
| _ => [(pat, rhs)]); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
531 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
532 |
fun strip_case ctxt d t = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
533 |
(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
|
534 |
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
|
535 |
| 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
|
536 |
|
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
537 |
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
|
538 |
(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
|
539 |
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
|
540 |
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
|
541 |
(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
|
542 |
| 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
|
543 |
(case t of |
52154 | 544 |
t $ u => strip_case_full ctxt d t $ strip_case_full ctxt d u |
545 |
| 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
|
546 |
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
|
547 |
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
|
548 |
| _ => t)); |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
549 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
550 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
551 |
(* term uncheck *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
552 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
553 |
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
|
554 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
555 |
fun uncheck_case ctxt ts = |
51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
556 |
if Config.get ctxt show_cases then map (strip_case_full ctxt true) ts else ts; |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
557 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
558 |
val term_uncheck_setup = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
559 |
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
|
560 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
561 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
562 |
(* theory setup *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
563 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
564 |
val setup = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
565 |
trfun_setup #> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
566 |
trfun_setup' #> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
567 |
term_check_setup #> |
51681 | 568 |
term_uncheck_setup #> |
569 |
Attrib.setup @{binding case_translation} |
|
570 |
(Args.term -- Scan.repeat1 Args.term >> |
|
571 |
(fn (t, ts) => Thm.declaration_attribute (K (register t ts)))) |
|
572 |
"declaration of case combinators and constructors"; |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
573 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
574 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
575 |
(* outer syntax commands *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
576 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
577 |
fun print_case_translations ctxt = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
578 |
let |
52155 | 579 |
val cases = map snd (Symtab.dest (cases_of ctxt)); |
580 |
val type_space = Proof_Context.type_space ctxt; |
|
581 |
||
582 |
val pretty_term = Syntax.pretty_term ctxt; |
|
583 |
||
584 |
fun pretty_data (data as (comb, ctrs)) = |
|
585 |
let |
|
586 |
val name = Tname_of_data data; |
|
587 |
val xname = Name_Space.extern ctxt type_space name; |
|
588 |
val markup = Name_Space.markup type_space name; |
|
589 |
val prt = |
|
590 |
(Pretty.block o Pretty.fbreaks) |
|
591 |
[Pretty.block [Pretty.mark_str (markup, xname), Pretty.str ":"], |
|
592 |
Pretty.block [Pretty.str "combinator:", Pretty.brk 1, pretty_term comb], |
|
593 |
Pretty.block (Pretty.str "constructors:" :: Pretty.brk 1 :: |
|
594 |
Pretty.commas (map pretty_term ctrs))]; |
|
595 |
in (xname, prt) end; |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
596 |
in |
52155 | 597 |
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
|
598 |
|> Pretty.writeln |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
599 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
600 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
601 |
val _ = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
602 |
Outer_Syntax.improper_command @{command_spec "print_case_translations"} |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
603 |
"print registered case combinators and constructors" |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
604 |
(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
|
605 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
606 |
end; |