4 Code generator facilities for inductive datatypes. |
4 Code generator facilities for inductive datatypes. |
5 *) |
5 *) |
6 |
6 |
7 signature DATATYPE_CODEGEN = |
7 signature DATATYPE_CODEGEN = |
8 sig |
8 sig |
|
9 val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option |
9 val mk_eq_eqns: theory -> string -> (thm * bool) list |
10 val mk_eq_eqns: theory -> string -> (thm * bool) list |
10 val mk_case_cert: theory -> string -> thm |
11 val mk_case_cert: theory -> string -> thm |
11 val setup: theory -> theory |
12 val setup: theory -> theory |
12 end; |
13 end; |
13 |
14 |
22 |
23 |
23 (* find shortest path to constructor with no recursive arguments *) |
24 (* find shortest path to constructor with no recursive arguments *) |
24 |
25 |
25 fun find_nonempty (descr: DatatypeAux.descr) is i = |
26 fun find_nonempty (descr: DatatypeAux.descr) is i = |
26 let |
27 let |
27 val (_, _, constrs) = valOf (AList.lookup (op =) descr i); |
28 val (_, _, constrs) = the (AList.lookup (op =) descr i); |
28 fun arg_nonempty (_, DatatypeAux.DtRec i) = if i mem is then NONE |
29 fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i |
|
30 then NONE |
29 else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i) |
31 else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i) |
30 | arg_nonempty _ = SOME 0; |
32 | arg_nonempty _ = SOME 0; |
31 fun max xs = Library.foldl |
33 fun max xs = Library.foldl |
32 (fn (NONE, _) => NONE |
34 (fn (NONE, _) => NONE |
33 | (SOME i, SOME j) => SOME (Int.max (i, j)) |
35 | (SOME i, SOME j) => SOME (Int.max (i, j)) |
34 | (_, NONE) => NONE) (SOME 0, xs); |
36 | (_, NONE) => NONE) (SOME 0, xs); |
35 val xs = sort (int_ord o pairself snd) |
37 val xs = sort (int_ord o pairself snd) |
36 (List.mapPartial (fn (s, dts) => Option.map (pair s) |
38 (map_filter (fn (s, dts) => Option.map (pair s) |
37 (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs) |
39 (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs) |
38 in case xs of [] => NONE | x :: _ => SOME x end; |
40 in case xs of [] => NONE | x :: _ => SOME x end; |
|
41 |
|
42 fun find_shortest_path descr i = find_nonempty descr [i] i; |
39 |
43 |
40 fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr = |
44 fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr = |
41 let |
45 let |
42 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; |
46 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; |
43 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
47 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
107 val tvs = map DatatypeAux.dest_DtTFree dts; |
111 val tvs = map DatatypeAux.dest_DtTFree dts; |
108 val Us = map (DatatypeAux.typ_of_dtyp descr sorts) dts; |
112 val Us = map (DatatypeAux.typ_of_dtyp descr sorts) dts; |
109 val T = Type (tname, Us); |
113 val T = Type (tname, Us); |
110 val (cs1, cs2) = |
114 val (cs1, cs2) = |
111 List.partition (exists DatatypeAux.is_rec_type o snd) cs; |
115 List.partition (exists DatatypeAux.is_rec_type o snd) cs; |
112 val SOME (cname, _) = find_nonempty descr [i] i; |
116 val SOME (cname, _) = find_shortest_path descr i; |
113 |
117 |
114 fun mk_delay p = Pretty.block |
118 fun mk_delay p = Pretty.block |
115 [str "fn () =>", Pretty.brk 1, p]; |
119 [str "fn () =>", Pretty.brk 1, p]; |
116 |
120 |
117 fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"]; |
121 fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"]; |