From d1b1cd6e8cb96d2c86cb4ebe6c9166049e2d89be Mon Sep 17 00:00:00 2001 From: krangelov Date: Thu, 9 Dec 2021 07:46:49 +0100 Subject: [PATCH] an API for constructing HOAS expressions --- src/runtime/haskell/PGF2.hsc | 3 ++- src/runtime/haskell/PGF2/Expr.hs | 14 +++++++++++++- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/runtime/haskell/PGF2.hsc b/src/runtime/haskell/PGF2.hsc index 92438b3a5..fa28034e5 100644 --- a/src/runtime/haskell/PGF2.hsc +++ b/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, diff --git a/src/runtime/haskell/PGF2/Expr.hs b/src/runtime/haskell/PGF2/Expr.hs index 66661c785..7c0dd1f8d 100644 --- a/src/runtime/haskell/PGF2/Expr.hs +++ b/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)