diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs index d7af03f22..e3b4ddbae 100644 --- a/src/GF/Grammar/Grammar.hs +++ b/src/GF/Grammar/Grammar.hs @@ -122,6 +122,7 @@ data Term = | App Term Term -- ^ application: @f a@ | Abs BindType Ident Term -- ^ abstraction: @\x -> b@ | Meta {-# UNPACK #-} !MetaId -- ^ metavariable: @?i@ (only parsable: ? = ?0) + | ImplArg Term -- ^ placeholder for implicit argument @{t}@ | Prod BindType Ident Term Term -- ^ function type: @(x : A) -> B@, @A -> B@, @({x} : A) -> B@ | Typed Term Term -- ^ type-annotated term -- @@ -177,6 +178,8 @@ data Patt = | PVal Patt Type Int -- ^ parameter value number: @T # i# | PAs Ident Patt -- ^ as-pattern: x@p + + | PImplArg Patt -- ^ placeholder for pattern for implicit argument @{p}@ -- regular expression patterns | PNeg Patt -- ^ negated pattern: -p diff --git a/src/GF/Grammar/Parser.y b/src/GF/Grammar/Parser.y index 4dea6b8ec..1c6b51e77 100644 --- a/src/GF/Grammar/Parser.y +++ b/src/GF/Grammar/Parser.y @@ -414,7 +414,8 @@ Exp3 Exp4 :: { Term } Exp4 - : Exp4 Exp5 { App $1 $2 } + : Exp4 Exp5 { App $1 $2 } + | Exp4 '{' Exp '}' { App $1 (ImplArg $3) } | 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of Typed _ t -> TTyped t _ -> TRaw @@ -488,7 +489,6 @@ Patt2 | '#' Ident '.' Ident { PM $2 $4 } | '_' { PW } | Ident { PV $1 } - | '{' Ident '}' { PC $2 [] } | Ident '.' Ident { PP $1 $3 [] } | Integer { PInt $1 } | Double { PFloat $1 } @@ -522,8 +522,12 @@ ListPattAss ListPatt :: { [Patt] } ListPatt - : Patt2 { [$1] } - | Patt2 ListPatt { $1 : $2 } + : PattArg { [$1] } + | PattArg ListPatt { $1 : $2 } + +PattArg :: { Patt } + : Patt2 { $1 } + | '{' Patt2 '}' { PImplArg $2 } Arg :: { [(BindType,Ident)] } Arg diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs index 8a30a0988..78dbfb6a8 100644 --- a/src/PGF/Expr.hs +++ b/src/PGF/Expr.hs @@ -14,7 +14,7 @@ module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(.. MetaId, -- helpers - pMeta,pStr,pFactor,pLit,freshName,ppMeta,ppLit,ppParens + pMeta,pStr,pArg,pLit,freshName,ppMeta,ppLit,ppParens ) where import PGF.CId @@ -56,7 +56,8 @@ data Expr = | EMeta {-# UNPACK #-} !MetaId -- ^ meta variable | EFun CId -- ^ function or data constructor | EVar {-# UNPACK #-} !Int -- ^ variable with de Bruijn index - | ETyped Expr Type + | ETyped Expr Type -- ^ local type signature + | EImplArg Expr -- ^ implicit argument in expression deriving (Eq,Ord,Show) -- | The pattern is used to define equations in the abstract syntax of the grammar. @@ -65,6 +66,7 @@ data Patt = | PLit Literal -- ^ literal | PVar CId -- ^ variable | PWild -- ^ wildcard + | PImplArg Patt -- ^ implicit argument in pattern deriving (Eq,Ord) -- | The equation is used to define lambda function as a sequence @@ -134,7 +136,10 @@ unDouble (ELit (LFlt f)) = Just f pExpr :: RP.ReadP Expr pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm) where - pTerm = fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces) + pTerm = do f <- pFactor + RP.skipSpaces + as <- RP.sepBy pArg RP.skipSpaces + return (foldl EApp f as) pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") pBinds e <- pExpr @@ -154,6 +159,10 @@ pBinds = do xss <- RP.sepBy1 (RP.skipSpaces >> pBind) (RP.skipSpaces >> RP.char (RP.skipSpaces >> RP.char '}') (RP.sepBy1 (RP.skipSpaces >> pCIdOrWild >>= \id -> return (Implicit,id)) (RP.skipSpaces >> RP.char ',')) +pArg = fmap EImplArg (RP.between (RP.char '{') (RP.char '}') pExpr) + RP.<++ + pFactor + pFactor = fmap EFun pCId RP.<++ fmap ELit pLit RP.<++ fmap EMeta pMeta @@ -203,6 +212,7 @@ ppExpr d scope (EMeta n) = ppMeta n ppExpr d scope (EFun f) = ppCId f ppExpr d scope (EVar i) = ppCId (scope !! i) ppExpr d scope (ETyped e ty)= PP.char '<' PP.<> ppExpr 0 scope e PP.<+> PP.colon PP.<+> ppType 0 scope ty PP.<> PP.char '>' +ppExpr d scope (EImplArg e) = PP.braces (ppExpr 0 scope e) ppPatt :: Int -> [CId] -> Patt -> ([CId],PP.Doc) ppPatt d scope (PApp f ps) = let (scope',ds) = mapAccumL (ppPatt 2) scope ps @@ -210,6 +220,8 @@ ppPatt d scope (PApp f ps) = let (scope',ds) = mapAccumL (ppPatt 2) scope ps ppPatt d scope (PLit l) = (scope,ppLit l) ppPatt d scope (PVar f) = (f:scope,ppCId f) ppPatt d scope PWild = (scope,PP.char '_') +ppPatt d scope (PImplArg p) = let (scope',d) = ppPatt 0 scope p + in (scope',PP.braces d) ppBind Explicit x = ppCId x ppBind Implicit x = PP.braces (ppCId x) @@ -250,6 +262,7 @@ normalForm funs k env e = value2expr k (eval funs env e) value2expr i (VSusp j env vs k) = value2expr i (k (VGen j vs)) value2expr i (VLit l) = ELit l value2expr i (VClosure env (EAbs b x e)) = EAbs b x (value2expr (i+1) (eval funs ((VGen i []):env) e)) + value2expr i (VImplArg v) = EImplArg (value2expr i v) data Value = VApp CId [Value] @@ -258,6 +271,7 @@ data Value | VSusp {-# UNPACK #-} !MetaId Env [Value] (Value -> Value) | VGen {-# UNPACK #-} !Int [Value] | VClosure Env Expr + | VImplArg Value type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun type Env = [Value] @@ -276,6 +290,7 @@ eval funs env (EAbs b x e) = VClosure env (EAbs b x e) eval funs env (EMeta i) = VMeta i env [] eval funs env (ELit l) = VLit l eval funs env (ETyped e _) = eval funs env e +eval funs env (EImplArg e) = VImplArg (eval funs env e) apply :: Funs -> Env -> Expr -> [Value] -> Value apply funs env e [] = eval funs env e @@ -291,6 +306,7 @@ apply funs env (EAbs _ x e) (v:vs) = apply funs (v:env) e vs apply funs env (EMeta i) vs = VMeta i env vs apply funs env (ELit l) vs = error "literal of function type" apply funs env (ETyped e _) vs = apply funs env e vs +apply funs env (EImplArg _) vs = error "implicit argument in function position" applyValue funs v [] = v applyValue funs (VApp f vs0) vs = apply funs [] (EFun f) (vs0++vs) @@ -299,6 +315,7 @@ applyValue funs (VMeta i env vs0) vs = VMeta i env (vs0++vs) applyValue funs (VGen i vs0) vs = VGen i (vs0++vs) applyValue funs (VSusp i env vs0 k) vs = VSusp i env vs0 (\v -> applyValue funs (k v) vs) applyValue funs (VClosure env (EAbs b x e)) (v:vs) = apply funs (v:env) e vs +applyValue funs (VImplArg _) vs = error "implicit argument in function position" ----------------------------------------------------- -- Pattern matching @@ -320,5 +337,6 @@ match funs f eqs as0 vs0 = tryMatch (p ) (VSusp i envi vs k) env = VSusp i envi vs (\v -> tryMatch p (k v) env) tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env + tryMatch (PImplArg p ) (VImplArg v ) env = tryMatch p v env tryMatch _ _ env = match funs f eqs as0 vs0 diff --git a/src/PGF/Expr.hs-boot b/src/PGF/Expr.hs-boot index 075f7f44b..34a62a410 100644 --- a/src/PGF/Expr.hs-boot +++ b/src/PGF/Expr.hs-boot @@ -18,8 +18,8 @@ instance Ord BindType instance Show BindType -pFactor :: RP.ReadP Expr -pBinds :: RP.ReadP [(BindType,CId)] +pArg :: RP.ReadP Expr +pBinds :: RP.ReadP [(BindType,CId)] ppExpr :: Int -> [CId] -> Expr -> PP.Doc diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs index 2b6862bbf..02c8463e7 100644 --- a/src/PGF/Type.hs +++ b/src/PGF/Type.hs @@ -62,7 +62,7 @@ pType = do pAtom = do cat <- pCId RP.skipSpaces - args <- RP.sepBy pFactor RP.skipSpaces + args <- RP.sepBy pArg RP.skipSpaces return (cat, args) ppType :: Int -> [CId] -> Type -> PP.Doc diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs index bbd3ae126..937c21786 100644 --- a/src/PGF/TypeCheck.hs +++ b/src/PGF/TypeCheck.hs @@ -154,6 +154,7 @@ data TcError | NotFunType [CId] Expr Type -- ^ Something that is not of function type was applied to an argument. | CannotInferType [CId] Expr -- ^ It is not possible to infer the type of an expression. | UnresolvedMetaVars [CId] Expr [MetaId] -- ^ Some metavariables have to be instantiated in order to complete the typechecking. + | UnexpectedImplArg [CId] Expr -- ^ Implicit argument was passed where the type doesn't allow it -- | Renders the type checking error to a document. See 'Text.PrettyPrint'. ppTcError :: TcError -> Doc @@ -168,6 +169,7 @@ ppTcError (NotFunType xs e ty) = text "A function type is expected for t ppTcError (CannotInferType xs e) = text "Cannot infer the type of expression" <+> ppExpr 0 xs e ppTcError (UnresolvedMetaVars xs e ms) = text "Meta variable(s)" <+> fsep (List.map ppMeta ms) <+> text "should be resolved" $$ text "in the expression:" <+> ppExpr 0 xs e +ppTcError (UnexpectedImplArg xs e) = braces (ppExpr 0 xs e) <+> text "is implicit argument but not implicit argument is expected here" ----------------------------------------------------- -- checkType @@ -186,11 +188,9 @@ tcType scope ty@(DTyp hyps cat es) = do (scope,hyps) <- tcHypos scope hyps c_hyps <- lookupCatHyps cat let m = length es - n = length c_hyps - if m == n - then do (delta,es) <- tcHypoExprs scope [] (zip es c_hyps) - return (DTyp hyps cat es) - else tcError (WrongCatArgs (scopeVars scope) ty cat n m) + n = length [ty | (Explicit,x,ty) <- c_hyps] + (delta,es) <- tcCatArgs scope es [] c_hyps ty n m + return (DTyp hyps cat es) tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo]) tcHypos scope [] = return (scope,[]) @@ -206,21 +206,30 @@ tcHypo scope (b,x,ty) = do then return (scope,(b,x,ty)) else return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,(b,x,ty)) -tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr]) -tcHypoExprs scope delta [] = return (delta,[]) -tcHypoExprs scope delta ((e,h):xs) = do - (delta,e ) <- tcHypoExpr scope delta e h - (delta,es) <- tcHypoExprs scope delta xs +tcCatArgs scope [] delta [] ty0 n m = return (delta,[]) +tcCatArgs scope (EImplArg e:es) delta ((Explicit,x,ty):hs) ty0 n m = tcError (UnexpectedImplArg (scopeVars scope) e) +tcCatArgs scope (EImplArg e:es) delta ((Implicit,x,ty):hs) ty0 n m = do + e <- tcExpr scope e (TTyp delta ty) + funs <- getFuns + (delta,es) <- if x == wildCId + then tcCatArgs scope es delta hs ty0 n m + else tcCatArgs scope es (eval funs (scopeEnv scope) e:delta) hs ty0 n m + return (delta,EImplArg e:es) +tcCatArgs scope es delta ((Implicit,x,ty):hs) ty0 n m = do + i <- newMeta scope + (delta,es) <- if x == wildCId + then tcCatArgs scope es delta hs ty0 n m + else tcCatArgs scope es (VMeta i (scopeEnv scope) [] : delta) hs ty0 n m + return (delta,EImplArg (EMeta i) : es) +tcCatArgs scope (e:es) delta ((Explicit,x,ty):hs) ty0 n m = do + e <- tcExpr scope e (TTyp delta ty) + funs <- getFuns + (delta,es) <- if x == wildCId + then tcCatArgs scope es delta hs ty0 n m + else tcCatArgs scope es (eval funs (scopeEnv scope) e:delta) hs ty0 n m return (delta,e:es) - -tcHypoExpr :: Scope -> Env -> Expr -> Hypo -> TcM (Env,Expr) -tcHypoExpr scope delta e (b,x,ty) = do - e <- tcExpr scope e (TTyp delta ty) - funs <- getFuns - if x == wildCId - then return ( delta,e) - else return (eval funs (scopeEnv scope) e:delta,e) - +tcCatArgs scope _ delta _ ty0@(DTyp _ cat _) n m = do + tcError (WrongCatArgs (scopeVars scope) ty0 cat n m) ----------------------------------------------------- -- checkExpr @@ -237,16 +246,33 @@ checkExpr pgf e ty = Fail err -> Left err tcExpr :: Scope -> Expr -> TType -> TcM Expr -tcExpr scope e0@(EAbs b x e) tty = +tcExpr scope e0@(EAbs Implicit x e) tty = case tty of - TTyp delta (DTyp ((_,y,ty):hs) c es) -> do e <- if y == wildCId - then tcExpr (addScopedVar x (TTyp delta ty) scope) - e (TTyp delta (DTyp hs c es)) - else tcExpr (addScopedVar x (TTyp delta ty) scope) - e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)) - return (EAbs b x e) - _ -> do ty <- evalType (scopeSize scope) tty - tcError (NotFunType (scopeVars scope) e0 ty) + TTyp delta (DTyp ((Implicit,y,ty):hs) c es) -> do e <- if y == wildCId + then tcExpr (addScopedVar x (TTyp delta ty) scope) + e (TTyp delta (DTyp hs c es)) + else tcExpr (addScopedVar x (TTyp delta ty) scope) + e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)) + return (EAbs Implicit x e) + _ -> do ty <- evalType (scopeSize scope) tty + tcError (NotFunType (scopeVars scope) e0 ty) +tcExpr scope e0 (TTyp delta (DTyp ((Implicit,y,ty):hs) c es)) = do + e0 <- if y == wildCId + then tcExpr (addScopedVar wildCId (TTyp delta ty) scope) + e0 (TTyp delta (DTyp hs c es)) + else tcExpr (addScopedVar wildCId (TTyp delta ty) scope) + e0 (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)) + return (EAbs Implicit wildCId e0) +tcExpr scope e0@(EAbs Explicit x e) tty = + case tty of + TTyp delta (DTyp ((Explicit,y,ty):hs) c es) -> do e <- if y == wildCId + then tcExpr (addScopedVar x (TTyp delta ty) scope) + e (TTyp delta (DTyp hs c es)) + else tcExpr (addScopedVar x (TTyp delta ty) scope) + e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)) + return (EAbs Explicit x e) + _ -> do ty <- evalType (scopeSize scope) tty + tcError (NotFunType (scopeVars scope) e0 ty) tcExpr scope (EMeta _) tty = do i <- newMeta scope return (EMeta i) @@ -277,12 +303,9 @@ inferExpr pgf e = infExpr :: Scope -> Expr -> TcM (Expr,TType) infExpr scope e0@(EApp e1 e2) = do - (e1,tty1) <- infExpr scope e1 - case tty1 of - (TTyp delta1 (DTyp (h:hs) c es)) -> do (delta1,e2) <- tcHypoExpr scope delta1 e2 h - return (EApp e1 e2,TTyp delta1 (DTyp hs c es)) - _ -> do ty1 <- evalType (scopeSize scope) tty1 - tcError (NotFunType (scopeVars scope) e1 ty1) + (e1,TTyp delta ty) <- infExpr scope e1 + (e0,delta,ty) <- tcArg scope e1 e2 delta ty + return (e0,TTyp delta ty) infExpr scope e0@(EFun x) = do case lookupVar x scope of Just (i,tty) -> return (EVar i,tty) @@ -300,8 +323,33 @@ infExpr scope (ETyped e ty) = do ty <- tcType scope ty e <- tcExpr scope e (TTyp (scopeEnv scope) ty) return (ETyped e ty,TTyp (scopeEnv scope) ty) +infExpr scope (EImplArg e) = do + (e,tty) <- infExpr scope e + return (EImplArg e,tty) infExpr scope e = tcError (CannotInferType (scopeVars scope) e) +tcArg scope e1 e2 delta ty0@(DTyp [] c es) = do + ty1 <- evalType (scopeSize scope) (TTyp delta ty0) + tcError (NotFunType (scopeVars scope) e1 ty1) +tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = tcError (UnexpectedImplArg (scopeVars scope) e2) +tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do + e2 <- tcExpr scope e2 (TTyp delta ty) + funs <- getFuns + if x == wildCId + then return (EApp e1 (EImplArg e2), delta,DTyp hs c es) + else return (EApp e1 (EImplArg e2),eval funs (scopeEnv scope) e2:delta,DTyp hs c es) +tcArg scope e1 e2 delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = do + e2 <- tcExpr scope e2 (TTyp delta ty) + funs <- getFuns + if x == wildCId + then return (EApp e1 e2, delta,DTyp hs c es) + else return (EApp e1 e2,eval funs (scopeEnv scope) e2:delta,DTyp hs c es) +tcArg scope e1 e2 delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do + i <- newMeta scope + if x == wildCId + 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) + ----------------------------------------------------- -- eqType ----------------------------------------------------- @@ -461,6 +509,7 @@ refineExpr_ ms e = refine e refine (EFun f) = EFun f refine (EVar i) = EVar i refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty) + refine (EImplArg e) = EImplArg (refine e) refineType :: Type -> TcM Type refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty)) diff --git a/testsuite/runtime/typecheck/Graph.gf b/testsuite/runtime/typecheck/Graph.gf new file mode 100644 index 000000000..a44cf35b5 --- /dev/null +++ b/testsuite/runtime/typecheck/Graph.gf @@ -0,0 +1,19 @@ +abstract Graph = { + +cat + Node ; + Link (n,m : Node) ; + Path (n,m : Node) ; + Label ({n} : Node) ; -- just to debug implicit arguments of categories + +fun + n1,n2,n3,n4,n5 : Node ; + + l12 : Link n1 n2 ; + l23 : Link n2 n3 ; + l34 : Link n3 n4 ; + l35 : Link n3 n5 ; + + link : ({n,m} : Node) -> Link n m -> Path n m ; + join : ({n,p,m} : Node) -> Link n p -> Path p m -> Path n m ; +} \ No newline at end of file diff --git a/testsuite/runtime/typecheck/implicit-arguments.gfs b/testsuite/runtime/typecheck/implicit-arguments.gfs new file mode 100644 index 000000000..0306a662a --- /dev/null +++ b/testsuite/runtime/typecheck/implicit-arguments.gfs @@ -0,0 +1,9 @@ +i testsuite/runtime/typecheck/Graph.gf +ai join l12 (link l23) +ai join {n1} {n2} {n3} l12 (link {n2} {n3} l23) +ai +ai +ai +ai <\x -> x : ({m},n : Node) -> Node> +ai Node> +ai Node> \ No newline at end of file diff --git a/testsuite/runtime/typecheck/implicit-arguments.gfs.gold b/testsuite/runtime/typecheck/implicit-arguments.gfs.gold new file mode 100644 index 000000000..8a5c08461 --- /dev/null +++ b/testsuite/runtime/typecheck/implicit-arguments.gfs.gold @@ -0,0 +1,22 @@ +Expression: join {n1} {n2} {n3} l12 (link {n2} {n3} l23) +Type: Path n1 n3 + +Expression: join {n1} {n2} {n3} l12 (link {n2} {n3} l23) +Type: Path n1 n3 + +Expression: +Type: Label {?1} + +Expression: +Type: Label {n1} + +{n1} is implicit argument but not implicit argument is expected here +Expression: <\{_1}, x -> x : ({m} : Node) -> (n : Node) -> Node> +Type: ({m} : Node) -> (n : Node) -> Node + +Expression: <\{_1} -> n1 : ({m} : Node) -> Node> +Type: ({m} : Node) -> Node + +Expression: <\{_1} -> ?1 : ({m} : Node) -> Node> +Type: ({m} : Node) -> Node +