diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-02 11:15:32 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-02 11:15:32 -0400 |
| commit | 49c123050b2bc8a24f250fcc0d55e49484bc604c (patch) | |
| tree | 9dfcca82a4a6629190d044d10950f50872dbe52e /src/core_env.sml | |
| parent | 16d3d1c3a6d1e78faab91076c20b76fdcb90edb9 (diff) | |
Case through corify
Diffstat (limited to 'src/core_env.sml')
| -rw-r--r-- | src/core_env.sml | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/core_env.sml b/src/core_env.sml index cb10a354..4895de9c 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -62,6 +62,7 @@ type env = { namedC : (string * kind * con option) IM.map, datatypes : (string * (string * int * con option) list) IM.map, + constructors : (string * con option * int) IM.map, relE : (string * con) list, namedE : (string * con * exp option * string) IM.map @@ -72,6 +73,7 @@ val empty = { namedC = IM.empty, datatypes = IM.empty, + constructors = IM.empty, relE = [], namedE = IM.empty @@ -82,6 +84,7 @@ fun pushCRel (env : env) x k = namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), datatypes = #datatypes env, + constructors = #constructors env, relE = map (fn (x, c) => (x, lift c)) (#relE env), namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)} @@ -95,6 +98,7 @@ fun pushCNamed (env : env) x n k co = namedC = IM.insert (#namedC env, n, (x, k, co)), datatypes = #datatypes env, + constructors = #constructors env, relE = #relE env, namedE = #namedE env} @@ -109,6 +113,9 @@ fun pushDatatype (env : env) x n xncs = namedC = #namedC env, datatypes = IM.insert (#datatypes env, n, (x, xncs)), + constructors = foldl (fn ((x, n, to), constructors) => + IM.insert (constructors, n, (x, to, n))) + (#constructors env) xncs, relE = #relE env, namedE = #namedE env} @@ -118,11 +125,17 @@ fun lookupDatatype (env : env) n = NONE => raise UnboundNamed n | SOME x => x +fun lookupConstructor (env : env) n = + case IM.find (#constructors env, n) of + NONE => raise UnboundNamed n + | SOME x => x + fun pushERel (env : env) x t = {relC = #relC env, namedC = #namedC env, datatypes = #datatypes env, + constructors = #constructors env, relE = (x, t) :: #relE env, namedE = #namedE env} @@ -136,6 +149,7 @@ fun pushENamed (env : env) x n t eo s = namedC = #namedC env, datatypes = #datatypes env, + constructors = #constructors env, relE = #relE env, namedE = IM.insert (#namedE env, n, (x, t, eo, s))} |