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

when faced with hard unification problem the type checker should just postpone the decision instead of failing immediately. added test case as well

Browse Source
This commit is contained in:
krasimir
2010-10-25 15:47:33 +00:00
parent aa6b07afdb
commit 0ba1daf5eb
4 changed files with 33 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -184,7 +184,7 @@ addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s ()
addConstraint i j c = do
mv <- getMeta j
case mv of
MUnbound s scope tty cs -> addRef >> setMeta j (MUnbound s scope tty ((\e -> release >> c e) : cs))
MUnbound s scope tty cs -> addRef >> setMeta j (MUnbound s scope tty ((\e -> release >> c e) : cs))
MBound e -> c e
MGuarded e cs x | x == 0 -> c e
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c e) : cs) x)
@@ -477,15 +477,11 @@ eqValue fail suspend k v1 v2 = do
eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VMeta i env1 vs1) v2 = do mv <- getMeta i
case mv of
MUnbound _ scopei _ cs -> do e2 <- mkLam i scopei env1 vs1 v2
setMeta i (MBound e2)
sequence_ [c e2 | c <- cs]
MUnbound _ scopei _ cs -> bind i scopei cs env1 vs1 v2
MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env1 e vs1 >>= \v1 -> eqValue' k v1 v2) : cs) x)
eqValue' k v1 (VMeta i env2 vs2) = do mv <- getMeta i
case mv of
MUnbound _ scopei _ cs -> do e1 <- mkLam i scopei env2 vs2 v1
setMeta i (MBound e1)
sequence_ [c e1 | c <- cs]
MUnbound _ scopei _ cs -> bind i scopei cs env2 vs2 v1
MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env2 e vs2 >>= \v2 -> eqValue' k v1 v2) : cs) x)
eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VConst f1 vs1) (VConst f2 vs2) | f1 == f2 = zipWithM_ (eqValue fail suspend k) vs1 vs2
@@ -495,16 +491,17 @@ eqValue fail suspend k v1 v2 = do
in eqExpr fail suspend (k+1) (v:env1) e1 (v:env2) e2
eqValue' k v1 v2 = fail
mkLam i scope env vs0 v = do
bind i scope cs env vs0 v = do
let k = scopeSize scope
vs = reverse (take k env) ++ vs0
xs = nub [i | VGen i [] <- vs]
if length vs == length xs
then return ()
else fail
v <- occurCheck i k xs v
e <- value2expr (length xs) v
return (addLam vs0 e)
if length vs /= length xs
then suspend i (\e -> apply env e vs0 >>= \iv -> eqValue fail suspend k iv v)
else do v <- occurCheck i k xs v
e0 <- value2expr (length xs) v
let e = addLam vs0 e0
setMeta i (MBound e)
sequence_ [c e | c <- cs]
where
addLam [] e = e
addLam (v:vs) e = EAbs Explicit var (addLam vs e)

14
testsuite/runtime/typecheck/Hard.gf Normal file
View File

@@ -0,0 +1,14 @@
abstract Hard = {
cat I ;
F (I -> I) ;
A (I -> I) I ;
S ;
fun
app : (f : I -> I) -> A f (f i) ;
ex : F (\x -> x) ;
i : I ;
s : (f : I -> I) -> A f i -> F f -> S ;
}

3
testsuite/runtime/typecheck/hard-unification.gfs Normal file
View File

@@ -0,0 +1,3 @@
i testsuite/runtime/typecheck/Hard.gf
ai s ? (app ?) ex
ai s ? (app ?) ?

5
testsuite/runtime/typecheck/hard-unification.gfs.gold Normal file
View File

@@ -0,0 +1,5 @@
Expression: s (\v0 -> v0) (app (\v0 -> v0)) ex
Type: S
Meta variable(s) ?2 should be resolved
in the expression: s ?2 (app ?2) ?4