Mercurial > urweb

comparison src/expl_env.sml @ 56:d3cc191cb25f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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