Mercurial > urweb
diff src/elab_env.sml @ 171:c7a6e6dbc318
Elaborating some basic pattern matching
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 31 Jul 2008 10:06:27 -0400 |
| parents | 06a98129b23f |
| children | 7ee424760d2f |
line wrap: on
line diff
--- a/src/elab_env.sml Tue Jul 29 16:38:15 2008 -0400 +++ b/src/elab_env.sml Thu Jul 31 10:06:27 2008 -0400 @@ -81,6 +81,7 @@ namedC : (string * kind * con option) IM.map, datatypes : datatyp IM.map, + constructors : (int * con option * int) SM.map, renameE : con var' SM.map, relE : (string * con) list, @@ -109,6 +110,7 @@ namedC = IM.empty, datatypes = IM.empty, + constructors = SM.empty, renameE = SM.empty, relE = [], @@ -131,6 +133,7 @@ namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), datatypes = #datatypes env, + constructors = #constructors env, renameE = #renameE env, relE = map (fn (x, c) => (x, lift c)) (#relE env), @@ -154,6 +157,7 @@ namedC = IM.insert (#namedC env, n, (x, k, co)), datatypes = #datatypes env, + constructors = #constructors env, renameE = #renameE env, relE = #relE env, @@ -192,6 +196,9 @@ datatypes = IM.insert (#datatypes env, n, foldl (fn ((x, n, to), cons) => IM.insert (cons, n, (x, to))) IM.empty xncs), + constructors = foldl (fn ((x, n', to), cmap) => + SM.insert (cmap, x, (n', to, n))) + (#constructors env) xncs, renameE = #renameE env, relE = #relE env, @@ -208,11 +215,13 @@ NONE => raise UnboundNamed n | SOME x => x -fun lookupConstructor dt n = +fun lookupDatatypeConstructor dt n = case IM.find (dt, n) of NONE => raise UnboundNamed n | SOME x => x +fun lookupConstructor (env : env) s = SM.find (#constructors env, s) + fun constructors dt = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt fun pushERel (env : env) x t = @@ -225,6 +234,7 @@ namedC = #namedC env, datatypes = #datatypes env, + constructors = #constructors env, renameE = SM.insert (renameE, x, Rel' (0, t)), relE = (x, t) :: #relE env, @@ -247,6 +257,7 @@ namedC = #namedC env, datatypes = #datatypes env, + constructors = #constructors env, renameE = SM.insert (#renameE env, x, Named' (n, t)), relE = #relE env, @@ -283,6 +294,7 @@ namedC = #namedC env, datatypes = #datatypes env, + constructors = #constructors env, renameE = #renameE env, relE = #relE env, @@ -315,6 +327,7 @@ namedC = #namedC env, datatypes = #datatypes env, + constructors = #constructors env, renameE = #renameE env, relE = #relE env,