Permalink
Browse files

More syntactic suagr.

Now we can write:

exists $ \x y z -> ...
  • Loading branch information...
1 parent 6cdb099 commit 8bca705cf60c996f6d233ea5f42ad0bfa64b63e0 @yav committed Apr 27, 2009
Showing with 17 additions and 1 deletion.
  1. +17 −1 src/Data/Integer/Presburger/HOAS.hs
View
18 src/Data/Integer/Presburger/HOAS.hs
@@ -1,5 +1,8 @@
+{-# LANGUAGE FlexibleInstances #-}
+
module Data.Integer.Presburger.HOAS
- (Formula(..), check, translate
+ ( Formula(..), check, translate
+ , Quant, exists, forall
, Term, (.*), is_constant
, PP(..)
) where
@@ -59,6 +62,19 @@ translate = loop 0
d :| t -> Leaf (Prop False (Divides d t))
+class Quant t where
+ quant :: ((Term -> Formula) -> Formula) -> t -> Formula
+
+instance Quant Formula where
+ quant _ p = p
+
+instance Quant t => Quant (Term -> t) where
+ quant q p = q (\x -> quant q (p x))
+
+exists, forall :: Quant t => t -> Formula
+exists p = quant Exists p
+forall p = quant Forall p
+
-- 4: wrap term, not
-- 3: wrap and
-- 2: wrap or

0 comments on commit 8bca705

Please sign in to comment.