msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

bugfix in the PGF typechecker and more test cases

Browse Source
This commit is contained in:
krasimir
2010-01-29 21:10:14 +00:00
parent e5de8ea9fe
commit 3b7e39fa4a
15 changed files with 81 additions and 53 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/compiler/GF/Command/Commands.hs
View File

@@ -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

6
src/compiler/GF/Compile/GrammarToPGF.hs
View File

@@ -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

2
src/compiler/GF/Compile/PGFtoJS.hs
View File

@@ -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)])

8
src/compiler/GF/Compile/PGFtoProlog.hs
View File

@@ -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

11
src/runtime/haskell/PGF.hs
View File

@@ -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

2
src/runtime/haskell/PGF/Check.hs
View File

@@ -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) =

8
src/runtime/haskell/PGF/Data.hs
View File

@@ -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 {

39
src/runtime/haskell/PGF/Expr.hs
View File

@@ -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

6
src/runtime/haskell/PGF/Macros.hs
View File

@@ -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

2
src/runtime/haskell/PGF/Paraphrase.hs
View File

@@ -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

13
src/runtime/haskell/PGF/Printer.hs
View File

@@ -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 =

18
src/runtime/haskell/PGF/TypeCheck.hs
View File

@@ -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))

3
testsuite/runtime/eval/Test.gf
View File

@@ -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 ;

6
testsuite/runtime/eval/eval.gfs
View File

@@ -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)
pt -compute plus err (succ zero)
pt -compute <\x -> dec (dec x) : Nat -> Nat>

8
testsuite/runtime/eval/eval.gfs.gold
View File

@@ -38,6 +38,12 @@ succ zero
\x -> g x
g ?1
5
@@ -54,3 +60,5 @@ dec2 0 err
f 32