summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Yices/Painless/Language.hs184
-rw-r--r--Yices/Painless/Type.hs18
-rw-r--r--tests/examples/ex24.hs16
-rw-r--r--tests/examples/ex5.ys18
-rw-r--r--tests/examples/ex6.ys18
-rw-r--r--yices-painless.cabal10
6 files changed, 176 insertions, 88 deletions
diff --git a/Yices/Painless/Language.hs b/Yices/Painless/Language.hs
index a607f60..f95fa56 100644
--- a/Yices/Painless/Language.hs
+++ b/Yices/Painless/Language.hs
@@ -2,6 +2,7 @@
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
@@ -52,6 +53,26 @@
-- > x1 => 0b100
-- > Satisfiable
--
+-- /Uninterpreted functions/
+--
+-- > {-# LANGUAGE ScopedTypeVariables #-}
+-- > import Yices.Painless.Language
+-- >
+-- > main = print =<< solve p
+-- >
+-- > p f g (n :: Exp Int) = f n &&* g (f n)
+--
+-- Returns an assignment to the variables, and a model for the functions
+-- (using Yices pretty printer):
+--
+-- > $ runhaskell ex0.hs
+-- > x0 => 1
+-- >
+-- > (= x0 1)
+-- > (= (f2 1) true)
+-- > (= (f1 true) true)
+--
+-- > Satisfiable
module Yices.Painless.Language (
@@ -60,6 +81,7 @@ module Yices.Painless.Language (
-- * Building Yices propositions.
Yices, Exp,
+ BitVector,
-- ** Scalar introduction
-- constant,
@@ -71,6 +93,9 @@ module Yices.Painless.Language (
-- ** Bit vectors
-- $BitInstances
+ -- ** Uninterpreted functions
+ -- $Functions
+
-- ** Conditional expressions
(?),
@@ -86,12 +111,15 @@ module Yices.Painless.Language (
-- * Design discussion
-- $Notes
+ module Data.Bits
+
) where
import Prelude hiding (not, or, and, min, max)
import Data.Typeable
import qualified Data.Map as M
+import Data.Maybe
import Data.Bits
@@ -134,6 +162,16 @@ import qualified Yices.Painless.Tuple as Tuple
-- into their symbolic form.
--
+-- $Functions
+--
+-- Uninterpreted functions may be introduced as variables (alongside
+-- scalar variables).
+--
+-- E.g.
+--
+-- > \f g x -> f (g x) ==* 7
+--
+
------------------------------------------------------------------------
-- Language
@@ -469,8 +507,12 @@ data YicesProg r where
data Exp t where
-- Needed for conversion to de Bruijn form
- Tag :: (IsScalar t) => Int -> Exp t
- -- environment size at defining occurrence
+ Tag :: (IsAType t) => Int -> Exp t
+
+ -- NNN
+ TagFn :: (IsAType (a -> b)) => Int -> (Exp a -> Exp b)
+ -- application of a symbolic function to an argument.
+ -- TODO: basically, a restricted form of application. Sort this out.
Const :: (Show t, IsScalar t)
=> t -> Exp t
@@ -531,13 +573,24 @@ instance Yices (Exp b) b where
-- Convert expressions
convert lyt e = OBody (convertOpenExp lyt e)
-instance (IsScalar a, Yices f r) => Yices (Exp a -> f) (a -> r) where
+instance (IsAType a, IsScalar a, Yices f r) => Yices (Exp a -> f) (a -> r) where
-- Convert binders, one bind at a time.
convert lyt f = OLam (convert lyt' (f a))
where
a = Tag (size lyt)
lyt' = inc lyt `PushLayout` ZeroIdx
+
+-- No instance for (Yices ((Exp Int -> Exp Int) -> Exp Int -> Exp Bool) r)
+
+-- Convert functions. Identical for the other recursive case.
+instance (IsScalar a, IsScalar b, Yices f r)
+ => Yices ((Exp a -> Exp b) -> f) ((a -> b) -> r) where
+ convert lyt f = OLam (convert lyt' (f g))
+ where
+ g = TagFn (size lyt) -- :: Exp a -> Exp b -- generate a fresh, anonymous function!
+ lyt' = inc lyt `PushLayout` ZeroIdx
+
------------------------------------------------------------------------
-- |Conversion from HOAS to de Bruijn expression AST
@@ -565,6 +618,8 @@ convertOpenExp lyt = cvt
where
cvt :: Exp t' -> OpenExp env t'
cvt (Tag i) = Var (prjIdx (size lyt - i - 1) lyt) -- indexing!
+ cvt (TagFn i arg) = VarFn (prjIdx (size lyt - i - 1) lyt) (cvt arg)-- indexing!
+ -- application.
cvt (Const v) = OConst v
cvt (Tuple tup) = OTuple (convertTuple lyt tup)
cvt (Cond e1 e2 e3) = OCond (cvt e1) (cvt e2) (cvt e3)
@@ -670,8 +725,9 @@ data OpenYices t where
-- |Function abstraction
--
data OpenFun env t where
- OBody :: OpenExp env t -> OpenFun env t
- OLam :: IsScalar a => OpenFun (env, a) t -> OpenFun env (a -> t)
+ OBody :: OpenExp env t -> OpenFun env t
+ -- OLam :: {-IsScalar a =>-} OpenFun (env, a) t -> OpenFun env (a -> t)
+ OLam :: IsAType a => OpenFun (env, a) t -> OpenFun env (a -> t)
-- |Function without free scalar variables
--
@@ -686,11 +742,15 @@ type OFun t = OpenFun () t
--
data OpenExp env t where
- -- Variable index, ranging only over tuples or scalars
- Var :: IsScalar t
+ -- Variable index
+ Var :: IsAType t
=> Idx env t
-> OpenExp env t
+ VarFn :: IsAType (a -> b) =>
+ Idx env (a -> b) -> (OpenExp env a -> OpenExp env b)
+ -- TODO: restricted form of application
+
-- Constant values
OConst :: (Show t, IsScalar t)
=> t
@@ -837,17 +897,24 @@ prettyYices n (OY f) = prettyFun n f
prettyFun :: Int -> OpenFun env a -> Doc
prettyFun lvl fun =
- let (n, bodyDoc) = count fun
+ let (n, vs, bodyDoc) = count fun
in
if n < 0
then bodyDoc
else
- char '\\' <> hsep [text $ "x" ++ show idx | idx <- reverse [0..n]] <+>
+ char '\\' <> hsep [text $ case ei of Left i -> "f" ++ show i ;
+ Right i -> "x" ++ show i
+ | ei <- vs] <+>
text "->" <+> bodyDoc
where
- count :: OpenFun env fun -> (Int, Doc)
- count (OBody body) = (-1, prettyExp lvl noParens body)
- count (OLam fun') = let (n, body) = count fun' in (1 + n, body)
+ count :: OpenFun env fun -> (Int, [Either Int Int], Doc)
+ count (OBody body) = ((-1), [], prettyExp lvl noParens body)
+
+ count (OLam (f :: OpenFun (env, a) t)) | (AFunctionType _ _) <- aType :: AType a =
+ let (n, vs, body) = count f in (1 + n, Left (1+n) : vs, body)
+
+ count (OLam (f :: OpenFun (env, a) t)) =
+ let (n, vs, body) = count f in (1 + n, Right (1+n) : vs, body)
-- Pretty print an expression.
--
@@ -856,7 +923,9 @@ prettyFun lvl fun =
prettyExp :: forall t env .
Int -> (Doc -> Doc) -> OpenExp env t -> Doc
+-- TODO: function types
prettyExp _ _ (Var idx) = text $ "x" ++ show (idxToInt idx)
+prettyExp lvl wrap (VarFn idx e) = text ( "f" ++ show (idxToInt idx)) <+> prettyExp lvl wrap e
prettyExp _ _ (OConst v) = text $ show (v :: t) -- dispatch differently for BitVector types
prettyExp lvl _ (OTuple tup) = prettyTuple lvl tup
@@ -934,7 +1003,7 @@ solve q' = do
Yices.setTypeChecker True
let t = convertYices q -- bind all the variables
- print t
+ -- print t
(g,e) <- execY c t
@@ -953,7 +1022,7 @@ solve q' = do
Nothing -> return Yices.Satisfiable
Just m -> do
- vs <- sequence
+ vs <- catMaybes `fmap` sequence
[ get m v t' d
| (v,(t',d)) <- M.toList g ]
@@ -963,25 +1032,32 @@ solve q' = do
Nothing -> putStrLn "_"
Just v -> print v)
+ -- TODO: extract functions.
+ Yices.display m
+
-- print cs
return Yices.Satisfiable
--- | Retrieving bindings by type
+-- | Retrieving bindings by type (can't retrieve functions)
--
-get :: Yices.Model -> String -> YType -> Yices.Decl -> IO (String, YValue)
-get m v (YType (ty :: ScalarType t)) d
+get :: Yices.Model -> String -> YType -> Yices.Decl -> IO (Maybe (String, YValue))
+get m v (YType (ty :: AType t)) d
- | NumScalarType (IntegralNumType (TypeInt _)) <- ty
+ | AScalarType (NumScalarType (IntegralNumType (TypeInt _))) <- ty
= do mn <- Yices.getValueInt m d
- return (v, YValue mn)
+ return $ Just (v, YValue mn)
- | NonNumScalarType (TypeBool _) <- ty
+ | AScalarType (NonNumScalarType (TypeBool _)) <- ty
= do mn <- Yices.getValueBool m d
- return (v, YValue mn)
+ return $ Just (v, YValue mn)
- | NumScalarType (IntegralNumType (TypeVectorBool _)) <- ty
+ | AScalarType (NumScalarType (IntegralNumType (TypeVectorBool _))) <- ty
= do mn <- Yices.getValueBitVector m d (fromIntegral $ 8 * sizeOf (undefined :: Word))
- return (v, YValue $ fmap BitVector mn)
+ return $ Just (v, YValue $ fmap BitVector mn)
+
+ -- Can't return function models?
+ | AFunctionType _ _ <- ty
+ = return Nothing
| otherwise = error "Yices.Painless.get: don't know how to get this type yet"
@@ -992,9 +1068,9 @@ get m v (YType (ty :: ScalarType t)) d
--
type YEnv = M.Map String (YType, Yices.Decl)
-data YType = forall a. IsScalar a => YType (ScalarType a)
+data YType = forall a. IsAType a => YType (AType a)
-data YValue = forall a. (Show a, IsScalar a) => YValue (Maybe a)
+data YValue = forall a. (Show a, IsAType a) => YValue (Maybe a)
--
-- To run,
@@ -1013,42 +1089,70 @@ execY c (OY f) = execF c f
-- Declaring variables. Begin with a closed Yices program.
--
execF :: Yices.Context -> OFun t -> IO (YEnv, Yices.Expr)
-execF c fn = go fn 0 M.empty
+execF c fn = go fn (count fn) M.empty
where
+ -- determine size of environment
+ count :: OpenFun env f -> Int
+ count (OBody _) = (-1)
+ count (OLam f) = 1 + count f
+
go :: OpenFun env u -> Int -> YEnv -> IO (YEnv, Yices.Expr)
go (OBody b) _ g = (,) g <$> exec c b
-- Numbers
go (OLam (f :: OpenFun (env, a) t)) n g
- | ty@(NumScalarType (IntegralNumType (TypeInt _))) <- scalarType :: ScalarType a
+ | ty@(AScalarType (NumScalarType (IntegralNumType (TypeInt _)))) <- aType :: AType a
= do
let nm = "x" ++ show n -- we get to actually name things
tynm <- Yices.mkType c "int"
d <- Yices.mkVarDecl c nm tynm
- go f (n + 1) (M.insert nm (YType ty, d) g)
+ go f (n - 1) (M.insert nm (YType ty, d) g)
-- Booleans
go (OLam (f :: OpenFun (env, a) t)) n g
- | ty@(NonNumScalarType (TypeBool _)) <- scalarType :: ScalarType a
+ | ty@(AScalarType (NonNumScalarType (TypeBool _))) <- aType :: AType a
= do
let nm = "x" ++ show n
d <- Yices.mkBoolDecl c nm
- go f (n + 1) (M.insert nm (YType ty, d) g)
+ go f (n - 1) (M.insert nm (YType ty, d) g)
-- Bit vectors
go (OLam (f :: OpenFun (env, a) t)) n g
- | ty@(NumScalarType (IntegralNumType (TypeVectorBool _))) <- scalarType :: ScalarType a
+ | ty@(AScalarType (NumScalarType (IntegralNumType (TypeVectorBool _)))) <- aType :: AType a
= do
let nm = "x" ++ show n
-- TODO: hack, no size information for bit vectors yet.
-- TODO: show bvs in a better form.
tynm <- Yices.mkBitVectorType c (fromIntegral $ 8 * sizeOf (undefined :: Word))
d <- Yices.mkVarDecl c nm tynm
- go f (n + 1) (M.insert nm (YType ty, d) g)
+ go f (n - 1) (M.insert nm (YType ty, d) g)
+ -- Uninterpreted functions
+ go (OLam (f :: OpenFun (env, a) t)) n g
+ | ty@(AFunctionType
+ [a]
+ r
+ ) <- aType :: AType a
+ = do let nm = "f" ++ show n -- we get to actually name things
+ argty <- toBuiltInYicesType c a
+ resty <- toBuiltInYicesType c r
+ tynm <- Yices.mkFunctionType c [argty] resty
+ d <- Yices.mkVarDecl c nm tynm
+ go f (n - 1) (M.insert nm (YType ty, d) g)
go _ _ _ = error "Yices.execF: don't know how to bind variables of this type yet"
+
+-- Only built in types.
+-- number, real, int, nat, bool, any
+toBuiltInYicesType :: Yices.Context -> ScalarType a -> IO Yices.Type
+toBuiltInYicesType c a = case a of
+ (NumScalarType (IntegralNumType (TypeInt _))) -> Yices.mkType c "int"
+ (NonNumScalarType (TypeBool _)) -> Yices.mkType c "bool"
+ _ -> error $ "Don't know how to bind this type yet: " ++ show a
+
+-- TODO: map ScalarTypes to yices strings.
+
-- | Execute an expression with free variables.
--
-- /TODO:/
@@ -1085,6 +1189,22 @@ exec c (Var i) = do
Nothing -> error "Undefined variable"
Just d -> Yices.mkVarFromDecl c d
+-- Application
+exec c (VarFn i e) = do
+ let n = "f" ++ show (idxToInt i)
+ v <- Yices.getVarDeclFromName c n -- sneaky. using Yices environment. TODO: use YEnv
+-- print n
+
+ -- get our yices function
+ yf <- case v of
+ Nothing -> error $ "Undefined variable: " ++ show n
+ Just d -> Yices.mkVarFromDecl c d
+
+ -- compile the expression
+ ye <- exec c e
+
+ Yices.mkApp c yf [ye]
+
-- Conditionals
exec c (OCond b t e) = do
eb <- exec c b
diff --git a/Yices/Painless/Type.hs b/Yices/Painless/Type.hs
index ad9bfb4..791e352 100644
--- a/Yices/Painless/Type.hs
+++ b/Yices/Painless/Type.hs
@@ -214,6 +214,12 @@ data ScalarType a where
NumScalarType :: NumType a -> ScalarType a
NonNumScalarType :: NonNumType a -> ScalarType a
+-- | All Yices types: functions over scalar types, or scalar types.
+data AType a where
+ AFunctionType :: [ScalarType t] -> ScalarType r -> AType (t -> r)
+ -- todo: tuples
+ AScalarType :: ScalarType a -> AType a
+
-- Showing type names
--
@@ -266,6 +272,7 @@ instance Show (ScalarType a) where
-- Querying scalar type representations
--
+
-- |Integral types
--
class (IsScalar a, IsNum a, IsBounded a) => IsIntegral a where
@@ -516,6 +523,17 @@ instance IsBounded CSChar where
instance IsBounded CUChar where
boundedType = NonNumBoundedType nonNumType
+-- | All types we can bind
+class Typeable a => IsAType a where
+ aType :: AType a
+
+instance IsAType Int where
+ aType = AScalarType scalarType
+
+instance (IsScalar a, IsScalar b) => IsAType (a -> b) where
+ aType = AFunctionType [scalarType] scalarType
+ -- todo: tuples
+
-- |All scalar type
--
class Typeable a => IsScalar a where
diff --git a/tests/examples/ex24.hs b/tests/examples/ex24.hs
deleted file mode 100644
index 6327503..0000000
--- a/tests/examples/ex24.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-import Yices.Painless.Language
-
-main = print =<< solve p
-
-data S = S1 | S2 | S3
- deriving (Show, Enum)
-
-p x1 x2 x3 x4 =
- and
- [ (/=*) x1 x2
- , (/=*) x1 x3
- , (/=*) x1 x4
- , (/=*) x2 x3
- , (/=*) x2 x4
- , (/=*) x3 x4
- ]
diff --git a/tests/examples/ex5.ys b/tests/examples/ex5.ys
deleted file mode 100644
index e813861..0000000
--- a/tests/examples/ex5.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-
-(define-type pc (scalar sleeping trying critical))
-(define f::(-> pc pc))
-(define g::(-> pc pc))
-(define x1::pc)
-(define x2::pc)
-(define x3::pc)
-(define x4::pc)
-(define x5::pc)
-(define x6::pc)
-
-
-
-(assert (/= (g (f x1)) (g (f x2))))
-(assert (= x1 x3))
-(assert (= x1 x4))
-(assert (= x3 x2))
-
diff --git a/tests/examples/ex6.ys b/tests/examples/ex6.ys
deleted file mode 100644
index 0bd00f3..0000000
--- a/tests/examples/ex6.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-
-(define-type pc (scalar sleeping trying critical))
-(define f::(-> pc pc))
-(define g::(-> pc pc))
-(define x1::pc)
-(define x2::pc)
-(define x3::pc)
-(define x4::pc)
-(define x5::pc)
-(define x6::pc)
-
-
-
-(assert (= x1 x3))
-(assert (= x1 x4))
-(assert (= x3 x2))
-(assert (/= (g (f x1)) (g (f x2))))
-
diff --git a/yices-painless.cabal b/yices-painless.cabal
index b215e4d..2aa8722 100644
--- a/yices-painless.cabal
+++ b/yices-painless.cabal
@@ -1,5 +1,5 @@
Name: yices-painless
-Version: 0.1.1
+Version: 0.1.2
Synopsis: An embedded language for programming the Yices SMT solver
Description:
This library defines an embedded language in Haskell for programming
@@ -13,14 +13,16 @@ Description:
MaxSMT (and, dually, unsat cores) and is competitive as an ordinary
SAT and MaxSAT solver.
.
- The embedded language embeds both terms and types into Haskell, via
- a typed higher-order abstract syntax representation. Propositions in
- the embedding are represented as (typed) pure expressions.
+ The embedded language embeds both terms, functions and types into
+ Haskell, via a typed higher-order abstract syntax representation.
+ Propositions in the embedding are represented as (typed) pure
+ expressions.
.
Solution variables in the proposition (notionally, free variables)
are bound an the outermost lambda term. Propositions constructed
from logical primitives can then be executed by the solver to yield
a satisfying assignment to those free variables in the proposition.
+ Uninterpreted functions may be introduced via variables as well.
.
More information about Yices:
.