GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-20 10:19:32 -06:00
Code Issues Packages Projects Releases Wiki Activity

bugfix in the handling of implicit arguments in the typechecker

Browse Source
This commit is contained in:
krasimir
2011-01-08 12:55:50 +00:00
parent a985ea56ef
commit d465292fde
7 changed files with 79 additions and 43 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
src/runtime/haskell/PGF/TypeCheck.hs
View File

@@ -351,6 +351,7 @@ tcExpr scope (EMeta _) tty = do
return (EMeta i)
tcExpr scope e0 tty = do
(e0,tty0) <- infExpr scope e0
(e0,tty0) <- appImplArg scope e0 tty0
i <- newGuardedMeta e0
eqType scope (scopeSize scope) i tty tty0
return (EMeta i)
@@ -424,6 +425,14 @@ tcArg scope e1 e2 delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
then tcArg scope (EApp e1 (EImplArg (EMeta i))) e2 delta (DTyp hs c es)
else tcArg scope (EApp e1 (EImplArg (EMeta i))) e2 (VMeta i (scopeEnv scope) [] : delta) (DTyp hs c es)
appImplArg scope e (TTyp delta (DTyp ((Implicit,x,ty1):hypos) cat es)) = do
i <- newMeta scope (TTyp delta ty1)
let delta' = if x == wildCId
then delta
else VMeta i (scopeEnv scope) [] : delta
appImplArg scope (EApp e (EImplArg (EMeta i))) (TTyp delta' (DTyp hypos cat es))
appImplArg scope e tty = return (e,tty)
-----------------------------------------------------
-- eqType
-----------------------------------------------------