From 1dfa67a30a6e15e8ac213a3fc967a3a740f170f5 Mon Sep 17 00:00:00 2001 From: krasimir Date: Sun, 20 Sep 2009 11:43:41 +0000 Subject: [PATCH] change the data types and the syntax in PGF to match the new syntax for implict arguments --- src/GF/Command/Interpreter.hs | 2 +- src/GF/Command/TreeOperations.hs | 2 +- src/GF/Compile/GFCCtoProlog.hs | 31 ++--- src/GF/Compile/GrammarToGFCC.hs | 6 +- src/PGF/Binary.hs | 17 ++- src/PGF/Expr.hs | 78 ++++++++---- src/PGF/Expr.hs-boot | 9 ++ src/PGF/Linearize.hs | 8 +- src/PGF/Macros.hs | 8 +- src/PGF/Parsing/FCFG/Incremental.hs | 2 +- src/PGF/Tree.hs | 52 +------- src/PGF/Type.hs | 33 +++-- src/PGF/TypeCheck.hs | 116 +++++++++--------- .../runtime/typecheck/typecheck.gfs.gold | 2 +- 14 files changed, 168 insertions(+), 198 deletions(-) diff --git a/src/GF/Command/Interpreter.hs b/src/GF/Command/Interpreter.hs index 17ff6aa29..ff84da8a3 100644 --- a/src/GF/Command/Interpreter.hs +++ b/src/GF/Command/Interpreter.hs @@ -74,7 +74,7 @@ appCommand xs c@(Command i os arg) = case arg of _ -> c where app e = case e of - EAbs x e -> EAbs x (app e) + EAbs b x e -> EAbs b x (app e) EApp e1 e2 -> EApp (app e1) (app e2) ELit l -> ELit l EMeta i -> xs !! i diff --git a/src/GF/Command/TreeOperations.hs b/src/GF/Command/TreeOperations.hs index 73cef05b2..941f03782 100644 --- a/src/GF/Command/TreeOperations.hs +++ b/src/GF/Command/TreeOperations.hs @@ -27,6 +27,6 @@ allTreeOps pgf = [ smallest :: [Expr] -> [Expr] smallest = sortBy (\t u -> compare (size t) (size u)) where size t = case t of - EAbs _ e -> size e + 1 + EAbs _ _ e -> size e + 1 EApp e1 e2 -> size e1 + size e2 + 1 _ -> 1 diff --git a/src/GF/Compile/GFCCtoProlog.hs b/src/GF/Compile/GFCCtoProlog.hs index a31fe4b84..702d4afe5 100644 --- a/src/GF/Compile/GFCCtoProlog.hs +++ b/src/GF/Compile/GFCCtoProlog.hs @@ -19,7 +19,7 @@ import GF.Text.UTF8 import qualified Data.Map as Map import Data.Char (isAlphaNum, isAsciiLower, isAsciiUpper, ord) -import Data.List (isPrefixOf) +import Data.List (isPrefixOf,mapAccumL) grammar2prolog, grammar2prolog_abs :: PGF -> String -- Most prologs have problems with UTF8 encodings, so we skip that: @@ -67,7 +67,7 @@ plAbstract (name, Abstr aflags funs cats _catfuns) = plCat :: (CId, [Hypo]) -> String plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ) - where ((_,subst), hypos') = alphaConvert emptyEnv hypos + where ((_,subst), hypos') = mapAccumL alphaConvertHypo emptyEnv hypos args = reverse [EFun x | (_,x) <- subst] typ = DTyp hypos' cat args @@ -76,7 +76,7 @@ plFun (fun, (typ,_,_)) = plFact "fun" (plp fun : plTypeWithHypos typ') where typ' = snd $ alphaConvert emptyEnv typ plTypeWithHypos :: Type -> [String] -plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plp hypos] +plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plList (map (\(_,x,ty) -> plOper ":" (plp x) (plp ty)) hypos)] plFundef :: (CId, (Type,Int,[Equation])) -> [String] plFundef (fun, (_,_,[])) = [] @@ -110,17 +110,12 @@ plConcrete (cncname, Concr cflags lins opers lincats lindefs instance PLPrint Type where plp (DTyp hypos cat args) | null hypos = result - | otherwise = plOper " -> " (plp hypos) result + | otherwise = plOper " -> " (plList (map (\(_,x,ty) -> plOper ":" (plp x) (plp ty)) hypos)) result where result = plTerm (plp cat) (map plp args) -instance PLPrint Hypo where - plp (Hyp typ) = plOper ":" (plp wildCId) (plp typ) - plp (HypI var typ) = plOper ":" (plp var) (plp typ) - plp (HypV var typ) = plOper ":" (plp var) (plp typ) - instance PLPrint Expr where plp (EFun x) = plp x - plp (EAbs x e) = plOper "^" (plp x) (plp e) + plp (EAbs _ x e)= plOper "^" (plp x) (plp e) plp (EApp e e') = plOper " * " (plp e) (plp e') plp (ELit lit) = plp lit plp (EMeta n) = "Meta_" ++ show n @@ -259,21 +254,15 @@ instance AlphaConvert a => AlphaConvert [a] where instance AlphaConvert Type where alphaConvert env@(_,subst) (DTyp hypos cat args) = ((ctr,subst), DTyp hypos' cat args') - where (env', hypos') = alphaConvert env hypos + where (env', hypos') = mapAccumL alphaConvertHypo env hypos ((ctr,_), args') = alphaConvert env' args -instance AlphaConvert Hypo where - alphaConvert env (Hyp typ) = ((ctr+1,subst), Hyp typ') - where ((ctr,subst), typ') = alphaConvert env typ - alphaConvert env (HypI x typ) = ((ctr+1,(x,x'):subst), HypI x' typ') - where ((ctr,subst), typ') = alphaConvert env typ - x' = createLogicalVariable ctr - alphaConvert env (HypV x typ) = ((ctr+1,(x,x'):subst), HypV x' typ') - where ((ctr,subst), typ') = alphaConvert env typ - x' = createLogicalVariable ctr +alphaConvertHypo env (b,x,typ) = ((ctr+1,(x,x'):subst), (b,x',typ')) + where ((ctr,subst), typ') = alphaConvert env typ + x' = createLogicalVariable ctr instance AlphaConvert Expr where - alphaConvert (ctr,subst) (EAbs x e) = ((ctr',subst), EAbs x' e') + alphaConvert (ctr,subst) (EAbs b x e) = ((ctr',subst), EAbs b x' e') where ((ctr',_), e') = alphaConvert (ctr+1,(x,x'):subst) e x' = createLogicalVariable ctr alphaConvert env (EApp e1 e2) = (env'', EApp e1' e2') diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs index b285faa81..a2b03ab63 100644 --- a/src/GF/Compile/GrammarToGFCC.hs +++ b/src/GF/Compile/GrammarToGFCC.hs @@ -129,7 +129,7 @@ mkExp :: [Ident] -> A.Term -> C.Expr mkExp scope t = case GM.termForm t of Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args)) where - mkAbs xs t = foldr (C.EAbs . i2i) t xs + mkAbs xs t = foldr (C.EAbs C.Explicit . i2i) t xs mkApp scope c args = case c of Q _ c -> foldl C.EApp (C.EFun (i2i c)) args QC _ c -> foldl C.EApp (C.EFun (i2i c)) args @@ -156,8 +156,8 @@ mkPatt scope p = mkContext :: [Ident] -> A.Context -> ([Ident],[C.Hypo]) mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty in if x == identW - then ( scope,C.Hyp ty') - else (x:scope,C.HypV (i2i x) ty')) scope hyps + then ( scope,(C.Explicit,i2i x,ty')) + else (x:scope,(C.Explicit,i2i x,ty'))) scope hyps mkTerm :: Term -> C.Term mkTerm tr = case tr of diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs index 87d61d1bc..e4ed98424 100644 --- a/src/PGF/Binary.hs +++ b/src/PGF/Binary.hs @@ -102,7 +102,7 @@ instance Binary Term where _ -> decodingError instance Binary Expr where - put (EAbs x exp) = putWord8 0 >> put (x,exp) + put (EAbs b x exp) = putWord8 0 >> put (b,x,exp) put (EApp e1 e2) = putWord8 1 >> put (e1,e2) put (ELit (LStr s)) = putWord8 2 >> put s put (ELit (LFlt d)) = putWord8 3 >> put d @@ -113,7 +113,7 @@ instance Binary Expr where put (ETyped e ty) = putWord8 8 >> put (e,ty) get = do tag <- getWord8 case tag of - 0 -> liftM2 EAbs get get + 0 -> liftM3 EAbs get get get 1 -> liftM2 EApp get get 2 -> liftM (ELit . LStr) get 3 -> liftM (ELit . LFlt) get @@ -149,15 +149,14 @@ instance Binary Type where put (DTyp hypos cat exps) = put (hypos,cat,exps) get = liftM3 DTyp get get get -instance Binary Hypo where - put (Hyp t) = putWord8 0 >> put t - put (HypV v t) = putWord8 1 >> put (v,t) - put (HypI v t) = putWord8 2 >> put (v,t) +instance Binary BindType where + put Explicit = putWord8 0 + put Implicit = putWord8 1 get = do tag <- getWord8 case tag of - 0 -> liftM Hyp get - 1 -> liftM2 HypV get get - 2 -> liftM2 HypI get get + 0 -> return Explicit + 1 -> return Implicit + _ -> decodingError instance Binary FFun where put (FFun fun prof lins) = put (fun,prof,lins) diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs index d3a5992bb..8a30a0988 100644 --- a/src/PGF/Expr.hs +++ b/src/PGF/Expr.hs @@ -1,5 +1,5 @@ -module PGF.Expr(Tree, Expr(..), Literal(..), Patt(..), Equation(..), - readExpr, showExpr, pExpr, ppExpr, ppPatt, +module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..), + readExpr, showExpr, pExpr, pBinds, ppExpr, ppPatt, mkApp, unApp, mkStr, unStr, @@ -36,6 +36,11 @@ data Literal = type MetaId = Int +data BindType = + Explicit + | Implicit + deriving (Eq,Ord,Show) + -- | Tree is the abstract syntax representation of a given sentence -- in some concrete syntax. Technically 'Tree' is a type synonym -- of 'Expr'. @@ -45,7 +50,7 @@ type Tree = Expr -- both parameter of a dependent type or an abstract syntax tree for -- for some sentence. data Expr = - EAbs CId Expr -- ^ lambda abstraction + EAbs BindType CId Expr -- ^ lambda abstraction | EApp Expr Expr -- ^ application | ELit Literal -- ^ literal | EMeta {-# UNPACK #-} !MetaId -- ^ meta variable @@ -131,10 +136,24 @@ pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm) where pTerm = fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces) - pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')) + pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") pBinds e <- pExpr - return (foldr EAbs e xs) - + return (foldr (\(b,x) e -> EAbs b x e) e xs) + +pBinds :: RP.ReadP [(BindType,CId)] +pBinds = do xss <- RP.sepBy1 (RP.skipSpaces >> pBind) (RP.skipSpaces >> RP.char ',') + return (concat xss) + where + pCIdOrWild = pCId `mplus` (RP.char '_' >> return wildCId) + + pBind = + do x <- pCIdOrWild + return [(Explicit,x)] + `mplus` + RP.between (RP.char '{') + (RP.skipSpaces >> RP.char '}') + (RP.sepBy1 (RP.skipSpaces >> pCIdOrWild >>= \id -> return (Implicit,id)) (RP.skipSpaces >> RP.char ',')) + pFactor = fmap EFun pCId RP.<++ fmap ELit pLit RP.<++ fmap EMeta pMeta @@ -170,14 +189,14 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"')) ----------------------------------------------------- ppExpr :: Int -> [CId] -> Expr -> PP.Doc -ppExpr d scope (EAbs x e) = let (xs,e1) = getVars [x] e +ppExpr d scope (EAbs b x e) = let (bs,xs,e1) = getVars [] [] (EAbs b x e) in ppParens (d > 1) (PP.char '\\' PP.<> - PP.hsep (PP.punctuate PP.comma (List.map ppCId (reverse xs))) PP.<+> + PP.hsep (PP.punctuate PP.comma (reverse (List.zipWith ppBind bs xs))) PP.<+> PP.text "->" PP.<+> ppExpr 1 (xs++scope) e1) where - getVars xs (EAbs x e) = getVars (freshName x xs:xs) e - getVars xs e = (xs,e) + getVars bs xs (EAbs b x e) = getVars (b:bs) ((freshName x xs):xs) e + getVars bs xs e = (bs,xs,e) ppExpr d scope (EApp e1 e2) = ppParens (d > 3) ((ppExpr 3 scope e1) PP.<+> (ppExpr 4 scope e2)) ppExpr d scope (ELit l) = ppLit l ppExpr d scope (EMeta n) = ppMeta n @@ -192,6 +211,9 @@ ppPatt d scope (PLit l) = (scope,ppLit l) ppPatt d scope (PVar f) = (f:scope,ppCId f) ppPatt d scope PWild = (scope,PP.char '_') +ppBind Explicit x = ppCId x +ppBind Implicit x = PP.braces (ppCId x) + ppLit (LStr s) = PP.text (show s) ppLit (LInt n) = PP.integer n ppLit (LFlt d) = PP.double d @@ -205,10 +227,12 @@ ppParens True = PP.parens ppParens False = id freshName :: CId -> [CId] -> CId -freshName x xs = loop 1 x +freshName x xs0 = loop 1 x where + xs = wildCId : xs0 + loop i y - | elem y xs = loop (i+1) (mkCId (show x++"'"++show i)) + | elem y xs = loop (i+1) (mkCId (show x++show i)) | otherwise = y @@ -220,12 +244,12 @@ freshName x xs = loop 1 x normalForm :: Funs -> Int -> Env -> Expr -> Expr normalForm funs k env e = value2expr k (eval funs env e) where - value2expr i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr i) vs) - value2expr i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr i) vs) - value2expr i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr i) vs) - value2expr i (VSusp j env vs k) = value2expr i (k (VGen j vs)) - value2expr i (VLit l) = ELit l - value2expr i (VClosure env (EAbs x e)) = EAbs x (value2expr (i+1) (eval funs ((VGen i []):env) e)) + value2expr i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr i) vs) + value2expr i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr i) vs) + value2expr i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr i) vs) + 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)) data Value = VApp CId [Value] @@ -248,7 +272,7 @@ eval funs env (EFun f) = case Map.lookup f funs of else VApp f [] Nothing -> error ("unknown function "++showCId f) eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2] -eval funs env (EAbs x e) = VClosure env (EAbs x e) +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 @@ -263,18 +287,18 @@ apply funs env (EFun f) vs = case Map.lookup f funs of else VApp f vs Nothing -> error ("unknown function "++showCId f) apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs) -apply funs env (EAbs x e) (v:vs) = apply funs (v:env) e vs +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 -applyValue funs v [] = v -applyValue funs (VApp f vs0) vs = apply funs [] (EFun f) (vs0++vs) -applyValue funs (VLit _) vs = error "literal of function type" -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 x e)) (v:vs) = apply funs (v:env) e vs +applyValue funs v [] = v +applyValue funs (VApp f vs0) vs = apply funs [] (EFun f) (vs0++vs) +applyValue funs (VLit _) vs = error "literal of function type" +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 ----------------------------------------------------- -- Pattern matching diff --git a/src/PGF/Expr.hs-boot b/src/PGF/Expr.hs-boot index 533feea75..075f7f44b 100644 --- a/src/PGF/Expr.hs-boot +++ b/src/PGF/Expr.hs-boot @@ -10,7 +10,16 @@ instance Eq Expr instance Ord Expr instance Show Expr + +data BindType = Explicit | Implicit + +instance Eq BindType +instance Ord BindType +instance Show BindType + + pFactor :: RP.ReadP Expr +pBinds :: RP.ReadP [(BindType,CId)] ppExpr :: Int -> [CId] -> Expr -> PP.Doc diff --git a/src/PGF/Linearize.hs b/src/PGF/Linearize.hs index 418ed9d5a..f733c8cb1 100644 --- a/src/PGF/Linearize.hs +++ b/src/PGF/Linearize.hs @@ -59,8 +59,8 @@ linTree :: PGF -> CId -> Expr -> Term linTree pgf lang = lin . expr2tree where lin (Abs xs e ) = case lin e of - R ts -> R $ ts ++ (Data.List.map (kks . showCId) xs) - TM s -> R $ (TM s) : (Data.List.map (kks . showCId) xs) + R ts -> R $ ts ++ (Data.List.map (kks . showCId . snd) xs) + TM s -> R $ (TM s) : (Data.List.map (kks . showCId . snd) xs) lin (Fun fun es) = let argVariants = mapM (liftVariants . lin) es in variants [compute pgf lang args $ look fun | args <- argVariants] lin (Lit (LStr s)) = R [kks (show s)] -- quoted @@ -130,8 +130,8 @@ linTreeMark :: PGF -> CId -> Expr -> Term linTreeMark pgf lang = lin [] . expr2tree where lin p (Abs xs e ) = case lin p e of - R ts -> R $ ts ++ (Data.List.map (kks . showCId) xs) - TM s -> R $ (TM s) : (Data.List.map (kks . showCId) xs) + R ts -> R $ ts ++ (Data.List.map (kks . showCId . snd) xs) + TM s -> R $ (TM s) : (Data.List.map (kks . showCId . snd) xs) lin p (Fun fun es) = let argVariants = mapM (\ (i,e) -> liftVariants $ lin (sub p i) e) (zip [0..] es) in variants [mark p $ compute pgf lang args $ look fun | args <- argVariants] diff --git a/src/PGF/Macros.hs b/src/PGF/Macros.hs index 05980d823..604f3c35d 100644 --- a/src/PGF/Macros.hs +++ b/src/PGF/Macros.hs @@ -100,17 +100,15 @@ restrictPGF cond pgf = pgf { abstr = abstract pgf depth :: Expr -> Int -depth (EAbs _ t) = depth t +depth (EAbs _ _ t) = depth t depth (EApp e1 e2) = max (depth e1) (depth e2) + 1 depth _ = 1 cftype :: [CId] -> CId -> Type -cftype args val = DTyp [Hyp (cftype [] arg) | arg <- args] val [] +cftype args val = DTyp [(Explicit,wildCId,cftype [] arg) | arg <- args] val [] typeOfHypo :: Hypo -> Type -typeOfHypo (Hyp ty) = ty -typeOfHypo (HypV _ ty) = ty -typeOfHypo (HypI _ ty) = ty +typeOfHypo (_,_,ty) = ty catSkeleton :: Type -> ([CId],CId) catSkeleton ty = case ty of diff --git a/src/PGF/Parsing/FCFG/Incremental.hs b/src/PGF/Parsing/FCFG/Incremental.hs index cae0ad80f..6ae18e3bf 100644 --- a/src/PGF/Parsing/FCFG/Incremental.hs +++ b/src/PGF/Parsing/FCFG/Incremental.hs @@ -134,7 +134,7 @@ extractTrees (State pgf pinfo chart items) ty@(DTyp _ start _) = check_ho_fun fun args | fun == _V = return (head args) - | fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs (mkVar (snd x)) e) (snd (head args)) (tail args)) + | fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs Explicit (mkVar (snd x)) e) (snd (head args)) (tail args)) | otherwise = return (Set.unions (map fst args),foldl (\e x -> EApp e (snd x)) (EFun fun) args) mkVar (EFun v) = v diff --git a/src/PGF/Tree.hs b/src/PGF/Tree.hs index c2d2f33f5..cf01b4470 100644 --- a/src/PGF/Tree.hs +++ b/src/PGF/Tree.hs @@ -1,6 +1,5 @@ module PGF.Tree ( Tree(..), - readTree, showTree, pTree, ppTree, tree2expr, expr2tree ) where @@ -18,54 +17,13 @@ import qualified Text.ParserCombinators.ReadP as RP -- allow unapplied lambda abstractions. The tree is used directly -- from the linearizer and is produced directly from the parser. data Tree = - Abs [CId] Tree -- ^ lambda abstraction. The list of variables is non-empty + Abs [(BindType,CId)] Tree -- ^ lambda abstraction. The list of variables is non-empty | Var CId -- ^ variable | Fun CId [Tree] -- ^ function application | Lit Literal -- ^ literal | Meta {-# UNPACK #-} !MetaId -- ^ meta variable deriving (Eq, Ord) --- | parses 'String' as an expression -readTree :: String -> Maybe Tree -readTree s = case [x | (x,cs) <- RP.readP_to_S (pTree False) s, all isSpace cs] of - [x] -> Just x - _ -> Nothing - --- | renders expression as 'String' -showTree :: Tree -> String -showTree = PP.render . ppTree 0 - -instance Show Tree where - showsPrec i x = showString (PP.render (ppTree i x)) - -instance Read Tree where - readsPrec _ = RP.readP_to_S (pTree False) - -pTrees :: RP.ReadP [Tree] -pTrees = liftM2 (:) (pTree True) pTrees RP.<++ (RP.skipSpaces >> return []) - -pTree :: Bool -> RP.ReadP Tree -pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Lit pLit RP.<++ fmap Meta pMeta) - where - pParen = RP.between (RP.char '(') (RP.char ')') (pTree False) - pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')) - t <- pTree False - return (Abs xs t) - pApp = do f <- pCId - ts <- (if isNested then return [] else pTrees) - return (Fun f ts) - -ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<> - PP.hsep (PP.punctuate PP.comma (List.map ppCId xs)) PP.<+> - PP.text "->" PP.<+> - ppTree 0 t) -ppTree d (Fun f []) = ppCId f -ppTree d (Fun f ts) = ppParens (d > 0) (ppCId f PP.<+> PP.hsep (List.map (ppTree 1) ts)) -ppTree d (Lit l) = ppLit l -ppTree d (Meta n) = ppMeta n -ppTree d (Var id) = ppCId id - - ----------------------------------------------------- -- Conversion Expr <-> Tree ----------------------------------------------------- @@ -78,7 +36,7 @@ tree2expr = tree2expr [] tree2expr ys (Fun x ts) = foldl EApp (EFun x) (List.map (tree2expr ys) ts) tree2expr ys (Lit l) = ELit l tree2expr ys (Meta n) = EMeta n - tree2expr ys (Abs xs t) = foldr EAbs (tree2expr (reverse xs++ys) t) xs + tree2expr ys (Abs xs t) = foldr (\(b,x) e -> EAbs b x e) (tree2expr (List.map snd (reverse xs)++ys) t) xs tree2expr ys (Var x) = case List.lookup x (zip ys [0..]) of Just i -> EVar i Nothing -> error "unknown variable" @@ -88,11 +46,11 @@ tree2expr = tree2expr [] expr2tree :: Expr -> Tree expr2tree e = abs [] [] e where - abs ys xs (EAbs x e) = abs ys (x:xs) e + abs ys xs (EAbs b x e) = abs ys ((b,x):xs) e abs ys xs (ETyped e _) = abs ys xs e abs ys xs e = case xs of [] -> app ys [] e - xs -> Abs (reverse xs) (app (xs++ys) [] e) + xs -> Abs (reverse xs) (app (map snd xs++ys) [] e) app xs as (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1 app xs as (ELit l) @@ -101,7 +59,7 @@ expr2tree e = abs [] [] e app xs as (EMeta n) | List.null as = Meta n | otherwise = error "meta variables of function type are not allowed in trees" - app xs as (EAbs x e) = error "beta redexes are not allowed in trees" + app xs as (EAbs _ x e) = error "beta redexes are not allowed in trees" app xs as (EVar i) = Var (xs !! i) app xs as (EFun f) = Fun f as app xs as (ETyped e _) = app xs as e diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs index dbd52343b..2b6862bbf 100644 --- a/src/PGF/Type.hs +++ b/src/PGF/Type.hs @@ -1,4 +1,4 @@ -module PGF.Type ( Type(..), Hypo(..), +module PGF.Type ( Type(..), Hypo, readType, showType, pType, ppType, ppHypo ) where @@ -16,11 +16,7 @@ data Type = deriving (Eq,Ord,Show) -- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis -data Hypo = - Hyp Type -- ^ hypothesis without bound variable like in A -> B - | HypV CId Type -- ^ hypothesis with bound variable like in (x : A) -> B x - | HypI CId Type -- ^ hypothesis with bound implicit variable like in {x : A} -> B x - deriving (Eq,Ord,Show) +type Hypo = (BindType,CId,Type) -- | Reads a 'Type' from a 'String'. readType :: String -> Maybe Type @@ -45,23 +41,23 @@ pType = do where pHypo = do (cat,args) <- pAtom - return [Hyp (DTyp [] cat args)] + return [(Explicit,wildCId,DTyp [] cat args)] RP.<++ (RP.between (RP.char '(') (RP.char ')') $ do - hyp <- RP.option (\ty -> [Hyp ty]) $ do - vs <- RP.sepBy (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',') + xs <- RP.option [(Explicit,wildCId)] $ do + xs <- pBinds RP.skipSpaces RP.char ':' - return (\ty -> [HypV v ty | v <- vs]) + return xs ty <- pType - return (hyp ty)) + return [(b,v,ty) | (b,v) <- xs]) RP.<++ (RP.between (RP.char '{') (RP.char '}') $ do vs <- RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',') RP.skipSpaces RP.char ':' ty <- pType - return [HypI v ty | v <- vs]) + return [(Implicit,v,ty) | v <- vs]) pAtom = do cat <- pCId @@ -77,8 +73,11 @@ ppType d scope (DTyp hyps cat args) where ppRes scope cat es = ppCId cat PP.<+> PP.hsep (map (ppExpr 4 scope) es) -ppHypo scope (Hyp typ) = ( scope,ppType 1 scope typ) -ppHypo scope (HypV x typ) = let y = freshName x scope - in (y:scope,PP.parens (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ)) -ppHypo scope (HypI x typ) = let y = freshName x scope - in (y:scope,PP.braces (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ)) +ppHypo scope (Explicit,x,typ) = if x == wildCId + then (scope,ppType 1 scope typ) + else let y = freshName x scope + in (y:scope,PP.parens (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ)) +ppHypo scope (Implicit,x,typ) = if x == wildCId + then (scope,PP.parens (PP.braces (ppCId x) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ)) + else let y = freshName x scope + in (y:scope,PP.parens (PP.braces (ppCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ)) diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs index 2683588d4..bbd3ae126 100644 --- a/src/PGF/TypeCheck.hs +++ b/src/PGF/TypeCheck.hs @@ -200,12 +200,11 @@ tcHypos scope (h:hs) = do return (scope,h:hs) tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo) -tcHypo scope (Hyp ty) = do +tcHypo scope (b,x,ty) = do ty <- tcType scope ty - return (scope,Hyp ty) -tcHypo scope (HypV x ty) = do - ty <- tcType scope ty - return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,HypV x ty) + if x == wildCId + 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,[]) @@ -215,13 +214,12 @@ tcHypoExprs scope delta ((e,h):xs) = do return (delta,e:es) tcHypoExpr :: Scope -> Env -> Expr -> Hypo -> TcM (Env,Expr) -tcHypoExpr scope delta e (Hyp ty) = do - e <- tcExpr scope e (TTyp delta ty) - return (delta,e) -tcHypoExpr scope delta e (HypV x ty) = do - e <- tcExpr scope e (TTyp delta ty) - funs <- getFuns - return (eval funs (scopeEnv scope) e:delta,e) +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) ----------------------------------------------------- @@ -239,16 +237,16 @@ checkExpr pgf e ty = Fail err -> Left err tcExpr :: Scope -> Expr -> TType -> TcM Expr -tcExpr scope e0@(EAbs x e) tty = +tcExpr scope e0@(EAbs b x e) tty = case tty of - TTyp delta (DTyp (h:hs) c es) -> do e <- case h of - Hyp ty -> tcExpr (addScopedVar x (TTyp delta ty) scope) - e (TTyp delta (DTyp hs c es)) - HypV y ty -> tcExpr (addScopedVar x (TTyp delta ty) scope) - e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)) - return (EAbs x e) - _ -> do ty <- evalType (scopeSize scope) tty - tcError (NotFunType (scopeVars scope) e0 ty) + 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) tcExpr scope (EMeta _) tty = do i <- newMeta scope return (EMeta i) @@ -322,14 +320,13 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env) eqHyps k delta1 [] delta2 [] = return (k,delta1,delta2) - eqHyps k delta1 (Hyp ty1 : h1s) delta2 (Hyp ty2 : h2s) = do + eqHyps k delta1 ((_,x,ty1) : h1s) delta2 ((_,y,ty2) : h2s) = do eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2) - (k,delta1,delta2) <- eqHyps k delta1 h1s delta2 h2s - return (k,delta1,delta2) - eqHyps k delta1 (HypV x ty1 : h1s) delta2 (HypV y ty2 : h2s) = do - eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2) - (k,delta1,delta2) <- eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s - return (k,delta1,delta2) + if x == wildCId && y == wildCId + then eqHyps k delta1 h1s delta2 h2s + else if x /= wildCId && y /= wildCId + then eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s + else raiseTypeMatchError eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM () @@ -353,23 +350,23 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 MUnbound _ _ -> return v deRef v = return v - eqValue' k (VSusp i env vs1 c) v2 = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2) - eqValue' k v1 (VSusp i env vs2 c) = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2)) - eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2 - eqValue' k (VMeta i env1 vs1) v2 = do (MUnbound scopei cs) <- getMeta i - e2 <- mkLam i scopei env1 vs1 v2 - setMeta i (MBound e2) - sequence_ [c e2 | c <- cs] - eqValue' k v1 (VMeta i env2 vs2) = do (MUnbound scopei cs) <- getMeta i - e1 <- mkLam i scopei env2 vs2 v1 - setMeta i (MBound e1) - sequence_ [c e1 | c <- cs] - eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2 - eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return () - eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2 - eqValue' k (VClosure env1 (EAbs x1 e1)) (VClosure env2 (EAbs x2 e2)) = let v = VGen k [] - in eqExpr (k+1) (v:env1) e1 (v:env2) e2 - eqValue' k v1 v2 = raiseTypeMatchError + eqValue' k (VSusp i env vs1 c) v2 = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2) + eqValue' k v1 (VSusp i env vs2 c) = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2)) + eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2 + eqValue' k (VMeta i env1 vs1) v2 = do (MUnbound scopei cs) <- getMeta i + e2 <- mkLam i scopei env1 vs1 v2 + setMeta i (MBound e2) + sequence_ [c e2 | c <- cs] + eqValue' k v1 (VMeta i env2 vs2) = do (MUnbound scopei cs) <- getMeta i + e1 <- mkLam i scopei env2 vs2 v1 + setMeta i (MBound e1) + sequence_ [c e1 | c <- cs] + eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2 + eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return () + eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2 + eqValue' k (VClosure env1 (EAbs _ x1 e1)) (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k [] + in eqExpr (k+1) (v:env1) e1 (v:env2) e2 + eqValue' k v1 v2 = raiseTypeMatchError mkLam i scope env vs0 v = do let k = scopeSize scope @@ -383,7 +380,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 return (addLam vs0 (value2expr funs (length xs) v)) where addLam [] e = e - addLam (v:vs) e = EAbs var (addLam vs e) + addLam (v:vs) e = EAbs Explicit var (addLam vs e) var = mkCId "v" @@ -439,9 +436,10 @@ evalType k (TTyp delta ty) = do funs <- getFuns 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) (Hyp ty) = ((k, delta),Hyp (evalTy sig k delta ty)) - evalHypo sig (k,delta) (HypV x ty) = ((k+1,(VGen k []):delta),HypV x (evalTy sig k delta ty)) - evalHypo sig (k,delta) (HypI x ty) = ((k+1,(VGen k []):delta),HypI x (evalTy sig k delta ty)) + 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)) ----------------------------------------------------- @@ -453,7 +451,7 @@ refineExpr e = TcM (\abstr metaid ms -> Ok metaid ms (refineExpr_ ms e)) refineExpr_ ms e = refine e where - refine (EAbs x e) = EAbs x (refine e) + refine (EAbs b x e) = EAbs b x (refine e) refine (EApp e1 e2) = EApp (refine e1) (refine e2) refine (ELit l) = ELit l refine (EMeta i) = case IntMap.lookup i ms of @@ -467,15 +465,11 @@ refineExpr_ ms e = refine e refineType :: Type -> TcM Type refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty)) -refineType_ ms (DTyp hyps cat es) = DTyp (List.map (refineHypo_ ms) hyps) cat (List.map (refineExpr_ ms) es) +refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es) -refineHypo_ ms (Hyp ty) = Hyp (refineType_ ms ty) -refineHypo_ ms (HypV x ty) = HypV x (refineType_ ms ty) -refineHypo_ ms (HypI x ty) = HypI x (refineType_ ms ty) - -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 (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 x e)) = EAbs x (value2expr sig (i+1) (eval sig ((VGen i []):env) e)) +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 (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)) diff --git a/testsuite/runtime/typecheck/typecheck.gfs.gold b/testsuite/runtime/typecheck/typecheck.gfs.gold index 5e27e1482..a43a0c216 100644 --- a/testsuite/runtime/typecheck/typecheck.gfs.gold +++ b/testsuite/runtime/typecheck/typecheck.gfs.gold @@ -30,7 +30,7 @@ In the expression: mkMorph (\x -> succ zero) Expression: Vector (succ zero) -> Vector (succ zero)> Type: Vector zero -> Vector (succ zero) -> Vector (succ zero) -Expression: <\n, v1, n'1, v2 -> append n n'1 v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)> +Expression: <\n, v1, n1, v2 -> append n n1 v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)> Type: (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m) Category EQ is not in scope