Mercurial > urweb
comparison src/expl_env.sml @ 56:d3cc191cb25f
Separate compilation and automatic basis importation
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Jun 2008 14:23:05 -0400 |
parents | 0a5c312de09a |
children | d609820c5834 |
comparison
equal
deleted
inserted
replaced
55:5c97b7cd912b | 56:d3cc191cb25f |
---|---|
249 SgiConAbs (x, n, k) => pushCNamed env x n k NONE | 249 SgiConAbs (x, n, k) => pushCNamed env x n k NONE |
250 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) | 250 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) |
251 | SgiVal (x, n, t) => pushENamed env x n t | 251 | SgiVal (x, n, t) => pushENamed env x n t |
252 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn | 252 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn |
253 | 253 |
254 | |
255 val ktype = (KType, ErrorMsg.dummySpan) | |
256 | |
257 fun bbind env x = | |
258 case ElabEnv.lookupC ElabEnv.basis x of | |
259 ElabEnv.NotBound => raise Fail "CoreEnv.bbind: Not bound" | |
260 | ElabEnv.Rel _ => raise Fail "CoreEnv.bbind: Rel" | |
261 | ElabEnv.Named (n, _) => pushCNamed env x n ktype NONE | |
262 | |
263 val basis = empty | |
264 val basis = bbind basis "int" | |
265 val basis = bbind basis "float" | |
266 val basis = bbind basis "string" | |
267 | |
268 end | 254 end |