forked from GitHub/gf-core
Added Read and Show instances for Type. This required moving some code around.
This commit is contained in:
@@ -69,8 +69,6 @@ import PGF.TypeCheck
|
||||
import PGF.Paraphrase
|
||||
import PGF.Macros
|
||||
import PGF.Data
|
||||
import PGF.Expr
|
||||
import PGF.Type
|
||||
import PGF.Raw.Convert
|
||||
import PGF.Raw.Parse
|
||||
import PGF.Raw.Print (printTree)
|
||||
|
||||
@@ -1,6 +1,8 @@
|
||||
module PGF.Data where
|
||||
module PGF.Data (module PGF.Data, module PGF.Expr, module PGF.Type) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Expr hiding (Value, Env)
|
||||
import PGF.Type
|
||||
import GF.Text.UTF8
|
||||
|
||||
import qualified Data.Map as Map
|
||||
@@ -40,42 +42,6 @@ data Concr = Concr {
|
||||
parser :: Maybe ParserInfo -- parser
|
||||
}
|
||||
|
||||
data Type =
|
||||
DTyp [Hypo] CId [Expr]
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
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)
|
||||
|
||||
data Term =
|
||||
R [Term]
|
||||
| P Term Term
|
||||
@@ -98,18 +64,6 @@ data Alternative =
|
||||
Alt [String] [String]
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
data Hypo =
|
||||
Hyp CId 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)
|
||||
|
||||
|
||||
type FCat = Int
|
||||
type FIndex = Int
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -1,7 +1,8 @@
|
||||
module PGF.Type ( readType, showType, pType, ppType ) where
|
||||
module PGF.Type ( Type(..), Hypo(..),
|
||||
readType, showType,
|
||||
pType, ppType ) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Data
|
||||
import PGF.Expr
|
||||
import Data.Char
|
||||
import qualified Text.PrettyPrint as PP
|
||||
@@ -9,16 +10,32 @@ import qualified Text.ParserCombinators.ReadP as RP
|
||||
import Control.Monad
|
||||
import Debug.Trace
|
||||
|
||||
-- | parses 'String' as an expression
|
||||
-- | To read a type from a 'String', use 'read' or 'readType'.
|
||||
data Type =
|
||||
DTyp [Hypo] CId [Expr]
|
||||
deriving (Eq,Ord)
|
||||
|
||||
data Hypo =
|
||||
Hyp CId Type
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- | Reads a 'Type' from a 'String'.
|
||||
readType :: String -> Maybe Type
|
||||
readType s = case [x | (x,cs) <- RP.readP_to_S pType s, all isSpace cs] of
|
||||
[x] -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
instance Show Type where
|
||||
showsPrec i x = showString (PP.render (ppType i x))
|
||||
|
||||
instance Read Type where
|
||||
readsPrec _ = RP.readP_to_S pType
|
||||
|
||||
-- | renders type as 'String'
|
||||
showType :: Type -> String
|
||||
showType = PP.render . ppType 0
|
||||
|
||||
pType :: RP.ReadP Type
|
||||
pType = do
|
||||
RP.skipSpaces
|
||||
hyps <- RP.sepBy (pHypo >>= \h -> RP.string "->" >> return h) RP.skipSpaces
|
||||
@@ -45,7 +62,7 @@ pType = do
|
||||
args <- RP.sepBy pFactor RP.skipSpaces
|
||||
return (mkCId cat, args)
|
||||
|
||||
|
||||
ppType :: Int -> Type -> PP.Doc
|
||||
ppType d (DTyp ctxt cat args)
|
||||
| null ctxt = ppRes cat args
|
||||
| otherwise = ppParens (d > 0) (foldr ppCtxt (ppRes cat args) ctxt)
|
||||
@@ -56,5 +73,6 @@ ppType d (DTyp ctxt cat args)
|
||||
|
||||
ppRes cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 2) es)
|
||||
|
||||
ppParens :: Bool -> PP.Doc -> PP.Doc
|
||||
ppParens True = PP.parens
|
||||
ppParens False = id
|
||||
|
||||
@@ -54,6 +54,7 @@ pgfMain pgf command =
|
||||
getCat =
|
||||
do mcat <- getInput "cat"
|
||||
case mcat of
|
||||
Nothing -> return Nothing
|
||||
Just "" -> return Nothing
|
||||
Just cat | cat `notElem` PGF.categories pgf ->
|
||||
throwCGIError 400 "Unknown category" ["Unknown category: " ++ cat]
|
||||
|
||||
Reference in New Issue
Block a user