author | haftmann |
Tue, 31 Aug 2010 13:29:38 +0200 | |
changeset 38923 | 79d7f2b4cf71 |
parent 37881 | 096c8397c989 |
child 48072 | ace701efe203 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/list_code.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
3 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
4 |
Code generation for list literals. |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
5 |
*) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
6 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
7 |
signature LIST_CODE = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
8 |
sig |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
9 |
val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
10 |
val default_list: int * string |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
11 |
-> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
12 |
-> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
13 |
val add_literal_list: string -> theory -> theory |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
14 |
end; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
15 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
16 |
structure List_Code : LIST_CODE = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
17 |
struct |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
18 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
19 |
open Basic_Code_Thingol; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
20 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
21 |
fun implode_list nil' cons' t = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
22 |
let |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
23 |
fun dest_cons (IConst (c, _) `$ t1 `$ t2) = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
24 |
if c = cons' |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
25 |
then SOME (t1, t2) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
26 |
else NONE |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
27 |
| dest_cons _ = NONE; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
28 |
val (ts, t') = Code_Thingol.unfoldr dest_cons t; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
29 |
in case t' |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
30 |
of IConst (c, _) => if c = nil' then SOME ts else NONE |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
31 |
| _ => NONE |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
32 |
end; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
33 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
34 |
fun default_list (target_fxy, target_cons) pr fxy t1 t2 = |
37242
97097e589715
brackify_infix etc.: no break before infix operator -- eases survival in Scala
haftmann
parents:
31055
diff
changeset
|
35 |
Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy ( |
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
36 |
pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1, |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
37 |
Code_Printer.str target_cons, |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
38 |
pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2 |
37242
97097e589715
brackify_infix etc.: no break before infix operator -- eases survival in Scala
haftmann
parents:
31055
diff
changeset
|
39 |
); |
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
40 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
41 |
fun add_literal_list target = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
42 |
let |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
43 |
fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
44 |
case Option.map (cons t1) (implode_list nil' cons' t2) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
45 |
of SOME ts => |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
46 |
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
47 |
| NONE => |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
48 |
default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; |
38923 | 49 |
in Code_Target.add_const_syntax target @{const_name Cons} |
37881 | 50 |
(SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))) |
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
51 |
end |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
52 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
53 |
end; |