280 Ts holds types of bound variables*) |
280 Ts holds types of bound variables*) |
281 fun fastype (Envir {tyenv, ...}) = |
281 fun fastype (Envir {tyenv, ...}) = |
282 let |
282 let |
283 val funerr = "fastype: expected function type"; |
283 val funerr = "fastype: expected function type"; |
284 fun fast Ts (f $ u) = |
284 fun fast Ts (f $ u) = |
285 (case fast Ts f of |
285 (case Type.devar tyenv (fast Ts f) of |
286 Type ("fun", [_, T]) => T |
286 Type ("fun", [_, T]) => T |
287 | TVar v => |
287 | TVar v => raise TERM (funerr, [f $ u]) |
288 (case Type.lookup tyenv v of |
|
289 SOME (Type ("fun", [_, T])) => T |
|
290 | _ => raise TERM (funerr, [f $ u])) |
|
291 | _ => raise TERM (funerr, [f $ u])) |
288 | _ => raise TERM (funerr, [f $ u])) |
292 | fast Ts (Const (_, T)) = T |
289 | fast Ts (Const (_, T)) = T |
293 | fast Ts (Free (_, T)) = T |
290 | fast Ts (Free (_, T)) = T |
294 | fast Ts (Bound i) = |
291 | fast Ts (Bound i) = |
295 (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i])) |
292 (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i])) |