From 16dfcb938ce0f7d2927938ec3bec46abd2fd1147 Mon Sep 17 00:00:00 2001 From: krangelov Date: Thu, 12 Aug 2021 12:06:50 +0200 Subject: [PATCH] more of the abstract API copied from the old runtimes --- src/runtime/haskell/PGF.hs | 8 ++ src/runtime/haskell/PGF2.hsc | 10 +- src/runtime/haskell/PGF2/Expr.hs | 149 ++++++++++++++++++++++++++++++ src/runtime/haskell/PGF2/Expr.hsc | 66 ------------- 4 files changed, 165 insertions(+), 68 deletions(-) create mode 100644 src/runtime/haskell/PGF2/Expr.hs delete mode 100644 src/runtime/haskell/PGF2/Expr.hsc diff --git a/src/runtime/haskell/PGF.hs b/src/runtime/haskell/PGF.hs index 00605d8ec..a309c75f0 100644 --- a/src/runtime/haskell/PGF.hs +++ b/src/runtime/haskell/PGF.hs @@ -7,6 +7,14 @@ module PGF ( PGF2.PGF, readPGF , functions, functionsByCat , PGF2.Expr(..), PGF2.Literal(..), Tree + , PGF2.readExpr + , PGF2.mkAbs, PGF2.unAbs + , PGF2.mkApp, PGF2.unApp, PGF2.unapply + , PGF2.mkStr, PGF2.unStr + , PGF2.mkInt, PGF2.unInt + , PGF2.mkDouble, PGF2.unDouble + , PGF2.mkFloat, PGF2.unFloat + , PGF2.mkMeta, PGF2.unMeta , PGF2.Type, PGF2.Hypo ) where diff --git a/src/runtime/haskell/PGF2.hsc b/src/runtime/haskell/PGF2.hsc index aaeac003f..5ecedbba2 100644 --- a/src/runtime/haskell/PGF2.hsc +++ b/src/runtime/haskell/PGF2.hsc @@ -24,8 +24,14 @@ module PGF2 (-- * PGF Fun, functions, functionsByCat, functionType, functionIsConstructor, functionProb, -- ** Expressions - Expr(..), Literal(..), - readExpr, + Expr(..), Literal(..), readExpr, + mkAbs, unAbs, + mkApp, unApp, unapply, + mkStr, unStr, + mkInt, unInt, + mkDouble, unDouble, + mkFloat, unFloat, + mkMeta, unMeta, -- ** Types Type(..), Hypo, BindType(..), readType, diff --git a/src/runtime/haskell/PGF2/Expr.hs b/src/runtime/haskell/PGF2/Expr.hs new file mode 100644 index 000000000..b97431755 --- /dev/null +++ b/src/runtime/haskell/PGF2/Expr.hs @@ -0,0 +1,149 @@ +module PGF2.Expr(Var, Cat, Fun, + BindType(..), Literal(..), Expr(..), + Type(..), Hypo, + Patt(..), Equation(..), + + mkAbs, unAbs, + mkApp, unApp, unapply, + mkStr, unStr, + mkInt, unInt, + mkDouble, unDouble, + mkFloat, unFloat, + mkMeta, unMeta, + ) 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 + + +mkAbs :: BindType -> Var -> Expr -> Expr +mkAbs = EAbs + +unAbs :: Expr -> Maybe (BindType, Var, Expr) +unAbs (EAbs bt x e) = Just (bt,x,e) +unAbs (ETyped e ty) = unAbs e +unAbs (EImplArg e) = unAbs e +unAbs _ = Nothing + +-- | Constructs an expression by applying a function to a list of expressions +mkApp :: Fun -> [Expr] -> Expr +mkApp f es = foldl EApp (EFun f) es + +-- | Decomposes an expression into application of function +unApp :: Expr -> Maybe (Fun,[Expr]) +unApp e = case unapply e of + (EFun f,es) -> Just (f,es) + _ -> Nothing + +-- | Decomposes an expression into an application of a constructor such as a constant or a metavariable +unapply :: Expr -> (Expr,[Expr]) +unapply = extract [] + where + extract es f@(EFun _) = (f,es) + extract es (EApp e1 e2) = extract (e2:es) e1 + extract es (ETyped e ty)= extract es e + extract es (EImplArg e) = extract es e + extract es h = (h,es) + +-- | Constructs an expression from string literal +mkStr :: String -> Expr +mkStr s = ELit (LStr s) + +-- | Decomposes an expression into string literal +unStr :: Expr -> Maybe String +unStr (ELit (LStr s)) = Just s +unStr (ETyped e ty) = unStr e +unStr (EImplArg e) = unStr e +unStr _ = Nothing + +-- | Constructs an expression from integer literal +mkInt :: Int -> Expr +mkInt i = ELit (LInt i) + +-- | Decomposes an expression into integer literal +unInt :: Expr -> Maybe Int +unInt (ELit (LInt i)) = Just i +unInt (ETyped e ty) = unInt e +unInt (EImplArg e) = unInt e +unInt _ = Nothing + +-- | Constructs an expression from real number literal +mkDouble :: Double -> Expr +mkDouble f = ELit (LFlt f) + +-- | Decomposes an expression into real number literal +unDouble :: Expr -> Maybe Double +unDouble (ELit (LFlt f)) = Just f +unDouble (ETyped e ty) = unDouble e +unDouble (EImplArg e) = unDouble e +unDouble _ = Nothing + +mkFloat = mkDouble +unFloat = unDouble + +-- | Constructs an expression which is meta variable +mkMeta :: Int -> Expr +mkMeta i = EMeta i + +-- | Checks whether an expression is a meta variable +unMeta :: Expr -> Maybe Int +unMeta (EMeta i) = Just i +unMeta (ETyped e ty) = unMeta e +unMeta (EImplArg e) = unMeta e +unMeta _ = Nothing diff --git a/src/runtime/haskell/PGF2/Expr.hsc b/src/runtime/haskell/PGF2/Expr.hsc deleted file mode 100644 index a16d6b00b..000000000 --- a/src/runtime/haskell/PGF2/Expr.hsc +++ /dev/null @@ -1,66 +0,0 @@ -#include - -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