comparison src/core_env.sml @ 163:80192edca30d

Datatypes through corify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 13:16:21 -0400
parents 76a4d69719d8
children 25b169416ea8
comparison
equal deleted inserted replaced
162:06a98129b23f 163:80192edca30d
117 fun lookupENamed (env : env) n = 117 fun lookupENamed (env : env) n =
118 case IM.find (#namedE env, n) of 118 case IM.find (#namedE env, n) of
119 NONE => raise UnboundNamed n 119 NONE => raise UnboundNamed n
120 | SOME x => x 120 | SOME x => x
121 121
122 fun declBinds env (d, _) = 122 fun declBinds env (d, loc) =
123 case d of 123 case d of
124 DCon (x, n, k, c) => pushCNamed env x n k (SOME c) 124 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
125 | DDatatype (x, n, xncs) =>
126 let
127 val env = pushCNamed env x n (KType, loc) NONE
128 in
129 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""
130 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc) NONE "")
131 env xncs
132 end
125 | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s 133 | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
126 | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis 134 | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis
127 | DExport _ => env 135 | DExport _ => env
128 136
129 end 137 end