summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/GF/Grammar/Grammar.hs3
-rw-r--r--src/GF/Grammar/Parser.y12
-rw-r--r--src/PGF/Expr.hs24
-rw-r--r--src/PGF/Expr.hs-boot4
-rw-r--r--src/PGF/Type.hs2
-rw-r--r--src/PGF/TypeCheck.hs117
6 files changed, 118 insertions, 44 deletions
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 ((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 ((_,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 ((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))
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 06:34:06 +0000