Mercurial > urweb

comparison src/elab_ops.sml @ 905:7a4b026e45dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Library improvements; proper list [un]urlification; remove server-side ServerCalls; eta reduction in type inference
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Aug 2009 16:13:27 -0400
parents 12b73f3c108e
children 46803e668a89
comparison
equal deleted inserted replaced
904:6d9538ce94d8 905:7a4b026e45dd
129 c 129 c
130 | c => c, 130 | c => c,
131 sgn_item = fn sgi => sgi, 131 sgn_item = fn sgi => sgi,
132 sgn = fn sgn => sgn} 132 sgn = fn sgn => sgn}
133 133
134 val occurs =
135 U.Con.existsB {kind = fn _ => false,
136 con = fn (n, c) =>
137 case c of
138 CRel n' => n' = n
139 | _ => false,
140 bind = fn (n, b) =>
141 case b of
142 U.Con.RelC _ => n + 1
143 | _ => n}
144 0
145
134 146
135 fun hnormCon env (cAll as (c, loc)) = 147 fun hnormCon env (cAll as (c, loc)) =
136 case c of 148 case c of
137 CUnif (_, _, _, ref (SOME c)) => hnormCon env c 149 CUnif (_, _, _, ref (SOME c)) => hnormCon env c
138 150
153 case E.projectCon env {sgn = sgn, str = str, field = x} of 165 case E.projectCon env {sgn = sgn, str = str, field = x} of
154 NONE => raise Fail "kindof: Unknown con in structure" 166 NONE => raise Fail "kindof: Unknown con in structure"
155 | SOME (_, NONE) => cAll 167 | SOME (_, NONE) => cAll
156 | SOME (_, SOME c) => hnormCon env c 168 | SOME (_, SOME c) => hnormCon env c
157 end 169 end
170
171 (* Eta reduction *)
172 | CAbs (x, k, b) =>
173 (case #1 (hnormCon (E.pushCRel env x k) b) of
174 CApp (f, (CRel 0, _)) =>
175 if occurs f then
176 cAll
177 else
178 hnormCon env (subConInCon (0, (CUnit, loc)) f)
179 | _ => cAll)
158 180
159 | CApp (c1, c2) => 181 | CApp (c1, c2) =>
160 (case #1 (hnormCon env c1) of 182 (case #1 (hnormCon env c1) of
161 CAbs (x, k, cb) => 183 CAbs (x, k, cb) =>
162 let 184 let