Mercurial > urweb

comparison src/core_env.sml @ 20:1ab48e37d0ef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some con reducing
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 15:47:44 -0400
parents bc7b76ca57e0
children d3cc191cb25f
comparison
equal deleted inserted replaced
19:e634ae817a8e 20:1ab48e37d0ef
60 type env = { 60 type env = {
61 relC : (string * kind) list, 61 relC : (string * kind) list,
62 namedC : (string * kind * con option) IM.map, 62 namedC : (string * kind * con option) IM.map,
63 63
64 relE : (string * con) list, 64 relE : (string * con) list,
65 namedE : (string * con) IM.map 65 namedE : (string * con * exp option) IM.map
66 } 66 }
67 67
68 val empty = { 68 val empty = {
69 relC = [], 69 relC = [],
70 namedC = IM.empty, 70 namedC = IM.empty,
76 fun pushCRel (env : env) x k = 76 fun pushCRel (env : env) x k =
77 {relC = (x, k) :: #relC env, 77 {relC = (x, k) :: #relC env,
78 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 78 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
79 79
80 relE = map (fn (x, c) => (x, lift c)) (#relE env), 80 relE = map (fn (x, c) => (x, lift c)) (#relE env),
81 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)} 81 namedE = IM.map (fn (x, c, eo) => (x, lift c, eo)) (#namedE env)}
82 82
83 fun lookupCRel (env : env) n = 83 fun lookupCRel (env : env) n =
84 (List.nth (#relC env, n)) 84 (List.nth (#relC env, n))
85 handle Subscript => raise UnboundRel n 85 handle Subscript => raise UnboundRel n
86 86
105 105
106 fun lookupERel (env : env) n = 106 fun lookupERel (env : env) n =
107 (List.nth (#relE env, n)) 107 (List.nth (#relE env, n))
108 handle Subscript => raise UnboundRel n 108 handle Subscript => raise UnboundRel n
109 109
110 fun pushENamed (env : env) x n t = 110 fun pushENamed (env : env) x n t eo =
111 {relC = #relC env, 111 {relC = #relC env,
112 namedC = #namedC env, 112 namedC = #namedC env,
113 113
114 relE = #relE env, 114 relE = #relE env,
115 namedE = IM.insert (#namedE env, n, (x, t))} 115 namedE = IM.insert (#namedE env, n, (x, t, eo))}
116 116
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, _) =
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 | DVal (x, n, t, _) => pushENamed env x n t 125 | DVal (x, n, t, e) => pushENamed env x n t (SOME e)
126 126
127 val ktype = (KType, ErrorMsg.dummySpan) 127 val ktype = (KType, ErrorMsg.dummySpan)
128 128
129 fun bbind env x = 129 fun bbind env x =
130 case ElabEnv.lookupC ElabEnv.basis x of 130 case ElabEnv.lookupC ElabEnv.basis x of