diff --git a/src/runtime/haskell/PGF.hs b/src/runtime/haskell/PGF.hs index 7000e01ee..00605d8ec 100644 --- a/src/runtime/haskell/PGF.hs +++ b/src/runtime/haskell/PGF.hs @@ -1,6 +1,42 @@ -module PGF (PGF2.PGF, readPGF +module PGF ( PGF2.PGF, readPGF + , abstractName + + , CId, mkCId, wildCId, showCId, readCId + + , categories + , functions, functionsByCat + + , PGF2.Expr(..), PGF2.Literal(..), Tree + + , PGF2.Type, PGF2.Hypo ) where import qualified PGF2 as PGF2 +newtype CId = CId String deriving (Show,Read,Eq,Ord) + +type Language = CId + readPGF = PGF2.readPGF + + +readLanguage = readCId +showLanguage (CId s) = s + + +abstractName gr = CId (PGF2.abstractName gr) + + +categories gr = map CId (PGF2.categories gr) + + +functions gr = map CId (PGF2.functions gr) +functionsByCat gr (CId c) = map CId (PGF2.functionsByCat gr c) + +type Tree = PGF2.Expr + + +mkCId x = CId x +wildCId = CId "_" +showCId (CId x) = x +readCId s = Just (CId s) diff --git a/src/runtime/haskell/PGF2.hsc b/src/runtime/haskell/PGF2.hsc index 3383e9a3c..93eebaf22 100644 --- a/src/runtime/haskell/PGF2.hsc +++ b/src/runtime/haskell/PGF2.hsc @@ -22,7 +22,10 @@ module PGF2 (-- * PGF Cat,categories, -- ** Functions Fun, functions, functionsByCat, - + -- ** Expressions + Expr(..), Literal(..), + -- ** Types + Type(..), Hypo, BindType(..), -- * Concrete syntax ConcName ) where diff --git a/src/runtime/haskell/PGF2/Expr.hsc b/src/runtime/haskell/PGF2/Expr.hsc index 0f24d0699..a16d6b00b 100644 --- a/src/runtime/haskell/PGF2/Expr.hsc +++ b/src/runtime/haskell/PGF2/Expr.hsc @@ -1,6 +1,66 @@ #include -module PGF2.Expr where +module PGF2.Expr(Var, Cat, Fun, + BindType(..), Literal(..), Expr(..), + Type(..), Hypo, + Patt(..), Equation(..) + ) where +type Var = String -- ^ Name of syntactic category type Cat = String -- ^ Name of syntactic category type Fun = String -- ^ Name of function + +type MetaId = Int + +data BindType = + Explicit + | Implicit + deriving (Eq,Ord,Show) + +data Literal = + LStr String -- ^ string constant + | LInt Int -- ^ integer constant + | LFlt Double -- ^ floating point constant + deriving (Eq,Ord,Show) + +-- | An expression in the abstract syntax of the grammar. It could be +-- both parameter of a dependent type or an abstract syntax tree for +-- for some sentence. +data Expr = + EAbs BindType Var Expr -- ^ lambda abstraction + | EApp Expr Expr -- ^ application + | ELit Literal -- ^ literal + | EMeta {-# UNPACK #-} !MetaId -- ^ meta variable + | EFun Fun -- ^ function or data constructor + | EVar {-# UNPACK #-} !Int -- ^ variable with de Bruijn index + | ETyped Expr Type -- ^ local type signature + | EImplArg Expr -- ^ implicit argument in expression + deriving (Eq,Ord,Show) + +-- | To read a type from a 'String', use 'readType'. +data Type = + DTyp [Hypo] Cat [Expr] + deriving (Eq,Ord,Show) + +-- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis +type Hypo = (BindType,Var,Type) + + +-- | The pattern is used to define equations in the abstract syntax of the grammar. +data Patt = + PApp Fun [Patt] -- ^ application. The identifier should be constructor i.e. defined with 'data' + | PLit Literal -- ^ literal + | PVar Var -- ^ variable + | PAs Var Patt -- ^ variable@pattern + | PWild -- ^ wildcard + | PImplArg Patt -- ^ implicit argument in pattern + | PTilde Expr + deriving 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 [Patt] Expr + deriving Show