author  blanchet 
Fri, 05 Feb 2010 12:04:54 +0100  
changeset 35075  888802be2019 
parent 35070  96136eb6218f 
child 35076  cc19e2aef17e 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_model.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:
34974
diff
changeset

3 
Copyright 2009, 2010 
33192  4 

5 
Model reconstruction for Nitpick. 

6 
*) 

7 

8 
signature NITPICK_MODEL = 

9 
sig 

33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33580
diff
changeset

10 
type styp = Nitpick_Util.styp 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

11 
type scope = Nitpick_Scope.scope 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

12 
type rep = Nitpick_Rep.rep 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

13 
type nut = Nitpick_Nut.nut 
33192  14 

15 
type params = { 

16 
show_skolems: bool, 

17 
show_datatypes: bool, 

18 
show_consts: bool} 

19 

20 
structure NameTable : TABLE 

21 

22 
val tuple_list_for_name : 

23 
nut NameTable.table > Kodkod.raw_bound list > nut > int list list 

24 
val reconstruct_hol_model : 

25 
params > scope > (term option * int list) list > styp list > nut list 

26 
> nut list > nut list > nut NameTable.table > Kodkod.raw_bound list 

27 
> Pretty.T * bool 

28 
val prove_hol_model : 

29 
scope > Time.time option > nut list > nut list > nut NameTable.table 

30 
> Kodkod.raw_bound list > term > bool option 

31 
end; 

32 

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

33 
structure Nitpick_Model : NITPICK_MODEL = 
33192  34 
struct 
35 

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

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

37 
open Nitpick_HOL 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

38 
open Nitpick_Scope 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

39 
open Nitpick_Peephole 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

40 
open Nitpick_Rep 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

41 
open Nitpick_Nut 
33192  42 

34126  43 
structure KK = Kodkod 
44 

33192  45 
type params = { 
46 
show_skolems: bool, 

47 
show_datatypes: bool, 

48 
show_consts: bool} 

49 

50 
val unknown = "?" 

51 
val unrep = "\<dots>" 

52 
val maybe_mixfix = "_\<^sup>?" 

53 
val base_mixfix = "_\<^bsub>base\<^esub>" 

54 
val step_mixfix = "_\<^bsub>step\<^esub>" 

55 
val abs_mixfix = "\<guillemotleft>_\<guillemotright>" 

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

56 
val opt_flag = nitpick_prefix ^ "opt" 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

57 
val non_opt_flag = nitpick_prefix ^ "non_opt" 
33192  58 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

59 
(* string > int > int > string *) 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

60 
fun nth_atom_suffix s j k = 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

61 
nat_subscript (k  j) 
33884
a0c43f185fef
generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents:
33705
diff
changeset

62 
> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s))) 
a0c43f185fef
generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents:
33705
diff
changeset

63 
? prefix "\<^isub>," 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

64 
(* string > typ > int > int > string *) 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

65 
fun nth_atom_name prefix (T as Type (s, _)) j k = 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

66 
let val s' = shortest_name s in 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

67 
prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^ 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

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

69 
end 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

70 
 nth_atom_name prefix (T as TFree (s, _)) j k = 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

71 
prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix s j k 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

72 
 nth_atom_name _ T _ _ = raise TYPE ("Nitpick_Model.nth_atom_name", [T], []) 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

73 
(* bool > typ > int > int > term *) 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

74 
fun nth_atom for_auto T j k = 
33192  75 
if for_auto then 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

76 
Free (nth_atom_name (hd (space_explode "." nitpick_prefix)) T j k, T) 
33192  77 
else 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

78 
Const (nth_atom_name "" T j k, T) 
33192  79 

34126  80 
(* term > real *) 
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34936
diff
changeset

81 
fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) = 
34126  82 
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2)) 
83 
 extract_real_number t = real (snd (HOLogic.dest_number t)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

84 
(* term * term > order *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

85 
fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) 
34126  86 
 nice_term_ord tp = Real.compare (pairself extract_real_number tp) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

87 
handle TERM ("dest_number", _) => 
34126  88 
case tp of 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

89 
(t11 $ t12, t21 $ t22) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

90 
(case nice_term_ord (t11, t21) of 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

91 
EQUAL => nice_term_ord (t12, t22) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

92 
 ord => ord) 
34126  93 
 _ => TermOrd.fast_term_ord tp 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

94 

34126  95 
(* nut NameTable.table > KK.raw_bound list > nut > int list list *) 
33192  96 
fun tuple_list_for_name rel_table bounds name = 
97 
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] 

98 

99 
(* term > term *) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

100 
fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

101 
unbit_and_unbox_term t1 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

102 
 unbit_and_unbox_term (Const (@{const_name PairBox}, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

103 
Type ("fun", [T1, Type ("fun", [T2, T3])])) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

104 
$ t1 $ t2) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

105 
let val Ts = map unbit_and_unbox_type [T1, T2] in 
33192  106 
Const (@{const_name Pair}, Ts > Type ("*", Ts)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

107 
$ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2 
33192  108 
end 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

109 
 unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

110 
 unbit_and_unbox_term (t1 $ t2) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

111 
unbit_and_unbox_term t1 $ unbit_and_unbox_term t2 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

112 
 unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

113 
 unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

114 
 unbit_and_unbox_term (Bound j) = Bound j 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

115 
 unbit_and_unbox_term (Abs (s, T, t')) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

116 
Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t') 
33192  117 

118 
(* typ > typ > (typ * typ) * (typ * typ) *) 

119 
fun factor_out_types (T1 as Type ("*", [T11, T12])) 

120 
(T2 as Type ("*", [T21, T22])) = 

121 
let val (n1, n2) = pairself num_factors_in_type (T11, T21) in 

122 
if n1 = n2 then 

123 
let 

124 
val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22 

125 
in 

126 
((Type ("*", [T11, T11']), opt_T12'), 

127 
(Type ("*", [T21, T21']), opt_T22')) 

128 
end 

129 
else if n1 < n2 then 

130 
case factor_out_types T1 T21 of 

131 
(p1, (T21', NONE)) => (p1, (T21', SOME T22)) 

132 
 (p1, (T21', SOME T22')) => 

133 
(p1, (T21', SOME (Type ("*", [T22', T22])))) 

134 
else 

135 
swap (factor_out_types T2 T1) 

136 
end 

137 
 factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE)) 

138 
 factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22)) 

139 
 factor_out_types T1 T2 = ((T1, NONE), (T2, NONE)) 

140 

141 
(* bool > typ > typ > (term * term) list > term *) 

142 
fun make_plain_fun maybe_opt T1 T2 = 

143 
let 

144 
(* typ > typ > (term * term) list > term *) 

145 
fun aux T1 T2 [] = 

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

146 
Const (if maybe_opt then opt_flag else non_opt_flag, T1 > T2) 
33192  147 
 aux T1 T2 ((t1, t2) :: ps) = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

148 
Const (@{const_name fun_upd}, (T1 > T2) > T1 > T2 > T1 > T2) 
33192  149 
$ aux T1 T2 ps $ t1 $ t2 
150 
in aux T1 T2 o rev end 

151 
(* term > bool *) 

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

152 
fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag) 
33192  153 
 is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) = 
154 
is_plain_fun t0 

155 
 is_plain_fun _ = false 

156 
(* term > bool * (term list * term list) *) 

157 
val dest_plain_fun = 

158 
let 

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

159 
(* term > bool * (term list * term list) *) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

160 
fun aux (Const (s, _)) = (s <> non_opt_flag, ([], [])) 
33192  161 
 aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = 
162 
let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end 

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

163 
 aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t]) 
33192  164 
in apsnd (pairself rev) o aux end 
165 

33565
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

166 
(* typ > typ > typ > term > term * term *) 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

167 
fun break_in_two T T1 T2 t = 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

168 
let 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

169 
val ps = HOLogic.flat_tupleT_paths T 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

170 
val cut = length (HOLogic.strip_tupleT T1) 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

171 
val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2) 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

172 
val (ts1, ts2) = t > HOLogic.strip_ptuple ps > chop cut 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

173 
in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end 
33192  174 
(* typ > term > term > term *) 
175 
fun pair_up (Type ("*", [T1', T2'])) 

176 
(t1 as Const (@{const_name Pair}, 

177 
Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12) 

178 
t2 = 

179 
if T1 = T1' then HOLogic.mk_prod (t1, t2) 

180 
else HOLogic.mk_prod (t11, pair_up T2' t12 t2) 

181 
 pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2) 

182 
(* typ > term > term list * term list > (term * term) list*) 

183 
fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3 

184 

185 
(* typ > typ > typ > term > term *) 

186 
fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t = 

187 
let 

33565
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

188 
(* typ > typ > typ > typ > term > term *) 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

189 
fun do_curry T1 T1a T1b T2 t = 
33192  190 
let 
191 
val (maybe_opt, ps) = dest_plain_fun t 

192 
val ps = 

33565
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

193 
ps >> map (break_in_two T1 T1a T1b) 
33192  194 
> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2)))) 
195 
> AList.coalesce (op =) 

196 
> map (apsnd (make_plain_fun maybe_opt T1b T2)) 

197 
in make_plain_fun maybe_opt T1a (T1b > T2) ps end 

198 
(* typ > typ > term > term *) 

199 
and do_uncurry T1 T2 t = 

200 
let 

201 
val (maybe_opt, tsp) = dest_plain_fun t 

202 
val ps = 

203 
tsp > op ~~ 

204 
> maps (fn (t1, t2) => 

205 
multi_pair_up T1 t1 (snd (dest_plain_fun t2))) 

206 
in make_plain_fun maybe_opt T1 T2 ps end 

207 
(* typ > typ > typ > typ > term > term *) 

208 
and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' > T2') 

209 
 do_arrow T1' T2' T1 T2 

210 
(Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = 

211 
Const (@{const_name fun_upd}, 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

212 
(T1' > T2') > T1' > T2' > T1' > T2') 
33192  213 
$ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2 
214 
 do_arrow _ _ _ _ t = 

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

215 
raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t]) 
33192  216 
and do_fun T1' T2' T1 T2 t = 
217 
case factor_out_types T1' T1 of 

218 
((_, NONE), (_, NONE)) => t > do_arrow T1' T2' T1 T2 

219 
 ((_, NONE), (T1a, SOME T1b)) => 

33565
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

220 
t > do_curry T1 T1a T1b T2 > do_arrow T1' T2' T1a (T1b > T2) 
33192  221 
 ((T1a', SOME T1b'), (_, NONE)) => 
222 
t > do_arrow T1a' (T1b' > T2') T1 T2 > do_uncurry T1' T2' 

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

223 
 _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], []) 
33192  224 
(* typ > typ > term > term *) 
225 
and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t = 

226 
do_fun T1' T2' T1 T2 t 

227 
 do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2])) 

228 
(Const (@{const_name Pair}, _) $ t1 $ t2) = 

229 
Const (@{const_name Pair}, Ts' > T') 

230 
$ do_term T1' T1 t1 $ do_term T2' T2 t2 

231 
 do_term T' T t = 

232 
if T = T' then t 

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

233 
else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], []) 
33192  234 
in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end 
34998  235 
 typecast_fun T' _ _ _ = 
236 
raise TYPE ("Nitpick_Model.typecast_fun", [T'], []) 

33192  237 

238 
(* term > string *) 

239 
fun truth_const_sort_key @{const True} = "0" 

240 
 truth_const_sort_key @{const False} = "2" 

241 
 truth_const_sort_key _ = "1" 

242 

243 
(* typ > term list > term *) 

244 
fun mk_tuple (Type ("*", [T1, T2])) ts = 

245 
HOLogic.mk_prod (mk_tuple T1 ts, 

246 
mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1)))) 

247 
 mk_tuple _ (t :: _) = t 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

248 
 mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) 
33192  249 

250 
(* string * string * string * string > scope > nut list > nut list 

34126  251 
> nut list > nut NameTable.table > KK.raw_bound list > typ > typ > rep 
252 
> int list list > term *) 

33192  253 
fun reconstruct_term (maybe_name, base_name, step_name, abs_name) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

254 
({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...} 
33192  255 
: scope) sel_names rel_table bounds = 
256 
let 

257 
val for_auto = (maybe_name = "") 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

258 
(* int list list > int *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

259 
fun value_of_bits jss = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

260 
let 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

261 
val j0 = offset_of_type ofs @{typ unsigned_bit} 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

262 
val js = map (Integer.add (~ j0) o the_single) jss 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

263 
in 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

264 
fold (fn j => Integer.add (reasonable_power 2 j > j = bits ? op ~)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

265 
js 0 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

266 
end 
33192  267 
(* bool > typ > typ > (term * term) list > term *) 
268 
fun make_set maybe_opt T1 T2 = 

269 
let 

270 
val empty_const = Const (@{const_name Set.empty}, T1 > T2) 

271 
val insert_const = Const (@{const_name insert}, 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

272 
T1 > (T1 > T2) > T1 > T2) 
33192  273 
(* (term * term) list > term *) 
274 
fun aux [] = 

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

275 
if maybe_opt andalso not (is_complete_type datatypes T1) then 
33192  276 
insert_const $ Const (unrep, T1) $ empty_const 
277 
else 

278 
empty_const 

279 
 aux ((t1, t2) :: zs) = 

280 
aux zs > t2 <> @{const False} 

281 
? curry (op $) (insert_const 

282 
$ (t1 > t2 <> @{const True} 

283 
? curry (op $) 

284 
(Const (maybe_name, 

285 
T1 > T1)))) 

286 
in aux end 

287 
(* typ > typ > typ > (term * term) list > term *) 

288 
fun make_map T1 T2 T2' = 

289 
let 

290 
val update_const = Const (@{const_name fun_upd}, 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

291 
(T1 > T2) > T1 > T2 > T1 > T2) 
33192  292 
(* (term * term) list > term *) 
293 
fun aux' [] = Const (@{const_name Map.empty}, T1 > T2) 

294 
 aux' ((t1, t2) :: ps) = 

295 
(case t2 of 

296 
Const (@{const_name None}, _) => aux' ps 

297 
 _ => update_const $ aux' ps $ t1 $ t2) 

298 
fun aux ps = 

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

299 
if not (is_complete_type datatypes T1) then 
33192  300 
update_const $ aux' ps $ Const (unrep, T1) 
301 
$ (Const (@{const_name Some}, T2' > T2) $ Const (unknown, T2')) 

302 
else 

303 
aux' ps 

304 
in aux end 

305 
(* typ list > term > term *) 

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

306 
fun polish_funs Ts t = 
33192  307 
(case fastype_of1 (Ts, t) of 
308 
Type ("fun", [T1, T2]) => 

309 
if is_plain_fun t then 

310 
case T2 of 

311 
@{typ bool} => 

312 
let 

313 
val (maybe_opt, ts_pair) = 

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

314 
dest_plain_fun t > pairself (map (polish_funs Ts)) 
33192  315 
in 
316 
make_set maybe_opt T1 T2 

317 
(sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair)) 

318 
end 

319 
 Type (@{type_name option}, [T2']) => 

320 
let 

321 
val ts_pair = snd (dest_plain_fun 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:
34974
diff
changeset

322 
> pairself (map (polish_funs Ts)) 
33192  323 
in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end 
324 
 _ => raise SAME () 

325 
else 

326 
raise SAME () 

327 
 _ => raise SAME ()) 

328 
handle SAME () => 

329 
case t 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:
34974
diff
changeset

330 
(t1 as Const (@{const_name fun_upd}, _) $ t11 $ _) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

331 
$ (t2 as Const (s, _)) => 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

332 
if s = unknown then polish_funs Ts t11 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

333 
else polish_funs Ts t1 $ polish_funs Ts t2 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

334 
 t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

335 
 Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t') 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

336 
 Const (s, Type ("fun", [T1, T2])) => 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

337 
if s = opt_flag orelse s = non_opt_flag then 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

338 
Abs ("x", T1, Const (unknown, T2)) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

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

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

341 
 t => t 
33192  342 
(* bool > typ > typ > typ > term list > term list > term *) 
343 
fun make_fun maybe_opt T1 T2 T' ts1 ts2 = 

34126  344 
ts1 ~~ ts2 > sort (nice_term_ord o pairself fst) 
34998  345 
> make_plain_fun maybe_opt T1 T2 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

346 
> unbit_and_unbox_term 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

347 
> typecast_fun (unbit_and_unbox_type T') 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

348 
(unbit_and_unbox_type T1) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

349 
(unbit_and_unbox_type T2) 
33192  350 
(* (typ * int) list > typ > typ > int > term *) 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

351 
fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k = 
33192  352 
let 
353 
val k1 = card_of_type card_assigns T1 

354 
val k2 = card_of_type card_assigns T2 

355 
in 

356 
term_for_rep seen T T' (Vect (k1, Atom (k2, 0))) 

357 
[nth_combination (replicate k1 (k2, 0)) j] 

358 
handle General.Subscript => 

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

359 
raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom", 
33192  360 
signed_string_of_int j ^ " for " ^ 
361 
string_for_rep (Vect (k1, Atom (k2, 0)))) 

362 
end 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

363 
 term_for_atom seen (Type ("*", [T1, T2])) _ j k = 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

364 
let 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

365 
val k1 = card_of_type card_assigns T1 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

366 
val k2 = k div k1 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

367 
in 
33192  368 
list_comb (HOLogic.pair_const T1 T2, 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

369 
map3 (fn T => term_for_atom seen T T) [T1, T2] 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

370 
[j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *) 
33192  371 
end 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

372 
 term_for_atom seen @{typ prop} _ j k = 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

373 
HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k) 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

374 
 term_for_atom _ @{typ bool} _ j _ = 
33192  375 
if j = 0 then @{const False} else @{const True} 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

376 
 term_for_atom _ @{typ unit} _ _ _ = @{const Unity} 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

377 
 term_for_atom seen T _ j k = 
33192  378 
if T = nat_T then 
379 
HOLogic.mk_number nat_T j 

380 
else if T = int_T then 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

381 
HOLogic.mk_number int_T (int_for_atom (k, 0) j) 
33192  382 
else if is_fp_iterator_type T then 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

383 
HOLogic.mk_number nat_T (k  j  1) 
33192  384 
else if T = @{typ bisim_iterator} then 
385 
HOLogic.mk_number nat_T j 

386 
else case datatype_spec datatypes T of 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

387 
NONE => nth_atom for_auto T j k 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

388 
 SOME {deep = false, ...} => nth_atom for_auto T j k 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

389 
 SOME {co, constrs, ...} => 
33192  390 
let 
391 
(* styp > int list *) 

392 
fun tuples_for_const (s, T) = 

393 
tuple_list_for_name rel_table bounds (ConstName (s, T, Any)) 

394 
(* unit > indexname * typ *) 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

395 
fun var () = ((nth_atom_name "" T j k, 0), T) 
33192  396 
val discr_jsss = map (tuples_for_const o discr_for_constr o #const) 
397 
constrs 

398 
val real_j = j + offset_of_type ofs T 

399 
val constr_x as (constr_s, constr_T) = 

400 
get_first (fn (jss, {const, ...}) => 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

401 
if member (op =) jss [real_j] then SOME const 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

402 
else NONE) 
33192  403 
(discr_jsss ~~ constrs) > the 
404 
val arg_Ts = curried_binder_types constr_T 

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

405 
val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x) 
33192  406 
(index_seq 0 (length arg_Ts)) 
407 
val sel_Rs = 

408 
map (fn x => get_first 

409 
(fn ConstName (s', T', R) => 

410 
if (s', T') = x then SOME R else NONE 

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

411 
 u => raise NUT ("Nitpick_Model.reconstruct_\ 
33192  412 
\term.term_for_atom", [u])) 
413 
sel_names > the) sel_xs 

414 
val arg_Rs = map (snd o dest_Func) sel_Rs 

415 
val sel_jsss = map tuples_for_const sel_xs 

416 
val arg_jsss = 

417 
map (map_filter (fn js => if hd js = real_j then SOME (tl js) 

418 
else NONE)) sel_jsss 

419 
val uncur_arg_Ts = binder_types constr_T 

420 
in 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

421 
if co andalso member (op =) seen (T, j) then 
33192  422 
Var (var ()) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

423 
else if constr_s = @{const_name Word} then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

424 
HOLogic.mk_number 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

425 
(if T = @{typ "unsigned_bit word"} then nat_T else int_T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

426 
(value_of_bits (the_single arg_jsss)) 
33192  427 
else 
428 
let 

429 
val seen = seen > co ? cons (T, j) 

430 
val ts = 

431 
if length arg_Ts = 0 then 

432 
[] 

433 
else 

434 
map3 (fn Ts => term_for_rep seen Ts Ts) arg_Ts arg_Rs 

435 
arg_jsss 

436 
> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts) 

437 
> dest_n_tuple (length uncur_arg_Ts) 

438 
val t = 

439 
if constr_s = @{const_name Abs_Frac} then 

440 
let 

441 
val num_T = body_type T 

442 
(* int > term *) 

443 
val mk_num = HOLogic.mk_number num_T 

444 
in 

445 
case ts of 

446 
[Const (@{const_name Pair}, _) $ t1 $ t2] => 

447 
(case snd (HOLogic.dest_number t1) of 

448 
0 => mk_num 0 

449 
 n1 => case HOLogic.dest_number t2 > snd of 

450 
1 => mk_num n1 

34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34936
diff
changeset

451 
 n2 => Const (@{const_name Algebras.divide}, 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

452 
num_T > num_T > num_T) 
33192  453 
$ mk_num n1 $ mk_num n2) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

454 
 _ => raise TERM ("Nitpick_Model.reconstruct_term.\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

455 
\term_for_atom (Abs_Frac)", ts) 
33192  456 
end 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

457 
else if not for_auto andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

458 
(is_abs_fun thy constr_x orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

459 
constr_s = @{const_name Quot}) then 
33192  460 
Const (abs_name, constr_T) $ the_single ts 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

461 
else if not for_auto andalso 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

462 
constr_s = @{const_name NonStd} then 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

463 
Const (fst (dest_Const (the_single ts)), T) 
33192  464 
else 
465 
list_comb (Const constr_x, ts) 

466 
in 

467 
if co then 

468 
let val var = var () in 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

469 
if exists_subterm (curry (op =) (Var var)) t then 
33192  470 
Const (@{const_name The}, (T > bool_T) > T) 
471 
$ Abs ("\<omega>", T, 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

472 
Const (@{const_name "op ="}, T > T > bool_T) 
33192  473 
$ Bound 0 $ abstract_over (Var var, t)) 
474 
else 

475 
t 

476 
end 

477 
else 

478 
t 

479 
end 

480 
end 

481 
(* (typ * int) list > int > rep > typ > typ > typ > int list 

482 
> term *) 

483 
and term_for_vect seen k R T1 T2 T' js = 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

484 
make_fun true T1 T2 T' 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

485 
(map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k)) 
33192  486 
(map (term_for_rep seen T2 T2 R o single) 
487 
(batch_list (arity_of_rep R) js)) 

488 
(* (typ * int) list > typ > typ > rep > int list list > term *) 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

489 
and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1 
33192  490 
 term_for_rep seen T T' (R as Atom (k, j0)) [[j]] = 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

491 
if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j  j0) k 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

492 
else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R]) 
33192  493 
 term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] = 
494 
let 

495 
val arity1 = arity_of_rep R1 

496 
val (js1, js2) = chop arity1 js 

497 
in 

498 
list_comb (HOLogic.pair_const T1 T2, 

499 
map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2] 

500 
[[js1], [js2]]) 

501 
end 

502 
 term_for_rep seen (Type ("fun", [T1, T2])) T' (R as Vect (k, R')) [js] = 

503 
term_for_vect seen k R' T1 T2 T' js 

504 
 term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut)) 

505 
jss = 

506 
let 

507 
val jss1 = all_combinations_for_rep R1 

508 
val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1 

509 
val ts2 = 

510 
map (fn js => term_for_rep seen T2 T2 (Atom (2, 0)) 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

511 
[[int_for_bool (member (op =) jss js)]]) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

512 
jss1 
33192  513 
in make_fun false T1 T2 T' ts1 ts2 end 
514 
 term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss = 

515 
let 

516 
val arity1 = arity_of_rep R1 

517 
val jss1 = all_combinations_for_rep R1 

518 
val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1 

519 
val grouped_jss2 = AList.group (op =) (map (chop arity1) jss) 

520 
val ts2 = map (term_for_rep seen T2 T2 R2 o the_default [] 

521 
o AList.lookup (op =) grouped_jss2) jss1 

522 
in make_fun true T1 T2 T' ts1 ts2 end 

523 
 term_for_rep seen T T' (Opt R) jss = 

524 
if null jss then Const (unknown, T) else term_for_rep seen T T' R jss 

525 
 term_for_rep seen T _ R jss = 

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

526 
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", 
33192  527 
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ 
528 
string_of_int (length jss)) 

529 
in 

34998  530 
polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] 
33192  531 
end 
532 

34126  533 
(* scope > nut list > nut NameTable.table > KK.raw_bound list > nut 
33192  534 
> term *) 
535 
fun term_for_name scope sel_names rel_table bounds name = 

536 
let val T = type_of name in 

537 
tuple_list_for_name rel_table bounds name 

538 
> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T 

539 
(rep_of name) 

540 
end 

541 

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

542 
(* Proof.context > (string * string * string * string) * Proof.context *) 
33192  543 
fun add_wacky_syntax ctxt = 
544 
let 

545 
(* term > string *) 

546 
val name_of = fst o dest_Const 

547 
val thy = ProofContext.theory_of ctxt > Context.reject_draft 

548 
val (maybe_t, thy) = 

33202  549 
Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), 
550 
Mixfix (maybe_mixfix, [1000], 1000)) thy 

33192  551 
val (base_t, thy) = 
33202  552 
Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}), 
553 
Mixfix (base_mixfix, [1000], 1000)) thy 

33192  554 
val (step_t, thy) = 
33202  555 
Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}), 
556 
Mixfix (step_mixfix, [1000], 1000)) thy 

33192  557 
val (abs_t, thy) = 
33202  558 
Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}), 
559 
Mixfix (abs_mixfix, [40], 40)) thy 

33192  560 
in 
561 
((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t), 

562 
ProofContext.transfer_syntax thy ctxt) 

563 
end 

564 

565 
(* term > term *) 

566 
fun unfold_outer_the_binders (t as Const (@{const_name The}, _) 

567 
$ Abs (s, T, Const (@{const_name "op ="}, _) 

568 
$ Bound 0 $ t')) = 

569 
betapply (Abs (s, T, t'), t) > unfold_outer_the_binders 

570 
 unfold_outer_the_binders t = t 

571 
(* typ list > int > term * term > bool *) 

572 
fun bisimilar_values _ 0 _ = true 

573 
 bisimilar_values coTs max_depth (t1, t2) = 

574 
let val T = fastype_of t1 in 

575 
if exists_subtype (member (op =) coTs) T then 

576 
let 

577 
val ((head1, args1), (head2, args2)) = 

578 
pairself (strip_comb o unfold_outer_the_binders) (t1, t2) 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

579 
val max_depth = max_depth  (if member (op =) coTs T then 1 else 0) 
33192  580 
in 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

581 
head1 = head2 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

582 
forall (bisimilar_values coTs max_depth) (args1 ~~ args2) 
33192  583 
end 
584 
else 

585 
t1 = t2 

586 
end 

587 

588 
(* params > scope > (term option * int list) list > styp list > nut list 

34126  589 
> nut list > nut list > nut NameTable.table > KK.raw_bound list 
33192  590 
> Pretty.T * bool *) 
591 
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} 

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

592 
({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs, 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

593 
user_axioms, debug, binary_ints, destroy_constrs, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

594 
specialize, skolemize, star_linear_preds, uncurry, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

595 
fast_descrs, tac_timeout, evals, case_names, def_table, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

596 
nondef_table, user_nondefs, simp_table, psimp_table, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

597 
intro_table, ground_thm_table, ersatz_table, skolems, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

598 
special_funs, unrolled_preds, wf_cache, constr_cache}, 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

599 
card_assigns, bits, bisim_depth, datatypes, ofs} : scope) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

600 
formats all_frees free_names sel_names nonsel_names rel_table bounds = 
33192  601 
let 
602 
val (wacky_names as (_, base_name, step_name, _), ctxt) = 

603 
add_wacky_syntax ctxt 

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

604 
val hol_ctxt = 
33192  605 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

606 
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

607 
binary_ints = binary_ints, destroy_constrs = destroy_constrs, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

608 
specialize = specialize, skolemize = skolemize, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

609 
star_linear_preds = star_linear_preds, uncurry = uncurry, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

610 
fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

611 
case_names = case_names, def_table = def_table, 
33192  612 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
613 
simp_table = simp_table, psimp_table = psimp_table, 

614 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

615 
ersatz_table = ersatz_table, skolems = skolems, 

616 
special_funs = special_funs, unrolled_preds = unrolled_preds, 

33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33571
diff
changeset

617 
wf_cache = wf_cache, constr_cache = constr_cache} 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

618 
val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns, 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

619 
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

620 
ofs = ofs} 
33192  621 
(* typ > typ > rep > int list list > term *) 
622 
val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table 

623 
bounds 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

624 
(* nat > typ > nat > typ *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

625 
fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]] 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

626 
(* nat > typ > typ list *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

627 
fun all_values_of_type card T = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

628 
index_seq 0 card > map (nth_value_of_type card T) > sort nice_term_ord 
33192  629 
(* dtype_spec list > dtype_spec > bool *) 
630 
fun is_codatatype_wellformed (cos : dtype_spec list) 

631 
({typ, card, ...} : dtype_spec) = 

632 
let 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

633 
val ts = all_values_of_type card typ 
33192  634 
val max_depth = Integer.sum (map #card cos) 
635 
in 

636 
forall (not o bisimilar_values (map #typ cos) max_depth) 

637 
(all_distinct_unordered_pairs_of ts) 

638 
end 

639 
(* string > Pretty.T *) 

640 
fun pretty_for_assign name = 

641 
let 

642 
val (oper, (t1, T'), T) = 

643 
case name of 

644 
FreeName (s, T, _) => 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

645 
let val t = Free (s, unbit_and_unbox_type T) in 
33192  646 
("=", (t, format_term_type thy def_table formats t), T) 
647 
end 

648 
 ConstName (s, T, _) => 

649 
(assign_operator_for_const (s, T), 

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

650 
user_friendly_const hol_ctxt (base_name, step_name) formats (s, T), 
33192  651 
T) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

652 
 _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\ 
33192  653 
\pretty_for_assign", [name]) 
654 
val t2 = if rep_of name = Any then 

655 
Const (@{const_name undefined}, T') 

656 
else 

657 
tuple_list_for_name rel_table bounds name 

658 
> term_for_rep T T' (rep_of name) 

659 
in 

660 
Pretty.block (Pretty.breaks 

33571  661 
[setmp_show_all_types (Syntax.pretty_term ctxt) t1, 
33192  662 
Pretty.str oper, Syntax.pretty_term ctxt t2]) 
663 
end 

664 
(* dtype_spec > Pretty.T *) 

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

665 
fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) = 
33192  666 
Pretty.block (Pretty.breaks 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

667 
[Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=", 
33192  668 
Pretty.enum "," "{" "}" 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

669 
(map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

670 
(if complete then [] else [Pretty.str unrep]))]) 
33192  671 
(* typ > dtype_spec list *) 
672 
fun integer_datatype T = 

673 
[{typ = T, card = card_of_type card_assigns T, co = false, 

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

674 
complete = false, concrete = true, deep = true, constrs = []}] 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

675 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] 
33192  676 
val (codatatypes, datatypes) = 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

677 
datatypes > filter #deep > List.partition #co 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

678 
> append (integer_datatype nat_T @ integer_datatype int_T) 
33192  679 
val block_of_datatypes = 
680 
if show_datatypes andalso not (null datatypes) then 

681 
[Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":") 

682 
(map pretty_for_datatype datatypes)] 

683 
else 

684 
[] 

685 
val block_of_codatatypes = 

686 
if show_datatypes andalso not (null codatatypes) then 

687 
[Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":") 

688 
(map pretty_for_datatype codatatypes)] 

689 
else 

690 
[] 

691 
(* bool > string > nut list > Pretty.T list *) 

692 
fun block_of_names show title names = 

693 
if show andalso not (null names) then 

694 
Pretty.str (title ^ plural_s_for_list names ^ ":") 

695 
:: map (Pretty.indent indent_size o pretty_for_assign) 

696 
(sort_wrt (original_name o nickname_of) names) 

697 
else 

698 
[] 

699 
val (skolem_names, nonskolem_nonsel_names) = 

700 
List.partition is_skolem_name nonsel_names 

701 
val (eval_names, noneval_nonskolem_nonsel_names) = 

702 
List.partition (String.isPrefix eval_prefix o nickname_of) 

703 
nonskolem_nonsel_names 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

704 
> filter_out (curry (op =) @{const_name bisim_iterator_max} 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

705 
o nickname_of) 
33192  706 
val free_names = 
707 
map (fn x as (s, T) => 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

708 
case filter (curry (op =) x 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

709 
o pairf nickname_of (unbit_and_unbox_type o type_of)) 
33192  710 
free_names of 
711 
[name] => name 

712 
 [] => FreeName (s, T, Any) 

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

713 
 _ => raise TERM ("Nitpick_Model.reconstruct_hol_model", 
33192  714 
[Const x])) all_frees 
715 
val chunks = block_of_names true "Free variable" free_names @ 

716 
block_of_names show_skolems "Skolem constant" skolem_names @ 

717 
block_of_names true "Evaluated term" eval_names @ 

718 
block_of_datatypes @ block_of_codatatypes @ 

719 
block_of_names show_consts "Constant" 

720 
noneval_nonskolem_nonsel_names 

721 
in 

722 
(Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"] 

723 
else chunks), 

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

724 
bisim_depth >= 0 orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

725 
forall (is_codatatype_wellformed codatatypes) codatatypes) 
33192  726 
end 
727 

728 
(* scope > Time.time option > nut list > nut list > nut NameTable.table 

34126  729 
> KK.raw_bound list > term > bool option *) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

730 
fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...}, 
34998  731 
card_assigns, ...}) 
33192  732 
auto_timeout free_names sel_names rel_table bounds prop = 
733 
let 

734 
(* typ * int > term *) 

735 
fun free_type_assm (T, k) = 

736 
let 

737 
(* int > term *) 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

738 
fun atom j = nth_atom true T j k 
33192  739 
fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j 
740 
val eqs = map equation_for_atom (index_seq 0 k) 

741 
val compreh_assm = 

742 
Const (@{const_name All}, (T > bool_T) > bool_T) 

743 
$ Abs ("x", T, foldl1 HOLogic.mk_disj eqs) 

744 
val distinct_assm = distinctness_formula T (map atom (index_seq 0 k)) 

34998  745 
in s_conj (compreh_assm, distinct_assm) end 
33192  746 
(* nut > term *) 
747 
fun free_name_assm name = 

748 
HOLogic.mk_eq (Free (nickname_of name, type_of name), 

749 
term_for_name scope sel_names rel_table bounds name) 

750 
val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns) 

751 
val model_assms = map free_name_assm free_names 

34998  752 
val assm = foldr1 s_conj (freeT_assms @ model_assms) 
33192  753 
(* bool > bool *) 
754 
fun try_out negate = 

755 
let 

756 
val concl = (negate ? curry (op $) @{const Not}) 

757 
(ObjectLogic.atomize_term thy prop) 

34998  758 
val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl)) 
33192  759 
> map_types (map_type_tfree 
34998  760 
(fn (s, []) => TFree (s, HOLogic.typeS) 
761 
 x => TFree x)) 

762 
val _ = if debug then 

763 
priority ((if negate then "Genuineness" else "Spuriousness") ^ 

764 
" goal: " ^ Syntax.string_of_term ctxt prop ^ ".") 

765 
else 

766 
() 

767 
val goal = prop > cterm_of thy > Goal.init 

33192  768 
in 
769 
(goal > SINGLE (DETERM_TIMEOUT auto_timeout 

770 
(auto_tac (clasimpset_of ctxt))) 

771 
> the > Goal.finish ctxt; true) 

772 
handle THM _ => false 

773 
 TimeLimit.TimeOut => false 

774 
end 

775 
in 

33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33580
diff
changeset

776 
if try_out false then SOME true 
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33580
diff
changeset

777 
else if try_out true then SOME false 
33192  778 
else NONE 
779 
end 

780 

781 
end; 