packages feed

smtlib2 0.2 → 0.3

raw patch · 6 files changed

+127/−105 lines, 6 files

Files

Language/SMTLib2.hs view
@@ -56,6 +56,7 @@          interpolationGroup,          assertInterp,          getInterpolant,+         interpolate,          -- * Expressions          var,varNamed,varNamedAnn,varAnn,argVars,argVarsAnn,argVarsAnnNamed,          untypedVar,untypedNamedVar,
Language/SMTLib2/Internals.hs view
@@ -48,10 +48,11 @@   SMTGetUnsatCore :: SMTRequest [ClauseId]   SMTSimplify :: SMTType t => SMTExpr t -> SMTRequest (SMTExpr t)   SMTGetInterpolant :: [InterpolationGroup] -> SMTRequest (SMTExpr Bool)+  SMTInterpolate :: [SMTExpr Bool] -> SMTRequest [SMTExpr Bool]   SMTComment :: String -> SMTRequest ()   SMTExit :: SMTRequest ()   SMTApply :: Tactic -> SMTRequest [SMTExpr Bool]-  SMTNameExpr :: String -> SMTExpr t -> SMTRequest Integer+  SMTNameExpr :: SMTType t => String -> SMTExpr t -> SMTRequest Integer   SMTNewInterpolationGroup :: SMTRequest InterpolationGroup   SMTNewClauseId :: SMTRequest ClauseId   deriving Typeable@@ -109,7 +110,7 @@   mangle :: Mangling t  -- | A type class for all types which support arithmetic operations in SMT-class (SMTValue t,Num t) => SMTArith t+class (SMTValue t,Num t,SMTAnnotation t ~ ()) => SMTArith t  -- | Lifts the 'Ord' class into SMT class (SMTType t) => SMTOrd t where@@ -208,7 +209,7 @@   Exists :: Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool   Let :: Integer -> [SMTExpr Untyped] -> SMTExpr b -> SMTExpr b   App :: (Args arg,SMTType res) => SMTFunction arg res -> arg -> SMTExpr res-  Named :: SMTExpr a -> String -> Integer -> SMTExpr a+  Named :: SMTExpr a -> Integer -> SMTExpr a   InternalObj :: (SMTType t,Typeable a,Ord a,Show a) => a -> SMTAnnotation t -> SMTExpr t   UntypedExpr :: SMTType t => SMTExpr t -> SMTExpr Untyped   UntypedExprValue :: SMTValue t => SMTExpr t -> SMTExpr UntypedValue@@ -221,7 +222,7 @@                       , bvSortUntyped :: Bool }              | ArraySort [a] a              | NamedSort String [a]-             deriving (Eq,Show,Functor,Foldable,Traversable)+             deriving (Eq,Ord,Show,Functor,Foldable,Traversable)  type Sort = Fix Sort' @@ -231,16 +232,16 @@            | BVValue { bvValueWidth :: Integer                      , bvValueValue :: Integer }            | ConstrValue String [Value] (Maybe (String,[Sort]))-           deriving (Eq,Show)+           deriving (Eq,Ord,Show)  data SMTFunction arg res where   SMTEq :: SMTType a => SMTFunction [SMTExpr a] Bool   SMTMap :: (Liftable arg,SMTType res,Args i) => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res)   SMTFun :: (Args arg,SMTType res) => Integer -> SMTAnnotation res -> SMTFunction arg res   SMTBuiltIn :: (Liftable arg,SMTType res) => String -> SMTAnnotation res -> SMTFunction arg res-  SMTOrd :: (SMTType a) => SMTOrdOp -> SMTFunction (SMTExpr a,SMTExpr a) Bool-  SMTArith :: (SMTType a,Num a) => SMTArithOp -> SMTFunction [SMTExpr a] a-  SMTMinus :: (SMTType a,Num a) => SMTFunction (SMTExpr a,SMTExpr a) a+  SMTOrd :: (SMTArith a) => SMTOrdOp -> SMTFunction (SMTExpr a,SMTExpr a) Bool+  SMTArith :: (SMTArith a) => SMTArithOp -> SMTFunction [SMTExpr a] a+  SMTMinus :: (SMTArith a) => SMTFunction (SMTExpr a,SMTExpr a) a   SMTIntArith :: SMTIntArithOp -> SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer   SMTDivide :: SMTFunction (SMTExpr Rational,SMTExpr Rational) Rational   SMTNeg :: (SMTType a,Num a) => SMTFunction (SMTExpr a) a@@ -777,7 +778,7 @@  class TypeableNat n where   typeOfNat :: Proxy n -> TypeRep-  typeOfNat p = Prelude.foldl+  typeOfNat p = foldl                 (\c _ -> mkTyConApp (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'S") [c])                 (mkTyConApp (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'Z") [])                 (genericReplicate (reflectNat p 0) ())@@ -858,7 +859,7 @@     reifyNat' 0 f = f (Proxy :: Proxy Z)     reifyNat' n f = reifyNat' (n-1) (\(_::Proxy n) -> f (Proxy::Proxy (S n))) -data BitVector (b :: BVKind) = BitVector Integer deriving (Eq,Ord)+data BitVector (b :: BVKind) = BitVector Integer deriving (Eq,Ord,Typeable)  instance TypeableBVKind k => Typeable (BitVector k) where   typeOf _ = mkTyConApp@@ -899,15 +900,16 @@ reifySum :: (Num a,Ord a) => a -> a -> (forall n1 n2. (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2))                                         => Proxy n1 -> Proxy n2 -> Proxy (Add n1 n2) -> r) -> r reifySum n1 n2 f-  | n1 < 0 || n2 < 0 = error "smtlib2: Cann only reify numbers >= 0."+  | n1 < 0 || n2 < 0 = error "smtlib2: Can only reify numbers >= 0."   | otherwise = reifySum' n1 n2 f   where     reifySum' :: (Num a,Ord a) => a -> a                  -> (forall n1 n2. (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2))                      => Proxy n1 -> Proxy n2 -> Proxy (Add n1 n2) -> r) -> r     reifySum' 0 n2' f' = reifyNat n2' $ \(_::Proxy i) -> f' (Proxy::Proxy Z) (Proxy::Proxy i) (Proxy::Proxy i)-    reifySum' n1' n2' f' = reifySum' (n1'-1) n2' $ \(_::Proxy i1) (_::Proxy i2) (_::Proxy i3)-                                                   -> f' (Proxy::Proxy (S i1)) (Proxy::Proxy i2) (Proxy::Proxy (S i3))+    reifySum' n1' n2' f' = reifySum' (n1'-1) n2' $+                           \(_::Proxy i1) (_::Proxy i2) (_::Proxy (Add i1 i2))+                           -> f' (Proxy::Proxy (S i1)) (Proxy::Proxy i2) (Proxy::Proxy (S (Add i1 i2)))  reifyExtract :: (Num a,Ord a) => a -> a -> a                 -> (forall n1 n2 n3 n4. (TypeableNat n1,TypeableNat n2,TypeableNat n3,TypeableNat n4,Add n4 n2 ~ S n3)@@ -1079,13 +1081,11 @@                                                 showsPrec 11 fun .                                                 showChar ' ' .                                                 strArgs)-showExpr p (Named expr name nc) = let strExpr = showExpr 11 expr-                                  in showParen (p>10) (showString "Named " .-                                                       strExpr .-                                                       showChar ' ' .-                                                       showsPrec 11 name .-                                                       showChar ' ' .-                                                       showsPrec 11 nc)+showExpr p (Named expr i) = let strExpr = showExpr 11 expr+                            in showParen (p>10) (showString "Named " .+                                                 strExpr .+                                                 showChar ' ' .+                                                 showsPrec 11 i) showExpr p (InternalObj obj ann) = showParen (p>10) (showString "InternalObj " .                                                      showsPrec 11 obj .                                                      showChar ' ' .@@ -1170,7 +1170,7 @@ quantificationLevel (Exists lvl _ _) = lvl+1 quantificationLevel (Let lvl _ _) = lvl+1 quantificationLevel (App _ arg) = maximum $ fmap quantificationLevel $ fromArgs arg-quantificationLevel (Named expr _ _) = quantificationLevel expr+quantificationLevel (Named expr _) = quantificationLevel expr quantificationLevel (UntypedExpr e) = quantificationLevel e quantificationLevel (UntypedExprValue e) = quantificationLevel e quantificationLevel _ = 0
Language/SMTLib2/Internals/Instances.hs view
@@ -65,7 +65,7 @@ extractAnnotation (Forall _ _ _) = () extractAnnotation (Exists _ _ _) = () extractAnnotation (Let _ _ f) = extractAnnotation f-extractAnnotation (Named x _ _) = extractAnnotation x+extractAnnotation (Named x _) = extractAnnotation x extractAnnotation (App f arg) = inferResAnnotation f (extractArgAnnotation arg) extractAnnotation (InternalObj _ ann) = ann extractAnnotation (UntypedExpr (expr::SMTExpr t)) = ProxyArg (undefined::t) (extractAnnotation expr)@@ -1274,7 +1274,7 @@                      (fmap (\s -> withSort mp s ProxyArg) args) f     Nothing -> error $ "smtlib2: Datatype "++name++" not defined." -withNumSort :: DataTypeInfo -> Sort -> (forall t. (SMTType t,Num t) => t -> SMTAnnotation t -> r) -> Maybe r+withNumSort :: DataTypeInfo -> Sort -> (forall t. (SMTArith t) => t -> SMTAnnotation t -> r) -> Maybe r withNumSort _ (Fix IntSort) f = Just $ f (undefined::Integer) () withNumSort _ (Fix RealSort) f = Just $ f (undefined::Rational) () withNumSort _ _ _ = Nothing@@ -1330,9 +1330,9 @@   (s',args') <- foldArgsM f s arg   return (s',[ App fun arg'              | arg' <- args' ])-foldExprM f s (Named expr name i) = do+foldExprM f s (Named expr i) = do   (s',exprs') <- foldExprM f s expr-  return (s',[ Named expr' name i+  return (s',[ Named expr' i              | expr' <- exprs' ]) foldExprM f s (UntypedExpr e) = do   (s',exprs') <- foldExprM f s e@@ -1559,9 +1559,9 @@   x -> x compareExprs (App _ _) _ = LT compareExprs _ (App _ _) = GT-compareExprs (Named _ n1 i1) (Named _ n2 i2) = compare (n1,i1) (n2,i2)-compareExprs (Named _ _ _) _ = LT-compareExprs _ (Named _ _ _) = GT+compareExprs (Named _ i1) (Named _ i2) = compare i1 i2+compareExprs (Named _ _) _ = LT+compareExprs _ (Named _ _) = GT compareExprs (InternalObj o1 ann1) (InternalObj o2 ann2) = case compare (typeOf o1) (typeOf o2) of       EQ -> case compare (typeOf ann1) (typeOf ann2) of         EQ -> case cast (o2,ann2) of@@ -1607,9 +1607,9 @@   (Let l1 a1 f1,Let l2 a2 f2) -> if l1==l2 && a1==a2                                  then eqExpr f1 f2                                  else Nothing-  (Named e1 n1 nc1,Named e2 n2 nc2) -> if n1==n2 && nc1 == nc2-                                       then eqExpr e1 e2-                                       else Nothing+  (Named e1 i1,Named e2 i2) -> if i1==i2+                               then eqExpr e1 e2+                               else Nothing   (App f1 arg1,App f2 arg2) -> case cast f2 of       Nothing -> Nothing       Just f2' -> case cast arg2 of
Language/SMTLib2/Internals/Interface.hs view
@@ -231,6 +231,9 @@ getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool) getInterpolant grps = smtBackend $ \b -> smtHandle b (SMTGetInterpolant grps) +interpolate :: Monad m => [SMTExpr Bool] -> SMT' m [SMTExpr Bool]+interpolate exprs = smtBackend $ \b -> smtHandle b (SMTInterpolate exprs)+ -- | Set an option for the underlying SMT solver setOption :: Monad m => SMTOption -> SMT' m () setOption opt = smtBackend $ \b -> smtHandle b (SMTSetOption opt)@@ -647,7 +650,7 @@          => String -> SMTExpr a -> SMT' m (SMTExpr a,SMTExpr a) named name expr = do   i <- smtBackend $ \b -> smtHandle b (SMTNameExpr name expr)-  return (Named expr name i,Var i (extractAnnotation expr))+  return (Named expr i,Var i (extractAnnotation expr))  -- | Like `named`, but defaults the name to "named". named' :: (SMTType a,SMTAnnotation a ~ (),Monad m)
Language/SMTLib2/Pipe.hs view
@@ -6,7 +6,7 @@         withPipe,         exprToLisp,         exprToLispWith,-        lispToExpr,+        lispToExpr,lispToExprWith,         sortToLisp,lispToSort,         renderExpr,         renderExpr',@@ -195,6 +195,10 @@   = Left $ L.List [L.Symbol "get-interpolant"                   ,L.List [ L.Symbol $ T.pack ("i"++show g) | InterpolationGroup g <- grps ]                   ]+renderSMTRequest _ getName dts (SMTInterpolate exprs)+  = Left $ L.List $ (L.Symbol "get-interpolant"):+    [ exprToLisp expr getName dts+    | expr <- exprs ] renderSMTRequest _ _ _ (SMTSetOption opt)   = Left $ L.List $ [L.Symbol "set-option"]     ++(case opt of@@ -262,7 +266,7 @@   return ((),pipe { smtState = (smtState pipe) { declaredDataTypes = ndts } }) handleRequest pipe (SMTDeclareSort name arity) = return ((),pipe) handleRequest pipe (SMTDeclareFun info)-  = let (v,name,nst) = smtStateAddFun info (smtState pipe)+  = let (v,_,nst) = smtStateAddFun info (smtState pipe)     in return (v,pipe { smtState = nst }) handleRequest pipe (SMTDefineFun name (_::Proxy arg) argAnn (body::SMTExpr res)) = do   let finfo = FunInfo { funInfoProxy = Proxy::Proxy (arg,res)@@ -285,6 +289,19 @@        gcast (Just $ Fix BoolSort) 0 val of     Just (Just x) -> return (x,pipe)     _ -> error $ "smtlib2: Failed to parse get-interpolant result: "++show val+handleRequest pipe (SMTInterpolate exprs) = case exprs of+  [] -> return ([],pipe)+  e:es -> do+    resp <- mapM (\_ -> do+                     val <- parseResponse pipe+                     case lispToExpr commonFunctions+                          (findName $ smtState pipe)+                          (declaredDataTypes $ smtState pipe)+                          gcast (Just $ Fix BoolSort) 0 val of+                      Just (Just x) -> return x+                      _ -> error $ "smtlib2: Failed to parse get-interpolant result: "++show val+                 ) es+    return (resp,pipe) handleRequest pipe (SMTSetOption opt) = return ((),pipe) handleRequest pipe (SMTSetLogic name) = return ((),pipe) handleRequest pipe SMTGetProof = do@@ -396,13 +413,14 @@                        _ -> error $ "smtlib2: Couldn't parse goal "++show expr                  _ -> error $ "smtlib2: Couldn't parse goal description "++show val                ) goals,pipe)-handleRequest pipe (SMTNameExpr name expr) = do-  return (nc,pipe { smtState = nst })+handleRequest pipe (SMTNameExpr name (expr::SMTExpr t)) = do+  return (i,pipe { smtState = nst })   where-    nc = case Map.lookup name (nameCount $ smtState pipe) of-      Just n -> n-      Nothing -> 0-    nst = (smtState pipe) { nameCount = Map.insert name (nc+1) (nameCount $ smtState pipe) }+    finfo = FunInfo { funInfoProxy = Proxy::Proxy ((),t)+                    , funInfoArgAnn = ()+                    , funInfoResAnn = extractAnnotation expr+                    , funInfoName = Just name }+    (i,_,nst) = smtStateAddFun finfo (smtState pipe) handleRequest pipe SMTNewInterpolationGroup = do   return (InterpolationGroup igrp,pipe { smtState = nst })   where@@ -425,6 +443,9 @@   Unknown -> Just "unknown" renderSMTResponse getName dts (SMTGetInterpolant grps) expr   = Just $ renderExpr' getName dts expr+renderSMTResponse getName dts (SMTInterpolate _) exprs+  = Just $ unwords [ renderExpr' getName dts expr+                   | expr <- exprs ] renderSMTResponse getName dts SMTGetProof proof   = Just $ renderExpr' getName dts proof renderSMTResponse getName dts (SMTSimplify _) expr@@ -436,7 +457,12 @@     [exprToLisp goal getName dts     | goal <- goals ] renderSMTResponse _ _ SMTGetUnsatCore core = Just (show core)-renderSMTResponse _ _ SMTGetModel mdl = Just (show mdl)+renderSMTResponse getName dts SMTGetModel mdl+  = Just $ "(model"++concat assignments++")"+  where+    assignments = [ "\n  ("++getName fun++" "+++                    renderExpr' getName dts expr++")"+                  | (fun,(_,_,expr)) <- Map.toList $ modelFunctions mdl ] renderSMTResponse _ _ _ _ = Nothing  -- | Spawn a new SMT solver process and create a pipe to communicate with it.@@ -589,11 +615,12 @@     in if Prelude.null x'        then l        else L.List $ l:x'-exprToLispWith objs (Named expr name nc) mp dts+exprToLispWith objs (Named expr idx) mp dts   = let expr' = exprToLispWith objs expr mp dts+        name = mp idx     in L.List [L.Symbol "!",expr'               ,L.Symbol ":named"-              ,L.Symbol $ T.pack $ escapeName (Left (name,nc))]+              ,L.Symbol $ T.pack name] exprToLispWith objs (InternalObj obj ann) _ _ = objs obj exprToLispWith objs (UntypedExpr expr) mp dts   = exprToLispWith objs expr mp dts@@ -973,7 +1000,24 @@               -> Integer -- ^ The current quantification level               -> L.Lisp -- ^ The lisp expression to parse               -> Maybe b-lispToExpr fun bound dts f expected lvl l = case lispToValue dts expected l of+lispToExpr = lispToExprWith lispToExpr++lispToExprWith :: (forall b. FunctionParser+                   -> (T.Text -> Maybe (SMTExpr Untyped))+                   -> DataTypeInfo+                   -> (forall a. SMTType a => SMTExpr a -> b)+                   -> Maybe Sort+                   -> Integer+                   -> L.Lisp -> Maybe b) -- ^ Recursive descend function+                  -> FunctionParser -- ^ The parser to use for function symbols+                  -> (T.Text -> Maybe (SMTExpr Untyped)) -- ^ How to handle variable names+                  -> DataTypeInfo -- ^ Information about declared data types+                  -> (forall a. SMTType a => SMTExpr a -> b) -- ^ A function to apply to the resulting SMT expression+                  -> Maybe Sort -- ^ If you know the sort of the expression, you can pass it here.+                  -> Integer -- ^ The current quantification level+                  -> L.Lisp -- ^ The lisp expression to parse+                  -> Maybe b+lispToExprWith recp fun bound dts f expected lvl l = case lispToValue dts expected l of   Just val -> valueToHaskell dts               (\_ (val'::t) ann                -> asValueType (undefined::t) ann $@@ -985,11 +1029,11 @@       Nothing -> Nothing       Just subst -> entype (\expr -> Just $ f expr) subst     L.List [L.Symbol "forall",L.List args',body]-      -> fmap f $ quantToExpr Forall fun bound dts args' lvl body+      -> fmap f $ quantToExpr recp Forall fun bound dts args' lvl body     L.List [L.Symbol "exists",L.List args',body]-      -> fmap f $ quantToExpr Exists fun bound dts args' lvl body+      -> fmap f $ quantToExpr recp Exists fun bound dts args' lvl body     L.List [L.Symbol "let",L.List args',body]-      -> parseLet fun bound dts f expected args' lvl body+      -> parseLet recp fun bound dts f expected args' lvl body     L.List [L.Symbol "_",L.Symbol "as-array",fsym]       -> case parseFun fun fsym fun dts of       Nothing -> Nothing@@ -1020,9 +1064,9 @@                         [] -> Just $ App rfun rargs                         _ -> Nothing) of                Just e -> f e-               Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym++": "++show arg_tps++" ("++show args'++")."+               Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym++": "++show arg_tps++" (Expected: "++show args'++")."       Just (DefinedParser arg_tps _ parse) -> do-        nargs <- mapM (\(el,tp) -> lispToExpr fun bound dts mkUntyped (Just tp) lvl el)+        nargs <- mapM (\(el,tp) -> recp fun bound dts mkUntyped (Just tp) lvl el)                  (zip args' arg_tps)         parse $ \(rfun :: SMTFunction arg res)                 -> case (do@@ -1032,16 +1076,16 @@                               [] -> Just $ App rfun rargs                               _ -> Nothing) of                      Just e -> f e-                     Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym+                     Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym++" (Expected: "++show arg_tps++")"     _ -> Nothing   where     lispToExprs constr exprs = do-      res <- mapM (\arg -> lispToExpr fun bound dts mkUntyped Nothing lvl arg) exprs+      res <- mapM (\arg -> recp fun bound dts mkUntyped Nothing lvl arg) exprs       let sorts = fmap (entype exprSort) res       if constr sorts         then return res         else (case generalizeSorts sorts of-                 Just sorts' -> mapM (\(arg,sort') -> lispToExpr fun bound dts mkUntyped (Just sort') lvl arg) (zip exprs sorts')+                 Just sorts' -> mapM (\(arg,sort') -> recp fun bound dts mkUntyped (Just sort') lvl arg) (zip exprs sorts')                  Nothing -> return res)     preprocessHack (L.List ((L.Symbol "concat"):args)) = foldl1 (\expr arg -> L.List [L.Symbol "concat",expr,arg]) args     preprocessHack x = x@@ -1073,12 +1117,19 @@ exprSort :: SMTType a => SMTExpr a -> Sort exprSort (expr::SMTExpr a) = getSort (undefined::a) (extractAnnotation expr) -quantToExpr :: (Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool)+quantToExpr :: (forall b. FunctionParser+                -> (T.Text -> Maybe (SMTExpr Untyped))+                -> DataTypeInfo+                -> (forall a. SMTType a => SMTExpr a -> b)+                -> Maybe Sort+                -> Integer+                -> L.Lisp -> Maybe b) -- ^ Recursive descend function+            -> (Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool)             -> FunctionParser             -> (T.Text -> Maybe (SMTExpr Untyped))             -> DataTypeInfo             -> [L.Lisp] -> Integer -> L.Lisp -> Maybe (SMTExpr Bool)-quantToExpr con fun bound dts args lvl body = do+quantToExpr recp con fun bound dts args lvl body = do   argLst <- mapM (\el -> case el of                    L.List [L.Symbol name,tp] -> do                      sort <- lispToSort tp@@ -1090,21 +1141,28 @@       bound' name = case Map.lookup name argMp of         Just (idx,tp) -> Just (QVar lvl idx tp)         Nothing -> bound name-  lispToExpr fun bound' dts+  recp fun bound' dts     (\body' -> case cast body' of       Just body'' -> con lvl (fmap snd argLst) body''     ) (Just $ Fix BoolSort) (lvl+1) body -parseLet :: FunctionParser+parseLet :: (forall b. FunctionParser+             -> (T.Text -> Maybe (SMTExpr Untyped))+             -> DataTypeInfo+             -> (forall a. SMTType a => SMTExpr a -> b)+             -> Maybe Sort+             -> Integer+             -> L.Lisp -> Maybe b) -- ^ Recursive descend function+         -> FunctionParser          -> (T.Text -> Maybe (SMTExpr Untyped))          -> DataTypeInfo          -> (forall a. SMTType a => SMTExpr a -> b)          -> Maybe Sort          -> [L.Lisp] -> Integer -> L.Lisp -> Maybe b-parseLet fun bound dts app expected args lvl body = do+parseLet recp fun bound dts app expected args lvl body = do   argLst <- mapM (\el -> case el of                    L.List [L.Symbol name,expr] -> do-                     expr' <- lispToExpr fun bound dts UntypedExpr Nothing (lvl+1) expr+                     expr' <- recp fun bound dts UntypedExpr Nothing (lvl+1) expr                      return (name,expr')                    _ -> Nothing                  ) args@@ -1113,50 +1171,10 @@       bound' name = case Map.lookup name argMp of         Just (idx,tp) -> Just (QVar lvl idx tp)         Nothing -> bound name-  lispToExpr fun bound' dts+  recp fun bound' dts     (\body' -> app (Let lvl (fmap snd argLst) body')     ) expected (lvl+1) body-{--data LetStruct where-  LetStruct :: SMTType a => SMTAnnotation a -> SMTExpr a -> (SMTExpr a -> LetStruct) -> LetStruct-  EndLet :: SMTType a => SMTExpr a -> LetStruct -parseLetStruct :: FunctionParser-                  -> (T.Text -> Maybe (SMTExpr Untyped))-                  -> DataTypeInfo-                  -> Maybe Sort-                  -> [L.Lisp] -> L.Lisp -> LetStruct-parseLetStruct fun bound tps expected (L.List [L.Symbol name,expr]:rest) arg-  = case lispToExpr fun bound tps-         (\expr' -> LetStruct (extractAnnotation expr') expr' $-                    \sym -> parseLetStruct fun-                            (\txt -> if txt==name-                                     then Just $ mkUntyped sym-                                     else bound txt) tps expected rest arg-         ) Nothing expr of-      Nothing -> error $ "smtlib2: Failed to parse argument in let-expression "++show expr-      Just x -> x-parseLetStruct fun bound tps expected [] arg-  = case lispToExpr fun bound tps EndLet expected arg of-    Nothing -> error $ "smtlib2: Failed to parse body of let-expression: "++show arg-    Just x -> x-parseLetStruct _ _ _ _ (el:_) _ = error $ "smtlib2: Invalid entry "++show el++" in let construct."--extractType :: (forall a. SMTType a => a -> b) -> LetStruct -> b-extractType f (EndLet x) = f (getUndef x)-extractType f (LetStruct _ expr g) = extractType f (g expr)--convertLetStructT :: SMTType a => LetStruct -> SMTExpr a-convertLetStructT (EndLet x) = case gcast x of-  Just x' -> x'-  Nothing -> error "smtlib2: Type error while converting let structure."-convertLetStructT (LetStruct ann x g) = Let ann x (\sym -> convertLetStructT (g sym))--convertLetStruct :: (forall a. SMTType a => SMTExpr a -> b) -> LetStruct -> b-convertLetStruct f x-  = extractType-    (\(_::t) -> f (convertLetStructT x :: SMTExpr t)) x--} withFirstArgSort :: DataTypeInfo -> L.Lisp -> [Sort] -> (forall t. SMTType t => t -> SMTAnnotation t -> a) -> a withFirstArgSort dts _ (s:rest) f = case s of   Fix (BVSort i False) -> if any (\sort -> case sort of@@ -1287,9 +1305,9 @@   where     p :: L.Lisp -> SMTOrdOp -> DataTypeInfo -> Maybe FunctionParser'     p sym op dts = Just $ OverloadedParser allEqConstraint (const $ Just $ getSort (undefined::Bool) ()) $-                   \sort_arg _ f -> withFirstArgSort dts sym sort_arg $-                                    \(_::t) _-                                    -> Just $ f (SMTOrd op :: SMTFunction (SMTExpr t,SMTExpr t) Bool)+                   \[sort_arg,_] _ f -> withNumSort dts sort_arg $+                                        \(_::t) _+                                         -> f (SMTOrd op :: SMTFunction (SMTExpr t,SMTExpr t) Bool)  arithOpParser = FunctionParser $ \sym _ dts -> case sym of   L.Symbol "+" -> Just $ OverloadedParser allEqConstraint (\sorts -> Just (head sorts)) $@@ -1436,13 +1454,13 @@     -> Just $ OverloadedParser (const True)        (\sort_arg -> case sort_arg of            (Fix (ArraySort _ vsort):_) -> Just vsort-           _ -> error "smtlib2: Wrong arguments for select function.") $+           _ -> error $ "smtlib2: Wrong arguments for select function ("++show sort_arg++").") $        \sort_arg sort_ret f -> case sort_arg of          (Fix (ArraySort isort1 _):_)            -> withSorts dts isort1 $               \(_::i) _ -> withSort dts sort_ret $                            \(_::v) _ -> Just $ f (SMTSelect::SMTFunction (SMTExpr (SMTArray i v),i) v)-         _ -> error "smtlib2: Wrong arguments for select function."+         _ -> error $ "smtlib2: Wrong arguments for select function ("++show sort_arg++")."   _ -> Nothing  storeParser = FunctionParser $ \sym _ dts -> case sym of
smtlib2.cabal view
@@ -1,5 +1,5 @@ Name:           smtlib2-Version:        0.2+Version:        0.3 Author:         Henning Günther <guenther@forsyte.at> Maintainer:     guenther@forsyte.at Synopsis:       A type-safe interface to communicate with an SMT solver.