an API for constructing HOAS expressions

src/runtime/haskell/PGF2.hsc

@@ -28,8 +28,9 @@ module PGF2 (-- * PGF
 
              -- ** Expressions
              Expr(..), Literal(..), showExpr, readExpr,
-             mkAbs,    unAbs,
+             mkAbs,    unAbs, Var,
              mkApp,    unApp, unapply,
+             mkVar,    unVar,
              mkStr,    unStr,
              mkInt,    unInt,
              mkDouble, unDouble,

src/runtime/haskell/PGF2/Expr.hs

@@ -1,10 +1,11 @@
-module PGF2.Expr(Var, Cat, Fun,
+module PGF2.Expr(Var, Cat, Fun, Var,
                  BindType(..), Literal(..), Expr(..),
                  Type(..), Hypo,
                  Patt(..), Equation(..),
 
                  mkAbs,    unAbs,
                  mkApp,    unApp, unapply,
+                 mkVar,    unVar,
                  mkStr,    unStr,
                  mkInt,    unInt,
                  mkDouble, unDouble,
@@ -107,6 +108,17 @@ unapply = extract []
     extract es (EImplArg e) = extract es e
     extract es h            = (h,es)
 
+-- | Constructs a variable expression from a de Bruijn index
+mkVar :: Int -> Expr
+mkVar = EVar
+
+-- | Extracts the de Bruijn index of a variable
+unVar :: Expr -> Maybe Int
+unVar (EVar i)      = Just i
+unVar (ETyped e ty) = unVar e
+unVar (EImplArg e)  = unVar e
+unVar _             = Nothing
+
 -- | Constructs an expression from string literal
 mkStr :: String -> Expr
 mkStr s = ELit (LStr s)