From 2174690c5e60667955bbf9fd6f0a8d3beb1734a9 Mon Sep 17 00:00:00 2001 From: bjorn Date: Mon, 20 Oct 2008 11:36:17 +0000 Subject: Added Read and Show instances for Type. This required moving some code around. --- src/PGF/Expr.hs | 45 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 43 insertions(+), 2 deletions(-) (limited to 'src/PGF/Expr.hs') diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs index 454989728..0dde19310 100644 --- a/src/PGF/Expr.hs +++ b/src/PGF/Expr.hs @@ -1,4 +1,7 @@ -module PGF.Expr(readTree, showTree, pTree, ppTree, +module PGF.Expr(Tree(..), Literal(..), + readTree, showTree, pTree, ppTree, + + Expr(..), Equation(..), readExpr, showExpr, pExpr, ppExpr, tree2expr, expr2tree, @@ -11,7 +14,6 @@ module PGF.Expr(readTree, showTree, pTree, ppTree, ) where import PGF.CId -import PGF.Data import Data.Char import Data.Maybe @@ -20,6 +22,45 @@ import qualified Text.PrettyPrint as PP import qualified Text.ParserCombinators.ReadP as RP import qualified Data.Map as Map +data Literal = + LStr String -- ^ string constant + | LInt Integer -- ^ integer constant + | LFlt Double -- ^ floating point constant + deriving (Eq,Ord,Show) + +-- | 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 Int -- ^ meta variable + deriving (Show, Eq, Ord) + +-- | An expression represents a potentially unevaluated expression +-- in the abstract syntax of the grammar. It can be evaluated with +-- the 'expr2tree' function and then linearized or it can be used +-- directly in the dependent types. +data Expr = + EAbs CId Expr -- ^ lambda abstraction + | EApp Expr Expr -- ^ application + | ELit Literal -- ^ literal + | EMeta Int -- ^ meta variable + | EVar CId -- ^ variable or function reference + | EEq [Equation] -- ^ lambda function defined as a set of equations with pattern matching + | EPi CId Expr Expr -- ^ dependent function type + deriving (Eq,Ord,Show) + +-- | The equation is used to define lambda function as a sequence +-- of equations with pattern matching. The list of 'Expr' represents +-- the patterns and the second 'Expr' is the function body for this +-- equation. +data Equation = + Equ [Expr] Expr + deriving (Eq,Ord,Show) -- | parses 'String' as an expression readTree :: String -> Maybe Tree -- cgit v1.2.3