1 (* Title: HOL/Tools/list_code.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Code generation for list literals. |
|
5 *) |
|
6 |
|
7 signature LIST_CODE = |
|
8 sig |
|
9 val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option |
|
10 val default_list: int * string |
|
11 -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T) |
|
12 -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T |
|
13 val add_literal_list: string -> theory -> theory |
|
14 end; |
|
15 |
|
16 structure List_Code : LIST_CODE = |
|
17 struct |
|
18 |
|
19 open Basic_Code_Thingol; |
|
20 |
|
21 fun implode_list nil' cons' t = |
|
22 let |
|
23 fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) = |
|
24 if c = cons' |
|
25 then SOME (t1, t2) |
|
26 else NONE |
|
27 | dest_cons _ = NONE; |
|
28 val (ts, t') = Code_Thingol.unfoldr dest_cons t; |
|
29 in case t' |
|
30 of IConst { name = c, ... } => if c = nil' then SOME ts else NONE |
|
31 | _ => NONE |
|
32 end; |
|
33 |
|
34 fun default_list (target_fxy, target_cons) pr fxy t1 t2 = |
|
35 Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy ( |
|
36 pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1, |
|
37 Code_Printer.str target_cons, |
|
38 pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2 |
|
39 ); |
|
40 |
|
41 fun add_literal_list target = |
|
42 let |
|
43 fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] = |
|
44 case Option.map (cons t1) (implode_list nil' cons' t2) |
|
45 of SOME ts => |
|
46 Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts) |
|
47 | NONE => |
|
48 default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; |
|
49 in Code_Target.add_const_syntax target @{const_name Cons} |
|
50 (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))) |
|
51 end |
|
52 |
|
53 end; |
|