author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37677  c5a8b612e571 
child 38329  16bb1e60204b 
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 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35021
diff
changeset

11 
val test_term: 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35021
diff
changeset

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

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

37390
8781d80026fc
moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents:
37198
diff
changeset

17 
structure Inductive_Codegen : INDUCTIVE_CODEGEN = 
11537  18 
struct 
19 

20 
open Codegen; 

21 

12557  22 
(**** theory data ****) 
23 

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

24 
fun merge_rules tabs = 
22642  25 
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

26 

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

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

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

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

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

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

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

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

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

43 

37390
8781d80026fc
moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents:
37198
diff
changeset

44 
fun warn thm = warning ("Inductive_Codegen: 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

45 
Display.string_of_thm_without_context thm); 
11537  46 

33244  47 
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

48 

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

52 
fun thyname_of s = (case optmod of 

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

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

57 
Const (s, _) => 

58 
CodegenData.put {intros = intros, graph = graph, 

59 
eqns = eqns > Symtab.map_default (s, []) 

60 
(AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy 

61 
 _ => (warn thm; thy)) 

22271  62 
 SOME (Const (s, _), _) => 
63 
let 

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

67 
SOME k => k 

68 
 NONE => (case rules of 

36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36001
diff
changeset

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

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

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

74 
in CodegenData.put 

75 
{intros = intros > 

22642  76 
Symtab.update (s, (AList.update Thm.eq_thm_prop 
77 
(thm, (thyname_of s, nparms)) rules)), 

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

18728  81 
 _ => (warn thm; thy)) 
20897  82 
end) I); 
12557  83 

84 
fun get_clauses thy s = 

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

85 
let val {intros, graph, ...} = CodegenData.get thy 
17412  86 
in case Symtab.lookup intros s of 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36001
diff
changeset

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

90 
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

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

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

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

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

99 
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

100 
end; 
12557  101 

102 

11537  103 
(**** check if a term contains only constructor functions ****) 
104 

105 
fun is_constrt thy = 

106 
let 

31784  107 
val cnstrs = flat (maps 
11537  108 
(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

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

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

11537  115 
 _ => false) 
116 
in check end; 

117 

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

119 

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

121 
 is_eqT _ = true; 

122 

123 
(**** mode inference ****) 

124 

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

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

128 
(iss @ [SOME is])); 

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

129 

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

130 
fun print_modes modes = message ("Inferred modes:\n" ^ 
26931  131 
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

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

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

134 

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

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

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

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

11537  141 

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

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

143 
 get_args is i (x::xs) = (if member (op =) is i then apfst else apsnd) (cons x) 
11537  144 
(get_args is (i+1) xs); 
145 

146 
fun merge xs [] = xs 

147 
 merge [] ys = ys 

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

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

150 

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

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

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

154 
else [[]]; 

155 

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

158 

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

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

161 
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

162 

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

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

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

166 
fun modes_of modes t = 

167 
let 

22271  168 
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

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

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

174 
if length args < length iss then 

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

176 
else chop (length iss) args; 

177 
val k = length args2; 

178 
val prfx = 1 upto k 

179 
in 

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

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

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

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

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

187 
end 

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

12557  189 

190 
in (case strip_comb t of 

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

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

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

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

197 
 _ => default) 

12557  198 
end; 
199 

26806  200 
datatype indprem = Prem of term list * term * bool  Sidecond of term; 
12557  201 

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

202 
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

203 
(fold Term.add_vars ts []); 
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 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

206 

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

207 
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

208 
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

209 

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

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

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

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

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

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

216 
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

217 
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

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

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

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

221 
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

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

223 
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

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

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

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

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

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

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

230 
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

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

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

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

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

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

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

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

238 
ps)); 
11537  239 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

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

241 

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

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

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

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

248 
 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

249 
(x, (m, []) :: _) :: _ => check_mode_prems 
33042  250 
(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

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

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

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

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

255 
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

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

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

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

261 
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

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

263 
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

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

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

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

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

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

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

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

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

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

273 
else NONE 
11537  274 
end; 
275 

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

17521  277 
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

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

279 
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

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

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

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

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

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

285 
end; 
11537  286 

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

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

290 

22271  291 
fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes => 
11537  292 
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

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

296 
subsets 1 k)))) arities); 
11537  297 

298 
(**** code generation ****) 

299 

300 
fun mk_eq (x::xs) = 

301 
let fun mk_eqs _ [] = [] 

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

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

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

305 
fun mk_tuple xs = Pretty.block (str "(" :: 
32952  306 
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

307 
[str ")"]); 
11537  308 

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

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

312 
 SOME xs => 

313 
let val s' = Name.variant names s 

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

11537  315 

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

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

319 
 distinct_v (t $ u) nvs = 

11537  320 
let 
33244  321 
val (t', nvs') = distinct_v t nvs; 
322 
val (u', nvs'') = distinct_v u nvs'; 

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

324 
 distinct_v t nvs = (t, nvs); 

11537  325 

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

326 
fun is_exhaustive (Var _) = true 
37390
8781d80026fc
moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents:
37198
diff
changeset

327 
 is_exhaustive (Const (@{const_name Pair}, _) $ t $ u) = 
15061
61a52739cd82
Added simple check that allows code generator to produce code containing
berghofe
parents:
15031
diff
changeset

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

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

330 

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

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

11537  334 
in 
335 
Pretty.block 

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

336 
([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @ 
37527  337 
(Pretty.block ((if null eqs then [] else str "if " :: 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

338 
[Pretty.block eqs, Pretty.brk 1, str "then "]) @ 
11537  339 
(success_p :: 
37527  340 
(if null 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

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

342 
[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

343 
else [str ")"]))) 
11537  344 
end; 
345 

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

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

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

22271  354 
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

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

356 
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

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

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

359 
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

360 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

381 
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

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

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

384 
(invoke_codegen thy defs dep module true t gr)); 
12557  385 

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

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

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

33244  392 
fun check_constrt t (names, eqs) = 
393 
if is_constrt thy t then (t, (names, eqs)) 

394 
else 

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

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

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

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

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

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

401 

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

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

405 
fun compile_prems out_ts' vs names [] gr = 
11537  406 
let 
33244  407 
val (out_ps, gr2) = 
408 
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

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

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

413 
val (out_ps', gr4) = 

414 
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

415 
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

416 
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

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

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

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

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

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

423 
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

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

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

426 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

444 
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

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

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

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

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

451 
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

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

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

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

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

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

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

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

462 
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

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

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

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

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

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

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

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

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

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

476 
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

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

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

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

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

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

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

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

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

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

487 
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

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

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

490 
[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

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

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

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

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

495 
(exists (not o is_exhaustive) out_ts''), gr3) 
11537  496 
end) 
497 
end; 

498 

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

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

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

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

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

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

507 
val xs = map str (Name.variant_list arg_vs 
22271  508 
(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

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

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

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

514 
(Pretty.block 
11537  515 
([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

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

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

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

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

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

524 
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

525 
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

526 
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

527 
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

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

533 
(**** processing of introduction rules ****) 

534 

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

536 
(string * ((int list option list * int list) * bool) list) list * 
22271  537 
(string * (int option list * int)) list; 
12557  538 

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

12557  542 

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

11537  548 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34962
diff
changeset

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

550 

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

551 
fun constrain cs [] = [] 
33244  552 
 constrain cs ((s, xs) :: ys) = 
553 
(s, 

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

555 
NONE => xs 

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

556 
 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

557 

17144  558 
fun mk_extra_defs thy defs gr dep names module ts = 
33244  559 
fold (fn name => fn gr => 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

560 
if member (op =) names name then gr 
33244  561 
else 
562 
(case get_clauses thy name of 

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

22271  569 
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

570 
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

571 
Graph.CYCLES (xs :: _) => 
37390
8781d80026fc
moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents:
37198
diff
changeset

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

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

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

578 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

579 
fun get_nparms s = if member (op =) names s then SOME nparms else 
22271  580 
Option.map #3 (get_clauses thy s); 
11537  581 

37677  582 
fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) = 
35364  583 
Prem ([t], Envir.beta_eta_contract u, true) 
584 
 dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) = 

585 
Prem ([t, u], eq, false) 

22271  586 
 dest_prem (_ $ t) = 
587 
(case strip_comb t of 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

588 
(v as Var _, ts) => if member (op =) args v then Prem (ts, v, false) else Sidecond t 
35364  589 
 (c as Const (s, _), ts) => 
590 
(case get_nparms s of 

591 
NONE => Sidecond t 

592 
 SOME k => 

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

594 
in Prem (ts2, list_comb (c, ts1), false) end) 

595 
 _ => Sidecond t); 

22271  596 

597 
fun add_clause intr (clauses, arities) = 

11537  598 
let 
22271  599 
val _ $ t = Logic.strip_imp_concl intr; 
600 
val (Const (name, T), ts) = strip_comb t; 

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

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

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

11537  604 
in 
22271  605 
(AList.update op = (name, these (AList.lookup op = clauses name) @ 
606 
[(ts2, prems)]) clauses, 

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

35364  608 
(Rs as _ :: _, @{typ bool}) => SOME (length Rs) 
22271  609 
 _ => NONE)) Ts, 
610 
length Us)) arities) 

11537  611 
end; 
612 

16645  613 
val gr' = mk_extra_defs thy defs 
17144  614 
(add_edge (hd names, dep) 
615 
(new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs; 

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

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

618 
val modes = constrain modecs 
22271  619 
(infer_modes thy extra_modes arities arg_vs clauses); 
620 
val _ = print_arities arities; 

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

622 
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

623 
arg_vs (modes @ extra_modes) clauses gr'; 
11537  624 
in 
17144  625 
(map_node (hd names) 
22271  626 
(K (SOME (Modes (modes, arities)), module, s)) gr'') 
16645  627 
end; 
11537  628 

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

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

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

634 

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

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

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

639 

35364  640 
fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1) 
33244  641 
 mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1); 
11537  642 

22271  643 
val module' = if_library thyname module; 
644 
val gr1 = mk_extra_defs thy defs 

645 
(mk_ind_def thy defs gr dep names module' 

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

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

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

22271  650 
else (ts2, 1 upto length (binder_types T)  k); 
651 
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

652 
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

653 
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

654 
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

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

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

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

660 

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

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

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

663 
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

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

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

666 
in 
22271  667 
rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop 
668 
(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

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

670 

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

673 
NONE => 

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

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

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

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

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

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

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

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

683 
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

684 
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

685 
[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

686 
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

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

22271  691 
[(pname, [([], mode)])] clauses 0; 
17144  692 
val (modes, _) = lookup_modes gr'' dep; 
22271  693 
val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop 
694 
(Logic.strip_imp_concl (hd clauses)))) modes mode 

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

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

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

698 

23761  699 
(* convert ntuple to nested pairs *) 
700 

701 
fun conv_ntuple fs ts p = 

702 
let 

703 
val k = length fs; 

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

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

707 
if member (op =) fs js then 
23761  708 
let 
709 
val (p, xs') = conv xs (1::js); 

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

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

712 
else (hd xs, tl xs) 

713 
in 

714 
if k > 0 then 

715 
Pretty.block 

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

716 
[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

717 
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

718 
str ")", Pretty.brk 1, parens p] 
23761  719 
else p 
720 
end; 

721 

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

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

724 
let val (r, Ts, fs) = HOLogic.strip_psplits u 
23761  725 
in case strip_comb r of 
726 
(Const (s, T), ts) => 

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

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

729 
let 

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

731 
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

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

735 
in 

736 
if null (duplicates op = ots) andalso 

737 
no_loose ts1 andalso no_loose its 

738 
then 

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

739 
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

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

741 
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

742 
[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

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

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

745 
gr') 
23761  746 
end 
747 
else NONE 

748 
end 

749 
 _ => NONE) 

750 
 _ => NONE 

751 
end 

22271  752 
 (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

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

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

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

757 
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

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

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

760 
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

761 
s T ts names thyname k intrs gr ) 
22271  762 
 _ => NONE) 
763 
 SOME eqns => 

764 
let 

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

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

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

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

770 
in SOME (mk_app brack (str id) ps, gr'') 
22271  771 
end) 
772 
 _ => NONE); 

11537  773 

12557  774 
val setup = 
18708  775 
add_codegen "inductive" inductive_codegen #> 
33244  776 
Attrib.setup @{binding code_ind} 
777 
(Scan.lift (Scan.option (Args.$$$ "target"  Args.colon  Args.name)  

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36692
diff
changeset

778 
Scan.option (Args.$$$ "params"  Args.colon  Parse.nat) >> uncurry add)) 
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31852
diff
changeset

779 
"introduction rules for executable predicates"; 
11537  780 

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

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

782 

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

783 
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

784 
Unsynchronized.ref (fn _ => NONE); 
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 strip_imp p = 
17926df64f0f
Added new counterexample generator SML_inductive for goals involving
berghofe
parents:
33522
diff
changeset

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

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

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

790 

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

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

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

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

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

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

796 

36001  797 
val (depth_bound, setup_depth_bound) = Attrib.config_int "ind_quickcheck_depth" (K 10); 
798 
val (depth_start, setup_depth_start) = Attrib.config_int "ind_quickcheck_depth_start" (K 1); 

799 
val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5); 

800 
val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0); 

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

801 

35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35021
diff
changeset

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

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

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

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

806 
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

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

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

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

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

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

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

813 
[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

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

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

816 
{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

817 
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

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

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

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

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

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

823 
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

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

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

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

827 
"\nopen Generated;\n\n" ^ string_of 
37390
8781d80026fc
moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents:
37198
diff
changeset

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

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

830 
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

831 
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

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

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

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

835 
[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

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

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

838 
"\n\nend;\n"; 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36960
diff
changeset

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

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

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

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

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

844 
val test_fn' = !test_fn; 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35021
diff
changeset

845 
val dummy_report = ([], false) 
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35021
diff
changeset

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

847 
(priority ("Search depth: " ^ string_of_int i); 
35378
95d0e3adf38e
added basic reporting of test cases to quickcheck
bulwahn
parents:
35021
diff
changeset

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

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

850 

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

851 
val quickcheck_setup = 
35997
07bce2802939
use regular Attrib.config instead of lowlevel Config.declare/Attrib.register_config;
wenzelm
parents:
35382
diff
changeset

852 
setup_depth_bound #> 
07bce2802939
use regular Attrib.config instead of lowlevel Config.declare/Attrib.register_config;
wenzelm
parents:
35382
diff
changeset

853 
setup_depth_start #> 
07bce2802939
use regular Attrib.config instead of lowlevel Config.declare/Attrib.register_config;
wenzelm
parents:
35382
diff
changeset

854 
setup_random_values #> 
07bce2802939
use regular Attrib.config instead of lowlevel Config.declare/Attrib.register_config;
wenzelm
parents:
35382
diff
changeset

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

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

857 

11537  858 
end; 