packages feed

tip-haskell-frontend (empty) → 0.1

raw patch · 22 files changed

+1933/−0 lines, 22 filesdep +QuickCheckdep +basedep +bytestringsetup-changed

Dependencies added: QuickCheck, base, bytestring, containers, directory, filepath, geniplate-mirror, ghc, ghc-paths, mtl, pretty, pretty-show, split, tip-haskell-frontend, 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,80 @@+module Main where++import Tip.HaskellFrontend++import Text.Show.Pretty hiding (Name)+import System.Environment+import qualified Data.Foldable as F+import Data.Ord++import Control.Monad++import Tip.Core+import Tip.Fresh+import Tip.Simplify+import Tip.Lint+import Tip.Passes++import Tip.Utils.Rename++import Tip.Pretty+import Tip.Pretty.SMT as SMT++import Text.PrettyPrint++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))++data Var = Var String | Refresh Var Int+  deriving (Show,Eq,Ord)++varMax :: Var -> Int+varMax Var{}         = 0+varMax (Refresh v i) = varMax v `max` i++instance PrettyVar Var where+  varStr (Var "")      = "x"+  varStr (Var xs)      = xs+  varStr (Refresh v i) = varStr v++disambigId :: Id -> [Var]+disambigId i = vs : [ Refresh vs x | x <- [0..] ]+  where+    vs = Var $ case varStr i of { [] -> "x"; xs -> xs }++instance Name Var where+  fresh     = refresh (Var "")+  refresh (Refresh v _) = refresh v+  refresh v@Var{}       = Refresh v `fmap` fresh++  freshNamed s = refresh (Var s)++  getUnique (Refresh _ i) = i+  getUnique Var{}         = 0+
+ src/Tip.hs view
@@ -0,0 +1,102 @@+{-# LANGUAGE TypeOperators, FlexibleInstances #-}+-- | The language properties are expressed in in the Haskell source+module Tip+    ( Equality+    , (:=>:)+    , And+    , Or+    , Neg+    , Forall+    , Exists+    , (===)+    , (=/=)+    , bool+    , (==>)+    , (.&&.)+    , (.||.)+    , neg+    , forAll+    , exists+    , module Test.QuickCheck+    ) where++import Test.QuickCheck hiding ((===), (==>), (.&&.), (.||.), forAll)+import qualified Test.QuickCheck as QC++infix 3 ===+infix 3 =/=+infixr 2 .&&.+infixr 1 .||.+infixr 0 ==>+infixr 0 :=>:++-- | The property data type++data Equality a = a :=: a+data a :=>: b = Given a b+data And a b = And a b+data Or a b = Or a b+data Neg a = Neg a+data Forall a b = Forall (a -> b)+data Exists a b = Exists (a -> b)++-- | Equality+(===) :: a -> a -> Equality a+(===) = (:=:)++-- | Inequality+(=/=) :: a -> a -> Neg (Equality a)+u =/= v = Neg (u === v)++-- | A synonym for '===', but for booleans+bool :: Bool -> Equality Bool+bool lhs = lhs === True++-- | Implication+(==>) :: a -> b -> a :=>: b+(==>) = Given++-- | Conjunction+(.&&.) :: a -> b -> And a b+(.&&.) = And++-- | Disjunction+(.||.) :: a -> b -> Or a b+(.||.) = Or++-- | Negation+neg :: a -> Neg a+neg = Neg++-- | Universal quantification+forAll :: (a -> b) -> Forall a b+forAll = Forall++-- | Existential quantification+exists :: (a -> b) -> Exists a b+exists = Exists++instance (Eq a, Show a) => Testable (Equality a) where+  property (x :=: y) = x QC.=== y++instance Testable b => Testable (Bool :=>: b) where+  property (Given x p) = x QC.==> p++instance Testable b => Testable (Neg Bool :=>: b) where+  property (Given (Neg x) p) = not x QC.==> p++instance Testable (Neg Bool) where+  property (Neg x) = property (not x)++instance (Eq a, Show a, Testable b) => Testable (Equality a :=>: b) where+  property (Given (x :=: y) p) = x == y QC.==> p++instance (Testable a, Testable b) => Testable (And a b) where+  property (And p q) = p QC..&&. q++instance (Testable a, Testable b) => Testable (Or a b) where+  property (Or p q)  = p QC..||. q++instance (Arbitrary a, Show a, Testable b) => Testable (Forall a b) where+  property (Forall p) = property p+
+ src/Tip/Calls.hs view
@@ -0,0 +1,58 @@+{-# 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+
+ src/Tip/Compile.hs view
@@ -0,0 +1,175 @@+{-# 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 }+
+ src/Tip/CoreToTip.hs view
@@ -0,0 +1,380 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+{-# LANGUAGE PatternGuards, TypeSynonymInstances, FlexibleInstances, CPP, RecordWildCards, FlexibleContexts, NamedFieldPuns, ScopedTypeVariables #-}++-- | Translation from GHC Core to the Tip IR+module Tip.CoreToTip where++import Prelude hiding (log)++import Control.Applicative+import Control.Monad.Error+import Control.Monad.Reader+import Control.Monad.Writer++#if __GLASGOW_HASKELL__ >= 708+import Data.ByteString (unpack)+import Data.Char (chr)+#else+import FastString (unpackFS)+#endif++import Tip.Core as Tip++import CoreUtils as C+import CoreSyn as C++import Data.Char (ord)+import Data.List ((\\),union)+import Data.Maybe (fromMaybe)++import PrimOp++import Unique+import DataCon+import Literal+import Var hiding (Id)+import TyCon hiding (data_cons)+import Type as C+import GHC (dataConType)++import TysWiredIn+import PrelNames (gHC_REAL)++import qualified TysPrim+import qualified PrelNames++import IdInfo+import Name++import Outputable++import Tip.GHCUtils (showOutputable,rmClass)+import Tip.DataConPattern+import Tip.TyAppBeta+import Tip.Id+import Tip.Utils (usort)++-- | The binders in our translated expressions.+--+--   We cannot use 'Var'/'Id' because 'TyCon's do not have them,+--   and 'DataCon's does not necessarily have a unique.+--   'Name's have, just as 'Var'/'Id', a 'Unique' in them.+--+--   The types need to be remembered so we used typed+--+--   The list of var is the variables in scope++type TM = ReaderT [Var] (Either String)++type TMW = WriterT [Function Id] TM++runTM :: TM a -> Either String a+runTM m = runReaderT m []++msgUnsupportedLiteral l    = "Unsupported literal: " ++ showOutputable l+msgIllegalType t           = "Illegal type: " ++ showOutputable t+msgTypeApplicationToExpr e = "Type application to expression: " ++ showOutputable e+msgTypeExpr e              = "Type expression: " ++ showOutputable e+msgCoercionExpr e          = "Coercion expression: " ++ showOutputable e+msgCastExpr e              = "Cast expression: " ++ showOutputable e+msgHigherRankType v t      = showOutputable v ++ " has a higher-rank type: " ++ showOutputable t+msgUnificationError t tvs dc e mu =+       "Unification error on " ++ showOutputable t+       ++ "\nWhen resolving type variables " ++ showOutputable tvs+       ++ " for constructor " ++ showOutputable dc +++       (case mu of+           Just u -> "\nObtained unifier: " ++ showOutputable u+           Nothing -> " without unifier")+       ++ "\nOriginating from expression: " ++ showOutputable e+msgNonVanillaDataCon dc tc =+       "Data constructor " ++ showOutputable dc ++++       " from type constructor " ++ showOutputable tc +++       " is not Haskell 98!"+msgNotAlgebraicTyCon tc =+       "Type constructor " ++ showOutputable tc ++ " is not algebraic!"+msgFail s = "Internal failure: " ++ s++trTyCon :: TyCon -> Either String (Datatype Id)+trTyCon tc = do+    unless (isAlgTyCon tc) (throwError (msgNotAlgebraicTyCon tc))+    dcs <- mapM tr_dc (tyConDataCons tc)+    return Datatype+        { data_name = idFromTyCon tc+        , data_tvs  = map idFromTyVar tc_tvs+        , data_cons = dcs+        }+  where+    tc_tvs = tyConTyVars tc++    tr_dc dc = do+        unless+            (isVanillaDataCon dc)+            (throwError (msgNonVanillaDataCon dc tc))+        let dc_tys = dataConInstArgTys dc (map mkTyVarTy tc_tvs)+        ts <- mapM trType dc_tys+        let cn = idFromDataCon dc+        return Constructor+            { con_name    = cn+            , con_discrim = Discrim cn+            , con_args    = map (Project cn) [0..] `zip` ts+            }++-- | Translate a definition+trDefn :: Var -> CoreExpr -> TM [Function Id]+trDefn v e = do+    let (tvs,ty) = splitForAllTys (C.exprType e)+    ty' <- lift (trType ty)+    let (tvs',body) = collectTyBinders e+    when (tvs /= tvs') (fail "Type variables do not match in type and lambda!")+    (body',fns) <- runWriterT (trExpr (tyAppBeta body))+    let v' = idFromVar v+    let rn x | x `elem` map func_name fns = Just (x `LiftedFrom` v')+             | otherwise                  = Nothing+    return $ fmap (rename rn) $ [Function+        { func_name    = v'+        , func_tvs     = map idFromTyVar tvs+        , func_args    = []+        , func_res     = ty'+        , func_body    = body'+        }] ++ fns++rename :: (Functor f,Ord a) => (a -> Maybe a) -> f a -> f a+rename lk = fmap (\ x -> fromMaybe x (lk x))++log :: Outputable a => a -> b -> b+log x = trace (showOutputable x)+-- | Translating variables+--+-- Need to conflate worker and wrapper data constructors otherwise+-- they might differ from case alternatives+-- (example: created tuples in partition's where clause)+-- It is unclear what disasters this might bring.+trVar :: Var -> [Tip.Type Id] -> TMW (Tip.Expr Id)+trVar x [] | x == trueDataConId  = return (bool True)+trVar x [] | x == falseDataConId = return (bool False)+trVar x []+  | nameModule_maybe (Var.varName x) == Just gHC_REAL+  , Just bu <- case getOccString x of+                "div" -> Just IntDiv+                "mod" -> Just IntMod+  = return+      $ Tip.Lam [ghcInt 0]+      $ Tip.Lam [ghcInt 1]+      $ Match (Lcl (ghcInt 0))+      [ Tip.Case (intPat [int 2])+      $ Match (Lcl (ghcInt 1))+      [ Tip.Case (intPat [int 3])+      $ Gbl iHash :@: [Builtin bu :@: [Lcl (int 2),Lcl (int 3)]]+      ]]+ where+  ghcInt i = Local (Eta i) ghcIntType+  ghcIntType = Tip.TyCon (idFromTyCon intTyCon) []+  int i = Local (Eta i) intType+  iHash = trConstructor intDataCon (Tip.PolyType [] [intType] ghcIntType) []+  intPat = ConPat iHash+trVar x _+  | tip:_ <- [ tip+             | (ghc,tip) <- primops+             , getUnique (getOccName x) == getUnique (primOpOcc ghc)+             ] = return tip+trVar x tys = do+    ty <- ll (trPolyType (varType x))+    lcl <- asks (x `elem`)+    if lcl+        then case ty of+                PolyType [] [] tr -> return (Lcl (Local (idFromVar x) tr))+                _                 -> fail ("Local identifier " ++ showOutputable x +++                                           " with forall-type: " ++ showOutputable (varType x))+        else return $ case idDetails x of+                DataConWorkId dc -> abstract $ trConstructor dc ty tys+                DataConWrapId dc -> abstract $ trConstructor dc ty tys+                _                -> Gbl (Global (idFromVar x) ty tys) :@: []+    where+      abstract gbl = foldr lam body etas+        where+          body = Gbl gbl :@: map Lcl etas+          etas = zipWith (Local . Eta) [0..] args+          (args, _) = applyPolyType (gbl_type gbl) tys+          lam lcl body = Tip.Lam [lcl] body++trPattern :: DataCon -> PolyType Id -> [Tip.Type Id] -> [Tip.Local Id] -> Pattern Id+trPattern dc _ [] []+  | dc == trueDataCon  = LitPat (Bool True)+  | dc == falseDataCon = LitPat (Bool False)+trPattern dc ty tys args = ConPat (trConstructor dc ty tys) args++trConstructor :: DataCon -> PolyType Id -> [Tip.Type Id] -> Global Id+trConstructor dc ty tys = Global (idFromName $ dataConName dc) (uncurryTy ty) tys+  where+    uncurryTy ty@PolyType{polytype_res = args :=>: res} =+      ty' { polytype_args = args ++ polytype_args ty' }+      where+        ty' = uncurryTy ty { polytype_res = res }+    uncurryTy ty = ty++ll :: Either String a -> TMW a+ll = lift . lift++errorType :: PolyType Id+errorType = PolyType [Eta 0] [] (TyVar (Eta 0))++errorCall :: Tip.Type Id -> Tip.Expr Id+errorCall ty = Gbl (Global Error errorType [ty]) :@: []++-- | Translating expressions+--+-- GHC Core allows application of types to arbitrary expressions,+-- but this language only allows application of types to variables.+--+-- The type variables applied to constructors in case patterns is+-- not immediately available in GHC Core, so this has to be reconstructed.+trExpr :: CoreExpr -> TMW (Tip.Expr Id)+trExpr e0 = case collectTypeArgs e0 of+    (C.App (C.App (C.Var patError) (C.Type ty)) (C.Lit _), _)+      | varUnique patError == PrelNames.patErrorIdKey -> do+          t <- ll (trType ty)+          return (errorCall t)+    (C.Var x, tys) -> mapM (ll . trType) tys >>= trVar x+    (_, _:_) -> throw (msgTypeApplicationToExpr e0)+    (C.Lit l, _) -> literal <$> trLit l++    (C.App e1 e2, _) -> (\ x y -> Builtin At :@: [x,y]) <$> trExpr e1 <*> trExpr e2++    (C.Lam x e, _) -> do+        t <- ll (trType (varType x))+        e' <- local (x:) (trExpr e)+        return (Tip.Lam [Local (idFromVar x) t] e')++    (C.Let (C.NonRec v b) e, _) -> do+        vt <- ll (trType (varType v))+        b' <- trExpr b+        e' <- local (v:) (trExpr e)+        return (Tip.Let (Local (idFromVar v) vt) b' e')++    (C.Let (C.Rec vses) b, _) -> do+        fns <- concat <$> mapM (lift . uncurry trDefn) vses+        body <- trExpr b+        let free_vars = usort $ concatMap fn_free_vars fns+        let free_tvs  = usort $ concatMap fn_free_tvs fns++        -- now each function in fns gets these fvs and vars and prepended+        let map_body = su_globals+                [ (func_name,\ ts es -> Gbl (Global func_name new_type (map TyVar free_tvs ++ ts)) :@: (map Lcl free_vars ++ es))+                | fn@Function{func_name} <- fns+                , let PolyType tvs args res = funcType fn+                      new_type = PolyType (free_tvs ++ tvs) (map lcl_type free_vars ++ args) res+                ]++        tell [ Function func_name (free_tvs ++ func_tvs) (free_vars ++ func_args) func_res (map_body func_body)+             | Function{..} <- fns+             ]++        return (map_body body)+      where+        fn_free_vars Function{func_args,func_body} = free func_body \\ func_args+        fn_free_tvs fn@Function{func_body} =+            (freeTyVars func_body `union` tyVars (args :=>: res)) \\ tvs+          where+            PolyType tvs args res = funcType fn++        su_globals :: [(Id,[Tip.Type Id] -> [Tip.Expr Id] -> Tip.Expr Id)] -> Tip.Expr Id -> Tip.Expr Id+        su_globals xks = transformExpr $ \ e0 -> case e0 of+            Gbl (Global y _ ts) :@: es | Just k <- lookup y xks -> k ts es+            _                                                   -> e0++    (C.Case e x _ alts, _) -> do++        e' <- trExpr e++        let t = C.exprType e++        t' <- ll (trType t)++        let tr_alt :: CoreAlt -> TMW (Tip.Case Id)+            tr_alt alt = case alt of+                (DEFAULT   ,[],rhs) -> Tip.Case Default <$> trExpr rhs++                (DataAlt dc,bs,rhs) -> do++                    let (dc_tvs,mu) = dcAppliedTo t dc+                        unif_err    = msgUnificationError t dc_tvs dc e0++                    case mu of+                        Just u -> case mapM (lookupTyVar u) dc_tvs of+                            Just tys -> do+                                tys' <- mapM (ll . trType) tys+                                bs' <- forM bs $ \ b ->+                                    (,) (idFromVar b) <$> ll (trType (varType b))+                                rhs' <- local (bs++) (trExpr rhs)+                                dct <- ll (trPolyType (dataConType dc))+                                return $ Tip.Case+                                    (trPattern dc dct tys' (map (uncurry Local) bs'))+                                    rhs'+                            Nothing -> throw (unif_err (Just u))+                        Nothing -> throw (unif_err Nothing)++                (LitAlt lit,[],rhs) -> do++                    -- let TyCon v [] = t'+                    lit' <- trLit lit+                    rhs' <- trExpr rhs+                    return (Tip.Case (LitPat lit') rhs')++                _ -> fail "Default or LitAlt with variable bindings"++        let scrut = Local (idFromVar x) t'++        Tip.Let scrut e' . Match (Lcl scrut) <$> local (x:) (mapM tr_alt alts)++    (C.Tick _ e, _) -> trExpr e+    (C.Type{}, _) -> throw (msgTypeExpr e0)+    (C.Coercion{}, _) -> throw (msgCoercionExpr e0)+    (C.Cast{}, _) -> throw (msgCastExpr e0)+    -- TODO:+    --     Do we need to do something about newtype casts?++collectTypeArgs :: CoreExpr -> (CoreExpr, [C.Type])+collectTypeArgs (C.App e (Type t)) = (e', tys ++ [t])+  where+    (e', tys) = collectTypeArgs e+collectTypeArgs e = (e, [])++trLit :: Literal -> TMW Lit+trLit (LitInteger x _type) = return (Int x)+trLit (MachInt x)          = return (Int x)+trLit (MachInt64 x)        = return (Int x)+trLit (MachChar ch)        = return (Int (toInteger (ord ch)))+#if __GLASGOW_HASKELL__ >= 708+trLit (MachStr s) = return (String (map (chr . fromInteger . toInteger) (unpack s)))+#else+trLit (MachStr s) = return (String (unpackFS s))+#endif+trLit l           = throw (msgUnsupportedLiteral l)++trPolyType :: C.Type -> Either String (Tip.PolyType Id)+trPolyType t0 =+    let (tv,t) = splitForAllTys (expandTypeSynonyms t0)+    in  PolyType (map idFromTyVar tv) [] <$> trType (rmClass t)++throw :: String -> TMW a+throw = ll . throwError++essentiallyInteger :: TyCon -> Bool+essentiallyInteger tc = tc == TysPrim.intPrimTyCon {-+                      || tc == TysPrim.charPrimTyCon+                      || tyConUnique tc == PrelNames.integerTyConKey+                      -}+++trType :: C.Type -> Either String (Tip.Type Id)+trType = go . expandTypeSynonyms+  where+    go t0+        | Just (t1,t2) <- splitFunTy_maybe t0    = (\ x y -> [x] :=>: y) <$> go t1 <*> go t2+        | Just (tc,[]) <- splitTyConApp_maybe t0, essentiallyInteger tc = return intType+        | Just (tc,[]) <- splitTyConApp_maybe t0, tc == boolTyCon       = return boolType+        | Just (tc,ts) <- splitTyConApp_maybe t0 = TyCon (idFromTyCon tc) <$> mapM go ts+        | Just tv <- getTyVar_maybe t0           = return (TyVar (idFromTyVar tv))+        | otherwise                              = throwError (msgIllegalType t0)+
+ src/Tip/DataConPattern.hs view
@@ -0,0 +1,16 @@++module Tip.DataConPattern where++import DataCon+import Var+import Type++import Unify++dcAppliedTo :: Type -> DataCon -> ([TyVar],Maybe TvSubst)+dcAppliedTo t dc = (dc_tvs,mu)+  where+    dc_tvs = dataConUnivTyVars dc+    res_ty = dataConOrigResTy dc+    mu = tcUnifyTys (const BindMe) [res_ty] [t]+
+ src/Tip/Dicts.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE PatternGuards, TypeSynonymInstances, FlexibleInstances, ViewPatterns, ExplicitForAll #-}+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleContexts, NamedFieldPuns #-}+{-# LANGUAGE CPP #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Tip.Dicts (inlineDicts,maybeUnfolding) where++import Tip.GHCUtils (showOutputable)+#if __GLASGOW_HASKELL__ >= 708+import DynFlags (unsafeGlobalDynFlags)+#endif+import CoreSyn+import CoreUtils()+import IdInfo+import Id+import Var+import Data.List (elemIndex)+import VarEnv (emptyInScopeSet)++import Data.Generics.Geniplate++import Outputable+import Type+import Literal+import Coercion++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+    CoreUnfolding{uf_tmpl} -> Just uf_tmpl+    _                      -> Nothing+  where+    ri = realIdUnfolding v++++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+#if __GLASGOW_HASKELL__ >= 708+        | [try] <- [ try | BuiltinRule _ _ 2 try <- idCoreRules f ]+        , Just e <- try unsafeGlobalDynFlags (emptyInScopeSet,realIdUnfolding) f [Type t,Var d]+        -> e+#endif+        | Just cl <- isClassOpId_maybe f+        , DFunId{} <- idDetails d+        -> case maybeUnfolding f of+            Just (collectBinders -> (_,Case _ _ _ [(_,ss,Var s)]))+              | Just i <- elemIndex s ss -> case realIdUnfolding d of+#if __GLASGOW_HASKELL__ == 706+                DFunUnfolding _ _ es -> drop (length es - length ss) (dfunArgExprs es) !! i+#else+                DFunUnfolding _ _ es -> drop (length es - length ss) es !! i+#endif+                CoreUnfolding{uf_tmpl} ->+                    let (_,es) = collectArgs uf_tmpl+                    in  drop (length es - length ss) es !! i+                x -> e0 -- error $ showOutputable (e0,x)+            x -> e0 -- error $ showOutputable (e0,x)+    _ -> e0++
+ src/Tip/FreeTyCons.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE PatternGuards #-}+module Tip.FreeTyCons (bindsTyCons,bindsTyCons',varTyCons,tyTyCons) where++import CoreSyn+import CoreUtils (exprType)+import DataCon+import TyCon+import Id+import Type+import Var++import Data.Set (Set)+import qualified Data.Set as S++bindsTyCons :: [CoreBind] -> [TyCon]+bindsTyCons = S.toList . S.unions . map bindTyCons . flattenBinds++bindsTyCons' :: [(Var,CoreExpr)] -> [TyCon]+bindsTyCons' = S.toList . S.unions . map bindTyCons++bindTyCons :: (Var,CoreExpr) -> Set TyCon+bindTyCons (v,e) = S.union (exprTyCons e) (varTyCons v)++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++-- | 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+
+ src/Tip/GHCScope.hs view
@@ -0,0 +1,49 @@+{-# 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+
+ src/Tip/GHCUtils.hs view
@@ -0,0 +1,65 @@+{-# LANGUAGE CPP,PatternGuards #-}+module Tip.GHCUtils where++import Outputable++import Var (varName)+import Name (Name,getOccString)+import DataCon+import Id+import TyCon+import Type++#if __GLASGOW_HASKELL__ >= 708+import DynFlags (unsafeGlobalDynFlags)+#elif __GLASGOW_HASKELL__ >= 706+import DynFlags (tracingDynFlags)+#endif++portableShowSDoc :: SDoc -> String+#if __GLASGOW_HASKELL__ >= 708+portableShowSDoc = showSDoc unsafeGlobalDynFlags+#elif __GLASGOW_HASKELL__ >= 706+portableShowSDoc = showSDoc tracingDynFlags+#else+portableShowSDoc = showSDoc+#endif++-- | Shows something outputable+showOutputable :: Outputable a => a -> String+showOutputable = portableShowSDoc . ppr++varToString :: Var -> String+varToString = nameToString . varName++nameToString :: Name -> String+nameToString = getOccString++-- | Is this Id a "constructor" to a newtype?+--   This is the only way I have found to do it...+isNewtypeConId :: Id -> Bool+isNewtypeConId i+    | Just dc <- isDataConId_maybe i = isNewTyCon (dataConTyCon dc)+    | otherwise = False++-- | Is this Id a data or newtype constructor?+--+--   Note: cannot run isDataConWorkId on things that aren't isId,+--         then we get a panic from idDetails.+--+--         (mainly from type variables)+isDataConId :: Id -> Bool+isDataConId v = isId v && (isConLikeId v || isNewtypeConId v)++-- Removes class constraints+rmClass :: Type -> Type+rmClass ty = case splitFunTy_maybe ty of+    Just (t1,t2) | isPredTy t1 -> rmClass t2+    _ -> ty++-- Has class constraint?+hasClass :: Type -> Bool+hasClass ty = case splitFunTy_maybe (snd (splitForAllTys ty)) of+    Just (t1,t2) -> isPredTy t1+    _            -> False+
+ src/Tip/HaskellFrontend.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE RecordWildCards, DisambiguateRecordFields, NamedFieldPuns #-}+-- | The Haskell frontend to Tip+module Tip.HaskellFrontend(readHaskellFile,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 Tip.Id+import Tip.Params+import Tip.ParseDSL+import Tip.Property+import Tip.RemoveDefault+import Tip.Unfoldings+import Tip.Uniquify+import Tip.GHCUtils+import Tip.Pretty++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 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++-- | Transforms a Haskell file to a Tip Theory, crashing if unsuccessful+readHaskellFile :: Params -> IO (Theory Id)+readHaskellFile params@Params{..} = do++    -- whenFlag params PrintParams $ putStrLn (ppShow params)++    -- maybe (return ()) setCurrentDirectory directory++    prop_ids <- compileHaskellFile params++    let vars = filterVarSet (not . varInTip) $+               unionVarSets (map (transCalls Without) prop_ids)++    us0 <- mkSplitUniqSupply 'h'++    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]+            ]++        tcs = filter (\ x -> isAlgTyCon x && not (nameInTip (tyConName x)) && not (isClassTyCon x))+                     (delete boolTyCon (bindsTyCons' binds))++    when (PrintCore `elem` flags) $ do+        putStrLn "Tip.HaskellFrontend, PrintInitialTip:"+        putStrLn (showOutputable binds)++    let tip_data =+          [ case trTyCon tc of+              Right tc' -> tc'+              Left err -> error $ showOutputable tc ++ ": " ++ err+          | tc <- tcs+          ]++    let tip_fns0 = concat+          [ case runTM (trDefn v e) of+              Right fn -> fn+              Left err -> error $ showOutputable v ++ ": " ++ err+          | (v,e) <- binds+          ]++        -- Now, split these into properties and non-properties+    let (prop_fns,tip_fns) = partition (isPropType . func_res) tip_fns0++        tip_props = either error id (mapM trProperty prop_fns)++        thy = Theory tip_data [] [Signature Error errorType] tip_fns tip_props++    when (PrintInitialTip `elem` flags) $ do+        putStrLn "Tip.HaskellFrontend, PrintInitialTip:"+        putStrLn (ppRender thy)++    return thy+
+ src/Tip/Id.hs view
@@ -0,0 +1,170 @@+{-# LANGUAGE PatternGuards,StandaloneDeriving,CPP #-}+module Tip.Id where++import Tip.Pretty+import Tip.Core++import Text.PrettyPrint (text)++import Name hiding (varName)+import OccName (occNameString)+-- import BasicTypes (TupleSort(..))+import PrelNames+import Tip.GHCUtils+import Var (Var,varName,idDetails,TyVar,tyVarName)+import IdInfo (IdDetails(..))+import TyCon (tyConName,TyCon)+import DataCon (dataConName,DataCon)+import Data.Char (toUpper)+import PrimOp++import TysWiredIn (trueDataCon,falseDataCon,boolTyCon)++idFromName :: Name -> Id+idFromName nm = GHCOrigin nm++idFromDataCon :: DataCon -> Id+idFromDataCon = idFromName . dataConName++idFromVar :: Var -> Id+idFromVar i = case idDetails i of+    DataConWorkId dc -> idFromDataCon dc+    DataConWrapId dc -> idFromDataCon dc+    _                -> idFromName (varName i)++idFromTyVar :: TyVar -> Id+idFromTyVar = idFromName . tyVarName++idFromTyCon :: TyCon -> Id+idFromTyCon tc = idFromName (tyConName tc)++tryGetGHCName :: Id -> Maybe Name+tryGetGHCName (GHCOrigin nm) = Just nm+tryGetGHCName _              = Nothing++-- | A representation of identifiers that come from GHC.+--+-- The 'PrettyVar' instance is one way to print the names.+data Id+    = GHCOrigin Name+    | Id `LiftedFrom` Id+    | Eta Int+    | Discrim Id+    | Project Id Int+    | Error+  deriving (Eq,Ord)++instance Show Id where+    show (GHCOrigin n)      = show (showOutputable n)+    show (Eta n)            = "eta" ++ show n+    show (Discrim c)        = "is-" ++ show c+    show (Project c i)      = show c ++ "_" ++ show i+    show (i `LiftedFrom` j) = show i ++ " `LiftedFrom` " ++ show j+    show Error              = "error"++instance PrettyVar Id where+    varStr = ppId++ppId :: Id -> String+ppId (GHCOrigin nm) = ppName nm+ppId (Eta n)        = "eta" ++ show n+ppId (Discrim c)    = "is-" ++ ppId c+ppId ((i `LiftedFrom` j) `LiftedFrom` k) = ppId (i `LiftedFrom` (j `LiftedFrom` k))+ppId (i `LiftedFrom` j)+  | Just nm <- tryGetGHCName i, isSystemName nm    = ppId j+  | ppId i /= ppId j && "prop_" /= take 5 (ppId j) = ppId j ++ "_" ++ ppId i+  | otherwise                                      = ppId i+ppId (Project c i)  = case (i,ppId c) of+                        (0,"Pair") -> "first"+                        (1,"Pair") -> "second"+                        (0,"cons") -> "head"+                        (1,"cons") -> "tail"+                        (0,"S")    -> "p"+                        (0,"Succ") -> "pred"+                        _          -> ppId c ++ "_" ++ show i+ppId Error = "error"++ppName :: Name -> String+ppName nm+    | k == listTyConKey      = "list"+    | k == nilDataConKey     = "nil"+    | k == consDataConKey    = "cons"+    | k == unitTyConKey      = "Unit"+    | k == genUnitDataConKey = "tt"+    | isSystemName nm        = "x"+    | otherwise = case getOccString nm of+        x | take 2 x == "ds"  -> "x"+        x | take 3 x == "ipv" -> "x"+        "(,)"  -> "Pair"+        "(,,)" -> "Triple"+        "+"   -> "plus"+        "-"   -> "minus"+        "/"   -> "div"+        "*"   -> "mult"+        "^"   -> "pow"+        "++"  -> "append"+        ">>=" -> "bind"+        "=<<" -> "dnib"+        ">=>" -> "dot_monadic"+        "<=<" -> "monadic_dot"+        "<*>" -> "ap"+        "<$>" -> "fmap"+        ">>"  -> "then"+        "||"  -> "or"+        "&&"  -> "and"+        "."   -> "dot"+        "=="  -> "equal"+        "/="  -> "unequal"+        ">"   -> "gt"+        ">="  -> "ge"+        "<"   -> "lt"+        "<="  -> "le"+        "$"   -> "apply"+        "!!"  -> "index"+        "\\\\" -> "difference"+        s     -> s+  where+    k = getUnique nm++primops :: [(PrimOp,Expr Id)]+primops =+  [ (ghc_op,Lam [int 0] (Lam [int 1] (Builtin tip_id :@: [Lcl (int 0),Lcl (int 1)])))+  | (ghc_op,tip_id) <-+    [ (IntAddOp, IntAdd)+    , (IntSubOp, IntSub)+    , (IntMulOp, IntMul)+    ]+  ] +++#if __GLASGOW_HASKELL__ <= 706+  [ (ghc_op,Lam [int 0] (Lam [int 1] (Builtin tip_id :@: [Lcl (int 0),Lcl (int 1)])))+  | (ghc_op,tip_id) <-+    [ (IntEqOp, Equal)+    , (IntNeOp, Distinct)+    , (IntGtOp, IntGt)+    , (IntGeOp, IntGe)+    , (IntLtOp, IntLt)+    , (IntLeOp, IntLe)+    ]+  ]+#else+  [ (ghc_op,Lam [int 0] (Lam [int 1]+              (makeIf (Builtin tip_id :@: [Lcl (int 0),Lcl (int 1)])+                      (literal (Int 1)) (literal (Int 0)))))+  | (ghc_op,tip_id) <-+    [ (IntEqOp, Equal)+    , (IntNeOp, Distinct)+    , (IntGtOp, IntGt)+    , (IntGeOp, IntGe)+    , (IntLtOp, IntLt)+    , (IntLeOp, IntLe)+    ]+  ] +++  [ (TagToEnumOp,Lam [int 0] (Match (Lcl (int 0))+                                [ Case Default          (bool False)+                                , Case (LitPat (Int 1)) (bool True)+                                ]))+  ]+#endif+ where+  int i = Local (Eta i) intType+
+ src/Tip/Params.hs view
@@ -0,0 +1,31 @@+module Tip.Params where++-- | Parameters+data Params = Params+  { file        :: FilePath+  -- ^ File to process+  , include     :: [FilePath]+  -- ^ Directories to include+  , flags       :: [DebugFlags]+  -- ^ Debugging flags+  , only        :: [String]+  -- ^ Only consider these properties+  , extra       :: [String]+  -- ^ Also translate these functions and its transitive dependencies+  }+  deriving Show++-- | Default parameters, given the name of the file to process+defaultParams :: FilePath -> Params+defaultParams fp = Params+  { file = fp+  , include = []+  , flags = []+  , only = []+  , extra = []+  }++-- | Debugging flags+data DebugFlags = PrintCore | PrintProps | PrintExtraIds | PrintInitialTip+  deriving (Eq,Show)+
+ src/Tip/ParseDSL.hs view
@@ -0,0 +1,65 @@+{-# LANGUAGE ViewPatterns #-}+module Tip.ParseDSL where++import Tip.GHCUtils+import Tip.Id+import Tip.Core+import qualified Tip.CoreToTip as CTT++import qualified Data.Foldable as F++import Name hiding (varName)+import Data.List++import Var hiding (Id,isId)+import TyCon (TyCon)++import Module++nameInTip :: Name -> Bool+nameInTip = F.any (\ n -> moduleNameString (moduleName n) == "Tip") . nameModule_maybe++varInTip :: Var -> Bool+varInTip = nameInTip . varName++idInTip :: Id -> Bool+idInTip = F.any nameInTip . tryGetGHCName++isId :: String -> Id -> Bool+isId s i = F.any (nameIs s) (tryGetGHCName i)++oneOf :: String -> String -> Id -> Bool+oneOf s1 s2 i = any (`isId` i) [s1,s2]++nameIs :: String -> Name -> Bool+nameIs s n = nameInTip n && s == occNameString (nameOccName n)++varIs :: String -> Var -> Bool+varIs s v = nameIs s (varName v)++isPropType :: Type Id -> Bool+isPropType = goo 0 . res+  where+  go = goo 1+  goo i (BuiltinType Boolean) = i > 0+  goo i (TyCon tc [t1]) =  isId "Equality" tc || (isId "Neg" tc && go t1)+  goo i (TyCon tc [t1,t2]) =+    let ok xs = or [ isId s tc | s <- xs ]+    in     (ok ["And","Or",":=>:"] && go t1 && go t2)+        || (ok ["Forall","Exists"] && go t2)+  goo i _ = False++  res (_ :=>: r) = res r+  res r          = r++isPropTyCon :: Var -> Bool+isPropTyCon v =+    or [ varIs s v+       | s <- ["Equality","Neg","And","Or",":=>:","Forall","Exists"]+       ]++varWithPropType :: Var -> Bool+varWithPropType x = case CTT.trPolyType (varType x) of+    Right (PolyType _ _ t) -> isPropType t+    _                      -> False+
+ src/Tip/Property.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE RecordWildCards, PatternGuards, ViewPatterns #-}+module Tip.Property where++import Tip.Core+import Tip.Id+import Tip.Pretty+import Tip.Pretty.SMT++import Tip.ParseDSL+import Tip.GHCUtils++import Control.Monad.Error+import Control.Applicative+import Data.Foldable (Foldable)+import Data.List (intercalate,union)+import Data.Map (Map)+import Data.Maybe (mapMaybe)+import Data.Traversable (Traversable)+import qualified Data.Map as M+-- import Text.PrettyPrint hiding (comma)++import Var (Var)+import TysWiredIn (trueDataCon,falseDataCon,boolTyCon)+-- import DataCon (dataConName)++-- | Translates a property that has been translated to a simple function earlier+trProperty :: Function Id -> Either String (Formula Id)+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))+  where+    unLam (Lam xs e) = let (ys,e') = unLam e in (xs ++ ys,e')+    unLam e          = ([],e)++-- | Tries to "parse" a property in the simple expression format+parseProperty :: Expr Id -> Either String (Expr Id)+parseProperty = goo 0+  where+  go = goo 1+  goo i e0@(projAt -> Just (projGlobal -> Just x,Lam bs e))++      | isId "forAll" x || isId "Forall" x = mkQuant Forall bs <$> go e++      | isId "exists" x || isId "Exists" x = mkQuant Exists bs <$> go e++  goo i e0@(projAt -> Just (projGlobal -> Just x,e))++      | isId "bool" x = return e++      | isId "Neg" x || isId "neg" x = neg <$> go e++  goo i e0@(projAt -> Just (projAt -> Just (projGlobal -> Just x,e1),e2))++      | isId "===" x || isId ":=:" x = return (e1 === e2)++      | isId "=/=" x                 = return (e1 =/= e2)++      | isId "==>" x || isId "Given" x = (==>) <$> go e1 <*> go e2++      | isId ".&&." x || isId "And" x  = (/\) <$> go e1 <*> go e2++      | isId ".||." x || isId "Or" x   = (\/) <$> go e1 <*> go e2++  goo i e0 | i > 0 && exprType e0 == boolType = return e0++  goo i e0 = throwError $ "Cannot parse property: " ++ ppRender e0+
+ src/Tip/RemoveDefault.hs view
@@ -0,0 +1,150 @@+{-# LANGUAGE ScopedTypeVariables, PackageImports #-}+{-++    Annoyances with the Default branch:++        * Functions that should be equal are not, such as f and g here:++            f x = case x of+                True -> e+                _    -> e'++            g x = case x of+                True  -> e+                False -> e'++        * GHC Core likes to recase on a variable that is already known, such as here:++            h x = case x of+                True -> True+                _ -> case x of+                    False -> False+                    _ -> undefined++          The call to undefined can never be reached here. Such cases should be+          removed. It also lead to a problem in the contracts checker:++          The last branch to BAD will never happen, but the alternative+          was translated to:++             ! [X] : ((X != True & X != False & X != UNR & X != BAD) => h(X) = BAD)++          I.e. for some untyped point *, we get h(*) = BAD, which is bad+          because now the true contract h ::: CF --> CF is satisfiable.+          Disaster!++          By unrolling all constructors, we get this:++              f = \ x -> case x of+                  True -> True+                  False -> case x of+                      False -> False+                      True -> BAD++          Now, x can be inlined by known-case.++    We need to do this in a m monad to put some variables in the+    bound fields of alternatives.++    TODO: We currently look at some data constructor's type constructor,+    which means we can get a problem if we have++        case e of { _ -> e' },++    we could check the type of e instead. If it is a type constructor+    with data constructors, we could unroll it.++-}+module Tip.RemoveDefault where++import Tip.DataConPattern+import Tip.GHCUtils++import CoreSyn+import CoreUtils hiding (findAlt)+import DataCon+import FastString+import TyCon+import Type+import Unique+import UniqSupply+import Id++import Control.Monad+import Control.Applicative++removeDefaults :: (Applicative m,MonadUnique m) => [CoreBind] -> m [CoreBind]+removeDefaults = mapM rmdBind++rmdBind :: (Applicative m,MonadUnique m) => CoreBind -> m CoreBind+rmdBind (NonRec f e) = NonRec f <$> rmdExpr e+rmdBind (Rec fses)   = Rec <$> mapM (\ (f,e) -> (,) f <$> rmdExpr e) fses++rmdExpr :: (Applicative m,MonadUnique m) => CoreExpr -> m CoreExpr+rmdExpr e0 = case e0 of+    App e1 e2       -> App <$> rmdExpr e1 <*> rmdExpr e2+    Lam x e         -> Lam x <$> rmdExpr e+    Let b e         -> Let <$> rmdBind b <*> rmdExpr e+    Case s t w alts -> Case <$> rmdExpr s <.> t <.> w+                            <*> (mapM rmdAlt <=< unrollDefault (exprType s)) alts+    Cast e c        -> Cast <$> rmdExpr e <.> c+    Tick t e        -> Tick t <$> rmdExpr e++    Type{}          -> return e0+    Var{}           -> return e0+    Lit{}           -> return e0+    Coercion{}      -> return e0++rmdAlt :: (Applicative m,MonadUnique m) => CoreAlt -> m CoreAlt+rmdAlt (ac,bs,rhs) = (,,) ac bs <$> rmdExpr rhs++infixl 4 <.>+(<.>) :: Applicative f => f (a -> b) -> a -> f b+f <.> x = f <*> pure x++unrollDefault :: forall m . (Applicative m,MonadUnique m) => Type -> [CoreAlt] -> m [CoreAlt]+unrollDefault t alts0 = case findDefault alts0 of+    (alts,Just def_rhs) -> case alts of+        (DataAlt dc,_,_):_ | missing (dataConTyCon dc) alts <= 1 -> unroll (dataConTyCon dc) alts def_rhs+        (LitAlt _  ,_,_):_ -> return alts0+        (DEFAULT   ,_,_):_ -> error "RemoveDefault.unrollDefault: duplicate DEFAULT"+        _                  -> return alts0+            -- only DEFAULT, this can be remedied by looking at the TyCon from+            -- the case scrutinee expression's type+    (alts,_)      -> return alts+  where+    missing :: TyCon -> [CoreAlt] -> Int+    missing ty_con alts = case tyConDataCons_maybe ty_con of+        Just dcs -> sum [ 1 | Nothing <- map (findAlt alts) dcs ]+        Nothing  -> error "RemoveDefault.unrollDefault: non-data TyCon?"++    unroll :: TyCon -> [CoreAlt] -> CoreExpr -> m [CoreAlt]+    unroll ty_con alts rhs = case tyConDataCons_maybe ty_con of+        Just dcs -> forM dcs $ \ dc ->+            fromMaybeM (makeAlt t rhs dc) (findAlt alts dc)+        Nothing  -> error "RemoveDefault.unrollDefault: non-data TyCon?"+            -- This could be remedied by just returning alts here,+            -- but it would be interesting what this ty_con really is,+            -- maybe we can do something better++findAlt :: [CoreAlt] -> DataCon -> Maybe CoreAlt+findAlt (alt@(DataAlt dc',_,_):_) dc | dc' == dc = Just alt+findAlt (_:alts) dc = findAlt alts dc+findAlt []       _  = Nothing++fromMaybeM :: (Applicative m,MonadUnique m) => Monad m => m a -> Maybe a -> m a+fromMaybeM _ (Just x) = return x+fromMaybeM m Nothing  = m++makeAlt :: (Applicative m,MonadUnique m) => Type -> CoreExpr -> DataCon -> m CoreAlt+makeAlt t rhs dc = case dcAppliedTo t dc of+    (_,Just s) -> do+        bound <- mapM (\ ty -> dummy_var (substTy s ty) <$> getUniqueM) (dataConRepArgTys dc)+        return (DataAlt dc,bound,rhs)+    _ -> error $ "RemoveDefault.makeAlt unification error:"+                 ++ "\n\t" ++ showOutputable t+                 ++ "\n\t" ++ showOutputable dc+  where+    dummy_var :: Type -> Unique -> Var+    dummy_var ty u = mkSysLocal (fsLit "d") u ty+
+ src/Tip/TyAppBeta.hs view
@@ -0,0 +1,36 @@++-- | Beta reduction for types (applied to lambdas)+module Tip.TyAppBeta where++import Type++import CoreSyn+import qualified CoreSubst as CS+import qualified Outputable++-- | Beta reduction for types (applied to lambdas)+tyAppBeta :: CoreExpr -> CoreExpr+tyAppBeta = go+  where+    go e0 = case e0 of+        App e1 e2 -> case (go e1,go e2) of+            (Lam x e,Type t) -> reduce x e t+            (e1',e2')        -> App e1' e2'+        Lam x e         -> Lam x (go e)+        Tick tk e       -> Tick tk (go e)+        Cast e co       -> Cast (go e) co+        Case e x t alts -> Case (go e) x t [ (p,bs,go rhs) | (p,bs,rhs) <- alts ]+        Let b e         -> Let (go' b) (go e)+        Var{}           -> e0+        Lit{}           -> e0+        Coercion{}      -> e0+        Type{}          -> e0++    go' b = case b of+        NonRec v e -> NonRec v (go e)+        Rec vses   -> Rec [ (v,go e) | (v,e) <- vses ]++-- | Reduces a type variable in an expression by applying it to a type+reduce :: TyVar -> CoreExpr -> Type -> CoreExpr+reduce x e t = CS.substExpr Outputable.empty su e+  where su = CS.extendTvSubst CS.emptySubst x t
+ src/Tip/Unfoldings.hs view
@@ -0,0 +1,95 @@+{-# 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+
+ src/Tip/Uniquify.hs view
@@ -0,0 +1,67 @@+-- | One could think that every identifier in GHC Core is supposed to be Unique,+-- but this is not the case. This module cleans up this mess.+--+-- The targets are local lets that happily gets the same name, and also+-- scrutinee vars that can get the same name if they are never used.+module Tip.Uniquify where++import CoreSyn++import UniqSupply++import Var++import Control.Monad.Reader+import Control.Applicative++import Data.Map (Map)+import qualified Data.Map as M++import Data.Maybe (fromMaybe)++type UQ m a = ReaderT (Map Var Var) m a++runUQ :: (Applicative m,MonadUnique m) => UQ m a -> m a+runUQ m = runReaderT m M.empty++insertVar :: (Applicative m,MonadUnique m) => Var -> UQ m a -> UQ m a+insertVar x m = do+    my <- asks (M.lookup x)+    x' <- case my of+        Just{} -> do+            u <- lift getUniqueM+            return (setVarUnique x u)+        Nothing -> return x+    local (M.insert x x') m++insertVars :: (Applicative m,MonadUnique m) => [Var] -> UQ m a -> UQ m a+insertVars xs m = foldr insertVar m xs++lookupVar :: (Applicative m,MonadUnique m) => Var -> UQ m Var+lookupVar x = fromMaybe x <$> asks (M.lookup x)++uqBind :: (Applicative m,MonadUnique m) => CoreBind -> (CoreBind -> UQ m a) -> UQ m a+uqBind (NonRec v e) k = insertVar v (k =<< NonRec <$> lookupVar v <*> uqExpr e)+uqBind (Rec vses)   k = insertVars (map fst vses) $ k . Rec =<< sequence+    [ (,) <$> lookupVar v <*> uqExpr e | (v,e) <- vses ]++uqExpr :: (Applicative m,MonadUnique m) => CoreExpr -> UQ m CoreExpr+uqExpr e0 = case e0 of+    Var x           -> Var <$> lookupVar x+    App e1 e2       -> App <$> uqExpr e1 <*> uqExpr e2+    Let bs e        -> uqBind bs $ \ bs' -> Let bs' <$> uqExpr e+    Lam x e         -> insertVar x (Lam <$> lookupVar x <*> uqExpr e)+    Case s x t alts -> do+        s' <- uqExpr s+        insertVar x $ do+            x' <- lookupVar x+            Case s' x' t <$> mapM uqAlt alts+    Cast e c        -> (`Cast` c) <$> uqExpr e+    Tick tk e       -> Tick tk <$> uqExpr e+    Type{}          -> return e0+    Lit{}           -> return e0+    Coercion{}      -> return e0++uqAlt :: (Applicative m,MonadUnique m) => CoreAlt -> UQ m CoreAlt+uqAlt (pat,bs,e) = insertVars bs ((,,) pat <$> mapM lookupVar bs <*> uqExpr e)+
+ tip-haskell-frontend.cabal view
@@ -0,0 +1,64 @@+name:                tip-haskell-frontend+version:             0.1+license:             BSD3+license-file:        LICENSE+author:              Dan Rosén+maintainer:          danr@chalmers.se+build-type:          Simple+cabal-version:       >=1.10+description:         Convert from Haskell to Tip+synopsis:            Convert from Haskell to Tip+homepage:            http://tip-org.github.io+bug-reports:         http://github.com/tip-org/tools/issues+category:            Theorem Provers++source-repository head+  type:     git+  location: http://github.com/tip-org/tools++library+  exposed-modules:+    Tip.HaskellFrontend+    Tip+  other-modules:+    Tip.Params+    Tip.Id+    Tip.GHCUtils+    Tip.Calls+    Tip.Compile+    Tip.CoreToTip+    Tip.DataConPattern+    Tip.Dicts+    Tip.FreeTyCons+    Tip.ParseDSL+    Tip.Property+    Tip.RemoveDefault+    Tip.GHCScope+    Tip.TyAppBeta+    Tip.Unfoldings+    Tip.Uniquify+  hs-source-dirs:      src+  include-dirs:        src+  default-language:    Haskell2010+  build-depends:       base >=4 && <5,+                       ghc,+                       ghc-paths >=0.1,+                       containers >=0.4,+                       filepath >=1.3,+                       directory >=1.1,+                       pretty >=1.1,+                       mtl >=2.1,+                       bytestring >=0.9.2,+                       split >=0.2,+                       geniplate-mirror >=0.7.1,+                       tip-lib == 0.1,+                       QuickCheck >= 2.8++executable tip-ghc+  main-is:             executable/Main.hs+  default-language:    Haskell2010+  build-depends:       base,+                       tip-haskell-frontend,+                       tip-lib,+                       pretty-show,+                       pretty