tip-haskell-frontend 0.1.1 → 0.2

raw patch · 16 files changed

+770/−538 lines, 16 filesdep +ghc-simpledep +optparse-applicativedep ~tip-libPVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-simple, optparse-applicative

Dependency ranges changed: tip-lib

API changes (from Hackage documentation)

Files

• changelog +6/−0
• executable/Main.hs +35/−27
• src/Tip.hs +5/−0
• src/Tip/Calls.hs +0/−58
• src/Tip/Compile.hs +0/−175
• src/Tip/CoreToTip.hs +5/−0
• src/Tip/Dicts.hs +4/−15
• src/Tip/FreeTyCons.hs +24/−35
• src/Tip/GHCScope.hs +0/−49
• src/Tip/GenericInstances.hs +34/−0
• src/Tip/HaskellFrontend.hs +154/−59
• src/Tip/Params.hs +39/−17
• src/Tip/Prelude.hs +454/−0
• src/Tip/Property.hs +2/−2
• src/Tip/Unfoldings.hs +0/−95
• tip-haskell-frontend.cabal +8/−6

@@ -1,3 +1,9 @@+tip-haskell-frontend 0.2 (released 2015-10-28):+* Depend on ghc-simple by Anton Ekblad, and simplify the internals.+* Export readHaskellOrTipFile.+* Add Tip.Prelude+* Add question (synonymous to neg)+ tip-haskell-frontend 0.1.1 (released 2015-06-11): * Relax dependency on tip-lib to >= 0.1.1 && <= 0.2. 

@@ -20,36 +20,44 @@ import Tip.Pretty import Tip.Pretty.SMT as SMT -import Text.PrettyPrint+import Text.PrettyPrint hiding ((<>)) +import Options.Applicative+ main :: IO () main = do-    f:es <- getArgs-    thy <- readHaskellFile Params-      { file = f-      , include = []-      , flags = [] -- [PrintCore,PrintProps,PrintExtraIds,PrintInitialTip]-      , only = es -- []-      , extra = [] -- es-      }-    -- putStrLn (ppRender thy)-    let renamed_thy = renameWith disambigId thy-    let pipeline =-          freshPass $-            runPasses-              [ SimplifyAggressively-              , RemoveNewtype-              , UncurryTheory-              , CommuteMatch-              , SimplifyGently-              , IfToBoolOp-              , RemoveAliases, CollapseEqual-              , CommuteMatch-              , SimplifyGently-              , CSEMatch-              , EliminateDeadCode-              ]-    print (SMT.ppTheory (pipeline renamed_thy))+    (file,params) <-+      execParser $+        info (helper <*>+                ((,) <$> strArgument (metavar "FILENAME" <> help "Haskell file to process")+                     <*> parseParams))+          (fullDesc <>+           progDesc "Translate Haskell to TIP" <>+           header "tip-ghc - translate Haskell to TIP")+    mthy <- readHaskellFile file params+    case mthy of+      Left s -> error s+      Right thy -> do+        when (PrintInitialTheory `elem` debug_flags params) $ putStrLn (ppRender thy)+        let renamed_thy = renameWith disambigId thy+        let pipeline =+              freshPass $+                runPasses+                  [ SimplifyAggressively+                  , RemoveNewtype+                  , UncurryTheory+                  , CommuteMatch+                  , SimplifyGently+                  , IfToBoolOp+                  , RemoveAliases, CollapseEqual+                  , CommuteMatch+                  , SimplifyGently+                  , CSEMatch+                  , EliminateDeadCode+                  ]+        case pipeline renamed_thy of+          [thy'] -> print (SMT.ppTheory thy')+          _      -> error "tip-ghc: not one theory!"  data Var = Var String | Refresh Var Int   deriving (Show,Eq,Ord)

@@ -15,6 +15,7 @@     , (.&&.)     , (.||.)     , neg+    , question     , forAll     , exists     , module Test.QuickCheck@@ -67,6 +68,10 @@ -- | Negation neg :: a -> Neg a neg = Neg++-- | Question (same as negation)+question :: a -> Neg a+question = Neg  -- | Universal quantification forAll :: (a -> b) -> Forall a b

@@ -1,58 +0,0 @@-{-# LANGUAGE NamedFieldPuns,ScopedTypeVariables #-}-module Tip.Calls-    ( module VarSet-    , Constructors(..)-    , exprCalls-    , calls-    , transCalls-    , transFrom-    ) where--import CoreSyn-import Id-import VarSet-import CoreFVs-import DataCon-import TyCon--import Tip.GHCUtils-import Tip.Unfoldings-import Tip.FreeTyCons--import qualified Data.Set as S--data Constructors = With | Without deriving Eq---- | The vars this expression calls-exprCalls :: Constructors -> CoreExpr -> VarSet-exprCalls cons = exprSomeFreeVars $ \ v ->-          (isLocalId v || isGlobalId v || (cons == With && isDataConId v && not (isNewtypeConId v)))-       && (cons == With || not (isDataConId v))---- | The functions this functions calls (not transitively)-calls :: Constructors -> Id -> VarSet-calls c v = cons `unionVarSet` case maybeUnfolding v of-    Just e -> exprCalls c e-    _      -> emptyVarSet-  where-    cons | c == With = mkVarSet (concatMap (map dataConWorkId . tyConDataCons)-                                           (filter (not . isClassTyCon) (S.toList (varTyCons v))))-                                           -- NOTE: Ignore all class contexts-         | otherwise = emptyVarSet---- | The functions this function calls transitively-transCalls :: Constructors -> Id -> VarSet-transCalls c = transFrom c . unitVarSet---- | The transitive closure of calls from this set-transFrom :: Constructors -> VarSet -> VarSet-transFrom c = go emptyVarSet-  where-    go visited queue-        | isEmptyVarSet to_visit = visited-        | otherwise = go (visited `unionVarSet` to_visit)-                         (foldVarSet (\ i vs -> calls c i `unionVarSet` vs)-                                     emptyVarSet-                                     to_visit)-      where to_visit = queue `minusVarSet` visited-

@@ -1,175 +0,0 @@-{-# LANGUAGE RecordWildCards, NamedFieldPuns, CPP #-}-module Tip.Compile (compileHaskellFile) where--import Tip.Calls-import Tip.Dicts (inlineDicts)-import Tip.GHCUtils-import Tip.Params-import Tip.ParseDSL-import Tip.GHCScope-import Tip.Unfoldings-import Data.List.Split (splitOn)--import Control.Monad-import Data.List-import Data.Maybe-import qualified Data.Foldable as F-import System.FilePath--import CoreMonad (liftIO)-import CoreSyn-import CoreSyn (flattenBinds)-import DynFlags-import GHC-import GHC.Paths-import HscTypes-import SimplCore-import Var-import VarSet-#if __GLASGOW_HASKELL__ < 708-import StaticFlags-#endif--compileHaskellFile :: Params  -> IO [Var]-compileHaskellFile params@Params{..} = do--    -- Notify ghc where ghc is installed-    runGhc (Just libdir) $ do--        -- Set interpreted so we can get the signature,-        -- and expose all unfoldings-        dflags0 <- getSessionDynFlags-        let dflags =-#if __GLASGOW_HASKELL__ >= 708-                updateWays $-                addWay' WayThreaded $-#endif-                     dflags0 { ghcMode = CompManager-                             , optLevel = 0-                             , profAuto = NoProfAuto-                             , importPaths = include ++ includePaths dflags0 ++ ["."]-                             }-                        `wopt_unset` Opt_WarnOverlappingPatterns-#if __GLASGOW_HASKELL__ >= 708-                        `gopt_unset` Opt_IgnoreInterfacePragmas-                        `gopt_unset` Opt_OmitInterfacePragmas-                        `gopt_set` Opt_ExposeAllUnfoldings-                        `gopt_set` Opt_BuildDynamicToo-#else-                        `dopt_unset` Opt_IgnoreInterfacePragmas-                        `dopt_unset` Opt_OmitInterfacePragmas-                        `dopt_set` Opt_ExposeAllUnfoldings-#endif-        _ <- setSessionDynFlags dflags--            -- add .hs if it is not present (apparently not supporting lhs)-        let file_with_ext = replaceExtension file ".hs"--        target <- guessTarget file_with_ext Nothing-        addTarget target-        r <- load LoadAllTargets-        when (failed r) $ error "Compilation failed!"--        mod_graph <- getModuleGraph-        let mod_sum = findModuleSum file_with_ext mod_graph--        -- Parse, typecheck and desugar the module-        p <- parseModule mod_sum-        t <- typecheckModule p-        d <- desugarModule t--        let modguts = dm_core_module d--        let binds = fixUnfoldings (inlineDicts (flattenBinds (mg_binds modguts)))--        let fix_id :: Id -> Id-            fix_id = fixId binds--        liftIO $ when (PrintCore `elem` flags) $-             putStrLn ("Tip.Compile, PrintCore:\n" ++ showOutputable binds)--        -- Set the context for evaluation-        setContext $-            [ IIDecl (simpleImportDecl (moduleName (ms_mod mod_sum)))-            , IIDecl (qualifiedImport "GHC.Types")-            , IIDecl (qualifiedImport "GHC.Base")-            , IIDecl (qualifiedImport "Prelude")-            ]-            -- Also include the imports the module is importing-            ++ map (IIDecl . unLoc) (ms_textual_imps mod_sum)--        ids_in_scope <- getIdsInScope fix_id--        let only' :: [String]-            only' = concatMap (splitOn ",") only--            props :: [Var]-            props =-                [ fix_id i-                | i <- ids_in_scope-                , varWithPropType i-                , not (varInTip i)-                , null only || varToString i `elem` only'-                ]--        when (PrintProps `elem` flags)-             (liftIO (putStrLn ("Tip.Compile, PrintProps:\n" ++ showOutputable props)))--        extra_ids <- extraIds params props--        -- Wrapping up-        return (props `union` extra_ids)--findModuleSum :: FilePath -> [ModSummary] -> ModSummary-findModuleSum file-    = fromMaybe (error $ "Cannot find module " ++ file)-    . find (maybe False (== file) . summaryHsFile)--summaryHsFile :: ModSummary -> Maybe FilePath-summaryHsFile = ml_hs_file . ms_location--parseToId :: String -> Ghc Id-parseToId s = do-    t <- lookupString s-    case mapMaybe thingToId t of-        []  -> error $ s ++ " not in scope!"-        [x] -> return x-        xs  -> error $ s ++ " in scope as too many things: " ++ showOutputable xs--extraIds :: Params -> [Var] -> Ghc [Var]-extraIds p@Params{..} prop_ids = do--    extra_ids <- mapM parseToId (concatMap (splitOn ",") extra)--    let trans_ids :: VarSet-        trans_ids = unionVarSets $-            map (transCalls With) (prop_ids ++ extra_ids)--    let ids = varSetElems $ filterVarSet (\ x -> not (varInTip x || varWithPropType x) && not (hasClass (varType x)))-            trans_ids--    -- Filters out silly things like-    -- Control.Exception.Base.patError and GHC.Prim.realWorld#-    let in_scope = inScope . varToString--    ids_in_scope <- filterM in_scope ids--    liftIO $ when (PrintExtraIds `elem` flags) $ do-        putStrLn "Tip.Compile, PrintExtraIds:"-        let out :: String -> [Id] -> IO ()-            out lbl os = putStrLn $ lbl ++ " =\n " ++ showOutputable [ (o{-,maybeUnfolding o-}) | o <- os ]-#define OUT(i) out "i" (i)-        OUT(prop_ids)-        OUT(extra_ids)-        OUT(ids)-        OUT(ids_in_scope)-#undef OUT--    return ids_in_scope--qualifiedImport :: String -> ImportDecl name-qualifiedImport = qualifiedImportDecl . mkModuleName--qualifiedImportDecl :: ModuleName -> ImportDecl name-qualifiedImportDecl m = (simpleImportDecl m) { ideclQualified = True }-

@@ -121,6 +121,11 @@             }  -- | Translate a definition+--+-- This does not work when+-- f = g+-- when it "should" be+-- f = /\ a . g @a trDefn :: Var -> CoreExpr -> TM [Function Id] trDefn v e = do     let (tvs,ty) = splitForAllTys (C.exprType e)

@@ -2,7 +2,7 @@ {-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleContexts, NamedFieldPuns #-} {-# LANGUAGE CPP #-} {-# OPTIONS_GHC -fno-warn-orphans #-}-module Tip.Dicts (inlineDicts,maybeUnfolding) where+module Tip.Dicts (inlineDicts,maybeUnfolding,varFromRealModule) where  import Tip.GHCUtils (showOutputable) #if __GLASGOW_HASKELL__ >= 708@@ -26,18 +26,6 @@ import Name (getOccString,nameModule_maybe) import PrelNames (gHC_REAL) -instanceTransformBiT-    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]-    [t| forall a . (Expr a,Expr a) |]--instanceTransformBiT-    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]-    [t| forall a . (Expr a,[Bind a]) |]--instanceTransformBiT-    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]-    [t| forall a . (Expr a,[(a,Expr a)]) |]- -- | Maybe the unfolding of an Id maybeUnfolding :: Id -> Maybe CoreExpr maybeUnfolding v = case ri of@@ -47,12 +35,13 @@     ri = realIdUnfolding v  +varFromRealModule :: Var -> String -> Bool+varFromRealModule x s = getOccString x == s && nameModule_maybe (varName x) == Just gHC_REAL  inlineDicts :: TransformBi (Expr Id) t => t -> t inlineDicts = transformBi $ \ e0 -> case e0 of     App (App (Var f) (Type t)) (Var d)-        | getOccString f == "div" && nameModule_maybe (varName f) == Just gHC_REAL -> Var f-        | getOccString f == "mod" && nameModule_maybe (varName f) == Just gHC_REAL -> Var f+        | any (varFromRealModule f) ["mod","div"] -> Var f #if __GLASGOW_HASKELL__ >= 708         | [try] <- [ try | BuiltinRule _ _ 2 try <- idCoreRules f ]         , Just e <- try unsafeGlobalDynFlags (emptyInScopeSet,realIdUnfolding) f [Type t,Var d]

@@ -1,5 +1,6 @@ {-# LANGUAGE PatternGuards #-}-module Tip.FreeTyCons (bindsTyCons,bindsTyCons',varTyCons,tyTyCons) where+{-# LANGUAGE ScopedTypeVariables #-}+module Tip.FreeTyCons (bindsTyCons) where  import CoreSyn import CoreUtils (exprType)@@ -12,48 +13,36 @@ import Data.Set (Set) import qualified Data.Set as S -bindsTyCons :: [CoreBind] -> [TyCon]-bindsTyCons = S.toList . S.unions . map bindTyCons . flattenBinds+import Tip.GenericInstances+import Data.Generics.Geniplate -bindsTyCons' :: [(Var,CoreExpr)] -> [TyCon]-bindsTyCons' = S.toList . S.unions . map bindTyCons+import Tip.Utils -bindTyCons :: (Var,CoreExpr) -> Set TyCon-bindTyCons (v,e) = S.union (exprTyCons e) (varTyCons v)+bindsTyCons :: [(Var,CoreExpr)] -> [TyCon]+bindsTyCons vses = S.toList $ S.unions+  [ varTyCons v `S.union` exprTyCons e+  | (v,e) <- vses+  ] +varTyCons :: Var -> Set TyCon+varTyCons = tyTyCons . varType+ tyTyCons :: Type -> Set TyCon tyTyCons = go . expandTypeSynonyms   where-    go t0-        | Just (t1,t2) <- splitFunTy_maybe t0    = S.union (go t1) (go t2)-        | Just (tc,ts) <- splitTyConApp_maybe t0 = S.insert tc (S.unions (map go ts))-        | Just (_,t) <- splitForAllTy_maybe t0   = go t-        | otherwise                              = S.empty--varTyCons :: Var -> Set TyCon-varTyCons = tyTyCons . varType+  go t0+    | Just (t1,t2) <- splitFunTy_maybe t0    = S.union (go t1) (go t2)+    | Just (tc,ts) <- splitTyConApp_maybe t0 = S.insert tc (S.unions (map go ts))+    | Just (_,t) <- splitForAllTy_maybe t0   = go t+    | otherwise                              = S.empty  -- | For all used constructors in expressions and patterns, --   return the TyCons they originate from exprTyCons :: CoreExpr -> Set TyCon-exprTyCons e0 = case e0 of-    Case e x t alts -> S.unions (varTyCons x:tyTyCons t:exprTyCons e:map altTyCons alts)-    App e1 e2       -> S.union (exprTyCons e1) (exprTyCons e2)-    Let bs e        -> S.unions (exprTyCons e:map exprTyCons (rhssOfBind bs))-    Lam _ e         -> exprTyCons e-    Cast e _        -> exprTyCons e-    Tick _ e        -> exprTyCons e-    Var x           -> varTyCons x-    Type t          -> tyTyCons t-    Coercion{}      -> S.empty-    Lit{}           -> tyTyCons (exprType e0)--altTyCons :: CoreAlt -> Set TyCon-altTyCons (alt,_,rhs) = patTyCons alt `S.union` exprTyCons rhs--patTyCons :: AltCon -> Set TyCon-patTyCons p = case p of-    DataAlt c -> S.singleton (dataConTyCon c)-    LitAlt{}  -> S.empty-    DEFAULT   -> S.empty+exprTyCons e =+  S.unions $+    [ varTyCons x `S.union` tyTyCons t | Case _ x t _  <- universeBi e ] +++    [ varTyCons x                      | Var x :: CoreExpr <- universeBi e ] +++    [ tyTyCons t                       | Type t :: CoreExpr <- universeBi e ] +++    [ S.singleton (dataConTyCon c) | DataAlt c <- universeBi e ] 

@@ -1,49 +0,0 @@-{-# LANGUAGE CPP #-}-module Tip.GHCScope where--import GHC hiding (Sig)--import Control.Applicative-import Data.Maybe--import DataCon--#if __GLASGOW_HASKELL__ >= 708-import ConLike-#endif--getIdsInScope :: (Id -> Id) -> Ghc [Id]-getIdsInScope fix_id = do--    ns <- getNamesInScope--    things <- catMaybes <$> mapM lookupName ns--    return [ fix_id i | AnId i <- things ]--parseName' :: String -> Ghc [Name]-parseName' = handleSourceError (\ _ -> return []) . parseName--inScope :: String -> Ghc Bool-inScope s = do-    xs <- parseName' s-    return $ if null xs then False else True--lookupString :: String -> Ghc [TyThing]-lookupString s = do-    xs <- parseName' s-    catMaybes <$> mapM lookupName xs--thingToId :: TyThing -> Maybe Id-thingToId (AnId i)     = Just i-#if __GLASGOW_HASKELL__ >= 708-thingToId (AConLike (RealDataCon dc)) = Just (dataConWorkId dc)-thingToId (AConLike (PatSynCon _pc))  = error "HipSpec.Sig.Scope: Pattern synonyms not supported"-#else-thingToId (ADataCon dc) = Just (dataConWorkId dc)-#endif-thingToId _            = Nothing--mapJust :: (a -> Maybe b) -> [a] -> Maybe b-mapJust k = listToMaybe . mapMaybe k-

@@ -0,0 +1,34 @@+{-# LANGUAGE PatternGuards, TypeSynonymInstances, FlexibleInstances, ViewPatterns, ExplicitForAll #-}+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleContexts, NamedFieldPuns #-}+-- | Data.Generic.Geniplate instances for GHC+module Tip.GenericInstances (module Tip.GenericInstances, module Data.Generics.Geniplate) where++import CoreSyn+import Data.Generics.Geniplate++import Var+import Coercion+import Id+import Literal+import Type+import DataCon++instanceTransformBiT+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]+    [t| forall a . (Expr a,Expr a) |]++instanceTransformBiT+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]+    [t| forall a . (Expr a,[Bind a]) |]++instanceTransformBiT+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]+    [t| forall a . (Expr a,[(a,Expr a)]) |]++instanceUniverseBiT+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]+    [t| forall a . (Expr a,Expr a) |]++instanceUniverseBiT+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|DataCon|] ]+    [t| forall a . (Expr a,AltCon) |]

@@ -1,93 +1,188 @@ {-# LANGUAGE RecordWildCards, DisambiguateRecordFields, NamedFieldPuns #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-} -- | The Haskell frontend to Tip-module Tip.HaskellFrontend(readHaskellFile,Id(..),module Tip.Params) where+module Tip.HaskellFrontend(readHaskellFile,readHaskellOrTipFile,Id(..),module Tip.Params) where -import Tip.Core-import Tip.Calls-import Tip.Compile-import Tip.CoreToTip-import Tip.Dicts (inlineDicts)-import Tip.FreeTyCons+import Language.Haskell.GHC.Simple hiding (Id) -- Thanks, Anton!+import qualified Language.Haskell.GHC.Simple as Simple++import Tip.Utils import Tip.Id import Tip.Params+import Tip.Core+import Tip.CoreToTip+ import Tip.ParseDSL import Tip.Property-import Tip.RemoveDefault-import Tip.Unfoldings-import Tip.Uniquify+ import Tip.GHCUtils-import Tip.Pretty +import CoreFVs+import VarSet+import UniqSupply++import Data.List+import Data.Either++import Tip.Dicts+import Tip.Uniquify+import Tip.RemoveDefault+import Tip.FreeTyCons++import TysWiredIn (boolTyCon,listTyCon)+ import Control.Monad-import Data.Char-import Data.List (partition,union,delete)-import Data.Map (Map)-import qualified Data.Map as M-import Data.Maybe (isNothing)-import System.Directory-import System.Exit++import Tip.GenericInstances import Data.Generics.Geniplate -import qualified Id as GHC-import qualified CoreSubst as GHC-import Var (Var)-import TyCon (isAlgTyCon,isClassTyCon,tyConName)-import TysWiredIn (boolTyCon)-import UniqSupply+import qualified Data.Foldable as F --- | Transforms a Haskell file to a Tip Theory, crashing if unsuccessful-readHaskellFile :: Params -> IO (Theory Id)-readHaskellFile params@Params{..} = do+import qualified Tip.Parser as TipP -    -- whenFlag params PrintParams $ putStrLn (ppShow params)+import System.FilePath -    -- maybe (return ()) setCurrentDirectory directory+-- | If the file cannot be read as a TIP file, it is instead read as a Haskell file.+readHaskellOrTipFile :: FilePath -> Params -> IO (Either String (Theory (Either TipP.Id Id)))+readHaskellOrTipFile file params =+  let ext = takeExtension file in+  if ext == ".smt2" then+    fmap (fmap (fmap Left)) (TipP.parseFile file)+  else if ext == ".hs" || ext == ".lhs" then+    fmap (fmap (fmap Right)) (readHaskellFile file params)+  else+    do mthy1 <- TipP.parseFile file+       case mthy1 of+         Right thy -> return (Right (fmap Left thy))+         Left err1 ->+           do mthy2 <- readHaskellFile file params+              case mthy2 of+                Right thy -> return (Right (fmap Right thy))+                Left err2 -> return (Left (err1 ++ "\n" ++ err2)) -    prop_ids <- compileHaskellFile params+-- | Transforms a Haskell file to a Tip Theory or an error+readHaskellFile :: FilePath -> Params -> IO (Either String (Theory Id))+readHaskellFile file params@Params{..} = do -    let vars = filterVarSet (not . varInTip) $-               unionVarSets (map (transCalls Without) prop_ids)+  let cfg :: CompConfig ModGuts+      cfg = defaultConfig {+          cfgUseGhcErrorLogger = True,+          cfgGhcFlags =+            ["-dynamic-too"+            ,"-fno-ignore-interface-pragmas"+            ,"-fno-omit-interface-pragmas"+            ,"-fexpose-all-unfoldings"]+            ++ include+        } -    us0 <- mkSplitUniqSupply 'h'+  mres <- compileWith cfg [file] -    let (binds,_us1) = initUs us0 $ sequence-            [ fmap ((,) v) (runUQ . uqExpr <=< rmdExpr $ inlineDicts e)-            | v <- varSetElems vars-            , isNothing (GHC.isClassOpId_maybe v)-            , Just e <- [maybeUnfolding v]+  case mres of+    Failure errs warns ->+      return . Left . unlines $+        [ showOutputable p ++ ":" ++ m ++ "\n" ++ l+        | Simple.Error p m l <- errs+        ]+    Success cms warns _ ->+      do {- putStrLn $ unlines+            [ showOutputable p ++ ":" ++ m+            | Simple.Warning p m <- warns             ]+         -}+         readModules params cms -        tcs = filter (\ x -> isAlgTyCon x && not (nameInTip (tyConName x)) && not (isClassTyCon x))-                     (delete boolTyCon (bindsTyCons' binds))+addUnfoldings :: [(Var,CoreExpr)] -> [(Var,CoreExpr)]+addUnfoldings binds | null unfs = binds+                    | otherwise = addUnfoldings (binds ++ unfs)+  where+    unfs = usortOn fst+      [ (x,inlineDicts e')+      | (_,e) <- binds+      , Var x :: CoreExpr <- universeBi e+      , x `notElem` map fst binds+      , Just e' <- [maybeUnfolding x]+      ] -    when (PrintCore `elem` flags) $ do-        putStrLn "Tip.HaskellFrontend, PrintInitialTip:"-        putStrLn (showOutputable binds)+readModules :: Params -> [CompiledModule ModGuts] -> IO (Either String (Theory Id))+readModules params@Params{..} cms = do+  let mgs    = map modCompiledModule cms+  let binds0 = addUnfoldings (map (fmap inlineDicts) (flattenBinds (concatMap mg_binds mgs))) -    let tip_data =+  us0 <- mkSplitUniqSupply 'h'++  let (binds,_us1) = initUs us0 $ sequence+         [ fmap ((,) v) (runUQ . uqExpr <=< rmdExpr $ e)+         | (v,e) <- binds0+         , not (varInTip v)+         ]++  let the_props  :: [(Var,CoreExpr)]+      the_props =+        [ ve+        | ve@(v,_) <- binds+        , not (varInTip v)+        , varToString v `elem` extra_names+          || (varWithPropType v && maybe True (varToString v `elem`) prop_names)+        ]++  let prop_ids = map fst the_props++  -- Find all bindings transitively from props++  let reachable = transFrom prop_ids binds++  when (PrintCore `elem` debug_flags) $ putStrLn $ showOutputable reachable++  let tycons =+         filter (\ x -> isAlgTyCon x && not (nameInTip (tyConName x)) && not (isClassTyCon x))+                (delete boolTyCon (bindsTyCons reachable))++  let (data_errs,tip_data) =+        partitionEithers           [ case trTyCon tc of-              Right tc' -> tc'-              Left err -> error $ showOutputable tc ++ ": " ++ err-          | tc <- tcs+              Right tc' -> Right tc'+              Left err  -> Left $ showOutputable tc ++ ": " ++ err+          | tc <- tycons           ] -    let tip_fns0 = concat+  let (fn_errs,concat -> tip_fns0) =+        partitionEithers           [ case runTM (trDefn v e) of-              Right fn -> fn-              Left err -> error $ showOutputable v ++ ": " ++ err-          | (v,e) <- binds+              Right fn -> Right fn+              Left err -> Left $ showOutputable v ++ ": " ++ err+          | (v,e) <- reachable+          , all (not . varFromRealModule v) ["mod","div"]           ] -        -- Now, split these into properties and non-properties-    let (prop_fns,tip_fns) = partition (isPropType . func_res) tip_fns0+  let (prop_fns,tip_fns) = partition (isPropType . func_res) tip_fns0 -        tip_props = either error id (mapM trProperty prop_fns)+      (prop_errs,tip_props) = partitionEithers (map trProperty prop_fns) -        thy = Theory tip_data [] [Signature Error errorType] tip_fns tip_props+      thy = Theory tip_data [] [ Signature Tip.Id.Error errorType+                               | any (Tip.Id.Error `F.elem`) tip_fns ||+                                 any (Tip.Id.Error `F.elem`) tip_props+                               ] tip_fns tip_props -    when (PrintInitialTip `elem` flags) $ do-        putStrLn "Tip.HaskellFrontend, PrintInitialTip:"-        putStrLn (ppRender thy)+      errs = data_errs ++ fn_errs ++ prop_errs -    return thy+  return (if null errs then Right thy else Left (unlines errs))++transFrom :: [Var] -> [(Var,CoreExpr)] -> [(Var,CoreExpr)]+transFrom (mkVarSet -> s0) binds = filter (\ (v,_) -> v `elemVarSet` fin) binds+  where+  fin = go s0++  go :: VarSet ->  VarSet+  go visited | isEmptyVarSet new = visited+             | otherwise         = go (new `unionVarSet` visited)+    where+    new :: VarSet+    new =+      unionVarSets+        [ exprSomeFreeVars (\ _ -> True) rhs_start+        | v_start <- varSetElems visited+        , Just rhs_start <- [lookup v_start binds]+        ]+      `minusVarSet` visited 

@@ -1,31 +1,53 @@ module Tip.Params where +import Options.Applicative++import Tip.Utils++import Data.List.Split+ -- | Parameters data Params = Params-  { file        :: FilePath-  -- ^ File to process-  , include     :: [FilePath]+  { include     :: [FilePath]   -- ^ Directories to include-  , flags       :: [DebugFlags]+  , debug_flags :: [DebugFlag]   -- ^ Debugging flags-  , only        :: [String]+  , prop_names :: Maybe [String]   -- ^ Only consider these properties-  , extra       :: [String]-  -- ^ Also translate these functions and its transitive dependencies+  , extra_names :: [String]+  -- ^ Extra names to consider   }   deriving Show --- | Default parameters, given the name of the file to process-defaultParams :: FilePath -> Params-defaultParams fp = Params-  { file = fp-  , include = []-  , flags = []-  , only = []-  , extra = []+commaSep :: [String] -> [String]+commaSep = concatMap (splitOn ",")++parseParams :: Parser Params+parseParams = Params+  <$> many (strOption (long "include" <> short 'i' <> metavar "PATH" <> help "Extra include directory"))+  <*> many (foldr (<|>) empty [ flag' debug_flag (long (flagifyShow debug_flag) <> help (debugHelp debug_flag))+                              | debug_flag <- [minBound..maxBound]+                              ])+  <*> (pure Nothing <|> fmap (Just . commaSep) (many (strOption prop_opt)))+  <*> fmap commaSep (many (strOption (long "extra" <> short 'e' <> metavar "NAME" <> help "Function declaration to add to theory")))++  where++  prop_opt = long "only" <> long "prop" <> short 'p' <> metavar "NAME" <> help "Property declaration to consider (default all)"++-- | Default (empty) parameters+defaultParams :: Params+defaultParams = Params+  { include = []+  , debug_flags = []+  , prop_names = Nothing+  , extra_names = []   }  -- | Debugging flags-data DebugFlags = PrintCore | PrintProps | PrintExtraIds | PrintInitialTip-  deriving (Eq,Show)+data DebugFlag = PrintCore | PrintInitialTheory+  deriving (Eq,Show,Enum,Bounded) +debugHelp :: DebugFlag -> String+debugHelp PrintCore          = "Print core bindings from GHC"+debugHelp PrintInitialTheory = "Print initial theory"

@@ -0,0 +1,454 @@+{-# LANGUAGE DeriveDataTypeable,FlexibleInstances #-}+-- | A drop-in replacement for Prelude with unfoldings exported, oriented towards Nats+module Tip.Prelude (module Tip, module Tip.Prelude, Bool(..), Maybe(..), Either(..), Int) where++import Prelude (Eq,Ord,Show,Bool(..),Int,Either(..),Maybe(..))+import qualified Prelude as P+import Data.Typeable+import Tip++-- * Booleans++otherwise :: Bool+otherwise = True++infixr 3 &&++(&&) :: Bool -> Bool -> Bool+True && x = x+_    && _ = False++infixr 2 ||++(||) :: Bool -> Bool -> Bool+False || x = x+_     || _ = True++not :: Bool -> Bool+not True = False+not False = True++-- * Nat functions++data Nat = Z | S Nat+  deriving (Eq,Show,Typeable,Ord)++even Z = True+even (S Z) = False+even (S (S x)) = even x++double :: Nat -> Nat+double Z     = Z+double (S x) = S (S (double x))++half :: Nat -> Nat+half Z = Z+half (S Z) = Z+half (S (S n)) = S (half n)++infixl 6 ++infixl 6 -++infixl 7 *++infixr 8 ^++(+) :: Nat -> Nat -> Nat+S n + m = S (n + m)+Z   + m = m++(*) :: Nat -> Nat -> Nat+S n * m = m + (n * m)+Z   * m = Z++(^) :: Nat -> Nat -> Nat+n ^ (S m) = n * n ^ m+n ^ Z     = S Z++-- * Truncated subtraction+(-) :: Nat -> Nat -> Nat+S n - S m = n - m+m   - Z   = m+Z   - _   = Z++infix 4 <+infix 4 <=+infix 4 >+infix 4 >=+infix 4 ==+infix 4 /=++(<) :: Nat -> Nat -> Bool+_ < Z     = False+Z < _     = True+S n < S m = n < m++(<=) :: Nat -> Nat -> Bool+Z   <= _   = True+_   <= Z   = False+S x <= S y = x <= y++(>) :: Nat -> Nat -> Bool+Z > _     = False+_ > Z     = True+S n > S m = n > m++(>=) :: Nat -> Nat -> Bool+_   >= Z   = True+Z   >= _   = False+S x >= S y = x >= y++(==) :: Nat -> Nat -> Bool+Z   == Z   = True+Z   == _   = False+S _ == Z   = False+S x == S y = x == y++(/=) :: Nat -> Nat -> Bool+x /= y = not (x == y)++max :: Nat -> Nat -> Nat+max Z n = n+max m Z = m+max (S n) (S m) = S (max n m)++min :: Nat -> Nat -> Nat+min Z _ = Z+min _ Z = Z+min (S n) (S m) = S (min n m)++-- * List functions on nats++take :: Nat -> [a] -> [a]+take Z _ = []+take _ [] = []+take (S x) (y:ys) = y : (take x ys)++drop :: Nat -> [a] -> [a]+drop Z xs = xs+drop _ [] = []+drop (S x) (_:xs) = drop x xs++splitAt :: Nat -> [a] -> ([a], [a])+splitAt n xs = (take n xs, drop n xs)++length :: [a] -> Nat+length [] = Z+length (_:xs) = S (length xs)++delete :: Nat -> [Nat] -> [Nat]+delete _ [] = []+delete n (x:xs) =+  case n == x of+    True -> xs+    False -> x : (delete n xs)++deleteAll :: Nat -> [Nat] -> [Nat]+deleteAll _ [] = []+deleteAll n (x:xs) =+  case n == x of+    True -> deleteAll n xs+    False -> x : (deleteAll n xs)++count :: Nat -> [Nat] -> Nat+count x [] = Z+count x (y:ys) =+  case x == y of+    True -> S (count x ys)+    _ -> count x ys++nub :: [Nat] -> [Nat]+nub (x:xs) = x:deleteAll x (nub xs)+nub []     = []++index :: [a] -> Nat -> Maybe a+index (x:xs) Z     = Just x+index (x:xs) (S n) = index xs n+index []     _     = Nothing++elem :: Nat -> [Nat] -> Bool+x `elem` [] = False+x `elem` (y:ys) = x == y || x `elem` ys++isPermutation :: [Nat] -> [Nat] -> Bool+[]     `isPermutation` ys = null ys+(x:xs) `isPermutation` ys = x `elem` ys && xs `isPermutation` delete x ys++sorted,ordered,uniqsorted :: [Nat] -> Bool+sorted = ordered+ordered []       = True+ordered [x]      = True+ordered (x:y:xs) = x <= y && ordered (y:xs)+uniqsorted []       = True+uniqsorted [x]      = True+uniqsorted (x:y:xs) = x < y && uniqsorted (y:xs)++unique :: [Nat] -> Bool+unique []     = True+unique (x:xs) = if x `elem` xs then False else unique xs++insert :: Nat -> [Nat] -> [Nat]+insert n [] = [n]+insert n (x:xs) =+  case n <= x of+    True -> n : x : xs+    _    -> x : (insert n xs)++isort :: [Nat] -> [Nat]+isort [] = []+isort (x:xs) = insert x (isort xs)++eqList :: [Nat] -> [Nat] -> Bool+eqList (x:xs) (y:ys) = (x == y) && (xs `eqList` ys)+eqList []     []     = True+eqList _      _      = False++sum :: [Nat] -> Nat+sum [] = Z+sum (x:xs) = x + sum xs++product :: [Nat] -> Nat+product [] = S Z+product (x:xs) = x * product xs++lookup :: Nat -> [(Nat,b)] -> Maybe b+lookup x ((y,b):ys) | x == y    = Just b+                    | otherwise = lookup x ys+lookup x [] = Nothing++-- * Int functions++zeq,zne,zle,zlt,zgt,zge :: Int -> Int -> Bool+zeq = (P.==)+zne = (P./=)+zle = (P.<=)+zlt = (P.<)+zgt = (P.>)+zge = (P.>=)++zplus,zmult,zminus,zmax,zmin :: Int -> Int -> Int+zplus = (P.+)+zmult = (P.*)+zminus = (P.-)+zmax = P.max+zmin = P.min++-- * List functions on Ints++{-# NOINLINE ztake #-}+ztake :: Int -> [a] -> [a]+ztake 0 _      = []+ztake _ []     = []+ztake n (x:xs) = x:ztake (n `zminus` 1) xs++{-# NOINLINE zdrop #-}+zdrop :: Int -> [a] -> [a]+zdrop 0 xs     = xs+zdrop _ []     = []+zdrop n (x:xs) = zdrop (n `zminus` 1) xs++zsplitAt :: Int -> [a] -> ([a], [a])+zsplitAt n xs = (ztake n xs, zdrop n xs)++{-# NOINLINE zlength #-}+zlength :: [a] -> Int+zlength []     = 0+zlength (x:xs) = 1 `zplus` zlength xs++zdelete :: Int -> [Int] -> [Int]+zdelete x [] = []+zdelete x (y:ys)+  | x `zeq` y = ys+  | otherwise = y:zdelete x ys++zdeleteAll :: Int -> [Int] -> [Int]+zdeleteAll _ [] = []+zdeleteAll n (x:xs) =+  case n `zeq` x of+    True -> zdeleteAll n xs+    False -> x : (zdeleteAll n xs)+++zcount :: Int -> [Int] -> Nat+zcount x []                 = Z+zcount x (y:xs) | x `zeq` y  = S (zcount x xs)+                | otherwise = zcount x xs++zzcount :: Int -> [Int] -> Int+zzcount x []                 = 0+zzcount x (y:xs) | x `zeq` y = 1 `zplus` zzcount x xs+                 | otherwise = zzcount x xs++znub :: [Int] -> [Int]+znub (x:xs) = x:zdeleteAll x (znub xs)+znub []     = []++zindex :: [a] -> Int -> Maybe a+zindex (x:xs) 0 = Just x+zindex (x:xs) n = zindex xs (n `zminus` 1)+zindex []     _ = Nothing++zelem :: Int -> [Int] -> Bool+x `zelem` [] = False+x `zelem` (y:ys) = x `zeq` y || x `zelem` ys++zisPermutation :: [Int] -> [Int] -> Bool+[]     `zisPermutation` ys = null ys+(x:xs) `zisPermutation` ys = x `zelem` ys && xs `zisPermutation` zdelete x ys++zsorted,zordered,zuniqsorted :: [Int] -> Bool+zordered []       = True+zordered [x]      = True+zordered (x:y:xs) = x `zle` y && zordered (y:xs)++zsorted = zordered++zuniqsorted []       = True+zuniqsorted [x]      = True+zuniqsorted (x:y:xs) = x `zlt` y && zuniqsorted (y:xs)++zunique :: [Int] -> Bool+zunique []     = True+zunique (x:xs) = if x `zelem` xs then False else zunique xs++zinsert :: Int -> [Int] -> [Int]+zinsert n [] = [n]+zinsert n (x:xs) =+  case n `zle` x of+    True -> n : x : xs+    _    -> x : (zinsert n xs)++zisort :: [Int] -> [Int]+zisort [] = []+zisort (x:xs) = zinsert x (zisort xs)++zeqList :: [Int] -> [Int] -> Bool+zeqList (x:xs) (y:ys) = (x `zeq` y) && (xs `zeqList` ys)+zeqList []     []     = True+zeqList _      _      = False++zsum :: [Int] -> Int+zsum [] = 0+zsum (x:xs) = x `zplus` zsum xs++zproduct :: [Int] -> Int+zproduct [] = 1+zproduct (x:xs) = x `zmult` zproduct xs++zlookup :: Int -> [(Int,b)] -> Maybe b+zlookup x ((y,b):ys) | x `zeq` y    = Just b+                     | otherwise = zlookup x ys+zlookup x [] = Nothing++-- * Polymorphic lists functions++{-# NOINLINE null #-}+null :: [a] -> Bool+null [] = True+null _  = False++(++) :: [a] -> [a] -> [a]+[]     ++ ys = ys+(x:xs) ++ ys = x : (xs ++ ys)++reverse :: [a] -> [a]+reverse []     = []+reverse (x:xs) = reverse xs ++ [x]++zip :: [a] -> [b] -> [(a, b)]+zip [] _ = []+zip _ [] = []+zip (x:xs) (y:ys) = (x, y) : (zip xs ys)++filter :: (a -> Bool) -> [a] -> [a]+filter p [] = []+filter p (x:xs) | p x = x:filter p xs+filter p (x:xs) = filter p xs+++map :: (a -> b) -> [a] -> [b]+map f []     = []+map f (x:xs) = f x:map f xs++concat :: [[a]] -> [a]+concat (xs:xss) = xs ++ concat xss+concat []       = []++concatMap :: (a -> [b]) -> [a] -> [b]+concatMap f (x:xs) = f x ++ concatMap f xs+concatMap _ []     = []++foldl :: (b -> a -> b) -> b -> [a] -> b+foldl f z []     = z+foldl f z (x:xs) = foldl f (f z x) xs++foldr :: (a -> b -> b) -> b -> [a] -> b+foldr f z []     = z+foldr f z (x:xs) = f x (foldr f z xs)++-- * Lists and booleans++and :: [Bool] -> Bool+and (x:xs) = x && and xs+and []     = True++or :: [Bool] -> Bool+or (x:xs) = x || or xs+or []     = False++all :: (a -> Bool) -> [a] -> Bool+all p []     = True+all p (x:xs) = p x && all p xs++any :: (a -> Bool) -> [a] -> Bool+any p []     = False+any p (x:xs) = p x || any p xs++takeWhile :: (a -> Bool) -> [a] -> [a]+takeWhile _ [] = []+takeWhile p (x:xs) =+  case p x of+    True -> x : (takeWhile p xs)+    _ -> []++dropWhile :: (a -> Bool) -> [a] -> [a]+dropWhile _ [] = []+dropWhile p (x:xs) =+  case p x of+    True -> dropWhile p xs+    _ -> x:xs++-- | Miscellaneous++id :: a -> a+id x = x++const :: a -> b -> a+const x _ = x++infixr 9 .++(.) :: (b -> c) -> (a -> b) -> a -> c+f . g = \ x -> f (g x)++flip :: (a -> b -> c) -> (b -> a -> c)+flip f x y = f y x++infixr 0 $+($) :: (a -> b) -> a -> b+f $ x = f x++maybe :: b -> (a -> b) -> Maybe a -> b+maybe n _ Nothing  = n+maybe _ j (Just x) = j x++either :: (a -> c) -> (b -> c) -> Either a b -> c+either f _ (Left x)  = f x+either _ g (Right y) = g y++fst :: (a,b) -> a+fst (x,_) = x++snd :: (a,b) -> b+snd (_,y) = y+

@@ -28,7 +28,7 @@ trProperty (Function _name tvs [] res_ty b) = case unLam b of   (args,e) -> do     pr <- parseProperty e-    return (Formula Prove tvs (mkQuant Forall args pr))+    return (Formula Prove UserAsserted tvs (mkQuant Forall args pr))   where     unLam (Lam xs e) = let (ys,e') = unLam e in (xs ++ ys,e')     unLam e          = ([],e)@@ -48,7 +48,7 @@        | isId "bool" x = return e -      | isId "Neg" x || isId "neg" x = neg <$> go e+      | isId "Neg" x || isId "neg" x || isId "question" x = neg <$> go e    goo i e0@(projAt -> Just (projAt -> Just (projGlobal -> Just x,e1),e2)) 

@@ -1,95 +0,0 @@-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE ScopedTypeVariables #-}-module Tip.Unfoldings (unfolding,maybeUnfolding,fixUnfoldings,fixId) where--import qualified Data.Map as M--import Control.Applicative-import Data.Traversable (sequenceA)--import Control.Monad.Reader--import CoreSyn-import CoreUnfold-import Id--import Data.Maybe--import Tip.GHCUtils-import Tip.Dicts---- | The unfolding of an Id-unfolding :: Id -> CoreExpr-unfolding i  = fromMaybe (error err) . maybeUnfolding $ i-  where-    err = "No unfolding for identifier " ++ showOutputable i ++-          " (possible solution: Remove *.hi files and try again)"----- | Fixes identifiers according to some core binds-fixId :: [(Var,CoreExpr)] -> Id -> Id-fixId bs = \ i -> case M.lookup i bind_map of-    Just rhs -> i `setIdUnfoldingLazily` mkInlineUnfolding Nothing rhs-    Nothing  -> i-  where-    bind_map = M.fromList bs---- | Ties the knot, fixes all the unfoldings in these core binds-fixUnfoldings :: [(Var,CoreExpr)] -> [(Var,CoreExpr)]-fixUnfoldings bs = map (idMap lkup) bs'-  where-    bs' :: [(Var,CoreExpr)]-    bs' = mapM (exprMap k) bs lkup--    lkup :: Id -> Id-    lkup = fixId bs'--    h :: Id -> (Id -> Id) -> Id-    h x = do-        m <- ask-        return (m x)--    k :: CoreExpr -> (Id -> Id) -> CoreExpr-    k = boringCases h k---- | Maps an expression fun over binds-exprMap :: Applicative f => (CoreExpr -> f CoreExpr) -> (Var,CoreExpr) -> f (Var,CoreExpr)-exprMap f (v,e) = (,) v <$> f e---- | Maps an identifier fun over binds-idMap :: (Id -> Id) -> (Var,CoreExpr) -> (Var,CoreExpr)-idMap f (v,e) = (f v,e)--bindMap :: Applicative f => (CoreExpr -> f CoreExpr) -> CoreBind -> f CoreBind-bindMap f (NonRec v e) = NonRec v <$> f e-bindMap f (Rec vses)   = Rec <$> sequenceA [ (,) v <$> f e | (v,e) <- vses ]--{---- | Maps an expression fun over binds-exprMap :: Applicative f => (CoreExpr -> f CoreExpr) -> CoreBind -> f CoreBind-exprMap f (NonRec v e) = NonRec v <$> f e-exprMap f (Rec vses)   = Rec <$> sequenceA [ (,) v <$> f e | (v,e) <- vses ]---- | Maps an identifier fun over binds-idMap :: (Id -> Id) -> CoreBind -> CoreBind-idMap f (NonRec v e) = NonRec (f v) e-idMap f (Rec vses)   = Rec [ (f v,e) | (v,e) <- vses ]--}---- | Fills in all boring cases for you-boringCases :: Applicative f => (Var -> f Var) -> (CoreExpr -> f CoreExpr) -> CoreExpr -> f CoreExpr-boringCases h f t = case t of-    Var x -> Var <$> h x-    Lit{} -> pure t-    App e1 e2 -> App <$> f e1 <*> f e2-    Lam x e -> Lam x <$> f e-    Let bs e -> Let <$> bindMap f bs <*> f e-    Case s ty w alts ->-        (\s' alts' -> Case s' ty w alts')-            <$> f s-            <*> sequenceA [ (,,) p bs <$> f e | (p,bs,e) <- alts ]-    Cast e co -> (`Cast` co) <$> f e-    Tick tk e -> Tick tk <$> f e-    Type{} -> pure t-    Coercion{} -> pure t-

@@ -1,5 +1,5 @@ name:                tip-haskell-frontend-version:             0.1.1+version:             0.2 license:             BSD3 license-file:        LICENSE author:              Dan Rosén@@ -22,13 +22,12 @@ library   exposed-modules:     Tip.HaskellFrontend+    Tip.Prelude     Tip   other-modules:     Tip.Params     Tip.Id     Tip.GHCUtils-    Tip.Calls-    Tip.Compile     Tip.CoreToTip     Tip.DataConPattern     Tip.Dicts@@ -36,10 +35,10 @@     Tip.ParseDSL     Tip.Property     Tip.RemoveDefault-    Tip.GHCScope     Tip.TyAppBeta-    Tip.Unfoldings     Tip.Uniquify+    Tip.GenericInstances+  ghc-options:         -fexpose-all-unfoldings   hs-source-dirs:      src   include-dirs:        src   default-language:    Haskell2010@@ -54,7 +53,9 @@                        bytestring >=0.9.2,                        split >=0.2,                        geniplate-mirror >=0.7.1,-                       tip-lib >= 0.1.1 && < 0.2,+                       tip-lib >= 0.2 && < 0.3,+                       ghc-simple >= 0.1.2.0 && < 0.2,+                       optparse-applicative,                        QuickCheck >= 2.8  executable tip-ghc@@ -64,4 +65,5 @@                        tip-haskell-frontend,                        tip-lib,                        pretty-show,+                       optparse-applicative,                        pretty