Mercurial > urweb
comparison src/elab_env.sml @ 5:258261a53842
Elaborating files
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 26 Jan 2008 16:02:47 -0500 |
parents | 64f09f7822c3 |
children | 14b533dbe6cc |
comparison
equal
deleted
inserted
replaced
4:5c3cc348e9e6 | 5:258261a53842 |
---|---|
73 | 73 |
74 fun lookupCRel (env : env) n = | 74 fun lookupCRel (env : env) n = |
75 (List.nth (#relC env, n)) | 75 (List.nth (#relC env, n)) |
76 handle Subscript => raise UnboundRel n | 76 handle Subscript => raise UnboundRel n |
77 | 77 |
78 fun pushCNamed (env : env) x k = | 78 fun pushCNamedAs (env : env) x n k = |
79 {renameC = SM.insert (#renameC env, x, CNamed' (n, k)), | |
80 relC = #relC env, | |
81 namedC = IM.insert (#namedC env, n, (x, k))} | |
82 | |
83 fun pushCNamed env x k = | |
79 let | 84 let |
80 val n = !namedCounter | 85 val n = !namedCounter |
81 in | 86 in |
82 namedCounter := n + 1; | 87 namedCounter := n + 1; |
83 ({renameC = SM.insert (#renameC env, x, CNamed' (n, k)), | 88 (pushCNamedAs env x n k, n) |
84 relC = #relC env, | |
85 namedC = IM.insert (#namedC env, n, (x, k))}, | |
86 n) | |
87 end | 89 end |
88 | 90 |
89 fun lookupCNamed (env : env) n = | 91 fun lookupCNamed (env : env) n = |
90 case IM.find (#namedC env, n) of | 92 case IM.find (#namedC env, n) of |
91 NONE => raise UnboundNamed n | 93 NONE => raise UnboundNamed n |