author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29287  5b0bfd63b5da 
child 31723  f5cafe803b55 
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 
18708  10 
val setup : theory > theory 
11537  11 
end; 
12 

13 
structure InductiveCodegen : INDUCTIVE_CODEGEN = 

14 
struct 

15 

16 
open Codegen; 

17 

12557  18 
(**** theory data ****) 
19 

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

20 
fun merge_rules tabs = 
22642  21 
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

22 

16424  23 
structure CodegenData = TheoryDataFun 
22846  24 
( 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

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

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

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

30 
{intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty}; 
12557  31 
val copy = I; 
16424  32 
val extend = I; 
33 
fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1}, 

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

34 
{intros=intros2, graph=graph2, eqns=eqns2}) = 
18930
29d39c10822e
replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents:
18928
diff
changeset

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

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

37 
eqns = merge_rules (eqns1, eqns2)}; 
22846  38 
); 
12557  39 

40 

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

26928  42 
Display.string_of_thm thm); 
11537  43 

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

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

45 

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

49 
fun thyname_of s = (case optmod of 

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

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

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

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

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

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

63 
SOME k => k 

64 
 NONE => (case rules of 

65 
[] => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of 

22791
992222f3d2eb
Moved function params_of to inductive_package.ML.
berghofe
parents:
22661
diff
changeset

66 
SOME (_, {raw_induct, ...}) => 
992222f3d2eb
Moved function params_of to inductive_package.ML.
berghofe
parents:
22661
diff
changeset

67 
length (InductivePackage.params_of raw_induct) 
22271  68 
 NONE => 0) 
69 
 xs => snd (snd (snd (split_last xs))))) 

70 
in CodegenData.put 

71 
{intros = intros > 

22642  72 
Symtab.update (s, (AList.update Thm.eq_thm_prop 
73 
(thm, (thyname_of s, nparms)) rules)), 

30190  74 
graph = List.foldr (uncurry (Graph.add_edge o pair s)) 
22271  75 
(Library.foldl add_node (graph, s :: cs)) cs, 
76 
eqns = eqns} thy 

77 
end 

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

81 
fun get_clauses thy s = 

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

82 
let val {intros, graph, ...} = CodegenData.get thy 
17412  83 
in case Symtab.lookup intros s of 
22271  84 
NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of 
15531  85 
NONE => NONE 
22271  86 
 SOME ({names, ...}, {intrs, raw_induct, ...}) => 
27398
768da1da59d6
simplified retrieval of theory names of consts and types
haftmann
parents:
26975
diff
changeset

87 
SOME (names, Codegen.thyname_of_const thy s, 
22791
992222f3d2eb
Moved function params_of to inductive_package.ML.
berghofe
parents:
22661
diff
changeset

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

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

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

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

96 
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

97 
end; 
12557  98 

99 

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

102 
fun is_constrt thy = 

103 
let 

15570  104 
val cnstrs = List.concat (List.concat (map 
11537  105 
(map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd) 
106 
(Symtab.dest (DatatypePackage.get_datatypes thy)))); 

107 
fun check t = (case strip_comb t of 

108 
(Var _, []) => true 

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

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

114 

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

116 

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

118 
 is_eqT _ = true; 

119 

120 
(**** mode inference ****) 

121 

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

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

125 
(iss @ [SOME is])); 

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

126 

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

127 
fun print_modes modes = message ("Inferred modes:\n" ^ 
26931  128 
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map 
15204
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

129 
string_of_mode ms)) modes)); 
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

130 

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

131 
val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars; 
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19025
diff
changeset

132 
val terms_vs = distinct (op =) o List.concat o (map term_vs); 
11537  133 

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

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

11537  137 

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

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

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

141 

142 
fun merge xs [] = xs 

143 
 merge [] ys = ys 

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

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

146 

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

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

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

150 
else [[]]; 

151 

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

154 

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

22271  157 
datatype mode = Mode of (int list option list * int list) * int list * mode option list; 
12557  158 

159 
fun modes_of modes t = 

160 
let 

22271  161 
val ks = 1 upto length (binder_types (fastype_of t)); 
162 
val default = [Mode (([], ks), ks, [])]; 

163 
fun mk_modes name args = Option.map (List.concat o 

164 
map (fn (m as (iss, is)) => 

165 
let 

166 
val (args1, args2) = 

167 
if length args < length iss then 

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

169 
else chop (length iss) args; 

170 
val k = length args2; 

171 
val prfx = 1 upto k 

172 
in 

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

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

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

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

177 
 (SOME js, arg) => map SOME (List.filter 

178 
(fn Mode (_, js', _) => js=js') (modes_of modes arg))) 

179 
(iss ~~ args1))) 

180 
end 

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

12557  182 

183 
in (case strip_comb t of 

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

184 
(Const ("op =", Type (_, [T, _])), _) => 
22271  185 
[Mode (([], [1]), [1], []), Mode (([], [2]), [2], [])] @ 
186 
(if is_eqT T then [Mode (([], [1, 2]), [1, 2], [])] else []) 

187 
 (Const (name, _), args) => the_default default (mk_modes name args) 

188 
 (Var ((name, _), _), args) => the (mk_modes name args) 

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

190 
 _ => default) 

12557  191 
end; 
192 

26806  193 
datatype indprem = Prem of term list * term * bool  Sidecond of term; 
12557  194 

11537  195 
fun select_mode_prem thy modes vs ps = 
19861  196 
find_first (is_some o snd) (ps ~~ map 
26806  197 
(fn Prem (us, t, is_set) => find_first (fn Mode (_, is, _) => 
11537  198 
let 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

199 
val (in_ts, out_ts) = get_args is 1 us; 
15570  200 
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts; 
201 
val vTs = List.concat (map term_vTs out_ts'); 

18964  202 
val dupTs = map snd (duplicates (op =) vTs) @ 
17521  203 
List.mapPartial (AList.lookup (op =) vTs) vs; 
11537  204 
in 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

205 
terms_vs (in_ts @ in_ts') subset vs andalso 
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

206 
forall (is_eqT o fastype_of) in_ts' andalso 
12557  207 
term_vs t subset vs andalso 
11537  208 
forall is_eqT dupTs 
209 
end) 

26806  210 
(if is_set then [Mode (([], []), [], [])] 
211 
else modes_of modes t handle Option => 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset

212 
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) 
22271  213 
 Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], [])) 
15531  214 
else NONE) ps); 
11537  215 

12557  216 
fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) = 
11537  217 
let 
15570  218 
val modes' = modes @ List.mapPartial 
15531  219 
(fn (_, NONE) => NONE  (v, SOME js) => SOME (v, [([], js)])) 
12557  220 
(arg_vs ~~ iss); 
15531  221 
fun check_mode_prems vs [] = SOME vs 
12557  222 
 check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of 
15531  223 
NONE => NONE 
224 
 SOME (x, _) => check_mode_prems 

26806  225 
(case x of Prem (us, _, _) => vs union terms_vs us  _ => vs) 
11537  226 
(filter_out (equal x) ps)); 
15570  227 
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts)); 
11537  228 
val in_vs = terms_vs in_ts; 
229 
val concl_vs = terms_vs ts 

230 
in 

18964  231 
forall is_eqT (map snd (duplicates (op =) (List.concat (map term_vTs in_ts)))) andalso 
15204
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

232 
forall (is_eqT o fastype_of) in_ts' andalso 
11537  233 
(case check_mode_prems (arg_vs union in_vs) ps of 
15531  234 
NONE => false 
235 
 SOME vs => concl_vs subset vs) 

11537  236 
end; 
237 

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

17521  239 
let val SOME rs = AList.lookup (op =) preds p 
15570  240 
in (p, List.filter (fn m => case find_index 
15204
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

241 
(not o check_mode_clause thy arg_vs modes m) rs of 
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

242 
~1 => true 
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

243 
 i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^ 
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

244 
p ^ " violates mode " ^ string_of_mode m); false)) ms) 
d15f85347fcb
 Inserted additional check for equality types in check_mode_clause that
berghofe
parents:
15126
diff
changeset

245 
end; 
11537  246 

22642  247 
fun fixp f (x : (string * (int list option list * int list) list) list) = 
11537  248 
let val y = f x 
249 
in if x = y then x else fixp f y end; 

250 

22271  251 
fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes => 
11537  252 
map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes) 
22271  253 
(map (fn (s, (ks, k)) => (s, cprod (cprods (map 
15531  254 
(fn NONE => [NONE] 
22271  255 
 SOME k' => map SOME (subsets 1 k')) ks), 
256 
subsets 1 k))) arities); 

11537  257 

258 
(**** code generation ****) 

259 

260 
fun mk_eq (x::xs) = 

261 
let fun mk_eqs _ [] = [] 

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

262 
 mk_eqs a (b::cs) = str (a ^ " = " ^ b) :: mk_eqs b cs 
11537  263 
in mk_eqs x xs end; 
264 

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

265 
fun mk_tuple xs = Pretty.block (str "(" :: 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

266 
List.concat (separate [str ",", Pretty.brk 1] (map single xs)) @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

267 
[str ")"]); 
11537  268 

17521  269 
fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of 
15531  270 
NONE => ((names, (s, [s])::vs), s) 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19861
diff
changeset

271 
 SOME xs => let val s' = Name.variant names s in 
17521  272 
((s'::names, AList.update (op =) (s, s'::xs) vs), s') end); 
11537  273 

274 
fun distinct_v (nvs, Var ((s, 0), T)) = 

275 
apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s)) 

276 
 distinct_v (nvs, t $ u) = 

277 
let 

278 
val (nvs', t') = distinct_v (nvs, t); 

279 
val (nvs'', u') = distinct_v (nvs', u); 

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

281 
 distinct_v x = x; 

282 

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

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

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

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

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

287 

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

288 
fun compile_match nvs eq_ps out_ps success_p can_fail = 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

289 
let val eqs = List.concat (separate [str " andalso", Pretty.brk 1] 
15570  290 
(map single (List.concat (map (mk_eq o snd) nvs) @ eq_ps))); 
11537  291 
in 
292 
Pretty.block 

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

293 
([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

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

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

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

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

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

300 
else [str ")"]))) 
11537  301 
end; 
302 

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

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

306 
in (space_implode "__" 
17144  307 
(mk_qual_id module id :: 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

308 
map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])), gr') 
17144  309 
end; 
11537  310 

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

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

313 
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

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

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

316 
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

317 
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

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

319 
([str name], gr) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

333 
in ((if brack andalso not (null ps andalso null ps') then 
22271  334 
single o parens o Pretty.block else I) 
335 
(List.concat (separate [Pretty.brk 1] 

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

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

338 
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

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

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

341 
(invoke_codegen thy defs dep module true t gr)); 
12557  342 

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

343 
fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr = 
11537  344 
let 
15570  345 
val modes' = modes @ List.mapPartial 
15531  346 
(fn (_, NONE) => NONE  (v, SOME js) => SOME (v, [([], js)])) 
12557  347 
(arg_vs ~~ iss); 
348 

11537  349 
fun check_constrt ((names, eqs), t) = 
350 
if is_constrt thy t then ((names, eqs), t) else 

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

351 
let val s = Name.variant names "x"; 
11537  352 
in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end; 
353 

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

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

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

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

357 

12557  358 
val (in_ts, out_ts) = get_args is 1 ts; 
11537  359 
val ((all_vs', eqs), in_ts') = 
30190  360 
Library.foldl_map check_constrt ((all_vs, []), in_ts); 
11537  361 

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

362 
fun compile_prems out_ts' vs names [] gr = 
11537  363 
let 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

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

365 
(invoke_codegen thy defs dep module false) out_ts gr; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

366 
val (eq_ps, gr3) = fold_map compile_eq eqs gr2; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

367 
val ((names', eqs'), out_ts'') = 
30190  368 
Library.foldl_map check_constrt ((names, []), out_ts'); 
369 
val (nvs, out_ts''') = Library.foldl_map distinct_v 

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

370 
((names', map (fn x => (x, [x])) vs), out_ts''); 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

371 
val (out_ps', gr4) = fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

372 
(invoke_codegen thy defs dep module false) (out_ts''') gr3; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

373 
val (eq_ps', gr5) = fold_map compile_eq eqs' gr4; 
11537  374 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

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

376 
(Pretty.block [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps]) 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

377 
(exists (not o is_exhaustive) out_ts'''), gr5) 
11537  378 
end 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

379 
 compile_prems out_ts vs names ps gr = 
11537  380 
let 
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19025
diff
changeset

381 
val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts)); 
22271  382 
val SOME (p, mode as SOME (Mode (_, js, _))) = 
15126
54ae6c6ef3b1
Fixed bug in compile_clause that caused equality constraints
berghofe
parents:
15061
diff
changeset

383 
select_mode_prem thy modes' vs' ps; 
11537  384 
val ps' = filter_out (equal p) ps; 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

385 
val ((names', eqs), out_ts') = 
30190  386 
Library.foldl_map check_constrt ((names, []), out_ts); 
387 
val (nvs, out_ts'') = Library.foldl_map distinct_v 

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

388 
((names', map (fn x => (x, [x])) vs), out_ts'); 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

389 
val (out_ps, gr0) = fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

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

391 
val (eq_ps, gr1) = fold_map compile_eq eqs gr0; 
11537  392 
in 
393 
(case p of 

26806  394 
Prem (us, t, is_set) => 
11537  395 
let 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

396 
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

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

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

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

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

402 
(if null in_ps then [] else [Pretty.brk 1]) @ 
22271  403 
separate (Pretty.brk 1) in_ps) 
404 
(compile_expr thy defs dep module false modes 

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

405 
(mode, t) gr2) 
26806  406 
else 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

407 
apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p]) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

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

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

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

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

414 
(exists (not o is_exhaustive) out_ts''), gr4) 
11537  415 
end 
416 
 Sidecond t => 

417 
let 

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

418 
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

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

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

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

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

424 
(exists (not o is_exhaustive) out_ts''), gr3) 
11537  425 
end) 
426 
end; 

427 

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

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

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

431 
str " :>", Pretty.brk 1, prem_p], gr') 
11537  432 
end; 
433 

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

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

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

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

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

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

443 
(Pretty.block 
11537  444 
([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

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

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

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

448 
[str " ="]), 
11537  449 
Pretty.brk 1] @ 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

450 
List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and ")) 
11537  451 
end; 
452 

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

453 
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

454 
let val (prs, (gr', _)) = fold_map (fn (s, cls) => 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

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

456 
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

457 
(((the o AList.lookup (op =) modes) s))) preds (gr, "fun ") 
11537  458 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

459 
(space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n", gr') 
11537  460 
end; 
461 

462 
(**** processing of introduction rules ****) 

463 

12557  464 
exception Modes of 
465 
(string * (int list option list * int list) list) list * 

22271  466 
(string * (int option list * int)) list; 
12557  467 

17144  468 
fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip 
469 
(map ((fn (SOME (Modes x), _, _) => x  _ => ([], [])) o get_node gr) 

470 
(Graph.all_preds (fst gr) [dep])))); 

12557  471 

22271  472 
fun print_arities arities = message ("Arities:\n" ^ 
26931  473 
cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ 
12557  474 
space_implode " > " (map 
22271  475 
(fn NONE => "X"  SOME k' => string_of_int k') 
476 
(ks @ [SOME k]))) arities)); 

11537  477 

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

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

479 

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

480 
fun constrain cs [] = [] 
22642  481 
 constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of 
15531  482 
NONE => xs 
483 
 SOME xs' => xs inter xs') :: constrain cs ys; 

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

484 

17144  485 
fun mk_extra_defs thy defs gr dep names module ts = 
15570  486 
Library.foldl (fn (gr, name) => 
12557  487 
if name mem names then gr 
488 
else (case get_clauses thy name of 

15531  489 
NONE => gr 
22271  490 
 SOME (names, thyname, nparms, intrs) => 
17144  491 
mk_ind_def thy defs gr dep names (if_library thyname module) 
22271  492 
[] (prep_intrs intrs) nparms)) 
29287  493 
(gr, fold Term.add_const_names ts []) 
12557  494 

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

496 
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

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

498 
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

499 
 Graph.UNDEF _ => 
11537  500 
let 
22271  501 
val _ $ u = Logic.strip_imp_concl (hd intrs); 
502 
val args = List.take (snd (strip_comb u), nparms); 

15570  503 
val arg_vs = List.concat (map term_vs args); 
15031
726dc9146bb1
 Added support for conditional equations whose premises involve
berghofe
parents:
14981
diff
changeset

504 

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

11537  507 

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

22271  510 
 dest_prem (_ $ t) = 
511 
(case strip_comb t of 

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

515 
 SOME k => 

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

26806  517 
in Prem (ts2, list_comb (c, ts1), false) end) 
22271  518 
 _ => Sidecond t); 
519 

520 
fun add_clause intr (clauses, arities) = 

11537  521 
let 
22271  522 
val _ $ t = Logic.strip_imp_concl intr; 
523 
val (Const (name, T), ts) = strip_comb t; 

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

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

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

11537  527 
in 
22271  528 
(AList.update op = (name, these (AList.lookup op = clauses name) @ 
529 
[(ts2, prems)]) clauses, 

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

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

532 
 _ => NONE)) Ts, 

533 
length Us)) arities) 

11537  534 
end; 
535 

16645  536 
val gr' = mk_extra_defs thy defs 
17144  537 
(add_edge (hd names, dep) 
538 
(new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs; 

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

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

541 
val modes = constrain modecs 
22271  542 
(infer_modes thy extra_modes arities arg_vs clauses); 
543 
val _ = print_arities arities; 

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

545 
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

546 
arg_vs (modes @ extra_modes) clauses gr'; 
11537  547 
in 
17144  548 
(map_node (hd names) 
22271  549 
(K (SOME (Modes (modes, arities)), module, s)) gr'') 
16645  550 
end; 
11537  551 

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

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

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

557 

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

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

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

562 

563 
fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) = 

564 
((ts, mode), i+1) 

565 
 mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1); 

11537  566 

22271  567 
val module' = if_library thyname module; 
568 
val gr1 = mk_extra_defs thy defs 

569 
(mk_ind_def thy defs gr dep names module' 

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

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

572 
val (ts', is) = if is_query then 

573 
fst (Library.foldl mk_mode ((([], []), 1), ts2)) 

574 
else (ts2, 1 upto length (binder_types T)  k); 

575 
val mode = find_mode gr1 dep s u modes is; 

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

576 
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

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

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

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

582 

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

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

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

585 
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

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

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

588 
in 
22271  589 
rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop 
590 
(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

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

592 

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

595 
NONE => 

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

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

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

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

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

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

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

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

605 
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

606 
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

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

608 
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

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

22271  613 
[(pname, [([], mode)])] clauses 0; 
17144  614 
val (modes, _) = lookup_modes gr'' dep; 
22271  615 
val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop 
616 
(Logic.strip_imp_concl (hd clauses)))) modes mode 

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

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

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

620 

23761  621 
(* convert ntuple to nested pairs *) 
622 

623 
fun conv_ntuple fs ts p = 

624 
let 

625 
val k = length fs; 

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

626 
val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k); 
23761  627 
val xs' = map (fn Bound i => nth xs (k  i)) ts; 
628 
fun conv xs js = 

629 
if js mem fs then 

630 
let 

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

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

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

634 
else (hd xs, tl xs) 

635 
in 

636 
if k > 0 then 

637 
Pretty.block 

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

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

639 
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

640 
str ")", Pretty.brk 1, parens p] 
23761  641 
else p 
642 
end; 

643 

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

644 
fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of 
23761  645 
(Const ("Collect", _), [u]) => 
646 
let val (r, Ts, fs) = HOLogic.strip_split u 

647 
in case strip_comb r of 

648 
(Const (s, T), ts) => 

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

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

651 
let 

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

653 
val ts2' = map 

654 
(fn Bound i => Term.dummy_pattern (nth Ts i)  t => t) ts2; 

655 
val (ots, its) = List.partition is_Bound ts2; 

656 
val no_loose = forall (fn t => not (loose_bvar (t, 0))) 

657 
in 

658 
if null (duplicates op = ots) andalso 

659 
no_loose ts1 andalso no_loose its 

660 
then 

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

661 
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

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

663 
in SOME ((if brack then parens else I) (Pretty.block 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26939
diff
changeset

664 
[str "DSeq.list_of", Pretty.brk 1, str "(", 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27809
diff
changeset

665 
conv_ntuple fs ots call_p, str ")"]), gr') 
23761  666 
end 
667 
else NONE 

668 
end 

669 
 _ => NONE) 

670 
 _ => NONE 

671 
end 

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

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

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

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

677 
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

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

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

680 
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

681 
s T ts names thyname k intrs gr ) 
22271  682 
 _ => NONE) 
683 
 SOME eqns => 

684 
let 

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

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

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

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

690 
in SOME (mk_app brack (str id) ps, gr'') 
22271  691 
end) 
692 
 _ => NONE); 

11537  693 

12557  694 
val setup = 
18708  695 
add_codegen "inductive" inductive_codegen #> 
24219  696 
Code.add_attribute ("ind", Scan.option (Args.$$$ "target"  Args.colon  Args.name)  
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27398
diff
changeset

697 
Scan.option (Args.$$$ "params"  Args.colon  OuterParse.nat) >> uncurry add); 
11537  698 

699 
end; 