Mercurial > urweb
changeset 13:6049e2193bf2
Lifting cons in ElabEnv
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 08 Jun 2008 11:32:48 -0400 |
| parents | d89477f07c1e |
| children | f1c36df29ed7 |
| files | src/elab_env.sig src/elab_env.sml src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/sources |
| diffstat | 7 files changed, 46 insertions(+), 31 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_env.sig Fri Mar 28 17:34:57 2008 -0400 +++ b/src/elab_env.sig Sun Jun 08 11:32:48 2008 -0400 @@ -27,6 +27,9 @@ signature ELAB_ENV = sig + exception SynUnif + val liftConInCon : int -> Elab.con -> Elab.con + type env val empty : env @@ -57,4 +60,6 @@ val lookupE : env -> string -> Elab.con var + val declBinds : env -> Elab.decl -> env + end
--- a/src/elab_env.sml Fri Mar 28 17:34:57 2008 -0400 +++ b/src/elab_env.sml Sun Jun 08 11:32:48 2008 -0400 @@ -29,6 +29,9 @@ open Elab +structure L' = Elab +structure U = ElabUtil + structure IM = IntBinaryMap structure SM = BinaryMapFn(struct type ord_key = string @@ -38,6 +41,30 @@ 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 @@ 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 @@ | 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
--- a/src/elab_print.sml Fri Mar 28 17:34:57 2008 -0400 +++ b/src/elab_print.sml Sun Jun 08 11:32:48 2008 -0400 @@ -270,7 +270,7 @@ fun p_file env file = let val (_, pds) = ListUtil.mapfoldl (fn (d, env) => - (ElabUtil.declBinds env d, + (E.declBinds env d, p_decl env d)) env file in
--- a/src/elab_util.sig Fri Mar 28 17:34:57 2008 -0400 +++ b/src/elab_util.sig Sun Jun 08 11:32:48 2008 -0400 @@ -75,6 +75,4 @@ exp : Elab.exp' -> bool} -> Elab.exp -> bool end -val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env - end
--- a/src/elab_util.sml Fri Mar 28 17:34:57 2008 -0400 +++ b/src/elab_util.sml Sun Jun 08 11:32:48 2008 -0400 @@ -286,11 +286,4 @@ end -structure E = ElabEnv - -fun declBinds env (d, _) = - case d of - DCon (x, n, k, c) => E.pushCNamedAs env x n k (SOME c) - | DVal (x, n, t, _) => E.pushENamedAs env x n t - end
--- a/src/elaborate.sml Fri Mar 28 17:34:57 2008 -0400 +++ b/src/elaborate.sml Sun Jun 08 11:32:48 2008 -0400 @@ -344,21 +344,8 @@ | CRecordFailure => eprefaces "Can't unify record constructors" [] -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} +exception SynUnif = E.SynUnif +val liftConInCon = E.liftConInCon val subConInCon = U.Con.mapB {kind = fn k => k,