From 01db0224bee788dacd18c51c42100afa4bcc6366 Mon Sep 17 00:00:00 2001
From: krangelov <kr.angelov@gmail.com>
Date: Thu, 12 Aug 2021 12:16:11 +0200
Subject: [PATCH] API for constructing types

---
 src/runtime/haskell/PGF.hs       |  4 +++-
 src/runtime/haskell/PGF2.hsc     |  2 ++
 src/runtime/haskell/PGF2/Expr.hs | 27 +++++++++++++++++++++++++++
 3 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/src/runtime/haskell/PGF.hs b/src/runtime/haskell/PGF.hs
index a309c75f0..7bdf40317 100644
--- a/src/runtime/haskell/PGF.hs
+++ b/src/runtime/haskell/PGF.hs
@@ -16,7 +16,9 @@ module PGF ( PGF2.PGF, readPGF
            , PGF2.mkFloat,  PGF2.unFloat
            , PGF2.mkMeta,   PGF2.unMeta
 
-           , PGF2.Type, PGF2.Hypo
+           , PGF2.Type(..), PGF2.Hypo
+           , PGF2.mkType, PGF2.unType
+           , PGF2.mkHypo, PGF2.mkDepHypo, PGF2.mkImplHypo
            ) where
 
 import qualified PGF2 as PGF2
diff --git a/src/runtime/haskell/PGF2.hsc b/src/runtime/haskell/PGF2.hsc
index 5ecedbba2..fb4ce37a8 100644
--- a/src/runtime/haskell/PGF2.hsc
+++ b/src/runtime/haskell/PGF2.hsc
@@ -35,6 +35,8 @@ module PGF2 (-- * PGF
              -- ** Types
              Type(..), Hypo, BindType(..),
              readType,
+             mkType, unType,
+             mkHypo, mkDepHypo, mkImplHypo,
              -- * Concrete syntax
              ConcName
             ) where
diff --git a/src/runtime/haskell/PGF2/Expr.hs b/src/runtime/haskell/PGF2/Expr.hs
index b97431755..fb211f8f0 100644
--- a/src/runtime/haskell/PGF2/Expr.hs
+++ b/src/runtime/haskell/PGF2/Expr.hs
@@ -10,6 +10,10 @@ module PGF2.Expr(Var, Cat, Fun,
                  mkDouble, unDouble,
                  mkFloat,  unFloat,
                  mkMeta,   unMeta,
+
+                 mkType, unType,
+                 mkHypo, mkDepHypo, mkImplHypo
+
                 ) where
 
 type Var = String -- ^ Name of syntactic category
@@ -147,3 +151,26 @@ unMeta (EMeta i)     = Just i
 unMeta (ETyped e ty) = unMeta e
 unMeta (EImplArg e)  = unMeta e
 unMeta _             = Nothing
+
+
+-- | 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] -> Cat -> [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,"_",ty)
+
+-- | creates hypothesis for dependent type i.e. (x : A)
+mkDepHypo :: Var -> Type -> Hypo
+mkDepHypo x ty = (Explicit,x,ty)
+
+-- | creates hypothesis for dependent type with implicit argument i.e. ({x} : A)
+mkImplHypo :: Var -> Type -> Hypo
+mkImplHypo x ty = (Implicit,x,ty)
+
+unType :: Type -> ([Hypo], Cat, [Expr])
+unType (DTyp hyps cat es) = (hyps, cat, es)