Mercurial > urweb

comparison src/elab_util.sml @ 11:e97c6d335869

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simple elaboration working
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 15:20:46 -0400
parents dde5c52e5e5e
children d89477f07c1e
comparison
equal deleted inserted replaced
10:dde5c52e5e5e 11:e97c6d335869
75 75
76 end 76 end
77 77
78 structure Con = struct 78 structure Con = struct
79 79
80 fun mapfold {kind = fk, con = fc} = 80 datatype binder =
81 Rel of string * Elab.kind
82 | Named of string * Elab.kind
83
84 fun mapfoldB {kind = fk, con = fc, bind} =
81 let 85 let
82 val mfk = Kind.mapfold fk 86 val mfk = Kind.mapfold fk
83 87
84 fun mfc c acc = 88 fun mfc ctx c acc =
85 S.bindP (mfc' c acc, fc) 89 S.bindP (mfc' ctx c acc, fc ctx)
86 90
87 and mfc' (cAll as (c, loc)) = 91 and mfc' ctx (cAll as (c, loc)) =
88 case c of 92 case c of
89 TFun (c1, c2) => 93 TFun (c1, c2) =>
90 S.bind2 (mfc c1, 94 S.bind2 (mfc ctx c1,
91 fn c1' => 95 fn c1' =>
92 S.map2 (mfc c2, 96 S.map2 (mfc ctx c2,
93 fn c2' => 97 fn c2' =>
94 (TFun (c1', c2'), loc))) 98 (TFun (c1', c2'), loc)))
95 | TCFun (e, x, k, c) => 99 | TCFun (e, x, k, c) =>
96 S.bind2 (mfk k, 100 S.bind2 (mfk k,
97 fn k' => 101 fn k' =>
98 S.map2 (mfc c, 102 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
99 fn c' => 103 fn c' =>
100 (TCFun (e, x, k', c'), loc))) 104 (TCFun (e, x, k', c'), loc)))
101 | TRecord c => 105 | TRecord c =>
102 S.map2 (mfc c, 106 S.map2 (mfc ctx c,
103 fn c' => 107 fn c' =>
104 (TRecord c', loc)) 108 (TRecord c', loc))
105 109
106 | CRel _ => S.return2 cAll 110 | CRel _ => S.return2 cAll
107 | CNamed _ => S.return2 cAll 111 | CNamed _ => S.return2 cAll
108 | CApp (c1, c2) => 112 | CApp (c1, c2) =>
109 S.bind2 (mfc c1, 113 S.bind2 (mfc ctx c1,
110 fn c1' => 114 fn c1' =>
111 S.map2 (mfc c2, 115 S.map2 (mfc ctx c2,
112 fn c2' => 116 fn c2' =>
113 (CApp (c1', c2'), loc))) 117 (CApp (c1', c2'), loc)))
114 | CAbs (x, k, c) => 118 | CAbs (x, k, c) =>
115 S.bind2 (mfk k, 119 S.bind2 (mfk k,
116 fn k' => 120 fn k' =>
117 S.map2 (mfc c, 121 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
118 fn c' => 122 fn c' =>
119 (CAbs (x, k', c'), loc))) 123 (CAbs (x, k', c'), loc)))
120 124
121 | CName _ => S.return2 cAll 125 | CName _ => S.return2 cAll
122 126
123 | CRecord (k, xcs) => 127 | CRecord (k, xcs) =>
124 S.bind2 (mfk k, 128 S.bind2 (mfk k,
125 fn k' => 129 fn k' =>
126 S.map2 (ListUtil.mapfold (fn (x, c) => 130 S.map2 (ListUtil.mapfold (fn (x, c) =>
127 S.bind2 (mfc x, 131 S.bind2 (mfc ctx x,
128 fn x' => 132 fn x' =>
129 S.map2 (mfc c, 133 S.map2 (mfc ctx c,
130 fn c' => 134 fn c' =>
131 (x', c')))) 135 (x', c'))))
132 xcs, 136 xcs,
133 fn xcs' => 137 fn xcs' =>
134 (CRecord (k', xcs'), loc))) 138 (CRecord (k', xcs'), loc)))
135 | CConcat (c1, c2) => 139 | CConcat (c1, c2) =>
136 S.bind2 (mfc c1, 140 S.bind2 (mfc ctx c1,
137 fn c1' => 141 fn c1' =>
138 S.map2 (mfc c2, 142 S.map2 (mfc ctx c2,
139 fn c2' => 143 fn c2' =>
140 (CConcat (c1', c2'), loc))) 144 (CConcat (c1', c2'), loc)))
141 145
142 | CError => S.return2 cAll 146 | CError => S.return2 cAll
143 | CUnif (_, _, ref (SOME c)) => mfc' c 147 | CUnif (_, _, ref (SOME c)) => mfc' ctx c
144 | CUnif _ => S.return2 cAll 148 | CUnif _ => S.return2 cAll
145 in 149 in
146 mfc 150 mfc
147 end 151 end
148 152
153 fun mapfold {kind = fk, con = fc} =
154 mapfoldB {kind = fk,
155 con = fn () => fc,
156 bind = fn ((), _) => ()} ()
157
158 fun mapB {kind, con, bind} ctx c =
159 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
160 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
161 bind = bind} ctx c () of
162 S.Continue (c, ()) => c
163 | S.Return _ => raise Fail "Con.mapB: Impossible"
164
149 fun exists {kind, con} k = 165 fun exists {kind, con} k =
150 case mapfold {kind = fn k => fn () => 166 case mapfold {kind = fn k => fn () =>
151 if kind k then 167 if kind k then
152 S.Return () 168 S.Return ()
153 else 169 else
162 178
163 end 179 end
164 180
165 structure Exp = struct 181 structure Exp = struct
166 182
167 fun mapfold {kind = fk, con = fc, exp = fe} = 183 datatype binder =
184 RelC of string * Elab.kind
185 | NamedC of string * Elab.kind
186 | RelE of string * Elab.con
187 | NamedE of string * Elab.con
188
189 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
168 let 190 let
169 val mfk = Kind.mapfold fk 191 val mfk = Kind.mapfold fk
170 val mfc = Con.mapfold {kind = fk, con = fc} 192
171 193 fun bind' (ctx, b) =
172 fun mfe e acc = 194 let
173 S.bindP (mfe' e acc, fe) 195 val b' = case b of
174 196 Con.Rel x => RelC x
175 and mfe' (eAll as (e, loc)) = 197 | Con.Named x => NamedC x
198 in
199 bind (ctx, b')
200 end
201 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
202
203 fun mfe ctx e acc =
204 S.bindP (mfe' ctx e acc, fe ctx)
205
206 and mfe' ctx (eAll as (e, loc)) =
176 case e of 207 case e of
177 ERel _ => S.return2 eAll 208 ERel _ => S.return2 eAll
178 | ENamed _ => S.return2 eAll 209 | ENamed _ => S.return2 eAll
179 | EApp (e1, e2) => 210 | EApp (e1, e2) =>
180 S.bind2 (mfe e1, 211 S.bind2 (mfe ctx e1,
181 fn e1' => 212 fn e1' =>
182 S.map2 (mfe e2, 213 S.map2 (mfe ctx e2,
183 fn e2' => 214 fn e2' =>
184 (EApp (e1', e2'), loc))) 215 (EApp (e1', e2'), loc)))
185 | EAbs (x, t, e) => 216 | EAbs (x, t, e) =>
186 S.bind2 (mfc t, 217 S.bind2 (mfc ctx t,
187 fn t' => 218 fn t' =>
188 S.map2 (mfe e, 219 S.map2 (mfe (bind (ctx, RelE (x, t))) e,
189 fn e' => 220 fn e' =>
190 (EAbs (x, t', e'), loc))) 221 (EAbs (x, t', e'), loc)))
191 222
192 | ECApp (e, c) => 223 | ECApp (e, c) =>
193 S.bind2 (mfe e, 224 S.bind2 (mfe ctx e,
194 fn e' => 225 fn e' =>
195 S.map2 (mfc c, 226 S.map2 (mfc ctx c,
196 fn c' => 227 fn c' =>
197 (ECApp (e', c'), loc))) 228 (ECApp (e', c'), loc)))
198 | ECAbs (expl, x, k, e) => 229 | ECAbs (expl, x, k, e) =>
199 S.bind2 (mfk k, 230 S.bind2 (mfk k,
200 fn k' => 231 fn k' =>
201 S.map2 (mfe e, 232 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
202 fn e' => 233 fn e' =>
203 (ECAbs (expl, x, k', e'), loc))) 234 (ECAbs (expl, x, k', e'), loc)))
204 235
205 | EError => S.return2 eAll 236 | EError => S.return2 eAll
206 in 237 in
207 mfe 238 mfe
208 end 239 end
209 240
241 fun mapfold {kind = fk, con = fc, exp = fe} =
242 mapfoldB {kind = fk,
243 con = fn () => fc,
244 exp = fn () => fe,
245 bind = fn ((), _) => ()} ()
246
210 fun exists {kind, con, exp} k = 247 fun exists {kind, con, exp} k =
211 case mapfold {kind = fn k => fn () => 248 case mapfold {kind = fn k => fn () =>
212 if kind k then 249 if kind k then
213 S.Return () 250 S.Return ()
214 else 251 else
230 267
231 structure E = ElabEnv 268 structure E = ElabEnv
232 269
233 fun declBinds env (d, _) = 270 fun declBinds env (d, _) =
234 case d of 271 case d of
235 DCon (x, n, k, _) => E.pushCNamedAs env x n k 272 DCon (x, n, k, c) => E.pushCNamedAs env x n k (SOME c)
236 | DVal (x, n, t, _) => E.pushENamedAs env x n t 273 | DVal (x, n, t, _) => E.pushENamedAs env x n t
237 274
238 end 275 end