mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 11:42:49 -06:00
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.Paraphrase
|
||||||
import PGF.Macros
|
import PGF.Macros
|
||||||
import PGF.Data
|
import PGF.Data
|
||||||
import PGF.Expr
|
|
||||||
import PGF.Type
|
|
||||||
import PGF.Raw.Convert
|
import PGF.Raw.Convert
|
||||||
import PGF.Raw.Parse
|
import PGF.Raw.Parse
|
||||||
import PGF.Raw.Print (printTree)
|
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.CId
|
||||||
|
import PGF.Expr hiding (Value, Env)
|
||||||
|
import PGF.Type
|
||||||
import GF.Text.UTF8
|
import GF.Text.UTF8
|
||||||
|
|
||||||
import qualified Data.Map as Map
|
import qualified Data.Map as Map
|
||||||
@@ -40,42 +42,6 @@ data Concr = Concr {
|
|||||||
parser :: Maybe ParserInfo -- parser
|
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 =
|
data Term =
|
||||||
R [Term]
|
R [Term]
|
||||||
| P Term Term
|
| P Term Term
|
||||||
@@ -98,18 +64,6 @@ data Alternative =
|
|||||||
Alt [String] [String]
|
Alt [String] [String]
|
||||||
deriving (Eq,Ord,Show)
|
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 FCat = Int
|
||||||
type FIndex = 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,
|
readExpr, showExpr, pExpr, ppExpr,
|
||||||
|
|
||||||
tree2expr, expr2tree,
|
tree2expr, expr2tree,
|
||||||
@@ -11,7 +14,6 @@ module PGF.Expr(readTree, showTree, pTree, ppTree,
|
|||||||
) where
|
) where
|
||||||
|
|
||||||
import PGF.CId
|
import PGF.CId
|
||||||
import PGF.Data
|
|
||||||
|
|
||||||
import Data.Char
|
import Data.Char
|
||||||
import Data.Maybe
|
import Data.Maybe
|
||||||
@@ -20,6 +22,45 @@ import qualified Text.PrettyPrint as PP
|
|||||||
import qualified Text.ParserCombinators.ReadP as RP
|
import qualified Text.ParserCombinators.ReadP as RP
|
||||||
import qualified Data.Map as Map
|
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
|
-- | parses 'String' as an expression
|
||||||
readTree :: String -> Maybe Tree
|
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.CId
|
||||||
import PGF.Data
|
|
||||||
import PGF.Expr
|
import PGF.Expr
|
||||||
import Data.Char
|
import Data.Char
|
||||||
import qualified Text.PrettyPrint as PP
|
import qualified Text.PrettyPrint as PP
|
||||||
@@ -9,16 +10,32 @@ import qualified Text.ParserCombinators.ReadP as RP
|
|||||||
import Control.Monad
|
import Control.Monad
|
||||||
import Debug.Trace
|
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 :: String -> Maybe Type
|
||||||
readType s = case [x | (x,cs) <- RP.readP_to_S pType s, all isSpace cs] of
|
readType s = case [x | (x,cs) <- RP.readP_to_S pType s, all isSpace cs] of
|
||||||
[x] -> Just x
|
[x] -> Just x
|
||||||
_ -> Nothing
|
_ -> 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'
|
-- | renders type as 'String'
|
||||||
showType :: Type -> String
|
showType :: Type -> String
|
||||||
showType = PP.render . ppType 0
|
showType = PP.render . ppType 0
|
||||||
|
|
||||||
|
pType :: RP.ReadP Type
|
||||||
pType = do
|
pType = do
|
||||||
RP.skipSpaces
|
RP.skipSpaces
|
||||||
hyps <- RP.sepBy (pHypo >>= \h -> RP.string "->" >> return h) 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
|
args <- RP.sepBy pFactor RP.skipSpaces
|
||||||
return (mkCId cat, args)
|
return (mkCId cat, args)
|
||||||
|
|
||||||
|
ppType :: Int -> Type -> PP.Doc
|
||||||
ppType d (DTyp ctxt cat args)
|
ppType d (DTyp ctxt cat args)
|
||||||
| null ctxt = ppRes cat args
|
| null ctxt = ppRes cat args
|
||||||
| otherwise = ppParens (d > 0) (foldr ppCtxt (ppRes cat args) ctxt)
|
| 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)
|
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 True = PP.parens
|
||||||
ppParens False = id
|
ppParens False = id
|
||||||
|
|||||||
@@ -54,6 +54,7 @@ pgfMain pgf command =
|
|||||||
getCat =
|
getCat =
|
||||||
do mcat <- getInput "cat"
|
do mcat <- getInput "cat"
|
||||||
case mcat of
|
case mcat of
|
||||||
|
Nothing -> return Nothing
|
||||||
Just "" -> return Nothing
|
Just "" -> return Nothing
|
||||||
Just cat | cat `notElem` PGF.categories pgf ->
|
Just cat | cat `notElem` PGF.categories pgf ->
|
||||||
throwCGIError 400 "Unknown category" ["Unknown category: " ++ cat]
|
throwCGIError 400 "Unknown category" ["Unknown category: " ++ cat]
|
||||||
|
|||||||
Reference in New Issue
Block a user