diff --git a/src/PGF.hs b/src/PGF.hs index 1efabcc3c..b9ad357c9 100644 --- a/src/PGF.hs +++ b/src/PGF.hs @@ -27,8 +27,9 @@ module PGF( languages, abstractName, languageCode, -- * Types - Type, + Type, Hypo, showType, readType, + mkType, mkHypo, mkDepHypo, mkImplHypo, categories, startCat, -- * Functions diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs index 02c8463e7..013754a45 100644 --- a/src/PGF/Type.hs +++ b/src/PGF/Type.hs @@ -1,5 +1,6 @@ module PGF.Type ( Type(..), Hypo, readType, showType, + mkType, mkHypo, mkDepHypo, mkImplHypo, pType, ppType, ppHypo ) where import PGF.CId @@ -10,7 +11,7 @@ import qualified Text.PrettyPrint as PP import qualified Text.ParserCombinators.ReadP as RP import Control.Monad --- | To read a type from a 'String', use 'read' or 'readType'. +-- | To read a type from a 'String', use 'readType'. data Type = DTyp [Hypo] CId [Expr] deriving (Eq,Ord,Show) @@ -31,6 +32,25 @@ readType s = case [x | (x,cs) <- RP.readP_to_S pType s, all isSpace cs] of showType :: [CId] -> Type -> String showType vars = PP.render . ppType 0 vars +-- | creates a type from list of hypothesises, category and +-- list of arguments for the category. The operation +-- @mkType [h_1,...,h_n] C [e_1,...,e_m]@ will create +-- @h_1 -> ... -> h_n -> C e_1 ... e_m@ +mkType :: [Hypo] -> CId -> [Expr] -> Type +mkType hyps cat args = DTyp hyps cat args + +-- | creates hypothesis for non-dependent type i.e. A +mkHypo :: Type -> Hypo +mkHypo ty = (Explicit,wildCId,ty) + +-- | creates hypothesis for dependent type i.e. (x : A) +mkDepHypo :: CId -> Type -> Hypo +mkDepHypo x ty = (Explicit,x,ty) + +-- | creates hypothesis for dependent type with implicit argument i.e. ({x} : A) +mkImplHypo :: CId -> Type -> Hypo +mkImplHypo x ty = (Implicit,x,ty) + pType :: RP.ReadP Type pType = do RP.skipSpaces