author  blanchet 
Sat, 24 Apr 2010 16:33:01 +0200  
changeset 36385  ff5f88702590 
parent 35832  1dac16f00cd2 
child 37256  0dca1ec52999 
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 : 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

13 
hol_context > bool > typ > term list * term list > bool 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

14 
val finitize_funs : 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

15 
hol_context > bool > (typ option * bool option) list > typ 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

16 
> term list * term list > term list * term list 
33192  17 
end; 
18 

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

19 
structure Nitpick_Mono : NITPICK_MONO = 
33192  20 
struct 
21 

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

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

23 
open Nitpick_HOL 
33192  24 

25 
type var = int 

26 

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

27 
datatype sign = Plus  Minus 
33192  28 
datatype sign_atom = S of sign  V of var 
29 

30 
type literal = var * sign 

31 

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

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

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

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

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

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

37 
MRec of string * typ list 
33192  38 

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

39 
datatype mterm = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

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

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

43 

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

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

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

46 
binarize: bool, 
33192  47 
alpha_T: typ, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

48 
no_harmless: bool, 
33192  49 
max_fresh: int Unsynchronized.ref, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

50 
datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

51 
constr_mcache: (styp * mtyp) list Unsynchronized.ref} 
33192  52 

35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

53 
exception UNSOLVABLE of unit 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

54 
exception MTYPE of string * mtyp list * typ list 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

55 
exception MTERM of string * mterm list 
33192  56 

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

57 
fun print_g (_ : string) = () 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

58 
(* val print_g = tracing *) 
33192  59 

60 
val string_for_var = signed_string_of_int 

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

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

63 
fun subscript_string_for_vars sep xs = 

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

65 

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

66 
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

67 
 string_for_sign Minus = "" 
33192  68 

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 
fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus 
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

70 
val negate = xor Minus 
33192  71 

72 
fun string_for_sign_atom (S sn) = string_for_sign sn 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

73 
 string_for_sign_atom (V x) = string_for_var x 
33192  74 

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

76 

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

77 
val bool_M = MType (@{type_name bool}, []) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

78 
val dummy_M = MType (nitpick_prefix ^ "dummy", []) 
33192  79 

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

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

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

82 
fun dest_MFun (MFun z) = z 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

83 
 dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], []) 
33192  84 

85 
val no_prec = 100 

86 

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

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

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

89 
 precedence_of_mtype _ = no_prec 
33192  90 

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

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

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

95 
val prec = precedence_of_mtype M 
33192  96 
val need_parens = (prec < outer_prec) 
97 
in 

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

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

99 
(if M = dummy_M then 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

100 
"_" 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

101 
else case M of 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

102 
MAlpha => "\<alpha>" 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

103 
 MFun (M1, a, M2) => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

104 
aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^ 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

105 
string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

106 
 MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

107 
 MType (s, []) => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

108 
if s = @{type_name prop} orelse s = @{type_name bool} then "o" 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

109 
else s 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

110 
 MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

111 
 MRec (s, _) => "[" ^ s ^ "]") ^ 
33192  112 
(if need_parens then ")" else "") 
113 
end 

114 
in aux 0 end 

115 

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

116 
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

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

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

119 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

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

122 
 precedence_of_mterm (MApp _) = 2 
33192  123 

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

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

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

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

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

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

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

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

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

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

133 
(case m of 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

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

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

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

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

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

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

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

142 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

144 
 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

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

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

147 
MFun (_, _, M12) => M12 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

148 
 M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], []) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

149 

ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

150 
fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 > (fn ms => append ms [m2]) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

151 
 strip_mcomb m = (m, []) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

152 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

154 
({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

155 
no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

156 
datatype_mcache = Unsynchronized.ref [], 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

157 
constr_mcache = Unsynchronized.ref []} : mdata) 
33192  158 

159 
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

160 
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

161 
exists (could_exist_alpha_subtype alpha_T) Ts) 
33192  162 
 could_exist_alpha_subtype alpha_T T = (T = alpha_T) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

163 
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

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

165 
 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

166 
(T = alpha_T orelse is_datatype thy [(NONE, true)] T) 
33192  167 

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

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

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

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

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

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

173 
 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

174 
 exists_alpha_sub_mtype (MRec _) = true 
33192  175 

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

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

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

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

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

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

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

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

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

184 
 exists_alpha_sub_mtype_fresh (MRec _) = true 
33192  185 

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

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

187 
fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z) 
33192  188 

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

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

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

191 
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

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

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

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

195 
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

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

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

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

200 
else repair_mtype cache (M :: seen) M 
33192  201 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

202 
fun repair_datatype_mcache cache = 
33192  203 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

206 
(AList.update (op =) (z, repair_mtype (!cache) [] M)) 
33192  207 
in List.app repair_one (rev (!cache)) end 
208 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

209 
fun repair_constr_mcache dtype_cache constr_mcache = 
33192  210 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

211 
fun repair_one (x, M) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

212 
Unsynchronized.change constr_mcache 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

213 
(AList.update (op =) (x, repair_mtype dtype_cache [] M)) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

214 
in List.app repair_one (!constr_mcache) end 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

215 

ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

216 
fun is_fin_fun_supported_type @{typ prop} = true 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

217 
 is_fin_fun_supported_type @{typ bool} = true 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

218 
 is_fin_fun_supported_type (Type (@{type_name option}, _)) = true 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

219 
 is_fin_fun_supported_type _ = false 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

220 
fun fin_fun_body _ _ (t as @{term False}) = SOME t 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

221 
 fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

222 
 fin_fun_body dom_T ran_T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

223 
((t0 as Const (@{const_name If}, _)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

224 
$ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1') 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

225 
$ t2 $ t3) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

226 
(if loose_bvar1 (t1', 0) then 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

227 
NONE 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

228 
else case fin_fun_body dom_T ran_T t3 of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

229 
NONE => NONE 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

230 
 SOME t3 => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

231 
SOME (t0 $ (Const (@{const_name is_unknown}, dom_T > bool_T) $ t1') 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

232 
$ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3))) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

233 
 fin_fun_body _ _ _ = NONE 
33192  234 

35672  235 
fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus 
236 
T1 T2 = 

33192  237 
let 
35672  238 
val M1 = fresh_mtype_for_type mdata all_minus T1 
239 
val M2 = fresh_mtype_for_type mdata all_minus T2 

240 
val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso 

241 
is_fin_fun_supported_type (body_type T2) then 

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

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

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

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

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

246 
and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T, 
35672  247 
datatype_mcache, constr_mcache, ...}) 
248 
all_minus = 

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

249 
let 
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 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

254 
Type (@{type_name fun}, [T1, T2]) => 
35672  255 
MFun (fresh_mfun_for_fun_type mdata false T1 T2) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

256 
 Type (@{type_name "*"}, [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 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

259 
case AList.lookup (op =) (!datatype_mcache) 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 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

263 
val _ = Unsynchronized.change datatype_mcache (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) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

279 
val _ = Unsynchronized.change datatype_mcache 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

280 
(AList.update (op =) (z, M)) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

281 
val _ = Unsynchronized.change constr_mcache 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

282 
(append (xs ~~ constr_Ms)) 
33192  283 
in 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

284 
if forall (not o is_MRec o snd) (!datatype_mcache) then 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

285 
(repair_datatype_mcache datatype_mcache; 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

286 
repair_constr_mcache (!datatype_mcache) constr_mcache; 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

287 
AList.lookup (op =) (!datatype_mcache) z > the) 
33192  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 
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

297 
 prodM_factors M = [M] 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

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

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

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

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

304 
case sel_no_from_name s of ~1 => bool_M  n => nth arg_Ms n) 
33192  305 
end 
306 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

309 
if could_exist_alpha_sub_mtype thy alpha_T T then 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

310 
case AList.lookup (op =) (!constr_mcache) x of 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

311 
SOME M => M 
35384  312 
 NONE => if T = alpha_T then 
35672  313 
let val M = fresh_mtype_for_type mdata false T in 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

314 
(Unsynchronized.change constr_mcache (cons (x, M)); M) 
35384  315 
end 
316 
else 

35672  317 
(fresh_mtype_for_type mdata false (body_type T); 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

318 
AList.lookup (op =) (!constr_mcache) x > the) 
33192  319 
else 
35672  320 
fresh_mtype_for_type mdata false T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

321 
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

322 
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

323 
> mtype_for_constr mdata > sel_mtype_from_constr_mtype s 
33192  324 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

325 
fun resolve_sign_atom lits (V x) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

326 
x > AList.lookup (op =) lits > Option.map S > the_default (V x) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

327 
 resolve_sign_atom _ a = a 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

330 
fun aux MAlpha = MAlpha 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

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

334 
 aux (MRec z) = MRec z 
33192  335 
in aux end 
336 

337 
datatype comp_op = Eq  Leq 

338 

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

340 
type sign_expr = literal list 

341 

35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

342 
type constraint_set = literal list * comp list * sign_expr list 
33192  343 

344 
fun string_for_comp_op Eq = "=" 

345 
 string_for_comp_op Leq = "\<le>" 

346 

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

348 
 string_for_sign_expr lits = 

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

350 

351 
fun do_literal _ NONE = NONE 

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

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

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

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

356 

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

358 
(case (a1, a2) of 

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

360 
 (V x1, S sn2) => 

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

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

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

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

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

366 
(_, 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

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

368 
 (S Minus, S Plus) => NONE 
33192  369 
 (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps) 
370 
 _ => 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

371 
 do_sign_atom_comp cmp xs a1 a2 (lits, comps) = 
33192  372 
SOME (lits, insert (op =) (a1, a2, cmp, xs) comps) 
373 

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

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

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

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

378 
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

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

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

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

384 
> do_mtype_comp Leq xs M21 M11 
33192  385 
> (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

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

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

388 
 V x => do_mtype_comp Leq (x :: xs) M11 M21) 
33192  389 
else 
390 
SOME accum) 

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

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

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

394 
(accum > fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)] 
33192  395 
handle Library.UnequalLengths => 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

397 
 do_mtype_comp _ _ (MType _) (MType _) accum = 
33192  398 
accum (* no need to compare them thanks to the cache *) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

399 
 do_mtype_comp cmp _ M1 M2 _ = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

400 
raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")", 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

401 
[M1, M2], []) 
33192  402 

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

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

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

406 
case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

407 
NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ()) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

408 
 SOME (lits, comps) => (lits, comps, sexps)) 
33192  409 

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

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

411 
val add_is_sub_mtype = add_mtype_comp Leq 
33192  412 

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

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

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

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

416 
 do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) = 
33192  417 
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

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

420 
 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

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

422 
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

423 
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

424 
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

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

426 
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

427 
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

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

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

430 
 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

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

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

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

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

436 
 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

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

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

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

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

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

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

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

445 
 do_notin_mtype_fv _ _ M _ = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

446 
raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], []) 
33192  447 

35832  448 
fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

449 
(print_g ("*** Add " ^ string_for_mtype M ^ " is " ^ 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

451 
case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

452 
NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ()) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

453 
 SOME (lits, sexps) => (lits, comps, sexps)) 
33192  454 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

455 
val add_mtype_is_concrete = add_notin_mtype_fv Minus 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

456 
val add_mtype_is_complete = add_notin_mtype_fv Plus 
33192  457 

35384  458 
val bool_from_minus = true 
459 

460 
fun bool_from_sign Plus = not bool_from_minus 

461 
 bool_from_sign Minus = bool_from_minus 

462 
fun sign_from_bool b = if b = bool_from_minus then Minus else Plus 

33192  463 

464 
fun prop_for_literal (x, sn) = 

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

466 
fun prop_for_sign_atom_eq (S sn', sn) = 

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

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

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

470 
fun prop_for_exists_eq xs sn = 

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

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

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

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

475 
 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

476 
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

477 
prop_for_sign_atom_eq (a2, Minus)) 
33192  478 
 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

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

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

481 
fun literals_from_assignments max_var assigns lits = 
33192  482 
fold (fn x => fn accum => 
483 
if AList.defined (op =) lits x then 

484 
accum 

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

485 
else case assigns x of 
33192  486 
SOME b => (x, sign_from_bool b) :: accum 
487 
 NONE => accum) (max_var downto 1) lits 

488 

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

490 
string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^ 

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

492 

493 
fun print_problem lits comps sexps = 

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

495 
map string_for_comp comps @ 

496 
map string_for_sign_expr sexps)) 

497 

498 
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

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

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

503 
end 

504 

35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

505 
fun solve max_var (lits, comps, sexps) = 
33192  506 
let 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

507 
fun do_assigns assigns = 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

508 
SOME (literals_from_assignments max_var assigns lits 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

509 
> tap print_solution) 
33192  510 
val _ = print_problem lits comps sexps 
511 
val prop = PropLogic.all (map prop_for_literal lits @ 

512 
map prop_for_comp comps @ 

513 
map prop_for_sign_expr sexps) 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

514 
val default_val = bool_from_sign Minus 
33192  515 
in 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

516 
if PropLogic.eval (K default_val) prop then 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

517 
do_assigns (K (SOME default_val)) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

518 
else 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

519 
let 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

520 
(* use the first ML solver (to avoid startup overhead) *) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

521 
val solvers = !SatSolver.solvers 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

522 
> filter (member (op =) ["dptsat", "dpll"] o fst) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

523 
in 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

524 
case snd (hd solvers) prop of 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

525 
SatSolver.SATISFIABLE assigns => do_assigns assigns 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

526 
 _ => NONE 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

527 
end 
33192  528 
end 
529 

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

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

531 
type mtype_context = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

532 
{bound_Ts: typ list, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

533 
bound_Ms: mtyp list, 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

535 
consts: (styp * mtyp) list} 
33192  536 

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

537 
type accumulator = mtype_context * constraint_set 
33192  538 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

539 
val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []} 
33192  540 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

541 
fun push_bound T M {bound_Ts, bound_Ms, frees, consts} = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

542 
{bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

543 
consts = consts} 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

544 
fun pop_bound {bound_Ts, bound_Ms, frees, consts} = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

545 
{bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

546 
consts = consts} 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

547 
handle List.Empty => initial_gamma (* FIXME: needed? *) 
33192  548 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

549 
fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

550 
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

551 
alpha_T, max_fresh, ...}) = 
33192  552 
let 
35672  553 
val mtype_for = fresh_mtype_for_type mdata false 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

555 
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

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

558 
val abs_M = mtype_for (domain_type (domain_type T)) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

561 
(MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M), 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

562 
(gamma, cset > add_mtype_is_complete abs_M)) 
33192  563 
end 
564 
fun do_equals T (gamma, cset) = 

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

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

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

567 
mtype_for (nth_range_type 2 T))), 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

568 
(gamma, cset > add_mtype_is_concrete M)) 
33192  569 
end 
570 
fun do_robust_set_operation T (gamma, cset) = 

571 
let 

572 
val set_T = domain_type T 

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

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

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

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

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

578 
(gamma, cset > add_is_sub_mtype M1 M3 > add_is_sub_mtype M2 M3)) 
33192  579 
end 
580 
fun do_fragile_set_operation T (gamma, cset) = 

581 
let 

582 
val set_T = domain_type T 

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

583 
val set_M = mtype_for set_T 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

586 
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

587 
 custom_mtype_for T = mtype_for T 
33192  588 
in 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

589 
(custom_mtype_for T, (gamma, cset > add_mtype_is_concrete set_M)) 
33192  590 
end 
591 
fun do_pair_constr T accum = 

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

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

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

594 
(MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

595 
 M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], []) 
33192  596 
fun do_nth_pair_sel n T = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

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

599 
pair (MFun (M, S Minus, if n = 0 then a_M else b_M)) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

603 
val abs_M = mtype_for abs_T 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

604 
val (bound_m, accum) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

605 
accum >> push_bound abs_T abs_M > do_term bound_t 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

608 
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

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

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

611 
val (M1, a, M2) = dest_MFun bound_M 
33192  612 
in 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

614 
MAbs (abs_s, abs_T, M1, a, 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

615 
MApp (MApp (MRaw (connective_t, 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

616 
mtype_for (fastype_of connective_t)), 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

618 
body_m))), accum) 
33192  619 
end 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

620 
and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts}, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

621 
cset)) = 
33192  622 
(case t of 
623 
Const (x as (s, T)) => 

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

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

625 
SOME M => (M, accum) 
33192  626 
 NONE => 
627 
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

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

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

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

633 
 @{const_name Ex} => 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

634 
let val set_T = domain_type T in 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

635 
do_term (Abs (Name.uu, set_T, 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

636 
@{const Not} $ (HOLogic.mk_eq 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

637 
(Abs (Name.uu, domain_type set_T, 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

638 
@{const False}), 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

639 
Bound 0)))) accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

640 
>> mtype_of_mterm 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

641 
end 
33192  642 
 @{const_name "op ="} => do_equals T accum 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

643 
 @{const_name The} => (print_g "*** The"; raise UNSOLVABLE ()) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

644 
 @{const_name Eps} => (print_g "*** Eps"; raise UNSOLVABLE ()) 
33192  645 
 @{const_name If} => 
646 
do_robust_set_operation (range_type T) accum 

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

647 
>> curry3 MFun bool_M (S Minus) 
33192  648 
 @{const_name Pair} => do_pair_constr T accum 
649 
 @{const_name fst} => do_nth_pair_sel 0 T accum 

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

651 
 @{const_name Id} => 

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

652 
(MFun (mtype_for (domain_type T), S Minus, bool_M), accum) 
33192  653 
 @{const_name insert} => 
654 
let 

655 
val set_T = domain_type (range_type T) 

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

656 
val M1 = mtype_for (domain_type set_T) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

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

661 
(MFun (M1, S Minus, MFun (M2, S Minus, M3)), 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

664 
> add_is_sub_mtype M2 M3)) 
33192  665 
end 
666 
 @{const_name converse} => 

667 
let 

668 
val x = Unsynchronized.inc max_fresh 

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

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

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

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

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

673 
in (MFun (ab_set_M, S Minus, ba_set_M), accum) end 
33192  674 
 @{const_name trancl} => do_fragile_set_operation T accum 
675 
 @{const_name rel_comp} => 

676 
let 

677 
val x = Unsynchronized.inc max_fresh 

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

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

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

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

681 
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

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

684 
(MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)), 
33192  685 
accum) 
686 
end 

687 
 @{const_name image} => 

688 
let 

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

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

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

692 
(MFun (MFun (a_M, S Minus, b_M), S Minus, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

693 
MFun (plus_set_mtype_for_dom a_M, S Minus, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

694 
plus_set_mtype_for_dom b_M)), accum) 
33192  695 
end 
35672  696 
 @{const_name finite} => 
697 
let val M1 = mtype_for (domain_type (domain_type T)) in 

698 
(MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum) 

699 
end 

33192  700 
 @{const_name Sigma} => 
701 
let 

702 
val x = Unsynchronized.inc max_fresh 

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

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

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

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

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

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

710 
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

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

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

714 
MFun (a_to_b_set_M, S Minus, ab_set_M)), accum) 
33192  715 
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

716 
 _ => 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

717 
if s = @{const_name safe_The} orelse 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

718 
s = @{const_name safe_Eps} then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

719 
let 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

720 
val a_set_M = mtype_for (domain_type T) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

721 
val a_M = dest_MFun a_set_M > #1 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

722 
in (MFun (a_set_M, S Minus, a_M), accum) end 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

723 
else if s = @{const_name minus_class.minus} andalso 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

724 
is_set_type (domain_type T) then 
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

725 
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

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

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

728 
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

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

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

731 
MFun (right_set_M, S Minus, left_set_M)), 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

733 
> 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

734 
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

735 
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

736 
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

737 
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

738 
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

739 
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

740 
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

741 
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

742 
else if is_sel s then 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

745 
(mtype_for_constr mdata x, accum) 
35672  746 
else if is_built_in_const thy stds fast_descrs x then 
747 
(fresh_mtype_for_type mdata true T, 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

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

749 
let val M = mtype_for T in 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

750 
(M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

751 
frees = frees, consts = (x, M) :: consts}, cset)) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

752 
end) >> curry MRaw t 
33192  753 
 Free (x as (_, T)) => 
754 
(case AList.lookup (op =) frees x of 

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

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

757 
let val M = mtype_for T in 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

758 
(M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

759 
frees = (x, M) :: frees, consts = consts}, cset)) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

760 
end) >> curry MRaw t 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

761 
 Var _ => (print_g "*** Var"; raise UNSOLVABLE ()) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

763 
 Abs (s, T, t') => 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

764 
(case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

765 
SOME t' => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

766 
let 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

767 
val M = mtype_for T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

768 
val a = V (Unsynchronized.inc max_fresh) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

769 
val (m', accum) = do_term t' (accum >> push_bound T M) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

770 
in (MAbs (s, T, M, a, m'), accum >> pop_bound) end 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

771 
 NONE => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

772 
((case t' of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

773 
t1' $ Bound 0 => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

774 
if not (loose_bvar1 (t1', 0)) then 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

775 
do_term (incr_boundvars ~1 t1') accum 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

776 
else 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

777 
raise SAME () 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

778 
 _ => raise SAME ()) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

779 
handle SAME () => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

780 
let 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

781 
val M = mtype_for T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

782 
val (m', accum) = do_term t' (accum >> push_bound T M) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

783 
in 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

784 
(MAbs (s, T, M, S Minus, m'), accum >> pop_bound) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

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

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

787 
$ 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

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

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

790 
$ 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

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

794 
 t1 $ t2 => 

795 
let 

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

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

797 
val (m2, accum) = do_term t2 accum 
33192  798 
in 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

799 
let 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

800 
val T11 = domain_type (fastype_of1 (bound_Ts, t1)) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

801 
val T2 = fastype_of1 (bound_Ts, t2) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

802 
val M11 = mtype_of_mterm m1 > dest_MFun > #1 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

803 
val M2 = mtype_of_mterm m2 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

804 
in (MApp (m1, m2), accum > add_is_sub_mtype M2 M11) end 
33192  805 
end) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

807 
string_for_mterm ctxt m)) 
33192  808 
in do_term end 
809 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

810 
fun force_minus_funs 0 _ = I 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

811 
 force_minus_funs n (M as MFun (M1, _, M2)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

812 
add_mtypes_equal M (MFun (M1, S Minus, M2)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

813 
#> force_minus_funs (n  1) M2 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

814 
 force_minus_funs _ M = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

815 
raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], []) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

816 
fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

817 
let 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

818 
val (m1, accum) = consider_term mdata t1 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

819 
val (m2, accum) = consider_term mdata t2 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

820 
val M1 = mtype_of_mterm m1 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

821 
val M2 = mtype_of_mterm m2 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

822 
val accum = accum > add_mtypes_equal M1 M2 
35672  823 
val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

824 
val m = MApp (MApp (MRaw (Const x, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

825 
MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

826 
in 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

827 
(m, if def then 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

828 
let val (head_m, arg_ms) = strip_mcomb m1 in 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

829 
accum > force_minus_funs (length arg_ms) (mtype_of_mterm head_m) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

830 
end 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

831 
else 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

832 
accum) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

833 
end 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

834 

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

835 
fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) = 
33192  836 
let 
35672  837 
val mtype_for = fresh_mtype_for_type mdata false 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

838 
val do_term = consider_term mdata 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

839 
fun do_formula sn t accum = 
33192  840 
let 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

841 
fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t = 
33192  842 
let 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

843 
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

844 
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex})) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

845 
val (body_m, accum) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

846 
accum > side_cond ? add_mtype_is_complete abs_M 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

847 
>> push_bound abs_T abs_M > do_formula sn body_t 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

848 
val body_M = mtype_of_mterm body_m 
33192  849 
in 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

850 
(MApp (MRaw (Const quant_x, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

851 
MFun (MFun (abs_M, S Minus, body_M), S Minus, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

852 
body_M)), 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

853 
MAbs (abs_s, abs_T, abs_M, S Minus, body_m)), 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

854 
accum >> pop_bound) 
33192  855 
end 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

856 
fun do_equals x t1 t2 = 
33192  857 
case sn of 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

858 
Plus => do_term t accum 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

859 
 Minus => consider_general_equals mdata false x t1 t2 accum 
33192  860 
in 
861 
case t of 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

862 
Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

863 
do_quantifier x s1 T1 t1 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

864 
 Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

865 
 @{const Trueprop} $ t1 => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

866 
let val (m1, accum) = do_formula sn t1 accum in 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

867 
(MApp (MRaw (@{const Trueprop}, mtype_for (bool_T > prop_T)), 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

868 
m1), accum) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

869 
end 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

870 
 @{const Not} $ t1 => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

871 
let val (m1, accum) = do_formula (negate sn) t1 accum in 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

872 
(MApp (MRaw (@{const Not}, mtype_for (bool_T > bool_T)), m1), 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

873 
accum) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

874 
end 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

875 
 Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

876 
do_quantifier x s1 T1 t1 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

877 
 Const (x0 as (s0 as @{const_name Ex}, T0)) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

878 
$ (t1 as Abs (s1, T1, t1')) => 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

879 
(case sn of 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

881 
 Minus => 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

882 
(* FIXME: Move elsewhere *) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

884 
$ (HOLogic.eq_const (domain_type T0) $ t1 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

885 
$ Abs (Name.uu, T1, @{const False}))) accum) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

886 
 Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

887 
do_equals x t1 t2 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

888 
 (t0 as Const (s0, _)) $ t1 $ t2 => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

889 
if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

890 
s0 = @{const_name "op "} orelse s0 = @{const_name "op >"} then 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

891 
let 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

892 
val impl = (s0 = @{const_name "==>"} orelse 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

893 
s0 = @{const_name "op >"}) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

894 
val (m1, accum) = do_formula (sn > impl ? negate) t1 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

895 
val (m2, accum) = do_formula sn t2 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

896 
in 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

897 
(MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

898 
accum) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

899 
end 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

900 
else 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

901 
do_term t accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

902 
 _ => do_term t accum 
33192  903 
end 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

904 
> tap (fn (m, _) => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

905 
print_g ("\<Gamma> \<turnstile> " ^ 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

906 
string_for_mterm ctxt m ^ " : o\<^sup>" ^ 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

907 
string_for_sign sn)) 
33192  908 
in do_formula end 
909 

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

911 
of (rather peculiar) userdefined axioms. *) 

912 
val harmless_consts = 

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

914 
val bounteous_consts = [@{const_name bisim}] 

915 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

916 
fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

917 
 is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

918 
Term.add_consts t [] 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

919 
> filter_out (is_built_in_const thy stds fast_descrs) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

920 
> (forall (member (op =) harmless_consts o original_name o fst) orf 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

921 
exists (member (op =) bounteous_consts o fst)) 
33192  922 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

923 
fun consider_nondefinitional_axiom mdata t = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

924 
if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M)) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

925 
else consider_general_formula mdata Plus t 
33192  926 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

927 
fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t = 
33192  928 
if not (is_constr_pattern_formula thy t) then 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

929 
consider_nondefinitional_axiom mdata t 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

930 
else if is_harmless_axiom mdata t then 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

931 
pair (MRaw (t, dummy_M)) 
33192  932 
else 
933 
let 

35672  934 
val mtype_for = fresh_mtype_for_type mdata false 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

935 
val do_term = consider_term mdata 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

936 
fun do_all quant_t abs_s abs_T body_t accum = 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

937 
let 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

938 
val abs_M = mtype_for abs_T 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

939 
val (body_m, accum) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

940 
accum >> push_bound abs_T abs_M > do_formula body_t 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

941 
val body_M = mtype_of_mterm body_m 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

942 
in 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

943 
(MApp (MRaw (quant_t, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

944 
MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M)), 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

945 
MAbs (abs_s, abs_T, abs_M, S Minus, body_m)), 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

946 
accum >> pop_bound) 
33192  947 
end 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

948 
and do_conjunction t0 t1 t2 accum = 
33192  949 
let 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

950 
val (m1, accum) = do_formula t1 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

951 
val (m2, accum) = do_formula t2 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

952 
in 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

953 
(MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

954 
end 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

955 
and do_implies t0 t1 t2 accum = 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

956 
let 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

957 
val (m1, accum) = do_term t1 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

958 
val (m2, accum) = do_formula t2 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

959 
in 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

960 
(MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

961 
end 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

962 
and do_formula t accum = 
33192  963 
case t of 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

964 
(t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

965 
do_all t0 s1 T1 t1 accum 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

966 
 @{const Trueprop} $ t1 => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

967 
let val (m1, accum) = do_formula t1 accum in 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

968 
(MApp (MRaw (@{const Trueprop}, mtype_for (bool_T > prop_T)), 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

969 
m1), accum) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

970 
end 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

971 
 Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

972 
consider_general_equals mdata true x t1 t2 accum 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

973 
 (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

974 
 (t0 as @{const Pure.conjunction}) $ t1 $ t2 => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

975 
do_conjunction t0 t1 t2 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

976 
 (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) => 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

977 
do_all t0 s0 T1 t1 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

978 
 Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 => 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

979 
consider_general_equals mdata true x t1 t2 accum 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

980 
 (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

981 
 (t0 as @{const "op >"}) $ t1 $ t2 => do_implies t0 t1 t2 accum 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

982 
 _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\ 
33192  983 
\do_formula", [t]) 
984 
in do_formula t end 

985 

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

986 
fun string_for_mtype_of_term ctxt lits t M = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

987 
Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M) 
33192  988 

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

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

990 
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

991 
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts 
33192  992 
> cat_lines > print_g 
993 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

994 
fun amass f t (ms, accum) = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

995 
let val (m, accum) = f t accum in (m :: ms, accum) end 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

996 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

997 
fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

998 
(nondef_ts, def_ts) = 
33192  999 
let 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1000 
val _ = print_g ("****** " ^ which ^ " analysis: " ^ 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1001 
string_for_mtype MAlpha ^ " is " ^ 
33192  1002 
Syntax.string_of_typ ctxt alpha_T) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1003 
val mdata as {max_fresh, constr_mcache, ...} = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1004 
initial_mdata hol_ctxt binarize no_harmless alpha_T 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1005 
val accum = (initial_gamma, ([], [], [])) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

1006 
val (nondef_ms, accum) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1007 
([], accum) > amass (consider_general_formula mdata Plus) (hd nondef_ts) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1008 
> fold (amass (consider_nondefinitional_axiom mdata)) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

1009 
(tl nondef_ts) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

1010 
val (def_ms, (gamma, cset)) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1011 
([], accum) > fold (amass (consider_definitional_axiom mdata)) def_ts 
33192  1012 
in 
1013 
case solve (!max_fresh) cset of 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1014 
SOME lits => (print_mtype_context ctxt lits gamma; 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1015 
SOME (lits, (nondef_ms, def_ms), !constr_mcache)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1016 
 _ => NONE 
33192  1017 
end 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1018 
handle UNSOLVABLE () => NONE 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1019 
 MTYPE (loc, Ms, Ts) => 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1020 
raise BAD (loc, commas (map string_for_mtype Ms @ 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1021 
map (Syntax.string_of_typ ctxt) Ts)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1022 
 MTERM (loc, ms) => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1023 
raise BAD (loc, commas (map (string_for_mterm ctxt) ms)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1024 

ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1025 
val formulas_monotonic = is_some oooo infer "Monotonicity" false 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1026 

ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1027 
fun fin_fun_constr T1 T2 = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1028 
(@{const_name FinFun}, (T1 > T2) > Type (@{type_name fin_fun}, [T1, T2])) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1029 

ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1030 
fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...}) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1031 
binarize finitizes alpha_T tsp = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1032 
case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1033 
SOME (lits, msp, constr_mtypes) => 
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1034 
if forall (curry (op =) Minus o snd) lits then 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1035 
tsp 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1036 
else 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1037 
let 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1038 
fun should_finitize T a = 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1039 
case triple_lookup (type_match thy) finitizes T of 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1040 
SOME (SOME false) => false 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1041 
 _ => resolve_sign_atom lits a = S Plus 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1042 
fun type_from_mtype T M = 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1043 
case (M, T) of 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1044 
(MAlpha, _) => T 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1045 
 (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1046 
Type (if should_finitize T a then @{type_name fin_fun} 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1047 
else @{type_name fun}, map2 type_from_mtype Ts [M1, M2]) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1048 
 (MPair (M1, M2), Type (@{type_name "*"}, Ts)) => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1049 
Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2]) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1050 
 (MType _, _) => T 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1051 
 _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype", 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1052 
[M], [T]) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1053 
fun finitize_constr (x as (s, T)) = 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1054 
(s, case AList.lookup (op =) constr_mtypes x of 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1055 
SOME M => type_from_mtype T M 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1056 
 NONE => T) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1057 
fun term_from_mterm Ts m = 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1058 
case m of 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1059 
MRaw (t, M) => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1060 
let 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1061 
val T = fastype_of1 (Ts, t) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1062 
val T' = type_from_mtype T M 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1063 
in 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1064 
case t of 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1065 
Const (x as (s, _)) => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1066 
if s = @{const_name insert} then 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1067 
case nth_range_type 2 T' of 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1068 
set_T' as Type (@{type_name fin_fun}, [elem_T', _]) => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1069 
Abs (Name.uu, elem_T', Abs (Name.uu, set_T', 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1070 
Const (@{const_name If}, 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1071 
bool_T > set_T' > set_T' > set_T') 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1072 
$ (Const (@{const_name is_unknown}, 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1073 
elem_T' > bool_T) $ Bound 1) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1074 
$ (Const (@{const_name unknown}, set_T')) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1075 
$ (coerce_term hol_ctxt Ts T' T (Const x) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1076 
$ Bound 1 $ Bound 0))) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1077 
 _ => Const (s, T') 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1078 
else if s = @{const_name finite} then 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1079 
case domain_type T' of 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1080 
set_T' as Type (@{type_name fin_fun}, _) => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1081 
Abs (Name.uu, set_T', @{const True}) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1082 
 _ => Const (s, T') 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1083 
else if s = @{const_name "=="} orelse 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1084 
s = @{const_name "op ="} then 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1085 
Const (s, T') 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1086 
else if is_built_in_const thy stds fast_descrs x then 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1087 
coerce_term hol_ctxt Ts T' T t 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1088 
else if is_constr thy stds x then 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1089 
Const (finitize_constr x) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1090 
else if is_sel s then 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1091 
let 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1092 
val n = sel_no_from_name s 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1093 
val x' = 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1094 
x > binarized_and_boxed_constr_for_sel hol_ctxt binarize 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1095 
> finitize_constr 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1096 
val x'' = 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1097 
binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1098 
x' n 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1099 
in Const x'' end 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1100 
else 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1101 
Const (s, T') 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1102 
 Free (s, T) => Free (s, type_from_mtype T M) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1103 
 Bound _ => t 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1104 
 _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm", 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1105 
[m]) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1106 
end 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1107 
 MApp (m1, m2) => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1108 
let 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1109 
val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1110 
val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1111 
val (t1', T2') = 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1112 
case T1 of 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1113 
Type (s, [T11, T12]) => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1114 
(if s = @{type_name fin_fun} then 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1115 
select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1116 
0 (T11 > T12) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1117 
else 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1118 
t1, T11) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1119 
 _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm", 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1120 
[T1], []) 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1121 
in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1122 
 MAbs (s, T, M, a, m') => 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1123 
let 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1124 
val T = type_from_mtype T M 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1125 
val t' = term_from_mterm (T :: Ts) m' 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1126 
val T' = fastype_of1 (T :: Ts, t') 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1127 
in 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1128 
Abs (s, T, t') 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1129 
> should_finitize (T > T') a 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1130 
? construct_value thy stds (fin_fun_constr T T') o single 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1131 
end 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1132 
in 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1133 
Unsynchronized.change constr_cache (map (apsnd (map finitize_constr))); 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1134 
pairself (map (term_from_mterm [])) msp 
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35672
diff
changeset

1135 
end 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1136 
 NONE => tsp 
33192  1137 

1138 
end; 