author  blanchet 
Thu, 25 Feb 2010 16:33:39 +0100  
changeset 35385  29f81babefd7 
parent 35384  88dbcfe75c45 
child 35386  45a4e19d3ebd 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_mono.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

3 
Copyright 2009, 2010 
33192  4 

35384  5 
Monotonicity inference for higherorder logic. 
33192  6 
*) 
7 

8 
signature NITPICK_MONO = 

9 
sig 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

10 
type hol_context = Nitpick_HOL.hol_context 
33192  11 

12 
val formulas_monotonic : 

35384  13 
hol_context > bool > typ > term list * term list * term > bool 
33192  14 
end; 
15 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

16 
structure Nitpick_Mono : NITPICK_MONO = 
33192  17 
struct 
18 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

19 
open Nitpick_Util 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

20 
open Nitpick_HOL 
33192  21 

22 
type var = int 

23 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

24 
datatype sign = Plus  Minus 
33192  25 
datatype sign_atom = S of sign  V of var 
26 

27 
type literal = var * sign 

28 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

29 
datatype mtyp = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

30 
MAlpha  
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

31 
MFun of mtyp * sign_atom * mtyp  
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

32 
MPair of mtyp * mtyp  
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

33 
MType of string * mtyp list  
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

34 
MRec of string * typ list 
33192  35 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

36 
datatype mterm = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

37 
MAtom of term * mtyp  
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

38 
MAbs of string * typ * mtyp * sign_atom * mterm  
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

39 
MApp of mterm * mterm 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

40 

29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

41 
type mdata = 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

42 
{hol_ctxt: hol_context, 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35079
diff
changeset

43 
binarize: bool, 
33192  44 
alpha_T: typ, 
45 
max_fresh: int Unsynchronized.ref, 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

46 
datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

47 
constr_cache: (styp * mtyp) list Unsynchronized.ref} 
33192  48 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

49 
exception MTYPE of string * mtyp list 
33192  50 

51 
(* string > unit *) 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

52 
fun print_g (_ : string) = () 
33192  53 

54 
(* var > string *) 

55 
val string_for_var = signed_string_of_int 

56 
(* string > var list > string *) 

57 
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>" 

58 
 string_for_vars sep xs = space_implode sep (map string_for_var xs) 

59 
fun subscript_string_for_vars sep xs = 

60 
if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>" 

61 

62 
(* sign > string *) 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

63 
fun string_for_sign Plus = "+" 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

64 
 string_for_sign Minus = "" 
33192  65 

66 
(* sign > sign > sign *) 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

67 
fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus 
33192  68 
(* sign > sign *) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

69 
val negate = xor Minus 
33192  70 

71 
(* sign_atom > string *) 

72 
fun string_for_sign_atom (S sn) = string_for_sign sn 

73 
 string_for_sign_atom (V j) = string_for_var j 

74 

75 
(* literal > string *) 

76 
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn 

77 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

78 
val bool_M = MType (@{type_name bool}, []) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

79 
val irrelevant_M = MType (nitpick_prefix ^ "irrelevant", []) 
33192  80 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

81 
(* mtyp > bool *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

82 
fun is_MRec (MRec _) = true 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

83 
 is_MRec _ = false 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

84 
(* mtyp > mtyp * sign_atom * mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

85 
fun dest_MFun (MFun z) = z 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

86 
 dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M]) 
33192  87 

88 
val no_prec = 100 

89 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

90 
(* mtyp > int *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

91 
fun precedence_of_mtype (MFun _) = 1 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

92 
 precedence_of_mtype (MPair _) = 2 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

93 
 precedence_of_mtype _ = no_prec 
33192  94 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

95 
(* mtyp > string *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

96 
val string_for_mtype = 
33192  97 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

98 
(* int > mtyp > string *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

99 
fun aux outer_prec M = 
33192  100 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

101 
val prec = precedence_of_mtype M 
33192  102 
val need_parens = (prec < outer_prec) 
103 
in 

104 
(if need_parens then "(" else "") ^ 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

105 
(case M of 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

106 
MAlpha => "\<alpha>" 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

107 
 MFun (M1, a, M2) => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

108 
aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

109 
string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

110 
 MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

111 
 MType (s, []) => 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

112 
if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

113 
 MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

114 
 MRec (s, _) => "[" ^ s ^ "]") ^ 
33192  115 
(if need_parens then ")" else "") 
116 
end 

117 
in aux 0 end 

118 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

119 
(* mtyp > mtyp list *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

120 
fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2] 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

121 
 flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

122 
 flatten_mtype M = [M] 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

123 

29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

124 
(* mterm > bool *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

125 
fun precedence_of_mterm (MAtom _) = no_prec 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

126 
 precedence_of_mterm (MAbs _) = 1 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

127 
 precedence_of_mterm (MApp _) = 2 
33192  128 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

129 
(* Proof.context > mterm > string *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

130 
fun string_for_mterm ctxt = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

131 
let 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

132 
(* mtype > string *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

133 
fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>" 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

134 
(* int > mterm > string *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

135 
fun aux outer_prec m = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

136 
let 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

137 
val prec = precedence_of_mterm m 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

138 
val need_parens = (prec < outer_prec) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

139 
in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

140 
(if need_parens then "(" else "") ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

141 
(case m of 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

142 
MAtom (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

143 
 MAbs (s, _, M, a, m) => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

144 
"\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

145 
string_for_sign_atom a ^ "\<^esup> " ^ aux prec m 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

146 
 MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

147 
(if need_parens then ")" else "") 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

148 
end 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

149 
in aux 0 end 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

150 

29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

151 
(* mterm > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

152 
fun mtype_of_mterm (MAtom (_, M)) = M 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

153 
 mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

154 
 mtype_of_mterm (MApp (m1, _)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

155 
case mtype_of_mterm m1 of 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

156 
MFun (_, _, M12) => M12 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

157 
 M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1]) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

158 

29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

159 
(* hol_context > bool > typ > mdata *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

160 
fun initial_mdata hol_ctxt binarize alpha_T = 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35079
diff
changeset

161 
({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T, 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35079
diff
changeset

162 
max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [], 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

163 
constr_cache = Unsynchronized.ref []} : mdata) 
33192  164 

165 
(* typ > typ > bool *) 

166 
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) = 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34123
diff
changeset

167 
T = alpha_T orelse (not (is_fp_iterator_type T) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34123
diff
changeset

168 
exists (could_exist_alpha_subtype alpha_T) Ts) 
33192  169 
 could_exist_alpha_subtype alpha_T T = (T = alpha_T) 
170 
(* theory > typ > typ > bool *) 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

171 
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T = 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

172 
could_exist_alpha_subtype alpha_T T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

173 
 could_exist_alpha_sub_mtype thy alpha_T T = 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

174 
(T = alpha_T orelse is_datatype thy [(NONE, true)] T) 
33192  175 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

176 
(* mtyp > bool *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

177 
fun exists_alpha_sub_mtype MAlpha = true 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

178 
 exists_alpha_sub_mtype (MFun (M1, _, M2)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

179 
exists exists_alpha_sub_mtype [M1, M2] 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

180 
 exists_alpha_sub_mtype (MPair (M1, M2)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

181 
exists exists_alpha_sub_mtype [M1, M2] 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

182 
 exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

183 
 exists_alpha_sub_mtype (MRec _) = true 
33192  184 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

185 
(* mtyp > bool *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

186 
fun exists_alpha_sub_mtype_fresh MAlpha = true 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

187 
 exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

188 
 exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

189 
exists_alpha_sub_mtype_fresh M2 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

190 
 exists_alpha_sub_mtype_fresh (MPair (M1, M2)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

191 
exists exists_alpha_sub_mtype_fresh [M1, M2] 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

192 
 exists_alpha_sub_mtype_fresh (MType (_, Ms)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

193 
exists exists_alpha_sub_mtype_fresh Ms 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

194 
 exists_alpha_sub_mtype_fresh (MRec _) = true 
33192  195 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

196 
(* string * typ list > mtyp list > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

197 
fun constr_mtype_for_binders z Ms = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

198 
fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z) 
33192  199 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

200 
(* ((string * typ list) * mtyp) list > mtyp list > mtyp > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

201 
fun repair_mtype _ _ MAlpha = MAlpha 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

202 
 repair_mtype cache seen (MFun (M1, a, M2)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

203 
MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

204 
 repair_mtype cache seen (MPair Mp) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

205 
MPair (pairself (repair_mtype cache seen) Mp) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

206 
 repair_mtype cache seen (MType (s, Ms)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

207 
MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

208 
 repair_mtype cache seen (MRec (z as (s, _))) = 
33192  209 
case AList.lookup (op =) cache z > the of 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

210 
MRec _ => MType (s, []) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

211 
 M => if member (op =) seen M then MType (s, []) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

212 
else repair_mtype cache (M :: seen) M 
33192  213 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

214 
(* ((string * typ list) * mtyp) list Unsynchronized.ref > unit *) 
33192  215 
fun repair_datatype_cache cache = 
216 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

217 
(* (string * typ list) * mtyp > unit *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

218 
fun repair_one (z, M) = 
33192  219 
Unsynchronized.change cache 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

220 
(AList.update (op =) (z, repair_mtype (!cache) [] M)) 
33192  221 
in List.app repair_one (rev (!cache)) end 
222 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

223 
(* (typ * mtyp) list > (styp * mtyp) list Unsynchronized.ref > unit *) 
33192  224 
fun repair_constr_cache dtype_cache constr_cache = 
225 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

226 
(* styp * mtyp > unit *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

227 
fun repair_one (x, M) = 
33192  228 
Unsynchronized.change constr_cache 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

229 
(AList.update (op =) (x, repair_mtype dtype_cache [] M)) 
33192  230 
in List.app repair_one (!constr_cache) end 
231 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

232 
(* mdata > typ > typ > mtyp * sign_atom * mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

233 
fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 = 
33192  234 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

235 
val M1 = fresh_mtype_for_type mdata T1 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

236 
val M2 = fresh_mtype_for_type mdata T2 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

237 
val a = if is_boolean_type (body_type T2) andalso 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

238 
exists_alpha_sub_mtype_fresh M1 then 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

239 
V (Unsynchronized.inc max_fresh) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

240 
else 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

241 
S Minus 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

242 
in (M1, a, M2) end 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

243 
(* mdata > typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

244 
and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

245 
datatype_cache, constr_cache, ...}) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

246 
let 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

247 
(* typ > typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

248 
val do_fun = MFun oo fresh_mfun_for_fun_type mdata 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

249 
(* typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

250 
fun do_type T = 
33192  251 
if T = alpha_T then 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

252 
MAlpha 
33192  253 
else case T of 
254 
Type ("fun", [T1, T2]) => do_fun T1 T2 

255 
 Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

256 
 Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2)) 
33192  257 
 Type (z as (s, _)) => 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

258 
if could_exist_alpha_sub_mtype thy alpha_T T then 
33192  259 
case AList.lookup (op =) (!datatype_cache) z of 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

260 
SOME M => M 
33192  261 
 NONE => 
262 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

263 
val _ = Unsynchronized.change datatype_cache (cons (z, MRec z)) 
35219
15a5f213ef5b
fix bug in Nitpick's monotonicity code w.r.t. binary integers
blanchet
parents:
35190
diff
changeset

264 
val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

265 
val (all_Ms, constr_Ms) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

266 
fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) => 
33192  267 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

268 
val binder_Ms = map do_type (binder_types T') 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

269 
val new_Ms = filter exists_alpha_sub_mtype_fresh 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

270 
binder_Ms 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

271 
val constr_M = constr_mtype_for_binders z 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

272 
binder_Ms 
33192  273 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

274 
(union (op =) new_Ms all_Ms, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

275 
constr_M :: constr_Ms) 
33192  276 
end) 
277 
xs ([], []) 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

278 
val M = MType (s, all_Ms) 
33192  279 
val _ = Unsynchronized.change datatype_cache 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

280 
(AList.update (op =) (z, M)) 
33192  281 
val _ = Unsynchronized.change constr_cache 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

282 
(append (xs ~~ constr_Ms)) 
33192  283 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

284 
if forall (not o is_MRec o snd) (!datatype_cache) then 
33192  285 
(repair_datatype_cache datatype_cache; 
286 
repair_constr_cache (!datatype_cache) constr_cache; 

287 
AList.lookup (op =) (!datatype_cache) z > the) 

288 
else 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

289 
M 
33192  290 
end 
291 
else 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

292 
MType (s, []) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

293 
 _ => MType (Refute.string_of_typ T, []) 
33192  294 
in do_type end 
295 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

296 
(* mtyp > mtyp list *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

297 
fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2] 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

298 
 prodM_factors M = [M] 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

299 
(* mtyp > mtyp list * mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

300 
fun curried_strip_mtype (MFun (M1, S Minus, M2)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

301 
curried_strip_mtype M2 >> append (prodM_factors M1) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

302 
 curried_strip_mtype M = ([], M) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

303 
(* string > mtyp > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

304 
fun sel_mtype_from_constr_mtype s M = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

305 
let val (arg_Ms, dataM) = curried_strip_mtype M in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

306 
MFun (dataM, S Minus, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

307 
case sel_no_from_name s of ~1 => bool_M  n => nth arg_Ms n) 
33192  308 
end 
309 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

310 
(* mdata > styp > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

311 
fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache, 
33192  312 
...}) (x as (_, T)) = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

313 
if could_exist_alpha_sub_mtype thy alpha_T T then 
33192  314 
case AList.lookup (op =) (!constr_cache) x of 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

315 
SOME M => M 
35384  316 
 NONE => if T = alpha_T then 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

317 
let val M = fresh_mtype_for_type mdata T in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

318 
(Unsynchronized.change constr_cache (cons (x, M)); M) 
35384  319 
end 
320 
else 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

321 
(fresh_mtype_for_type mdata (body_type T); 
35384  322 
AList.lookup (op =) (!constr_cache) x > the) 
33192  323 
else 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

324 
fresh_mtype_for_type mdata T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

325 
fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) = 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35079
diff
changeset

326 
x > binarized_and_boxed_constr_for_sel hol_ctxt binarize 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

327 
> mtype_for_constr mdata > sel_mtype_from_constr_mtype s 
33192  328 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

329 
(* literal list > mtyp > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

330 
fun instantiate_mtype lits = 
33192  331 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

332 
(* mtyp > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

333 
fun aux MAlpha = MAlpha 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

334 
 aux (MFun (M1, V x, M2)) = 
33192  335 
let 
336 
val a = case AList.lookup (op =) lits x of 

337 
SOME sn => S sn 

338 
 NONE => V x 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

339 
in MFun (aux M1, a, aux M2) end 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

340 
 aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

341 
 aux (MPair Mp) = MPair (pairself aux Mp) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

342 
 aux (MType (s, Ms)) = MType (s, map aux Ms) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

343 
 aux (MRec z) = MRec z 
33192  344 
in aux end 
345 

346 
datatype comp_op = Eq  Leq 

347 

348 
type comp = sign_atom * sign_atom * comp_op * var list 

349 
type sign_expr = literal list 

350 

351 
datatype constraint_set = 

352 
UnsolvableCSet  

353 
CSet of literal list * comp list * sign_expr list 

354 

355 
(* comp_op > string *) 

356 
fun string_for_comp_op Eq = "=" 

357 
 string_for_comp_op Leq = "\<le>" 

358 

359 
(* sign_expr > string *) 

360 
fun string_for_sign_expr [] = "\<bot>" 

361 
 string_for_sign_expr lits = 

362 
space_implode " \<or> " (map string_for_literal lits) 

363 

364 
(* constraint_set *) 

365 
val slack = CSet ([], [], []) 

366 

367 
(* literal > literal list option > literal list option *) 

368 
fun do_literal _ NONE = NONE 

369 
 do_literal (x, sn) (SOME lits) = 

370 
case AList.lookup (op =) lits x of 

371 
SOME sn' => if sn = sn' then SOME lits else NONE 

372 
 NONE => SOME ((x, sn) :: lits) 

373 

374 
(* comp_op > var list > sign_atom > sign_atom > literal list * comp list 

375 
> (literal list * comp list) option *) 

376 
fun do_sign_atom_comp Eq [] a1 a2 (accum as (lits, comps)) = 

377 
(case (a1, a2) of 

378 
(S sn1, S sn2) => if sn1 = sn2 then SOME accum else NONE 

379 
 (V x1, S sn2) => 

380 
Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits)) 

381 
 (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps) 

382 
 _ => do_sign_atom_comp Eq [] a2 a1 accum) 

383 
 do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) = 

384 
(case (a1, a2) of 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

385 
(_, S Minus) => SOME accum 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

386 
 (S Plus, _) => SOME accum 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

387 
 (S Minus, S Plus) => NONE 
33192  388 
 (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps) 
389 
 _ => do_sign_atom_comp Eq [] a1 a2 accum) 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

390 
 do_sign_atom_comp cmp xs a1 a2 (lits, comps) = 
33192  391 
SOME (lits, insert (op =) (a1, a2, cmp, xs) comps) 
392 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

393 
(* comp > var list > mtyp > mtyp > (literal list * comp list) option 
33192  394 
> (literal list * comp list) option *) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

395 
fun do_mtype_comp _ _ _ _ NONE = NONE 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

396 
 do_mtype_comp _ _ MAlpha MAlpha accum = accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

397 
 do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22)) 
33192  398 
(SOME accum) = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

399 
accum > do_sign_atom_comp Eq xs a1 a2 > do_mtype_comp Eq xs M11 M21 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

400 
> do_mtype_comp Eq xs M12 M22 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

401 
 do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22)) 
33192  402 
(SOME accum) = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

403 
(if exists_alpha_sub_mtype M11 then 
33192  404 
accum > do_sign_atom_comp Leq xs a1 a2 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

405 
> do_mtype_comp Leq xs M21 M11 
33192  406 
> (case a2 of 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

407 
S Minus => I 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

408 
 S Plus => do_mtype_comp Leq xs M11 M21 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

409 
 V x => do_mtype_comp Leq (x :: xs) M11 M21) 
33192  410 
else 
411 
SOME accum) 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

412 
> do_mtype_comp Leq xs M12 M22 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

413 
 do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22)) 
33192  414 
accum = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

415 
(accum > fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)] 
33192  416 
handle Library.UnequalLengths => 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

417 
raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

418 
 do_mtype_comp _ _ (MType _) (MType _) accum = 
33192  419 
accum (* no need to compare them thanks to the cache *) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

420 
 do_mtype_comp _ _ M1 M2 _ = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

421 
raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]) 
33192  422 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

423 
(* comp_op > mtyp > mtyp > constraint_set > constraint_set *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

424 
fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

425 
 add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

426 
(print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

427 
" " ^ string_for_mtype M2); 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

428 
case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of 
33192  429 
NONE => (print_g "**** Unsolvable"; UnsolvableCSet) 
430 
 SOME (lits, comps) => CSet (lits, comps, sexps)) 

431 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

432 
(* mtyp > mtyp > constraint_set > constraint_set *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

433 
val add_mtypes_equal = add_mtype_comp Eq 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

434 
val add_is_sub_mtype = add_mtype_comp Leq 
33192  435 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

436 
(* sign > sign_expr > mtyp > (literal list * sign_expr list) option 
33192  437 
> (literal list * sign_expr list) option *) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

438 
fun do_notin_mtype_fv _ _ _ NONE = NONE 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

439 
 do_notin_mtype_fv Minus _ MAlpha accum = accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

440 
 do_notin_mtype_fv Plus [] MAlpha _ = NONE 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

441 
 do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) = 
33192  442 
SOME lits > do_literal (x, sn) > Option.map (rpair sexps) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

443 
 do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) = 
33192  444 
SOME (lits, insert (op =) sexp sexps) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

445 
 do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum = 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

446 
accum > (if sn' = Plus andalso sn = Plus then 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

447 
do_notin_mtype_fv Plus sexp M1 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

448 
else 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

449 
I) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

450 
> (if sn' = Minus orelse sn = Plus then 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

451 
do_notin_mtype_fv Minus sexp M1 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

452 
else 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

453 
I) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

454 
> do_notin_mtype_fv sn sexp M2 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

455 
 do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum = 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

456 
accum > (case do_literal (x, Minus) (SOME sexp) of 
33192  457 
NONE => I 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

458 
 SOME sexp' => do_notin_mtype_fv Plus sexp' M1) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

459 
> do_notin_mtype_fv Minus sexp M1 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

460 
> do_notin_mtype_fv Plus sexp M2 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

461 
 do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum = 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

462 
accum > (case do_literal (x, Plus) (SOME sexp) of 
33192  463 
NONE => I 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

464 
 SOME sexp' => do_notin_mtype_fv Plus sexp' M1) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

465 
> do_notin_mtype_fv Minus sexp M2 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

466 
 do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

467 
accum > fold (do_notin_mtype_fv sn sexp) [M1, M2] 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

468 
 do_notin_mtype_fv sn sexp (MType (_, Ms)) accum = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

469 
accum > fold (do_notin_mtype_fv sn sexp) Ms 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

470 
 do_notin_mtype_fv _ _ M _ = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

471 
raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M]) 
33192  472 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

473 
(* sign > mtyp > constraint_set > constraint_set *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

474 
fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

475 
 add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

476 
(print_g ("*** Add " ^ string_for_mtype M ^ " is right" ^ 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

477 
(case sn of Minus => "unique"  Plus => "total") ^ "."); 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

478 
case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of 
33192  479 
NONE => (print_g "**** Unsolvable"; UnsolvableCSet) 
480 
 SOME (lits, sexps) => CSet (lits, comps, sexps)) 

481 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

482 
(* mtyp > constraint_set > constraint_set *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

483 
val add_mtype_is_right_unique = add_notin_mtype_fv Minus 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

484 
val add_mtype_is_right_total = add_notin_mtype_fv Plus 
33192  485 

35384  486 
val bool_from_minus = true 
487 

33192  488 
(* sign > bool *) 
35384  489 
fun bool_from_sign Plus = not bool_from_minus 
490 
 bool_from_sign Minus = bool_from_minus 

33192  491 
(* bool > sign *) 
35384  492 
fun sign_from_bool b = if b = bool_from_minus then Minus else Plus 
33192  493 

494 
(* literal > PropLogic.prop_formula *) 

495 
fun prop_for_literal (x, sn) = 

496 
(not (bool_from_sign sn) ? PropLogic.Not) (PropLogic.BoolVar x) 

497 
(* sign_atom > PropLogic.prop_formula *) 

498 
fun prop_for_sign_atom_eq (S sn', sn) = 

499 
if sn = sn' then PropLogic.True else PropLogic.False 

500 
 prop_for_sign_atom_eq (V x, sn) = prop_for_literal (x, sn) 

501 
(* sign_expr > PropLogic.prop_formula *) 

502 
fun prop_for_sign_expr xs = PropLogic.exists (map prop_for_literal xs) 

503 
(* var list > sign > PropLogic.prop_formula *) 

504 
fun prop_for_exists_eq xs sn = 

505 
PropLogic.exists (map (fn x => prop_for_literal (x, sn)) xs) 

506 
(* comp > PropLogic.prop_formula *) 

507 
fun prop_for_comp (a1, a2, Eq, []) = 

508 
PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []), 

509 
prop_for_comp (a2, a1, Leq, [])) 

510 
 prop_for_comp (a1, a2, Leq, []) = 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

511 
PropLogic.SOr (prop_for_sign_atom_eq (a1, Plus), 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

512 
prop_for_sign_atom_eq (a2, Minus)) 
33192  513 
 prop_for_comp (a1, a2, cmp, xs) = 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

514 
PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, [])) 
33192  515 

516 
(* var > (int > bool option) > literal list > literal list *) 

34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

517 
fun literals_from_assignments max_var assigns lits = 
33192  518 
fold (fn x => fn accum => 
519 
if AList.defined (op =) lits x then 

520 
accum 

34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

521 
else case assigns x of 
33192  522 
SOME b => (x, sign_from_bool b) :: accum 
523 
 NONE => accum) (max_var downto 1) lits 

524 

525 
(* comp > string *) 

526 
fun string_for_comp (a1, a2, cmp, xs) = 

527 
string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^ 

528 
subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2 

529 

530 
(* literal list > comp list > sign_expr list > unit *) 

531 
fun print_problem lits comps sexps = 

532 
print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @ 

533 
map string_for_comp comps @ 

534 
map string_for_sign_expr sexps)) 

535 

536 
(* literal list > unit *) 

537 
fun print_solution lits = 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

538 
let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in 
33192  539 
print_g ("*** Solution:\n" ^ 
540 
"+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^ 

541 
": " ^ commas (map (string_for_var o fst) neg)) 

542 
end 

543 

35384  544 
(* var > constraint_set > literal list option *) 
33192  545 
fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE) 
546 
 solve max_var (CSet (lits, comps, sexps)) = 

547 
let 

548 
val _ = print_problem lits comps sexps 

549 
val prop = PropLogic.all (map prop_for_literal lits @ 

550 
map prop_for_comp comps @ 

551 
map prop_for_sign_expr sexps) 

34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

552 
(* use the first ML solver (to avoid startup overhead) *) 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

553 
val solvers = !SatSolver.solvers 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

554 
> filter (member (op =) ["dptsat", "dpll"] o fst) 
33192  555 
in 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

556 
case snd (hd solvers) prop of 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

557 
SatSolver.SATISFIABLE assigns => 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

558 
SOME (literals_from_assignments max_var assigns lits 
33192  559 
> tap print_solution) 
560 
 _ => NONE 

561 
end 

562 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

563 
type mtype_schema = mtyp * constraint_set 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

564 
type mtype_context = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

565 
{bounds: mtyp list, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

566 
frees: (styp * mtyp) list, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

567 
consts: (styp * mtyp) list} 
33192  568 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

569 
type accumulator = mtype_context * constraint_set 
33192  570 

571 
val initial_gamma = {bounds = [], frees = [], consts = []} 

572 
val unsolvable_accum = (initial_gamma, UnsolvableCSet) 

573 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

574 
(* mtyp > mtype_context > mtype_context *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

575 
fun push_bound M {bounds, frees, consts} = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

576 
{bounds = M :: bounds, frees = frees, consts = consts} 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

577 
(* mtype_context > mtype_context *) 
33192  578 
fun pop_bound {bounds, frees, consts} = 
579 
{bounds = tl bounds, frees = frees, consts = consts} 

580 
handle List.Empty => initial_gamma 

581 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

582 
(* mdata > term > accumulator > mterm * accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

583 
fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

584 
def_table, ...}, 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

585 
alpha_T, max_fresh, ...}) = 
33192  586 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

587 
(* typ > typ > mtyp * sign_atom * mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

588 
val mfun_for = fresh_mfun_for_fun_type mdata 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

589 
(* typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

590 
val mtype_for = fresh_mtype_for_type mdata 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

591 
(* mtyp > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

592 
fun pos_set_mtype_for_dom M = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

593 
MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

594 
(* typ > accumulator > mterm * accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

595 
fun do_all T (gamma, cset) = 
33192  596 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

597 
val abs_M = mtype_for (domain_type (domain_type T)) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

598 
val body_M = mtype_for (range_type T) 
33192  599 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

600 
(MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

601 
(gamma, cset > add_mtype_is_right_total abs_M)) 
33192  602 
end 
603 
fun do_equals T (gamma, cset) = 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

604 
let val M = mtype_for (domain_type T) in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

605 
(MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

606 
mtype_for (nth_range_type 2 T))), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

607 
(gamma, cset > add_mtype_is_right_unique M)) 
33192  608 
end 
609 
fun do_robust_set_operation T (gamma, cset) = 

610 
let 

611 
val set_T = domain_type T 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

612 
val M1 = mtype_for set_T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

613 
val M2 = mtype_for set_T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

614 
val M3 = mtype_for set_T 
33192  615 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

616 
(MFun (M1, S Minus, MFun (M2, S Minus, M3)), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

617 
(gamma, cset > add_is_sub_mtype M1 M3 > add_is_sub_mtype M2 M3)) 
33192  618 
end 
619 
fun do_fragile_set_operation T (gamma, cset) = 

620 
let 

621 
val set_T = domain_type T 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

622 
val set_M = mtype_for set_T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

623 
(* typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

624 
fun custom_mtype_for (T as Type ("fun", [T1, T2])) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

625 
if T = set_T then set_M 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

626 
else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

627 
 custom_mtype_for T = mtype_for T 
33192  628 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

629 
(custom_mtype_for T, (gamma, cset > add_mtype_is_right_unique set_M)) 
33192  630 
end 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

631 
(* typ > accumulator > mtyp * accumulator *) 
33192  632 
fun do_pair_constr T accum = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

633 
case mtype_for (nth_range_type 2 T) of 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

634 
M as MPair (a_M, b_M) => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

635 
(MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

636 
 M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M]) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

637 
(* int > typ > accumulator > mtyp * accumulator *) 
33192  638 
fun do_nth_pair_sel n T = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

639 
case mtype_for (domain_type T) of 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

640 
M as MPair (a_M, b_M) => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

641 
pair (MFun (M, S Minus, if n = 0 then a_M else b_M)) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

642 
 M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M]) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

643 
(* mtyp * accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

644 
val mtype_unsolvable = (irrelevant_M, unsolvable_accum) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

645 
(* term > mterm * accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

646 
fun mterm_unsolvable t = (MAtom (t, irrelevant_M), unsolvable_accum) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

647 
(* term > string > typ > term > term > term > accumulator 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

648 
> mterm * accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

649 
fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum = 
33192  650 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

651 
val abs_M = mtype_for abs_T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

652 
val (bound_m, accum) = accum >> push_bound abs_M > do_term bound_t 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

653 
val expected_bound_M = pos_set_mtype_for_dom abs_M 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

654 
val (body_m, accum) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

655 
accum > add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

656 
> do_term body_t > apfst pop_bound 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

657 
val bound_M = mtype_of_mterm bound_m 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

658 
val (M1, a, M2) = dest_MFun bound_M 
33192  659 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

660 
(MApp (MAtom (t0, MFun (bound_M, S Minus, bool_M)), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

661 
MAbs (abs_s, abs_T, M1, a, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

662 
MApp (MApp (MAtom (connective_t, irrelevant_M), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

663 
MApp (bound_m, MAtom (Bound 0, M1))), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

664 
body_m))), accum) 
33192  665 
end 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

666 
(* term > accumulator > mterm * accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

667 
and do_term t (_, UnsolvableCSet) = mterm_unsolvable t 
33192  668 
 do_term t (accum as (gamma as {bounds, frees, consts}, cset)) = 
669 
(case t of 

670 
Const (x as (s, T)) => 

671 
(case AList.lookup (op =) consts x of 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

672 
SOME M => (M, accum) 
33192  673 
 NONE => 
674 
if not (could_exist_alpha_subtype alpha_T T) then 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

675 
(mtype_for T, accum) 
33192  676 
else case s of 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

677 
@{const_name all} => do_all T accum 
33192  678 
 @{const_name "=="} => do_equals T accum 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

679 
 @{const_name All} => do_all T accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

680 
 @{const_name Ex} => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

681 
do_term (@{const Not} 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

682 
$ (HOLogic.eq_const (domain_type T) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

683 
$ Abs (Name.uu, T, @{const False}))) accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

684 
>> mtype_of_mterm 
33192  685 
 @{const_name "op ="} => do_equals T accum 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

686 
 @{const_name The} => (print_g "*** The"; mtype_unsolvable) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

687 
 @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable) 
33192  688 
 @{const_name If} => 
689 
do_robust_set_operation (range_type T) accum 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

690 
>> curry3 MFun bool_M (S Minus) 
33192  691 
 @{const_name Pair} => do_pair_constr T accum 
692 
 @{const_name fst} => do_nth_pair_sel 0 T accum 

693 
 @{const_name snd} => do_nth_pair_sel 1 T accum 

694 
 @{const_name Id} => 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

695 
(MFun (mtype_for (domain_type T), S Minus, bool_M), accum) 
33192  696 
 @{const_name insert} => 
697 
let 

698 
val set_T = domain_type (range_type T) 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

699 
val M1 = mtype_for (domain_type set_T) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

700 
val M1' = pos_set_mtype_for_dom M1 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

701 
val M2 = mtype_for set_T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

702 
val M3 = mtype_for set_T 
33192  703 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

704 
(MFun (M1, S Minus, MFun (M2, S Minus, M3)), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

705 
(gamma, cset > add_mtype_is_right_unique M1 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

706 
> add_is_sub_mtype M1' M3 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

707 
> add_is_sub_mtype M2 M3)) 
33192  708 
end 
709 
 @{const_name converse} => 

710 
let 

711 
val x = Unsynchronized.inc max_fresh 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

712 
(* typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

713 
fun mtype_for_set T = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

714 
MFun (mtype_for (domain_type T), V x, bool_M) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

715 
val ab_set_M = domain_type T > mtype_for_set 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

716 
val ba_set_M = range_type T > mtype_for_set 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

717 
in (MFun (ab_set_M, S Minus, ba_set_M), accum) end 
33192  718 
 @{const_name trancl} => do_fragile_set_operation T accum 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

719 
 @{const_name rtrancl} => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

720 
(print_g "*** rtrancl"; mtype_unsolvable) 
33192  721 
 @{const_name finite} => 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

722 
let val M1 = mtype_for (domain_type (domain_type T)) in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

723 
(MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum) 
33192  724 
end 
725 
 @{const_name rel_comp} => 

726 
let 

727 
val x = Unsynchronized.inc max_fresh 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

728 
(* typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

729 
fun mtype_for_set T = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

730 
MFun (mtype_for (domain_type T), V x, bool_M) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

731 
val bc_set_M = domain_type T > mtype_for_set 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

732 
val ab_set_M = domain_type (range_type T) > mtype_for_set 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

733 
val ac_set_M = nth_range_type 2 T > mtype_for_set 
33192  734 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

735 
(MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)), 
33192  736 
accum) 
737 
end 

738 
 @{const_name image} => 

739 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

740 
val a_M = mtype_for (domain_type (domain_type T)) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

741 
val b_M = mtype_for (range_type (domain_type T)) 
33192  742 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

743 
(MFun (MFun (a_M, S Minus, b_M), S Minus, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

744 
MFun (pos_set_mtype_for_dom a_M, S Minus, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

745 
pos_set_mtype_for_dom b_M)), accum) 
33192  746 
end 
747 
 @{const_name Sigma} => 

748 
let 

749 
val x = Unsynchronized.inc max_fresh 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

750 
(* typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

751 
fun mtype_for_set T = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

752 
MFun (mtype_for (domain_type T), V x, bool_M) 
33192  753 
val a_set_T = domain_type T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

754 
val a_M = mtype_for (domain_type a_set_T) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

755 
val b_set_M = mtype_for_set (range_type (domain_type 
33192  756 
(range_type T))) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

757 
val a_set_M = mtype_for_set a_set_T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

758 
val a_to_b_set_M = MFun (a_M, S Minus, b_set_M) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

759 
val ab_set_M = mtype_for_set (nth_range_type 2 T) 
33192  760 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

761 
(MFun (a_set_M, S Minus, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

762 
MFun (a_to_b_set_M, S Minus, ab_set_M)), accum) 
33192  763 
end 
764 
 @{const_name Tha} => 

765 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

766 
val a_M = mtype_for (domain_type (domain_type T)) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

767 
val a_set_M = pos_set_mtype_for_dom a_M 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

768 
in (MFun (a_set_M, S Minus, a_M), accum) end 
33192  769 
 @{const_name FunBox} => 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

770 
let val dom_M = mtype_for (domain_type T) in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

771 
(MFun (dom_M, S Minus, dom_M), accum) 
33192  772 
end 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

773 
 _ => 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

774 
if s = @{const_name minus_class.minus} andalso 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

775 
is_set_type (domain_type T) then 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

776 
let 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

777 
val set_T = domain_type T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

778 
val left_set_M = mtype_for set_T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

779 
val right_set_M = mtype_for set_T 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

780 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

781 
(MFun (left_set_M, S Minus, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

782 
MFun (right_set_M, S Minus, left_set_M)), 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

783 
(gamma, cset > add_mtype_is_right_unique right_set_M 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

784 
> add_is_sub_mtype right_set_M left_set_M)) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

785 
end 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

786 
else if s = @{const_name ord_class.less_eq} andalso 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

787 
is_set_type (domain_type T) then 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

788 
do_fragile_set_operation T accum 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

789 
else if (s = @{const_name semilattice_inf_class.inf} orelse 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

790 
s = @{const_name semilattice_sup_class.sup}) andalso 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

791 
is_set_type (domain_type T) then 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

792 
do_robust_set_operation T accum 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

793 
else if is_sel s then 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

794 
if constr_name_for_sel_like s = @{const_name FunBox} then 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

795 
let val dom_M = mtype_for (domain_type T) in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

796 
(MFun (dom_M, S Minus, dom_M), accum) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

797 
end 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

798 
else 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

799 
(mtype_for_sel mdata x, accum) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

800 
else if is_constr thy stds x then 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

801 
(mtype_for_constr mdata x, accum) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

802 
else if is_built_in_const thy stds fast_descrs x then 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

803 
case def_of_const thy def_table x of 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

804 
SOME t' => do_term t' accum >> mtype_of_mterm 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

805 
 NONE => (print_g ("*** builtin " ^ s); mtype_unsolvable) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

806 
else 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

807 
let val M = mtype_for T in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

808 
(M, ({bounds = bounds, frees = frees, 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

809 
consts = (x, M) :: consts}, cset)) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

810 
end) >> curry MAtom t 
33192  811 
 Free (x as (_, T)) => 
812 
(case AList.lookup (op =) frees x of 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

813 
SOME M => (M, accum) 
33192  814 
 NONE => 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

815 
let val M = mtype_for T in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

816 
(M, ({bounds = bounds, frees = (x, M) :: frees, 
33192  817 
consts = consts}, cset)) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

818 
end) >> curry MAtom t 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

819 
 Var _ => (print_g "*** Var"; mterm_unsolvable t) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

820 
 Bound j => (MAtom (t, nth bounds j), accum) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

821 
 Abs (s, T, t' as @{const False}) => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

822 
let val (M1, a, M2) = mfun_for T bool_T in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

823 
(MAbs (s, T, M1, a, MAtom (t', M2)), accum) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

824 
end 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

825 
 Abs (s, T, t') => 
34998  826 
((case t' of 
827 
t1' $ Bound 0 => 

828 
if not (loose_bvar1 (t1', 0)) then 

829 
do_term (incr_boundvars ~1 t1') accum 

830 
else 

831 
raise SAME () 

832 
 _ => raise SAME ()) 

833 
handle SAME () => 

834 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

835 
val M = mtype_for T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

836 
val (m', accum) = do_term t' (accum >> push_bound M) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

837 
in (MAbs (s, T, M, S Minus, m'), accum >> pop_bound) end) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

838 
 (t0 as Const (@{const_name All}, _)) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

839 
$ Abs (s', T', (t10 as @{const "op >"}) $ (t11 $ Bound 0) $ t12) => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

840 
do_bounded_quantifier t0 s' T' t10 t11 t12 accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

841 
 (t0 as Const (@{const_name Ex}, _)) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

842 
$ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

843 
do_bounded_quantifier t0 s' T' t10 t11 t12 accum 
33192  844 
 Const (@{const_name Let}, _) $ t1 $ t2 => 
845 
do_term (betapply (t2, t1)) accum 

846 
 t1 $ t2 => 

847 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

848 
val (m1, accum) = do_term t1 accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

849 
val (m2, accum) = do_term t2 accum 
33192  850 
in 
851 
case accum of 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

852 
(_, UnsolvableCSet) => mterm_unsolvable t 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

853 
 _ => (MApp (m1, m2), accum) 
33192  854 
end) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

855 
> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

856 
string_for_mterm ctxt m)) 
33192  857 
in do_term end 
858 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

859 
(* mdata > sign > term > accumulator > accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

860 
fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) = 
33192  861 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

862 
(* typ > mtyp *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

863 
val mtype_for = fresh_mtype_for_type mdata 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

864 
(* term > accumulator > mtyp * accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

865 
val do_term = apfst mtype_of_mterm oo consider_term mdata 
33192  866 
(* sign > term > accumulator > accumulator *) 
867 
fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

868 
 do_formula sn t (accum as (gamma, cset)) = 
33192  869 
let 
870 
(* term > accumulator > accumulator *) 

871 
val do_co_formula = do_formula sn 

872 
val do_contra_formula = do_formula (negate sn) 

873 
(* string > typ > term > accumulator *) 

874 
fun do_quantifier quant_s abs_T body_t = 

875 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

876 
val abs_M = mtype_for abs_T 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

877 
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex})) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

878 
val cset = cset > side_cond ? add_mtype_is_right_total abs_M 
33192  879 
in 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

880 
(gamma > push_bound abs_M, cset) 
35384  881 
> do_co_formula body_t >> pop_bound 
33192  882 
end 
883 
(* typ > term > accumulator *) 

884 
fun do_bounded_quantifier abs_T body_t = 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

885 
accum >> push_bound (mtype_for abs_T) > do_co_formula body_t 
33192  886 
>> pop_bound 
887 
(* term > term > accumulator *) 

888 
fun do_equals t1 t2 = 

889 
case sn of 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

890 
Plus => do_term t accum > snd 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

891 
 Minus => let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

892 
val (M1, accum) = do_term t1 accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

893 
val (M2, accum) = do_term t2 accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

894 
in accum > add_mtypes_equal M1 M2 end 
33192  895 
in 
896 
case t of 

897 
Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) => 

898 
do_quantifier s0 T1 t1 

899 
 Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 

900 
 @{const "==>"} $ t1 $ t2 => 

901 
accum > do_contra_formula t1 > do_co_formula t2 

902 
 @{const Trueprop} $ t1 => do_co_formula t1 accum 

903 
 @{const Not} $ t1 => do_contra_formula t1 accum 

904 
 Const (@{const_name All}, _) 

905 
$ Abs (_, T1, t1 as @{const "op >"} $ (_ $ Bound 0) $ _) => 

906 
do_bounded_quantifier T1 t1 

907 
 Const (s0 as @{const_name All}, _) $ Abs (_, T1, t1) => 

908 
do_quantifier s0 T1 t1 

909 
 Const (@{const_name Ex}, _) 

910 
$ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) => 

911 
do_bounded_quantifier T1 t1 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

912 
 Const (s0 as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

913 
(case sn of 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

914 
Plus => do_quantifier s0 T1 t1' 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

915 
 Minus => 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

916 
do_term (@{const Not} 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

917 
$ (HOLogic.eq_const (domain_type T0) $ t1 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

918 
$ Abs (Name.uu, T1, @{const False}))) accum > snd) 
33192  919 
 Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 
920 
 @{const "op &"} $ t1 $ t2 => 

921 
accum > do_co_formula t1 > do_co_formula t2 

922 
 @{const "op "} $ t1 $ t2 => 

923 
accum > do_co_formula t1 > do_co_formula t2 

924 
 @{const "op >"} $ t1 $ t2 => 

925 
accum > do_contra_formula t1 > do_co_formula t2 

926 
 Const (@{const_name If}, _) $ t1 $ t2 $ t3 => 

33732
385381514eed
added constraint for Eq^ in Nitpick's implementation of the monotonicity calculus
blanchet
parents:
33580
diff
changeset

927 
accum > do_term t1 > snd > fold do_co_formula [t2, t3] 
33192  928 
 Const (@{const_name Let}, _) $ t1 $ t2 => 
929 
do_co_formula (betapply (t2, t1)) accum 

33732
385381514eed
added constraint for Eq^ in Nitpick's implementation of the monotonicity calculus
blanchet
parents:
33580
diff
changeset

930 
 _ => do_term t accum > snd 
33192  931 
end 
932 
> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^ 

933 
Syntax.string_of_term ctxt t ^ 

934 
" : o\<^sup>" ^ string_for_sign sn)) 

935 
in do_formula end 

936 

937 
(* The harmless axiom optimization below is somewhat too aggressive in the face 

938 
of (rather peculiar) userdefined axioms. *) 

939 
val harmless_consts = 

940 
[@{const_name ord_class.less}, @{const_name ord_class.less_eq}] 

941 
val bounteous_consts = [@{const_name bisim}] 

942 

943 
(* term > bool *) 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

944 
fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

945 
Term.add_consts t [] 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

946 
> filter_out (is_built_in_const thy stds fast_descrs) 
33192  947 
> (forall (member (op =) harmless_consts o original_name o fst) 
948 
orf exists (member (op =) bounteous_consts o fst)) 

949 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

950 
(* mdata > sign > term > accumulator > accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

951 
fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) sn t = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

952 
not (is_harmless_axiom hol_ctxt t) ? consider_general_formula mdata sn t 
33192  953 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

954 
(* mdata > term > accumulator > accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

955 
fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t = 
33192  956 
if not (is_constr_pattern_formula thy t) then 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

957 
consider_nondefinitional_axiom mdata Plus t 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset

958 
else if is_harmless_axiom hol_ctxt t then 
33192  959 
I 
960 
else 

961 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

962 
(* term > accumulator > mtyp * accumulator *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

963 
val do_term = apfst mtype_of_mterm oo consider_term mdata 
33192  964 
(* typ > term > accumulator > accumulator *) 
965 
fun do_all abs_T body_t accum = 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

966 
let val abs_M = fresh_mtype_for_type mdata abs_T in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

967 
accum >> push_bound abs_M > do_formula body_t >> pop_bound 
33192  968 
end 
969 
(* term > term > accumulator > accumulator *) 

970 
and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2 

971 
and do_equals t1 t2 accum = 

972 
let 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

973 
val (M1, accum) = do_term t1 accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

974 
val (M2, accum) = do_term t2 accum 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

975 
in accum > add_mtypes_equal M1 M2 end 
33192  976 
(* term > accumulator > accumulator *) 
977 
and do_formula _ (_, UnsolvableCSet) = unsolvable_accum 

978 
 do_formula t accum = 

979 
case t of 

980 
Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum 

981 
 @{const Trueprop} $ t1 => do_formula t1 accum 

982 
 Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 accum 

983 
 @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum 

984 
 @{const Pure.conjunction} $ t1 $ t2 => 

985 
accum > do_formula t1 > do_formula t2 

986 
 Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum 

987 
 Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum 

988 
 @{const "op &"} $ t1 $ t2 => accum > do_formula t1 > do_formula t2 

989 
 @{const "op >"} $ t1 $ t2 => do_implies t1 t2 accum 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

990 
 _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\ 
33192  991 
\do_formula", [t]) 
992 
in do_formula t end 

993 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

994 
(* Proof.context > literal list > term > mtyp > string *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

995 
fun string_for_mtype_of_term ctxt lits t M = 
33192  996 
Syntax.string_of_term ctxt t ^ " : " ^ 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

997 
string_for_mtype (instantiate_mtype lits M) 
33192  998 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

999 
(* theory > literal list > mtype_context > unit *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1000 
fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1001 
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1002 
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts 
33192  1003 
> cat_lines > print_g 
1004 

35384  1005 
(* hol_context > bool > typ > term list * term list * term > bool *) 
1006 
fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T 

1007 
(def_ts, nondef_ts, core_t) = 

33192  1008 
let 
35384  1009 
val _ = print_g ("****** Monotonicity analysis: " ^ 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1010 
string_for_mtype MAlpha ^ " is " ^ 
33192  1011 
Syntax.string_of_typ ctxt alpha_T) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1012 
val mdata as {max_fresh, constr_cache, ...} = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1013 
initial_mdata hol_ctxt binarize alpha_T 
35384  1014 
val (gamma as {frees, consts, ...}, cset) = 
33192  1015 
(initial_gamma, slack) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1016 
> fold (consider_definitional_axiom mdata) def_ts 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1017 
> fold (consider_nondefinitional_axiom mdata Plus) nondef_ts 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1018 
> consider_general_formula mdata Plus core_t 
33192  1019 
in 
1020 
case solve (!max_fresh) cset of 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1021 
SOME lits => (print_mtype_context ctxt lits gamma; true) 
33192  1022 
 _ => false 
1023 
end 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1024 
handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms)) 
33192  1025 

1026 
end; 