Browse files

Fixed evaluation under binders

Ignore-this: 38101a08c6a6a83defea342679056aa3

darcs-hash:20090727110432-228f4-06a5afa9857c4b60b90198c429de4b5d66743a8a.gz
  • Loading branch information...
1 parent 8d9a89d commit 1fcabbe605e33f064992dd196ae0fbd2dbdfc517 eb committed Jul 27, 2009
Showing with 4 additions and 3 deletions.
  1. +4 −3 Ivor/Evaluator.lhs
View
7 Ivor/Evaluator.lhs
@@ -77,9 +77,10 @@ Code Stack Env Result
> evalScope n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats
> evalScope n ty sc [] env pats
-> | open = let n' = uniqify n (map sfst env)
-> newsc = pToV n' (eval sc [] ((n',ty,P n'):env) pats) in
-> buildenv env $ unload (Bind n' (B Lambda ty) newsc)
+> | open = let n' = uniqify n (map sfst env ++ map fst pats)
+> tmpname = (MN ("E", length env))
+> newsc = pToV tmpname (eval sc [] ((n',ty,P tmpname):env) pats) in
+> buildenv env $ unload (Bind n' (B Lambda ty) newsc)
> [] pats env
> | otherwise
> = buildenv env $ unload (Bind n (B Lambda ty) (Sc sc)) [] pats env -- in Whnf

0 comments on commit 1fcabbe

Please sign in to comment.