Mercurial > urweb
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 |