author | haftmann |
Tue, 01 Jun 2010 13:52:11 +0200 | |
changeset 37242 | 97097e589715 |
parent 31055 | 2cf6efca6c71 |
child 37744 | 3daaf23b9ab4 |
permissions | -rw-r--r-- |
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
1 |
(* Author: Florian Haftmann, TU Muenchen |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
2 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
3 |
Code generation for list literals. |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
4 |
*) |
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 |
signature LIST_CODE = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
7 |
sig |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
8 |
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
|
9 |
val default_list: int * string |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
10 |
-> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
11 |
-> 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
|
12 |
val add_literal_list: string -> theory -> theory |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
13 |
end; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
14 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
15 |
structure List_Code : LIST_CODE = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
16 |
struct |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
17 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
18 |
open Basic_Code_Thingol; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
19 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
20 |
fun implode_list nil' cons' t = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
21 |
let |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
22 |
fun dest_cons (IConst (c, _) `$ t1 `$ t2) = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
23 |
if c = cons' |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
24 |
then SOME (t1, t2) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
25 |
else NONE |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
26 |
| dest_cons _ = NONE; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
27 |
val (ts, t') = Code_Thingol.unfoldr dest_cons t; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
28 |
in case t' |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
29 |
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
|
30 |
| _ => NONE |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
31 |
end; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
32 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
33 |
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
|
34 |
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
|
35 |
pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1, |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
36 |
Code_Printer.str target_cons, |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
37 |
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
|
38 |
); |
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
39 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
40 |
fun add_literal_list target = |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
41 |
let |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
42 |
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
|
43 |
case Option.map (cons t1) (implode_list nil' cons' t2) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
44 |
of SOME ts => |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
45 |
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
|
46 |
| NONE => |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
47 |
default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
48 |
in Code_Target.add_syntax_const target |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
49 |
@{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty))) |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
50 |
end |
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
51 |
|
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
diff
changeset
|
52 |
end; |