comparison src/cjrize.sml @ 29:537db4ee89f4

Translation to Cjr
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Jun 2008 18:28:43 -0400
parents
children 198172560b73
comparison
equal deleted inserted replaced
28:104d43266b33 29:537db4ee89f4
1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 structure Cjrize :> CJRIZE = struct
29
30 structure L = Flat
31 structure L' = Cjr
32
33 structure Sm :> sig
34 type t
35
36 val empty : t
37 val find : t * (string * L.typ) list * (string * L'.typ) list -> t * int
38
39 val declares : t -> (int * (string * L'.typ) list) list
40 end = struct
41
42 structure FM = BinaryMapFn(struct
43 type ord_key = L.typ
44 val compare = FlatUtil.Typ.compare
45 end)
46
47 type t = int * int FM.map * (int * (string * L'.typ) list) list
48
49 val empty = (0, FM.empty, [])
50
51 fun find ((n, m, ds), xts, xts') =
52 let
53 val t = (L.TRecord xts, ErrorMsg.dummySpan)
54 in
55 case FM.find (m, t) of
56 NONE => ((n+1, FM.insert (m, t, n), (n, xts') :: ds), n)
57 | SOME i => ((n, m, ds), i)
58 end
59
60 fun declares (_, _, ds) = ds
61
62 end
63
64 fun cifyTyp ((t, loc), sm) =
65 case t of
66 L.TTop => ((L'.TTop, loc), sm)
67 | L.TFun (t1, t2) =>
68 let
69 val (_, sm) = cifyTyp (t1, sm)
70 val (_, sm) = cifyTyp (t2, sm)
71 in
72 ((L'.TFun, loc), sm)
73 end
74 | L.TCode (t1, t2) =>
75 let
76 val (t1, sm) = cifyTyp (t1, sm)
77 val (t2, sm) = cifyTyp (t2, sm)
78 in
79 ((L'.TCode (t1, t2), loc), sm)
80 end
81 | L.TRecord xts =>
82 let
83 val old_xts = xts
84 val (xts, sm) = ListUtil.foldlMap (fn ((x, t), sm) =>
85 let
86 val (t, sm) = cifyTyp (t, sm)
87 in
88 ((x, t), sm)
89 end)
90 sm xts
91 val (sm, si) = Sm.find (sm, old_xts, xts)
92 in
93 ((L'.TRecord si, loc), sm)
94 end
95 | L.TNamed n => ((L'.TNamed n, loc), sm)
96
97 fun cifyExp ((e, loc), sm) =
98 case e of
99 L.EPrim p => ((L'.EPrim p, loc), sm)
100 | L.ERel n => ((L'.ERel n, loc), sm)
101 | L.ENamed n => ((L'.ENamed n, loc), sm)
102 | L.ECode n => ((L'.ECode n, loc), sm)
103 | L.EApp (e1, e2) =>
104 let
105 val (e1, sm) = cifyExp (e1, sm)
106 val (e2, sm) = cifyExp (e2, sm)
107 in
108 ((L'.EApp (e1, e2), loc), sm)
109 end
110
111 | L.ERecord xes =>
112 let
113 val old_xts = map (fn (x, _, t) => (x, t)) xes
114
115 val (xets, sm) = ListUtil.foldlMap (fn ((x, e, t), sm) =>
116 let
117 val (e, sm) = cifyExp (e, sm)
118 val (t, sm) = cifyTyp (t, sm)
119 in
120 ((x, e, t), sm)
121 end)
122 sm xes
123
124 val (sm, si) = Sm.find (sm, old_xts, map (fn (x, _, t) => (x, t)) xets)
125
126 val xes = map (fn (x, e, _) => (x, e)) xets
127 val xes = ListMergeSort.sort (fn ((x1, _), (x2, _)) => String.compare (x1, x2) = GREATER) xes
128 in
129 ((L'.ERecord (si, xes), loc), sm)
130 end
131 | L.EField (e, x) =>
132 let
133 val (e, sm) = cifyExp (e, sm)
134 in
135 ((L'.EField (e, x), loc), sm)
136 end
137
138 | L.ELet (xes, e) =>
139 let
140 val (xes, sm) = ListUtil.foldlMap (fn ((x, t, e), sm) =>
141 let
142 val (t, sm) = cifyTyp (t, sm)
143 val (e, sm) = cifyExp (e, sm)
144 in
145 ((x, t, e), sm)
146 end)
147 sm xes
148 val (e, sm) = cifyExp (e, sm)
149 in
150 ((L'.ELet (xes, e), loc), sm)
151 end
152
153 fun cifyDecl ((d, loc), sm) =
154 case d of
155 L.DVal (x, n, t, e) =>
156 let
157 val (t, sm) = cifyTyp (t, sm)
158 val (e, sm) = cifyExp (e, sm)
159 in
160 ((L'.DVal (x, n, t, e), loc), sm)
161 end
162 | L.DFun (n, x, dom, ran, e) =>
163 let
164 val (dom, sm) = cifyTyp (dom, sm)
165 val (ran, sm) = cifyTyp (ran, sm)
166 val (e, sm) = cifyExp (e, sm)
167 in
168 ((L'.DFun (n, x, dom, ran, e), loc), sm)
169 end
170
171 fun cjrize ds =
172 let
173 val (ds, sm) = ListUtil.foldlMap cifyDecl Sm.empty ds
174 in
175 List.revAppend (map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm),
176 ds)
177 end
178
179 end