Mercurial > urweb
diff src/elab_env.sml @ 31:1c91c5e6840f
Simple signature matching
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 12 Jun 2008 17:16:20 -0400 |
parents | 9bd8669d53c2 |
children | 44b5405e74c7 |
line wrap: on
line diff
--- a/src/elab_env.sml Thu Jun 12 14:04:22 2008 -0400 +++ b/src/elab_env.sml Thu Jun 12 17:16:20 2008 -0400 @@ -80,7 +80,13 @@ renameE : con var' SM.map, relE : (string * con) list, - namedE : (string * con) IM.map + namedE : (string * con) IM.map, + + renameSgn : (int * sgn) SM.map, + sgn : (string * sgn) IM.map, + + renameStr : (int * sgn) SM.map, + str : (string * sgn) IM.map } val namedCounter = ref 0 @@ -92,7 +98,13 @@ renameE = SM.empty, relE = [], - namedE = IM.empty + namedE = IM.empty, + + renameSgn = SM.empty, + sgn = IM.empty, + + renameStr = SM.empty, + str = IM.empty } fun pushCRel (env : env) x k = @@ -106,7 +118,14 @@ renameE = #renameE env, relE = map (fn (x, c) => (x, lift c)) (#relE env), - namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)} + namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env + } end fun lookupCRel (env : env) n = @@ -120,7 +139,13 @@ renameE = #renameE env, relE = #relE env, - namedE = #namedE env} + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env} fun pushCNamed env x k co = let @@ -152,7 +177,13 @@ renameE = SM.insert (renameE, x, Rel' (0, t)), relE = (x, t) :: #relE env, - namedE = #namedE env} + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env} end fun lookupERel (env : env) n = @@ -166,7 +197,13 @@ renameE = SM.insert (#renameE env, x, Named' (n, t)), relE = #relE env, - namedE = IM.insert (#namedE env, n, (x, t))} + namedE = IM.insert (#namedE env, n, (x, t)), + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env} fun pushENamed env x t = let @@ -187,10 +224,80 @@ | SOME (Rel' x) => Rel x | SOME (Named' x) => Named x +fun pushSgnNamedAs (env : env) x n sgis = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, + + renameSgn = SM.insert (#renameSgn env, x, (n, sgis)), + sgn = IM.insert (#sgn env, n, (x, sgis)), + + renameStr = #renameStr env, + str = #str env} + +fun pushSgnNamed env x sgis = + let + val n = !namedCounter + in + namedCounter := n + 1; + (pushSgnNamedAs env x n sgis, n) + end + +fun lookupSgnNamed (env : env) n = + case IM.find (#sgn env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun lookupSgn (env : env) x = SM.find (#renameSgn env, x) + +fun pushStrNamedAs (env : env) x n sgis = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = SM.insert (#renameStr env, x, (n, sgis)), + str = IM.insert (#str env, n, (x, sgis))} + +fun pushStrNamed env x sgis = + let + val n = !namedCounter + in + namedCounter := n + 1; + (pushStrNamedAs env x n sgis, n) + end + +fun lookupStrNamed (env : env) n = + case IM.find (#str env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun lookupStr (env : env) x = SM.find (#renameStr env, 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 + | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn + | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn + +fun sgiBinds env (sgi, _) = + case sgi of + SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE + | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) + | SgiVal (x, n, t) => pushENamedAs env x n t + | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn + val ktype = (KType, ErrorMsg.dummySpan)