From 9e547710f57c5bd45fa459d6ae0cbc2c8ac4b8cc Mon Sep 17 00:00:00 2001 From: krasimir Date: Fri, 29 Jan 2010 21:10:14 +0000 Subject: [PATCH] bugfix in the PGF typechecker and more test cases --- src/compiler/GF/Command/Commands.hs | 2 +- src/compiler/GF/Compile/GrammarToPGF.hs | 6 ++-- src/compiler/GF/Compile/PGFtoJS.hs | 2 +- src/compiler/GF/Compile/PGFtoProlog.hs | 8 ++--- src/runtime/haskell/PGF.hs | 11 +++---- src/runtime/haskell/PGF/Check.hs | 2 +- src/runtime/haskell/PGF/Data.hs | 8 ++--- src/runtime/haskell/PGF/Expr.hs | 39 +++++++++++++++---------- src/runtime/haskell/PGF/Macros.hs | 6 ++-- src/runtime/haskell/PGF/Paraphrase.hs | 2 +- src/runtime/haskell/PGF/Printer.hs | 13 +++++---- src/runtime/haskell/PGF/TypeCheck.hs | 18 +++++++----- testsuite/runtime/eval/Test.gf | 3 ++ testsuite/runtime/eval/eval.gfs | 6 +++- testsuite/runtime/eval/eval.gfs.gold | 8 +++++ 15 files changed, 81 insertions(+), 53 deletions(-) diff --git a/src/compiler/GF/Command/Commands.hs b/src/compiler/GF/Command/Commands.hs index 1d3ccd833..27c4886c8 100644 --- a/src/compiler/GF/Command/Commands.hs +++ b/src/compiler/GF/Command/Commands.hs @@ -825,7 +825,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [ if null (functionsToCat pgf id) then empty else space $$ - vcat [ppFun fid (ty,0,[]) | (fid,ty) <- functionsToCat pgf id]) + vcat [ppFun fid (ty,0,Just []) | (fid,ty) <- functionsToCat pgf id]) Nothing -> do putStrLn ("unknown category of function identifier "++show id) return void [e] -> case inferExpr pgf e of diff --git a/src/compiler/GF/Compile/GrammarToPGF.hs b/src/compiler/GF/Compile/GrammarToPGF.hs index 2fe52f660..364b54bd3 100644 --- a/src/compiler/GF/Compile/GrammarToPGF.hs +++ b/src/compiler/GF/Compile/GrammarToPGF.hs @@ -60,9 +60,9 @@ canon2pgf opts pars cgr@(M.MGrammar ((a,abm):cms)) = do gflags = Map.empty aflags = Map.fromList [(mkCId f,C.LStr x) | (f,x) <- optionsPGF (M.flags abm)] - mkDef (Just eqs) = [C.Equ ps' (mkExp scope' e) | (ps,e) <- eqs, let (scope',ps') = mapAccumL mkPatt [] ps] - mkDef Nothing = [] - + mkDef (Just eqs) = Just [C.Equ ps' (mkExp scope' e) | (ps,e) <- eqs, let (scope',ps') = mapAccumL mkPatt [] ps] + mkDef Nothing = Nothing + mkArrity (Just a) = a mkArrity Nothing = 0 diff --git a/src/compiler/GF/Compile/PGFtoJS.hs b/src/compiler/GF/Compile/PGFtoJS.hs index 354720c9b..bb29ff7c5 100644 --- a/src/compiler/GF/Compile/PGFtoJS.hs +++ b/src/compiler/GF/Compile/PGFtoJS.hs @@ -34,7 +34,7 @@ pgf2js pgf = abstract2js :: String -> Abstr -> JS.Expr abstract2js start ds = new "GFAbstract" [JS.EStr start, JS.EObj $ map absdef2js (Map.assocs (funs ds))] -absdef2js :: (CId,(Type,Int,[Equation])) -> JS.Property +absdef2js :: (CId,(Type,Int,Maybe [Equation])) -> JS.Property absdef2js (f,(typ,_,_)) = let (args,cat) = M.catSkeleton typ in JS.Prop (JS.IdentPropName (JS.Ident (showCId f))) (new "Type" [JS.EArray [JS.EStr (showCId x) | x <- args], JS.EStr (showCId cat)]) diff --git a/src/compiler/GF/Compile/PGFtoProlog.hs b/src/compiler/GF/Compile/PGFtoProlog.hs index c55bf0522..896e18934 100644 --- a/src/compiler/GF/Compile/PGFtoProlog.hs +++ b/src/compiler/GF/Compile/PGFtoProlog.hs @@ -69,16 +69,16 @@ plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ) args = reverse [EFun x | (_,x) <- subst] typ = DTyp hypos' cat args -plFun :: (CId, (Type, Int, [Equation])) -> String +plFun :: (CId, (Type, Int, Maybe [Equation])) -> String 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), plList (map (\(_,x,ty) -> plOper ":" (plp x) (plp ty)) hypos)] -plFundef :: (CId, (Type,Int,[Equation])) -> [String] -plFundef (fun, (_,_,[])) = [] -plFundef (fun, (_,_,eqs)) = [plFact "def" [plp fun, plp fundef']] +plFundef :: (CId, (Type,Int,Maybe [Equation])) -> [String] +plFundef (fun, (_,_,Nothing )) = [] +plFundef (fun, (_,_,Just eqs)) = [plFact "def" [plp fun, plp fundef']] where fundef' = snd $ alphaConvert emptyEnv eqs diff --git a/src/runtime/haskell/PGF.hs b/src/runtime/haskell/PGF.hs index 9bc5c6567..2ca152db9 100644 --- a/src/runtime/haskell/PGF.hs +++ b/src/runtime/haskell/PGF.hs @@ -298,11 +298,12 @@ browse :: PGF -> CId -> Maybe (String,[CId],[CId]) browse pgf id = fmap (\def -> (def,producers,consumers)) definition where definition = case Map.lookup id (funs (abstract pgf)) of - Just (ty,_,eqs) -> Just $ render (text "fun" <+> ppCId id <+> colon <+> ppType 0 [] ty $$ - if null eqs - then empty - else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts - in ppCId id <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs]) + Just (ty,_,Just eqs) -> Just $ render (text "fun" <+> ppCId id <+> colon <+> ppType 0 [] ty $$ + if null eqs + then empty + else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts + in ppCId id <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs]) + Just (ty,_,Nothing ) -> Just $ render (text "data" <+> ppCId id <+> colon <+> ppType 0 [] ty) Nothing -> case Map.lookup id (cats (abstract pgf)) of Just hyps -> Just $ render (text "cat" <+> ppCId id <+> hsep (snd (mapAccumL ppHypo [] hyps))) Nothing -> Nothing diff --git a/src/runtime/haskell/PGF/Check.hs b/src/runtime/haskell/PGF/Check.hs index 6ac8c9b20..8f3b82eb7 100644 --- a/src/runtime/haskell/PGF/Check.hs +++ b/src/runtime/haskell/PGF/Check.hs @@ -38,7 +38,7 @@ checkConcrete pgf (lang,cnc) = checkl = checkLin pgf lang -} -type PGFSig = (Map.Map CId (Type,Int,[Equation]),Map.Map CId Term,Map.Map CId Term) +type PGFSig = (Map.Map CId (Type,Int,Maybe [Equation]),Map.Map CId Term,Map.Map CId Term) checkLin :: PGFSig -> CId -> (CId,Term) -> Err ((CId,Term),Bool) checkLin pgf lang (f,t) = diff --git a/src/runtime/haskell/PGF/Data.hs b/src/runtime/haskell/PGF/Data.hs index f2b4b913c..a23958d82 100644 --- a/src/runtime/haskell/PGF/Data.hs +++ b/src/runtime/haskell/PGF/Data.hs @@ -24,10 +24,10 @@ data PGF = PGF { } data Abstr = Abstr { - aflags :: Map.Map CId Literal, -- value of a flag - funs :: Map.Map CId (Type,Int,[Equation]), -- type, arrity and definition of function - cats :: Map.Map CId [Hypo], -- context of a cat - catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup) + aflags :: Map.Map CId Literal, -- value of a flag + funs :: Map.Map CId (Type,Int,Maybe [Equation]), -- type, arrity and definition of function + cats :: Map.Map CId [Hypo], -- context of a cat + catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup) } data Concr = Concr { diff --git a/src/runtime/haskell/PGF/Expr.hs b/src/runtime/haskell/PGF/Expr.hs index 674422217..19fc8f627 100644 --- a/src/runtime/haskell/PGF/Expr.hs +++ b/src/runtime/haskell/PGF/Expr.hs @@ -269,6 +269,7 @@ normalForm funs k env e = value2expr k (eval funs env e) 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 (VConst f vs) = foldl EApp (EFun f) (List.map (value2expr i) 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) @@ -279,20 +280,23 @@ data Value | VMeta {-# UNPACK #-} !MetaId Env [Value] | VSusp {-# UNPACK #-} !MetaId Env [Value] (Value -> Value) | VGen {-# UNPACK #-} !Int [Value] + | VConst CId [Value] | VClosure Env Expr | VImplArg Value -type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun +type Funs = Map.Map CId (Type,Int,Maybe [Equation]) -- type and def of a fun type Env = [Value] eval :: Funs -> Env -> Expr -> Value eval funs env (EVar i) = env !! i eval funs env (EFun f) = case Map.lookup f funs of - Just (_,a,eqs) -> if a == 0 - then case eqs of - Equ [] e : _ -> eval funs [] e - _ -> VApp f [] - else VApp f [] + Just (_,a,meqs) -> case meqs of + Just eqs -> if a == 0 + then case eqs of + Equ [] e : _ -> eval funs [] e + _ -> VConst f [] + else VApp f [] + Nothing -> 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 b x e) = VClosure env (EAbs b x e) @@ -305,10 +309,11 @@ apply :: Funs -> Env -> Expr -> [Value] -> Value apply funs env e [] = eval funs env e apply funs env (EVar i) vs = applyValue funs (env !! i) vs apply funs env (EFun f) vs = case Map.lookup f funs of - Just (_,a,eqs) -> if a <= length vs - then let (as,vs') = splitAt a vs - in match funs f eqs as vs' - else VApp f vs + Just (_,a,meqs) -> case meqs of + Just eqs -> if a <= length vs + then match funs f eqs vs + else VApp f vs + Nothing -> 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 @@ -323,6 +328,7 @@ applyValue funs (VLit _) vs = error "literal of function 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 (VConst f vs0) vs = VConst f (vs0++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" @@ -330,22 +336,23 @@ applyValue funs (VImplArg _) vs = error "implicit argument in -- Pattern matching ----------------------------------------------------- -match :: Funs -> CId -> [Equation] -> [Value] -> [Value] -> Value -match funs f eqs as0 vs0 = +match :: Funs -> CId -> [Equation] -> [Value] -> Value +match funs f eqs as0 = case eqs of - [] -> VApp f (as0++vs0) + [] -> VConst f as0 (Equ ps res):eqs -> tryMatches eqs ps as0 res [] where - tryMatches eqs [] [] res env = apply funs env res vs0 + tryMatches eqs [] as res env = apply funs env res as tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env where tryMatch (PVar x ) (v ) env = tryMatches eqs ps as res (v:env) tryMatch (PWild ) (_ ) env = tryMatches eqs ps as res env tryMatch (p ) (VMeta i envi vs ) env = VSusp i envi vs (\v -> tryMatch p v env) - tryMatch (p ) (VGen i vs ) env = VApp f (as0++vs0) + tryMatch (p ) (VGen i vs ) env = VConst f as0 tryMatch (p ) (VSusp i envi vs k) env = VSusp i envi vs (\v -> tryMatch p (k v) env) + tryMatch (p ) v@(VConst _ _ ) env = VConst f as0 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 + tryMatch _ _ env = match funs f eqs as0 diff --git a/src/runtime/haskell/PGF/Macros.hs b/src/runtime/haskell/PGF/Macros.hs index 03c5d0fe4..34f32c386 100644 --- a/src/runtime/haskell/PGF/Macros.hs +++ b/src/runtime/haskell/PGF/Macros.hs @@ -22,7 +22,7 @@ lookType pgf f = case lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf)) of (ty,_,_) -> ty -lookDef :: PGF -> CId -> [Equation] +lookDef :: PGF -> CId -> Maybe [Equation] lookDef pgf f = case lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf)) of (_,a,eqs) -> eqs @@ -30,8 +30,8 @@ lookDef pgf f = isData :: PGF -> CId -> Bool isData pgf f = case Map.lookup f (funs (abstract pgf)) of - Just (_,_,[]) -> True -- the encoding of data constrs - _ -> False + Just (_,_,Nothing) -> True -- the encoding of data constrs + _ -> False lookValCat :: PGF -> CId -> CId lookValCat pgf = valCat . lookType pgf diff --git a/src/runtime/haskell/PGF/Paraphrase.hs b/src/runtime/haskell/PGF/Paraphrase.hs index 58d15b2e8..3835b73c7 100644 --- a/src/runtime/haskell/PGF/Paraphrase.hs +++ b/src/runtime/haskell/PGF/Paraphrase.hs @@ -53,7 +53,7 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where isClosed d || (length equs == 1 && isLinear d)] equss = [(f,[(Fun f (map patt2tree ps), expr2tree d) | (Equ ps d) <- eqs]) | - (f,(_,_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)] + (f,(_,_,Just eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)] trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True diff --git a/src/runtime/haskell/PGF/Printer.hs b/src/runtime/haskell/PGF/Printer.hs index ee0fd4070..d458eb1a7 100644 --- a/src/runtime/haskell/PGF/Printer.hs +++ b/src/runtime/haskell/PGF/Printer.hs @@ -27,12 +27,13 @@ ppAbs name a = text "abstract" <+> ppCId name <+> char '{' $$ ppCat :: CId -> [Hypo] -> Doc ppCat c hyps = text "cat" <+> ppCId c <+> hsep (snd (mapAccumL ppHypo [] hyps)) -ppFun :: CId -> (Type,Int,[Equation]) -> Doc -ppFun f (t,_,eqs) = text "fun" <+> ppCId f <+> colon <+> ppType 0 [] t $$ - if null eqs - then empty - else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts - in ppCId f <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs] +ppFun :: CId -> (Type,Int,Maybe [Equation]) -> Doc +ppFun f (t,_,Just eqs) = text "fun" <+> ppCId f <+> colon <+> ppType 0 [] t $$ + if null eqs + then empty + else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts + in ppCId f <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs] +ppFun f (t,_,Nothing) = text "data" <+> ppCId f <+> colon <+> ppType 0 [] t ppCnc :: Language -> Concr -> Doc ppCnc name cnc = diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs index 937c21786..4e91827aa 100644 --- a/src/runtime/haskell/PGF/TypeCheck.hs +++ b/src/runtime/haskell/PGF/TypeCheck.hs @@ -409,12 +409,13 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 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 (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2 + eqValue' k (VConst f1 vs1) (VConst 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 v1 v2 = raiseTypeMatchError mkLam i scope env vs0 v = do let k = scopeSize scope @@ -452,6 +453,8 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 Just i -> do vs <- mapM (occurCheck i0 k xs) vs return (VGen i vs) Nothing -> raiseTypeMatchError + occurCheck i0 k xs (VConst f vs) = do vs <- mapM (occurCheck i0 k xs) vs + return (VConst f vs) occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env return (VClosure env e) @@ -516,9 +519,10 @@ 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 (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr sig i) vs) +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)) diff --git a/testsuite/runtime/eval/Test.gf b/testsuite/runtime/eval/Test.gf index a0131d767..748f974f9 100644 --- a/testsuite/runtime/eval/Test.gf +++ b/testsuite/runtime/eval/Test.gf @@ -22,6 +22,9 @@ cat Nat ; data zero : Nat ; succ : Nat -> Nat ; err : Nat ; + +fun zeroF : Nat ; + succF : Nat -> Nat ; fun dec : Nat -> Nat ; def dec zero = zero ; diff --git a/testsuite/runtime/eval/eval.gfs b/testsuite/runtime/eval/eval.gfs index 9317ce92a..b2e215a8e 100644 --- a/testsuite/runtime/eval/eval.gfs +++ b/testsuite/runtime/eval/eval.gfs @@ -20,6 +20,9 @@ pt -compute g0 23 pt -compute const 3.14 "pi" pt -compute dec (succ (succ zero)) pt -compute dec (succ ?) +pt -compute dec (succ zeroF) +pt -compute dec (succF zeroF) +pt -compute dec zeroF pt -compute <\x -> dec x : Nat -> Nat> pt -compute dec ? pt -compute <\f -> f 0 : (Int -> Int) -> Int> (g3 ?) @@ -27,4 +30,5 @@ pt -compute g (g2 ? 0) pt -compute plus (succ zero) (succ zero) pt -compute dec2 0 (succ zero) pt -compute dec2 0 err -pt -compute plus err (succ zero) \ No newline at end of file +pt -compute plus err (succ zero) +pt -compute <\x -> dec (dec x) : Nat -> Nat> \ No newline at end of file diff --git a/testsuite/runtime/eval/eval.gfs.gold b/testsuite/runtime/eval/eval.gfs.gold index 1c6282f27..665ee86fb 100644 --- a/testsuite/runtime/eval/eval.gfs.gold +++ b/testsuite/runtime/eval/eval.gfs.gold @@ -38,6 +38,12 @@ succ zero ?1 +zeroF + +dec (succF zeroF) + +dec zeroF + \x -> dec x dec ?1 @@ -54,3 +60,5 @@ dec2 0 err succ err +\x -> dec (dec x) +