Merge pull request #179 from GaloisInc/forall-keyword

Rename the `forall` and `exists` operators to `forall_` and `exists_`

Author: robdockins

what4/CHANGES.md

@@ -1,5 +1,12 @@
 # next (TBA)
 
+* According to
+  [this discussion](https://github.com/ghc-proposals/ghc-proposals/discussions/440),
+  the `forall` identifier will be claimed, and `forall` made into a
+  full keyword. Therefore, the `forall` and `exists` combinators of
+  `What4.Protocol.SMTLib2.Syntax` have been
+  renamed into `forall_` and `exists_`.
+
 * Add operations for increased control over the scope of
   configuration options, both in the `What4.Config` and
   `What4.Expr.Builder` modules.

what4/src/What4/Protocol/SMTLib2.hs

@@ -638,8 +638,8 @@ newWriter _ h in_h ack isStrict solver_name permitDefineFun arithOption quantSup
 type instance Command (Writer a) = SMT2.Command
 
 instance SMTLib2Tweaks a => SMTWriter (Writer a) where
-  forallExpr vars t = SMT2.forall (varBinding @a <$> vars) t
-  existsExpr vars t = SMT2.exists (varBinding @a <$> vars) t
+  forallExpr vars t = SMT2.forall_ (varBinding @a <$> vars) t
+  existsExpr vars t = SMT2.exists_ (varBinding @a <$> vars) t
 
   arrayConstant =
     case smtlib2arrayConstant @a of

what4/src/What4/Protocol/SMTLib2/Syntax.hs

@@ -79,8 +79,8 @@ module What4.Protocol.SMTLib2.Syntax
   , eq
   , distinct
   , ite
-  , forall
-  , exists
+  , forall_
+  , exists_
   , letBinder
     -- * @Ints@, @Reals@, @Reals_Ints@ theories
   , negate
@@ -319,18 +319,18 @@ ite c x y = term_app "ite" [c, x, y]
 varBinding :: (Text,Sort) -> Builder
 varBinding (nm, tp) = "(" <> Builder.fromText nm <> " " <> unSort tp <> ")"
 
--- | @forall vars t@ denotes a predicate that holds if @t@ for every valuation of the
+-- | @forall_ vars t@ denotes a predicate that holds if @t@ for every valuation of the
 -- variables in @vars@.
-forall :: [(Text, Sort)] -> Term -> Term
-forall [] r = r
-forall vars r =
+forall_ :: [(Text, Sort)] -> Term -> Term
+forall_ [] r = r
+forall_ vars r =
   T $ app "forall" [builder_list (varBinding <$> vars), renderTerm r]
 
--- | @exists vars t@ denotes a predicate that holds if @t@ for some valuation of the
+-- | @exists_ vars t@ denotes a predicate that holds if @t@ for some valuation of the
 -- variables in @vars@.
-exists :: [(Text, Sort)] -> Term -> Term
-exists [] r = r
-exists vars r =
+exists_ :: [(Text, Sort)] -> Term -> Term
+exists_ [] r = r
+exists_ vars r =
   T $ app "exists" [builder_list (varBinding <$> vars), renderTerm r]
 
 letBinding :: (Text, Term) -> Builder