Mercurial > urweb
diff src/cjr_env.sml @ 181:31dfab1d4050
Cjrize ECon
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 03 Aug 2008 11:17:33 -0400 |
parents | 25b169416ea8 |
children | d11754ffe252 |
line wrap: on
line diff
--- a/src/cjr_env.sml Sun Aug 03 11:03:35 2008 -0400 +++ b/src/cjr_env.sml Sun Aug 03 11:17:33 2008 -0400 @@ -39,6 +39,7 @@ type env = { datatypes : (string * (string * int * typ option) list) IM.map, + constructors : (string * typ option * int) IM.map, numRelE : int, relE : (string * typ) list, @@ -49,6 +50,7 @@ val empty = { datatypes = IM.empty, + constructors = IM.empty, numRelE = 0, relE = [], @@ -59,6 +61,9 @@ fun pushDatatype (env : env) x n xncs = {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, numRelE = #numRelE env, relE = #relE env, @@ -71,8 +76,14 @@ 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 = {datatypes = #datatypes env, + constructors = #constructors env, numRelE = #numRelE env + 1, relE = (x, t) :: #relE env, @@ -90,6 +101,7 @@ fun pushENamed (env : env) x n t = {datatypes = #datatypes env, + constructors = #constructors env, numRelE = #numRelE env, relE = #relE env, @@ -104,6 +116,7 @@ fun pushStruct (env : env) n xts = {datatypes = #datatypes env, + constructors = #constructors env, numRelE = #numRelE env, relE = #relE env,