author  wenzelm 
Fri, 07 Mar 2014 10:22:27 +0100  
changeset 55971  7644d63e8c3f 
parent 55444  ec73f81e49e7 
child 55974  c835a9379026 
permissions  rwrr 
54701  1 
(* Title: HOL/Tools/Ctr_Sugar/case_translation.ML 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

2 
Author: Konrad Slind, Cambridge University Computer Laboratory 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

3 
Author: Stefan Berghofer, TU Muenchen 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

4 
Author: Dmitriy Traytel, TU Muenchen 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

5 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

6 
Nested case expressions via a generic data slot for case combinators and constructors. 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

7 
*) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

8 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

9 
signature CASE_TRANSLATION = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

10 
sig 
54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

11 
val indexify_names: string list > string list 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

12 
val make_tnames: typ list > string list 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

13 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

14 
datatype config = Error  Warning  Quiet 
51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset

15 
val case_tr: bool > Proof.context > term list > term 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

16 
val lookup_by_constr: Proof.context > string * typ > (term * term list) option 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

17 
val lookup_by_constr_permissive: Proof.context > string * typ > (term * term list) option 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

18 
val lookup_by_case: Proof.context > string > (term * term list) option 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

19 
val make_case: Proof.context > config > Name.context > term > (term * term) list > term 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

20 
val print_case_translations: Proof.context > unit 
51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset

21 
val strip_case: Proof.context > bool > term > (term * (term * term) list) option 
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset

22 
val strip_case_full: Proof.context > bool > term > term 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

23 
val show_cases: bool Config.T 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

24 
val register: term > term list > Context.generic > Context.generic 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

25 
end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

26 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

27 
structure Case_Translation: CASE_TRANSLATION = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

28 
struct 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

29 

54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

30 
(** general utilities **) 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

31 

100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

32 
fun indexify_names names = 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

33 
let 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

34 
fun index (x :: xs) tab = 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

35 
(case AList.lookup (op =) tab x of 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

36 
NONE => 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

37 
if member (op =) xs x 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

38 
then (x ^ "1") :: index xs ((x, 2) :: tab) 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

39 
else x :: index xs tab 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

40 
 SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab)) 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

41 
 index [] _ = []; 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

42 
in index names [] end; 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

43 

100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

44 
fun make_tnames Ts = 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

45 
let 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

46 
fun type_name (TFree (name, _)) = unprefix "'" name 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

47 
 type_name (Type (name, _)) = 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

48 
let val name' = Long_Name.base_name name 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

49 
in if Symbol_Pos.is_identifier name' then name' else "x" end; 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

50 
in indexify_names (map type_name Ts) end; 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

51 

100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

52 

100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

53 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

54 
(** data management **) 
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 
datatype data = Data of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

57 
{constrs: (string * (term * term list)) list Symtab.table, 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

58 
cases: (term * term list) Symtab.table}; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

59 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

60 
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

61 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

62 
structure Data = Generic_Data 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

63 
( 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

64 
type T = data; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

65 
val empty = make_data (Symtab.empty, Symtab.empty); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

66 
val extend = I; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

67 
fun merge 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

68 
(Data {constrs = constrs1, cases = cases1}, 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

69 
Data {constrs = constrs2, cases = cases2}) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

70 
make_data 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

71 
(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

72 
Symtab.merge (K true) (cases1, cases2)); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

73 
); 
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 map_data f = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

76 
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

77 
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

78 
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

79 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

80 
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

81 

51684  82 
fun T_of_data (comb, constrs : term list) = 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

83 
fastype_of comb 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

84 
> funpow (length constrs) range_type 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

85 
> domain_type; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

86 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

87 
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

88 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

89 
val constrs_of = #constrs o rep_data; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

90 
val cases_of = #cases o rep_data; 
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 
fun lookup_by_constr ctxt (c, T) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

93 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

94 
val tab = Symtab.lookup_list (constrs_of ctxt) c; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

95 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

96 
(case body_type T of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

97 
Type (tyco, _) => AList.lookup (op =) tab tyco 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

98 
 _ => NONE) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

99 
end; 
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 lookup_by_constr_permissive ctxt (c, T) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

102 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

103 
val tab = Symtab.lookup_list (constrs_of ctxt) c; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

104 
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

105 
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

106 
(*conservative wrt. overloaded constructors*) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

107 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

108 
(case hint of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

109 
NONE => default 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

110 
 SOME tyco => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

111 
(case AList.lookup (op =) tab tyco of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

112 
NONE => default (*permissive*) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

113 
 SOME info => SOME info)) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

114 
end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

115 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

116 
val lookup_by_case = Symtab.lookup o cases_of; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

117 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

118 

52154  119 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

120 
(** installation **) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

121 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

122 
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

123 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

124 
val name_of = try (dest_Const #> fst); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

125 

52154  126 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

127 
(* parse translation *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

128 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

129 
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

130 

51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset

131 
fun case_tr err ctxt [t, u] = 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

132 
let 
52157  133 
val consts = Proof_Context.consts_of ctxt; 
134 
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

135 

52158
d5fa81343322
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents:
52157
diff
changeset

136 
fun variant_free x used = 
d5fa81343322
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents:
52157
diff
changeset

137 
let val (x', used') = Name.variant x used 
d5fa81343322
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents:
52157
diff
changeset

138 
in if is_const x' then variant_free x' used' else (x', used') end; 
d5fa81343322
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents:
52157
diff
changeset

139 

52157  140 
fun abs p tTs t = 
141 
Syntax.const @{const_syntax case_abs} $ 

142 
fold constrain_Abs tTs (absfree p t); 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

143 

51693  144 
fun abs_pat (Const (@{syntax_const "_constrain"}, _) $ t $ tT) tTs = 
145 
abs_pat t (tT :: tTs) 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

146 
 abs_pat (Free (p as (x, _))) tTs = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

147 
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

148 
 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

149 
 abs_pat _ _ = I; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

150 

51680
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

151 
(* replace occurrences of dummy_pattern by distinct variables *) 
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

152 
fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used = 
52158
d5fa81343322
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm
parents:
52157
diff
changeset

153 
let val (x, used') = variant_free "x" used 
51680
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

154 
in (Free (x, T), used') end 
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

155 
 replace_dummies (t $ u) used = 
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

156 
let 
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

157 
val (t', used') = replace_dummies t used; 
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

158 
val (u', used'') = replace_dummies u used'; 
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

159 
in (t' $ u', used'') end 
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

160 
 replace_dummies t used = (t, used); 
8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

161 

8b8cd5a527bc
Handle dummy patterns in parse translation rather than check phase
berghofe
parents:
51679
diff
changeset

162 
fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) = 
52154  163 
let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context) in 
164 
abs_pat l' [] 

165 
(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

166 
end 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

167 
 dest_case1 _ = case_error "dest_case1"; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

168 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

169 
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

170 
 dest_case2 t = [t]; 
51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset

171 

1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset

172 
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

173 
in 
52154  174 
Syntax.const @{const_syntax case_guard} $ errt $ t $ 
175 
(fold_rev 

176 
(fn t => fn u => Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u) 

177 
(dest_case2 u) 

178 
(Syntax.const @{const_syntax case_nil})) 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

179 
end 
51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51677
diff
changeset

180 
 case_tr _ _ _ = case_error "case_tr"; 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

181 

55971  182 
val _ = Theory.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

183 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

184 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

185 
(* print translation *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

186 

51751
cf039b3c42a7
slightly more aggressive syntax translation for printing case expressions
traytel
parents:
51693
diff
changeset

187 
fun case_tr' (_ :: x :: t :: ts) = 
52159  188 
let 
189 
fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used = 

190 
let val (s', used') = Name.variant s used 

191 
in mk_clause t ((s', T) :: xs) used' end 

192 
 mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ = 

193 
Syntax.const @{syntax_const "_case1"} $ 

194 
subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $ 

195 
subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs) 

196 
 mk_clause _ _ _ = raise Match; 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

197 

52159  198 
fun mk_clauses (Const (@{const_syntax case_nil}, _)) = [] 
199 
 mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) = 

200 
mk_clause t [] (Term.declare_term_frees t Name.context) :: mk_clauses u 

201 
 mk_clauses _ = raise Match; 

202 
in 

203 
list_comb (Syntax.const @{syntax_const "_case_syntax"} $ x $ 

204 
foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u) 

205 
(mk_clauses t), ts) 

206 
end 

207 
 case_tr' _ = raise Match; 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

208 

55971  209 
val _ = Theory.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

210 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

211 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

212 
(* declarations *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

213 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

214 
fun register raw_case_comb raw_constrs context = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

215 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

216 
val ctxt = Context.proof_of context; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

217 
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

218 
val constrs = Variable.polymorphic ctxt raw_constrs; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

219 
val case_key = case_comb > dest_Const > fst; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

220 
val constr_keys = map (fst o dest_Const) constrs; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

221 
val data = (case_comb, constrs); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

222 
val Tname = Tname_of_data data; 
55444
ec73f81e49e7
iteration n in the 'default' vs. 'update_new' vs. 'update' saga  'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents:
55392
diff
changeset

223 
val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys; 
ec73f81e49e7
iteration n in the 'default' vs. 'update_new' vs. 'update' saga  'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents:
55392
diff
changeset

224 
val update_cases = Symtab.update (case_key, data); 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

225 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

226 
context 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

227 
> map_constrs update_constrs 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

228 
> map_cases update_cases 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

229 
end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

230 

55971  231 
val _ = Theory.setup 
232 
(Attrib.setup @{binding case_translation} 

233 
(Args.term  Scan.repeat1 Args.term >> 

234 
(fn (t, ts) => Thm.declaration_attribute (K (register t ts)))) 

235 
"declaration of case combinators and constructors"); 

236 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

237 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

238 
(* (Un)check phases *) 
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 
datatype config = Error  Warning  Quiet; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

241 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

242 
exception CASE_ERROR of string * int; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

243 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

244 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

245 
(*Each pattern carries with it a tag i, which denotes the clause it 
52154  246 
came from. i = ~1 indicates that the clause was added by pattern 
247 
completion.*) 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

248 

52159  249 
fun add_row_used ((prfx, pats), (tm, _)) = 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

250 
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

251 

52154  252 
(*try to preserve names given by user*) 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

253 
fun default_name "" (Free (name', _)) = name' 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

254 
 default_name name _ = name; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

255 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

256 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

257 
(*Produce an instance of a constructor, plus fresh variables for its arguments.*) 
51675  258 
fun fresh_constr colty used c = 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

259 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

260 
val (_, T) = dest_Const c; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

261 
val Ts = binder_types T; 
52154  262 
val (names, _) = 
54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52705
diff
changeset

263 
fold_map Name.variant (make_tnames (map Logic.unvarifyT_global Ts)) used; 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

264 
val ty = body_type T; 
51675  265 
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

266 
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

267 
val c' = Envir.subst_term_types ty_theta c; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

268 
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

269 
in (c', gvars) end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

270 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

271 
(*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

272 
pattern with constructor = name.*) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

273 
fun mk_group (name, T) rows = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

274 
let val k = length (binder_types T) in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

275 
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

276 
fn ((in_group, not_in_group), names) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

277 
(case strip_comb p of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

278 
(Const (name', _), args) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

279 
if name = name' then 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

280 
if length args = k then 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

281 
((((prfx, args @ ps), rhs) :: in_group, not_in_group), 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

282 
map2 default_name names args) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

283 
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

284 
else ((in_group, row :: not_in_group), names) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

285 
 _ => raise CASE_ERROR ("Not a constructor pattern", i))) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

286 
rows (([], []), replicate k "") >> pairself rev 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

287 
end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

288 

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 
(* Partitioning *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

291 

51675  292 
fun partition _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1) 
52154  293 
 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

294 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

295 
fun part [] [] = [] 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

296 
 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

297 
 part (c :: cs) rows = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

298 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

299 
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

300 
val used' = fold add_row_used in_group used; 
51675  301 
val (c', gvars) = fresh_constr colty used' c; 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

302 
val in_group' = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

303 
if null in_group (* Constructor not given *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

304 
then 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

305 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

306 
val Ts = map fastype_of ps; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

307 
val (xs, _) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

308 
fold_map Name.variant 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

309 
(replicate (length ps) "x") 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

310 
(fold Term.declare_term_frees gvars used'); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

311 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

312 
[((prfx, gvars @ map Free (xs ~~ Ts)), 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

313 
(Const (@{const_name undefined}, res_ty), ~1))] 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

314 
end 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

315 
else in_group; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

316 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

317 
{constructor = c', 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

318 
new_formals = gvars, 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

319 
names = names, 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

320 
group = in_group'} :: part cs not_in_group 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

321 
end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

322 
in part constructors rows end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

323 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

324 
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

325 
 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

326 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

327 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

328 
(* Translation of pattern terms into nested case expressions. *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

329 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

330 
fun mk_case ctxt used range_ty = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

331 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

332 
val get_info = lookup_by_constr_permissive ctxt; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

333 

52159  334 
fun expand _ _ _ ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1) 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

335 
 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

336 
if is_Free p then 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

337 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

338 
val used' = add_row_used row used; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

339 
fun expnd c = 
51675  340 
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

341 
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

342 
in map expnd constructors end 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

343 
else [row]; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

344 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

345 
val (name, _) = Name.variant "a" used; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

346 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

347 
fun mk _ [] = raise CASE_ERROR ("no rows", ~1) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

348 
 mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *) 
52159  349 
 mk path ((row as ((_, [Free _]), _)) :: _ :: _) = mk path [row] 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

350 
 mk (u :: us) (rows as ((_, _ :: _), _) :: _) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

351 
let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in 
52154  352 
(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

353 
NONE => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

354 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

355 
val rows' = map (fn ((v, _), row) => row > 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

356 
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

357 
in mk us rows' end 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

358 
 SOME (Const (cname, cT), i) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

359 
(case get_info (cname, cT) of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

360 
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

361 
 SOME (case_comb, constructors) => 
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 
val pty = body_type cT; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

364 
val used' = fold Term.declare_term_frees us used; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

365 
val nrows = maps (expand constructors used' pty) rows; 
52154  366 
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

367 
val (pat_rect, dtrees) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

368 
split_list (map (fn {new_formals, group, ...} => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

369 
mk (new_formals @ us) group) subproblems); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

370 
val case_functions = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

371 
map2 (fn {new_formals, names, ...} => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

372 
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

373 
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

374 
(new_formals ~~ names)) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

375 
subproblems dtrees; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

376 
val types = map fastype_of (case_functions @ [u]); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

377 
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

378 
val tree = list_comb (case_const, case_functions @ [u]); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

379 
in (flat pat_rect, tree) end) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

380 
 SOME (t, i) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

381 
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

382 
end 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

383 
 mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

384 
in mk end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

385 

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 
(*Repeated variable occurrences in a pattern are not allowed.*) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

388 
fun no_repeat_vars ctxt pat = fold_aterms 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

389 
(fn x as Free (s, _) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

390 
(fn xs => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

391 
if member op aconv xs x then 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

392 
case_error (quote s ^ " occurs repeatedly in the pattern " ^ 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

393 
quote (Syntax.string_of_term ctxt pat)) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

394 
else x :: xs) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

395 
 _ => I) pat []; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

396 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

397 
fun make_case ctxt config used x clauses = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

398 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

399 
fun string_of_clause (pat, rhs) = 
52705
c12602c1b13b
do not apply string_of_term to dummytyped syntactic constants (ensures that uncheck phases work on welltyped terms)
traytel
parents:
52690
diff
changeset

400 
Syntax.unparse_term ctxt 
c12602c1b13b
do not apply string_of_term to dummytyped syntactic constants (ensures that uncheck phases work on welltyped terms)
traytel
parents:
52690
diff
changeset

401 
(Term.list_comb (Syntax.const @{syntax_const "_case1"}, 
c12602c1b13b
do not apply string_of_term to dummytyped syntactic constants (ensures that uncheck phases work on welltyped terms)
traytel
parents:
52690
diff
changeset

402 
Syntax.uncheck_terms ctxt [pat, rhs])) 
c12602c1b13b
do not apply string_of_term to dummytyped syntactic constants (ensures that uncheck phases work on welltyped terms)
traytel
parents:
52690
diff
changeset

403 
> Pretty.string_of; 
52690
2fa3110539a5
more opportunistic string_of_clause, to make doublesure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);
wenzelm
parents:
52685
diff
changeset

404 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

405 
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

406 
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

407 
val rangeT = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

408 
(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

409 
[] => case_error "no clauses given" 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

410 
 [T] => T 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

411 
 _ => 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

412 
val used' = fold add_row_used rows used; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

413 
val (tags, case_tm) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

414 
mk_case ctxt used' rangeT [x] rows 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

415 
handle CASE_ERROR (msg, i) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

416 
case_error 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

417 
(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

418 
val _ = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

419 
(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

420 
[] => () 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

421 
 is => 
52685
554d684d8520
nonstrict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to illtyped use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
wenzelm
parents:
52285
diff
changeset

422 
if config = Quiet then () 
554d684d8520
nonstrict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to illtyped use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
wenzelm
parents:
52285
diff
changeset

423 
else 
52690
2fa3110539a5
more opportunistic string_of_clause, to make doublesure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);
wenzelm
parents:
52685
diff
changeset

424 
(if config = Error then case_error else warning (*FIXME lack of syntactic context!?*)) 
52685
554d684d8520
nonstrict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to illtyped use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
wenzelm
parents:
52285
diff
changeset

425 
("The following clauses are redundant (covered by preceding clauses):\n" ^ 
554d684d8520
nonstrict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to illtyped use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
wenzelm
parents:
52285
diff
changeset

426 
cat_lines (map (string_of_clause o nth clauses) is))); 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

427 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

428 
case_tm 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

429 
end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

430 

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 
(* term check *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

433 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

434 
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

435 
let val (s', used') = Name.variant s used 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

436 
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

437 
 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

438 
(subst_bounds (xs, t), subst_bounds (xs, u)) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

439 
 decode_clause _ _ _ = case_error "decode_clause"; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

440 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

441 
fun decode_cases (Const (@{const_name case_nil}, _)) = [] 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

442 
 decode_cases (Const (@{const_name case_cons}, _) $ t $ u) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

443 
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

444 
decode_cases u 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

445 
 decode_cases _ = case_error "decode_cases"; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

446 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

447 
fun check_case ctxt = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

448 
let 
51679
e7316560928b
disallow coercions to interfere with case translations
traytel
parents:
51678
diff
changeset

449 
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

450 
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

451 
Name.context (decode_case u) (decode_cases t) 
51676  452 
 decode_case (t $ u) = decode_case t $ decode_case u 
453 
 decode_case (Abs (x, T, u)) = 

454 
let val (x', u') = Term.dest_abs (x, T, u); 

455 
in Term.absfree (x', T) (decode_case u') end 

456 
 decode_case t = t; 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

457 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

458 
map decode_case 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

459 
end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

460 

55971  461 
val _ = Context.>> (Syntax_Phases.term_check 1 "case" check_case); 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

462 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

463 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

464 
(* Pretty printing of nested case expressions *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

465 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

466 
(* destruct one level of pattern matching *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

467 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

468 
fun dest_case ctxt d used t = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

469 
(case apfst name_of (strip_comb t) of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

470 
(SOME cname, ts as _ :: _) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

471 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

472 
val (fs, x) = split_last ts; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

473 
fun strip_abs i Us t = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

474 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

475 
val zs = strip_abs_vars t; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

476 
val j = length zs; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

477 
val (xs, ys) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

478 
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

479 
else chop i zs; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

480 
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

481 
val xs' = map Free 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

482 
((fold_map Name.variant (map fst xs) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

483 
(Term.declare_term_names u used) > fst) ~~ 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

484 
map snd xs); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

485 
val (xs1, xs2) = chop j xs' 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

486 
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

487 
fun is_dependent i t = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

488 
let val k = length (strip_abs_vars t)  i 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

489 
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

490 
fun count_cases (_, _, true) = I 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

491 
 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

492 
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

493 
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

494 
val get_info = lookup_by_case ctxt; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

495 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

496 
(case get_info cname of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

497 
SOME (_, constructors) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

498 
if length fs = length constructors then 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

499 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

500 
val cases = map (fn (Const (s, U), t) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

501 
let 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

502 
val Us = binder_types U; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

503 
val k = length Us; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

504 
val p as (xs, _) = strip_abs k Us t; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

505 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

506 
(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

507 
end) (constructors ~~ fs); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

508 
val cases' = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

509 
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

510 
(fold_rev count_cases cases []); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

511 
val R = fastype_of t; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

512 
val dummy = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

513 
if d then Term.dummy_pattern R 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

514 
else Free (Name.variant "x" used > fst, R); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

515 
in 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

516 
SOME (x, 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

517 
map mk_case 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

518 
(case find_first (is_undefined o fst) cases' of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

519 
SOME (_, cs) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

520 
if length cs = length constructors then [hd cases] 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

521 
else filter_out (fn (_, (_, body), _) => is_undefined body) cases 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

522 
 NONE => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

523 
(case cases' of 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

524 
[] => cases 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

525 
 (default, cs) :: _ => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

526 
if length cs = 1 then cases 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

527 
else if length cs = length constructors then 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

528 
[hd cases, (dummy, ([], default), false)] 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

529 
else 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

530 
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

531 
[(dummy, ([], default), false)]))) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

532 
end 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

533 
else NONE 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

534 
 _ => NONE) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

535 
end 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

536 
 _ => NONE); 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

537 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

538 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

539 
(* destruct nested patterns *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

540 

51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset

541 
fun encode_clause recur S T (pat, rhs) = 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

542 
fold (fn x as (_, U) => fn t => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

543 
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

544 
(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

545 
(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

546 

51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset

547 
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

548 
 encode_cases recur S T (p :: ps) = 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

549 
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

550 
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

551 

51677
d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset

552 
fun encode_case recur (t, ps as (pat, rhs) :: _) = 
52154  553 
let 
554 
val tT = fastype_of t; 

555 
val T = fastype_of rhs; 

556 
in 

557 
Const (@{const_name case_guard}, @{typ bool} > tT > (tT > T) > T) $ 

558 
@{term True} $ t $ (encode_cases recur (fastype_of pat) (fastype_of rhs) ps) 

559 
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

560 
 encode_case _ _ = case_error "encode_case"; 
51673
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 
fun strip_case' ctxt d (pat, rhs) = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

563 
(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

564 
SOME (exp as Free _, clauses) => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

565 
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

566 
not (exists (fn (_, rhs') => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

567 
Term.exists_subterm (curry (op aconv) exp) rhs') clauses) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

568 
then 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

569 
maps (strip_case' ctxt d) (map (fn (pat', rhs') => 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

570 
(subst_free [(exp, pat')] pat, rhs')) clauses) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

571 
else [(pat, rhs)] 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

572 
 _ => [(pat, rhs)]); 
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 
fun strip_case ctxt d t = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

575 
(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

576 
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

577 
 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

578 

d2b3372e6033
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
traytel
parents:
51676
diff
changeset

579 
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

580 
(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

581 
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

582 
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

583 
(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

584 
 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

585 
(case t of 
52154  586 
t $ u => strip_case_full ctxt d t $ strip_case_full ctxt d u 
587 
 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

588 
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

589 
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

590 
 _ => t)); 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

591 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

592 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

593 
(* term uncheck *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

594 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

595 
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

596 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

597 
fun uncheck_case ctxt ts = 
52285
da42b500a6aa
permissive uncheck  allow printing of malformed terms (e.g. in error messages);
wenzelm
parents:
52265
diff
changeset

598 
if Config.get ctxt show_cases 
da42b500a6aa
permissive uncheck  allow printing of malformed terms (e.g. in error messages);
wenzelm
parents:
52265
diff
changeset

599 
then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts 
da42b500a6aa
permissive uncheck  allow printing of malformed terms (e.g. in error messages);
wenzelm
parents:
52265
diff
changeset

600 
else ts; 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

601 

55971  602 
val _ = Context.>> (Syntax_Phases.term_uncheck 1 "case" uncheck_case); 
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

603 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

604 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

605 
(* outer syntax commands *) 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

606 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

607 
fun print_case_translations ctxt = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

608 
let 
52155  609 
val cases = map snd (Symtab.dest (cases_of ctxt)); 
610 
val type_space = Proof_Context.type_space ctxt; 

611 

612 
val pretty_term = Syntax.pretty_term ctxt; 

613 

614 
fun pretty_data (data as (comb, ctrs)) = 

615 
let 

616 
val name = Tname_of_data data; 

617 
val xname = Name_Space.extern ctxt type_space name; 

618 
val markup = Name_Space.markup type_space name; 

619 
val prt = 

620 
(Pretty.block o Pretty.fbreaks) 

621 
[Pretty.block [Pretty.mark_str (markup, xname), Pretty.str ":"], 

622 
Pretty.block [Pretty.str "combinator:", Pretty.brk 1, pretty_term comb], 

623 
Pretty.block (Pretty.str "constructors:" :: Pretty.brk 1 :: 

624 
Pretty.commas (map pretty_term ctrs))]; 

625 
in (xname, prt) end; 

51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

626 
in 
52155  627 
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

628 
> Pretty.writeln 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

629 
end; 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

630 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

631 
val _ = 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

632 
Outer_Syntax.improper_command @{command_spec "print_case_translations"} 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

633 
"print registered case combinators and constructors" 
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

634 
(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

635 

4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
diff
changeset

636 
end; 