author | traytel |
Fri, 05 Apr 2013 22:08:42 +0200 | |
changeset 51677 | d2b3372e6033 |
parent 51676 | d602caf11e48 |
child 51678 | 1e33b81c328a |
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 |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
12 |
val case_tr: Proof.context -> term list -> term |
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 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
56 |
fun T_of_data (comb, constrs) = |
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 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
93 |
(** installation **) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
94 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
95 |
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
|
96 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
97 |
val name_of = try (dest_Const #> fst); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
98 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
99 |
(* parse translation *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
100 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
101 |
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
|
102 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
103 |
fun case_tr ctxt [t, u] = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
104 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
105 |
val thy = Proof_Context.theory_of ctxt; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
106 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
107 |
fun is_const s = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
108 |
Sign.declared_const thy (Proof_Context.intern_const ctxt s); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
109 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
110 |
fun abs p tTs t = Syntax.const @{const_syntax case_abs} $ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
111 |
fold constrain_Abs tTs (absfree p t); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
112 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
113 |
fun abs_pat (Const ("_constrain", _) $ t $ tT) tTs = abs_pat t (tT :: tTs) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
114 |
| abs_pat (Free (p as (x, _))) tTs = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
115 |
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
|
116 |
| 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
|
117 |
| abs_pat _ _ = I; |
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 |
fun dest_case1 (Const (@{syntax_const "_case1"}, _) $ l $ r) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
120 |
abs_pat l [] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
121 |
(Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l $ r) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
122 |
| dest_case1 _ = case_error "dest_case1"; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
123 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
124 |
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
|
125 |
| dest_case2 t = [t]; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
126 |
in |
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
127 |
Syntax.const @{const_syntax case_guard} $ (fold_rev |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
128 |
(fn t => fn u => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
129 |
Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
130 |
(dest_case2 u) |
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
131 |
(Syntax.const @{const_syntax case_nil}) $ t) |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
132 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
133 |
| case_tr _ _ = case_error "case_tr"; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
134 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
135 |
val trfun_setup = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
136 |
Sign.add_advanced_trfuns ([], |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
137 |
[(@{syntax_const "_case_syntax"}, case_tr)], |
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 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
140 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
141 |
(* print translation *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
142 |
|
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
143 |
fun case_tr' [tx] = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
144 |
let |
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
145 |
val (t, x) = Term.dest_comb tx; |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
146 |
fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
147 |
let val (s', used') = Name.variant s used |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
148 |
in mk_clause t ((s', T) :: xs) used' end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
149 |
| mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
150 |
Syntax.const @{syntax_const "_case1"} $ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
151 |
subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
152 |
subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs); |
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 |
fun mk_clauses (Const (@{const_syntax case_nil}, _)) = [] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
155 |
| mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
156 |
mk_clause t [] (Term.declare_term_frees t Name.context) :: |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
157 |
mk_clauses u |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
158 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
159 |
Syntax.const @{syntax_const "_case_syntax"} $ x $ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
160 |
foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u) |
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
161 |
(mk_clauses t) |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
162 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
163 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
164 |
val trfun_setup' = Sign.add_trfuns |
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
165 |
([], [], [(@{const_syntax "case_guard"}, case_tr')], []); |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
166 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
167 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
168 |
(* declarations *) |
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 register raw_case_comb raw_constrs context = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
171 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
172 |
val ctxt = Context.proof_of context; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
173 |
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
|
174 |
val constrs = Variable.polymorphic ctxt raw_constrs; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
175 |
val case_key = case_comb |> dest_Const |> fst; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
176 |
val constr_keys = map (fst o dest_Const) constrs; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
177 |
val data = (case_comb, constrs); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
178 |
val Tname = Tname_of_data data; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
179 |
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
|
180 |
val update_cases = Symtab.update (case_key, data); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
181 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
182 |
context |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
183 |
|> map_constrs update_constrs |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
184 |
|> map_cases update_cases |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
185 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
186 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
187 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
188 |
(* (Un)check phases *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
189 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
190 |
datatype config = Error | Warning | Quiet; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
191 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
192 |
exception CASE_ERROR of string * int; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
193 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
194 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
195 |
(*Each pattern carries with it a tag i, which denotes the clause it |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
196 |
came from. i = ~1 indicates that the clause was added by pattern |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
197 |
completion.*) |
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 |
fun add_row_used ((prfx, pats), (tm, tag)) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
200 |
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
|
201 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
202 |
(* try to preserve names given by user *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
203 |
fun default_name "" (Free (name', _)) = name' |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
204 |
| default_name name _ = name; |
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 |
(*Produce an instance of a constructor, plus fresh variables for its arguments.*) |
51675 | 208 |
fun fresh_constr colty used c = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
209 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
210 |
val (_, T) = dest_Const c; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
211 |
val Ts = binder_types T; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
212 |
val (names, _) = fold_map Name.variant |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
213 |
(Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
214 |
val ty = body_type T; |
51675 | 215 |
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
|
216 |
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
|
217 |
val c' = Envir.subst_term_types ty_theta c; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
218 |
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
|
219 |
in (c', gvars) end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
220 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
221 |
(*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
|
222 |
pattern with constructor = name.*) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
223 |
fun mk_group (name, T) rows = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
224 |
let val k = length (binder_types T) in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
225 |
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
|
226 |
fn ((in_group, not_in_group), names) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
227 |
(case strip_comb p of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
228 |
(Const (name', _), args) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
229 |
if name = name' then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
230 |
if length args = k then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
231 |
((((prfx, args @ ps), rhs) :: in_group, not_in_group), |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
232 |
map2 default_name names args) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
233 |
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
|
234 |
else ((in_group, row :: not_in_group), names) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
235 |
| _ => raise CASE_ERROR ("Not a constructor pattern", i))) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
236 |
rows (([], []), replicate k "") |>> pairself rev |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
237 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
238 |
|
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 |
(* Partitioning *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
241 |
|
51675 | 242 |
fun partition _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1) |
243 |
| partition used constructors colty res_ty |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
244 |
(rows as (((prfx, _ :: ps), _) :: _)) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
245 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
246 |
fun part [] [] = [] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
247 |
| 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
|
248 |
| part (c :: cs) rows = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
249 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
250 |
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
|
251 |
val used' = fold add_row_used in_group used; |
51675 | 252 |
val (c', gvars) = fresh_constr colty used' c; |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
253 |
val in_group' = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
254 |
if null in_group (* Constructor not given *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
255 |
then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
256 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
257 |
val Ts = map fastype_of ps; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
258 |
val (xs, _) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
259 |
fold_map Name.variant |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
260 |
(replicate (length ps) "x") |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
261 |
(fold Term.declare_term_frees gvars used'); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
262 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
263 |
[((prfx, gvars @ map Free (xs ~~ Ts)), |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
264 |
(Const (@{const_name undefined}, res_ty), ~1))] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
265 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
266 |
else in_group; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
267 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
268 |
{constructor = c', |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
269 |
new_formals = gvars, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
270 |
names = names, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
271 |
group = in_group'} :: part cs not_in_group |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
272 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
273 |
in part constructors rows end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
274 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
275 |
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
|
276 |
| 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
|
277 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
278 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
279 |
(* Translation of pattern terms into nested case expressions. *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
280 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
281 |
fun mk_case ctxt used range_ty = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
282 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
283 |
val get_info = lookup_by_constr_permissive ctxt; |
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 |
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
|
286 |
| 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
|
287 |
if is_Free p then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
288 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
289 |
val used' = add_row_used row used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
290 |
fun expnd c = |
51675 | 291 |
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
|
292 |
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
|
293 |
in map expnd constructors end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
294 |
else [row]; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
295 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
296 |
val (name, _) = Name.variant "a" used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
297 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
298 |
fun mk _ [] = raise CASE_ERROR ("no rows", ~1) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
299 |
| mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
300 |
| 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
|
301 |
| mk (u :: us) (rows as ((_, _ :: _), _) :: _) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
302 |
let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
303 |
(case Option.map (apfst head_of) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
304 |
(find_first (not o is_Free o fst) col0) of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
305 |
NONE => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
306 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
307 |
val rows' = map (fn ((v, _), row) => row ||> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
308 |
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
|
309 |
in mk us rows' end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
310 |
| SOME (Const (cname, cT), i) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
311 |
(case get_info (cname, cT) of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
312 |
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
|
313 |
| SOME (case_comb, constructors) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
314 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
315 |
val pty = body_type cT; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
316 |
val used' = fold Term.declare_term_frees us used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
317 |
val nrows = maps (expand constructors used' pty) rows; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
318 |
val subproblems = |
51675 | 319 |
partition used' constructors pty range_ty nrows; |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
320 |
val (pat_rect, dtrees) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
321 |
split_list (map (fn {new_formals, group, ...} => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
322 |
mk (new_formals @ us) group) subproblems); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
323 |
val case_functions = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
324 |
map2 (fn {new_formals, names, ...} => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
325 |
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
|
326 |
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
|
327 |
(new_formals ~~ names)) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
328 |
subproblems dtrees; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
329 |
val types = map fastype_of (case_functions @ [u]); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
330 |
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
|
331 |
val tree = list_comb (case_const, case_functions @ [u]); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
332 |
in (flat pat_rect, tree) end) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
333 |
| SOME (t, i) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
334 |
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
|
335 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
336 |
| mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
337 |
in mk end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
338 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
339 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
340 |
(* replace occurrences of dummy_pattern by distinct variables *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
341 |
fun replace_dummies (Const (@{const_name dummy_pattern}, T)) used = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
342 |
let val (x, used') = Name.variant "x" used |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
343 |
in (Free (x, T), used') end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
344 |
| replace_dummies (t $ u) used = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
345 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
346 |
val (t', used') = replace_dummies t used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
347 |
val (u', used'') = replace_dummies u used'; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
348 |
in (t' $ u', used'') end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
349 |
| replace_dummies t used = (t, used); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
350 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
351 |
(*Repeated variable occurrences in a pattern are not allowed.*) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
352 |
fun no_repeat_vars ctxt pat = fold_aterms |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
353 |
(fn x as Free (s, _) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
354 |
(fn xs => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
355 |
if member op aconv xs x then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
356 |
case_error (quote s ^ " occurs repeatedly in the pattern " ^ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
357 |
quote (Syntax.string_of_term ctxt pat)) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
358 |
else x :: xs) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
359 |
| _ => I) pat []; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
360 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
361 |
fun make_case ctxt config used x clauses = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
362 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
363 |
fun string_of_clause (pat, rhs) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
364 |
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
|
365 |
val _ = map (no_repeat_vars ctxt o fst) clauses; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
366 |
val (rows, used') = used |> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
367 |
fold (fn (pat, rhs) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
368 |
Term.declare_term_frees pat #> Term.declare_term_frees rhs) clauses |> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
369 |
fold_map (fn (i, (pat, rhs)) => fn used => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
370 |
let val (pat', used') = replace_dummies pat used |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
371 |
in ((([], [pat']), (rhs, i)), used') end) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
372 |
(map_index I clauses); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
373 |
val rangeT = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
374 |
(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
|
375 |
[] => case_error "no clauses given" |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
376 |
| [T] => T |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
377 |
| _ => 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
|
378 |
val used' = fold add_row_used rows used; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
379 |
val (tags, case_tm) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
380 |
mk_case ctxt used' rangeT [x] rows |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
381 |
handle CASE_ERROR (msg, i) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
382 |
case_error |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
383 |
(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
|
384 |
val _ = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
385 |
(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
|
386 |
[] => () |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
387 |
| is => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
388 |
(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
|
389 |
("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
|
390 |
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
|
391 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
392 |
case_tm |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
393 |
end; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
394 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
395 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
396 |
(* term check *) |
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_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
|
399 |
let val (s', used') = Name.variant s used |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
400 |
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
|
401 |
| 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
|
402 |
(subst_bounds (xs, t), subst_bounds (xs, u)) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
403 |
| decode_clause _ _ _ = case_error "decode_clause"; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
404 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
405 |
fun decode_cases (Const (@{const_name case_nil}, _)) = [] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
406 |
| decode_cases (Const (@{const_name case_cons}, _) $ t $ u) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
407 |
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
|
408 |
decode_cases u |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
409 |
| decode_cases _ = case_error "decode_cases"; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
410 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
411 |
fun check_case ctxt = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
412 |
let |
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
413 |
fun decode_case (Const (@{const_name case_guard}, _) $ (t $ u)) = |
51676 | 414 |
make_case ctxt Error Name.context (decode_case u) (decode_cases t) |
415 |
| decode_case (t $ u) = decode_case t $ decode_case u |
|
416 |
| decode_case (Abs (x, T, u)) = |
|
417 |
let val (x', u') = Term.dest_abs (x, T, u); |
|
418 |
in Term.absfree (x', T) (decode_case u') end |
|
419 |
| decode_case t = t; |
|
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
420 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
421 |
map decode_case |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
422 |
end; |
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 |
val term_check_setup = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
425 |
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
|
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 |
(* Pretty printing of nested case expressions *) |
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 |
(* destruct one level of pattern matching *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
431 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
432 |
fun dest_case ctxt d used t = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
433 |
(case apfst name_of (strip_comb t) of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
434 |
(SOME cname, ts as _ :: _) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
435 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
436 |
val (fs, x) = split_last ts; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
437 |
fun strip_abs i Us t = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
438 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
439 |
val zs = strip_abs_vars t; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
440 |
val j = length zs; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
441 |
val (xs, ys) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
442 |
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
|
443 |
else chop i zs; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
444 |
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
|
445 |
val xs' = map Free |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
446 |
((fold_map Name.variant (map fst xs) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
447 |
(Term.declare_term_names u used) |> fst) ~~ |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
448 |
map snd xs); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
449 |
val (xs1, xs2) = chop j xs' |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
450 |
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
|
451 |
fun is_dependent i t = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
452 |
let val k = length (strip_abs_vars t) - i |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
453 |
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
|
454 |
fun count_cases (_, _, true) = I |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
455 |
| 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
|
456 |
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
|
457 |
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
|
458 |
val get_info = lookup_by_case ctxt; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
459 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
460 |
(case get_info cname of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
461 |
SOME (_, constructors) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
462 |
if length fs = length constructors then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
463 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
464 |
val cases = map (fn (Const (s, U), t) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
465 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
466 |
val Us = binder_types U; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
467 |
val k = length Us; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
468 |
val p as (xs, _) = strip_abs k Us t; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
469 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
470 |
(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
|
471 |
end) (constructors ~~ fs); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
472 |
val cases' = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
473 |
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
|
474 |
(fold_rev count_cases cases []); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
475 |
val R = fastype_of t; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
476 |
val dummy = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
477 |
if d then Term.dummy_pattern R |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
478 |
else Free (Name.variant "x" used |> fst, R); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
479 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
480 |
SOME (x, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
481 |
map mk_case |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
482 |
(case find_first (is_undefined o fst) cases' of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
483 |
SOME (_, cs) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
484 |
if length cs = length constructors then [hd cases] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
485 |
else filter_out (fn (_, (_, body), _) => is_undefined body) cases |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
486 |
| NONE => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
487 |
(case cases' of |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
488 |
[] => cases |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
489 |
| (default, cs) :: _ => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
490 |
if length cs = 1 then cases |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
491 |
else if length cs = length constructors then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
492 |
[hd cases, (dummy, ([], default), false)] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
493 |
else |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
494 |
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
|
495 |
[(dummy, ([], default), false)]))) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
496 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
497 |
else NONE |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
498 |
| _ => NONE) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
499 |
end |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
500 |
| _ => NONE); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
501 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
502 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
503 |
(* destruct nested patterns *) |
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_clause recur S T (pat, rhs) = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
506 |
fold (fn x as (_, U) => fn t => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
507 |
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
|
508 |
(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
|
509 |
(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
|
510 |
|
51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
511 |
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
|
512 |
| encode_cases recur S T (p :: ps) = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
513 |
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
|
514 |
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
|
515 |
|
51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
516 |
fun encode_case recur (t, ps as (pat, rhs) :: _) = |
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
517 |
let |
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
518 |
val T = fastype_of rhs; |
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
519 |
in |
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
520 |
Const (@{const_name case_guard}, T --> 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
|
521 |
(encode_cases recur (fastype_of pat) (fastype_of rhs) ps $ t) |
51674
2b1498a2ce85
special constant to prevent eta-contraction of the check-phase syntax of case translations
traytel
parents:
51673
diff
changeset
|
522 |
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
|
523 |
| encode_case _ _ = case_error "encode_case"; |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
524 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
525 |
fun strip_case' ctxt d (pat, rhs) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
526 |
(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
|
527 |
SOME (exp as Free _, clauses) => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
528 |
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
|
529 |
not (exists (fn (_, rhs') => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
530 |
Term.exists_subterm (curry (op aconv) exp) rhs') clauses) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
531 |
then |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
532 |
maps (strip_case' ctxt d) (map (fn (pat', rhs') => |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
533 |
(subst_free [(exp, pat')] pat, rhs')) clauses) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
534 |
else [(pat, rhs)] |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
535 |
| _ => [(pat, rhs)]); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
536 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
537 |
fun strip_case ctxt d t = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
538 |
(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
|
539 |
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
|
540 |
| 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
|
541 |
|
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
542 |
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
|
543 |
(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
|
544 |
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
|
545 |
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
|
546 |
(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
|
547 |
| 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
|
548 |
(case 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
|
549 |
(t $ u) => strip_case_full ctxt d t $ strip_case_full ctxt d u |
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset
|
550 |
| (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
|
551 |
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
|
552 |
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
|
553 |
| _ => t)); |
51673
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 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
556 |
(* term uncheck *) |
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 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
|
559 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
560 |
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
|
561 |
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
|
562 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
563 |
val term_uncheck_setup = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
564 |
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
|
565 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
566 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
567 |
(* theory setup *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
568 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
569 |
val setup = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
570 |
trfun_setup #> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
571 |
trfun_setup' #> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
572 |
term_check_setup #> |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
573 |
term_uncheck_setup; |
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 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
576 |
(* outer syntax commands *) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
577 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
578 |
fun print_case_translations ctxt = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
579 |
let |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
580 |
val cases = Symtab.dest (cases_of ctxt); |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
581 |
fun show_case (_, data as (comb, ctrs)) = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
582 |
Pretty.big_list |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
583 |
(Pretty.string_of (Pretty.block [Pretty.str (Tname_of_data data), Pretty.str ":"])) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
584 |
[Pretty.block [Pretty.brk 3, Pretty.block |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
585 |
[Pretty.str "combinator:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt comb)]], |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
586 |
Pretty.block [Pretty.brk 3, Pretty.block |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
587 |
[Pretty.str "constructors:", Pretty.brk 1, |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
588 |
Pretty.list "" "" (map (Pretty.quote o Syntax.pretty_term ctxt) ctrs)]]]; |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
589 |
in |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
590 |
Pretty.big_list "Case translations:" (map show_case cases) |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
591 |
|> Pretty.writeln |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
592 |
end; |
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 |
val _ = |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
595 |
Outer_Syntax.improper_command @{command_spec "print_case_translations"} |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
596 |
"print registered case combinators and constructors" |
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
597 |
(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
|
598 |
|
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset
|
599 |
end; |