packages feed

tip-lib (empty) → 0.1

raw patch · 45 files changed

+5567/−0 lines, 45 filesdep +arraydep +basedep +containerssetup-changed

Dependencies added: array, base, containers, geniplate-mirror, mtl, optparse-applicative, pretty, pretty-show, split, tip-lib

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Dan Rosén++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Dan Rosén nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ executable/Main.hs view
@@ -0,0 +1,78 @@+module Main where++import System.Environment++import Tip.Parser+import Tip.Pretty.SMT as SMT+import Tip.Pretty.Why3 as Why3+import Tip.Pretty.Isabelle as Isabelle+import Tip.Pretty.Haskell as HS+import Tip.Pretty+import Tip.CallGraph++import Tip.Passes+import Tip.Lint+import Tip.Fresh+import Tip.Core+import Options.Applicative++import Control.Monad++data OutputMode = Haskell | Why3 | CVC4 | Isabelle | TIP++parseOutputMode :: Parser OutputMode+parseOutputMode =+      flag' Haskell (long "haskell" <> help "Haskell output")+  <|> flag' Why3 (long "why" <> help "WhyML output")+  <|> flag' CVC4 (long "smtlib" <> help "SMTLIB output (CVC4-compatible)")+  <|> flag' Isabelle (long "isabelle" <> help "Isabelle output")+  <|> flag  TIP TIP (long "tip" <> help "TIP output (default)")++optionParser :: Parser ([StandardPass], Maybe String, OutputMode)+optionParser =+  (,,) <$> parsePasses <*> parseFile <*> parseOutputMode+  where+    parseFile =+      fmap Just (strArgument (metavar "FILENAME")) <|> pure Nothing++main :: IO ()+main = do+  (passes, files, mode) <-+    execParser $+      info (helper <*> optionParser)+        (fullDesc <>+         progDesc "Transform a TIP problem" <>+         header "tip - a tool for processing TIP problems")+  case files of+    Nothing ->+      handle passes mode =<< getContents+    Just f ->+      handle passes mode =<< readFile f++handle :: [StandardPass] -> OutputMode -> String -> IO ()+handle passes mode s =+  case parse s of+    Left err  -> error $ "Parse failed: " ++ err+    Right thy -> do+      let fmap_pp f = fmap (show . f)+      let show_passes c = fmap (\ s -> c ++ show passes ++ "\n" ++ s)+      let pipeline =+            case mode of+              CVC4 ->+                fmap_pp SMT.ppTheory . runPasses+                  (passes +++                  [ LambdaLift, AxiomatizeLambdas+                  , CollapseEqual, RemoveAliases+                  , SimplifyGently, RemoveMatch+                  , SimplifyGently, NegateConjecture+                  , SimplifyGently+                  ])+              Haskell ->+                fmap_pp HS.ppTheory . runPasses passes+              Why3 ->+                fmap_pp Why3.ppTheory . runPasses (passes ++ [CSEMatchWhy3])+              Isabelle ->+                fmap_pp Isabelle.ppTheory . runPasses passes+              TIP ->+                show_passes "; " . fmap_pp SMT.ppTheory . runPasses passes+      putStrLn (freshPass pipeline (lint "parse" thy))
+ src/Tip/CallGraph.hs view
@@ -0,0 +1,61 @@+-- | Calculate the call graph of a theory.+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE RecordWildCards, CPP, DeriveFunctor #-}+module Tip.CallGraph where++#include "errors.h"+import Tip.Scope+import Tip.Utils+import Tip.Core+import Tip.Pretty+import qualified Data.Map as Map+import Data.List++type FS = Function :+: Signature++data Block a =+  Block {+    callers :: [FS a],+    callees :: [FS a] }+  deriving (Show, Functor)++flattenBlock :: Block a -> [FS a]+flattenBlock block = callers block ++ callees block++theoryStuff :: Theory a -> [FS a]+theoryStuff Theory{..} = map InL thy_funcs ++ map InR thy_sigs++callGraph :: (PrettyVar a, Ord a) => Theory a -> [Block a]+callGraph thy@Theory{..} =+  [ Map.findWithDefault __ xs m | xs <- top ]+  where+    stuff = theoryStuff thy+    top   = topsort stuff+    tops  = Map.fromList [(x, xs) | xs <- top, x <- xs]+    m     = foldl op Map.empty top+    funcs = Map.fromList [(defines func, func) | func <- stuff]+    op m xs =+      Map.insert xs (Block xs (usort ys \\ xs)) m+      where+        ys =+          concat+            [ flattenBlock (Map.findWithDefault (Block [] []) ys m)+            | x <- xs,+              y <- uses x,+              Just func <- [Map.lookup y funcs],+              Just ys   <- [Map.lookup func tops]]++data CallGraphOpts =+  CallGraphOpts {+    exploreSingleFunctions :: Bool,+    exploreCalleesFirst    :: Bool }++flatCallGraph :: (PrettyVar a, Ord a) => CallGraphOpts -> Theory a -> [[FS a]]+flatCallGraph CallGraphOpts{..} thy =+  nub . filter (not . null) $+  concat [ map callers blocks | exploreSingleFunctions ] ++ concatMap flatten blocks +++  [concat (topsort (theoryStuff thy))]+  where+    blocks = callGraph thy+    flatten block@Block{..} =+      [ callees | exploreCalleesFirst ] ++ [flattenBlock block]
+ src/Tip/Core.hs view
@@ -0,0 +1,441 @@+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, PatternGuards #-}+{-# LANGUAGE ExplicitForAll, FlexibleContexts, FlexibleInstances, TemplateHaskell, MultiParamTypeClasses #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+-- | General functions for constructing and examining Tip syntax.+module Tip.Core(module Tip.Types, module Tip.Core) where++#include "errors.h"+import Tip.Types+import Tip.Fresh+import Tip.Utils+import Tip.Pretty+import Data.Traversable (Traversable)+import Data.Foldable (Foldable)+import qualified Data.Foldable as F+import Data.Generics.Geniplate+import Data.List ((\\))+import Data.Ord+import Control.Monad+import qualified Data.Map as Map+import Control.Applicative ((<|>))++infix  4 ===+-- infixr 3 /\+infixr 2 \/+infixr 1 ==>+infixr 0 ===>++-- * Constructing expressions++(===) :: Expr a -> Expr a -> Expr a+e1 === e2 = Builtin Equal :@: [e1,e2]++(=/=) :: Expr a -> Expr a -> Expr a+e1 =/= e2 = Builtin Distinct :@: [e1,e2]++neg :: Expr a -> Expr a+neg (Builtin op :@: [e1,e2])+  | Equal    <- op = e1 =/= e2+  | Distinct <- op = e1 === e2+neg e+  | Just b <- boolView e = if b then falseExpr else trueExpr+  | otherwise = Builtin Not :@: [e]++(/\) :: Expr a -> Expr a -> Expr a+e1 /\ e2+  | Just b <- boolView e1 = if b then e2 else falseExpr+  | Just b <- boolView e2 = if b then e1 else falseExpr+  | otherwise = Builtin And :@: [e1,e2]++(\/) :: Expr a -> Expr a -> Expr a+e1 \/ e2+  | Just b <- boolView e1 = if b then trueExpr else e2+  | Just b <- boolView e2 = if b then trueExpr else e1+  | otherwise = Builtin Or :@: [e1,e2]++ands :: [Expr a] -> Expr a+ands xs = foldl (/\) trueExpr xs++ors :: [Expr a] -> Expr a+ors xs = foldl (\/) falseExpr xs++(==>) :: Expr a -> Expr a -> Expr a+e1 ==> e2+  | Just a <- boolView e1 = if a then e2 else trueExpr+  | Just b <- boolView e2 = if b then trueExpr else neg e1+  | otherwise = Builtin Implies :@: [e1,e2]++(===>) :: [Expr a] -> Expr a -> Expr a+xs ===> y = foldr (==>) y xs++mkQuant :: Quant -> [Local a] -> Expr a -> Expr a+mkQuant q [] e = e+mkQuant q xs e = Quant NoInfo q xs e++bool :: Bool -> Expr a+bool = literal . Bool++trueExpr :: Expr a+trueExpr  = bool True++falseExpr :: Expr a+falseExpr = bool False++makeIf :: Expr a -> Expr a -> Expr a -> Expr a+makeIf c t f+  | Just b <- boolView c = if b then t else f+  | otherwise = Match c [Case (LitPat (Bool True)) t,Case (LitPat (Bool False)) f]++intLit :: Integer -> Expr a+intLit = literal . Int++literal :: Lit -> Expr a+literal lit = Builtin (Lit lit) :@: []++intType :: Type a+intType = BuiltinType Integer++boolType :: Type a+boolType = BuiltinType Boolean++applyFunction :: Function a -> [Type a] -> [Expr a] -> Expr a+applyFunction fn@Function{..} tyargs args+  = Gbl (Global func_name (funcType fn) tyargs) :@: args++applySignature :: Signature a -> [Type a] -> [Expr a] -> Expr a+applySignature Signature{..} tyargs args+  = Gbl (Global sig_name sig_type tyargs) :@: args++apply :: Expr a -> [Expr a] -> Expr a+apply e es@(_:_) = Builtin At :@: (e:es)+apply _ [] = ERROR("tried to construct nullary lambda function")++applyType :: Ord a => [a] -> [Type a] -> Type a -> Type a+applyType tvs tys ty+  | length tvs == length tys =+      flip transformType ty $ \ty' ->+        case ty' of+          TyVar x ->+            Map.findWithDefault ty' x m+          _ -> ty'+  | otherwise = ERROR("wrong number of type arguments")+  where+    m = Map.fromList (zip tvs tys)++applyPolyType :: Ord a => PolyType a -> [Type a] -> ([Type a], Type a)+applyPolyType PolyType{..} tys =+  (map (applyType polytype_tvs tys) polytype_args,+   applyType polytype_tvs tys polytype_res)++-- * Predicates and examinations on expressions++litView :: Expr a -> Maybe Lit+litView (Builtin (Lit l) :@: []) = Just l+litView _ = Nothing++boolView :: Expr a -> Maybe Bool+boolView e = case litView e of Just (Bool b) -> Just b+                               _             -> Nothing++-- | A representation of Nested patterns, used in 'patternMatchingView'+data DeepPattern a+  = DeepConPat (Global a) [DeepPattern a]+  | DeepVarPat (Local a)+  | DeepLitPat Lit++-- | Match as left-hand side pattern-matching definitions+--+-- Stops at default patterns, for simplicity+patternMatchingView :: Ord a => [Local a] -> Expr a -> [([DeepPattern a],Expr a)]+patternMatchingView = go . map DeepVarPat+  where+  go ps (Match (Lcl l) brs)+    | null [ () | Case Default _ <- brs ]+    , Just k <- modDeepPatterns l ps+    = concat [ go (k (deep p)) ((patToExpr p `unsafeSubst` l) rhs) | Case p rhs <- brs ]+  go ps e = [(ps,e)]++  (<$$>) :: (Functor f,Functor g) => (a -> b) -> f (g a) -> f (g b)+  (<$$>) = fmap . fmap++  -- Variable not in pattern: returns Nothing+  modDeepPattern :: Eq a => Local a -> DeepPattern a -> Maybe (DeepPattern a -> DeepPattern a)+  modDeepPattern l (DeepConPat g nps) = DeepConPat g <$$> modDeepPatterns l nps+  modDeepPattern l (DeepVarPat l') | l == l'   = Just id+                                   | otherwise = Nothing+  modDeepPattern l (DeepLitPat lit) = Nothing++  -- Variable not in patterns: returns Nothing+  modDeepPatterns :: Eq a => Local a -> [DeepPattern a] -> Maybe (DeepPattern a -> [DeepPattern a])+  modDeepPatterns l (np:nps) = ((:nps) <$$> modDeepPattern l np) <|> ((np:) <$$> modDeepPatterns l nps)+  modDeepPatterns l []       = Nothing++  deep :: Pattern a -> DeepPattern a+  deep (ConPat g ls) = DeepConPat g (map DeepVarPat ls)+  deep (LitPat lit)  = DeepLitPat lit+  deep Default       = error "patternMatchingView.deep: Default"++  patToExpr :: Pattern a -> Expr a+  patToExpr (ConPat g ls) = Gbl g :@: map Lcl ls+  patToExpr (LitPat lit)  = literal lit+  patToExpr Default       = error "patternMatchingView.patToExpr: Default"++ifView :: Expr a -> Maybe (Expr a,Expr a,Expr a)+ifView (Match c [Case _ e1,Case (LitPat (Bool b)) e2])+  | b         = Just (c,e2,e1)+  | otherwise = Just (c,e1,e2)+ifView (Match c [Case Default e1,Case (LitPat i@Int{}) e2])    = Just (c === literal i,e2,e1)+ifView (Match c (Case Default e1:Case (LitPat i@Int{}) e2:es)) = Just (c === literal i,e2,Match c (Case Default e1:es))+ifView _ = Nothing++projAt :: Expr a -> Maybe (Expr a,Expr a)+projAt (Builtin At :@: [a,b]) = Just (a,b)+projAt _                          = Nothing++projGlobal :: Expr a -> Maybe a+projGlobal (Gbl (Global x _ _) :@: []) = Just x+projGlobal _                           = Nothing++atomic :: Expr a -> Bool+atomic (_ :@: []) = True+atomic Lcl{}      = True+atomic _          = False++occurrences :: Eq a => Local a -> Expr a -> Int+occurrences var body = length (filter (== var) (universeBi body))++-- | The signature of a function+signature :: Function a -> Signature a+signature func@Function{..} = Signature func_name (funcType func)++-- | The type of a function+funcType :: Function a -> PolyType a+funcType (Function _ tvs lcls res _) = PolyType tvs (map lcl_type lcls) res++bound, free, locals :: Ord a => Expr a -> [Local a]+bound e =+  usort $+    concat [ lcls | Lam lcls _       <- universeBi e ] +++           [ lcl  | Let lcl _ _      <- universeBi e ] +++    concat [ lcls | Quant _ _ lcls _ <- universeBi e ] +++    concat [ lcls | ConPat _ lcls    <- universeBi e ]+locals = usort . universeBi+free e = locals e \\ bound e++globals :: (UniverseBi (t a) (Global a),UniverseBi (t a) (Type a),Ord a)+        => t a -> [a]+globals e =+  usort $+    [ gbl_name | Global{..} <- universeBi e ] +++    [ tc | TyCon tc _ <- universeBi e ]++tyVars :: Ord a => Type a -> [a]+tyVars t = usort $ [ a | TyVar a <- universeBi t ]++-- The free type variables are in the locals, and the globals:+-- but only in the types applied to the global variable.+freeTyVars :: Ord a => Expr a -> [a]+freeTyVars e =+  usort $+    concatMap tyVars $+             [ lcl_type | Local{..} <- universeBi e ] +++      concat [ gbl_args | Global{..} <- universeBi e ]++-- | The type of an expression+exprType :: Ord a => Expr a -> Type a+exprType (Gbl (Global{..}) :@: _) = res+  where+    (_, res) = applyPolyType gbl_type gbl_args+exprType (Builtin blt :@: es) = builtinType blt (map exprType es)+exprType (Lcl lcl) = lcl_type lcl+exprType (Lam args body) = map lcl_type args :=>: exprType body+exprType (Match _ (Case _ body:_)) = exprType body+exprType (Match _ []) = ERROR("empty case expression")+exprType (Let _ _ body) = exprType body+exprType Quant{} = boolType++-- | The result type of a built in function, applied to some types+builtinType :: Ord a => Builtin -> [Type a] -> Type a+builtinType (Lit Int{}) _ = intType+builtinType (Lit Bool{}) _ = boolType+builtinType (Lit String{}) _ = ERROR("strings are not really here")+builtinType And _ = boolType+builtinType Or _ = boolType+builtinType Not _ = boolType+builtinType Implies _ = boolType+builtinType Equal _ = boolType+builtinType Distinct _ = boolType+builtinType IntAdd _ = intType+builtinType IntSub _ = intType+builtinType IntMul _ = intType+builtinType IntDiv _ = intType+builtinType IntMod _ = intType+builtinType IntGt _ = boolType+builtinType IntGe _ = boolType+builtinType IntLt _ = boolType+builtinType IntLe _ = boolType+builtinType At ((_  :=>: res):_) = res+builtinType At _ = ERROR("ill-typed lambda application")+++-- * Substition and refreshing++freshLocal :: Name a => Type a -> Fresh (Local a)+freshLocal ty = liftM2 Local fresh (return ty)++freshArgs :: Name a => Global a -> Fresh [Local a]+freshArgs gbl = mapM freshLocal (polytype_args (gbl_type gbl))++refreshLocal :: Name a => Local a -> Fresh (Local a)+refreshLocal (Local name ty) = liftM2 Local (refresh name) (return ty)++-- Rename bound variables in an expression to fresh variables.+freshen :: Name a => Expr a -> Fresh (Expr a)+freshen e = freshenNames (map lcl_name (bound e)) e++freshenNames :: (TransformBi a (f a), Name a) =>+  [a] -> f a -> Fresh (f a)+freshenNames names e = do+  sub <- fmap (Map.fromList . zip names) (mapM refresh names)+  return . flip transformBi e $ \x ->+    case Map.lookup x sub of+      Nothing -> x+      Just y -> y++-- | Substitution, of local variables+--+-- Since there are only rank-1 types, bound variables from lambdas and+-- case never have a forall type and thus are not applied to any types.+(//) :: Name a => Expr a -> Local a -> Expr a -> Fresh (Expr a)+e // x = transformExprM $ \ e0 -> case e0 of+  Lcl y | x == y -> freshen e+  _              -> return e0++substMany :: Name a => [(Local a, Expr a)] -> Expr a -> Fresh (Expr a)+substMany xs e0 = foldM (\e (x,xe) -> (xe // x) e) e0 xs++letExpr :: Name a => Expr a -> (Local a -> Fresh (Expr a)) -> Fresh (Expr a)+letExpr (Lcl x) k = k x+letExpr b k =+  do v <- freshLocal (exprType b)+     rest <- k v+     return (Let v b rest)++-- | Substitution, but without refreshing. Only use when the replacement+-- expression contains no binders (i.e. no lambdas, no lets, no quantifiers),+-- since the binders are not refreshed at every insertion point.+unsafeSubst :: Ord a => Expr a -> Local a -> Expr a -> Expr a+e `unsafeSubst` _ | not (null (bound e)) = error "Tip.unsafeSubst: contains binders"+e `unsafeSubst` x = transformExpr $ \ e0 -> case e0 of+  Lcl y | x == y -> e+  _              -> e0++-- * Making new locals and functions++updateLocalType :: Type a -> Local a -> Local a+updateLocalType ty (Local name _) = Local name ty++updateFuncType :: PolyType a -> Function a -> Function a+updateFuncType (PolyType tvs lclTys res) (Function name _ lcls _ body)+  | length lcls == length lclTys =+      Function name tvs (zipWith updateLocalType lclTys lcls) res body+  | otherwise = ERROR("non-matching type")+++-- * Matching++matchTypesIn :: Ord a => [a] -> [(Type a, Type a)] -> Maybe [Type a]+matchTypesIn tvs tys = do+  sub <- matchTypes tys+  forM tvs $ \tv -> lookup tv sub++matchTypes :: Ord a => [(Type a, Type a)] -> Maybe [(a, Type a)]+matchTypes tys = mapM (uncurry match) tys >>= collect . usort . concat+  where+    match (TyVar x) ty = Just [(x, ty)]+    match (TyCon x tys1) (TyCon y tys2)+      | x == y && length tys1 == length tys2 =+        fmap concat (zipWithM match tys1 tys2)+    match (args1 :=>: res1) (args2 :=>: res2)+      | length args1 == length args2 =+        fmap concat (zipWithM match (res1:args1) (res2:args2))+    match ty1 ty2 | ty1 == ty2 = Just []+    match _ _ = Nothing++    collect [] = Just []+    collect [x] = Just [x]+    collect ((x, _):(y, _):_) | x == y = Nothing+    collect (x:xs) = fmap (x:) (collect xs)++makeGlobal :: Ord a => a -> PolyType a -> [Type a] -> Maybe (Type a) -> Maybe (Global a)+makeGlobal name polyty@PolyType{..} args mres = do+  vars <- matchTypesIn polytype_tvs tys+  return (Global name polyty vars)+  where+    tys =+      (case mres of Nothing -> []; Just res -> [(polytype_res, res)]) +++      zip polytype_args args++-- * Data types++constructorType :: Datatype a -> Constructor a -> PolyType a+constructorType Datatype{..} Constructor{..} =+  PolyType data_tvs (map snd con_args) (TyCon data_name (map TyVar data_tvs))++destructorType :: Datatype a -> Type a -> PolyType a+destructorType Datatype{..} ty =+  PolyType data_tvs [TyCon data_name (map TyVar data_tvs)] ty++constructor :: Datatype a -> Constructor a -> [Type a] -> Global a+constructor dt con@Constructor{..} tys =+  Global con_name (constructorType dt con) tys++projector :: Datatype a -> Constructor a -> Int -> [Type a] -> Global a+projector dt Constructor{..} i tys =+  Global proj_name (destructorType dt proj_ty) tys+  where+    (proj_name, proj_ty) = con_args !! i++discriminator :: Datatype a -> Constructor a -> [Type a] -> Global a+discriminator dt Constructor{..} tys =+  Global con_discrim (destructorType dt (BuiltinType Boolean)) tys++-- * Operations on theories++mapDecls :: forall a b . (forall t . Traversable t => t a -> t b) -> Theory a -> Theory b+mapDecls k (Theory a b c d e) = Theory (map k a) (map k b) (map k c) (map k d) (map k e)++-- * Topologically sorting definitions++topsort :: (Ord a,Definition f) => [f a] -> [[f a]]+topsort = sortThings defines uses++class Definition f where+  defines :: f a -> a+  uses    :: f a -> [a]++data (f :+: g) a = InL (f a) | InR (g a)+  deriving (Eq,Ord,Show,Functor)++instance (Definition f,Definition g) => Definition (f :+: g) where+  defines (InL x) = defines x+  defines (InR y) = defines y+  uses (InL x) = uses x+  uses (InR y) = uses y++instance Definition Signature where+  defines = sig_name+  uses _  = []++instance Definition Function where+  defines = func_name+  uses    = F.toList . func_body++instance Definition Datatype where+  defines = data_name+  uses    = concatMap F.toList . data_cons+
+ src/Tip/Fresh.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | Fresh monad and the Name type class+module Tip.Fresh where++import Tip.Utils+import Tip.Pretty+import Control.Applicative hiding (empty)+import Control.Monad.State+import Control.Arrow ((&&&))++import Data.Foldable (Foldable)++-- | The Fresh monad+newtype Fresh a = Fresh (State Int a)+  deriving (Monad, Applicative, Functor, MonadFix)++-- | Continues making unique names after the highest+--   numbered name in a foldable value.+freshPass :: (Foldable f,Name a) => (f a -> Fresh b) -> f a -> b+f `freshPass` x = f x `freshFrom` x++-- | Run fresh from starting from the greatest unique in a structure+freshFrom :: (Foldable f,Name b) => Fresh a -> f b -> a+freshFrom m x = runFreshFrom (succ (maximumOn getUnique x)) m++-- | Run fresh, starting from zero+runFresh :: Fresh a -> a+runFresh (Fresh m) = evalState m 0++-- | Run fresh from some starting value+runFreshFrom :: Int -> Fresh a -> a+runFreshFrom n (Fresh m) = evalState m (n+1)++-- | The Name type class+class (PrettyVar a, Ord a) => Name a where+  -- | Make a fresh name+  fresh   :: Fresh a++  -- | Refresh a name, which could have some resemblance to the original+  -- name+  refresh :: a -> Fresh a+  refresh _ = fresh++  -- | Make a fresh name that can incorporate the given string+  freshNamed :: String -> Fresh a+  freshNamed _ = fresh++  -- | Refresh a name with an additional hint string+  refreshNamed :: String -> a -> Fresh a+  refreshNamed s n = freshNamed (s ++ varStr n)++  -- | Gets the unique associated with a name.+  getUnique :: a -> Int++instance Name Int where+  fresh     = Fresh (state (id &&& succ))+  getUnique = id+
+ src/Tip/Haskell/Rename.hs view
@@ -0,0 +1,137 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE CPP #-}+module Tip.Haskell.Rename (renameDecls, isOperator, RenameMap) where++#include "errors.h"+import Tip.Haskell.Repr+import Tip.Haskell.Translate+import Tip.Utils.Rename+import Tip.Pretty++import Data.Set (Set)+import qualified Data.Set as S++import Data.Map (Map)+import qualified Data.Map as M++import Data.Char++import qualified Data.Foldable as F++type RenameMap a = Map (HsId a) (HsId String)++renameDecls :: forall a . (Ord a,PrettyVar a) => Decls (HsId a) -> (Decls (HsId String),RenameMap a)+renameDecls ds = runRenameM suggest blocks M.empty (rename ds)+  where+  blocks = map Other (keywords ++ map snd hsBuiltins ++ exacts)++  exacts :: [String]+  exacts = [ s | Exact s <- F.toList ds ]+        ++ [ s | Qualified _ _ s <- F.toList ds ]++  suggest :: HsId a -> [HsId String]+  suggest (Qualified m ms s) = Qualified m ms s:__+  suggest (Exact s) = Exact s:__+  suggest i+    | i `S.member` us = map (Other . upper) (disambigHs (makeUniform (varStr i)))+    | otherwise       = map (Other . lower) (disambigHs (makeUniform (varStr i)))++  us = uppercase ds++uppercase :: Ord a => Decls a -> Set a+uppercase (Decls ds) = S.fromList $+    [ x | TypeDef (TyCon x _) _ <- ds ] +++    [ x | DataDecl x _ _ _ <- ds ] +++    [ x | DataDecl _ _ cons _ <- ds, (x,_) <- cons ]++makeUniform :: String -> String+makeUniform s+    | couldBeOperator s = filter (`elem` opSyms) s+    | otherwise    = initialAlpha (filter isAlphaNum s)++initialAlpha :: String -> String+initialAlpha s@(c:_) | isAlpha c = s+                     | otherwise = 'x':s++disambigHs :: String -> [String]+disambigHs s+    | isOperator s = s : [ s ++ replicate n '.' | n <- [1..] ]+    | otherwise    = disambig id s++upper :: String -> String+upper s@(c:r)+    | isOperator s = if c == ':' then s else ':':s+    | otherwise    = if isUpper c then s else toUpper c:r++lower :: String -> String+lower s@(c:r)+    | isOperator s = if c == ':' then r else s+    | otherwise    = if isLower c then s else toLower c:r++isOperator :: String -> Bool+isOperator = all (`elem` opSyms)++couldBeOperator :: String -> Bool+couldBeOperator s = i2d (numOps s) / i2d (length s) >= 0.5+  where+  i2d :: Int -> Double+  i2d = fromInteger . toInteger++numOps :: String -> Int+numOps = length . filter (`elem` opSyms)++opSyms :: String+opSyms = "!#$%&*+./<=>?@\\^|-~:"++keywords :: [String]+keywords =+  [ "!"+  , "'"+  , "''"+  , "-"+  , "--"+  , "-<"+  , "-<<"+  , "->"+  , "::"+  , ";"+  , "<-"+  , ","+  , "="+  , "=>"+  , ">"+  , "?"+  , "#"+  , "*"+  , "@"+  , "\\"+  , "_"+  , "`"+  , "|"+  , "~"+  , "as"+  , "case", "of"+  , "class"+  , "data"+  , "family"+  , "instance"+  , "default"+  , "deriving"+  , "do"+  , "forall"+  , "foreign"+  , "hiding"+  , "if", "then", "else"+  , "import"+  , "infix", "infixl", "infixr"+  , "let", "in"+  , "mdo"+  , "module"+  , "newtype"+  , "proc"+  , "qualified"+  , "rec"+  , "type"+  , "family"+  , "where"+  ]
+ src/Tip/Haskell/Repr.hs view
@@ -0,0 +1,99 @@+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+-- | A representation of Haskell programs+module Tip.Haskell.Repr where++import Data.Foldable (Foldable)+import Data.Traversable (Traversable)++data Decls a = Decls [Decl a]+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)++data Decl a+  = TySig a+          [Type a] {- class contexts -}+          (Type a)+  | FunDecl a [([Pat a],Expr a)]+  | DataDecl a               {- type constructor name -}+             [a]             {- type variables -}+             [(a,[Type a])]  {- constructors -}+             [a]             {- instance derivings -}+  | InstDecl [Type a] {- context -}+             (Type a) {- head -}+             [Decl a] {- declarations (associated types and fun decls) -}+  | TypeDef (Type a) (Type a)+  | Decl a `Where` [Decl a]+  | TH (Expr a)+  | Module String+  | LANGUAGE String+  | QualImport String (Maybe String)+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)++funDecl :: a -> [a] -> Expr a -> Decl a+funDecl f xs b = FunDecl f [(map VarPat xs,b)]++data Type a+  = TyCon a [Type a]+  | TyVar a+  | TyTup [Type a]+  | TyArr (Type a) (Type a)+  | TyForall [a] (Type a)+  | TyCtx [Type a] (Type a)+  | TyImp a (Type a)+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)++modTyCon :: (a -> a) -> Type a -> Type a+modTyCon f t0 =+  case t0 of+    TyCon t ts  -> TyCon (f t) (map (modTyCon f) ts)+    TyVar x     -> TyVar x+    TyTup ts    -> TyTup (map (modTyCon f) ts)+    TyArr t1 t2 -> TyArr (modTyCon f t1) (modTyCon f t2)++data Expr a+  = Apply a [Expr a]+  | ImpVar a+  | Do [Stmt a] (Expr a)+  | Lam [Pat a] (Expr a)+  | Let a (Expr a) (Expr a)+  | ImpLet a (Expr a) (Expr a)+  | List [Expr a] -- a literal list+  | Tup [Expr a]  -- a literal tuple+  | String a      -- string from a name...+  | Noop          -- | @return ()@+  | Case (Expr a) [(Pat a,Expr a)]+  | Int Integer+  | QuoteTyCon a -- Template Haskell ''+  | QuoteName a  -- Template Haskell '+  | THSplice (Expr a) -- Template Haskell $(..)+  | Record (Expr a) [(a,Expr a)] -- record update+  | Expr a ::: Type a+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)++nestedTyTup :: [Type a] -> Type a+nestedTyTup []     = TyTup []+nestedTyTup (t:ts) = TyTup [t,nestedTyTup ts]++nestedTup :: [Expr a] -> Expr a+nestedTup [] = Tup []+nestedTup (d:ds) = Tup [d,nestedTup ds]++nestedTupPat :: [Pat a] -> Pat a+nestedTupPat []     = TupPat []+nestedTupPat (d:ds) = TupPat [d,nestedTupPat ds]++mkDo []      x = x+mkDo ss1 (Do ss2 e) = mkDo (ss1 ++ ss2) e+mkDo ss Noop = case (init ss,last ss) of+  (i,Stmt e)   -> mkDo i e+  (i,Bind x e) -> mkDo i e+mkDo ss e = Do ss e++var :: a -> Expr a+var x = Apply x []++data Pat a = VarPat a | ConPat a [Pat a] | TupPat [Pat a] | WildPat | IntPat Integer+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)++data Stmt a = Bind a (Expr a) | BindTyped a (Type a) (Expr a) | Stmt (Expr a)+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)+
+ src/Tip/Haskell/Translate.hs view
@@ -0,0 +1,509 @@+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE CPP #-}+module Tip.Haskell.Translate where++#include "errors.h"+import Tip.Haskell.Repr as H+import Tip.Core as T hiding (Formula(..),globals,Type(..))+import Tip.Core (Type((:=>:),BuiltinType))+import qualified Tip.Core as T+import Tip.Pretty+import Tip.Utils+import Tip.Scope++import Tip.CallGraph++import Control.Monad++import qualified Data.Foldable as F+import Data.Foldable (Foldable)+import Data.Traversable (Traversable)++import qualified Data.Map as M++import Data.Generics.Geniplate++import Data.List (nub,partition)++prelude :: String -> HsId a+prelude = Qualified "Prelude" (Just "P")++tipDSL :: String -> HsId a+tipDSL = Qualified "Tip" Nothing++quickCheck :: String -> HsId a+quickCheck = Qualified "Test.QuickCheck" (Just "QC")++quickCheckUnsafe :: String -> HsId a+quickCheckUnsafe = Qualified "Test.QuickCheck.Gen.Unsafe" (Just "QU")++quickCheckAll :: String -> HsId a+quickCheckAll = Qualified "Test.QuickCheck.All" (Just "QC")++quickSpec :: String -> HsId a+quickSpec = Qualified "QuickSpec" (Just "QS")++feat :: String -> HsId a+feat = Qualified "Test.Feat" (Just "F")++typeable :: String -> HsId a+typeable = Qualified "Data.Typeable" (Just "T")++data HsId a+    = Qualified+         { qual_module       :: String+         , qual_module_short :: Maybe String+         , qual_func         :: String+         }+    -- ^ A qualified import+    | Exact String+    -- ^ The current module defines something with this very important name+    | Other a+    -- ^ From the theory+    | Derived (HsId a) String+    -- ^ For various purposes...+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)++instance PrettyVar a => PrettyVar (HsId a) where+  varStr (Qualified _ (Just m) s) = m ++ "." ++ s+  varStr (Qualified m Nothing  s) = m ++ "." ++ s+  varStr (Exact s) = s+  varStr (Other x) = varStr x+  varStr (Derived o s) = s ++ varStr o++addHeader :: Decls a -> Decls a+addHeader (Decls ds) =+    Decls (map LANGUAGE ["TemplateHaskell","DeriveDataTypeable","TypeOperators","ImplicitParams","RankNTypes"] ++ Module "A" : ds)++addImports :: Ord a => Decls (HsId a) -> Decls (HsId a)+addImports d@(Decls ds) = Decls (QualImport "Text.Show.Functions" Nothing : imps ++ ds)+  where+  imps = usort [ QualImport m short | Qualified m short _ <- F.toList d ]++trTheory :: (Ord a,PrettyVar a) => Theory a -> Decls (HsId a)+trTheory = trTheory' . fmap Other++data Kind = Expr | Formula deriving Eq++theorySigs :: Theory (HsId a) -> [HsId a]+theorySigs Theory{..} = map sig_name thy_sigs++ufInfo :: Theory (HsId a) -> (Bool,[H.Type (HsId a)])+ufInfo Theory{thy_sigs} = (not (null imps),imps)+  where+  imps = [TyImp (Derived f "imp") (H.TyCon (Derived f "") []) | Signature f _ <- thy_sigs]++trTheory' :: forall a b . (a ~ HsId b,Ord b,PrettyVar b) => Theory a -> Decls a+trTheory' thy@Theory{..} =+  Decls $+    concatMap tr_datatype thy_datatypes +++    map tr_sort thy_sorts +++    concatMap tr_sig thy_sigs +++    concatMap tr_func thy_funcs +++    tr_asserts thy_asserts +++    [makeSig thy]+  where+  (translate_UFs,imps) = ufInfo thy++  tr_datatype :: Datatype a -> [Decl a]+  tr_datatype (Datatype tc tvs cons) =+    [ DataDecl tc tvs+        [ (c,map (trType . snd) args) | Constructor c _ args <- cons ]+        (map prelude ["Eq","Ord","Show"] ++ [typeable "Typeable"])+    , TH (Apply (feat "deriveEnumerable") [QuoteTyCon tc])+    , InstDecl [H.TyCon (feat "Enumerable") [H.TyVar a] | a <- tvs]+               (H.TyCon (quickCheck "Arbitrary") [H.TyCon tc (map H.TyVar tvs)])+               [funDecl+                  (quickCheck "arbitrary") []+                  (Apply (quickCheck "sized") [Apply (feat "uniform") []])]+    ]++  tr_sort :: Sort a -> Decl a+  tr_sort (Sort _ i) | i /= 0 = error "Higher-kinded abstract sort"+  tr_sort (Sort s i) = TypeDef (TyCon s []) (TyCon (prelude "Int") [])++  tr_sig :: Signature a -> [Decl a]+  tr_sig (Signature f pt) =+    -- newtype f_NT = f_Mk (forall tvs . (Arbitrary a, CoArbitrary a) => T)+    [ DataDecl (Derived f "") [] [ (Derived f "Mk",[tr_polyTypeArbitrary pt]) ] []+    , FunDecl (Derived f "get")+       [( [H.ConPat (Derived f "Mk") [VarPat (Derived f "x")]]+        , var (Derived f "x")+        )]++    -- f :: (?f_imp :: f_NT) => T+    -- f = f_get ?f_imp+    , TySig f [] (tr_polyType pt)+    , funDecl f [] (Apply (Derived f "get") [ImpVar (Derived f "imp")])++    -- instance Arbitrary f_NT where+    --   arbitrary = do+    --      Capture x <- capture+    --      return (f_Mk (x arbitrary))+    , InstDecl [] (TyCon (quickCheck "Arbitrary") [TyCon (Derived f "") []])+        [ funDecl (quickCheck "arbitrary") []+          (mkDo [Bind (Derived f "x") (Apply (quickCheckUnsafe "capture") [])]+                (H.Case (var (Derived f "x"))+                   [(H.ConPat (quickCheckUnsafe "Capture") [VarPat (Derived f "y")]+                    ,Apply (prelude "return")+                    [Apply (Derived f "Mk")+                    [Apply (Derived f "y")+                    [Apply (quickCheck "arbitrary") []]]]+                    )]+                )+          )+        ]++    -- gen :: Gen (Dict (?f_imp :: f_NT))+    -- gen = do+    --   x <- arbitrary+    --   let ?f_imp = x+    --   return Dict+    , TySig (Derived f "gen") []+        (TyCon (quickCheck "Gen")+          [TyCon (quickSpec "Dict")+            [TyImp (Derived f "imp") (TyCon (Derived f "") [])]])+    , funDecl (Derived f "gen") []+        (mkDo [Bind (Derived f "x") (Apply (quickCheck "arbitrary") [])]+              (ImpLet (Derived f "imp") (var (Derived f "x"))+                (Apply (prelude "return") [Apply (quickSpec "Dict") []])))+    ]++  tr_func :: Function a -> [Decl a]+  tr_func fn@Function{..} =+    [ TySig func_name [] (tr_polyType (funcType fn))+    , FunDecl+        func_name+        [ (map tr_deepPattern dps,tr_expr Expr rhs)+        | (dps,rhs) <- patternMatchingView func_args func_body+        ]+    ]++  tr_asserts :: [T.Formula a] -> [Decl a]+  tr_asserts fms =+    let (names,decls) = unzip (zipWith tr_assert [1..] fms)+    in  decls {- +++          [ TH (Apply (prelude "return") [List []])+          , funDecl (Exact "main") []+              (mkDo [ Stmt (THSplice (Apply (quickCheckAll "polyQuickCheck")+                                            [QuoteName name]))+                    | name <- names ]+                    Noop)+          ] -}++  tr_assert :: Int -> T.Formula a -> (a,Decl a)+  tr_assert i (T.Formula r _ b) =+    (prop_name,funDecl prop_name args (assume (tr_expr Formula body)))+    where+    prop_name | i == 1    = Exact "prop"+              | otherwise = Exact ("prop" ++ show i)+    (args,body) =+      case b of+        Quant _ Forall lcls term -> (map lcl_name lcls,term)+        _                        -> ([],b)++    assume e =+      case r of+        Prove  -> e+        Assert -> Apply (tipDSL "assume") [e]++  tr_deepPattern :: DeepPattern a -> H.Pat a+  tr_deepPattern (DeepConPat Global{..} dps) = H.ConPat gbl_name (map tr_deepPattern dps)+  tr_deepPattern (DeepVarPat Local{..})      = VarPat lcl_name+  tr_deepPattern (DeepLitPat (T.Int i))      = IntPat i+  tr_deepPattern (DeepLitPat (Bool b))       = withBool H.ConPat b++  tr_pattern :: T.Pattern a -> H.Pat a+  tr_pattern Default = WildPat+  tr_pattern (T.ConPat Global{..} xs) = H.ConPat gbl_name (map (VarPat . lcl_name) xs)+  tr_pattern (T.LitPat (T.Int i))     = H.IntPat i+  tr_pattern (T.LitPat (Bool b))      = withBool H.ConPat b++  tr_expr :: Kind -> T.Expr a -> H.Expr a+  tr_expr k e0 =+    case e0 of+      Builtin (Lit (T.Int i)) :@: [] -> H.Int i+      Builtin (Lit (Bool b)) :@: []  -> withBool Apply b+      hd :@: es -> let (f,k') = tr_head k hd+                   in Apply f (map (tr_expr k') es)+      Lcl x -> var (lcl_name x)+      T.Lam xs b  -> H.Lam (map (VarPat . lcl_name) xs) (tr_expr Expr b)+      Match e alts -> H.Case (tr_expr Expr e) [ (tr_pattern p,tr_expr Expr rhs) | T.Case p rhs <- default_last alts ]+      T.Let x e b -> H.Let (lcl_name x) (tr_expr Expr e) (tr_expr k b)+      T.Quant _ q xs b ->+        foldr+          (\ x e ->+              Apply (tipDSL (case q of Forall -> "forAll"; Exists -> "exists"))+                [H.Lam [VarPat (lcl_name x)] e])+          (tr_expr Formula b)+          xs++    where+    default_last (def@(T.Case Default _):alts) = alts ++ [def]+    default_last alts = alts++  tr_head :: Kind -> T.Head a -> (a,Kind)+  tr_head k (Gbl Global{..}) = (gbl_name,Expr)+  tr_head k (Builtin b)      = tr_builtin k b++  tr_builtin :: Kind -> T.Builtin -> (a,Kind)+  tr_builtin k b =+    case b of+      At        -> (prelude "id",Expr)+      Lit{}     -> error "tr_builtin"+      And       -> case_kind ".&&."+      Or        -> case_kind ".||."+      Not       -> case_kind "neg"+      Implies   -> case_kind "==>"+      Equal     -> case_kind "==="+      Distinct  -> case_kind "=/="+      _         -> prelude_fn+    where+    Just prelude_str_ = lookup b hsBuiltins+    prelude_fn = (prelude prelude_str_,Expr)++    case_kind sf =+      case k of+        Expr    -> prelude_fn+        Formula -> (tipDSL sf,Formula)++  -- ignores the type variables+  tr_polyType_inner :: T.PolyType a -> H.Type a+  tr_polyType_inner (PolyType _ ts t) = trType (ts :=>: t)++  tr_polyType :: T.PolyType a -> H.Type a+  tr_polyType pt@(PolyType tvs _ _)+    | translate_UFs = TyForall tvs (TyCtx (arb tvs ++ imps) (tr_polyType_inner pt))+    | otherwise     = tr_polyType_inner pt++  -- translate type and add Arbitrary a, CoArbitrary a in the context for+  -- all type variables a+  tr_polyTypeArbitrary :: T.PolyType a -> H.Type a+  tr_polyTypeArbitrary pt@(PolyType tvs _ _) = TyForall tvs (TyCtx (arb tvs) (tr_polyType_inner pt))++  arb = arbitrary . map H.TyVar++arbitrary :: [H.Type (HsId a)] -> [H.Type (HsId a)]+arbitrary ts =+  [ TyCon (quickCheck tc) [t]+  | t <- ts+  , tc <- ["Arbitrary","CoArbitrary"]+  ]++trType :: (a ~ HsId b) => T.Type a -> H.Type a+trType (T.TyVar x)     = H.TyVar x+trType (T.TyCon tc ts) = H.TyCon tc (map trType ts)+trType (ts :=>: t)     = foldr TyArr (trType t) (map trType ts)+trType (BuiltinType b) = trBuiltinType b++trBuiltinType :: BuiltinType -> H.Type (HsId a)+trBuiltinType t | Just s <- lookup t hsBuiltinTys = H.TyCon (prelude s) []++withBool :: (a ~ HsId b) => (a -> [c] -> d) -> Bool -> d+withBool k b = k (prelude (show b)) []++-- * Builtins++hsBuiltinTys :: [(T.BuiltinType,String)]+hsBuiltinTys =+  [ (Integer, "Int")+  , (Boolean, "Bool")+  ]++hsBuiltins :: [(T.Builtin,String)]+hsBuiltins =+  [ (And      , "&&" )+  , (Or       , "||" )+  , (Not      , "not")+  , (Implies  , "<=" )+  , (Equal    , "==" )+  , (Distinct , "/=" )+  , (IntAdd   , "+"  )+  , (IntSub   , "-"  )+  , (IntMul   , "*"  )+  , (IntDiv   , "div")+  , (IntMod   , "mod")+  , (IntGt    , ">"  )+  , (IntGe    , ">=" )+  , (IntLt    , "<"  )+  , (IntLe    , "<=" )+  ]++typeOfBuiltin :: Builtin -> T.Type a+typeOfBuiltin b = case b of+  And      -> bbb+  Or       -> bbb+  Not      -> bb+  Implies  -> bbb+  Equal    -> iib -- TODO: equality could be used on other types than int+  Distinct -> iib -- ditto+  IntAdd   -> iii+  IntSub   -> iii+  IntMul   -> iii+  IntDiv   -> iii+  IntMod   -> iii+  IntGt    -> iib+  IntGe    -> iib+  IntLt    -> iib+  IntLe    -> iib+  _        -> __+  where+  bb  = [boolType] :=>: boolType+  bbb = [boolType,boolType] :=>: boolType+  iii = [intType,intType] :=>: intType+  iib = [intType,intType] :=>: boolType+++-- * QuickSpec signatures++makeSig :: forall a . (PrettyVar a,Ord a) => Theory (HsId a) -> Decl (HsId a)+makeSig thy@Theory{..} =+  funDecl (Exact "sig") [] $+    Tup+      [ List+          [ Tup+              [ constant_decl ft+              , List $+                  if use_cg+                    then+                      [ int_lit num+                      | (members,num) <- cg `zip` [0..]+                      , f `elem` members+                      ]+                    else+                      [int_lit 0]++              ]+          | ft@(f,_) <- func_constants+          ]+      , Apply (quickSpec "signature") [] `Record`+          [ (quickSpec "constants",+               List $+                 builtin_decls +++                 map constant_decl+                   (ctor_constants ++ builtin_constants))+          , (quickSpec "instances", List $+               [ mk_inst [] (mk_class (feat "Enumerable") (H.TyCon (prelude "Int") [])) ] +++               [ mk_inst (map (mk_class c1) tys) (mk_class c2 (H.TyCon t tys))+               | (t,n) <- type_univ+               , (c1, c2) <- [(prelude "Ord", prelude "Ord"),+                              (feat "Enumerable", feat "Enumerable"),+                              (feat "Enumerable",quickCheck "Arbitrary")]+               , let tys = map trType (qsTvs n)+               ] +++               [ Apply (quickSpec "makeInstance") [H.Lam [TupPat []] (Apply (Derived f "gen") [])]+               | Signature f _ <- thy_sigs+               ])+          , (quickSpec "maxTermSize", Apply (prelude "Just") [H.Int (if translate_UFs then 15 else 7)])+          , (quickSpec "testTimeout", Apply (prelude "Just") [H.Int 100000])+          ]+      ]+  where+  (translate_UFs,imps) = ufInfo thy++  use_cg = True++  int_lit x = H.Int x ::: H.TyCon (prelude "Int") []++  mk_inst ctx res =+    Apply (quickSpec ("inst" ++ concat [ show (length ctx) | length ctx >= 2 ]))+                 [ Apply (quickSpec "Sub") [Apply (quickSpec "Dict") []] :::+                   H.TyCon (quickSpec ":-") [TyTup ctx,res] ]++  mk_class c x = H.TyCon c [x]++  scp = scope thy++  cg = map (map defines) (flatCallGraph (CallGraphOpts True False) thy)++  poly_type (PolyType _ args res) = args :=>: res++  constant_decl (f,t) =+    Apply (quickSpec "constant") [H.String f,lam (Apply f []) ::: qs_type]+    where+    (pre,qs_type) = qsType t+    lam | null pre  = id+        | otherwise = H.Lam (replicate (length pre) (H.ConPat (quickSpec "Dict") []))++  int_lit_decl x =+    Apply (quickSpec "constant") [H.String (Exact (show x)),int_lit x]++  bool_lit_decl b =+    Apply (quickSpec "constant") [H.String (prelude (show b)),withBool Apply b]++  ctor_constants =+    [ (f,poly_type (globalType g))+    | (f,g@ConstructorInfo{}) <- M.toList (globals scp)+    ]++  func_constants =+    [ (f,poly_type (globalType g))+    | (f,g@FunctionInfo{}) <- M.toList (globals scp)+    ]++  type_univ =+    [ (data_name, length data_tvs)+    | (_,DatatypeInfo Datatype{..}) <- M.toList (types scp)+    ]++  -- builtins++  (builtin_lits,builtin_funs) =+    partition litBuiltin $+      usort+        [ b+        | Builtin b :@: args <- universeBi thy++        -- only count equality if argument is int:+        , let is_int = case args of+                         a1:_ -> exprType a1 == (intType :: T.Type (HsId a))+                         _    -> __+        , case b of+            Equal    -> is_int+            Distinct -> is_int+            _         -> True+        ]++  used_builtin_types :: [BuiltinType]+  used_builtin_types =+    usort [ t | BuiltinType t :: T.Type (HsId a) <- universeBi thy ]++  bool_used = Boolean `elem` used_builtin_types+  int_used  = -- Integer `elem` used_builtin_types+              or [ op `elem` builtin_funs | op <- [IntAdd,IntSub,IntMul,IntDiv,IntMod] ]++  builtin_decls+    =  [ bool_lit_decl b | bool_used, b <- [False,True] ]+    ++ [ int_lit_decl x  | int_used,  x <- [0,1] +++                                           [ x+                                           | Lit (T.Int x) <- builtin_lits ]]++  builtin_constants+    =  [ (prelude s,typeOfBuiltin b)+       | b <- nub $+              [ b      | bool_used, b <- [And,Or,Not] ]+           -- [ IntAdd | int_used ]+           -- [ Equal  | bool_used && int_used ]+           ++ [ b | b <- builtin_funs, intBuiltin b || eqRelatedBuiltin b ]+       , Just s <- [lookup b hsBuiltins]+       ]++  qsType :: Ord a => T.Type (HsId a) -> ([H.Type (HsId a)],H.Type (HsId a))+  qsType t = (pre,foldr TyArr inner [ TyCon (quickSpec "Dict") [p] | p <- pre ])+    where+    pre | translate_UFs = arbitrary (map trType qtvs) ++ imps+        | otherwise     = []+    inner = trType (applyType tvs qtvs t)+    qtvs = qsTvs (length tvs)+    tvs = tyVars t++  qsTvs :: Int -> [T.Type (HsId a)]+  qsTvs n = take n (cycle [ T.TyCon (quickSpec qs_tv) [] | qs_tv <- ["A","B","C","D","E"] ])++theoryBuiltins :: Ord a => Theory a -> [T.Builtin]+theoryBuiltins = usort . universeBi+
+ src/Tip/Lint.hs view
@@ -0,0 +1,259 @@+{-# LANGUAGE CPP, RecordWildCards, OverloadedStrings, FlexibleContexts, ViewPatterns #-}+-- | Check that a theory is well-typed.+--+-- Invariants:+--+--  * No shadowing---checked by scope monad.+--+--  * Each local is bound before it's used.+--+--  * All expressions are well-typed.+--+--  * The result of each constructor should be a value of that datatype.+--+--  * Default case comes first. No duplicate cases.+--+--  * Expressions and formulas not mixed.+module Tip.Lint (lint, lintM, lintTheory) where++#include "errors.h"+import Tip.Core+import Tip.Scope+import Tip.Pretty+import Tip.Rename+import Control.Monad+import Control.Monad.Error+import Control.Monad.State+import Data.Maybe+import Text.PrettyPrint+import Tip.Pretty.SMT+import Data.List+--import Debug.Trace++-- | Crashes if the theory is malformed+lint :: (PrettyVar a, Ord a) => String -> Theory a -> Theory a+lint pass thy0@(renameAvoiding [] return -> thy) =+  -- trace ("Linting:" ++ pass ++ ":\n" ++ ppRender thy) $+  case lintTheory thy0 of+    Nothing -> thy0+    Just doc ->+      case lintTheory thy of+        Just doc ->+          error ("Lint failed after " ++ pass ++ ":\n" ++ show doc ++ "\n!!!")+        Nothing ->+          error ("Non-renamed linting pass failed!? " ++ pass ++ ":\n" ++ show doc ++ "\n!!!")++-- | Same as 'lint', but returns in a monad, for convenience+lintM :: (PrettyVar a, Ord a, Monad m) => String -> Theory a -> m (Theory a)+lintM pass = return . lint pass++check :: (PrettyVar a, Ord a) => Doc -> (Scope a -> Bool) -> ScopeM a ()+check x p = check' x (guard . p)++check' :: (PrettyVar a, Ord a) => Doc -> (Scope a -> Maybe b) -> ScopeM a b+check' x p = do+  scp <- get+  case p scp of+    Nothing -> throwError x+    Just y  -> return y++-- | Returns the error if the theory is malformed+lintTheory :: (PrettyVar a, Ord a) => Theory a -> Maybe Doc+lintTheory thy@Theory{..} =+  either Just (const Nothing) .+  runScope . withTheory thy $ inContext thy $ do+    mapM_ lintDatatype thy_datatypes+    mapM_ lintSignature thy_sigs+    mapM_ lintFunction thy_funcs+    mapM_ lintFormula thy_asserts++lintDatatype :: (PrettyVar a, Ord a) => Datatype a -> ScopeM a ()+lintDatatype dt@Datatype{..} =+  local $ inContext dt $ do+    mapM_ newTyVar data_tvs+    forM_ data_cons $ \Constructor{..} -> do+      forM_ con_args $ \(_, ty) ->+        lintType ty++lintPolyType :: (PrettyVar a, Ord a) => PolyType a -> ScopeM a ()+lintPolyType polyty@PolyType{..} =+  newScope $ inContext polyty $ do+    mapM_ newTyVar polytype_tvs+    mapM_ lintType polytype_args+    lintType polytype_res++lintType :: (PrettyVar a, Ord a) => Type a -> ScopeM a ()+lintType (TyVar x) =+  check (fsep ["Type variable", nest 2 (ppVar x), "not in scope"])+    (isTyVar x)+lintType (TyCon x tys) = do+  info <- check' (fsep ["Type constructor", nest 2 (ppVar x), "not in scope"])+    (lookupType x)+  let checkArity n =+        unless (n == length tys) $+          throwError $ fsep [+            "Type constructor", nest 2 (ppVar x),+            "of arity" <+> int n,+            "applied to" <+> int (length tys) <+> "type arguments"]+  case info of+    TyVarInfo ->+      throwError (fsep ["Type variable", nest 2 (ppVar x), "used as type constructor"])+    SortInfo n -> checkArity n+    DatatypeInfo Datatype{..} -> checkArity (length data_tvs)+  mapM_ lintType tys+lintType (args :=>: res) = do+  mapM_ lintType args+  lintType res+lintType BuiltinType{} = return ()++lintSignature :: (PrettyVar a, Ord a) => Signature a -> ScopeM a ()+lintSignature func@Signature{..} =+  inContext func (lintPolyType sig_type)++lintFunction :: (PrettyVar a, Ord a) => Function a -> ScopeM a ()+lintFunction func@Function{..} =+  local $ inContext func $ do+    mapM_ newTyVar func_tvs+    mapM_ lintBinder func_args+    lintType func_res+    lintExpr ExprKind func_body+    unless (func_res == exprType func_body) $+      throwError (fsep [+        "Declared return type", nest 2 (pp func_res),+        "does not match actual return type", nest 2 (pp (exprType func_body))])++lintBinder :: (PrettyVar a, Ord a) => Local a -> ScopeM a ()+lintBinder lcl@Local{..} = do+  lintType lcl_type+  newLocal lcl++lintFormula :: (PrettyVar a, Ord a) => Formula a -> ScopeM a ()+lintFormula form@(Formula _ tvs expr) =+  local $ inContext form $ do+    mapM_ newTyVar tvs+    lintExpr FormulaKind expr+    unless (exprType expr == boolType) $+      throwError $+        fsep ["Formula has non-boolean type", nest 2 (pp (exprType expr))]++data ExprKind = ExprKind | FormulaKind deriving Eq++lintExpr :: (PrettyVar a, Ord a) => ExprKind -> Expr a -> ScopeM a ()+lintExpr _ (Gbl gbl@Global{..} :@: exprs) = do+  lintGlobal gbl+  mapM_ (lintExpr ExprKind) exprs+  let (args, _) = applyPolyType gbl_type gbl_args+  lintCall (Gbl gbl) exprs args+lintExpr kind (Builtin bltin :@: exprs) = do+  mapM_ (lintExpr (if isExpression bltin then ExprKind else kind)) exprs+  tys <- lintBuiltin bltin (map exprType exprs)+  lintCall (Builtin bltin) exprs tys+lintExpr _ (Lcl lcl@Local{..}) = do+  check ("Unbound variable" <+> pp lcl) (isLocal lcl_name)+  check ("Inconsistent type for local" <+> pp lcl) $+    \scp -> whichLocal lcl_name scp == lcl_type+lintExpr kind (Lam lcls expr) =+  local $ do+    mapM_ lintBinder lcls+    lintExpr ExprKind expr+lintExpr kind (Match expr cases) = do+  lintExpr (if kind == FormulaKind && exprType expr /= boolType then ExprKind else kind)+    expr+  when (null cases) $+    throwError "Case with no alternatives"+  mapM_ (lintCase kind expr) cases++  when (Default `elem` drop 1 (map case_pat cases)) $+    throwError "Default case is in wrong position"+  unless (Default `elem` map case_pat cases) $ do+    let strip (ConPat gbl _) = ConPat gbl []+        strip x = x+        stripped = map (strip . case_pat) cases+    unless (nub stripped == stripped) $+      throwError "The same constructor appears several times"+  unless (length (nub (map (exprType . case_rhs) cases)) == 1) $+    throwError "Not all case clauses have the same type"+lintExpr kind (Let lcl@Local{..} expr body) = do+  lintExpr ExprKind expr+  local $ do+    lintBinder lcl+    lintExpr kind body+  unless (lcl_type == exprType expr) $+    throwError (fsep [+      "Expression of type", nest 2 (pp (exprType expr)),+      "bound to variable" <+> pp lcl,+      "of type", nest 2 (pp lcl_type)])+lintExpr ExprKind (Quant NoInfo _ lcls expr) =+  throwError "Quantifier found in expression"+lintExpr FormulaKind (Quant NoInfo _ lcls expr) =+  local $ do+    mapM_ lintBinder lcls+    lintExpr FormulaKind expr++lintGlobal :: (PrettyVar a, Ord a) => Global a -> ScopeM a ()+lintGlobal gbl@Global{..} = do+  lintPolyType gbl_type+  mapM_ lintType gbl_args+  unless (length gbl_args == length (polytype_tvs gbl_type)) $+    throwError (fsep ["Global" <+> pp gbl, "applied to type arguments", nest 2 (vcat (map pp gbl_args)), "but expects" <+> int (length (polytype_tvs gbl_type))])+  check ("Unbound global" <+> pp gbl) (isGlobal gbl_name)++  scp <- get+  check (fsep ["Global" <+> pp gbl, "occurs with type", nest 2 (ppPolyType gbl_type), "but was declared with type", nest 2 (ppPolyType (globalType (whichGlobal gbl_name scp)))]) $+    \scp -> globalType (whichGlobal gbl_name scp) `polyEq` gbl_type+    where+      t `polyEq` PolyType{..} =+        applyPolyType t (map TyVar polytype_tvs) == (polytype_args, polytype_res)++lintCall :: (PrettyVar a, Ord a) => Head a -> [Expr a] -> [Type a] -> ScopeM a ()+lintCall hd exprs args =+  unless (args == map exprType exprs) $+    throwError (fsep ["Function" <+> pp hd, "which expects arguments of type", nest 2 (vcat (map pp args)), "applied to arguments of type", nest 2 (vcat (map pp (map exprType exprs))), "in", nest 2 (pp (hd :@: exprs))])++lintBuiltin :: (PrettyVar a, Ord a) => Builtin -> [Type a] -> ScopeM a [Type a]+lintBuiltin At [] = throwError "@ cannot have arity 0"+lintBuiltin At ((args :=>: res):_) =+  return ((args :=>: res):args)+lintBuiltin At (ty:_) =+  throwError (fsep ["First argument of @ has non-function type", nest 2 (pp ty)])+lintBuiltin Lit{} _ = return []+lintBuiltin And tys = return (replicate (length tys) boolType)+lintBuiltin Or tys = return (replicate (length tys) boolType)+lintBuiltin Not _ = return [boolType]+lintBuiltin Implies _ = return [boolType, boolType]+lintBuiltin Equal [] = throwError "Nullary ="+lintBuiltin Equal tys@(ty:_) = return (replicate (length tys) ty)+lintBuiltin Distinct [] = throwError "Nullary distinct"+lintBuiltin Distinct tys@(ty:_) = return (replicate (length tys) ty)+lintBuiltin IntAdd tys = return (replicate (length tys) intType)+lintBuiltin IntSub _ = return [intType, intType]+lintBuiltin IntMul _ = return [intType, intType]+lintBuiltin IntDiv _ = return [intType, intType]+lintBuiltin IntMod _ = return [intType, intType]+lintBuiltin IntGt _ = return [intType, intType]+lintBuiltin IntGe _ = return [intType, intType]+lintBuiltin IntLt _ = return [intType, intType]+lintBuiltin IntLe _ = return [intType, intType]++isExpression :: Builtin -> Bool+isExpression Equal = True+isExpression Distinct = True+isExpression IntGt = True+isExpression IntGe = True+isExpression IntLt = True+isExpression IntLe = True+isExpression _ = False++lintCase :: (PrettyVar a, Ord a) => ExprKind -> Expr a -> Case a -> ScopeM a ()+lintCase kind _ (Case Default body) = lintExpr kind body+lintCase kind _ (Case LitPat{} body) = lintExpr kind body+lintCase kind expr (Case (ConPat gbl@Global{..} args) body) =+  local $ do+    mapM_ lintBinder args+    lintExpr kind (Gbl gbl :@: map Lcl args)+    lintExpr kind body+    check ("Global" <+> pp gbl <+> "used as constructor")+      (isJust . lookupConstructor gbl_name)+    let (_, res) = applyPolyType gbl_type gbl_args+    unless (res == exprType expr) $+      throwError (fsep ["Constructor", nest 2 (pp (Gbl gbl :@: map Lcl args)), "has type", nest 2 (pp res), "but should be", nest 2 (pp (exprType expr))])
+ src/Tip/Parser.hs view
@@ -0,0 +1,19 @@+-- | Parses the TIP format+module Tip.Parser(parse,Id,idPos) where++import Data.Monoid++import Tip.Parser.ParTIP+import Tip.Parser.AbsTIP (Start(..))+import Tip.Parser.ErrM++import Tip.Parser.Convert+import Tip.Core++-- | Parse, and get either an error or the string's theory+parse :: String -> Either String (Theory Id)+parse s =+  case pStart . myLexer $ s of+    Ok (Start ds) -> runCM (trDecls ds)+    Bad err       -> Left err+
+ src/Tip/Parser/AbsTIP.hs view
@@ -0,0 +1,119 @@+++module Tip.Parser.AbsTIP where++-- Haskell module generated by the BNF converter+++++newtype Symbol = Symbol ((Int,Int),String) deriving (Eq,Ord,Show,Read)+data Start =+   Start [Decl]+  deriving (Eq,Ord,Show,Read)++data Decl =+   DeclareDatatypes [Symbol] [Datatype]+ | DeclareSort Symbol Integer+ | DeclareFun FunDecl+ | DefineFunsRec [FunDef] [Expr]+ | MonoAssert Assertion Expr+ | ParAssert Assertion [Symbol] Expr+  deriving (Eq,Ord,Show,Read)++data Assertion =+   AssertIt+ | AssertNot+  deriving (Eq,Ord,Show,Read)++data FunDef =+   ParFunDef [Symbol] InnerFunDef+ | MonoFunDef InnerFunDef+  deriving (Eq,Ord,Show,Read)++data InnerFunDef =+   InnerFunDef Symbol [Binding] Type+  deriving (Eq,Ord,Show,Read)++data FunDecl =+   ParFunDecl [Symbol] InnerFunDecl+ | MonoFunDecl InnerFunDecl+  deriving (Eq,Ord,Show,Read)++data InnerFunDecl =+   InnerFunDecl Symbol [Type] Type+  deriving (Eq,Ord,Show,Read)++data Datatype =+   Datatype Symbol [Constructor]+  deriving (Eq,Ord,Show,Read)++data Constructor =+   Constructor Symbol [Binding]+  deriving (Eq,Ord,Show,Read)++data Binding =+   Binding Symbol Type+  deriving (Eq,Ord,Show,Read)++data LetDecl =+   LetDecl Binding Expr+  deriving (Eq,Ord,Show,Read)++data Type =+   TyVar Symbol+ | TyApp Symbol [Type]+ | ArrowTy [Type]+ | IntTy+ | BoolTy+  deriving (Eq,Ord,Show,Read)++data Expr =+   Var Symbol+ | As Expr Type+ | App Head [Expr]+ | Match Expr [Case]+ | Let [LetDecl] Expr+ | Binder Binder [Binding] Expr+ | LitInt Integer+ | LitTrue+ | LitFalse+  deriving (Eq,Ord,Show,Read)++data Binder =+   Lambda+ | Forall+ | Exists+  deriving (Eq,Ord,Show,Read)++data Case =+   Case Pattern Expr+  deriving (Eq,Ord,Show,Read)++data Pattern =+   Default+ | ConPat Symbol [Symbol]+ | SimplePat Symbol+  deriving (Eq,Ord,Show,Read)++data Head =+   Const Symbol+ | At+ | IfThenElse+ | And+ | Or+ | Not+ | Implies+ | Equal+ | Distinct+ | IntAdd+ | IntSub+ | IntMul+ | IntDiv+ | IntMod+ | IntGt+ | IntGe+ | IntLt+ | IntLe+  deriving (Eq,Ord,Show,Read)+
+ src/Tip/Parser/Convert.hs view
@@ -0,0 +1,302 @@+{-# LANGUAGE OverloadedStrings #-}+module Tip.Parser.Convert where++import Tip.Parser.AbsTIP as A -- from A ...+import Tip.Core          as T -- ... to T+import Tip.Pretty+import Tip.Pretty.SMT++import Text.PrettyPrint+import Control.Applicative+import Control.Monad.State+import Control.Monad.Error+import Data.Foldable (foldrM)++import qualified Tip.Scope+import Tip.Scope+import Tip.Fresh++import Data.List+import Data.Function++import Data.Map (Map)+import qualified Data.Map as M++data IdKind = LocalId | GlobalId+  deriving Eq++type CM a = ScopeT Id (StateT (Map String (Id,IdKind)) Fresh) a++runCM :: CM a -> Either String a+runCM m = either (Left . show) Right $ runFresh (evalStateT (runScopeT m) M.empty)++-- | Identifiers from parsed Tip syntax+data Id = Id+  { idString :: String+  , idUnique :: Int+  , idPos    :: Maybe (Int,Int)+  -- ^ A source position of the identifier, if available+  }+  deriving Show++instance Eq Id where+  (==) = (==) `on` idUnique++instance Ord Id where+  compare = compare `on` idUnique++instance PrettyVar Id where+  varStr (Id s _ _) = s++instance Name Id where+  freshNamed n+    = do u <- fresh+         return (Id n u Nothing)++  fresh = freshNamed "x"++  refresh = refreshNamed ""++  getUnique (Id _ u _) = u++ppSym :: Symbol -> Doc+ppSym (Symbol ((x,y),s)) = text s <+> "(" <> int x <> ":" <> int y <> ")"++lkSym :: Symbol -> CM Id+lkSym sym@(Symbol (p,s)) =+  do mik <- lift $ gets (M.lookup s)+     case mik of+       Just (i,_) -> return $ i { idPos = Just p }+       Nothing    -> throwError $ "Symbol" <+> ppSym sym <+> "not bound"++addSym :: IdKind -> Symbol -> CM Id+addSym ik sym@(Symbol (p,s)) =+  do mik <- lift $ gets (M.lookup s)+     case mik of+       Just (_,GlobalId)       -> throwError $ "Symbol" <+> ppSym sym <+> "is already globally bound"+       Just _ | ik == GlobalId -> throwError $ "Symbol" <+> ppSym sym <+> "is locally bound, and cannot be overwritten by a global"+       _                       -> return ()+     u <- lift (lift fresh)+     let i = Id s u (Just p)+     lift $ modify (M.insert s (i,ik))+     return i++trDecls :: [Decl] -> CM (Theory Id)+trDecls [] = return emptyTheory+trDecls (d:ds) =+  do thy <- trDecl d+     withTheory thy $+       do thy_rest <- trDecls ds+          return (thy `joinTheories` thy_rest)++trDecl :: Decl -> CM (Theory Id)+trDecl x =+  local $+    case x of+      DeclareDatatypes tvs datatypes ->+        do -- add their types, abstractly+           forM_ datatypes $ \dt -> do+             sym <- addSym GlobalId (dataSym dt)+             newSort (Sort sym (length tvs))+           newScope $+             do tvi <- mapM (addSym LocalId) tvs+                mapM newTyVar tvi+                ds <- mapM (trDatatype tvi) datatypes+                return emptyTheory{ thy_datatypes = ds }++      DeclareSort s n ->+        do i <- addSym GlobalId s+           return emptyTheory{ thy_sorts = [Sort i (fromIntegral n)] }++      DeclareFun fundecl ->+        do d <- trFunDecl fundecl+           return emptyTheory{ thy_sigs = [d] }++      DefineFunsRec fundefs bodies ->+        do -- add their correct types, abstractly+           fds <- mapM (trFunDecl . defToDecl) fundefs+           withTheory emptyTheory{ thy_sigs = fds } $ do+             fns <- zipWithM trFunDef fundefs bodies+             return emptyTheory{ thy_funcs = fns }++      MonoAssert role expr    -> trDecl (ParAssert role [] expr)+      ParAssert role tvs expr ->+        do tvi <- mapM (addSym LocalId) tvs+           mapM newTyVar tvi+           let toRole AssertIt  = Assert+               toRole AssertNot = Prove+           fm <- Formula (toRole role) tvi <$> trExpr expr+           return emptyTheory{ thy_asserts = [fm] }++++defToDecl :: FunDef -> FunDecl+defToDecl x = case x of+  MonoFunDef inner -> defToDecl (ParFunDef [] inner)+  ParFunDef tvs (InnerFunDef fsym bindings res_type) ->+    ParFunDecl tvs (InnerFunDecl fsym (map bindingType bindings) res_type)++trFunDef :: FunDef -> A.Expr -> CM (T.Function Id)+trFunDef x body = case x of+  MonoFunDef inner -> trFunDef (ParFunDef [] inner) body+  ParFunDef tvs (InnerFunDef fsym bindings res_type) ->+    newScope $+      do f <- lkSym fsym+         tvi <- mapM (addSym LocalId) tvs+         mapM newTyVar tvi+         args <- mapM trLocalBinding bindings+         Function f tvi args <$> trType res_type <*> trExpr body++trFunDecl :: FunDecl -> CM (T.Signature Id)+trFunDecl x = case x of+  MonoFunDecl inner -> trFunDecl (ParFunDecl [] inner)+  ParFunDecl tvs (InnerFunDecl fsym args res) ->+    newScope $+      do f <- addSym GlobalId fsym+         tvi <- mapM (addSym LocalId) tvs+         mapM newTyVar tvi+         pt <- PolyType tvi <$> mapM trType args <*> trType res+         return (Signature f pt)++dataSym :: A.Datatype -> Symbol+dataSym (A.Datatype sym _) = sym++trDatatype :: [Id] -> A.Datatype -> CM (T.Datatype Id)+trDatatype tvs (A.Datatype sym constructors) =+  do x <- lkSym sym+     T.Datatype x tvs <$> mapM trConstructor constructors++trConstructor :: A.Constructor -> CM (T.Constructor Id)+trConstructor (A.Constructor name@(Symbol (p,s)) args) =+  do c <- addSym GlobalId name+     is_c <- addSym GlobalId (Symbol (p,"is-" ++ s))+     T.Constructor c is_c <$> mapM (trBinding GlobalId) args++bindingType :: Binding -> A.Type+bindingType (Binding _ t) = t++-- adds to the symbol map+trBinding :: IdKind -> Binding -> CM (Id,T.Type Id)+trBinding ik (Binding s t) =+  do i <- addSym ik s+     t' <- trType t+     return (i,t')++-- adds to the symbol map and to the local scope+trLocalBinding :: Binding -> CM (Local Id)+trLocalBinding b =+  do (x,t) <- trBinding LocalId b+     let l = Local x t+     newLocal l+     return l++trLetDecls :: [LetDecl] -> A.Expr -> CM (T.Expr Id)+trLetDecls [] e = trExpr e+trLetDecls (LetDecl binding expr:bs) e+  = newScope $ T.Let <$> trLocalBinding binding <*> trExpr expr <*> trLetDecls bs e++trExpr :: A.Expr -> CM (T.Expr Id)+trExpr e0 = case e0 of+  A.Var sym ->+    do x <- lkSym sym+       ml <- gets (lookupLocal x)+       case ml of+         Just t -> return (Lcl (Local x t))+         _      -> trExpr (A.App (A.Const sym) [])++  A.As (A.Var sym) ty -> trExpr (A.As (A.App (A.Const sym) []) ty)+  A.As (A.App head exprs) ty -> do ty' <- trType ty+                                   trHead (Just ty') head =<< mapM trExpr exprs+  A.As e _ -> trExpr e++  A.App head exprs           -> trHead Nothing head =<< mapM trExpr exprs++  A.Match expr cases  -> do e <- trExpr expr+                            cases' <- sort <$> mapM (trCase (exprType e)) cases+                            return (T.Match e cases')+  A.Let letdecls expr -> trLetDecls letdecls expr+  A.Binder binder bindings expr -> newScope $ trBinder binder <$> mapM trLocalBinding bindings <*> trExpr expr+  A.LitInt n -> return $ intLit n+  A.LitTrue  -> return $ bool True+  A.LitFalse -> return $ bool False++trHead :: Maybe (T.Type Id) -> A.Head -> [T.Expr Id] -> CM (T.Expr Id)+trHead mgt A.IfThenElse  [c,t,f] = return (makeIf c t f)+trHead mgt A.IfThenElse  args    = throwError $ "if-then-else with " <+> int (length args) <+> " arguments!"+trHead mgt (A.Const sym) args    =+  do x <- lkSym sym+     mt <- gets (fmap globalType . lookupGlobal x)+     case mt of+       Just pt+         | Just gbl <- makeGlobal x pt (map exprType args) mgt+         -> return (Gbl gbl :@: args)+         | otherwise+         -> throwError $ "Not a well-applied global:" <+> ppSym sym+                      $$ " with goal type " <+> case mgt of Nothing -> "Nothing"; Just t -> pp t+                      $$ " with argument types " <+> fsep (punctuate "," (map (pp . exprType) args))+                      $$ " with polymorphic type " <+> pp pt+       _ -> throwError $ "No type information for:" <+> ppSym sym++trHead _ x args = return (Builtin b :@: args)+ where+  b = case x of+    A.At       -> T.At+    A.And      -> T.And+    A.Or       -> T.Or+    A.Not      -> T.Not+    A.Implies  -> T.Implies+    A.Equal    -> T.Equal+    A.Distinct -> T.Distinct+    A.IntAdd   -> T.IntAdd+    A.IntSub   -> T.IntSub+    A.IntMul   -> T.IntMul+    A.IntDiv   -> T.IntDiv+    A.IntMod   -> T.IntMod+    A.IntGt    -> T.IntGt+    A.IntGe    -> T.IntGe+    A.IntLt    -> T.IntLt+    A.IntLe    -> T.IntLe+++trBinder :: A.Binder -> [Local Id] -> T.Expr Id -> T.Expr Id+trBinder b = case b of+  A.Lambda -> T.Lam+  A.Forall -> mkQuant T.Forall+  A.Exists -> mkQuant T.Exists++trCase :: T.Type Id -> A.Case -> CM (T.Case Id)+trCase goal_type (A.Case pattern expr) =+  newScope $ T.Case <$> trPattern goal_type pattern <*> trExpr expr++trPattern :: T.Type Id -> A.Pattern -> CM (T.Pattern Id)+trPattern goal_type p = case p of+  A.Default          -> return T.Default+  A.SimplePat sym    -> trPattern goal_type (A.ConPat sym [])+  A.ConPat sym bound ->+    do x <- lkSym sym+       mt <- gets (fmap globalType . lookupGlobal x)+       case mt of+         Just pt@(PolyType tvs arg res)+           | Just ty_app <- matchTypesIn tvs [(res,goal_type)] ->+             do let (var_types, _) = applyPolyType pt ty_app+                ls <- sequence+                   [ do b <- addSym LocalId b_sym+                        let l = Local b t+                        newLocal l+                        return l+                   | (b_sym,t) <- bound `zip` var_types+                   ]+                return (T.ConPat (Global x pt ty_app) ls)+         _ -> throwError $ "type-incorrect case"++trType :: A.Type -> CM (T.Type Id)+trType t0 = case t0 of+  A.TyVar s -> do x <- lkSym s+                  mtv <- gets (isTyVar x)+                  if mtv then return (T.TyVar x)+                         else trType (A.TyApp s [])+  A.TyApp s ts -> T.TyCon <$> lkSym s <*> mapM trType ts+  A.ArrowTy ts -> (:=>:) <$> mapM trType (init ts) <*> trType (last ts)+  A.IntTy      -> return intType+  A.BoolTy     -> return boolType+
+ src/Tip/Parser/ErrM.hs view
@@ -0,0 +1,37 @@+-- BNF Converter: Error Monad+-- Copyright (C) 2004  Author:  Aarne Ranta++-- This file comes with NO WARRANTY and may be used FOR ANY PURPOSE.+module Tip.Parser.ErrM where++-- the Error monad: like Maybe type with error msgs++import Control.Monad (MonadPlus(..), liftM)+import Control.Applicative (Applicative(..), Alternative(..))++data Err a = Ok a | Bad String+  deriving (Read, Show, Eq, Ord)++instance Monad Err where+  return      = Ok+  fail        = Bad+  Ok a  >>= f = f a+  Bad s >>= _ = Bad s++instance Applicative Err where+  pure = Ok+  (Bad s) <*> _ = Bad s+  (Ok f) <*> o  = liftM f o+++instance Functor Err where+  fmap = liftM++instance MonadPlus Err where+  mzero = Bad "Err.mzero"+  mplus (Bad _) y = y+  mplus x       _ = x++instance Alternative Err where+  empty = mzero+  (<|>) = mplus
+ src/Tip/Parser/LexTIP.x view
@@ -0,0 +1,183 @@+-- -*- haskell -*-+-- This Alex file was machine-generated by the BNF converter+{+{-# OPTIONS -fno-warn-incomplete-patterns #-}+{-# OPTIONS_GHC -w #-}+module Tip.Parser.LexTIP where++++import qualified Data.Bits+import Data.Word (Word8)+}+++$l = [a-zA-Z\192 - \255] # [\215 \247]    -- isolatin1 letter FIXME+$c = [A-Z\192-\221] # [\215]    -- capital isolatin1 letter FIXME+$s = [a-z\222-\255] # [\247]    -- small isolatin1 letter FIXME+$d = [0-9]                -- digit+$i = [$l $d _ ']          -- identifier character+$u = [\0-\255]          -- universal: any character++@rsyms =    -- symbols and non-identifier-like reserved words+   \( | "check" \- "sat" | \) | "declare" \- "datatypes" | "declare" \- "sort" | "declare" \- "fun" | "define" \- "funs" \- "rec" | "assert" \- "not" | \= \> | \@ | \= | \+ | \- | \* | \> | \> \= | \< | \< \=++:-+";" [.]* ; -- Toss single line comments++$white+ ;+@rsyms { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }+($l | [\~ \! \@ \$ \% \^ \& \* \_ \- \+ \= \< \> \. \? \/]) ($l | $d | [\~ \! \@ \$ \% \^ \& \* \_ \- \+ \= \< \> \. \? \/]) * { tok (\p s -> PT p (eitherResIdent (T_Symbol . share) s)) }++$l $i*   { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }+++$d+      { tok (\p s -> PT p (TI $ share s))    }+++{++tok :: (Posn -> String -> Token) -> (Posn -> String -> Token)+tok f p s = f p s++share :: String -> String+share = id++data Tok =+   TS !String !Int    -- reserved words and symbols+ | TL !String         -- string literals+ | TI !String         -- integer literals+ | TV !String         -- identifiers+ | TD !String         -- double precision float literals+ | TC !String         -- character literals+ | T_Symbol !String++ deriving (Eq,Show,Ord)++data Token =+   PT  Posn Tok+ | Err Posn+  deriving (Eq,Show,Ord)++tokenPos :: [Token] -> String+tokenPos (PT (Pn _ l _) _ :_) = "line " ++ show l+tokenPos (Err (Pn _ l _) :_) = "line " ++ show l+tokenPos _ = "end of file"++tokenPosn :: Token -> Posn+tokenPosn (PT p _) = p+tokenPosn (Err p) = p++tokenLineCol :: Token -> (Int, Int)+tokenLineCol = posLineCol . tokenPosn++posLineCol :: Posn -> (Int, Int)+posLineCol (Pn _ l c) = (l,c)++mkPosToken :: Token -> ((Int, Int), String)+mkPosToken t@(PT p _) = (posLineCol p, prToken t)++prToken :: Token -> String+prToken t = case t of+  PT _ (TS s _) -> s+  PT _ (TL s)   -> s+  PT _ (TI s)   -> s+  PT _ (TV s)   -> s+  PT _ (TD s)   -> s+  PT _ (TC s)   -> s+  PT _ (T_Symbol s) -> s+++data BTree = N | B String Tok BTree BTree deriving (Show)++eitherResIdent :: (String -> Tok) -> String -> Tok+eitherResIdent tv s = treeFind resWords+  where+  treeFind N = tv s+  treeFind (B a t left right) | s < a  = treeFind left+                              | s > a  = treeFind right+                              | s == a = t++resWords :: BTree+resWords = b "check-sat" 20 (b ">" 10 (b "-" 5 (b "*" 3 (b ")" 2 (b "(" 1 N N) N) (b "+" 4 N N)) (b "=" 8 (b "<=" 7 (b "<" 6 N N) N) (b "=>" 9 N N))) (b "and" 15 (b "Bool" 13 (b "@" 12 (b ">=" 11 N N) N) (b "Int" 14 N N)) (b "assert-not" 18 (b "assert" 17 (b "as" 16 N N) N) (b "case" 19 N N)))) (b "forall" 30 (b "define-funs-rec" 25 (b "declare-sort" 23 (b "declare-fun" 22 (b "declare-datatypes" 21 N N) N) (b "default" 24 N N)) (b "exists" 28 (b "div" 27 (b "distinct" 26 N N) N) (b "false" 29 N N))) (b "mod" 35 (b "let" 33 (b "lambda" 32 (b "ite" 31 N N) N) (b "match" 34 N N)) (b "par" 38 (b "or" 37 (b "not" 36 N N) N) (b "true" 39 N N))))+   where b s n = let bs = id s+                  in B bs (TS bs n)++unescapeInitTail :: String -> String+unescapeInitTail = id . unesc . tail . id where+  unesc s = case s of+    '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs+    '\\':'n':cs  -> '\n' : unesc cs+    '\\':'t':cs  -> '\t' : unesc cs+    '"':[]    -> []+    c:cs      -> c : unesc cs+    _         -> []++-------------------------------------------------------------------+-- Alex wrapper code.+-- A modified "posn" wrapper.+-------------------------------------------------------------------++data Posn = Pn !Int !Int !Int+      deriving (Eq, Show,Ord)++alexStartPos :: Posn+alexStartPos = Pn 0 1 1++alexMove :: Posn -> Char -> Posn+alexMove (Pn a l c) '\t' = Pn (a+1)  l     (((c+7) `div` 8)*8+1)+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1)   1+alexMove (Pn a l c) _    = Pn (a+1)  l     (c+1)++type Byte = Word8++type AlexInput = (Posn,     -- current position,+                  Char,     -- previous char+                  [Byte],   -- pending bytes on the current char+                  String)   -- current input string++tokens :: String -> [Token]+tokens str = go (alexStartPos, '\n', [], str)+    where+      go :: AlexInput -> [Token]+      go inp@(pos, _, _, str) =+               case alexScan inp 0 of+                AlexEOF                   -> []+                AlexError (pos, _, _, _)  -> [Err pos]+                AlexSkip  inp' len        -> go inp'+                AlexToken inp' len act    -> act pos (take len str) : (go inp')++alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))+alexGetByte (p, _, [], s) =+  case  s of+    []  -> Nothing+    (c:s) ->+             let p'     = alexMove p c+                 (b:bs) = utf8Encode c+              in p' `seq` Just (b, (p', c, bs, s))++alexInputPrevChar :: AlexInput -> Char+alexInputPrevChar (p, c, bs, s) = c++-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.+utf8Encode :: Char -> [Word8]+utf8Encode = map fromIntegral . go . ord+ where+  go oc+   | oc <= 0x7f       = [oc]++   | oc <= 0x7ff      = [ 0xc0 + (oc `Data.Bits.shiftR` 6)+                        , 0x80 + oc Data.Bits..&. 0x3f+                        ]++   | oc <= 0xffff     = [ 0xe0 + (oc `Data.Bits.shiftR` 12)+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)+                        , 0x80 + oc Data.Bits..&. 0x3f+                        ]+   | otherwise        = [ 0xf0 + (oc `Data.Bits.shiftR` 18)+                        , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)+                        , 0x80 + oc Data.Bits..&. 0x3f+                        ]+}
+ src/Tip/Parser/ParTIP.y view
@@ -0,0 +1,277 @@+-- This Happy file was machine-generated by the BNF converter+{+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}+module Tip.Parser.ParTIP where+import Tip.Parser.AbsTIP+import Tip.Parser.LexTIP+import Tip.Parser.ErrM++}++%name pStart Start+%name pListDecl ListDecl+%name pDecl Decl+%name pAssertion Assertion+%name pFunDef FunDef+%name pInnerFunDef InnerFunDef+%name pFunDecl FunDecl+%name pInnerFunDecl InnerFunDecl+%name pDatatype Datatype+%name pConstructor Constructor+%name pBinding Binding+%name pLetDecl LetDecl+%name pType Type+%name pExpr Expr+%name pBinder Binder+%name pCase Case+%name pPattern Pattern+%name pHead Head+%name pListLetDecl ListLetDecl+%name pListCase ListCase+%name pListExpr ListExpr+%name pListDatatype ListDatatype+%name pListConstructor ListConstructor+%name pListBinding ListBinding+%name pListSymbol ListSymbol+%name pListType ListType+%name pListFunDecl ListFunDecl+%name pListFunDef ListFunDef++-- no lexer declaration+%monad { Err } { thenM } { returnM }+%tokentype { Token }++%token+  '(' { PT _ (TS _ 1) }+  ')' { PT _ (TS _ 2) }+  '*' { PT _ (TS _ 3) }+  '+' { PT _ (TS _ 4) }+  '-' { PT _ (TS _ 5) }+  '<' { PT _ (TS _ 6) }+  '<=' { PT _ (TS _ 7) }+  '=' { PT _ (TS _ 8) }+  '=>' { PT _ (TS _ 9) }+  '>' { PT _ (TS _ 10) }+  '>=' { PT _ (TS _ 11) }+  '@' { PT _ (TS _ 12) }+  'Bool' { PT _ (TS _ 13) }+  'Int' { PT _ (TS _ 14) }+  'and' { PT _ (TS _ 15) }+  'as' { PT _ (TS _ 16) }+  'assert' { PT _ (TS _ 17) }+  'assert-not' { PT _ (TS _ 18) }+  'case' { PT _ (TS _ 19) }+  'check-sat' { PT _ (TS _ 20) }+  'declare-datatypes' { PT _ (TS _ 21) }+  'declare-fun' { PT _ (TS _ 22) }+  'declare-sort' { PT _ (TS _ 23) }+  'default' { PT _ (TS _ 24) }+  'define-funs-rec' { PT _ (TS _ 25) }+  'distinct' { PT _ (TS _ 26) }+  'div' { PT _ (TS _ 27) }+  'exists' { PT _ (TS _ 28) }+  'false' { PT _ (TS _ 29) }+  'forall' { PT _ (TS _ 30) }+  'ite' { PT _ (TS _ 31) }+  'lambda' { PT _ (TS _ 32) }+  'let' { PT _ (TS _ 33) }+  'match' { PT _ (TS _ 34) }+  'mod' { PT _ (TS _ 35) }+  'not' { PT _ (TS _ 36) }+  'or' { PT _ (TS _ 37) }+  'par' { PT _ (TS _ 38) }+  'true' { PT _ (TS _ 39) }++L_integ  { PT _ (TI $$) }+L_Symbol { PT _ (T_Symbol _) }+++%%++Integer :: { Integer } : L_integ  { (read ( $1)) :: Integer }+Symbol    :: { Symbol} : L_Symbol { Symbol (mkPosToken $1)}++Start :: { Start }+Start : ListDecl { Start $1 } +++ListDecl :: { [Decl] }+ListDecl : '(' 'check-sat' ')' { [] } +  | '(' Decl ')' ListDecl { (:) $2 $4 }+++Decl :: { Decl }+Decl : 'declare-datatypes' '(' ListSymbol ')' '(' ListDatatype ')' { DeclareDatatypes (reverse $3) (reverse $6) } +  | 'declare-sort' Symbol Integer { DeclareSort $2 $3 }+  | 'declare-fun' FunDecl { DeclareFun $2 }+  | 'define-funs-rec' '(' ListFunDef ')' '(' ListExpr ')' { DefineFunsRec (reverse $3) (reverse $6) }+  | Assertion Expr { MonoAssert $1 $2 }+  | Assertion '(' 'par' '(' ListSymbol ')' Expr ')' { ParAssert $1 (reverse $5) $7 }+++Assertion :: { Assertion }+Assertion : 'assert' { AssertIt } +  | 'assert-not' { AssertNot }+++FunDef :: { FunDef }+FunDef : '(' 'par' '(' ListSymbol ')' InnerFunDef ')' { ParFunDef (reverse $4) $6 } +  | InnerFunDef { MonoFunDef $1 }+++InnerFunDef :: { InnerFunDef }+InnerFunDef : '(' Symbol '(' ListBinding ')' Type ')' { InnerFunDef $2 (reverse $4) $6 } +++FunDecl :: { FunDecl }+FunDecl : '(' 'par' '(' ListSymbol ')' '(' InnerFunDecl ')' ')' { ParFunDecl (reverse $4) $7 } +  | InnerFunDecl { MonoFunDecl $1 }+++InnerFunDecl :: { InnerFunDecl }+InnerFunDecl : Symbol '(' ListType ')' Type { InnerFunDecl $1 (reverse $3) $5 } +++Datatype :: { Datatype }+Datatype : '(' Symbol ListConstructor ')' { Datatype $2 (reverse $3) } +++Constructor :: { Constructor }+Constructor : '(' Symbol ListBinding ')' { Constructor $2 (reverse $3) } +++Binding :: { Binding }+Binding : '(' Symbol Type ')' { Binding $2 $3 } +++LetDecl :: { LetDecl }+LetDecl : '(' Binding Expr ')' { LetDecl $2 $3 } +++Type :: { Type }+Type : Symbol { TyVar $1 } +  | '(' Symbol ListType ')' { TyApp $2 (reverse $3) }+  | '(' '=>' ListType ')' { ArrowTy (reverse $3) }+  | 'Int' { IntTy }+  | 'Bool' { BoolTy }+++Expr :: { Expr }+Expr : Symbol { Var $1 } +  | '(' 'as' Expr Type ')' { As $3 $4 }+  | '(' Head ListExpr ')' { App $2 (reverse $3) }+  | '(' 'match' Expr ListCase ')' { Match $3 (reverse $4) }+  | '(' 'let' '(' ListLetDecl ')' Expr ')' { Let (reverse $4) $6 }+  | '(' Binder '(' ListBinding ')' Expr ')' { Binder $2 (reverse $4) $6 }+  | Integer { LitInt $1 }+  | 'true' { LitTrue }+  | 'false' { LitFalse }+++Binder :: { Binder }+Binder : 'lambda' { Lambda } +  | 'forall' { Forall }+  | 'exists' { Exists }+++Case :: { Case }+Case : '(' 'case' Pattern Expr ')' { Case $3 $4 } +++Pattern :: { Pattern }+Pattern : 'default' { Default } +  | '(' Symbol ListSymbol ')' { ConPat $2 (reverse $3) }+  | Symbol { SimplePat $1 }+++Head :: { Head }+Head : Symbol { Const $1 } +  | '@' { At }+  | 'ite' { IfThenElse }+  | 'and' { And }+  | 'or' { Or }+  | 'not' { Not }+  | '=>' { Implies }+  | '=' { Equal }+  | 'distinct' { Distinct }+  | '+' { IntAdd }+  | '-' { IntSub }+  | '*' { IntMul }+  | 'div' { IntDiv }+  | 'mod' { IntMod }+  | '>' { IntGt }+  | '>=' { IntGe }+  | '<' { IntLt }+  | '<=' { IntLe }+++ListLetDecl :: { [LetDecl] }+ListLetDecl : {- empty -} { [] } +  | ListLetDecl LetDecl { flip (:) $1 $2 }+++ListCase :: { [Case] }+ListCase : {- empty -} { [] } +  | ListCase Case { flip (:) $1 $2 }+++ListExpr :: { [Expr] }+ListExpr : {- empty -} { [] } +  | ListExpr Expr { flip (:) $1 $2 }+++ListDatatype :: { [Datatype] }+ListDatatype : {- empty -} { [] } +  | ListDatatype Datatype { flip (:) $1 $2 }+++ListConstructor :: { [Constructor] }+ListConstructor : {- empty -} { [] } +  | ListConstructor Constructor { flip (:) $1 $2 }+++ListBinding :: { [Binding] }+ListBinding : {- empty -} { [] } +  | ListBinding Binding { flip (:) $1 $2 }+++ListSymbol :: { [Symbol] }+ListSymbol : {- empty -} { [] } +  | ListSymbol Symbol { flip (:) $1 $2 }+++ListType :: { [Type] }+ListType : {- empty -} { [] } +  | ListType Type { flip (:) $1 $2 }+++ListFunDecl :: { [FunDecl] }+ListFunDecl : {- empty -} { [] } +  | ListFunDecl FunDecl { flip (:) $1 $2 }+++ListFunDef :: { [FunDef] }+ListFunDef : {- empty -} { [] } +  | ListFunDef FunDef { flip (:) $1 $2 }++++{++returnM :: a -> Err a+returnM = return++thenM :: Err a -> (a -> Err b) -> Err b+thenM = (>>=)++happyError :: [Token] -> Err a+happyError ts =+  Bad $ "syntax error at " ++ tokenPos ts ++ +  case ts of+    [] -> []+    [Err _] -> " due to lexer error"+    _ -> " before " ++ unwords (map (id . prToken) (take 4 ts))++myLexer = tokens+}+
+ src/Tip/Pass/AddMatch.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE PatternGuards, RecordWildCards #-}+module Tip.Pass.AddMatch where++import Tip.Core+import Tip.Fresh+import Tip.Scope+import qualified Data.Map as Map+import Data.Map(Map)++-- | Replace SMTLIB-style selector and discriminator functions+--   (@is-nil@, @head@, @tail@) with case expressions.+addMatch :: Name a => Theory a -> Fresh (Theory a)+addMatch thy =+  flip transformExprInM thy $ \e ->+    case e of+      Gbl Global{..} :@: [t] | Just (d, c) <- lookupDiscriminator gbl_name scp -> do+        let con = constructor d c gbl_args+        args <- freshArgs con+        return $+          Match t [+            Case Default (bool False),+            Case (ConPat con args) (bool True) ]+      Gbl Global{..} :@: [t] | Just (d, c, i, _) <- lookupProjector gbl_name scp -> do+        let con = constructor d c gbl_args+        args <- freshArgs con+        return $+          Match t [+            Case (ConPat con args) (Lcl (args !! i)) ]+      _ -> return e+  where+    scp = scope thy
+ src/Tip/Pass/AxiomatizeFuncdefs.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Tip.Pass.AxiomatizeFuncdefs where++#include "errors.h"+import Tip.Core+import Tip.Fresh++import Data.Generics.Geniplate+import Control.Applicative++--conProjs :: Project a => Global a -> [Global a]+conProjs = undefined+{- (Global k (PolyType tvs arg_tys res_ty) ts _)+  = [ Global (project k i) (PolyType tvs [res_ty] arg_ty) ts ProjectNS+    | (i,arg_ty) <- zip [0..] arg_tys+    ]+    -}++axiomatizeFuncdefs :: Theory a -> Theory a+axiomatizeFuncdefs thy@Theory{..} =+  thy{+    thy_funcs   = [],+    thy_sigs    = thy_sigs ++ abs,+    thy_asserts = fms ++ thy_asserts+  }+ where+  (abs,fms) = unzip (map axiomatize thy_funcs)++-- Passes needed afterwards:+--+-- 1)  x = e ==> F[x] ~~> F[e]+--+-- 2)+--     all x (D => (all y . E) /\ (all z . F))+-- ~~>+--     all x ((D => all y . E) /\ (D => all z . F))+-- ~~>+--     (all x y (D => E)) /\ (all x z (D => F))+--+-- (TODO)++axiomatize :: forall a . Function a -> (Signature a, Formula a)+axiomatize fn@Function{..} =+  ( Signature func_name (funcType fn)+  , Formula Assert func_tvs (ax func_body)+  )+ where+  lhs = applyFunction fn (map TyVar func_tvs) (map Lcl func_args)++  ax :: Expr a -> Expr a+  ax e0 = case e0 of+    Match s (Case Default def_rhs:alts) -> invert_alts s alts def_rhs /\ ax_alts s alts+    Match s alts -> ax_alts s alts+    Let{}        -> __ -- could use ==> while Let is neither recursive nor polymorphic+    Lam{}        -> __+    Quant{}      -> __+    _            -> lhs === e0 -- e0 should now only be (:@:) and Lcl+   where+    invert_alts :: Expr a -> [Case a] -> Expr a -> Expr a+    invert_alts _ []                def_rhs = def_rhs+    invert_alts s (Case pat _:alts) def_rhs = s === invert_pat s pat \/+                                              invert_alts s alts def_rhs+     where+      invert_pat :: Expr a -> Pattern a -> Expr a+      invert_pat _ Default      = __+      invert_pat _ (LitPat lit) = literal lit+      invert_pat s (ConPat k _) = Gbl k :@: [ Gbl p :@: [s] | p <- conProjs k ]++    ax_alts :: Expr a -> [Case a] -> Expr a+    ax_alts s alts = ands [ ax_pat s pat rhs | Case pat rhs <- alts ]+     where+      ax_pat :: Expr a -> Pattern a -> Expr a -> Expr a+      ax_pat _ Default       _   = __+      ax_pat s (LitPat lit)  rhs = s === literal lit ==> ax rhs+      ax_pat s (ConPat k bs) rhs = mkQuant Forall bs+                                     (s === Gbl k :@: map Lcl bs ==> ax rhs)+
+ src/Tip/Pass/Booleans.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE FlexibleContexts, ViewPatterns, RecordWildCards #-}+module Tip.Pass.Booleans where++import Tip.Core++import Data.Generics.Geniplate++-- | Transforms boolean operators to if, but not in expression contexts.+theoryBoolOpToIf :: Ord a => Theory a -> Theory a+theoryBoolOpToIf Theory{..} =+  Theory{+    thy_funcs   = map boolOpToIf thy_funcs,+    thy_asserts =+      let k fm@Formula{..} = fm { fm_body = formulaBoolOpToIf fm_body }+      in  map k thy_asserts,+    ..+  }++formulaBoolOpToIf :: Ord a => Expr a -> Expr a+formulaBoolOpToIf e0 =+  case e0 of+    Builtin op :@: args@(a:_)+      | op `elem` [And,Or,Not,Implies] ||+        op `elem` [Equal,Distinct] && hasBoolType a ->+        Builtin op :@: map formulaBoolOpToIf args+    Quant qi q as e -> Quant qi q as (formulaBoolOpToIf e)+    _ -> boolOpToIf e0++hasBoolType :: Ord a => Expr a -> Bool+hasBoolType e = exprType e == boolType++-- | Transforms @and@, @or@, @=>@, @not@ and @=@ and @distict@ on @Bool@+--   into @ite@ (i.e. @match@)+boolOpToIf :: (Ord a,TransformBi (Expr a) (f a)) => f a -> f a+boolOpToIf = transformExprIn $+  \ e0 -> case e0 of+    Builtin And :@: [a,b]     -> makeIf a b falseExpr+    Builtin Or  :@: [a,b]     -> makeIf a trueExpr b+    Builtin Not :@: [a]       -> makeIf a falseExpr trueExpr+    Builtin Implies :@: [a,b] -> makeIf a b trueExpr+    Builtin Equal    :@: [a,b] | hasBoolType a -> makeIf a b (neg_if b)+    Builtin Distinct :@: [a,b] | hasBoolType a -> makeIf a (neg_if b) b+    _ -> e0+  where+    neg_if a = makeIf a falseExpr trueExpr++-- | Transforms @ite@ (@match@) on boolean literals in the branches+--   into the corresponding builtin boolean function.+ifToBoolOp :: TransformBi (Expr a) (f a) => f a -> f a+ifToBoolOp = transformExprIn $+  \ e0 -> case ifView e0 of+    Just (b,t,f)+      | Just True  <- boolView t -> b \/ f+      | Just False <- boolView t -> neg b /\ f+      | Just True  <- boolView f -> b ==> t -- neg b \/ t+      | Just False <- boolView f -> b /\ t+    _ -> e0+
+ src/Tip/Pass/CSEMatch.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE PatternGuards, RecordWildCards #-}+module Tip.Pass.CSEMatch where++import Tip.Core+import Tip.Fresh++data CSEMatchOpts =+  CSEMatchOpts {+    cse_nullary :: Bool+    -- ^ Also do CSE for nullary constructors+  }++cseMatchNormal, cseMatchWhy3 :: CSEMatchOpts+cseMatchNormal = CSEMatchOpts False+cseMatchWhy3   = CSEMatchOpts True++-- | Look for expressions of the form+--   @(match x (case P ...P...) ...)@+-- and replace them with+--   @(match x (case P ...x...) ...)@.+-- This helps Why3's termination checker in some cases.+cseMatch :: Name a => CSEMatchOpts -> Theory a -> Theory a+cseMatch CSEMatchOpts{..} =+  transformExprIn $ \e ->+    case e of+      Match (Lcl x) pats ->+        Match (Lcl x) (map (replaceWith x) pats)+      _ -> e+  where+    replaceWith x (Case (ConPat con args) body)+      | length args > 0 || cse_nullary =+        Case (ConPat con args) $+        flip transformExpr body $ \e ->+          if e == Gbl con :@: map Lcl args+          then Lcl x+          else e+    replaceWith x case_ = case_
+ src/Tip/Pass/CommuteMatch.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE FlexibleContexts #-}+module Tip.Pass.CommuteMatch where++#include "errors.h"+import Tip.Core+import Tip.Fresh++import Data.Generics.Geniplate+import Control.Applicative++-- | Makes an effort to move match statements upwards: moves match above+-- function applications, and moves matches inside scrutinees outside.+--+-- Does not move past quantifiers, lets, and lambdas.+commuteMatch :: (Name a, TransformBiM Fresh (Expr a) (f a)) => f a -> Fresh (f a)+commuteMatch = transformExprInM $ \ e0 ->+  case e0 of+    Match (Match e inner_alts) outer_alts ->+      commuteMatch =<< do+        Match e <$> sequence+          [ Case lhs <$> freshen (Match rhs outer_alts)+          | Case lhs rhs <- inner_alts+          ]++    hd :@: args+      | and [ not (logicalBuiltin b) | Builtin b <- [hd] ]+      , let isMatch Match{} = True+            isMatch _       = False+      , (left, Match e alts:right) <- break isMatch args+      -> commuteMatch =<< do+           Match e <$> sequence+             [ Case lhs <$> freshen (hd :@: (left ++ [rhs] ++ right))+             | Case lhs rhs <- alts+             ]++    Lam bs e  -> Lam bs <$> commuteMatch e++    Quant qi q bs e -> Quant qi q bs <$> commuteMatch e++    Let x b e -> Let x b <$> commuteMatch e++    _ -> return e0+
+ src/Tip/Pass/EliminateDeadCode.hs view
@@ -0,0 +1,25 @@+-- Very bad dead code elimination (doesn't detect dead recursive functions).++{-# LANGUAGE RecordWildCards #-}+module Tip.Pass.EliminateDeadCode where++import Tip.Core+import qualified Data.Set as Set+import Data.Generics.Geniplate++eliminateDeadCode :: Ord a => Theory a -> Theory a+eliminateDeadCode = fixpoint elim+  where+    elim thy@Theory{..} =+      thy {+        thy_sigs = filter (flip Set.member alive . sig_name) thy_sigs,+        thy_funcs = filter (flip Set.member alive . func_name) thy_funcs }+      where+        alive = Set.fromList (map gbl_name (universeBi thy))++fixpoint :: Eq a => (a -> a) -> a -> a+fixpoint f x+  | x == y = x+  | otherwise = fixpoint f y+  where+    y = f x
+ src/Tip/Pass/EqualFunctions.hs view
@@ -0,0 +1,101 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PatternGuards #-}+module Tip.Pass.EqualFunctions(collapseEqual, removeAliases) where++import Tip.Core+import Tip.Fresh++import Data.Traversable+import Control.Applicative+import Data.Either+import Data.List (delete, inits)++import Data.Map (Map)+import qualified Data.Map as M++import Control.Monad.State++import Data.Generics.Geniplate++renameVars :: forall f a . (Ord a,Traversable f) => (a -> Bool) -> f a -> f (Either a Int)+renameVars is_var t = runFresh (evalStateT (traverse rename t) M.empty)+  where+    rename :: a -> StateT (Map a Int) Fresh (Either a Int)+    rename x | is_var x = do my <- gets (M.lookup x)+                             case my of+                               Just y  -> do return (Right y)+                               Nothing -> do y <- lift fresh+                                             modify (M.insert x y)+                                             return (Right y)+    rename x = return (Left x)++renameFn :: Ord a => Function a -> Function (Either a Int)+renameFn fn = renameVars (`notElem` gbls) fn+  where+    gbls = delete (func_name fn) (globals fn)++rename :: Eq a => [(a,a)] -> a -> a+rename d x = case lookup x d of+    Just y  -> y+    Nothing -> x++-- | If we have+--+-- > f x = E[x]+-- > g y = E[y]+--+-- then we remove @g@ and replace it with @f@ everywhere+collapseEqual :: forall a . Ord a => Theory a -> Theory a+collapseEqual thy@(Theory{ thy_funcs = fns0 })+    = fmap (rename renamings) thy{ thy_funcs = survivors }+  where+    rfs :: [(Function a,Function (Either a Int))]+    rfs = [ (f,renameFn f) | f <- fns0 ]++    renamings :: [(a,a)]+    survivors :: [Function a]+    (renamings,survivors) = partitionEithers+        [ case [ (func_name f,func_name g) | (g,rg) <- prev , rf == rg ] of+            []   -> Right f -- f is better+            fg:_ -> Left fg -- g is better+        | ((f,rf),prev) <- withPrevious rfs+        ]++-- | Pair up a list with its previous elements+--+-- > withPrevious "abc" = [('a',""),('b',"a"),('c',"ab")]+withPrevious :: [a] -> [(a,[a])]+withPrevious xs = zip xs (inits xs)++renameGlobals :: Eq a => [(a,[Type a] -> Head a)] -> Theory a -> Theory a+renameGlobals rns = transformBi $ \ h0 ->+  case h0 of+    Gbl (Global g _ ts) | Just hd <- lookup g rns -> hd ts+    _ -> h0++-- | If we have+--+-- > g x y = f x y+--+-- then we remove @g@ and replace it with @f@ everywhere+removeAliases :: Eq a => Theory a -> Theory a+removeAliases thy@(Theory{thy_funcs=fns0})+    | null renamings = thy+    | otherwise = removeAliases $ renameGlobals renamings thy{ thy_funcs = survivors }+  where+    renamings = take 1+      [ (g,k)+      | Function g ty_vars vars _res_ty (hd :@: args) <- fns0+      , map Lcl vars == args+      , let (ok,k) = case hd of+              Gbl (Global f pty ty_args) -> (map TyVar ty_vars == ty_args, \ ts -> Gbl (Global f pty ts))+              Builtin{}                  -> (True, \ _ -> hd)+      , ok+      ]++    remove = map fst renamings++    survivors = filter ((`notElem` remove) . func_name) fns0+
+ src/Tip/Pass/FillInCases.hs view
@@ -0,0 +1,35 @@+-- Fill in any missing cases with a default value.++{-# LANGUAGE RecordWildCards #-}+module Tip.Pass.FillInCases where++import Tip.Core+import Tip.Scope+import Tip.Utils+import Tip.Fresh+import Tip.Pretty+import Tip.Pretty.SMT+import Debug.Trace+import Text.PrettyPrint++fillInCases :: (Ord a, PrettyVar a) => (Type a -> Expr a) -> Theory a -> Theory a+fillInCases def thy =+  flip transformExprIn thy $ \e ->+    case e of+      Match val cases+        | not (exhaustive (exprType val) (map case_pat cases)) ->+          Match val (Case Default (def (exprType e)):cases)+      _ -> e+  where+    exhaustive _ (Default:_) = True+    exhaustive (TyCon ty _) pats =+      case lookupType ty scp of+        Just (DatatypeInfo Datatype{..}) ->+          usort (map con_name data_cons) ==+          usort [ gbl_name pat_con | ConPat{..} <- pats ]+        _ -> False+    exhaustive (BuiltinType Boolean) pats =+      usort pats == usort [LitPat (Bool False), LitPat (Bool True)]+    exhaustive _ _ = False++    scp = scope thy
+ src/Tip/Pass/Lift.hs view
@@ -0,0 +1,163 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE CPP #-}+module Tip.Pass.Lift (lambdaLift, letLift, axiomatizeLambdas) where++#include "errors.h"+import Tip.Core+import Tip.Fresh+import Tip.Utils++import Data.Either+import Data.List+import Data.Generics.Geniplate+import Control.Applicative+import Control.Monad+import Control.Monad.Writer+import qualified Data.Map as Map++type LiftM a = WriterT [Function a] Fresh++type TopLift a = Expr a -> LiftM a (Expr a)++liftAnywhere :: (Name a,TransformBiM (LiftM a) (Expr a) (t a)) =>+                TopLift a -> t a -> Fresh (t a,[Function a])+liftAnywhere top = runWriterT . transformExprInM top++liftTheory :: Name a => TopLift a -> Theory a -> Fresh (Theory a)+liftTheory top thy0 =+  do (Theory{..},new_func_decls) <- liftAnywhere top thy0+     return Theory{thy_funcs = new_func_decls ++ thy_funcs,..}++lambdaLiftTop :: Name a => TopLift a+lambdaLiftTop e0 =+  case e0 of+    Lam lam_args lam_body ->+      do g_name <- lift (freshNamed "lam")+         let g_args = free e0+         let g_tvs  = freeTyVars e0+         let g_type = map lcl_type lam_args :=>: exprType lam_body+         let g = Function g_name g_tvs g_args g_type (Lam lam_args lam_body)+         tell [g]+         return (applyFunction g (map TyVar g_tvs) (map Lcl g_args))+    _ -> return e0++-- | Defunctionalization.+--+-- > f x = ... \ y -> e [ x ] ...+--+-- becomes+--+-- > f x = ... g x ...+-- > g x = \ y -> e [ x ]+--+-- where @g@ is a fresh function.+--+-- After this pass, lambdas only exist at the top level of functions.+lambdaLift :: Name a => Theory a -> Fresh (Theory a)+lambdaLift = liftTheory lambdaLiftTop++letLiftTop :: Name a => TopLift a+letLiftTop e0 =+  case e0 of+    Let xl@(Local x xt) b e ->+      do let fvs = free b+         let tvs = freeTyVars b+         let xfn = Function x tvs fvs (exprType b) b+         tell [xfn]+         lift ((applyFunction xfn (map TyVar tvs) (map Lcl fvs) // xl) e)+    _ -> return e0++-- | Lift lets to the top level.+--+-- > let x = b[fvs] in e[x]+--+-- becomes+--+-- > e[f fvs]+-- > f fvs = b[fvs]+letLift :: Name a => Theory a -> Fresh (Theory a)+letLift = liftTheory letLiftTop++axLamFunc :: Function a -> Maybe (Signature a,Formula a)+axLamFunc Function{..} =+  case func_body of+    Lam lam_args e ->+      let abs = Signature func_name (PolyType func_tvs (map lcl_type func_args) func_res)+          fm  = Formula Assert func_tvs+                  (mkQuant+                    Forall+                    (func_args ++ lam_args)+                    (apply+                      (applySignature abs (map TyVar func_tvs) (map Lcl func_args))+                      (map Lcl lam_args)+                     === e))+      in  Just (abs,fm)+    _ -> Nothing++-- | Axiomatize lambdas.+--+-- > f x = \ y -> E[x,y]+--+-- becomes+--+-- > declare-fun f ...+-- > assert (forall x y . @ (f x) y = E[x,y])+axiomatizeLambdas :: forall a. Name a => Theory a -> Fresh (Theory a)+axiomatizeLambdas thy0 = do+  arrows <- fmap Map.fromList (mapM makeArrow arities)+  ats    <- fmap Map.fromList (mapM (makeAt arrows) arities)+  return $+    transformBi (eliminateArrows arrows) $+    transformBi (eliminateAts ats)+    thy {+      thy_sigs = Map.elems ats    ++ thy_sigs thy,+      thy_sorts = Map.elems arrows ++ thy_sorts thy+    }+  where+    thy =+      thy0 {+        thy_sigs = new_abs ++ thy_sigs thy0,+        thy_funcs = survivors,+        thy_asserts = new_form ++ thy_asserts thy0+      }+    (survivors,new) =+      partitionEithers+        [ maybe (Left fn) Right (axLamFunc fn)+        | fn <- thy_funcs thy0+        ]++    (new_abs,new_form) = unzip new++    arities = usort [ length args | args :=>: _ <- universeBi thy :: [Type a] ]+    makeArrow n = do+      ty <- freshNamed ("fun" ++ show n)+      return (n, Sort ty (n+1))+    makeAt arrows n = do+      name <- freshNamed ("apply" ++ show n)+      tvs <- mapM (freshNamed . mkTyVarName) [0..(n-1)]+      tv  <- freshNamed (mkTyVarName n)+      let Sort{..} = Map.findWithDefault __ n arrows+          ty          = TyCon sort_name (map TyVar (tvs ++ [tv]))+      return $+        (n, Signature name (PolyType (tvs ++ [tv]) (ty:map TyVar tvs) (TyVar tv)))++    eliminateArrows arrows (args :=>: res) =+      TyCon sort_name (map (eliminateArrows arrows) (args ++ [res]))+      where+        Sort{..} = Map.findWithDefault __ (length args) arrows+    eliminateArrows _ ty = ty++    eliminateAts ats (Builtin At :@: (e:es)) =+      Gbl (Global sig_name sig_type (args ++ [res])) :@:+      map (eliminateAts ats) (e:es)+      where+        args :=>: res = exprType e+        Signature{..} = Map.findWithDefault __ (length args) ats+    eliminateAts _ e = e++mkTyVarName :: Int -> String+mkTyVarName x = vars !! x+  where vars = ["a","b","c","d"] ++ ["t" ++ show i | i <- [0..]]+
+ src/Tip/Pass/NegateConjecture.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE PatternGuards #-}+module Tip.Pass.NegateConjecture where++import Tip.Core+import Tip.Fresh+import Control.Monad+import Data.Generics.Geniplate++-- | Negates the conjecture: changes assert-not into assert, and+--   introduce skolem types in case the goal is polymorphic.+negateConjecture :: Name a => Theory a -> Fresh (Theory a)+negateConjecture thy =+  foldM negateConjecture1+    thy { thy_asserts = filter (not . isProve) (thy_asserts thy) }+    (filter isProve (thy_asserts thy))+  where+    isProve (Formula Prove _ form) = True+    isProve _ = False++    negateConjecture1 thy (Formula Prove tvs form) = do+      tvs' <- mapM (refreshNamed "sk_") tvs+      return thy {+        thy_asserts = Formula Assert [] (neg (makeTyCons (zip tvs tvs') form)):thy_asserts thy,+        thy_sorts = [ Sort tv 0 | tv <- tvs' ] ++ thy_sorts thy }++    makeTyCons tvs =+      transformTypeInExpr $ \ty ->+        case ty of+          TyVar tv | Just tv' <- lookup tv tvs -> TyCon tv' []+          _ -> ty
+ src/Tip/Pass/Pipeline.hs view
@@ -0,0 +1,51 @@+module Tip.Pass.Pipeline where++import Tip.Lint+import Tip.Types (Theory)++import Tip.Utils++import Tip.Fresh+++import Data.List (intercalate)+import Data.Either (partitionEithers)+import Control.Monad ((>=>))+import Options.Applicative++class Pass p where+  runPass   :: Name a => p -> Theory a -> Fresh (Theory a)+  passName  :: p -> String+  parsePass :: Parser p++unitPass :: Pass p => p -> Mod FlagFields () -> Parser p+unitPass p mod = flag' () (long (flagify (passName p)) <> mod) *> pure p++runPassLinted :: (Pass p, Name a) => p -> Theory a -> Fresh (Theory a)+runPassLinted p = runPass p >=> lintM (passName p)++-- | A sum type that supports 'Enum' and 'Bounded'+data Choice a b = First a | Second b+  deriving (Eq,Ord,Show)++-- | 'either' for 'Choice'+choice :: (a -> c) -> (b -> c) -> Choice a b -> c+choice f _ (First x)  = f x+choice _ g (Second y) = g y++instance (Pass a, Pass b) => Pass (Choice a b) where+  passName  = choice passName passName+  runPass   = choice runPass runPass+  parsePass = (First <$> parsePass) <|> (Second <$> parsePass)++runPasses :: (Pass p,Name a) => [p] -> Theory a -> Fresh (Theory a)+runPasses = go []+ where+  go _    [] = return+  go past (p:ps) =+        runPass p+    >=> lintM (passName p ++ "(and " ++ intercalate "," past ++ ")")+    >=> go (passName p:past) ps++parsePasses :: Pass p => Parser [p]+parsePasses = many parsePass
+ src/Tip/Pass/RemoveMatch.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE RecordWildCards, CPP #-}+module Tip.Pass.RemoveMatch where++#include "errors.h"+import Tip.Core+import Tip.Fresh+import Tip.Scope+import qualified Data.Map as Map+import Data.Generics.Geniplate++-- | Turn case expressions into @is-Cons@, @head@, @tail@ etc.+removeMatch :: Name a => Theory a -> Fresh (Theory a)+removeMatch thy@Theory{..} = transformBiM go thy+  where+    scp = scope thy+    go = transformBiM $ \e0 ->+      case e0 of+        Match e cs | all acceptable (map case_pat cs) ->+          letExpr e $ \x ->+            match x (reverse cs) >>= go+        _ -> return e0++    acceptable Default = True+    acceptable ConPat{} = True+    acceptable _ = False++    match x [Case (ConPat c xs) body] = caseBody x (gbl_name c) xs body+    match x [Case Default body] = return body+    match x (Case (ConPat c xs) body:cs) = do+      clause <- caseBody x (gbl_name c) xs body+      rest <- match x cs+      return $+        Match (matches x (gbl_name c))+          [Case Default rest,+           Case (LitPat (Bool True)) clause]++    matches x c =+      Gbl (uncurry discriminator (whichConstructor c scp) args) :@: [Lcl x]+      where+        TyCon _ args = lcl_type x++    caseBody x c lcls body = substMany sub body+      where+        sub = [(lcl, Gbl (uncurry projector (whichConstructor c scp) i args) :@: [Lcl x]) | (i, lcl) <- zip [0..] lcls]+        TyCon _ args = lcl_type x
+ src/Tip/Pass/RemoveNewtype.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE RecordWildCards, PatternGuards, CPP #-}+module Tip.Pass.RemoveNewtype where++#include "errors.h"+import Tip.Core+import Tip.Fresh+import Tip.Scope+import qualified Data.Map as Map+import qualified Data.Set as Set+import Data.Generics.Geniplate+import Data.Maybe++-- | Remove datatypes that have only one constructor with one field.+--   Can only be run after the @addMatch@ pass.+removeNewtype :: Name a => Theory a -> Theory a+removeNewtype thy@Theory{..} =+  -- Replace e.g.:+  -- I# x -> x+  -- (case x of _ -> e) -> e+  -- (case x of (I# y) -> e) -> let y = x in e+  -- Int -> Int#+  transformBi replaceTypes (replaceCons thy')+  where+    replaceTypes (TyCon ty []) =+      case lookupNewtype ty of+        Just ty' -> ty'+        Nothing -> TyCon ty []+    replaceTypes (args :=>: res) =+      map replaceTypes args :=>: replaceTypes res+    replaceTypes ty = ty++    replaceCons =+      transformBi $ \e0 ->+        case e0 of+          Match e cs | TyCon ty [] <- exprType e, isJust (lookupNewtype ty) ->+            case cs of+              Case Default body:_ -> body+              Case (ConPat _ [x]) body:_ -> Let x e body+              _ -> ERROR("type-incorrect pattern?")+          Gbl con :@: [e]+            | Just (dt, _) <- lookupConstructor (gbl_name con) scp+            , isJust (lookupNewtype (data_name dt)) ->+            e+          _ -> e0++    thy' =+      thy {+        thy_datatypes = [ d | d <- thy_datatypes, isNothing (lookupNewtype (data_name d)) ]}+    lookupNewtype ty = do+      Datatype{data_cons = [Constructor{con_args = [(_, ty')]}]} <- lookupDatatype ty scp+      return ty'+    scp = scope thy
+ src/Tip/Pass/Uncurry.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE RecordWildCards #-}+module Tip.Pass.Uncurry(uncurryTheory) where++import Tip.Core+import Tip.Fresh+import Tip.WorkerWrapper++-- | Replace "fat arrow", @=>@, functions with normal functions wherever possible.+uncurryTheory :: Name a => Theory a -> Fresh (Theory a)+uncurryTheory thy =+  workerWrapperFunctions outerUncurryWW thy >>=+  workerWrapperFunctions innerUncurryWW++-- Transform A -> B => C into A B -> C.+outerUncurryWW :: Name a => Function a -> Maybe (Fresh (WorkerWrapper a))+outerUncurryWW func@Function{func_res = args :=>: res, ..} = Just $ do+  lcls <- mapM freshLocal args+  return WorkerWrapper {+    ww_func = func,+    ww_args = func_args ++ lcls,+    ww_res  = res,+    ww_def  = \e -> apply e (map Lcl lcls),+    ww_use  =+      \hd@(Gbl Global{..}) orig_args -> do+        new_args <- mapM (freshLocal . applyType func_tvs gbl_args) args+        return (Lam new_args (hd :@: (orig_args ++ map Lcl new_args)))+  }+outerUncurryWW _ = Nothing++-- Transform A => B => C into A B => C.+innerUncurryWW :: Name a => Function a -> Maybe (Fresh (WorkerWrapper a))+innerUncurryWW _func = Nothing
+ src/Tip/Passes.hs view
@@ -0,0 +1,142 @@+-- | Passes+module Tip.Passes+  (+  -- * Running passes in the Fresh monad+    freshPass++  -- * Simplifications+  , simplifyTheory, gently, aggressively, SimplifyOpts(..)+  , removeNewtype+  , uncurryTheory+  , negateConjecture++  -- * Boolean builtins+  , ifToBoolOp+  , boolOpToIf+  , theoryBoolOpToIf++  -- * Match expressions+  , addMatch+  , commuteMatch+  , removeMatch+  , cseMatch+  , cseMatchNormal+  , cseMatchWhy3+  , fillInCases++  -- * Duplicated functions+  , collapseEqual+  , removeAliases++  -- * Lambda and let lifting+  , lambdaLift+  , letLift+  , axiomatizeLambdas++  -- * Building pass pipelines+  , StandardPass(..)+  , module Tip.Pass.Pipeline+  ) where++import Tip.Simplify++import Tip.Pass.AddMatch+import Tip.Pass.CommuteMatch+import Tip.Pass.RemoveMatch+import Tip.Pass.CSEMatch+import Tip.Pass.Uncurry+import Tip.Pass.RemoveNewtype+import Tip.Pass.NegateConjecture+import Tip.Pass.EqualFunctions+import Tip.Pass.Lift+import Tip.Pass.Booleans+import Tip.Pass.EliminateDeadCode+import Tip.Pass.FillInCases++import Tip.Fresh++import Tip.Pass.Pipeline++import Options.Applicative++-- | The passes in the standard Tip distribution+data StandardPass+  = SimplifyGently+  | SimplifyAggressively+  | RemoveNewtype+  | UncurryTheory+  | NegateConjecture+  | IfToBoolOp+  | BoolOpToIf+  | AddMatch+  | CommuteMatch+  | RemoveMatch+  | CollapseEqual+  | RemoveAliases+  | LambdaLift+  | LetLift+  | AxiomatizeLambdas+  | CSEMatch+  | CSEMatchWhy3+  | EliminateDeadCode+ deriving (Eq,Ord,Show,Read,Enum,Bounded)++instance Pass StandardPass where+  passName = show+  runPass p = case p of+    SimplifyGently       -> simplifyTheory gently+    SimplifyAggressively -> simplifyTheory aggressively+    RemoveNewtype        -> return . removeNewtype+    UncurryTheory        -> uncurryTheory+    NegateConjecture     -> negateConjecture+    IfToBoolOp           -> return . ifToBoolOp+    BoolOpToIf           -> return . theoryBoolOpToIf+    AddMatch             -> addMatch+    CommuteMatch         -> commuteMatch+    RemoveMatch          -> removeMatch+    CollapseEqual        -> return . collapseEqual+    RemoveAliases        -> return . removeAliases+    LambdaLift           -> lambdaLift+    LetLift              -> letLift+    AxiomatizeLambdas    -> axiomatizeLambdas+    CSEMatch             -> return . cseMatch cseMatchNormal+    CSEMatchWhy3         -> return . cseMatch cseMatchWhy3+    EliminateDeadCode    -> return . eliminateDeadCode+  parsePass =+    foldr (<|>) empty [+      unitPass SimplifyGently $+        help "Simplify the problem, trying not to increase its size",+      unitPass SimplifyAggressively $+        help "Simplify the problem even at the cost of making it bigger",+      unitPass RemoveNewtype $+        help "Eliminate single-constructor, single-argument datatypes",+      unitPass UncurryTheory $+        help "Eliminate unnecessary use of higher-order functions",+      unitPass NegateConjecture $+        help "Transform the goal into a negated conjecture",+      unitPass IfToBoolOp $+        help "Replace if-then-else by and/or where appropriate",+      unitPass BoolOpToIf $+        help "Replace and/or by if-then-else",+      unitPass AddMatch $+        help "Transform SMTLIB-style datatype access into pattern matching",+      unitPass CommuteMatch $+        help "Eliminate matches that occur in weird positions (e.g. as arguments to function calls)",+      unitPass RemoveMatch $+        help "Replace pattern matching with SMTLIB-style datatype access",+      unitPass CollapseEqual $+        help "Merge functions with equal definitions",+      unitPass RemoveAliases $+        help "Eliminate any function defined simply as f(x) = g(x)",+      unitPass LambdaLift $+        help "Lift lambdas to the top level",+      unitPass LetLift $+        help "Lift let-expressions to the top level.",+      unitPass AxiomatizeLambdas $+        help "Eliminate lambdas by axiomatisation (requires --lambda-lift)",+      unitPass CSEMatch $+        help "Perform CSE on match scrutinees",+      unitPass CSEMatchWhy3 $+        help "Aggressively perform CSE on match scrutinees (helps Why3's termination checker)",+      unitPass EliminateDeadCode $+        help "Dead code elimination (doesn't work on dead recursive functions)"]
+ src/Tip/Pretty.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE RecordWildCards, OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}+module Tip.Pretty where++import Text.PrettyPrint++import Tip.Types++infixl 1 $\++-- | Typeclass for pretty things+class Pretty a where+  pp :: a -> Doc++-- | Pretty to string+ppRender :: Pretty a => a -> String+ppRender = render . pp++-- | Print something pretty+pprint :: Pretty a => a -> IO ()+pprint = putStrLn . ppRender++instance PrettyVar String where+  varStr = id++instance PrettyVar Int where+  varStr = show++-- | Typeclass for variables+class PrettyVar a where+  -- | The string in a variable+  varStr :: a -> String++-- | Variable to 'Doc'+ppVar :: PrettyVar a => a -> Doc+ppVar = text . varStr++-- * Utilities on Docs++-- | Infix 'hang'+($\) :: Doc -> Doc -> Doc+d1 $\ d2 = hang d1 2 d2+++-- | Conditional parentheses+parIf :: Bool -> Doc -> Doc+parIf True  = parens+parIf False = id+
+ src/Tip/Pretty/Haskell.hs view
@@ -0,0 +1,165 @@+{-# LANGUAGE OverloadedStrings #-}+module Tip.Pretty.Haskell (module Tip.Pretty.Haskell, RenameMap) where++import Tip.Haskell.Repr+import Tip.Haskell.Translate+import Tip.Haskell.Rename+import qualified Tip.Core as T+import Tip.Pretty+import Tip.Fresh+import Text.PrettyPrint++import Data.Map (Map)++ppTheory :: Name a => T.Theory a -> Doc+ppTheory = fst . ppTheoryWithRenamings++ppTheoryWithRenamings :: Name a => T.Theory a -> (Doc,RenameMap a)+ppTheoryWithRenamings = fst_pp . renameDecls . addHeader . addImports . trTheory+  where fst_pp (x,y) = (pp x,y)++-- * Pretty printing++-- | In instance declarations, you cannot write qualified variables,+--   but need to write them unqualified. As an example, the mempty part+--   here is incorrect:+--+-- @+-- instance Data.Monoid.Monoid T where+--   Data.Monoid.mempty = K+-- @+--+-- Thus, instance function declarations will be pretty printed with ppUnqual.+class PrettyVar a => PrettyHsVar a where+  varUnqual :: a -> String++ppUnqual :: PrettyHsVar a => a -> Doc+ppUnqual = text . varUnqual++ppHsVar :: PrettyHsVar a => a -> Doc+ppHsVar x = parIf (isOp x) (ppVar x)++ppOperQ :: PrettyHsVar a => Bool -> a -> [Doc] -> Doc+ppOperQ qual x ds =+  case ds of+    d1:d2:ds | isOp x -> parIf (not (null ds)) (d1 <+> pp_x $\ d2) $\ fsep ds+    _ -> parIf (isOp x) (pp_x $\ fsep ds)+  where+  pp_x | qual = ppVar x+       | otherwise = ppUnqual x++ppOper :: PrettyHsVar a => a -> [Doc] -> Doc+ppOper = ppOperQ True++isOp :: PrettyHsVar a => a -> Bool+isOp = isOperator . varUnqual++instance PrettyVar a => PrettyHsVar (HsId a) where+  varUnqual (Qualified _ _ s) = s+  varUnqual v                 = varStr v++tuple ds = parens (fsep (punctuate "," ds))++csv = sep . punctuate ","++instance PrettyHsVar a => Pretty (Expr a) where+  pp e =+    case e of+      Apply x [] -> ppHsVar x+      Apply x es | Lam ps b <- last es -> ((ppHsVar x $\ fsep (map pp_par (init es))) $\ "(\\" <+> fsep (map (ppPat 1) ps) <+> "->") $\ pp b <> ")"+      Apply x es -> ppOper x (map pp_par es)+      ImpVar x   -> "?" <> ppHsVar x+      Do ss e    -> "do" <+> (vcat (map pp (ss ++ [Stmt e])))+      Let x e b  -> "let" <+> (ppHsVar x <+> "=" $\ pp e) $\ "in" <+> pp b+      ImpLet x e b  -> "let" <+> ("?" <> ppHsVar x <+> "=" $\ pp e) $\ "in" <+> pp b+      Lam ps e   -> "\\" <+> fsep (map pp ps) <+> "->" $\ pp e+      List es    -> brackets (csv (map pp es))+      Tup es     -> tuple (map pp es)+      String s   -> "\"" <> ppUnqual s <> "\""+      Case e brs -> ("case" <+> pp e <+> "of") $\ vcat [ (ppPat 0 p <+> "->") $\ pp rhs | (p,rhs) <- brs ]+      Int i      -> integer i+      Noop       -> "Prelude.return ()"+      QuoteTyCon tc -> "''" <> ppHsVar tc+      QuoteName x   -> "'" <> ppHsVar x+      THSplice e    -> "$" <> parens (pp e)+      Record e upd  -> pp_par e $\ braces (sep (punctuate "," [ ppHsVar f <+> "=" $\ pp rhs | (f,rhs) <- upd ]))+      e ::: t       -> pp_par e <+> "::" $\ pp t+   where+    pp_par e0 =+      case e0 of+        Apply x []  -> pp e0+        List{}      -> pp e0+        Tup{}       -> pp e0+        String{}    -> pp e0+        _           -> parens (pp e0)++instance PrettyHsVar a => Pretty (Stmt a) where+  pp (Bind x e)        = ppHsVar x <+> "<-" $\ pp e+  pp (BindTyped x t e) = (ppHsVar x <+> "::" $\ pp t <+> "<-") $\ pp e+  pp (Stmt e)          = pp e++instance PrettyHsVar a => Pretty (Pat a) where+  pp = ppPat 0++ppPat :: PrettyHsVar a => Int -> Pat a -> Doc+ppPat i p =+  case p of+    VarPat x    -> ppHsVar x+    ConPat k [] -> ppHsVar k+    ConPat k ps -> parIf (i >= 1) (ppOper k (map (ppPat 1) ps))+    TupPat ps   -> tuple (map (ppPat 0) ps)+    WildPat     -> "_"++instance PrettyHsVar a => Pretty (Decl a) where+  pp = go 0+    where+    pp_ctx [] = empty+    pp_ctx ctx = pp (TyTup ctx) <+> "=>"+    go i d =+      case d of+        TySig f ctx t -> (ppHsVar f <+> "::" $\ pp_ctx ctx) $\ pp t+        FunDecl f xs ->+          vcat+            [ (ppOperQ (i == 0) f (map (ppPat 1) ps) <+> "=") $\ pp b+            | (ps,b) <- xs+            ]+        DataDecl tc tvs cons derivs ->+          let dat = case cons of+               [(_,[_])] -> "newtype"+               _         -> "data"+          in ((dat $\ ppOper tc (map ppHsVar tvs) <+> "=") $\+              fsep (punctuate " |" [ ppOper c (map (ppType True 2) ts) | (c,ts) <- cons ])) $\+              (if null derivs then empty+               else "deriving" $\ tuple (map ppHsVar derivs))+        InstDecl ctx head ds ->+          (("instance" $\+            (pp_ctx ctx $\ pp head)) $\+               "where") $\ vcat (map (go 1) ds)+        TypeDef lhs rhs -> "type" <+> ppType False 0 lhs <+> "=" $\ pp rhs+        decl `Where` ds -> go i decl $\ "where" $\ vcat (map (go 1) ds)+        TH e -> pp e+        Module s -> "module" <+> text s <+> "where"+        LANGUAGE s -> "{-#" <+> "LANGUAGE" <+> text s <+> "#-}"+        QualImport m ms -> "import" <+> "qualified" <+> text m $\+                             case ms of+                                Nothing -> empty+                                Just s  -> "as" <+> text s++instance PrettyHsVar a => Pretty (Decls a) where+  pp (Decls ds) = vcat (map pp ds)++instance PrettyHsVar a => Pretty (Type a) where+  pp = ppType True 0++ppType :: PrettyHsVar a => Bool -> Int -> Type a -> Doc+ppType qual i t0 =+  case t0 of+    TyCon t []  -> ppHsVar t+    TyCon t ts  -> parIf (i >= 2) (ppOperQ qual t (map (ppType True 2) ts))+    TyVar x     -> ppHsVar x+    TyTup ts    -> tuple (map (ppType True 0) ts)+    TyArr t1 t2 -> parIf (i >= 1) (ppType True 1 t1 <+> "->" $\ ppType True 0 t2)+    TyCtx ctx t -> parIf (i >= 1) (pp (TyTup ctx) <+> "=>" $\ ppType qual 0 t)+    TyForall tvs t  -> parIf (i >= 1) ("forall" <+> fsep (map ppVar tvs) <+> "." $\ ppType qual 0 t)+    TyImp x t       -> parIf (i >= 1) ("?" <> ppVar x <+> "::" $\ ppType qual 0 t)+
+ src/Tip/Pretty/Isabelle.hs view
@@ -0,0 +1,286 @@+{-# LANGUAGE RecordWildCards, OverloadedStrings, PatternGuards, ScopedTypeVariables, ViewPatterns #-}+module Tip.Pretty.Isabelle where++import Text.PrettyPrint++import Tip.Pretty+import Tip.Types+import Tip.Utils.Rename (renameWith,disambig)+import Tip.Rename+import Tip.Core (ifView, DeepPattern(..), patternMatchingView, topsort, makeGlobal, exprType)++import Data.Char+import Data.Maybe+import Data.List (intersperse, partition)++import Data.Generics.Geniplate++import qualified Data.Set as S+++($-$), block :: Doc -> Doc -> Doc+d $-$ b = vcat [d,"",b]++block d c = (d $\ c)++pcsv, csv, csv1 :: [Doc] -> Doc+csv = fsep . punctuate ","++csv1 [x] = x+csv1 xs  = pcsv xs++pcsv = parens . csv++separating :: ([Doc] -> Doc) -> [Doc] -> [Doc] -> Doc+separating comb seps docs = comb (go seps docs)+  where+    go (s:ss) (d:ds) = s <+> d : go ss ds+    go _      []     = []+    go []     _      = error "separating: ran out of separators!"++escape :: Char -> String+escape x | isAlphaNum x = [x]+escape _                = []++intersperseWithPre :: (a -> a -> a) -> a -> [a] -> [a]+intersperseWithPre f  s (t1:t2:ts) = t1:map (f s) (t2:ts)+intersperseWithPre _f _s ts        = ts++quote :: Doc -> Doc+quote d = "\""<> d <> "\""++quoteWhen :: (a -> Bool) -> a -> (Doc -> Doc)+quoteWhen p t | p t       = quote+              | otherwise = id++ppAsTuple :: [a] -> (a -> Doc) -> Doc+ppAsTuple ts toDoc = parIf (length ts > 1) ((sep.punctuate ",") (map toDoc ts))++ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc+ppTheory (renameAvoiding isabelleKeywords escape -> Theory{..})+  = vcat ["theory" <+> "A",+          --"imports $HIPSTER_HOME/IsaHipster",+          "imports Main",+          --"        \"../../IsaHipster\"",  -- convenience+          "begin"] $$+    foldl ($-$) empty (+      map ppSort thy_sorts +++      map ppDatas (topsort thy_datatypes) +++      map ppUninterp thy_sigs +++      map ppFuncs (topsort thy_funcs) +++      -- ["(*hipster" <+> sep (map (ppVar.func_name) thy_funcs) <+> "*)"] ++   -- convenience+      zipWith ppFormula thy_asserts [0..])+    $-$+    "end"++ppSort :: (PrettyVar a, Ord a) => Sort a -> Doc+--ppSort (Sort sort 0) = "type" $\ ppVar sort+ppSort (Sort sort n) =+  error $ "Can't translate abstract sort " ++ show (ppVar sort) ++ " of arity " ++ show n ++ " to Isabelle"++ppDatas :: (PrettyVar a, Ord a) => [Datatype a] -> Doc+ppDatas []  = empty+ppDatas dts = "datatype" <+>+    vcat (intersperseWithPre ($\) "and" (map ppData dts))++ppData :: (PrettyVar a, Ord a) => Datatype a -> Doc+ppData (Datatype tc tvs cons) =+  ppAsTuple tvs ppTyVar $\+    ppVar tc $\ separating fsep ("=":repeat "|") (map ppCon cons)+--ppDatas (d:ds) = ppData "datatype" d+        -- FIXME: No mutual recusion for now...+        --vcat (ppData "type" d:map (ppData "with") ds)++ppCon :: (PrettyVar a, Ord a) => Constructor a -> Doc+ppCon (Constructor c _d as) = ppVar c <+> fsep (map (quote . ppType 0 . snd) as)++ppQuant :: (PrettyVar a, Ord a) => Doc -> [Local a] -> Doc -> Doc -> Doc+ppQuant _name [] _to d = d+ppQuant name  ls to  d = (name $\ fsep (map (parens . ppLocalBinder) ls) <+> to) $\ d++ppBinder :: (PrettyVar a, Ord a) => a -> Type a -> Doc+ppBinder x t = ppVar x <+> "::" $\ ppType 0 t++ppLocalBinder :: (PrettyVar a, Ord a) => Local a -> Doc+ppLocalBinder (Local x t) = ppBinder x t++ppUninterp :: (PrettyVar a, Ord a) => Signature a -> Doc+ppUninterp (Signature f (PolyType _ arg_types result_type)) =+  --"function" $\ ppVar f $\ fsep (map (ppType 1) arg_types) $\ (":" <+> ppType 1 result_type)+  -- XXX: consts maybe?+  error $ "Can't translate uninterpreted function " ++ varStr f++ppFuncs :: (PrettyVar a, Ord a) => [Function a] -> Doc+ppFuncs []       = empty+ppFuncs (fn:fns) = header <+>+    vcat (intersperseWithPre ($\) "and" fTys) <+> "where" $$+    vcat (intersperseWithPre ($\) "|" fDefs) $$+    termination+  where (header,termination) | null fns  = ("fun",empty)+                             | otherwise = ("function","by pat_completeness auto")+        (fTys, fDefs) = foldr (\(ppFunc -> (pf,pds)) (ftys,fdefs) ->+                                  (pf:ftys, pds++fdefs))+                        ([],[]) (fn:fns)++ppFunc :: (PrettyVar a, Ord a) => Function a -> (Doc,[Doc])+ppFunc (Function f _tvs xts t e) =+     (ppVar f <+> "::" <+> quote (ppType (-1) (map lcl_type xts :=>: t)),+      [ quote $ ppVar f $\ fsep (map ppDeepPattern dps) <+> "=" $\ ppExpr 0 rhs+                  | (dps,rhs) <- patternMatchingView xts e ])++   -- (header $\ ppVar f $\ fsep (map (parens . ppLocalBinder) xts) $\ (":" <+> ppType 0 t <+> "="))+   --  $\ ppExpr 0 e++ppDeepPattern :: PrettyVar a => DeepPattern a -> Doc+ppDeepPattern (DeepConPat (Global k _ _) dps) = parens (ppVar k <+> fsep (map ppDeepPattern dps))+ppDeepPattern (DeepVarPat (Local x _)) = ppVar x+ppDeepPattern (DeepLitPat lit) = ppLit lit+++ppFormula :: (PrettyVar a, Ord a) => Formula a -> Int -> Doc+ppFormula (Formula role _tvs term) i =+  (ppRole role <+> ("x" <> int i) <+> ":") $\ quote (ppExpr 0 term) $$ "oops"+  -- "by (tactic {* Subgoal.FOCUS_PARAMS (K (Tactic_Data.hard_tac @{context})) @{context} 1 *})" convenience++ppRole :: Role -> Doc+ppRole Assert = "lemma" --Better with lemma and sorry-proof here. Then need to insert 'sorry' on the line below somehow.+ppRole Prove  = "theorem"++ppExpr :: (PrettyVar a, Ord a) => Int -> Expr a -> Doc+ppExpr i e | Just (c,t,f) <- ifView e = parens $ "if" $\ ppExpr 0 c $\ "then" $\ ppExpr 0 t $\ "else" $\ ppExpr 0 f+ppExpr i e@(hd@(Gbl Global{..}) :@: es)+  | isNothing (makeGlobal gbl_name gbl_type (map exprType es) Nothing) =+    parIf (i > 0) $+    ppHead hd (map (ppExpr 1) es)-- $\ "::" $\ ppType 0 (exprType e)+ppExpr i (hd :@: es)  = parIf ((i > 0 && not (null es)) || isLogB hd) $+                          ppHead hd (map (ppExpr 1) es)+  where isLogB (Builtin b) = logicalBuiltin b+        isLogB _           = False+ppExpr _ (Lcl l)      = ppVar (lcl_name l)+ppExpr i (Lam ls e)   = parIf (i > 0) $ ppQuant "%" ls "=>" (ppExpr 0 e)+ppExpr i (Let x b e)  = parIf (i > 0) $ sep ["let" $\ ppLocalBinder x <+> "=" $\ ppExpr 0 b, "in" <+> ppExpr 0 e]+ppExpr i (Quant _ q ls e) = parIf (i > 0) $ ppQuant (ppQuantName q) ls "." (ppExpr 0 e)+ppExpr i (Match e alts) =+  parIf (i <= 0) $ block ("case" $\ ppExpr 0 e $\ "of")+                         (vcat (intersperseWithPre ($\) "|" (map ppCase+                                  (uncurry (++) (partition ((/= Default).case_pat) alts)))))++ppHead :: (PrettyVar a, Ord a) => Head a -> [Doc] -> Doc+ppHead (Gbl gbl)      args                        = ppVar (gbl_name gbl) $\ fsep args+ppHead (Builtin b)    [u,v] | Just d <- ppBinOp b = u <+> d $\ v+ppHead (Builtin At{}) args                        = fsep args+ppHead (Builtin b)    args                        = ppBuiltin b $\ fsep args++ppBuiltin :: Builtin -> Doc+ppBuiltin (Lit lit) = ppLit lit+ppBuiltin IntDiv    = "(op div)"+ppBuiltin IntMod    = "mod"+ppBuiltin Not       = "~"+ppBuiltin b         = error $ "Isabelle.ppBuiltin: " ++ show b++ppBinOp :: Builtin -> Maybe Doc+ppBinOp And       = Just "&"+ppBinOp Or        = Just "|"+ppBinOp Implies   = Just "==>"+ppBinOp Equal     = Just "="+ppBinOp Distinct  = Just "~="+ppBinOp IntAdd    = Just "+"+ppBinOp IntSub    = Just "-"+ppBinOp IntMul    = Just "*"+ppBinOp IntGt     = Just ">"+ppBinOp IntGe     = Just ">="+ppBinOp IntLt     = Just "<"+ppBinOp IntLe     = Just "<="+ppBinOp _         = Nothing++ppLit :: Lit -> Doc+ppLit (Int i)      = integer i+ppLit (Bool True)  = "True"+ppLit (Bool False) = "False"+ppLit (String s)   = text (show s)++ppQuantName :: Quant -> Doc+ppQuantName Forall = "!!"+ppQuantName Exists = "??"++ppCase :: (PrettyVar a, Ord a) => Case a -> Doc+ppCase (Case pat rhs) = ppPat pat <+> "=>" $\ ppExpr 0 rhs++ppPat :: (PrettyVar a, Ord a) => Pattern a -> Doc+ppPat pat = case pat of+  Default     -> "other"+  ConPat g ls -> ppVar (gbl_name g) $\ fsep (map (ppVar . lcl_name) ls)+  LitPat l    -> ppLit l++ppType :: (PrettyVar a, Ord a) => Int -> Type a -> Doc+ppType _ (TyVar x)     = ppTyVar x+ppType i (TyCon tc ts) = parIf (i > 0 && (not . null) ts) $+                           ppAsTuple ts (ppType 2 {-1-}) $\ ppVar tc+ppType i (ts :=>: r)   = parIf (i >= 0) $ fsep (punctuate " =>" (map (ppType 0) (ts ++ [r])))+ppType _ (BuiltinType Integer) = "int"+ppType _ (BuiltinType Boolean) = "bool"++ppTyVar :: (PrettyVar a, Ord a) => a -> Doc+ppTyVar x = "'" <> ppVar x++-- FIXME: THESE are just copied from the Why3-file+isabelleKeywords :: [String]+isabelleKeywords = (words . unlines)+    [ "equal not use import goal int"+    , "and or"+    , "forall exists"+    , "module theory"+    , "ac"+    , "and"+    , "axiom"+    , "inversion"+    , "bitv"+    , "check"+    , "cut"+    , "distinct"+    , "else"+    , "exists"+    , "false"+    , "forall"+    , "function"+    , "goal"+    , "if"+    , "in"+    , "include"+    , "int"+    , "let"+    , "logic"+    , "not"+    , "or"+    , "predicate"+    , "prop"+    , "real"+    , "rewriting"+    , "then"+    , "true"+    , "type"+    , "unit"+    , "void"+    , "with"+    , "sign Nil Cons"+    , "div"+    , "mod"+    ] +++    [ "theorem lemma declare axiomatization"+    , "prefer def thm term typ"+    , "fun primrec definition value where infixl infixr abbreviation notation for"+    , "datatype type_synonym option consts typedecl inductive_set inductive_cases"+    , "True False None Some abs"+    , "class instantiation fixes instance assumes shows proof fix show have obtain"+    , "unfolding qed from"+    , "begin end imports ML using"+    , "apply done oops sorry by back"+    , "text header chapter section subsection subsubsection sect subsect subsubsect"+    , "nil cons Nil Cons"+    , "nil"+    , "cons"+    , "Nil"+    , "Cons"+    , "EX ALL"+    ]+
+ src/Tip/Pretty/SMT.hs view
@@ -0,0 +1,252 @@+{-# LANGUAGE RecordWildCards, OverloadedStrings, PatternGuards, ViewPatterns #-}+module Tip.Pretty.SMT where++import Text.PrettyPrint++import Tip.Pretty+import Tip.Types+import Tip.Core (ifView, topsort, neg, exprType, makeGlobal)+import Tip.Rename+import Data.Maybe+import Data.Char (isAlphaNum)++expr,parExpr,parExprSep :: Doc -> [Doc] -> Doc+parExpr s [] = parens s+parExpr s xs = ("(" <> s) $\ (fsep xs <> ")")++parExprSep s [x]    = ("(" <> s) $\ (x <> ")")+parExprSep s (x:xs) = (("(" <> s) $\ x) $\ (fsep xs <> ")")+parExprSep s xs     = parExpr s xs++expr s [] = s+expr s xs = parExpr s xs++exprSep s [] = s+exprSep s xs = parExprSep s xs++apply :: Doc -> Doc -> Doc+apply s x = parExpr s [x]++validSMTChar :: Char -> String+validSMTChar x+  | isAlphaNum x                             = [x]+  | x `elem` ("~!@$%^&*_-+=<>.?/" :: String) = [x]+  | otherwise                                = ""++ppTheory :: (Ord a,PrettyVar a) => Theory a -> Doc+ppTheory (renameAvoiding smtKeywords validSMTChar -> Theory{..})+  = vcat+     (map ppSort thy_sorts +++      map ppDatas (topsort thy_datatypes) +++      map ppUninterp thy_sigs +++      map ppFuncs (topsort thy_funcs) +++      map ppFormula thy_asserts +++      ["(check-sat)"])++ppSort :: PrettyVar a => Sort a -> Doc+ppSort (Sort sort n) = parExpr "declare-sort" [ppVar sort, int n]++ppDatas :: PrettyVar a => [Datatype a] -> Doc+ppDatas datatypes@(Datatype _ tyvars _:_) =+  parExprSep "declare-datatypes" [parens (fsep (map ppVar tyvars)), parens (fsep (map ppData datatypes))]++ppData :: PrettyVar a => Datatype a -> Doc+ppData (Datatype tycon _ datacons) =+  parExprSep (ppVar tycon) (map ppCon datacons)++ppCon :: PrettyVar a => Constructor a -> Doc+ppCon (Constructor datacon selector args) =+  parExprSep (ppVar datacon) [apply (ppVar p) (ppType t) | (p,t) <- args]+++par :: (PrettyVar a) => [a] -> Doc -> Doc+par [] d = d+par xs d = parExprSep "par" [parens (fsep (map ppVar xs)), parens d]++par' :: (PrettyVar a) => [a] -> Doc -> Doc+par' [] d = d+par' xs d = parExprSep "par" [parens (fsep (map ppVar xs)), d]++ppUninterp :: PrettyVar a => Signature a -> Doc+ppUninterp (Signature f (PolyType tyvars arg_types result_type)) =+  apply "declare-fun"+    (par' tyvars+      (apply (ppVar f)+        (sep [parens (fsep (map ppType arg_types)), ppType result_type])))++ppFuncs :: (Ord a, PrettyVar a) => [Function a] -> Doc+ppFuncs fs = expr "define-funs-rec"+  [ parens (vcat (map ppFuncSig fs))+  , parens (vcat (map (ppExpr . func_body) fs))+  ]++ppFuncSig :: PrettyVar a => Function a -> Doc+ppFuncSig (Function f tyvars args res_ty body) =+  (par' tyvars+    (parens+      (ppVar f $\ fsep [ppLocals args, ppType res_ty])))++ppFormula :: (Ord a, PrettyVar a) => Formula a -> Doc+ppFormula (Formula Prove tvs term)  = apply "assert-not" (par' tvs (ppExpr term))+ppFormula (Formula Assert tvs term) = apply "assert"     (par' tvs (ppExpr term))++ppExpr :: (Ord a, PrettyVar a) => Expr a -> Doc+ppExpr e | Just (c,t,f) <- ifView e = parExpr "ite" (map ppExpr [c,t,f])+ppExpr e@(hd@(Gbl Global{..}) :@: es)+  | isNothing (makeGlobal gbl_name gbl_type (map exprType es) Nothing)+      = exprSep "as" [exprSep (ppHead hd) (map ppExpr es), ppType (exprType e)]+ppExpr (hd :@: es)  = exprSep (ppHead hd) (map ppExpr es)+ppExpr (Lcl l)      = ppVar (lcl_name l)+ppExpr (Lam ls e)   = parExprSep "lambda" [ppLocals ls,ppExpr e]+ppExpr (Match e as) = "(match" $\ ppExpr e $\ (vcat (map ppCase as) <> ")")+ppExpr (Let x b e)  = parExprSep "let" [parens (parens (ppLocal x $\ ppExpr b)), ppExpr e]+ppExpr (Quant _ q ls e) = parExprSep (ppQuant q) [ppLocals ls, ppExpr e]++ppLocals :: PrettyVar a => [Local a] -> Doc+ppLocals ls = parens (fsep (map ppLocal ls))++ppLocal :: PrettyVar a => Local a -> Doc+ppLocal (Local l t) = expr (ppVar l) [ppType t]++ppHead :: PrettyVar a => Head a -> Doc+ppHead (Builtin b) = ppBuiltin b+ppHead (Gbl gbl)   = ppVar (gbl_name gbl) {- -- $$ ";" <> ppPolyType (gbl_type gbl)+                                             -- $$ ";" <> fsep (map ppType (gbl_args gbl))+                                             -- $$ text ""+                                          -}++ppBuiltin :: Builtin -> Doc+ppBuiltin (Lit lit) = ppLit lit+ppBuiltin Not       = "not"+ppBuiltin And       = "and"+ppBuiltin Or        = "or"+ppBuiltin Implies   = "=>"+ppBuiltin Equal     = "="+ppBuiltin Distinct  = "distinct"+ppBuiltin IntAdd    = "+"+ppBuiltin IntSub    = "-"+ppBuiltin IntMul    = "*"+ppBuiltin IntDiv    = "div"+ppBuiltin IntMod    = "mod"+ppBuiltin IntGt     = ">"+ppBuiltin IntGe     = ">="+ppBuiltin IntLt     = "<"+ppBuiltin IntLe     = "<="+ppBuiltin At{}      = "@"++ppLit :: Lit -> Doc+ppLit (Int i)      = integer i+ppLit (Bool True)  = "true"+ppLit (Bool False) = "false"+ppLit (String s)   = text (show s)++ppQuant :: Quant -> Doc+ppQuant Forall = "forall"+ppQuant Exists = "exists"++ppCase :: (Ord a, PrettyVar a) => Case a -> Doc+ppCase (Case pat rhs) = parExprSep "case" [ppPat pat,ppExpr rhs]++ppPat :: PrettyVar a => Pattern a -> Doc+ppPat Default         = "default"+ppPat (ConPat g args) = expr (ppVar (gbl_name g)) [ppVar (lcl_name arg) | arg <- args]+ppPat (LitPat lit)    = ppLit lit++ppType :: PrettyVar a => Type a -> Doc+ppType (TyVar x)     = ppVar x+ppType (TyCon tc ts) = expr (ppVar tc) (map ppType ts)+ppType (ts :=>: r)   = parExpr "=>" (map ppType (ts ++ [r]))+ppType (BuiltinType Integer) = "Int"+ppType (BuiltinType Boolean) = "Bool"++-- Temporary use SMTLIB as the pretty printer:++instance (Ord a,PrettyVar a) => Pretty (Theory a) where+  pp = ppTheory++instance (Ord a, PrettyVar a) => Pretty (Expr a) where+  pp = ppExpr++ppPolyType :: PrettyVar a => PolyType a -> Doc+ppPolyType (PolyType tyvars arg_types result_type) =+  par tyvars+    (parens+      (sep [parens (fsep (map ppType arg_types)), ppType result_type]))++instance PrettyVar a => Pretty (PolyType a) where+  pp = ppPolyType++instance PrettyVar a => Pretty (Type a) where+  pp = ppType++instance (Ord a, PrettyVar a) => Pretty (Function a) where+  pp = ppFuncs . return++instance (Ord a, PrettyVar a) => Pretty (Formula a) where+  pp = ppFormula++instance PrettyVar a => Pretty (Datatype a) where+  pp = ppDatas . return++instance PrettyVar a => Pretty (Signature a) where+  pp = ppUninterp++instance PrettyVar a => Pretty (Local a) where+  pp = ppLocal++instance PrettyVar a => Pretty (Global a) where+  pp = ppHead . Gbl++instance PrettyVar a => Pretty (Head a) where+  pp = ppHead++instance PrettyVar a => Pretty (Pattern a) where+  pp = ppPat++smtKeywords :: [String]+smtKeywords =+    [ "ac"+    , "and"+    , "axiom"+    , "inversion"+    , "bitv"+    , "bool"+    , "check"+    , "cut"+    , "distinct"+    , "else"+    , "exists"+    , "false"+    , "forall"+    , "function"+    , "goal"+    , "if"+    , "in"+    , "include"+    , "int"+    , "let"+    , "logic"+    , "not"+    , "or"+    , "predicate"+    , "prop"+    , "real"+    , "rewriting"+    , "then"+    , "true"+    , "type"+    , "unit"+    , "void"+    , "with"+    , "assert", "check-sat"+    , "abs", "min", "max", "const"+    , "mod", "div"+    , "=", "=>", "+", "-", "*", ">", ">=", "<", "<=", "@", "!"+    -- Z3:+    , "Bool", "Int", "Array", "List", "insert"+    , "isZero"+    , "map"+    -- CVC4:+    , "as", "concat"+    ]+
+ src/Tip/Pretty/Why3.hs view
@@ -0,0 +1,241 @@+{-# LANGUAGE RecordWildCards, OverloadedStrings, PatternGuards, ScopedTypeVariables, ViewPatterns #-}+module Tip.Pretty.Why3 where++import Text.PrettyPrint++import Tip.Pretty+import Tip.Types+import Tip.Utils.Rename (renameWith,disambig)+import Tip.Rename+import Tip.Core (ifView, DeepPattern(..), patternMatchingView, topsort, makeGlobal, exprType)++import Data.Char+import Data.Maybe++import Data.Generics.Geniplate++import qualified Data.Set as S++data Why3Var a = Why3Var Bool {- is constructor -} a+  deriving (Eq,Ord,Show)++instance PrettyVar a => PrettyVar (Why3Var a) where+  varStr (Why3Var b x) = (if b then toUpper else toLower) `mapHead` addAlpha (varStr x)+   where+    mapHead :: (Char -> Char) -> String -> String+    f `mapHead` []     = [f 'x']+    f `mapHead` (x:xs) = f x:xs++    addAlpha :: String -> String+    addAlpha s@(x:_) | isAlpha x = s+    addAlpha s                   = "x" ++ s++why3VarTheory :: forall a . Ord a => Theory a -> Theory (Why3Var a)+why3VarTheory thy = fmap mk thy+ where+  cons = S.fromList [ c | Constructor c _ _ <- universeBi thy ]+  mk x = Why3Var (x `S.member` cons) x++block :: Doc -> Doc -> Doc+block d c = (d $\ c) $$ "end"++pcsv, csv, csv1 :: [Doc] -> Doc+csv = fsep . punctuate ","++csv1 [x] = x+csv1 xs  = pcsv xs++pcsv = parens . csv++separating :: ([Doc] -> Doc) -> [Doc] -> [Doc] -> Doc+separating comb seps docs = comb (go seps docs)+  where+    go (s:ss) (d:ds) = s <+> d : go ss ds+    go _      []     = []+    go []     _      = error "separating: ran out of separators!"++escape :: Char -> String+escape x | isAlphaNum x = [x]+escape _                = []++ppTheory :: (Ord a,PrettyVar a) => Theory a -> Doc+ppTheory (renameAvoiding why3Keywords escape . why3VarTheory -> Theory{..})+  = block ("module" <+> "A") $+    vcat (+      "use HighOrd" :+      "use import int.Int" :+      "use import int.EuclideanDivision" :+      map ppSort thy_sorts +++      map ppDatas (topsort thy_datatypes) +++      map ppUninterp thy_sigs +++      map ppFuncs (topsort thy_funcs) +++      zipWith ppFormula thy_asserts [0..])++ppSort :: (PrettyVar a, Ord a) => Sort a -> Doc+ppSort (Sort sort 0) = "type" $\ ppVar sort+ppSort (Sort sort n) =+  error $ "Can't translate abstract sort " ++ show (ppVar sort) ++ " of arity " ++ show n ++ " to Why3"++ppDatas :: (PrettyVar a, Ord a) => [Datatype a] -> Doc+ppDatas (d:ds) = vcat (ppData "type" d:map (ppData "with") ds)++ppData :: (PrettyVar a, Ord a) => Doc -> Datatype a -> Doc+ppData header (Datatype tc tvs cons) =+  header $\ (ppVar tc $\ sep (map ppTyVar tvs) $\+    separating fsep ("=":repeat "|") (map ppCon cons))++ppCon :: (PrettyVar a, Ord a) => Constructor a -> Doc+ppCon (Constructor c _d as) = ppVar c <+> fsep (map (ppType 1 . snd) as)++ppQuant :: (PrettyVar a, Ord a) => Doc -> [Local a] -> Doc -> Doc+ppQuant _name [] d = d+ppQuant name  ls d = (name $\ fsep (punctuate "," (map ppLocalBinder ls)) <+> ".") $\ d++ppBinder :: (PrettyVar a, Ord a) => a -> Type a -> Doc+ppBinder x t = ppVar x <+> ":" $\ ppType 0 t++ppLocalBinder :: (PrettyVar a, Ord a) => Local a -> Doc+ppLocalBinder (Local x t) = ppBinder x t++ppUninterp :: (PrettyVar a, Ord a) => Signature a -> Doc+ppUninterp (Signature f (PolyType _ arg_types result_type)) =+  "function" $\ ppVar f $\ fsep (map (ppType 1) arg_types) $\ (":" <+> ppType 1 result_type)++ppFuncs :: (PrettyVar a, Ord a) => [Function a] -> Doc+ppFuncs (fn:fns) = vcat (ppFunc "function" fn:map (ppFunc "with") fns)++ppFunc :: (PrettyVar a, Ord a) => Doc -> Function a -> Doc+ppFunc header (Function f _tvs xts t e) =+   ((header $\ ppVar f $\ fsep (map (parens . ppLocalBinder) xts) $\ (":" <+> ppType 0 t <+> "="))+     $\ ppExpr 0 e+   ) $$+   ("(*" <+> vcat [ ppVar f $\ fsep (map ppDeepPattern dps) <+> "=" $\ ppExpr 0 rhs+                  | (dps,rhs) <- patternMatchingView xts e ] <+> "*)")++ppDeepPattern :: PrettyVar a => DeepPattern a -> Doc+ppDeepPattern (DeepConPat (Global k _ _) dps) = parens (ppVar k <+> fsep (map ppDeepPattern dps))+ppDeepPattern (DeepVarPat (Local x _)) = ppVar x+ppDeepPattern (DeepLitPat lit) = ppLit lit++ppFormula :: (PrettyVar a, Ord a) => Formula a -> Int -> Doc+ppFormula (Formula role _tvs term) i =+  (ppRole role <+> ("x" <> int i) <+> ":") $\ (ppExpr 0 term)++ppRole :: Role -> Doc+ppRole Assert = "lemma"+ppRole Prove  = "goal"++ppExpr :: (PrettyVar a, Ord a) => Int -> Expr a -> Doc+ppExpr i e | Just (c,t,f) <- ifView e = parIf (i > 0) $ "if" $\ ppExpr 0 c $\ "then" $\ ppExpr 0 t $\ "else" $\ ppExpr 0 f+ppExpr i e@(hd@(Gbl Global{..}) :@: es)+  | isNothing (makeGlobal gbl_name gbl_type (map exprType es) Nothing) =+    parIf (i > 0) $+    ppHead hd (map (ppExpr 1) es) $\ ":" $\ ppType 0 (exprType e)+ppExpr i (hd :@: es)  = parIf (i > 0 && not (null es)) $ ppHead hd (map (ppExpr 1) es)+ppExpr _ (Lcl l)      = ppVar (lcl_name l)+ppExpr i (Lam ls e)   = parIf (i > 0) $ ppQuant "\\" ls (ppExpr 0 e)+ppExpr i (Let x b e)  = parIf (i > 0) $ sep ["let" $\ ppVar (lcl_name x) <+> "=" $\ ppExpr 0 b <+> ":" $\ ppType 0 (lcl_type x), "in" <+> ppExpr 0 e]+ppExpr i (Quant _ q ls e) = parIf (i > 0) $ ppQuant (ppQuantName q) ls (ppExpr 0 e)+ppExpr i (Match e alts) =+  parIf (i > 0) $ block ("match" $\ ppExpr 0 e $\ "with")+                        (separating vcat (repeat "|") (map ppCase alts))++ppHead :: (PrettyVar a, Ord a) => Head a -> [Doc] -> Doc+ppHead (Gbl gbl)   args = ppVar (gbl_name gbl) $\ fsep args+ppHead (Builtin b) [u,v] | Just d <- ppBinOp b = u <+> d $\ v+ppHead (Builtin At{}) args = fsep args+ppHead (Builtin b) args = ppBuiltin b $\ fsep args++ppBuiltin :: Builtin -> Doc+ppBuiltin (Lit lit) = ppLit lit+ppBuiltin IntDiv    = "div"+ppBuiltin IntMod    = "mod"+ppBuiltin Not       = "not"+ppBuiltin b         = error $ "Why3.ppBuiltin: " ++ show b++ppBinOp :: Builtin -> Maybe Doc+ppBinOp And       = Just "&&"+ppBinOp Or        = Just "||"+ppBinOp Implies   = Just "->"+ppBinOp Equal     = Just "="+ppBinOp Distinct  = Just "<>"+ppBinOp IntAdd    = Just "+"+ppBinOp IntSub    = Just "-"+ppBinOp IntMul    = Just "*"+ppBinOp IntGt     = Just ">"+ppBinOp IntGe     = Just ">="+ppBinOp IntLt     = Just "<"+ppBinOp IntLe     = Just "<="+ppBinOp _         = Nothing++ppLit :: Lit -> Doc+ppLit (Int i)      = integer i+ppLit (Bool True)  = "true"+ppLit (Bool False) = "false"+ppLit (String s)   = text (show s)++ppQuantName :: Quant -> Doc+ppQuantName Forall = "forall"+ppQuantName Exists = "exists"++ppCase :: (PrettyVar a, Ord a) => Case a -> Doc+ppCase (Case pat rhs) = ppPat pat <+> "->" $\ ppExpr 0 rhs++ppPat :: (PrettyVar a, Ord a) => Pattern a -> Doc+ppPat pat = case pat of+  Default     -> "_"+  ConPat g ls -> ppVar (gbl_name g) $\ fsep (map (ppVar . lcl_name) ls)+  LitPat l    -> ppLit l++ppType :: (PrettyVar a, Ord a) => Int -> Type a -> Doc+ppType _ (TyVar x)     = ppTyVar x+ppType i (TyCon tc ts) = parIf (i > 0) $ ppVar tc $\ fsep (map (ppType 1) ts)+ppType i (ts :=>: r)   = parIf (i > 0) $ fsep (punctuate " ->" (map (ppType 1) (ts ++ [r])))+ppType _ (BuiltinType Integer) = "int"+ppType _ (BuiltinType Boolean) = "bool"++ppTyVar :: (PrettyVar a, Ord a) => a -> Doc+ppTyVar x = "'" <> ppVar x++why3Keywords :: [String]+why3Keywords = words $ unlines+    [ "equal not function use import goal int"+    , "and or"+    , "forall exists"+    , "module theory"+    , "ac"+    , "and"+    , "axiom"+    , "inversion"+    , "bitv"+    , "check"+    , "cut"+    , "distinct"+    , "else"+    , "exists"+    , "false"+    , "forall"+    , "function"+    , "goal"+    , "if"+    , "in"+    , "include"+    , "int"+    , "let"+    , "logic"+    , "not"+    , "or"+    , "predicate"+    , "prop"+    , "real"+    , "rewriting"+    , "then"+    , "true"+    , "type"+    , "unit"+    , "void"+    , "with"+    , "sign Nil Cons"+    , "div"+    , "mod"+    ]
+ src/Tip/Rename.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Tip.Rename(renameAvoiding,RenamedId(..)) where++#include "errors.h"+import Data.Char (isDigit)+import Tip.Core hiding (globals)+import Tip.Scope+import Tip.Pretty+import Tip.Utils.Rename+import Data.Traversable (Traversable)+import Data.Foldable (Foldable)+import qualified Data.Foldable as F+import qualified Data.Map as M++-- | The representation of renamed Ids.+newtype RenamedId = RenamedId String+  deriving (Eq,Ord,Show)++instance PrettyVar RenamedId where+  varStr (RenamedId x) = x++data TwoStage a = Remain a | Renamed String+ deriving (Eq,Ord)++instance PrettyVar a => Show (TwoStage a) where+  show (Remain x)  = "Remain " ++ varStr x+  show (Renamed s) = "Renamed " ++ s++renameSome+  :: (Traversable t,Ord a,PrettyVar a)+  => (a -> Bool) -> [String] -> (a -> [String]) -> t a -> t (TwoStage a)+renameSome p_rename kwds mk_name =+  renameWithBlocks+    (map Renamed kwds)+    (\ v ->+      if p_rename v then map Renamed (mk_name v)+                    else Remain v:__)++renameRest+  :: (Traversable t,Ord a,PrettyVar a)+  => [String] -> (a -> [String]) -> t (TwoStage a) -> t RenamedId+renameRest kwds mk_name =+  renameWithBlocks+    (map RenamedId kwds)+    (\ v ->+       case v of+         Renamed s -> RenamedId s:__+         Remain a  -> map RenamedId (mk_name a))++-- | Renames a theory+renameAvoiding :: forall a . (Ord a,PrettyVar a) =>+       [String]         -- ^ Keywords to avoid+    -> (Char -> String) -- ^ Escaping+    -> Theory a         -- ^ Theory to be renamed+    -> Theory RenamedId -- ^ The renamed theory+renameAvoiding kwds repl thy+   = mapDecls (renameRest kwds (filter (`notElem` assigned_gbl_names) . disambig rn)) first_pass+ where+  first_pass :: Theory (TwoStage a)+  first_pass = renameSome (`elem` gbls0) kwds (disambig rn) thy+    where gbls0 = M.keys (globals (scope thy)) ++ M.keys (types (scope thy))++  assigned_gbl_names   = [ s | Renamed s <- F.toList first_pass ]++  rn :: a -> String+  rn = concatMap repl . varStr+
+ src/Tip/Scope.hs view
@@ -0,0 +1,220 @@+-- | A monad for keeping track of variable scope.+{-# LANGUAGE CPP, RecordWildCards, GeneralizedNewtypeDeriving, FlexibleContexts #-}+module Tip.Scope where++#include "errors.h"+import Tip.Core hiding (globals, locals)+import Tip.Pretty+import Control.Applicative+import Control.Monad+import Control.Monad.State+import Control.Monad.Error+import Data.Map (Map)+import Data.Set (Set)+import qualified Data.Map as M+import qualified Data.Set as S+import Text.PrettyPrint+import Control.Monad.Identity+import Data.Maybe++-- | The scope of a theory+scope :: (PrettyVar a, Ord a) => Theory a -> Scope a+scope thy = checkScope (withTheory thy get)++data Scope a = Scope+  { inner   :: Set a+  , types   :: Map a (TypeInfo a)+  , locals  :: Map a (Type a)+  , globals :: Map a (GlobalInfo a) }+  deriving Show++-- * Querying the scope++data TypeInfo a =+    TyVarInfo+  | DatatypeInfo (Datatype a)+  | SortInfo Int+  deriving (Eq, Show)++data GlobalInfo a =+    FunctionInfo      (PolyType a)+  | ConstructorInfo   (Datatype a) (Constructor a)+  | ProjectorInfo     (Datatype a) (Constructor a) Int (Type a)+  | DiscriminatorInfo (Datatype a) (Constructor a)+  deriving Show++globalType :: GlobalInfo a -> PolyType a+globalType (FunctionInfo ty) = ty+globalType (ConstructorInfo dt con) = constructorType dt con+globalType (ProjectorInfo dt _ _ ty) = destructorType dt ty+globalType (DiscriminatorInfo dt _) = destructorType dt (BuiltinType Boolean)+++isType, isTyVar, isSort, isLocal, isGlobal :: Ord a => a -> Scope a -> Bool+isType x s = M.member x (types s)+isLocal x s = M.member x (locals s)+isGlobal x s = M.member x (globals s)+isTyVar x s = M.lookup x (types s) == Just TyVarInfo+isSort x s = case M.lookup x (types s) of Just SortInfo{} -> True+                                          _               -> False++lookupType :: Ord a => a -> Scope a -> Maybe (TypeInfo a)+lookupType x s = M.lookup x (types s)++lookupLocal :: Ord a => a -> Scope a -> Maybe (Type a)+lookupLocal x s = M.lookup x (locals s)++lookupGlobal :: Ord a => a -> Scope a -> Maybe (GlobalInfo a)+lookupGlobal x s = M.lookup x (globals s)++lookupDatatype :: Ord a => a -> Scope a -> Maybe (Datatype a)+lookupDatatype x s = do+  DatatypeInfo dt <- M.lookup x (types s)+  return dt++lookupFunction :: Ord a => a -> Scope a -> Maybe (PolyType a)+lookupFunction x s = do+  FunctionInfo ty <- M.lookup x (globals s)+  return ty++lookupConstructor :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a)+lookupConstructor x s = do+  ConstructorInfo dt con <- M.lookup x (globals s)+  return (dt, con)++lookupDiscriminator :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a)+lookupDiscriminator x s = do+  DiscriminatorInfo dt con <- M.lookup x (globals s)+  return (dt, con)++lookupProjector :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a, Int, Type a)+lookupProjector x s = do+  ProjectorInfo dt con i ty <- M.lookup x (globals s)+  return (dt, con, i, ty)++whichDatatype :: Ord a => a -> Scope a -> Datatype a+whichDatatype s = fromMaybe __ . lookupDatatype s+whichLocal :: Ord a => a -> Scope a -> Type a+whichLocal s = fromMaybe __ . lookupLocal s+whichGlobal :: Ord a => a -> Scope a -> GlobalInfo a+whichGlobal s = fromMaybe __ . lookupGlobal s+whichFunction :: Ord a => a -> Scope a -> PolyType a+whichFunction s = fromMaybe __ . lookupFunction s+whichConstructor :: Ord a => a -> Scope a -> (Datatype a, Constructor a)+whichConstructor s = fromMaybe __ . lookupConstructor s+whichDiscriminator :: Ord a => a -> Scope a -> (Datatype a, Constructor a)+whichDiscriminator s = fromMaybe __ . lookupDiscriminator s+whichProjector :: Ord a => a -> Scope a -> (Datatype a, Constructor a, Int, Type a)+whichProjector s = fromMaybe __ . lookupProjector s++-- * The scope monad++newtype ScopeT a m b = ScopeT { unScopeT :: StateT (Scope a) (ErrorT Doc m) b }+  deriving (Functor, Applicative, Monad, MonadPlus, Alternative, MonadState (Scope a), MonadError Doc)++instance MonadTrans (ScopeT a) where+  lift = ScopeT . lift . lift++instance Error Doc where+  strMsg = text++runScopeT :: Monad m => ScopeT a m b -> m (Either Doc b)+runScopeT (ScopeT m) = runErrorT (evalStateT m emptyScope)++checkScopeT :: Monad m => ScopeT a m b -> m b+checkScopeT m = runScopeT m >>= check+  where+    check (Left err) = fail (show err)+    check (Right x)  = return x++type ScopeM a = ScopeT a Identity++runScope :: ScopeM a b -> Either Doc b+runScope = runIdentity . runScopeT++checkScope :: ScopeM a b -> b+checkScope = runIdentity . checkScopeT++emptyScope :: Scope a+emptyScope = Scope S.empty M.empty M.empty M.empty++inContext :: Pretty a => a -> ScopeM b c -> ScopeM b c+inContext x m =+  catchError m (\e -> throwError (sep [e, text "in context", nest 2 (pp x)]))++local :: Monad m => ScopeT a m b -> ScopeT a m b+local m = do+  s <- get+  x <- m+  put s+  return x++-- * Adding things to the scope in the scope monad++newScope :: Monad m => ScopeT a m b -> ScopeT a m b+newScope m = local $ do+  modify (\s -> s { inner = S.empty })+  m++newName :: (PrettyVar a, Ord a, Monad m) => a -> ScopeT a m ()+newName x = do+  s <- gets inner+  case S.member x s of+    True ->+      throwError $+        fsep [text "Name", ppVar x, text "rebound"]+    False ->+      modify (\s -> s { inner = S.insert x (inner s) })++newTyVar :: (Monad m, Ord a, PrettyVar a) => a -> ScopeT a m ()+newTyVar ty = do+  newName ty+  modify $ \s -> s {+    types = M.insert ty TyVarInfo (types s) }++newSort :: (Monad m, Ord a, PrettyVar a) => Sort a -> ScopeT a m ()+newSort Sort{..} = do+  newName sort_name+  modify $ \s -> s {+    types = M.insert sort_name (SortInfo sort_arity) (types s) }++newDatatype :: (Monad m, Ord a, PrettyVar a) => Datatype a -> ScopeT a m ()+newDatatype dt@Datatype{..} = do+  newName data_name+  modify $ \s -> s {+    types = M.insert data_name (DatatypeInfo dt) (types s) }+  mapM_ (newConstructor dt) data_cons++newConstructor :: (Monad m, Ord a, PrettyVar a) => Datatype a -> Constructor a -> ScopeT a m ()+newConstructor dt con@Constructor{..} = do+  mapM_ (newName . fst) funcs+  modify $ \s -> s {+    -- OBS entries from left argument take precedence+    globals = M.union (M.fromList funcs) (globals s) }+  where+    funcs =+      (con_name, ConstructorInfo dt con):+      (con_discrim, DiscriminatorInfo dt con):+      [(name, ProjectorInfo dt con i ty) | (i, (name, ty)) <- zip [0..] con_args]++newFunction :: (Monad m, Ord a, PrettyVar a) => Signature a -> ScopeT a m ()+newFunction Signature{..} = do+  newName sig_name+  modify $ \s -> s {+    globals = M.insert sig_name (FunctionInfo sig_type) (globals s) }++newLocal :: (Monad m, Ord a, PrettyVar a) => Local a -> ScopeT a m ()+newLocal Local{..} = do+  newName lcl_name+  modify $ \s -> s {+    locals = M.insert lcl_name lcl_type (locals s) }++-- | Add everything in a theory+withTheory :: (Monad m, Ord a, PrettyVar a) => Theory a -> ScopeT a m b -> ScopeT a m b+withTheory Theory{..} m = do+  mapM_ newDatatype thy_datatypes+  mapM_ newSort thy_sorts+  mapM_ (newFunction . signature) thy_funcs+  mapM_ newFunction thy_sigs+  m+
+ src/Tip/Simplify.hs view
@@ -0,0 +1,184 @@+{-# LANGUAGE FlexibleContexts, RecordWildCards, ScopedTypeVariables, ViewPatterns, PatternGuards #-}+module Tip.Simplify where++import Tip.Core+import Tip.Scope+import Tip.Fresh+import Data.Generics.Geniplate+import Data.List+import Data.Maybe+import Data.Monoid+import Control.Applicative+import Control.Monad+import qualified Data.Map as Map+import Tip.Writer++-- | Options for the simplifier+data SimplifyOpts a =+  SimplifyOpts {+    touch_lets    :: Bool,+    -- ^ Allow simplifications on lets+    should_inline :: Maybe (Scope a) -> Expr a -> Bool,+    -- ^ Inlining predicate+    inline_match  :: Bool+    -- ^ Allow function inlining to introduce match+  }++-- | Gentle options: if there is risk for code duplication, only inline atomic expressions+gently :: SimplifyOpts a+gently       = SimplifyOpts True (const atomic) True++-- | Aggressive options: inline everything that might plausibly lead to simplification+aggressively :: Name a => SimplifyOpts a+aggressively = SimplifyOpts True useful True+  where+    useful _ Lam{} = True+    useful mscp (f :@: _) = isConstructor mscp f+    useful _ _ = False++-- | Simplify an entire theory+simplifyTheory :: Name a => SimplifyOpts a -> Theory a -> Fresh (Theory a)+simplifyTheory opts thy@Theory{..} = do+  thy_funcs   <- mapM (simplifyExprIn (Just thy) opts) thy_funcs+  thy_asserts <- mapM (simplifyExprIn (Just thy) opts{inline_match = False}) thy_asserts+  return Theory{..}++-- | Simplify an expression, without knowing its theory+simplifyExpr :: forall f a. (TransformBiM (WriterT Any Fresh) (Expr a) (f a), Name a) => SimplifyOpts a -> f a -> Fresh (f a)+simplifyExpr opts = simplifyExprIn Nothing opts++-- | Simplify an expression within a theory+simplifyExprIn :: forall f a. (TransformBiM (WriterT Any Fresh) (Expr a) (f a), Name a) => Maybe (Theory a) -> SimplifyOpts a -> f a -> Fresh (f a)+simplifyExprIn mthy opts@SimplifyOpts{..} = fmap fst . runWriterT . aux+  where+    {-# SPECIALISE aux :: Expr a -> WriterT Any Fresh (Expr a) #-}+    aux :: forall f. TransformBiM (WriterT Any Fresh) (Expr a) (f a) => f a -> WriterT Any Fresh (f a)+    aux = transformBiM $ \e0 ->+      let+        share e1 | e1 /= e0  = return e1+                 | otherwise = return e0 in+      case e0 of+        Builtin At :@: (Lam vars body:args) ->+          hooray $+          aux (foldr (uncurry Let) body (zip vars args))++        Let x e body | touch_lets && (atomic e || occurrences x body <= 1) ->+          lift ((e // x) body) >>= aux++        Let x e body | touch_lets && inlineable body x e ->+          do e1 <- lift ((e // x) body)+             (e2, Any simplified) <- lift (runWriterT (aux e1))+             if simplified then hooray $ return e2 else return e0++        Match e [Case _ e1,Case (LitPat (Bool b)) e2]+          | e1 == bool (not b) && e2 == bool b -> hooray $ return e+          | e1 == bool b && e2 == bool (not b) -> hooray $ return (neg e)++        Match (Let x e body) alts | touch_lets ->+          aux (Let x e (Match body alts))++        Match _ [Case Default body] -> hooray $ return body++        Match (hd :@: args) alts | isConstructor mscp hd ->+          -- We use reverse because the default case comes first and we want it last+          case filter (matches hd . case_pat) (reverse alts) of+            [] -> return e0+            Case (ConPat _ lcls) body:_ ->+              hooray $+              aux $+                foldr (uncurry Let) body (zip lcls args)+            Case _ body:_ -> hooray $ return body+          where+            matches (Gbl gbl) (ConPat gbl' _) = gbl == gbl'+            matches (Builtin (Lit lit)) (LitPat lit') = lit == lit'+            matches _ Default = True+            matches _ _ = False++        Match (Lcl x) alts ->+          Match (Lcl x) <$> sequence+          [ Case pat <$> case pat of+              ConPat g bs -> subst ((Gbl g :@: map Lcl bs) /// x) rhs+              LitPat l    -> subst (literal l /// x) rhs+              _           -> return rhs+          | Case pat rhs <- alts+          ]+          where+            subst f e = do+              (e', Any successful) <- lift (runWriterT (f e))+              if successful then aux e' else return e++        Builtin Equal :@: [Builtin (Lit (Bool x)) :@: [], t]+          | x -> hooray $ return t+          | otherwise -> hooray $ return $ neg t++        Builtin Equal :@: [t, Builtin (Lit (Bool x)) :@: []]+          | x -> hooray $ return t+          | otherwise -> hooray $ return $ neg t++        Builtin Equal :@: [litView -> Just s,litView -> Just t] -> hooray $ return (bool (s == t))++        Builtin Distinct :@: [litView -> Just s,litView -> Just t] -> hooray $ return (bool (s /= t))++        Builtin Not     :@: [e]      -> share (neg e)+        Builtin And     :@: [e1, e2] -> share (e1 /\ e2)+        Builtin Or      :@: [e1, e2] -> share (e1 \/ e2)+        Builtin Implies :@: [e1, e2] -> share (e1 ==> e2)++        Builtin Equal :@: [e1, e2] ->+          case exprType e1 of+            t@(_ :=>: _) -> hooray $ go t e1 e2 []+              where+              go (args :=>: rest) u v lcls =+                do more <- lift (mapM freshLocal args)+                   go rest (apply u (map Lcl more))+                           (apply v (map Lcl more))+                           (lcls ++ more)+              go _ u v lcls = return (mkQuant Forall lcls (u === v))+            _ -> return e0++        Gbl gbl@Global{..} :@: ts ->+          case Map.lookup gbl_name inlinings of+            Just func@Function{..}+              | and [ inlineable func_body x t | (x, t) <- zip func_args ts ] -> do+                  func_body <- boo $ aux func_body+                  e1 <-+                    transformTypeInExpr (applyType func_tvs gbl_args) <$>+                      lift (substMany (zip func_args ts) func_body)+                  (e2, Any simplified) <- lift (runWriterT (aux e1))+                  if (simplified && (inline_match || not (containsMatch e2))) || atomic func_body+                  then hooray $ return e2+                  else return (Gbl gbl :@: ts)+            _ -> return (Gbl gbl :@: ts)++        _ -> return e0++    inlineable body var val = should_inline mscp val || occurrences var body <= 1+    mscp = fmap scope mthy++    isRecursiveGroup [fun] = defines fun `elem` uses fun+    isRecursiveGroup _     = True++    inlinings =+      case mthy of+        Nothing -> Map.empty+        Just Theory{..} ->+          Map.fromList . map (\fun -> (func_name fun, fun)) .+          concat . filter (not . isRecursiveGroup) . topsort $ thy_funcs++    containsMatch e = not (null [ e' | e'@Match{} <- universe e ])++    new /// old = transformExprM $ \e ->+      if e == Lcl old then hooray $ lift (freshen new) else return e++    hooray x = do+      tell (Any True)+      x++    boo x = censor (const (Any False)) x++isConstructor :: Name a => Maybe (Scope a) -> Head a -> Bool+isConstructor _ (Builtin Lit{}) = True+isConstructor mscp (Gbl gbl) = isJust $ do+  scp <- mscp+  lookupConstructor (gbl_name gbl) scp+isConstructor _ _ = False
+ src/Tip/Types.hs view
@@ -0,0 +1,256 @@+-- | The abstract syntax+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, PatternGuards #-}+{-# LANGUAGE ExplicitForAll, FlexibleContexts, FlexibleInstances, TemplateHaskell, MultiParamTypeClasses #-}+module Tip.Types where++import Data.Generics.Geniplate+import Data.Foldable (Foldable)+import Data.Traversable (Traversable)+import Data.Monoid++data Head a+  = Gbl (Global a)+  | Builtin Builtin+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++data Local a = Local { lcl_name :: a, lcl_type :: Type a }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++data Global a = Global+  { gbl_name      :: a+  , gbl_type      :: PolyType a+  , gbl_args      :: [Type a]+  }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++infix 5 :@:++data Expr a+  -- maybe move Lit from Builtin under Head to straight here+  = Head a :@: [Expr a]+  | Lcl (Local a)+  | Lam [Local a] (Expr a)+  -- Merge with Quant?+  | Match (Expr a) [Case a]+  -- ^ The default case comes first if there is one+  | Let (Local a) (Expr a) (Expr a)+  -- Allow a list of bound variables, like in SMT-LIB?+  | Quant QuantInfo Quant [Local a] (Expr a)+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++data Quant = Forall | Exists+  deriving (Eq,Ord,Show)++data QuantInfo = NoInfo+  deriving (Eq,Ord,Show)++data Case a = Case { case_pat :: Pattern a, case_rhs :: Expr a }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++data Builtin+  = At+  | Lit Lit+  | And+  | Or+  | Not+  | Implies+  | Equal+  | Distinct+  | IntAdd+  | IntSub+  | IntMul+  | IntDiv+  | IntMod+  | IntGt+  | IntGe+  | IntLt+  | IntLe+  deriving (Eq,Ord,Show)++intBuiltin :: Builtin -> Bool+intBuiltin b = b `elem` [IntAdd,IntSub,IntMul,IntDiv,IntMod,IntGt,IntGe,IntLt,IntLe]++litBuiltin :: Builtin -> Bool+litBuiltin Lit{} = True+litBuiltin _     = False++eqRelatedBuiltin :: Builtin -> Bool+eqRelatedBuiltin b = b `elem` [Equal,Distinct]++logicalBuiltin :: Builtin -> Bool+logicalBuiltin b = b `elem` [And,Or,Implies,Equal,Distinct,Not]++data Lit+  = Int Integer+  | Bool Bool+  | String String -- Not really here but might come from GHC+  deriving (Eq,Ord,Show)++-- | Patterns in branches+data Pattern a+  = Default+  | ConPat { pat_con  :: Global a, pat_args :: [Local a] }+  | LitPat Lit+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++-- | Polymorphic types+data PolyType a =+  PolyType+    { polytype_tvs  :: [a]+    , polytype_args :: [Type a]+    , polytype_res  :: Type a+    }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++-- | Types+data Type a+  = TyVar a+  | TyCon a [Type a]+  | [Type a] :=>: Type a+  | BuiltinType BuiltinType+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++data BuiltinType+  = Integer | Boolean+  deriving (Eq,Ord,Show)++data Function a = Function+  { func_name :: a+  , func_tvs  :: [a]+  , func_args :: [Local a]+  , func_res  :: Type a+  , func_body :: Expr a+  }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++-- | Uninterpreted function+data Signature a = Signature+  { sig_name :: a+  , sig_type :: PolyType a+  }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++-- | Uninterpreted sort+data Sort a = Sort+  { sort_name :: a+  , sort_arity :: Int }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++-- | Data definition+data Datatype a = Datatype+  { data_name :: a+  , data_tvs  :: [a]+  , data_cons :: [Constructor a]+  }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++data Constructor a = Constructor+  { con_name    :: a+  , con_discrim :: a+  , con_args    :: [(a,Type a)]+  }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++data Theory a = Theory+  { thy_datatypes   :: [Datatype a]+  , thy_sorts       :: [Sort a]+  , thy_sigs        :: [Signature a]+  , thy_funcs       :: [Function a]+  , thy_asserts     :: [Formula a]+  }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++emptyTheory :: Theory a+emptyTheory = Theory [] [] [] [] []++joinTheories :: Theory a -> Theory a -> Theory a+joinTheories (Theory a o e u i) (Theory s n t h d) = Theory (a++s) (o++n) (e++t) (u++h) (i++d)++instance Monoid (Theory a) where+  mempty  = emptyTheory+  mappend = joinTheories++data Formula a = Formula+  { fm_role :: Role+  , fm_tvs  :: [a]+  -- ^ top-level quantified type variables+  , fm_body :: Expr a+  }+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)++data Role = Assert | Prove+  deriving (Eq,Ord,Show)++instanceUniverseBi [t| forall a . (Expr a,Expr a) |]+instanceUniverseBi [t| forall a . (Function a,Expr a) |]+instanceUniverseBi [t| forall a . (Function a,Global a) |]+instanceUniverseBi [t| forall a . (Function a,Type a) |]+instanceUniverseBi [t| forall a . (Datatype a,Type a) |]+instanceUniverseBi [t| forall a . (Expr a,Pattern a) |]+instanceUniverseBi [t| forall a . (Expr a,Local a) |]+instanceUniverseBi [t| forall a . (Expr a,Global a) |]+instanceUniverseBi [t| forall a . (Theory a,Expr a) |]+instanceUniverseBi [t| forall a . (Theory a,Type a) |]+instanceUniverseBi [t| forall a . (Type a,Type a) |]+instanceUniverseBi [t| forall a . (Theory a,Constructor a) |]+instanceUniverseBi [t| forall a . (Theory a,Global a) |]+instanceUniverseBi [t| forall a . (Theory a,Builtin) |]+instanceTransformBi [t| forall a . (Expr a,Expr a) |]+instanceTransformBi [t| forall a . (a,Expr a) |]+instanceTransformBi [t| forall a . (a,Formula a) |]+instanceTransformBi [t| forall a . (Expr a,Function a) |]+instanceTransformBi [t| forall a . (Expr a,Theory a) |]+instanceTransformBi [t| forall a . (Head a,Expr a) |]+instanceTransformBi [t| forall a . (Head a,Theory a) |]+instanceTransformBi [t| forall a . (Local a,Expr a) |]+instanceTransformBi [t| forall a . (Pattern a,Expr a) |]+instanceTransformBi [t| forall a . (Pattern a,Theory a) |]+instanceTransformBi [t| forall a . (Type a,Theory a) |]+instanceTransformBi [t| forall a . (Type a,Expr a) |]+instanceTransformBi [t| forall a . (Type a,Type a) |]+instance Monad m => TransformBiM m (Expr a) (Expr a) where+  {-# INLINE transformBiM #-}+  transformBiM = $(genTransformBiM' [t| forall m a . (Expr a -> m (Expr a)) -> Expr a -> m (Expr a) |])+instance Monad m => TransformBiM m (Expr a) (Function a) where+  {-# INLINE transformBiM #-}+  transformBiM = $(genTransformBiM' [t| forall m a . (Expr a -> m (Expr a)) -> Function a -> m (Function a) |])+instance Monad m => TransformBiM m (Pattern a) (Expr a) where+  {-# INLINE transformBiM #-}+  transformBiM = $(genTransformBiM' [t| forall m a . (Pattern a -> m (Pattern a)) -> Expr a -> m (Expr a) |])+instance Monad m => TransformBiM m (Local a) (Expr a) where+  {-# INLINE transformBiM #-}+  transformBiM = $(genTransformBiM' [t| forall m a . (Local a -> m (Local a)) -> Expr a -> m (Expr a) |])+instance Monad m => TransformBiM m (Expr a) (Theory a) where+  {-# INLINE transformBiM #-}+  transformBiM = $(genTransformBiM' [t| forall m a . (Expr a -> m (Expr a)) -> Theory a -> m (Theory a) |])+instance Monad m => TransformBiM m (Expr a) (Formula a) where+  {-# INLINE transformBiM #-}+  transformBiM = $(genTransformBiM' [t| forall m a . (Expr a -> m (Expr a)) -> Formula a -> m (Formula a) |])+instance Monad m => TransformBiM m (Type a) (Type a) where+  {-# INLINE transformBiM #-}+  transformBiM = $(genTransformBiM' [t| forall m a . (Type a -> m (Type a)) -> Type a -> m (Type a) |])+instance Monad m => TransformBiM m (Function a) (Theory a) where+  {-# INLINE transformBiM #-}+  transformBiM = $(genTransformBiM' [t| forall m a . (Function a -> m (Function a)) -> Theory a -> m (Theory a) |])++transformExpr :: (Expr a -> Expr a) -> Expr a -> Expr a+transformExpr = transformBi++transformExprM :: Monad m => (Expr a -> m (Expr a)) -> Expr a -> m (Expr a)+transformExprM = transformBiM++transformExprIn :: TransformBi (Expr a) (f a) => (Expr a -> Expr a) -> f a -> f a+transformExprIn = transformBi++transformExprInM :: TransformBiM m (Expr a) (f a) => (Expr a -> m (Expr a)) -> f a -> m (f a)+transformExprInM = transformBiM++transformType :: (Type a -> Type a) -> Type a -> Type a+transformType = transformBi++transformTypeInExpr :: (Type a -> Type a) -> Expr a -> Expr a+transformTypeInExpr =+  $(genTransformBiT' [[t|PolyType|]] [t|forall a. (Type a -> Type a) -> Expr a -> Expr a|])+++
+ src/Tip/Utils.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE ScopedTypeVariables #-}+-- | Handy utilities+module Tip.Utils where++import Data.List+import Data.Graph+import Data.List.Split+import Data.Char+import Data.Foldable (Foldable)+import qualified Data.Foldable as F+import Data.Ord++-- | Sort and remove duplicates+usort :: Ord a => [a] -> [a]+usort = map head . group . sort++-- | Sort things in topologically in strongly connected components+sortThings :: Ord name => (thing -> name) -> (thing -> [name]) -> [thing] -> [[thing]]+sortThings name refers things =+    map flattenSCC $ stronglyConnComp+        [ (thing,name thing,filter (`elem` names) (refers thing))+        | thing <- things+        ]+  where+    names = map name things++-- | Makes a nice flag from a constructor string+--+-- > > flagify "PrintPolyFOL"+-- > "print-poly-fol"+flagify :: String -> String+flagify+    = map toLower . intercalate "-"+    . split (condense $ dropInitBlank $ keepDelimsL $ whenElt (\x -> isUpper x || isSpace x))++-- | Makes a flag from something @Show@-able+flagifyShow :: Show a => a -> String+flagifyShow = flagify . show++-- | Calculates the maximum value of a foldable value.+--+-- Useful to find the highest unique in a structure+maximumOn :: forall f a b . (F.Foldable f,Ord b) => (a -> b) -> f a -> b+maximumOn f = f . F.maximumBy (comparing f)+
+ src/Tip/Utils/Rename.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE ViewPatterns, FlexibleContexts #-}+module Tip.Utils.Rename where++import Control.Monad.State+import Control.Monad.Reader++import Data.Traversable (Traversable)+import qualified Data.Traversable as T++import Data.Map (Map)+import qualified Data.Map as M+import Data.Set (Set)+import qualified Data.Set as S++import Data.Maybe (fromMaybe)+import Data.List (find)++import Control.Arrow++import Unsafe.Coerce++type RenameM a b = ReaderT (Suggestor a b) (State (Map a b,Set b))++type Suggestor a b = a -> [b]++disambig :: (a -> String) -> Suggestor a String+disambig f (f -> x) = x : extra x ++ [ x ++ show (i :: Int) | i <- [2..] ]+  where+    extra x = fromMaybe [] (find (x `elem`) families)++    families =+       [ ["a","b","c"]+       , ["f","g","h"]+       , ["p","q"]+       , ["n","m","o"]+       , ["x","y","z"]+       , ["xs","ys","zs"]+       ]++disambig2 :: (a -> String) -> (b -> String) -> Suggestor (Either a b) String+disambig2 f _ (Left a)  = disambig f a+disambig2 _ g (Right b) = disambig g b++evalRenameM :: (Ord b) => Suggestor a b -> [b] -> RenameM a b r -> r+evalRenameM f block m = fst (runRenameM f block M.empty m)++runRenameM :: (Ord b) => Suggestor a b -> [b] -> Map a b -> RenameM a b r -> (r,Map a b)+runRenameM f block alloc m = second fst (runState (runReaderT m f) s0)+  where s0 = (alloc,S.fromList (block ++ M.elems alloc))++insert :: (Ord a,Ord b) => a -> RenameM a b b+insert n = go 0 =<< asks ($ n)+  where+    go i (s:ss) = do+        u <- gets snd+        if s `S.member` u then go (i+1) ss else do+            modify (M.insert n s *** S.insert s)+            return s+    go i [] = error "ran out of names!?"++insertMany :: (Ord a,Ord b) => [a] -> RenameM a b [b]+insertMany = mapM insert++lkup :: (Ord a,Ord b) => a -> RenameM a b b+lkup n = do+    m_s <- gets (M.lookup n . fst)+    case m_s of+        Just s  -> return s+        Nothing -> insert n++rename :: (Ord a,Ord b,Traversable t) => t a -> RenameM a b (t b)+rename = T.mapM lkup++renameWith :: (Ord a,Ord b,Traversable t) => Suggestor a b -> t a -> t b+renameWith = renameWithBlocks []++renameWithBlocks :: (Ord a,Ord b,Traversable t) => [b] -> Suggestor a b -> t a -> t b+renameWithBlocks bs f = evalRenameM f bs . rename+
+ src/Tip/WorkerWrapper.hs view
@@ -0,0 +1,50 @@+-- Generic support for the worker-wrapper transform.+{-# LANGUAGE PatternGuards, RecordWildCards #-}+module Tip.WorkerWrapper where++import Tip.Core+import Tip.Fresh+import Tip.Simplify+import qualified Data.Map as Map+import Data.Maybe++data WorkerWrapper a = WorkerWrapper+  { ww_func :: Function a                           -- ^ The function to transform+  , ww_args :: [Local a]                            -- ^ New function argument type+  , ww_res  :: Type a                               -- ^ New function result type+  , ww_def  :: Expr a -> Expr a                     -- ^ Transform function body+  , ww_use  :: Head a -> [Expr a] -> Fresh (Expr a) -- ^ Transform call to function+  }++workerWrapperTheory :: Name a => (Theory a -> Fresh [WorkerWrapper a]) -> Theory a -> Fresh (Theory a)+workerWrapperTheory f thy = do+  ww <- f thy+  case ww of+    [] -> return thy+    _ -> workerWrapper ww thy >>= workerWrapperTheory f++workerWrapperFunctions :: Name a => (Function a -> Maybe (Fresh (WorkerWrapper a))) -> Theory a -> Fresh (Theory a)+workerWrapperFunctions f =+  workerWrapperTheory (sequence . catMaybes . map f . thy_funcs)++workerWrapper :: Name a => [WorkerWrapper a] -> Theory a -> Fresh (Theory a)+workerWrapper wws thy@Theory{..} =+  transformExprInM updateUse thy' >>= simplifyTheory gently+  where+    thy' = thy { thy_funcs = map updateDef thy_funcs }+    m = Map.fromList [(func_name (ww_func ww), ww) | ww <- wws]+    updateDef func@Function{..} =+      case Map.lookup func_name m of+        Nothing -> func+        Just WorkerWrapper{..} ->+          func {+            func_args = ww_args, func_res = ww_res,+            func_body = ww_def func_body+          }+    updateUse (Gbl gbl :@: args)+      | Just WorkerWrapper{ww_func=Function{..}, ..} <- Map.lookup (gbl_name gbl) m =+          let gbl_type = PolyType { polytype_tvs = func_tvs,+                                    polytype_args = map lcl_type ww_args,+                                    polytype_res = ww_res}+          in ww_use (Gbl gbl{gbl_type = gbl_type}) args+    updateUse e = return e
+ src/Tip/Writer.hs view
@@ -0,0 +1,46 @@+-- A faster implementation of the writer monad.++{-# LANGUAGE Rank2Types #-}+module Tip.Writer where++import Data.Monoid++import Control.Monad+import Control.Applicative++newtype WriterT w m a = WriterT { unWriterT :: forall b. (w -> a -> m b) -> m b }++instance (Monoid w, Monad m) => Functor (WriterT w m) where+  {-# INLINE fmap #-}+  fmap f x = x >>= return . f++instance (Monoid w, Monad m) => Applicative (WriterT w m) where+  {-# INLINE pure #-}+  pure = return+  {-# INLINE (<*>) #-}+  (<*>) = liftM2 ($)++instance (Monoid w, Monad m) => Monad (WriterT w m) where+  {-# INLINE return #-}+  return x = WriterT (\k -> k mempty x)++  {-# INLINE (>>=) #-}+  WriterT m >>= f =+    WriterT $ \k ->+      m (\w x -> unWriterT (f x) (\w' y -> k (w `mappend` w') y))++{-# INLINE runWriterT #-}+runWriterT :: (Monoid w, Monad m) => WriterT w m a -> m (a, w)+runWriterT (WriterT f) = f (\w x -> return (x, w))++{-# INLINE tell #-}+tell :: (Monoid w, Monad m) => w -> WriterT w m ()+tell w = WriterT (\k -> k w ())++{-# INLINE lift #-}+lift :: (Monoid w, Monad m) => m a -> WriterT w m a+lift x = WriterT (\k -> x >>= \y -> k mempty y)++{-# INLINE censor #-}+censor :: (Monoid w, Monad m) => (w -> w) -> WriterT w m a -> WriterT w m a+censor f (WriterT m) = WriterT (\k -> m (\w x -> k (f w) x))
+ tip-lib.cabal view
@@ -0,0 +1,88 @@+name:                tip-lib+version:             0.1+synopsis:            tons of inductive problems - support library and tools+description:         This package provides a tool for processing inductive theorem proving problems in TIP format (see the homepage for details).+homepage:            http://tip-org.github.io+bug-reports:         http://github.com/tip-org/tools/issues+license:             BSD3+license-file:        LICENSE+author:              Dan Rosén, Nick Smallbone+maintainer:          danr@chalmers.se+category:            Theorem Provers+build-type:          Simple+cabal-version:       >=1.10++source-repository head+  type:     git+  location: http://github.com/tip-org/tools++library+  exposed-modules:+    Tip.Core+    Tip.Lint+    Tip.Types+    Tip.Scope+    Tip.Fresh+    Tip.WorkerWrapper+    Tip.Simplify+    Tip.Passes+    Tip.Pretty+    Tip.Pretty.SMT+    Tip.Pretty.Why3+    Tip.Pretty.Isabelle+    Tip.Pretty.Haskell++    Tip.Parser++    Tip.Utils+    Tip.Writer++    Tip.Rename+    Tip.Utils.Rename+    Tip.Haskell.Repr+    Tip.Haskell.Translate+    Tip.Haskell.Rename+    Tip.CallGraph+  other-modules:+    Tip.Pass.AxiomatizeFuncdefs+    Tip.Pass.Lift+    Tip.Pass.Booleans+    Tip.Pass.CommuteMatch+    Tip.Pass.AddMatch+    Tip.Pass.CSEMatch+    Tip.Pass.RemoveNewtype+    Tip.Pass.RemoveMatch+    Tip.Pass.NegateConjecture+    Tip.Pass.EqualFunctions+    Tip.Pass.Uncurry+    Tip.Pass.Pipeline+    Tip.Pass.EliminateDeadCode+    Tip.Pass.FillInCases++    Tip.Parser.ErrM+    Tip.Parser.AbsTIP+    Tip.Parser.LexTIP+    Tip.Parser.ParTIP+    Tip.Parser.Convert++  hs-source-dirs:      src+  include-dirs:        src+  ghc-options:         -w+  default-language:    Haskell2010+  build-depends:       base >=4 && <5,+                       geniplate-mirror >=0.7.1,+                       split,+                       containers,+                       mtl,+                       pretty,+                       array,+                       optparse-applicative++executable tip+  main-is:             executable/Main.hs+  default-language:    Haskell2010+  build-depends:       base,+                       tip-lib,+                       pretty-show,+                       pretty,+                       optparse-applicative