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

1 files changed, 3 insertions, 99 deletions

diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs
index 62a97698a..42f9138c9 100644
--- a/src/PGF/Expr.hs
+++ b/src/PGF/Expr.hs
@@ -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 =

@@ -75,22 +60,6 @@ data Equation =
   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

                [x] -> Just x

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