diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-08-03 19:49:21 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-03 19:49:21 -0400 |
commit | 744cdbb9e3907db9bb01576750634c614147e1a3 (patch) | |
tree | aecef31d4055d34a31977834cbda020811d1dfab /src/elab_env.sml | |
parent | 9a9f1738a8eae9df07f97da224cd9cf45033e9dc (diff) |
Datatype representation optimization
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r-- | src/elab_env.sml | 43 |
1 files changed, 24 insertions, 19 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 0367e023..23b29155 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -81,7 +81,7 @@ type env = { namedC : (string * kind * con option) IM.map, datatypes : datatyp IM.map, - constructors : (int * con option * int) SM.map, + constructors : (datatype_kind * int * con option * int) SM.map, renameE : con var' SM.map, relE : (string * con) list, @@ -189,26 +189,30 @@ fun lookupC (env : env) x = | SOME (Named' x) => Named x fun pushDatatype (env : env) n xncs = - {renameC = #renameC env, - relC = #relC env, - namedC = #namedC env, + let + val dk = U.classifyDatatype xncs + in + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, - 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, + 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, (dk, n', to, n))) + (#constructors env) xncs, - renameE = #renameE env, - relE = #relE env, - namedE = #namedE env, + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, - renameSgn = #renameSgn env, - sgn = #sgn env, + renameSgn = #renameSgn env, + sgn = #sgn env, - renameStr = #renameStr env, - str = #str env} + renameStr = #renameStr env, + str = #str env} + end fun lookupDatatype (env : env) n = case IM.find (#datatypes env, n) of @@ -579,13 +583,14 @@ fun projectConstructor env {sgn, str, field} = if x <> field then NONE else - SOME (n', to, (CNamed n, #2 str))) xncs + SOME (U.classifyDatatype xncs, n', to, (CNamed n, #2 str))) xncs in case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs) | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs) | _ => NONE) sgis of NONE => NONE - | SOME ((n, to, t), subs) => SOME (n, Option.map (sgnSubCon (str, subs)) to, sgnSubCon (str, subs) t) + | SOME ((dk, n, to, t), subs) => SOME (dk, n, Option.map (sgnSubCon (str, subs)) to, + sgnSubCon (str, subs) t) end | _ => NONE |