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

now the datatype Tree is only internal. All API functions are working with Expr directly. Commands gt, gr, p and rf filter out the output via the typechecker

Browse Source
This commit is contained in:
krasimir
2009-09-08 08:40:28 +00:00
parent 9940c44259
commit 28a7c4b5c7
23 changed files with 272 additions and 322 deletions
Download Patch File Download Diff File Expand all files Collapse all files

102
src/PGF/Expr.hs
View File

@@ -1,10 +1,7 @@
module PGF.Expr(Tree(..), Literal(..),
readTree, showTree, pTree, ppTree,
Expr(..), Patt(..), Equation(..),
module PGF.Expr(Expr(..), Literal(..), Patt(..), Equation(..),
readExpr, showExpr, pExpr, ppExpr, ppPatt,
tree2expr, expr2tree, normalForm,
normalForm,
-- needed in the typechecker
Value(..), Env, Funs, eval, apply,
@@ -12,7 +9,7 @@ module PGF.Expr(Tree(..), Literal(..),
MetaId,
-- helpers
pStr,pFactor,freshName,ppMeta
pMeta,pStr,pFactor,pLit,freshName,ppMeta,ppLit,ppParens
) where
import PGF.CId
@@ -34,18 +31,6 @@ data Literal =
type MetaId = Int
-- | The tree is an evaluated expression in the abstract syntax
-- of the grammar. The type is especially restricted to not
-- 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
| Var CId -- ^ variable
| Fun CId [Tree] -- ^ function application
| Lit Literal -- ^ literal
| Meta {-# UNPACK #-} !MetaId -- ^ meta variable
deriving (Eq, Ord)
-- | An expression represents a potentially unevaluated expression
-- in the abstract syntax of the grammar.
data Expr =
@@ -74,22 +59,6 @@ data Equation =
Equ [Patt] Expr
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)
-- | parses 'String' as an expression
readExpr :: String -> Maybe Expr
readExpr s = case [x | (x,cs) <- RP.readP_to_S pExpr s, all isSpace cs] of
@@ -111,20 +80,6 @@ instance Read Expr where
-- Parsing
-----------------------------------------------------
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)
pExpr :: RP.ReadP Expr
pExpr = pExpr0 >>= optTyped
where
@@ -169,17 +124,6 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"'))
-- Printing
-----------------------------------------------------
ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>
PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) xs)) PP.<+>
PP.text "->" PP.<+>
ppTree 0 t)
ppTree d (Fun f []) = PP.text (prCId f)
ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId 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) = PP.text (prCId id)
ppExpr :: Int -> [CId] -> Expr -> PP.Doc
ppExpr d scope (EAbs x e) = let (xs,e1) = getVars [x] e
in ppParens (d > 1) (PP.char '\\' PP.<>
@@ -221,46 +165,6 @@ freshName x xs = loop 1 x
| elem y xs = loop (i+1) (mkCId (show x++"'"++show i))
| otherwise = y
-----------------------------------------------------
-- Conversion Expr <-> Tree
-----------------------------------------------------
-- | Converts a tree to expression. The conversion
-- is always total, every tree is a valid expression.
tree2expr :: Tree -> Expr
tree2expr = tree2expr []
where
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 (Var x) = case List.lookup x (zip ys [0..]) of
Just i -> EVar i
Nothing -> error "unknown variable"
-- | Converts an expression to tree. The conversion is only partial.
-- Variables and meta variables of function type and beta redexes are not allowed.
expr2tree :: Expr -> Tree
expr2tree e = abs [] [] e
where
abs ys xs (EAbs x e) = abs ys (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)
app xs as (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1
app xs as (ELit l)
| List.null as = Lit l
| otherwise = error "literal of function type encountered"
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 (EVar i) = Var (xs !! i)
app xs as (EFun f) = Fun f as
app xs as (ETyped e _) = app xs as e
-----------------------------------------------------
-- Computation