summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 11:32:48 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 11:32:48 -0400
commitc060d15003e3435d4d4c770d8f109f756db13ef5 (patch)
tree5c9410e11fe016de62d0172051144d570239de43 /src/elab_env.sml
parente9b1040a1f27a07afc7b2bf33522b1058163bf2b (diff)
Lifting cons in ElabEnv
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml38
1 files changed, 35 insertions, 3 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 27ea1750..417eab74 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -29,6 +29,9 @@ structure ElabEnv :> ELAB_ENV = struct
open Elab
+structure L' = Elab
+structure U = ElabUtil
+
structure IM = IntBinaryMap
structure SM = BinaryMapFn(struct
type ord_key = string
@@ -38,6 +41,30 @@ structure SM = BinaryMapFn(struct
exception UnboundRel of int
exception UnboundNamed of int
+
+(* AST utility functions *)
+
+exception SynUnif
+
+val liftConInCon =
+ U.Con.mapB {kind = fn k => k,
+ con = fn bound => fn c =>
+ case c of
+ L'.CRel xn =>
+ if xn < bound then
+ c
+ else
+ L'.CRel (xn + 1)
+ | L'.CUnif _ => raise SynUnif
+ | _ => c,
+ bind = fn (bound, U.Con.Rel _) => bound + 1
+ | (bound, _) => bound}
+
+val lift = liftConInCon 0
+
+
+(* Back to environments *)
+
datatype 'a var' =
Rel' of int * 'a
| Named' of int * 'a
@@ -76,11 +103,11 @@ fun pushCRel (env : env) x k =
in
{renameC = SM.insert (renameC, x, Rel' (0, k)),
relC = (x, k) :: #relC env,
- namedC = #namedC env,
+ namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
renameE = #renameE env,
- relE = #relE env,
- namedE = #namedE env}
+ relE = map (fn (x, c) => (x, lift c)) (#relE env),
+ namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)}
end
fun lookupCRel (env : env) n =
@@ -161,4 +188,9 @@ fun lookupE (env : env) x =
| SOME (Rel' x) => Rel x
| SOME (Named' x) => Named x
+fun declBinds env (d, _) =
+ case d of
+ DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
+ | DVal (x, n, t, _) => pushENamedAs env x n t
+
end