diff options
| -rw-r--r-- | src/runtime/haskell/PGF/TypeCheck.hs | 47 | ||||
| -rw-r--r-- | testsuite/runtime/typecheck/Test.gf | 2 | ||||
| -rw-r--r-- | testsuite/runtime/typecheck/typecheck.gfs | 3 | ||||
| -rw-r--r-- | testsuite/runtime/typecheck/typecheck.gfs.gold | 3 |
4 files changed, 36 insertions, 19 deletions
diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs index b64383aad..06459b991 100644 --- a/src/runtime/haskell/PGF/TypeCheck.hs +++ b/src/runtime/haskell/PGF/TypeCheck.hs @@ -425,8 +425,8 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 then return () else raiseTypeMatchError v <- occurCheck i k xs v - funs <- getFuns - return (addLam vs0 (value2expr funs (length xs) v)) + e <- value2expr (length xs) v + return (addLam vs0 e) where addLam [] e = e addLam (v:vs) e = EAbs Explicit var (addLam vs e) @@ -481,16 +481,20 @@ checkResolvedMetaStore scope e = TcM (\abstr metaid ms -> evalType :: Int -> TType -> TcM Type evalType k (TTyp delta ty) = do funs <- getFuns - refineType (evalTy funs k delta ty) + evalTy funs k delta ty where - evalTy sig k delta (DTyp hyps cat es) = - let ((k1,delta1),hyps1) = mapAccumL (evalHypo sig) (k,delta) hyps - in DTyp hyps1 cat (List.map (normalForm sig k1 delta1) es) - - evalHypo sig (k,delta) (b,x,ty) = - if x == wildCId - then ((k, delta),(b,x,evalTy sig k delta ty)) - else ((k+1,(VGen k []):delta),(b,x,evalTy sig k delta ty)) + evalTy sig k delta (DTyp hyps cat es) = do + (k,delta,hyps) <- evalHypos sig k delta hyps + es <- mapM (value2expr k . eval sig delta) es + return (DTyp hyps cat es) + + evalHypos sig k delta [] = return (k,delta,[]) + evalHypos sig k delta ((b,x,ty):hyps) = do + ty <- evalTy sig k delta ty + (k,delta,hyps) <- if x == wildCId + then evalHypos sig k delta hyps + else evalHypos sig (k+1) ((VGen k []):delta) hyps + return (k,delta,(b,x,ty) : hyps) ----------------------------------------------------- @@ -519,10 +523,17 @@ refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty)) refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es) -value2expr sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs) -value2expr sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs) -value2expr sig i (VConst f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs) -value2expr sig i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr sig i) vs) -value2expr sig i (VSusp j env vs k) = value2expr sig i (k (VGen j vs)) -value2expr sig i (VLit l) = ELit l -value2expr sig i (VClosure env (EAbs b x e)) = EAbs b x (value2expr sig (i+1) (eval sig ((VGen i []):env) e)) +value2expr :: Int -> Value -> TcM Expr +value2expr i v = TcM (\abstr metaid ms -> Ok metaid ms (value2expr ms (funs abstr) i v)) + where + value2expr ms sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr ms sig i) vs) + value2expr ms sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr ms sig i) vs) + value2expr ms sig i (VConst f vs) = foldl EApp (EFun f) (List.map (value2expr ms sig i) vs) + value2expr ms sig i (VMeta j env vs) = case IntMap.lookup j ms of + Just (MBound e ) -> value2expr ms sig i (apply sig env e vs) + Just (MGuarded e _ _) -> value2expr ms sig i (apply sig env e vs) + _ -> foldl EApp (EMeta j) (List.map (value2expr ms sig i) vs) + value2expr ms sig i (VSusp j env vs k) = value2expr ms sig i (k (VGen j vs)) + value2expr ms sig i (VLit l) = ELit l + value2expr ms sig i (VClosure env (EAbs b x e)) = EAbs b x (value2expr ms sig (i+1) (eval sig ((VGen i []):env) e)) + value2expr ms sig i (VImplArg v) = EImplArg (value2expr ms sig i v) diff --git a/testsuite/runtime/typecheck/Test.gf b/testsuite/runtime/typecheck/Test.gf index 8ef0e03cf..9df65365e 100644 --- a/testsuite/runtime/typecheck/Test.gf +++ b/testsuite/runtime/typecheck/Test.gf @@ -34,4 +34,6 @@ fun h : (n : Nat) -> U n n -> Int ; -- fun u2 : (n : Nat) -> U (plus n zero) zero ;
-- fun h2 : (f : Nat -> Nat) -> ((n : Nat) -> U (f n) (f zero)) -> Int ;
+fun forall2 : (n : Nat) -> (Vector n -> Vector n -> Int) -> Int ;
+
}
\ No newline at end of file diff --git a/testsuite/runtime/typecheck/typecheck.gfs b/testsuite/runtime/typecheck/typecheck.gfs index 5a663aef3..60114b035 100644 --- a/testsuite/runtime/typecheck/typecheck.gfs +++ b/testsuite/runtime/typecheck/typecheck.gfs @@ -27,4 +27,5 @@ ai h ? (u1 ?) ai cmpVector (succ (succ zero)) (vector (succ (succ zero))) (append ? (succ zero) (vector ?) (vector (succ zero)))
ai diff ? (succ (succ zero)) (vector (succ (succ (succ (succ (succ zero)))))) (vector (succ (succ (succ zero))))
ai diff ? (succ (succ zero)) (vector (succ (succ (succ (succ zero))))) (vector (succ (succ (succ zero))))
-ai idMorph (mkMorph2 (\x -> ?) (vector zero))
\ No newline at end of file +ai idMorph (mkMorph2 (\x -> ?) (vector zero))
+ai <(\n -> forall2 n (\x,y -> cmpVector zero x y)) : Nat -> Int>
\ No newline at end of file diff --git a/testsuite/runtime/typecheck/typecheck.gfs.gold b/testsuite/runtime/typecheck/typecheck.gfs.gold index a43a0c216..9630aa3bf 100644 --- a/testsuite/runtime/typecheck/typecheck.gfs.gold +++ b/testsuite/runtime/typecheck/typecheck.gfs.gold @@ -69,3 +69,6 @@ In the expression: vector (succ (succ (succ (succ zero)))) Couldn't match expected type Vector ?1
against inferred type Vector zero
In the expression: vector zero
+Couldn't match expected type Vector zero
+ against inferred type Vector n
+In the expression: x
|