author  haftmann 
Fri, 22 Jan 2010 16:56:51 +0100  
changeset 34962  807f6ce0273d 
parent 33963  977b94b64905 
child 35021  c839a4c670c6 
permissions  rwrr 
24584  1 
(* Title: HOL/Tools/inductive_codegen.ML 
11539  2 
Author: Stefan Berghofer, TU Muenchen 
11537  3 

11539  4 
Code generator for inductive predicates. 
11537  5 
*) 
6 

7 
signature INDUCTIVE_CODEGEN = 

8 
sig 

22271  9 
val add : string option > int option > attribute 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

10 
val test_fn : (int * int * int > term list option) Unsynchronized.ref 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

11 
val test_term: Proof.context > term > int > term list option 
18708  12 
val setup : theory > theory 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

13 
val quickcheck_setup : theory > theory 
11537  14 
end; 
15 

16 
structure InductiveCodegen : INDUCTIVE_CODEGEN = 

17 
struct 

18 

19 
open Codegen; 

20 

12557  21 
(**** theory data ****) 
22 

18930
29d39c10822e
replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents:
18928
diff
changeset

23 
fun merge_rules tabs = 
22642  24 
Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs; 
18930
29d39c10822e
replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents:
18928
diff
changeset

25 

33522  26 
structure CodegenData = Theory_Data 
22846  27 
( 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

28 
type T = 
22271  29 
{intros : (thm * (string * int)) list Symtab.table, 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

30 
graph : unit Graph.T, 
16645  31 
eqns : (thm * string) list Symtab.table}; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

32 
val empty = 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

33 
{intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty}; 
16424  34 
val extend = I; 
33522  35 
fun merge ({intros=intros1, graph=graph1, eqns=eqns1}, 
36 
{intros=intros2, graph=graph2, eqns=eqns2}) : T = 

18930
29d39c10822e
replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents:
18928
diff
changeset

37 
{intros = merge_rules (intros1, intros2), 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

38 
graph = Graph.merge (K true) (graph1, graph2), 
18930
29d39c10822e
replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents:
18928
diff
changeset

39 
eqns = merge_rules (eqns1, eqns2)}; 
22846  40 
); 
12557  41 

42 

43 
fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^ 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31998
diff
changeset

44 
Display.string_of_thm_without_context thm); 
11537  45 

33244  46 
fun add_node x g = Graph.new_node (x, ()) g handle Graph.DUP _ => g; 
14162
f05f299512e9
Fixed problem with "code ind" attribute that caused code generator to
berghofe
parents:
13105
diff
changeset

47 

22271  48 
fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy => 
16645  49 
let 
50 
val {intros, graph, eqns} = CodegenData.get thy; 

51 
fun thyname_of s = (case optmod of 

27398
768da1da59d6
simplified retrieval of theory names of consts and types
haftmann
parents:
26975
diff
changeset

52 
NONE => Codegen.thyname_of_const thy s  SOME s => s); 
22271  53 
in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of 
54 
SOME (Const ("op =", _), [t, _]) => (case head_of t of 

15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

55 
Const (s, _) => 
18728  56 
CodegenData.put {intros = intros, graph = graph, 
22642  57 
eqns = eqns > Symtab.map_default (s, []) 
58 
(AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy 

18728  59 
 _ => (warn thm; thy)) 
22271  60 
 SOME (Const (s, _), _) => 
61 
let 

29287  62 
val cs = fold Term.add_const_names (Thm.prems_of thm) []; 
22271  63 
val rules = Symtab.lookup_list intros s; 
64 
val nparms = (case optnparms of 

65 
SOME k => k 

66 
 NONE => (case rules of 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30190
diff
changeset

67 
[] => (case try (Inductive.the_inductive (ProofContext.init thy)) s of 
22791
992222f3d2eb
Moved function params_of to inductive_package.ML.
berghofe
parents:
22661
diff
changeset

68 
SOME (_, {raw_induct, ...}) => 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30190
diff
changeset

69 
length (Inductive.params_of raw_induct) 
22271  70 
 NONE => 0) 
71 
 xs => snd (snd (snd (split_last xs))))) 

72 
in CodegenData.put 

73 
{intros = intros > 

22642  74 
Symtab.update (s, (AList.update Thm.eq_thm_prop 
75 
(thm, (thyname_of s, nparms)) rules)), 

33338  76 
graph = fold_rev (Graph.add_edge o pair s) cs (fold add_node (s :: cs) graph), 
22271  77 
eqns = eqns} thy 
78 
end 

18728  79 
 _ => (warn thm; thy)) 
20897  80 
end) I); 
12557  81 

82 
fun get_clauses thy s = 

15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

83 
let val {intros, graph, ...} = CodegenData.get thy 
17412  84 
in case Symtab.lookup intros s of 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30190
diff
changeset

85 
NONE => (case try (Inductive.the_inductive (ProofContext.init thy)) s of 
15531  86 
NONE => NONE 
22271  87 
 SOME ({names, ...}, {intrs, raw_induct, ...}) => 
27398
768da1da59d6
simplified retrieval of theory names of consts and types
haftmann
parents:
26975
diff
changeset

88 
SOME (names, Codegen.thyname_of_const thy s, 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30190
diff
changeset

89 
length (Inductive.params_of raw_induct), 
22661
f3ba63a2663e
Removed erroneous application of rev in get_clauses that caused
berghofe
parents:
22642
diff
changeset

90 
preprocess thy intrs)) 
15531  91 
 SOME _ => 
16645  92 
let 
93 
val SOME names = find_first 

22642  94 
(fn xs => member (op =) xs s) (Graph.strong_conn graph); 
95 
val intrs as (_, (thyname, nparms)) :: _ = 

96 
maps (the o Symtab.lookup intros) names; 

97 
in SOME (names, thyname, nparms, preprocess thy (map fst (rev intrs))) end 

14162
f05f299512e9
Fixed problem with "code ind" attribute that caused code generator to
berghofe
parents:
13105
diff
changeset

98 
end; 
12557  99 

100 

11537  101 
(**** check if a term contains only constructor functions ****) 
102 

103 
fun is_constrt thy = 

104 
let 

31784  105 
val cnstrs = flat (maps 
11537  106 
(map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd) 
33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33771
diff
changeset

107 
(Symtab.dest (Datatype_Data.get_all thy))); 
11537  108 
fun check t = (case strip_comb t of 
109 
(Var _, []) => true 

17521  110 
 (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of 
15531  111 
NONE => false 
112 
 SOME i => length ts = i andalso forall check ts) 

11537  113 
 _ => false) 
114 
in check end; 

115 

116 
(**** check if a type is an equality type (i.e. doesn't contain fun) ****) 

117 

118 
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts 

119 
 is_eqT _ = true; 

120 

121 
(**** mode inference ****) 

122 

15204
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

123 
fun string_of_mode (iss, is) = space_implode " > " (map 
15531  124 
(fn NONE => "X" 
125 
 SOME js => enclose "[" "]" (commas (map string_of_int js))) 

126 
(iss @ [SOME is])); 

15204
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

127 

d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

128 
fun print_modes modes = message ("Inferred modes:\n" ^ 
26931  129 
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

130 
(fn (m, rnd) => string_of_mode m ^ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

131 
(if rnd then " (random)" else "")) ms)) modes)); 
15204
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

132 

29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28537
diff
changeset

133 
val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars; 
32952  134 
val terms_vs = distinct (op =) o maps term_vs; 
11537  135 

136 
(** collect all Vars in a term (with duplicates!) **) 

16861  137 
fun term_vTs tm = 
138 
fold_aterms (fn Var ((x, _), T) => cons (x, T)  _ => I) tm []; 

11537  139 

140 
fun get_args _ _ [] = ([], []) 

141 
 get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x) 

142 
(get_args is (i+1) xs); 

143 

144 
fun merge xs [] = xs 

145 
 merge [] ys = ys 

146 
 merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) 

147 
else y::merge (x::xs) ys; 

148 

149 
fun subsets i j = if i <= j then 

150 
let val is = subsets (i+1) j 

151 
in merge (map (fn ks => i::ks) is) is end 

152 
else [[]]; 

153 

12557  154 
fun cprod ([], ys) = [] 
155 
 cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys); 

156 

30190  157 
fun cprods xss = List.foldr (map op :: o cprod) [[]] xss; 
12557  158 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

159 
datatype mode = Mode of ((int list option list * int list) * bool) * int list * mode option list; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

160 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

161 
fun needs_random (Mode ((_, b), _, ms)) = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

162 
b orelse exists (fn NONE => false  SOME m => needs_random m) ms; 
12557  163 

164 
fun modes_of modes t = 

165 
let 

22271  166 
val ks = 1 upto length (binder_types (fastype_of t)); 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

167 
val default = [Mode ((([], ks), false), ks, [])]; 
32952  168 
fun mk_modes name args = Option.map 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

169 
(maps (fn (m as ((iss, is), _)) => 
22271  170 
let 
171 
val (args1, args2) = 

172 
if length args < length iss then 

173 
error ("Too few arguments for inductive predicate " ^ name) 

174 
else chop (length iss) args; 

175 
val k = length args2; 

176 
val prfx = 1 upto k 

177 
in 

178 
if not (is_prefix op = prfx is) then [] else 

179 
let val is' = map (fn i => i  k) (List.drop (is, k)) 

180 
in map (fn x => Mode (m, is', x)) (cprods (map 

181 
(fn (NONE, _) => [NONE] 

33317  182 
 (SOME js, arg) => map SOME (filter 
22271  183 
(fn Mode (_, js', _) => js=js') (modes_of modes arg))) 
184 
(iss ~~ args1))) 

185 
end 

186 
end)) (AList.lookup op = modes name) 

12557  187 

188 
in (case strip_comb t of 

14163
5ffa75ce4919
Improved handling of modes for equality predicate, to avoid illtyped
berghofe
parents:
14162
diff
changeset

189 
(Const ("op =", Type (_, [T, _])), _) => 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

190 
[Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

191 
(if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else []) 
22271  192 
 (Const (name, _), args) => the_default default (mk_modes name args) 
193 
 (Var ((name, _), _), args) => the (mk_modes name args) 

194 
 (Free (name, _), args) => the (mk_modes name args) 

195 
 _ => default) 

12557  196 
end; 
197 

26806  198 
datatype indprem = Prem of term list * term * bool  Sidecond of term; 
12557  199 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

200 
fun missing_vars vs ts = subtract (fn (x, ((y, _), _)) => x = y) vs 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

201 
(fold Term.add_vars ts []); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

202 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

203 
fun monomorphic_vars vs = null (fold (Term.add_tvarsT o snd) vs []); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

204 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

205 
fun mode_ord p = int_ord (pairself (fn (Mode ((_, rnd), _, _), vs) => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

206 
length vs + (if null vs then 0 else 1) + (if rnd then 1 else 0)) p); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

207 

11537  208 
fun select_mode_prem thy modes vs ps = 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

209 
sort (mode_ord o pairself (hd o snd)) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

210 
(filter_out (null o snd) (ps ~~ map 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

211 
(fn Prem (us, t, is_set) => sort mode_ord 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

212 
(List.mapPartial (fn m as Mode (_, is, _) => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

213 
let 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

214 
val (in_ts, out_ts) = get_args is 1 us; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

215 
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

216 
val vTs = maps term_vTs out_ts'; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

217 
val dupTs = map snd (duplicates (op =) vTs) @ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

218 
map_filter (AList.lookup (op =) vTs) vs; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

219 
val missing_vs = missing_vars vs (t :: in_ts @ in_ts') 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

220 
in 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

221 
if forall (is_eqT o fastype_of) in_ts' andalso forall is_eqT dupTs 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

222 
andalso monomorphic_vars missing_vs 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

223 
then SOME (m, missing_vs) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

224 
else NONE 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

225 
end) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

226 
(if is_set then [Mode ((([], []), false), [], [])] 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

227 
else modes_of modes t handle Option => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

228 
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

229 
 Sidecond t => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

230 
let val missing_vs = missing_vars vs [t] 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

231 
in 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

232 
if monomorphic_vars missing_vs 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

233 
then [(Mode ((([], []), false), [], []), missing_vs)] 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

234 
else [] 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

235 
end) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

236 
ps)); 
11537  237 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

238 
fun use_random () = "random_ind" mem !Codegen.mode; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

239 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

240 
fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) = 
11537  241 
let 
32952  242 
val modes' = modes @ map_filter 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

243 
(fn (_, NONE) => NONE  (v, SOME js) => SOME (v, [(([], js), false)])) 
12557  244 
(arg_vs ~~ iss); 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

245 
fun check_mode_prems vs rnd [] = SOME (vs, rnd) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

246 
 check_mode_prems vs rnd ps = (case select_mode_prem thy modes' vs ps of 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

247 
(x, (m, []) :: _) :: _ => check_mode_prems 
33042  248 
(case x of Prem (us, _, _) => union (op =) vs (terms_vs us)  _ => vs) 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

249 
(rnd orelse needs_random m) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

250 
(filter_out (equal x) ps) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

251 
 (_, (_, vs') :: _) :: _ => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

252 
if use_random () then 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

253 
check_mode_prems (union (op =) vs (map (fst o fst) vs')) true ps 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

254 
else NONE 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

255 
 _ => NONE); 
15570  256 
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts)); 
11537  257 
val in_vs = terms_vs in_ts; 
258 
in 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

259 
if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

260 
forall (is_eqT o fastype_of) in_ts' 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

261 
then (case check_mode_prems (union (op =) arg_vs in_vs) rnd ps of 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

262 
NONE => NONE 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

263 
 SOME (vs, rnd') => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

264 
let val missing_vs = missing_vars vs ts 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

265 
in 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

266 
if null missing_vs orelse 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

267 
use_random () andalso monomorphic_vars missing_vs 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

268 
then SOME (rnd' orelse not (null missing_vs)) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

269 
else NONE 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

270 
end) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

271 
else NONE 
11537  272 
end; 
273 

274 
fun check_modes_pred thy arg_vs preds modes (p, ms) = 

17521  275 
let val SOME rs = AList.lookup (op =) preds p 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

276 
in (p, List.mapPartial (fn m as (m', _) => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

277 
let val xs = map (check_mode_clause thy arg_vs modes m) rs 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

278 
in case find_index is_none xs of 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

279 
~1 => SOME (m', exists (fn SOME b => b) xs) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

280 
 i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

281 
p ^ " violates mode " ^ string_of_mode m'); NONE) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

282 
end) ms) 
15204
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

283 
end; 
11537  284 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

285 
fun fixp f (x : (string * ((int list option list * int list) * bool) list) list) = 
11537  286 
let val y = f x 
287 
in if x = y then x else fixp f y end; 

288 

22271  289 
fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes => 
11537  290 
map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes) 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

291 
(map (fn (s, (ks, k)) => (s, map (rpair false) (cprod (cprods (map 
15531  292 
(fn NONE => [NONE] 
22271  293 
 SOME k' => map SOME (subsets 1 k')) ks), 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

294 
subsets 1 k)))) arities); 
11537  295 

296 
(**** code generation ****) 

297 

298 
fun mk_eq (x::xs) = 

299 
let fun mk_eqs _ [] = [] 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

300 
 mk_eqs a (b::cs) = str (a ^ " = " ^ b) :: mk_eqs b cs 
11537  301 
in mk_eqs x xs end; 
302 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

303 
fun mk_tuple xs = Pretty.block (str "(" :: 
32952  304 
flat (separate [str ",", Pretty.brk 1] (map single xs)) @ 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

305 
[str ")"]); 
11537  306 

33244  307 
fun mk_v s (names, vs) = 
308 
(case AList.lookup (op =) vs s of 

309 
NONE => (s, (names, (s, [s])::vs)) 

310 
 SOME xs => 

311 
let val s' = Name.variant names s 

312 
in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end); 

11537  313 

33244  314 
fun distinct_v (Var ((s, 0), T)) nvs = 
315 
let val (s', nvs') = mk_v s nvs 

316 
in (Var ((s', 0), T), nvs') end 

317 
 distinct_v (t $ u) nvs = 

11537  318 
let 
33244  319 
val (t', nvs') = distinct_v t nvs; 
320 
val (u', nvs'') = distinct_v u nvs'; 

321 
in (t' $ u', nvs'') end 

322 
 distinct_v t nvs = (t, nvs); 

11537  323 

15061
61a52739cd82
Added simple check that allows code generator to produce code containing
berghofe
parents:
15031
diff
changeset

324 
fun is_exhaustive (Var _) = true 
61a52739cd82
Added simple check that allows code generator to produce code containing
berghofe
parents:
15031
diff
changeset

325 
 is_exhaustive (Const ("Pair", _) $ t $ u) = 
61a52739cd82
Added simple check that allows code generator to produce code containing
berghofe
parents:
15031
diff
changeset

326 
is_exhaustive t andalso is_exhaustive u 
61a52739cd82
Added simple check that allows code generator to produce code containing
berghofe
parents:
15031
diff
changeset

327 
 is_exhaustive _ = false; 
61a52739cd82
Added simple check that allows code generator to produce code containing
berghofe
parents:
15031
diff
changeset

328 

61a52739cd82
Added simple check that allows code generator to produce code containing
berghofe
parents:
15031
diff
changeset

329 
fun compile_match nvs eq_ps out_ps success_p can_fail = 
32952  330 
let val eqs = flat (separate [str " andalso", Pretty.brk 1] 
331 
(map single (maps (mk_eq o snd) nvs @ eq_ps))); 

11537  332 
in 
333 
Pretty.block 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

334 
([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

335 
(Pretty.block ((if eqs=[] then [] else str "if " :: 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

336 
[Pretty.block eqs, Pretty.brk 1, str "then "]) @ 
11537  337 
(success_p :: 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

338 
(if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) :: 
15061
61a52739cd82
Added simple check that allows code generator to produce code containing
berghofe
parents:
15031
diff
changeset

339 
(if can_fail then 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

340 
[Pretty.brk 1, str " _ => DSeq.empty)"] 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

341 
else [str ")"]))) 
11537  342 
end; 
343 

17144  344 
fun modename module s (iss, is) gr = 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

345 
let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr) 
17144  346 
else mk_const_id module s gr 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

347 
in (space_implode "__" 
17144  348 
(mk_qual_id module id :: 
32952  349 
map (space_implode "_" o map string_of_int) (map_filter I iss @ [is])), gr') 
17144  350 
end; 
11537  351 

22271  352 
fun mk_funcomp brack s k p = (if brack then parens else I) 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

353 
(Pretty.block [Pretty.block ((if k = 0 then [] else [str "("]) @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

354 
separate (Pretty.brk 1) (str s :: replicate k (str "> ???")) @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

355 
(if k = 0 then [] else [str ")"])), Pretty.brk 1, p]); 
22271  356 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

357 
fun compile_expr thy defs dep module brack modes (NONE, t) gr = 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

358 
apfst single (invoke_codegen thy defs dep module brack t gr) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

359 
 compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr = 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

360 
([str name], gr) 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

361 
 compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr = 
22271  362 
(case strip_comb t of 
363 
(Const (name, _), args) => 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

364 
if name = @{const_name "op ="} orelse AList.defined op = modes name then 
22271  365 
let 
366 
val (args1, args2) = chop (length ms) args; 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

367 
val ((ps, mode_id), gr') = gr > fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

368 
(compile_expr thy defs dep module true modes) (ms ~~ args1) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

369 
>> modename module name mode; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

370 
val (ps', gr'') = (case mode of 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

371 
([], []) => ([str "()"], gr') 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

372 
 _ => fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

373 
(invoke_codegen thy defs dep module true) args2 gr') 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

374 
in ((if brack andalso not (null ps andalso null ps') then 
22271  375 
single o parens o Pretty.block else I) 
32952  376 
(flat (separate [Pretty.brk 1] 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

377 
([str mode_id] :: ps @ map single ps'))), gr') 
22271  378 
end 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

379 
else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

380 
(invoke_codegen thy defs dep module true t gr) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

381 
 _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

382 
(invoke_codegen thy defs dep module true t gr)); 
12557  383 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

384 
fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr = 
11537  385 
let 
32952  386 
val modes' = modes @ map_filter 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

387 
(fn (_, NONE) => NONE  (v, SOME js) => SOME (v, [(([], js), false)])) 
12557  388 
(arg_vs ~~ iss); 
389 

33244  390 
fun check_constrt t (names, eqs) = 
391 
if is_constrt thy t then (t, (names, eqs)) 

392 
else 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19861
diff
changeset

393 
let val s = Name.variant names "x"; 
33244  394 
in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end; 
11537  395 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

396 
fun compile_eq (s, t) gr = 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

397 
apfst (Pretty.block o cons (str (s ^ " = ")) o single) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

398 
(invoke_codegen thy defs dep module false t gr); 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

399 

12557  400 
val (in_ts, out_ts) = get_args is 1 ts; 
33244  401 
val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []); 
11537  402 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

403 
fun compile_prems out_ts' vs names [] gr = 
11537  404 
let 
33244  405 
val (out_ps, gr2) = 
406 
fold_map (invoke_codegen thy defs dep module false) out_ts gr; 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

407 
val (eq_ps, gr3) = fold_map compile_eq eqs gr2; 
33244  408 
val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []); 
409 
val (out_ts''', nvs) = 

410 
fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs); 

411 
val (out_ps', gr4) = 

412 
fold_map (invoke_codegen thy defs dep module false) out_ts''' gr3; 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

413 
val (eq_ps', gr5) = fold_map compile_eq eqs' gr4; 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

414 
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts')); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

415 
val missing_vs = missing_vars vs' out_ts; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

416 
val final_p = Pretty.block 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

417 
[str "DSeq.single", Pretty.brk 1, mk_tuple out_ps] 
11537  418 
in 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

419 
if null missing_vs then 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

420 
(compile_match (snd nvs) (eq_ps @ eq_ps') out_ps' 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

421 
final_p (exists (not o is_exhaustive) out_ts'''), gr5) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

422 
else 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

423 
let 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

424 
val (pat_p, gr6) = invoke_codegen thy defs dep module true 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

425 
(HOLogic.mk_tuple (map Var missing_vs)) gr5; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

426 
val gen_p = mk_gen gr6 module true [] "" 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

427 
(HOLogic.mk_tupleT (map snd missing_vs)) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

428 
in 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

429 
(compile_match (snd nvs) eq_ps' out_ps' 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

430 
(Pretty.block [str "DSeq.generator ", gen_p, 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

431 
str " :>", Pretty.brk 1, 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

432 
compile_match [] eq_ps [pat_p] final_p false]) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

433 
(exists (not o is_exhaustive) out_ts'''), 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

434 
gr6) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

435 
end 
11537  436 
end 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

437 
 compile_prems out_ts vs names ps gr = 
11537  438 
let 
31852
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31784
diff
changeset

439 
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); 
33244  440 
val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []); 
441 
val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs); 

442 
val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr; 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

443 
val (eq_ps, gr1) = fold_map compile_eq eqs gr0; 
11537  444 
in 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

445 
(case hd (select_mode_prem thy modes' vs' ps) of 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

446 
(p as Prem (us, t, is_set), (mode as Mode (_, js, _), []) :: _) => 
11537  447 
let 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

448 
val ps' = filter_out (equal p) ps; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

449 
val (in_ts, out_ts''') = get_args js 1 us; 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

450 
val (in_ps, gr2) = fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

451 
(invoke_codegen thy defs dep module true) in_ts gr1; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

452 
val (ps, gr3) = 
26806  453 
if not is_set then 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

454 
apfst (fn ps => ps @ 
24129
591394d9ee66
 Added cycle test to function mk_ind_def to avoid nontermination
berghofe
parents:
23761
diff
changeset

455 
(if null in_ps then [] else [Pretty.brk 1]) @ 
22271  456 
separate (Pretty.brk 1) in_ps) 
457 
(compile_expr thy defs dep module false modes 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

458 
(SOME mode, t) gr2) 
26806  459 
else 
31852
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31784
diff
changeset

460 
apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p, 
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31784
diff
changeset

461 
str "of", str "Set", str "xs", str "=>", str "xs)"]) 
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31784
diff
changeset

462 
(*this is a very strong assumption about the generated code!*) 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

463 
(invoke_codegen thy defs dep module true t gr2); 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

464 
val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3; 
11537  465 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

466 
(compile_match (snd nvs) eq_ps out_ps 
12557  467 
(Pretty.block (ps @ 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

468 
[str " :>", Pretty.brk 1, rest])) 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

469 
(exists (not o is_exhaustive) out_ts''), gr4) 
11537  470 
end 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

471 
 (p as Sidecond t, [(_, [])]) => 
11537  472 
let 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

473 
val ps' = filter_out (equal p) ps; 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

474 
val (side_p, gr2) = invoke_codegen thy defs dep module true t gr1; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

475 
val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2; 
11537  476 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

477 
(compile_match (snd nvs) eq_ps out_ps 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

478 
(Pretty.block [str "?? ", side_p, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

479 
str " :>", Pretty.brk 1, rest]) 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

480 
(exists (not o is_exhaustive) out_ts''), gr3) 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

481 
end 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

482 
 (_, (_, missing_vs) :: _) => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

483 
let 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

484 
val T = HOLogic.mk_tupleT (map snd missing_vs); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

485 
val (_, gr2) = invoke_tycodegen thy defs dep module false T gr1; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

486 
val gen_p = mk_gen gr2 module true [] "" T; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

487 
val (rest, gr3) = compile_prems 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

488 
[HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

489 
in 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

490 
(compile_match (snd nvs) eq_ps out_ps 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

491 
(Pretty.block [str "DSeq.generator", Pretty.brk 1, 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

492 
gen_p, str " :>", Pretty.brk 1, rest]) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

493 
(exists (not o is_exhaustive) out_ts''), gr3) 
11537  494 
end) 
495 
end; 

496 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

497 
val (prem_p, gr') = compile_prems in_ts' arg_vs all_vs' ps gr ; 
11537  498 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

499 
(Pretty.block [str "DSeq.single", Pretty.brk 1, inp, 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

500 
str " :>", Pretty.brk 1, prem_p], gr') 
11537  501 
end; 
502 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

503 
fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr = 
22271  504 
let 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

505 
val xs = map str (Name.variant_list arg_vs 
22271  506 
(map (fn i => "x" ^ string_of_int i) (snd mode))); 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

507 
val ((cl_ps, mode_id), gr') = gr > 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

508 
fold_map (fn cl => compile_clause thy defs 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

509 
dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls >> 
22271  510 
modename module s mode 
11537  511 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

512 
(Pretty.block 
11537  513 
([Pretty.block (separate (Pretty.brk 1) 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

514 
(str (prfx ^ mode_id) :: 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

515 
map str arg_vs @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

516 
(case mode of ([], []) => [str "()"]  _ => xs)) @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

517 
[str " ="]), 
11537  518 
Pretty.brk 1] @ 
32952  519 
flat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and ")) 
11537  520 
end; 
521 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

522 
fun compile_preds thy defs dep module all_vs arg_vs modes preds gr = 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

523 
let val (prs, (gr', _)) = fold_map (fn (s, cls) => 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

524 
fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

525 
dep module prfx' all_vs arg_vs modes s cls mode gr') 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

526 
(((the o AList.lookup (op =) modes) s))) preds (gr, "fun ") 
11537  527 
in 
32952  528 
(space_implode "\n\n" (map string_of (flat prs)) ^ ";\n\n", gr') 
11537  529 
end; 
530 

531 
(**** processing of introduction rules ****) 

532 

12557  533 
exception Modes of 
33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

534 
(string * ((int list option list * int list) * bool) list) list * 
22271  535 
(string * (int option list * int)) list; 
12557  536 

32952  537 
fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip 
17144  538 
(map ((fn (SOME (Modes x), _, _) => x  _ => ([], [])) o get_node gr) 
539 
(Graph.all_preds (fst gr) [dep])))); 

12557  540 

22271  541 
fun print_arities arities = message ("Arities:\n" ^ 
26931  542 
cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ 
12557  543 
space_implode " > " (map 
22271  544 
(fn NONE => "X"  SOME k' => string_of_int k') 
545 
(ks @ [SOME k]))) arities)); 

11537  546 

32957  547 
fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

548 

726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

549 
fun constrain cs [] = [] 
33244  550 
 constrain cs ((s, xs) :: ys) = 
551 
(s, 

552 
case AList.lookup (op =) cs (s : string) of 

553 
NONE => xs 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

554 
 SOME xs' => inter (op = o apfst fst) xs' xs) :: constrain cs ys; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

555 

17144  556 
fun mk_extra_defs thy defs gr dep names module ts = 
33244  557 
fold (fn name => fn gr => 
12557  558 
if name mem names then gr 
33244  559 
else 
560 
(case get_clauses thy name of 

15531  561 
NONE => gr 
22271  562 
 SOME (names, thyname, nparms, intrs) => 
17144  563 
mk_ind_def thy defs gr dep names (if_library thyname module) 
22271  564 
[] (prep_intrs intrs) nparms)) 
33244  565 
(fold Term.add_const_names ts []) gr 
12557  566 

22271  567 
and mk_ind_def thy defs gr dep names module modecs intrs nparms = 
24129
591394d9ee66
 Added cycle test to function mk_ind_def to avoid nontermination
berghofe
parents:
23761
diff
changeset

568 
add_edge_acyclic (hd names, dep) gr handle 
591394d9ee66
 Added cycle test to function mk_ind_def to avoid nontermination
berghofe
parents:
23761
diff
changeset

569 
Graph.CYCLES (xs :: _) => 
591394d9ee66
 Added cycle test to function mk_ind_def to avoid nontermination
berghofe
parents:
23761
diff
changeset

570 
error ("InductiveCodegen: illegal cyclic dependencies:\n" ^ commas xs) 
591394d9ee66
 Added cycle test to function mk_ind_def to avoid nontermination
berghofe
parents:
23761
diff
changeset

571 
 Graph.UNDEF _ => 
11537  572 
let 
22271  573 
val _ $ u = Logic.strip_imp_concl (hd intrs); 
574 
val args = List.take (snd (strip_comb u), nparms); 

32952  575 
val arg_vs = maps term_vs args; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

576 

22271  577 
fun get_nparms s = if s mem names then SOME nparms else 
578 
Option.map #3 (get_clauses thy s); 

11537  579 

26806  580 
fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true) 
581 
 dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq, false) 

22271  582 
 dest_prem (_ $ t) = 
583 
(case strip_comb t of 

26806  584 
(v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t 
22271  585 
 (c as Const (s, _), ts) => (case get_nparms s of 
586 
NONE => Sidecond t 

587 
 SOME k => 

588 
let val (ts1, ts2) = chop k ts 

26806  589 
in Prem (ts2, list_comb (c, ts1), false) end) 
22271  590 
 _ => Sidecond t); 
591 

592 
fun add_clause intr (clauses, arities) = 

11537  593 
let 
22271  594 
val _ $ t = Logic.strip_imp_concl intr; 
595 
val (Const (name, T), ts) = strip_comb t; 

596 
val (ts1, ts2) = chop nparms ts; 

597 
val prems = map dest_prem (Logic.strip_imp_prems intr); 

598 
val (Ts, Us) = chop nparms (binder_types T) 

11537  599 
in 
22271  600 
(AList.update op = (name, these (AList.lookup op = clauses name) @ 
601 
[(ts2, prems)]) clauses, 

602 
AList.update op = (name, (map (fn U => (case strip_type U of 

603 
(Rs as _ :: _, Type ("bool", [])) => SOME (length Rs) 

604 
 _ => NONE)) Ts, 

605 
length Us)) arities) 

11537  606 
end; 
607 

16645  608 
val gr' = mk_extra_defs thy defs 
17144  609 
(add_edge (hd names, dep) 
610 
(new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs; 

22271  611 
val (extra_modes, extra_arities) = lookup_modes gr' (hd names); 
612 
val (clauses, arities) = fold add_clause intrs ([], []); 

15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

613 
val modes = constrain modecs 
22271  614 
(infer_modes thy extra_modes arities arg_vs clauses); 
615 
val _ = print_arities arities; 

11537  616 
val _ = print_modes modes; 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

617 
val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

618 
arg_vs (modes @ extra_modes) clauses gr'; 
11537  619 
in 
17144  620 
(map_node (hd names) 
22271  621 
(K (SOME (Modes (modes, arities)), module, s)) gr'') 
16645  622 
end; 
11537  623 

22271  624 
fun find_mode gr dep s u modes is = (case find_first (fn Mode (_, js, _) => is=js) 
15660  625 
(modes_of modes u handle Option => []) of 
17144  626 
NONE => codegen_error gr dep 
627 
("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is)) 

15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

628 
 mode => mode); 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

629 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

630 
fun mk_ind_call thy defs dep module is_query s T ts names thyname k intrs gr = 
22271  631 
let 
632 
val (ts1, ts2) = chop k ts; 

633 
val u = list_comb (Const (s, T), ts1); 

634 

33244  635 
fun mk_mode (Const ("dummy_pattern", _)) ((ts, mode), i) = ((ts, mode), i + 1) 
636 
 mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1); 

11537  637 

22271  638 
val module' = if_library thyname module; 
639 
val gr1 = mk_extra_defs thy defs 

640 
(mk_ind_def thy defs gr dep names module' 

641 
[] (prep_intrs intrs) k) dep names module' [u]; 

642 
val (modes, _) = lookup_modes gr1 dep; 

33244  643 
val (ts', is) = 
644 
if is_query then fst (fold mk_mode ts2 (([], []), 1)) 

22271  645 
else (ts2, 1 upto length (binder_types T)  k); 
646 
val mode = find_mode gr1 dep s u modes is; 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

647 
val _ = if is_query orelse not (needs_random (the mode)) then () 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

648 
else warning ("Illegal use of random data generators in " ^ s); 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

649 
val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

650 
val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2; 
22271  651 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

652 
(Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @ 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

653 
separate (Pretty.brk 1) in_ps), gr3) 
22271  654 
end; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

655 

726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

656 
fun clause_of_eqn eqn = 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

657 
let 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

658 
val (t, u) = HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of eqn)); 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

659 
val (Const (s, T), ts) = strip_comb t; 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

660 
val (Ts, U) = strip_type T 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

661 
in 
22271  662 
rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop 
663 
(list_comb (Const (s ^ "_aux", Ts @ [U] > HOLogic.boolT), ts @ [u])))) 

15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

664 
end; 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

665 

17144  666 
fun mk_fun thy defs name eqns dep module module' gr = 
667 
case try (get_node gr) name of 

668 
NONE => 

15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

669 
let 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

670 
val clauses = map clause_of_eqn eqns; 
17144  671 
val pname = name ^ "_aux"; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

672 
val arity = length (snd (strip_comb (fst (HOLogic.dest_eq 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

673 
(HOLogic.dest_Trueprop (concl_of (hd eqns))))))); 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

674 
val mode = 1 upto arity; 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

675 
val ((fun_id, mode_id), gr') = gr > 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

676 
mk_const_id module' name >> 
17144  677 
modename module' pname ([], mode); 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

678 
val vars = map (fn i => str ("x" ^ string_of_int i)) mode; 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

679 
val s = string_of (Pretty.block 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

680 
[mk_app false (str ("fun " ^ snd fun_id)) vars, str " =", 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

681 
Pretty.brk 1, str "DSeq.hd", Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

682 
parens (Pretty.block (separate (Pretty.brk 1) (str mode_id :: 
22271  683 
vars)))]) ^ ";\n\n"; 
17144  684 
val gr'' = mk_ind_def thy defs (add_edge (name, dep) 
685 
(new_node (name, (NONE, module', s)) gr')) name [pname] module' 

22271  686 
[(pname, [([], mode)])] clauses 0; 
17144  687 
val (modes, _) = lookup_modes gr'' dep; 
22271  688 
val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop 
689 
(Logic.strip_imp_concl (hd clauses)))) modes mode 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

690 
in (mk_qual_id module fun_id, gr'') end 
17144  691 
 SOME _ => 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

692 
(mk_qual_id module (get_const_id gr name), add_edge (name, dep) gr); 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

693 

23761  694 
(* convert ntuple to nested pairs *) 
695 

696 
fun conv_ntuple fs ts p = 

697 
let 

698 
val k = length fs; 

33063  699 
val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1); 
23761  700 
val xs' = map (fn Bound i => nth xs (k  i)) ts; 
701 
fun conv xs js = 

702 
if js mem fs then 

703 
let 

704 
val (p, xs') = conv xs (1::js); 

705 
val (q, xs'') = conv xs' (2::js) 

706 
in (mk_tuple [p, q], xs'') end 

707 
else (hd xs, tl xs) 

708 
in 

709 
if k > 0 then 

710 
Pretty.block 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

711 
[str "DSeq.map (fn", Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

712 
mk_tuple xs', str " =>", Pretty.brk 1, fst (conv xs []), 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

713 
str ")", Pretty.brk 1, parens p] 
23761  714 
else p 
715 
end; 

716 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

717 
fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of 
23761  718 
(Const ("Collect", _), [u]) => 
32342
3fabf5b5fc83
pathsensitive tuple combinators carry a "p"(ath) prefix; combinators for standard rightfold tuples
haftmann
parents:
32287
diff
changeset

719 
let val (r, Ts, fs) = HOLogic.strip_psplits u 
23761  720 
in case strip_comb r of 
721 
(Const (s, T), ts) => 

722 
(case (get_clauses thy s, get_assoc_code thy (s, T)) of 

723 
(SOME (names, thyname, k, intrs), NONE) => 

724 
let 

725 
val (ts1, ts2) = chop k ts; 

726 
val ts2' = map 

34962
807f6ce0273d
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding deBruin index (closer correspondence to similar strip operations)
haftmann
parents:
33963
diff
changeset

727 
(fn Bound i => Term.dummy_pattern (nth Ts (length Ts  i  1))  t => t) ts2; 
23761  728 
val (ots, its) = List.partition is_Bound ts2; 
729 
val no_loose = forall (fn t => not (loose_bvar (t, 0))) 

730 
in 

731 
if null (duplicates op = ots) andalso 

732 
no_loose ts1 andalso no_loose its 

733 
then 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

734 
let val (call_p, gr') = mk_ind_call thy defs dep module true 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

735 
s T (ts1 @ ts2') names thyname k intrs gr 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

736 
in SOME ((if brack then parens else I) (Pretty.block 
31852
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31784
diff
changeset

737 
[str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(", 
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31784
diff
changeset

738 
conv_ntuple fs ots call_p, str "))"]), 
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31784
diff
changeset

739 
(*this is a very strong assumption about the generated code!*) 
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31784
diff
changeset

740 
gr') 
23761  741 
end 
742 
else NONE 

743 
end 

744 
 _ => NONE) 

745 
 _ => NONE 

746 
end 

22271  747 
 (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

748 
NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of 
22271  749 
(SOME (names, thyname, k, intrs), NONE) => 
750 
if length ts < k then NONE else SOME 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

751 
(let val (call_p, gr') = mk_ind_call thy defs dep module false 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

752 
s T (map Term.no_dummy_patterns ts) names thyname k intrs gr 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

753 
in (mk_funcomp brack "?!" 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

754 
(length (binder_types T)  length ts) (parens call_p), gr') 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

755 
end handle TERM _ => mk_ind_call thy defs dep module true 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

756 
s T ts names thyname k intrs gr ) 
22271  757 
 _ => NONE) 
758 
 SOME eqns => 

759 
let 

22642  760 
val (_, thyname) :: _ = eqns; 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

761 
val (id, gr') = mk_fun thy defs s (preprocess thy (map fst (rev eqns))) 
22271  762 
dep module (if_library thyname module) gr; 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

763 
val (ps, gr'') = fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

764 
(invoke_codegen thy defs dep module true) ts gr'; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

765 
in SOME (mk_app brack (str id) ps, gr'') 
22271  766 
end) 
767 
 _ => NONE); 

11537  768 

12557  769 
val setup = 
18708  770 
add_codegen "inductive" inductive_codegen #> 
33244  771 
Attrib.setup @{binding code_ind} 
772 
(Scan.lift (Scan.option (Args.$$$ "target"  Args.colon  Args.name)  

773 
Scan.option (Args.$$$ "params"  Args.colon  OuterParse.nat) >> uncurry add)) 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31852
diff
changeset

774 
"introduction rules for executable predicates"; 
11537  775 

33771
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

776 
(**** Quickcheck involving inductive predicates ****) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

777 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

778 
val test_fn : (int * int * int > term list option) Unsynchronized.ref = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

779 
Unsynchronized.ref (fn _ => NONE); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

780 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

781 
fun strip_imp p = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

782 
let val (q, r) = HOLogic.dest_imp p 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

783 
in strip_imp r >> cons q end 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

784 
handle TERM _ => ([], p); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

785 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

786 
fun deepen bound f i = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

787 
if i > bound then NONE 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

788 
else (case f i of 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

789 
NONE => deepen bound f (i + 1) 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

790 
 SOME x => SOME x); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

791 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

792 
val depth_bound_value = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

793 
Config.declare false "ind_quickcheck_depth" (Config.Int 10); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

794 
val depth_bound = Config.int depth_bound_value; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

795 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

796 
val depth_start_value = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

797 
Config.declare false "ind_quickcheck_depth_start" (Config.Int 1); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

798 
val depth_start = Config.int depth_start_value; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

799 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

800 
val random_values_value = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

801 
Config.declare false "ind_quickcheck_random" (Config.Int 5); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

802 
val random_values = Config.int random_values_value; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

803 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

804 
val size_offset_value = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

805 
Config.declare false "ind_quickcheck_size_offset" (Config.Int 0); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

806 
val size_offset = Config.int size_offset_value; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

807 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

808 
fun test_term ctxt t = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

809 
let 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

810 
val thy = ProofContext.theory_of ctxt; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

811 
val (xs, p) = strip_abs t; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

812 
val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

813 
val args = map Free args'; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

814 
val (ps, q) = strip_imp p; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

815 
val Ts = map snd xs; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

816 
val T = Ts > HOLogic.boolT; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

817 
val rl = Logic.list_implies 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

818 
(map (HOLogic.mk_Trueprop o curry subst_bounds (rev args)) ps @ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

819 
[HOLogic.mk_Trueprop (HOLogic.mk_not (subst_bounds (rev args, q)))], 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

820 
HOLogic.mk_Trueprop (list_comb (Free ("quickcheckp", T), args))); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

821 
val (_, thy') = Inductive.add_inductive_global 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

822 
{quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false, 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

823 
no_elim=true, no_ind=false, skip_mono=false, fork_mono=false} 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

824 
[((Binding.name "quickcheckp", T), NoSyn)] [] 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

825 
[(Attrib.empty_binding, rl)] [] (Theory.copy thy); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

826 
val pred = HOLogic.mk_Trueprop (list_comb 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

827 
(Const (Sign.intern_const thy' "quickcheckp", T), 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

828 
map Term.dummy_pattern Ts)); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

829 
val (code, gr) = setmp_CRITICAL mode ["term_of", "test", "random_ind"] 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

830 
(generate_code_i thy' [] "Generated") [("testf", pred)]; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

831 
val s = "structure TestTerm =\nstruct\n\n" ^ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

832 
cat_lines (map snd code) ^ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

833 
"\nopen Generated;\n\n" ^ string_of 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

834 
(Pretty.block [str "val () = InductiveCodegen.test_fn :=", 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

835 
Pretty.brk 1, str "(fn p =>", Pretty.brk 1, 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

836 
str "case Seq.pull (testf p) of", Pretty.brk 1, 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

837 
str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"], 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

838 
str " =>", Pretty.brk 1, str "SOME ", 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

839 
Pretty.block (str "[" :: 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

840 
Pretty.commas (map (fn (s, T) => Pretty.block 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

841 
[mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

842 
[str "]"]), Pretty.brk 1, 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

843 
str " NONE => NONE);"]) ^ 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

844 
"\n\nend;\n"; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

845 
val _ = ML_Context.eval_in (SOME ctxt) false Position.none s; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

846 
val values = Config.get ctxt random_values; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

847 
val bound = Config.get ctxt depth_bound; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

848 
val start = Config.get ctxt depth_start; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

849 
val offset = Config.get ctxt size_offset; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

850 
val test_fn' = !test_fn; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

851 
fun test k = deepen bound (fn i => 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

852 
(priority ("Search depth: " ^ string_of_int i); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

853 
test_fn' (i, values, k+offset))) start; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

854 
in test end; 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

855 

17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

856 
val quickcheck_setup = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

857 
Attrib.register_config depth_bound_value #> 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

858 
Attrib.register_config depth_start_value #> 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

859 
Attrib.register_config random_values_value #> 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

860 
Attrib.register_config size_offset_value #> 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

861 
Quickcheck.add_generator ("SML_inductive", test_term); 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

862 

11537  863 
end; 