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

change the data types and the syntax in PGF to match the new syntax for implict arguments

Browse Source
This commit is contained in:
krasimir
2009-09-20 11:43:41 +00:00
parent d09371280d
commit b1a51f46f5
14 changed files with 168 additions and 198 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/GF/Command/Interpreter.hs
View File

@@ -74,7 +74,7 @@ appCommand xs c@(Command i os arg) = case arg of
_ -> c _ -> c
where where
app e = case e of 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) EApp e1 e2 -> EApp (app e1) (app e2)
ELit l -> ELit l ELit l -> ELit l
EMeta i -> xs !! i EMeta i -> xs !! i

2
src/GF/Command/TreeOperations.hs
View File

@@ -27,6 +27,6 @@ allTreeOps pgf = [
smallest :: [Expr] -> [Expr] smallest :: [Expr] -> [Expr]
smallest = sortBy (\t u -> compare (size t) (size u)) where smallest = sortBy (\t u -> compare (size t) (size u)) where
size t = case t of size t = case t of
EAbs _ e -> size e + 1 EAbs _ _ e -> size e + 1
EApp e1 e2 -> size e1 + size e2 + 1 EApp e1 e2 -> size e1 + size e2 + 1
_ -> 1 _ -> 1

31
src/GF/Compile/GFCCtoProlog.hs
View File

@@ -19,7 +19,7 @@ import GF.Text.UTF8
import qualified Data.Map as Map import qualified Data.Map as Map
import Data.Char (isAlphaNum, isAsciiLower, isAsciiUpper, ord) import Data.Char (isAlphaNum, isAsciiLower, isAsciiUpper, ord)
import Data.List (isPrefixOf) import Data.List (isPrefixOf,mapAccumL)
grammar2prolog, grammar2prolog_abs :: PGF -> String grammar2prolog, grammar2prolog_abs :: PGF -> String
-- Most prologs have problems with UTF8 encodings, so we skip that: -- 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 :: (CId, [Hypo]) -> String
plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ) 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] args = reverse [EFun x | (_,x) <- subst]
typ = DTyp hypos' cat args typ = DTyp hypos' cat args
@@ -76,7 +76,7 @@ plFun (fun, (typ,_,_)) = plFact "fun" (plp fun : plTypeWithHypos typ')
where typ' = snd $ alphaConvert emptyEnv typ where typ' = snd $ alphaConvert emptyEnv typ
plTypeWithHypos :: Type -> [String] 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 :: (CId, (Type,Int,[Equation])) -> [String]
plFundef (fun, (_,_,[])) = [] plFundef (fun, (_,_,[])) = []
@@ -110,17 +110,12 @@ plConcrete (cncname, Concr cflags lins opers lincats lindefs
instance PLPrint Type where instance PLPrint Type where
plp (DTyp hypos cat args) | null hypos = result 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) 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 instance PLPrint Expr where
plp (EFun x) = plp x 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 (EApp e e') = plOper " * " (plp e) (plp e')
plp (ELit lit) = plp lit plp (ELit lit) = plp lit
plp (EMeta n) = "Meta_" ++ show n plp (EMeta n) = "Meta_" ++ show n
@@ -259,21 +254,15 @@ instance AlphaConvert a => AlphaConvert [a] where
instance AlphaConvert Type where instance AlphaConvert Type where
alphaConvert env@(_,subst) (DTyp hypos cat args) alphaConvert env@(_,subst) (DTyp hypos cat args)
= ((ctr,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 ((ctr,_), args') = alphaConvert env' args
instance AlphaConvert Hypo where alphaConvertHypo env (b,x,typ) = ((ctr+1,(x,x'):subst), (b,x',typ'))
alphaConvert env (Hyp typ) = ((ctr+1,subst), Hyp typ') where ((ctr,subst), typ') = alphaConvert env typ
where ((ctr,subst), typ') = alphaConvert env typ x' = createLogicalVariable ctr
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
instance AlphaConvert Expr where 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 where ((ctr',_), e') = alphaConvert (ctr+1,(x,x'):subst) e
x' = createLogicalVariable ctr x' = createLogicalVariable ctr
alphaConvert env (EApp e1 e2) = (env'', EApp e1' e2') alphaConvert env (EApp e1 e2) = (env'', EApp e1' e2')

6
src/GF/Compile/GrammarToGFCC.hs
View File

@@ -129,7 +129,7 @@ mkExp :: [Ident] -> A.Term -> C.Expr
mkExp scope t = case GM.termForm t of mkExp scope t = case GM.termForm t of
Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args)) Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args))
where 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 mkApp scope c args = case c of
Q _ c -> foldl C.EApp (C.EFun (i2i c)) args Q _ c -> foldl C.EApp (C.EFun (i2i c)) args
QC _ 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 :: [Ident] -> A.Context -> ([Ident],[C.Hypo])
mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty
in if x == identW in if x == identW
then ( scope,C.Hyp ty') then ( scope,(C.Explicit,i2i x,ty'))
else (x:scope,C.HypV (i2i x) ty')) scope hyps else (x:scope,(C.Explicit,i2i x,ty'))) scope hyps
mkTerm :: Term -> C.Term mkTerm :: Term -> C.Term
mkTerm tr = case tr of mkTerm tr = case tr of

17
src/PGF/Binary.hs
View File

@@ -102,7 +102,7 @@ instance Binary Term where
_ -> decodingError _ -> decodingError
instance Binary Expr where 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 (EApp e1 e2) = putWord8 1 >> put (e1,e2)
put (ELit (LStr s)) = putWord8 2 >> put s put (ELit (LStr s)) = putWord8 2 >> put s
put (ELit (LFlt d)) = putWord8 3 >> put d 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) put (ETyped e ty) = putWord8 8 >> put (e,ty)
get = do tag <- getWord8 get = do tag <- getWord8
case tag of case tag of
0 -> liftM2 EAbs get get 0 -> liftM3 EAbs get get get
1 -> liftM2 EApp get get 1 -> liftM2 EApp get get
2 -> liftM (ELit . LStr) get 2 -> liftM (ELit . LStr) get
3 -> liftM (ELit . LFlt) get 3 -> liftM (ELit . LFlt) get
@@ -149,15 +149,14 @@ instance Binary Type where
put (DTyp hypos cat exps) = put (hypos,cat,exps) put (DTyp hypos cat exps) = put (hypos,cat,exps)
get = liftM3 DTyp get get get get = liftM3 DTyp get get get
instance Binary Hypo where instance Binary BindType where
put (Hyp t) = putWord8 0 >> put t put Explicit = putWord8 0
put (HypV v t) = putWord8 1 >> put (v,t) put Implicit = putWord8 1
put (HypI v t) = putWord8 2 >> put (v,t)
get = do tag <- getWord8 get = do tag <- getWord8
case tag of case tag of
0 -> liftM Hyp get 0 -> return Explicit
1 -> liftM2 HypV get get 1 -> return Implicit
2 -> liftM2 HypI get get _ -> decodingError
instance Binary FFun where instance Binary FFun where
put (FFun fun prof lins) = put (fun,prof,lins) put (FFun fun prof lins) = put (fun,prof,lins)

78
src/PGF/Expr.hs
View File

@@ -1,5 +1,5 @@
module PGF.Expr(Tree, Expr(..), Literal(..), Patt(..), Equation(..), module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..),
readExpr, showExpr, pExpr, ppExpr, ppPatt, readExpr, showExpr, pExpr, pBinds, ppExpr, ppPatt,
mkApp, unApp, mkApp, unApp,
mkStr, unStr, mkStr, unStr,
@@ -36,6 +36,11 @@ data Literal =
type MetaId = Int type MetaId = Int
data BindType =
Explicit
| Implicit
deriving (Eq,Ord,Show)
-- | Tree is the abstract syntax representation of a given sentence -- | Tree is the abstract syntax representation of a given sentence
-- in some concrete syntax. Technically 'Tree' is a type synonym -- in some concrete syntax. Technically 'Tree' is a type synonym
-- of 'Expr'. -- of 'Expr'.
@@ -45,7 +50,7 @@ type Tree = Expr
-- both parameter of a dependent type or an abstract syntax tree for -- both parameter of a dependent type or an abstract syntax tree for
-- for some sentence. -- for some sentence.
data Expr = data Expr =
EAbs CId Expr -- ^ lambda abstraction EAbs BindType CId Expr -- ^ lambda abstraction
| EApp Expr Expr -- ^ application | EApp Expr Expr -- ^ application
| ELit Literal -- ^ literal | ELit Literal -- ^ literal
| EMeta {-# UNPACK #-} !MetaId -- ^ meta variable | EMeta {-# UNPACK #-} !MetaId -- ^ meta variable
@@ -131,10 +136,24 @@ pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)
where where
pTerm = fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces) 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 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 pFactor = fmap EFun pCId
RP.<++ fmap ELit pLit RP.<++ fmap ELit pLit
RP.<++ fmap EMeta pMeta 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 :: 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.<> 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.<+> PP.text "->" PP.<+>
ppExpr 1 (xs++scope) e1) ppExpr 1 (xs++scope) e1)
where where
getVars xs (EAbs x e) = getVars (freshName x xs:xs) e getVars bs xs (EAbs b x e) = getVars (b:bs) ((freshName x xs):xs) e
getVars xs e = (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 (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 (ELit l) = ppLit l
ppExpr d scope (EMeta n) = ppMeta n 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 (PVar f) = (f:scope,ppCId f)
ppPatt d scope PWild = (scope,PP.char '_') 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 (LStr s) = PP.text (show s)
ppLit (LInt n) = PP.integer n ppLit (LInt n) = PP.integer n
ppLit (LFlt d) = PP.double d ppLit (LFlt d) = PP.double d
@@ -205,10 +227,12 @@ ppParens True = PP.parens
ppParens False = id ppParens False = id
freshName :: CId -> [CId] -> CId freshName :: CId -> [CId] -> CId
freshName x xs = loop 1 x freshName x xs0 = loop 1 x
where where
xs = wildCId : xs0
loop i y 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 | otherwise = y
@@ -220,12 +244,12 @@ freshName x xs = loop 1 x
normalForm :: Funs -> Int -> Env -> Expr -> Expr normalForm :: Funs -> Int -> Env -> Expr -> Expr
normalForm funs k env e = value2expr k (eval funs env e) normalForm funs k env e = value2expr k (eval funs env e)
where where
value2expr i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr i) vs) 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 (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 (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 (VSusp j env vs k) = value2expr i (k (VGen j vs))
value2expr i (VLit l) = ELit l 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 (VClosure env (EAbs b x e)) = EAbs b x (value2expr (i+1) (eval funs ((VGen i []):env) e))
data Value data Value
= VApp CId [Value] = VApp CId [Value]
@@ -248,7 +272,7 @@ eval funs env (EFun f) = case Map.lookup f funs of
else VApp f [] else VApp f []
Nothing -> error ("unknown function "++showCId f) Nothing -> error ("unknown function "++showCId f)
eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2] 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 (EMeta i) = VMeta i env []
eval funs env (ELit l) = VLit l eval funs env (ELit l) = VLit l
eval funs env (ETyped e _) = eval funs env e 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 else VApp f vs
Nothing -> error ("unknown function "++showCId f) 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 (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 (EMeta i) vs = VMeta i env vs
apply funs env (ELit l) vs = error "literal of function type" 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 (ETyped e _) vs = apply funs env e vs
applyValue funs v [] = v applyValue funs v [] = v
applyValue funs (VApp f vs0) vs = apply funs [] (EFun f) (vs0++vs) applyValue funs (VApp f vs0) vs = apply funs [] (EFun f) (vs0++vs)
applyValue funs (VLit _) vs = error "literal of function type" applyValue funs (VLit _) vs = error "literal of function type"
applyValue funs (VMeta i env vs0) vs = VMeta i env (vs0++vs) applyValue funs (VMeta i env vs0) vs = VMeta i env (vs0++vs)
applyValue funs (VGen i vs0) vs = VGen i (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 (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 (VClosure env (EAbs b x e)) (v:vs) = apply funs (v:env) e vs
----------------------------------------------------- -----------------------------------------------------
-- Pattern matching -- Pattern matching

9
src/PGF/Expr.hs-boot
View File

@@ -10,7 +10,16 @@ instance Eq Expr
instance Ord Expr instance Ord Expr
instance Show Expr instance Show Expr
data BindType = Explicit | Implicit
instance Eq BindType
instance Ord BindType
instance Show BindType
pFactor :: RP.ReadP Expr pFactor :: RP.ReadP Expr
pBinds :: RP.ReadP [(BindType,CId)]
ppExpr :: Int -> [CId] -> Expr -> PP.Doc ppExpr :: Int -> [CId] -> Expr -> PP.Doc

8
src/PGF/Linearize.hs
View File

@@ -59,8 +59,8 @@ linTree :: PGF -> CId -> Expr -> Term
linTree pgf lang = lin . expr2tree linTree pgf lang = lin . expr2tree
where where
lin (Abs xs e ) = case lin e of lin (Abs xs e ) = case lin e of
R ts -> R $ ts ++ (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) xs) TM s -> R $ (TM s) : (Data.List.map (kks . showCId . snd) xs)
lin (Fun fun es) = let argVariants = mapM (liftVariants . lin) es lin (Fun fun es) = let argVariants = mapM (liftVariants . lin) es
in variants [compute pgf lang args $ look fun | args <- argVariants] in variants [compute pgf lang args $ look fun | args <- argVariants]
lin (Lit (LStr s)) = R [kks (show s)] -- quoted lin (Lit (LStr s)) = R [kks (show s)] -- quoted
@@ -130,8 +130,8 @@ linTreeMark :: PGF -> CId -> Expr -> Term
linTreeMark pgf lang = lin [] . expr2tree linTreeMark pgf lang = lin [] . expr2tree
where where
lin p (Abs xs e ) = case lin p e of lin p (Abs xs e ) = case lin p e of
R ts -> R $ ts ++ (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) xs) TM s -> R $ (TM s) : (Data.List.map (kks . showCId . snd) xs)
lin p (Fun fun es) = let argVariants = lin p (Fun fun es) = let argVariants =
mapM (\ (i,e) -> liftVariants $ lin (sub p i) e) (zip [0..] es) mapM (\ (i,e) -> liftVariants $ lin (sub p i) e) (zip [0..] es)
in variants [mark p $ compute pgf lang args $ look fun | args <- argVariants] in variants [mark p $ compute pgf lang args $ look fun | args <- argVariants]

8
src/PGF/Macros.hs
View File

@@ -100,17 +100,15 @@ restrictPGF cond pgf = pgf {
abstr = abstract pgf abstr = abstract pgf
depth :: Expr -> Int depth :: Expr -> Int
depth (EAbs _ t) = depth t depth (EAbs _ _ t) = depth t
depth (EApp e1 e2) = max (depth e1) (depth e2) + 1 depth (EApp e1 e2) = max (depth e1) (depth e2) + 1
depth _ = 1 depth _ = 1
cftype :: [CId] -> CId -> Type 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 :: Hypo -> Type
typeOfHypo (Hyp ty) = ty typeOfHypo (_,_,ty) = ty
typeOfHypo (HypV _ ty) = ty
typeOfHypo (HypI _ ty) = ty
catSkeleton :: Type -> ([CId],CId) catSkeleton :: Type -> ([CId],CId)
catSkeleton ty = case ty of catSkeleton ty = case ty of

2
src/PGF/Parsing/FCFG/Incremental.hs
View File

@@ -134,7 +134,7 @@ extractTrees (State pgf pinfo chart items) ty@(DTyp _ start _) =
check_ho_fun fun args check_ho_fun fun args
| fun == _V = return (head 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) | otherwise = return (Set.unions (map fst args),foldl (\e x -> EApp e (snd x)) (EFun fun) args)
mkVar (EFun v) = v mkVar (EFun v) = v

52
src/PGF/Tree.hs
View File

@@ -1,6 +1,5 @@
module PGF.Tree module PGF.Tree
( Tree(..), ( Tree(..),
readTree, showTree, pTree, ppTree,
tree2expr, expr2tree tree2expr, expr2tree
) where ) where
@@ -18,54 +17,13 @@ import qualified Text.ParserCombinators.ReadP as RP
-- allow unapplied lambda abstractions. The tree is used directly -- allow unapplied lambda abstractions. The tree is used directly
-- from the linearizer and is produced directly from the parser. -- from the linearizer and is produced directly from the parser.
data Tree = 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 | Var CId -- ^ variable
| Fun CId [Tree] -- ^ function application | Fun CId [Tree] -- ^ function application
| Lit Literal -- ^ literal | Lit Literal -- ^ literal
| Meta {-# UNPACK #-} !MetaId -- ^ meta variable | Meta {-# UNPACK #-} !MetaId -- ^ meta variable
deriving (Eq, Ord) 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 -- 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 (Fun x ts) = foldl EApp (EFun x) (List.map (tree2expr ys) ts)
tree2expr ys (Lit l) = ELit l tree2expr ys (Lit l) = ELit l
tree2expr ys (Meta n) = EMeta n 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 tree2expr ys (Var x) = case List.lookup x (zip ys [0..]) of
Just i -> EVar i Just i -> EVar i
Nothing -> error "unknown variable" Nothing -> error "unknown variable"
@@ -88,11 +46,11 @@ tree2expr = tree2expr []
expr2tree :: Expr -> Tree expr2tree :: Expr -> Tree
expr2tree e = abs [] [] e expr2tree e = abs [] [] e
where 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 (ETyped e _) = abs ys xs e
abs ys xs e = case xs of abs ys xs e = case xs of
[] -> app ys [] e [] -> 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 (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1
app xs as (ELit l) app xs as (ELit l)
@@ -101,7 +59,7 @@ expr2tree e = abs [] [] e
app xs as (EMeta n) app xs as (EMeta n)
| List.null as = Meta n | List.null as = Meta n
| otherwise = error "meta variables of function type are not allowed in trees" | 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 (EVar i) = Var (xs !! i)
app xs as (EFun f) = Fun f as app xs as (EFun f) = Fun f as
app xs as (ETyped e _) = app xs as e app xs as (ETyped e _) = app xs as e

33
src/PGF/Type.hs
View File

@@ -1,4 +1,4 @@
module PGF.Type ( Type(..), Hypo(..), module PGF.Type ( Type(..), Hypo,
readType, showType, readType, showType,
pType, ppType, ppHypo ) where pType, ppType, ppHypo ) where
@@ -16,11 +16,7 @@ data Type =
deriving (Eq,Ord,Show) deriving (Eq,Ord,Show)
-- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis -- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis
data Hypo = type Hypo = (BindType,CId,Type)
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)
-- | Reads a 'Type' from a 'String'. -- | Reads a 'Type' from a 'String'.
readType :: String -> Maybe Type readType :: String -> Maybe Type
@@ -45,23 +41,23 @@ pType = do
where where
pHypo = pHypo =
do (cat,args) <- pAtom do (cat,args) <- pAtom
return [Hyp (DTyp [] cat args)] return [(Explicit,wildCId,DTyp [] cat args)]
RP.<++ RP.<++
(RP.between (RP.char '(') (RP.char ')') $ do (RP.between (RP.char '(') (RP.char ')') $ do
hyp <- RP.option (\ty -> [Hyp ty]) $ do xs <- RP.option [(Explicit,wildCId)] $ do
vs <- RP.sepBy (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',') xs <- pBinds
RP.skipSpaces RP.skipSpaces
RP.char ':' RP.char ':'
return (\ty -> [HypV v ty | v <- vs]) return xs
ty <- pType ty <- pType
return (hyp ty)) return [(b,v,ty) | (b,v) <- xs])
RP.<++ RP.<++
(RP.between (RP.char '{') (RP.char '}') $ do (RP.between (RP.char '{') (RP.char '}') $ do
vs <- RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',') vs <- RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')
RP.skipSpaces RP.skipSpaces
RP.char ':' RP.char ':'
ty <- pType ty <- pType
return [HypI v ty | v <- vs]) return [(Implicit,v,ty) | v <- vs])
pAtom = do pAtom = do
cat <- pCId cat <- pCId
@@ -77,8 +73,11 @@ ppType d scope (DTyp hyps cat args)
where where
ppRes scope cat es = ppCId cat PP.<+> PP.hsep (map (ppExpr 4 scope) es) 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 (Explicit,x,typ) = if x == wildCId
ppHypo scope (HypV x typ) = let y = freshName x scope then (scope,ppType 1 scope typ)
in (y:scope,PP.parens (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ)) else let y = freshName x scope
ppHypo scope (HypI x typ) = let y = freshName x scope in (y:scope,PP.parens (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
in (y:scope,PP.braces (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))

116
src/PGF/TypeCheck.hs
View File

@@ -200,12 +200,11 @@ tcHypos scope (h:hs) = do
return (scope,h:hs) return (scope,h:hs)
tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo) tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
tcHypo scope (Hyp ty) = do tcHypo scope (b,x,ty) = do
ty <- tcType scope ty ty <- tcType scope ty
return (scope,Hyp ty) if x == wildCId
tcHypo scope (HypV x ty) = do then return (scope,(b,x,ty))
ty <- tcType scope ty else return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,(b,x,ty))
return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,HypV x ty)
tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr]) tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr])
tcHypoExprs scope delta [] = return (delta,[]) tcHypoExprs scope delta [] = return (delta,[])
@@ -215,13 +214,12 @@ tcHypoExprs scope delta ((e,h):xs) = do
return (delta,e:es) return (delta,e:es)
tcHypoExpr :: Scope -> Env -> Expr -> Hypo -> TcM (Env,Expr) tcHypoExpr :: Scope -> Env -> Expr -> Hypo -> TcM (Env,Expr)
tcHypoExpr scope delta e (Hyp ty) = do tcHypoExpr scope delta e (b,x,ty) = do
e <- tcExpr scope e (TTyp delta ty) e <- tcExpr scope e (TTyp delta ty)
return (delta,e) funs <- getFuns
tcHypoExpr scope delta e (HypV x ty) = do if x == wildCId
e <- tcExpr scope e (TTyp delta ty) then return ( delta,e)
funs <- getFuns else return (eval funs (scopeEnv scope) e:delta,e)
return (eval funs (scopeEnv scope) e:delta,e)
----------------------------------------------------- -----------------------------------------------------
@@ -239,16 +237,16 @@ checkExpr pgf e ty =
Fail err -> Left err Fail err -> Left err
tcExpr :: Scope -> Expr -> TType -> TcM Expr tcExpr :: Scope -> Expr -> TType -> TcM Expr
tcExpr scope e0@(EAbs x e) tty = tcExpr scope e0@(EAbs b x e) tty =
case tty of case tty of
TTyp delta (DTyp (h:hs) c es) -> do e <- case h of TTyp delta (DTyp ((_,y,ty):hs) c es) -> do e <- if y == wildCId
Hyp ty -> tcExpr (addScopedVar x (TTyp delta ty) scope) then tcExpr (addScopedVar x (TTyp delta ty) scope)
e (TTyp delta (DTyp hs c es)) e (TTyp delta (DTyp hs c es))
HypV y ty -> tcExpr (addScopedVar x (TTyp delta ty) scope) else tcExpr (addScopedVar x (TTyp delta ty) scope)
e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)) e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
return (EAbs x e) return (EAbs b x e)
_ -> do ty <- evalType (scopeSize scope) tty _ -> do ty <- evalType (scopeSize scope) tty
tcError (NotFunType (scopeVars scope) e0 ty) tcError (NotFunType (scopeVars scope) e0 ty)
tcExpr scope (EMeta _) tty = do tcExpr scope (EMeta _) tty = do
i <- newMeta scope i <- newMeta scope
return (EMeta i) 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 :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env)
eqHyps k delta1 [] delta2 [] = eqHyps k delta1 [] delta2 [] =
return (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) eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
(k,delta1,delta2) <- eqHyps k delta1 h1s delta2 h2s if x == wildCId && y == wildCId
return (k,delta1,delta2) then eqHyps k delta1 h1s delta2 h2s
eqHyps k delta1 (HypV x ty1 : h1s) delta2 (HypV y ty2 : h2s) = do else if x /= wildCId && y /= wildCId
eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2) then eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s
(k,delta1,delta2) <- eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s else raiseTypeMatchError
return (k,delta1,delta2)
eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError
eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM () 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 MUnbound _ _ -> return v
deRef v = 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 (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 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) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
eqValue' k (VMeta i env1 vs1) v2 = do (MUnbound scopei cs) <- getMeta i eqValue' k (VMeta i env1 vs1) v2 = do (MUnbound scopei cs) <- getMeta i
e2 <- mkLam i scopei env1 vs1 v2 e2 <- mkLam i scopei env1 vs1 v2
setMeta i (MBound e2) setMeta i (MBound e2)
sequence_ [c e2 | c <- cs] sequence_ [c e2 | c <- cs]
eqValue' k v1 (VMeta i env2 vs2) = do (MUnbound scopei cs) <- getMeta i eqValue' k v1 (VMeta i env2 vs2) = do (MUnbound scopei cs) <- getMeta i
e1 <- mkLam i scopei env2 vs2 v1 e1 <- mkLam i scopei env2 vs2 v1
setMeta i (MBound e1) setMeta i (MBound e1)
sequence_ [c e1 | c <- cs] sequence_ [c e1 | c <- cs]
eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2 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 (VLit l1) (VLit l2 ) | l1 == l2 = return ()
eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2 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 [] 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 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 mkLam i scope env vs0 v = do
let k = scopeSize scope 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)) return (addLam vs0 (value2expr funs (length xs) v))
where where
addLam [] e = e 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" 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 let ((k1,delta1),hyps1) = mapAccumL (evalHypo sig) (k,delta) hyps
in DTyp hyps1 cat (List.map (normalForm sig k1 delta1) es) 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) (b,x,ty) =
evalHypo sig (k,delta) (HypV x ty) = ((k+1,(VGen k []):delta),HypV x (evalTy sig k delta ty)) if x == wildCId
evalHypo sig (k,delta) (HypI x ty) = ((k+1,(VGen k []):delta),HypI x (evalTy sig k delta ty)) 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 refineExpr_ ms e = refine e
where 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 (EApp e1 e2) = EApp (refine e1) (refine e2)
refine (ELit l) = ELit l refine (ELit l) = ELit l
refine (EMeta i) = case IntMap.lookup i ms of refine (EMeta i) = case IntMap.lookup i ms of
@@ -467,15 +465,11 @@ refineExpr_ ms e = refine e
refineType :: Type -> TcM Type refineType :: Type -> TcM Type
refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty)) 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) value2expr sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs)
refineHypo_ ms (HypV x ty) = HypV x (refineType_ ms ty) value2expr sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs)
refineHypo_ ms (HypI x ty) = HypI x (refineType_ ms ty) 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 (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs) value2expr sig i (VLit l) = ELit l
value2expr sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs) value2expr sig i (VClosure env (EAbs b x e)) = EAbs b x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))
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))

2
testsuite/runtime/typecheck/typecheck.gfs.gold
View File

@@ -30,7 +30,7 @@ In the expression: mkMorph (\x -> succ zero)
Type: Vector (plus (succ (succ zero)) (succ zero)) Type: Vector (plus (succ (succ zero)) (succ zero))
Expression: <\m, n -> vector (plus m n) : (m : Nat) -> (n : Nat) -> Vector (plus m n)> Expression: <\m, n -> vector (plus m n) : (m : Nat) -> (n : Nat) -> Vector (plus m n)>