Merge pull request #177 from GaloisInc/OpenTerm

Add `OpenTerm` operations.
GaloisInc · Mar 10, 2021 · c65d73e · c65d73e
2 parents a97a81b + a11f5d7
commit c65d73e
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/saw-core/src/Verifier/SAW/OpenTerm.hs b/saw-core/src/Verifier/SAW/OpenTerm.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 {- |
 Module      : Verifier.SAW.OpenTerm
@@ -21,11 +22,13 @@ module Verifier.SAW.OpenTerm (
   -- * Basic operations for building open terms
   closedOpenTerm, flatOpenTerm, sortOpenTerm, natOpenTerm,
   unitOpenTerm, unitTypeOpenTerm,
+  stringLitOpenTerm, stringTypeOpenTerm,
   pairOpenTerm, pairTypeOpenTerm, pairLeftOpenTerm, pairRightOpenTerm,
   tupleOpenTerm, tupleTypeOpenTerm, projTupleOpenTerm,
   ctorOpenTerm, dataTypeOpenTerm, globalOpenTerm,
   applyOpenTerm, applyOpenTermMulti,
   lambdaOpenTerm, lambdaOpenTermMulti, piOpenTerm, piOpenTermMulti,
+  arrowOpenTerm,
   letOpenTerm,
   -- * Monadic operations for building terms with binders
   OpenTermM(..), completeOpenTermM,
@@ -35,6 +38,7 @@ module Verifier.SAW.OpenTerm (
 
 import Control.Monad
 import Control.Monad.IO.Class
+import Data.Text (Text)
 import Numeric.Natural
 
 import Verifier.SAW.Term.Functor
@@ -83,6 +87,14 @@ unitOpenTerm = flatOpenTerm UnitValue
 unitTypeOpenTerm :: OpenTerm
 unitTypeOpenTerm = flatOpenTerm UnitType
 
+-- | Build a SAW core string literal.
+stringLitOpenTerm :: Text -> OpenTerm
+stringLitOpenTerm = flatOpenTerm . StringLit
+
+-- | Return the SAW core type @String@ of strings.
+stringTypeOpenTerm :: OpenTerm
+stringTypeOpenTerm = globalOpenTerm "Prelude.String"
+
 -- | Build an 'OpenTerm' for a pair
 pairOpenTerm :: OpenTerm -> OpenTerm -> OpenTerm
 pairOpenTerm t1 t2 = flatOpenTerm $ PairValue t1 t2
@@ -186,6 +198,10 @@ piOpenTerm x (OpenTerm tpM) body_f = OpenTerm $
      body <- bindOpenTerm x tp body_f
      typeInferComplete $ Pi x tp body
 
+-- | Build a non-dependent function type.
+arrowOpenTerm :: LocalName -> OpenTerm -> OpenTerm -> OpenTerm
+arrowOpenTerm x tp body = piOpenTerm x tp (const body)
+
 -- | Build a nested sequence of Pi abstractions as an 'OpenTerm'
 piOpenTermMulti :: [(LocalName, OpenTerm)] -> ([OpenTerm] -> OpenTerm) ->
                        OpenTerm