-- this file contains the main driver for the core->core optimizations module E.Main(processInitialHo,processDecls,compileWholeProgram,dumpRules) where import Control.Exception import Control.Monad.Identity import Control.Monad.Reader import Control.Monad.State import Control.Monad.Writer import System.Mem import qualified Data.Map as Map import qualified Data.Set as Set import Data.List import DataConstructors import Doc.PPrint import E.Annotate(annotateDs,annotateCombs,annotateProgram) import E.E import E.Eta import E.FromHs import E.Inline import E.LambdaLift import E.LetFloat import E.Lint import E.Program import E.Rules import E.Traverse import E.TypeAnalysis import E.TypeCheck import E.Values import E.WorkerWrapper import FrontEnd.Class(augmentClassHierarchy) import FrontEnd.HsSyn import FrontEnd.KindInfer import FrontEnd.Tc.Module import FrontEnd.Warning import Grin.Show(render) import Ho.Build import Ho.Collected import Info.Types import Name.Id import Name.Name import Options import Support.CanType(getType) import Support.FreeVars import Support.TempDir import Support.Transform import Util.Gen import Util.Graph import Util.Progress import Util.SetLike as S import qualified E.CPR import qualified E.Demand as Demand(analyzeProgram) import qualified E.SSimplify as SS import qualified FlagDump as FD import qualified FlagOpts as FO import qualified Info.Info as Info import qualified Stats lamann _ nfo = return nfo letann e nfo = return (annotateArity e nfo) idann ps i nfo = return (props ps i nfo) where props :: IdMap Properties -> Id -> Info.Info -> Info.Info props ps i = case mlookup i ps of Just ps -> modifyProperties (mappend ps) Nothing -> id processInitialHo :: CollectedHo -- ^ current accumulated ho -> Ho -- ^ new ho, freshly read from file -> IO CollectedHo -- ^ final combined ho data. processInitialHo accumho aho = withStackStatus "processInitialHo" $ do let Rules rm = hoRules $ hoBuild aho newTVrs = fsts $ hoEs (hoBuild aho) (_,orphans) = spartition (\ (k,_) -> k `elem` map tvrIdent newTVrs) rm let fakeEntry = emptyComb { combRules = map ruleUpdate . concat $ values orphans } combs = fakeEntry:[combRules_s (map ruleUpdate $ findWithDefault [] (tvrIdent t) rm) (bindComb (t,e)) | (t,e) <- hoEs (hoBuild aho) ] -- extract new combinators and processed rules let choCombinators' = fromList [ (combIdent c,c) | c <- runIdentity $ annotateCombs (choVarMap accumho) (\_ -> return) letann lamann combs] nrules = map ruleUpdate . combRules $ findWithDefault emptyComb emptyId choCombinators' reRule :: Comb -> Comb reRule comb = combRules_u f comb where f rs = Data.List.union rs [ x | x <- nrules, ruleHead x == combHead comb] let choCombs = sfilter (\(k,_) -> k /= emptyId) choCombinators' return $ updateChoHo mempty { choExternalNames = choExternalNames accumho `mappend` (fromList . map tvrIdent $ newTVrs), choCombinators = choCombs `mappend` fmap reRule (choCombinators accumho), choHoMap = Map.singleton (hoModuleGroup aho) aho `mappend` choHoMap accumho } processDecls :: CollectedHo -- ^ Collected ho -> Ho -- ^ preliminary haskell object data -> TiData -- ^ front end output -> IO (CollectedHo,Ho) -- ^ (new accumulated ho, final ho for this modules) processDecls cho ho' tiData = withStackStatus "processDecls" $ do -- some useful values let ho = choHo cho -- XXX typechecker drops foreign exports! decls = tiDataDecls tiData ++ [ x | x@HsForeignExport {} <- originalDecls ] originalDecls = concat [ hsModuleDecls m | (_,m) <- tiDataModules tiData ] -- build datatables let derives = (collectDeriving originalDecls) let dataTable = toDataTable (getConstructorKinds (hoKinds $ hoTcInfo ho')) (tiAllAssumptions tiData) originalDecls (hoDataTable $ hoBuild ho) classInstances = deriveClasses (choCombinators cho) fullDataTable derives fullDataTable = dataTable `mappend` hoDataTable (hoBuild ho) wdump FD.Datatable $ putErrLn (render $ showDataTable dataTable) wdump FD.Derived $ do mapM_ print derives mapM_ (\ (v,lc) -> printCheckName'' fullDataTable v lc) classInstances -- initial program let prog = program { progDataTable = fullDataTable, progExternalNames = choExternalNames cho, progModule = head (fsts $ tiDataModules tiData) } -- Convert Haskell decls to E let allAssumps = (tiAllAssumptions tiData `mappend` hoAssumps (hoTcInfo ho)) theProps = fromList [ (toId x,y) | (x,y) <- Map.toList $ tiProps tiData] ds' <- convertDecls tiData theProps (hoClassHierarchy $ hoTcInfo ho') allAssumps fullDataTable decls processIOErrors let ds = classInstances ++ [ (v,lc) | (n,v,lc) <- ds', v `notElem` fsts classInstances ] -- Build rules from instances, specializations, and user specified rules and catalysts let augmentedClassHierarchy = hoClassHierarchy (hoTcInfo ho) `augmentClassHierarchy` hoClassHierarchy (hoTcInfo ho') instanceRules <- createInstanceRules fullDataTable augmentedClassHierarchy (ds `mappend` hoEs (hoBuild ho)) userRules <- convertRules (progModule prog) tiData (hoClassHierarchy $ hoTcInfo ho') allAssumps fullDataTable decls (nds,specializeRules) <- procAllSpecs fullDataTable (tiCheckedRules tiData) ds ds <- return $ ds ++ nds wdump FD.CoreInitial $ mapM_ (\(v,lc) -> printCheckName'' fullDataTable v lc) ds ds <- annotateDs mempty (\_ nfo -> return nfo) (\_ nfo -> return nfo) (\_ nfo -> return nfo) ds wdump FD.CoreInitial $ mapM_ (\(v,lc) -> printCheckName'' fullDataTable v lc) ds let rules@(Rules rules') = instanceRules `mappend` userRules `mappend` specializeRules dumpRules rules let seasoning = freeVars [ rs | (k,rs) <- toList rules', k `notMember` defined ] `intersection` defined defined = fromList $ map (tvrIdent . fst) ds :: IdSet -- our initial program prog <- return prog { progSeasoning = seasoning } Identity prog <- return $ programMapDs (\ (t,e) -> return (shouldBeExported (getExports $ hoTcInfo ho') t,e)) $ atomizeApps False (programSetDs ds prog) -- now we must attach rules to the existing chos, as well as the current ones let addRule c = case mlookup (combIdent c) rules' of Nothing -> c Just rs -> combRules_u (map ruleUpdate . Data.List.union rs) c prog <- return $ progCombinators_u (map addRule) prog cho <- return $ updateChoHo $ choCombinators_u (fmap addRule) cho -- Here we substitute in all the original types, with rules and properties defined in the current module included prog <- return $ runIdentity $ annotateProgram (choVarMap cho) (idann theProps) letann lamann prog lintCheckProgram (putErrLn "LintPostProcess") prog let entryPoints = fromList . execWriter $ programMapDs_ (\ (t,_) -> when (getProperty prop_EXPORTED t || getProperty prop_INSTANCE t || getProperty prop_SPECIALIZATION t) (tell [tvrIdent t])) prog prog <- return $ prog { progEntry = entryPoints `mappend` progSeasoning prog } lintCheckProgram (putErrLn "InitialLint") prog prog <- programPrune prog -- initial pass, performs -- eta expansion of definitons -- simplify -- type analysis -- floating outward -- simplify -- floating inward let sopt = SS.cacheSimpOpts SS.emptySimplifyOpts { SS.so_boundVars = choCombinators cho, SS.so_forwardVars = progSeasoning prog } let tparms = transformParms { transformPass = "PreInit", transformDumpProgress = verbose } -- quick float inward pass to inline once used functions and prune unused ones prog <- transformProgram tparms { transformCategory = "FloatInward", transformOperation = programFloatInward } prog putProgress "<" pr_r <- progressIONew (length $ programDecomposedDs prog) 25 '.' let fint mprog = do let names = pprint [ n | (n,_) <- programDs mprog] withStackStatus ("fint: " ++ names) $ do when coreMini $ putErrLn ("----\n" ++ names) let tparms = transformParms { transformPass = "Init", transformDumpProgress = coreMini } lintCheckProgram onerrNone mprog mprog <- evaluate $ etaAnnotateProgram mprog lintCheckProgram onerrNone mprog mprog <- simplifyProgram sopt "Init-One" coreMini mprog -- this catches more static arguments if we wait until after the initial normalizing simplification pass mprog <- transformProgram tparms { transformSkipNoStats = True, transformCategory = "SimpleRecursive" , transformOperation = return . staticArgumentTransform } mprog mprog <- transformProgram tparms { transformCategory = "FloatOutward", transformOperation = floatOutward } mprog mprog <- transformProgram tparms { transformCategory = "typeAnalyze", transformPass = "PreInit" , transformOperation = typeAnalyze True } mprog mprog <- transformProgram tparms { transformCategory = "FloatOutward", transformOperation = floatOutward } mprog -- perform another supersimplify in order to substitute the once used -- variables back in and replace the variable of case of variables with -- the default binding of the case statement. mprog <- simplifyProgram sopt "Init-Two-FloatOutCleanup" coreMini mprog mprog <- transformProgram tparms { transformCategory = "typeAnalyze", transformOperation = typeAnalyze True } mprog mprog <- transformProgram tparms { transformCategory = "FloatInward", transformOperation = programFloatInward } mprog mprog <- Demand.analyzeProgram mprog lintCheckProgram onerrNone mprog mprog <- simplifyProgram sopt "Init-Three-AfterDemand" False mprog when miniCorePass $ printProgram mprog -- mapM_ (\ (v,lc) -> printCheckName'' fullDataTable v lc) (programDs mprog) when miniCoreSteps $ Stats.printLStat (optStatLevel options) ("InitialOptimize:" ++ names) (progStats mprog) wdump FD.Progress $ let SubProgram isRec = progType mprog in progressIOSteps pr_r (if isRec then "*" else ".") return mprog lintCheckProgram onerrNone prog prog <- programMapProgGroups mempty fint prog wdump FD.Stats $ Stats.printLStat (optStatLevel options) "Initial Pass Stats" (progStats prog) lintCheckProgram onerrNone prog prog <- etaExpandProg "Init-Big-One" prog { progStats = mempty } prog <- transformProgram tparms { transformPass = "Init-Big-One", transformCategory = "FloatInward", transformOperation = programFloatInward } prog prog <- Demand.analyzeProgram prog prog <- simplifyProgram' sopt "Init-Big-One" verbose (IterateMax 4) prog wdump FD.Stats $ Stats.printLStat (optStatLevel options) "Init-Big-One Stats" (progStats prog) pr_r <- progressIONew (length $ programDecomposedCombs prog) 25 '.' -- This is the main function that optimizes the routines before writing them out let optWW mprog = do let names = pprint [ n | (n,_) <- programDs mprog] liftIO $ when coreMini $ putErrLn ("----\n" ++ names) smap <- get let tparms = transformParms { transformPass = "OptWW", transformDumpProgress = coreMini } sopt = SS.cacheSimpOpts SS.emptySimplifyOpts { SS.so_boundVars = smap, SS.so_forwardVars = progSeasoning mprog } mprog <- simplifyProgram sopt "Simplify-One" coreMini mprog mprog <- transformProgram tparms { transformCategory = "FloatInward", transformOperation = programFloatInward } mprog mprog <- Demand.analyzeProgram mprog mprog <- simplifyProgram sopt "Simplify-Two" coreMini mprog mprog <- transformProgram tparms { transformCategory = "FloatInward", transformOperation = programFloatInward } mprog mprog <- Demand.analyzeProgram mprog mprog <- return $ E.CPR.cprAnalyzeProgram mprog mprog' <- transformProgram tparms { transformSkipNoStats = True, transformCategory = "WorkWrap", transformOperation = return . workWrapProgram } mprog let wws = length (programDs mprog') - length (programDs mprog) -- liftIO $ wdump FD.Progress $ putErr (replicate wws 'w') mprog <- return mprog' mprog <- simplifyProgram sopt "Simplify-Three" coreMini mprog --mprog <- transformProgram tparms { transformCategory = "FloatInward", transformOperation = programFloatInward } mprog --mprog <- Demand.analyzeProgram mprog --mprog <- return $ E.CPR.cprAnalyzeProgram mprog --mprog <- transformProgram tparms { transformSkipNoStats = True, transformCategory = "WorkWrap2", transformOperation = return . workWrapProgram } mprog --mprog <- simplifyProgram sopt "Simplify-Four" coreMini mprog -- annotate our bindings for further passes mprog <- return $ etaAnnotateProgram mprog mprog <- Demand.analyzeProgram mprog mprog <- return $ E.CPR.cprAnalyzeProgram mprog put $ fromList [ (combIdent c,c) | c <- progCombinators mprog] `S.union` smap --liftIO $ wdump FD.Progress $ let SubProgram rec = progType mprog in putErr (if rec then "*" else ".") liftIO $ wdump FD.Progress $ let SubProgram isRec = progType mprog in progressIOSteps pr_r (if wws > 0 then "w" else if isRec then "*" else ".") return mprog prog <- evalStateT (programMapProgGroups mempty optWW prog { progStats = mempty }) (SS.so_boundVars sopt) putProgressLn ">" wdump FD.Stats $ Stats.printLStat (optStatLevel options) "MainPass Stats" (progStats prog) processIOErrors lintCheckProgram (putErrLn "After the workwrap/CPR") prog prog <- programPrune prog lintCheckProgram (putErrLn "After the Opimization") prog wdump FD.Core $ printProgram prog let newHoBuild = (hoBuild ho') { hoDataTable = dataTable, hoEs = programDs prog, hoRules = hoRules (hoBuild ho') `mappend` rules } newMap = fmap (\c -> Just (EVar $ combHead c)) $ progCombMap prog return (updateChoHo $ mempty { choHoMap = Map.singleton (hoModuleGroup ho') ho' { hoBuild = newHoBuild}, choCombinators = fromList $ [ (combIdent c,c) | c <- progCombinators prog ], choExternalNames = idMapToIdSet newMap } `mappend` cho,ho' { hoBuild = newHoBuild }) coreMini = dump FD.CoreMini corePass = dump FD.CorePass coreSteps = dump FD.CoreSteps miniCorePass = coreMini && corePass miniCoreSteps = coreMini && coreSteps dumpRules rules = do wdump FD.Rules $ putStrLn " ---- user rules ---- " >> printRules RuleUser rules wdump FD.Rules $ putStrLn " ---- user catalysts ---- " >> printRules RuleCatalyst rules wdump FD.RulesSpec $ putStrLn " ---- specializations ---- " >> printRules RuleSpecialization rules programPruneUnreachable :: Program -> Program programPruneUnreachable prog = progCombinators_s ds' prog where ds' = reachableFrom combIdent freeVars (progCombinators prog) (toList $ progEntry prog) programPrune :: Program -> IO Program programPrune prog = transformProgram transformParms { transformCategory = "PruneUnreachable" , transformDumpProgress = miniCorePass , transformOperation = evaluate . programPruneUnreachable } prog etaExpandProg :: String -> Program -> IO Program etaExpandProg pass prog = do let f prog = prog' { progStats = progStats prog `mappend` stats } where (prog',stats) = Stats.runStatM $ etaExpandProgram prog transformProgram transformParms { transformPass = pass, transformCategory = "EtaExpansion" , transformDumpProgress = miniCorePass, transformOperation = evaluate . f } prog getExports ho = Set.fromList $ map toId $ concat $ Map.elems (hoExports ho) shouldBeExported exports tvr | tvrIdent tvr `Set.member` exports || getProperty prop_SRCLOC_ANNOTATE_FUN tvr = setProperty prop_EXPORTED tvr | otherwise = tvr transTypeAnalyze = transformParms { transformCategory = "typeAnalyze", transformOperation = typeAnalyze True } simplifyProgram sopt name dodump prog = liftIO $ do let istat = progStats prog let g prog = do let nprog = SS.programPruneOccurance prog when (corePass && dodump) $ do putStrLn "-- After Occurance Analysis" printProgram nprog lintCheckProgram (putErrLn "AfterOccurance") nprog return $ SS.programSSimplify sopt nprog prog <- transformProgram transformParms { transformCategory = "Simplify" , transformPass = name , transformIterate = IterateDone , transformDumpProgress = dodump , transformOperation = g } prog { progStats = mempty } when (dodump && (dump FD.Progress || coreSteps)) $ Stats.printLStat (optStatLevel options) ("Total: " ++ name) (progStats prog) return prog { progStats = progStats prog `mappend` istat } {- simplifyProgramPStat sopt name dodump prog = do let istat = progStats prog let g = SS.programSSimplifyPStat sopt { SS.so_dataTable = progDataTable prog } . SS.programPruneOccurance prog <- transformProgram ("PS:" ++ name) IterateDone dodump g prog { progStats = mempty } when ((dodump && dump FD.Progress) || dump FD.CoreSteps) $ Stats.printStat ("Total: " ++ name) (progStats prog) return prog { progStats = progStats prog `mappend` istat } -} simplifyProgram' sopt name dodump iterate prog = do let istat = progStats prog let g = return . SS.programSSimplify sopt . SS.programPruneOccurance prog <- transformProgram transformParms { transformCategory = "Simplify" , transformPass = name , transformIterate = iterate , transformDumpProgress = dodump , transformOperation = g } prog { progStats = mempty } when (dodump && (dump FD.Progress || coreSteps)) $ Stats.printLStat (optStatLevel options) ("Total: " ++ name) (progStats prog) return prog { progStats = progStats prog `mappend` istat } {-# NOINLINE compileWholeProgram #-} compileWholeProgram prog = do performGC when verbose $ do Stats.print "PassStats" Stats.theStats Stats.clear Stats.theStats esmap <- programEsMap prog let mainFunc = parseName Val (maybe "Main.main" snd (optMainFunc options)) dataTable = progDataTable prog ffiExportNames = [ tv | tv <- map combHead $ progCombinators prog, name <- tvrName tv, "FE@" `isPrefixOf` show name ] (main,mainv) <- getMainFunction dataTable mainFunc esmap prog <- return $ programUpdate prog { progMain = tvrIdent main, progEntry = fromList $ map tvrIdent (main:ffiExportNames), progCombinators = emptyComb { combHead = main, combBody = mainv }:map (unsetProperty prop_EXPORTED) (progCombinators prog) } prog <- transformProgram transformParms { transformCategory = "PruneUnreachable", transformOperation = evaluate . programPruneUnreachable } prog prog <- if (fopts FO.TypeAnalysis) then do transformProgram transformParms { transformCategory = "TypeAnalyzeMethods", transformOperation = typeAnalyze False, transformDumpProgress = dump FD.Progress } prog else return prog when verbose $ do putStrLn "Type analyzed methods" flip mapM_ (sortUnder (show . fst) (programDs prog)) $ \ (t,e) -> do let (_,ts) = fromLam e ts' = takeWhile (sortKindLike . getType) ts when (not (null ts')) $ putStrLn $ (pprint t) ++ " \\" ++ concat [ "(" ++ show (Info.fetch (tvrInfo t) :: Typ) ++ ")" | t <- ts' ] lintCheckProgram onerrNone prog prog <- programPrune prog cmethods <- do let es' = concatMap expandPlaceholder (progCombinators prog) es' <- return [ combBody_u floatInward e | e <- es' ] wdump FD.Class $ do sequence_ [ printCheckName'' dataTable (combHead x) (combBody x) | x <- es'] return es' prog <- evaluate $ progCombinators_s ([ p | p <- progCombinators prog, combHead p `notElem` map combHead cmethods] ++ cmethods) prog prog <- annotateProgram mempty (\_ nfo -> return $ unsetProperty prop_INSTANCE nfo) letann (\_ nfo -> return nfo) prog if not (fopts FO.GlobalOptimize) then do prog <- programPrune prog wdump FD.CoreBeforelift $ printProgram prog prog <- transformProgram transformParms { transformCategory = "LambdaLift", transformDumpProgress = dump FD.Progress, transformOperation = lambdaLift } prog wdump FD.CoreAfterlift $ printProgram prog prog <- return $ atomizeApps True prog wdump FD.CoreMangled $ dumpCore "mangled" prog return prog else do prog <- transformProgram transTypeAnalyze { transformPass = "Main-AfterMethod", transformDumpProgress = verbose } prog prog <- simplifyProgram SS.emptySimplifyOpts "Main-One" verbose prog prog <- etaExpandProg "Main-AfterOne" prog wdump FD.CorePass $ dumpCore "before-TypeAnalyze-Main-AfterSimp" prog prog <- transformProgram transTypeAnalyze { transformPass = "Main-AfterSimp", transformDumpProgress = verbose } prog prog <- simplifyProgram SS.emptySimplifyOpts "Main-Two" verbose prog -- run optimization again with no rules enabled prog <- return $ runIdentity $ annotateProgram mempty (\_ nfo -> return $ modifyProperties (flip (foldr S.delete) [prop_HASRULE,prop_WORKER]) nfo) letann (\_ -> return) prog --prog <- transformProgram "float inward" DontIterate True programFloatInward prog prog <- simplifyProgram SS.emptySimplifyOpts { SS.so_finalPhase = True } "SuperSimplify no rules" verbose prog -- We should float inward right before lambda lifting so that when a case statement is lifted out, it takes any local definitions with it. -- prog <- transformProgram transformParms { -- transformCategory = "FloatInward", -- transformDumpProgress = dump FD.Progress, -- transformOperation = programFloatInward -- } prog -- perform lambda lifting -- prog <- denewtypeProgram prog prog <- transformProgram transformParms { transformCategory = "BoxifyProgram", transformDumpProgress = dump FD.Progress, transformOperation = boxifyProgram } prog prog <- programPrune prog prog <- Demand.analyzeProgram prog prog <- return $ E.CPR.cprAnalyzeProgram prog prog <- transformProgram transformParms { transformCategory = "Boxy WorkWrap", transformDumpProgress = dump FD.Progress, transformOperation = evaluate . workWrapProgram } prog prog <- simplifyProgram SS.emptySimplifyOpts { SS.so_finalPhase = True } "SuperSimplify after Boxy WorkWrap" verbose prog prog <- return $ runIdentity $ programMapBodies (return . cleanupE) prog wdump FD.CoreBeforelift $ dumpCore "before-lift" prog prog <- transformProgram transformParms { transformCategory = "LambdaLift", transformDumpProgress = dump FD.Progress, transformOperation = lambdaLift } prog wdump FD.CoreAfterlift $ dumpCore "after-lift" prog finalStats <- Stats.new -- final optimization pass to clean up lambda lifting droppings -- prog <- flip programMapBodies prog $ \ e -> do -- let cm stats e = do -- let sopt = mempty { SS.so_dataTable = dataTable } -- let (stat, e') = SS.simplifyE sopt e -- Stats.tickStat stats stat -- return e' -- doopt (mangle' Nothing dataTable) False finalStats "PostLambdaLift" cm e -- wdump FD.Progress $ Stats.print "PostLifting" finalStats lintCheckProgram (putErrLn "LintPostLifting") prog -- wdump FD.Progress $ printEStats (programE prog) prog <- Demand.analyzeProgram prog prog <- return $ E.CPR.cprAnalyzeProgram prog prog <- simplifyProgram SS.emptySimplifyOpts { SS.so_postLift = True, SS.so_finalPhase = True } "PostLiftSimplify" verbose prog -- prog <- programFloatInward prog when verbose $ do Stats.print "PassStats" Stats.theStats Stats.clear Stats.theStats prog <- return $ atomizeApps True prog wdump FD.CoreMangled $ dumpCore "mangled" prog return prog -- | this gets rid of all type variables, replacing them with boxes that can hold any type. -- The program is still type-safe, but all polymorphism has been removed in favor of -- implicit coercion to a universal type in preparation for the grin transformation. boxifyProgram :: Program -> IO Program boxifyProgram prog = ans where ans = do programMapDs f (progCombinators_u (map $ combRules_s []) prog) f (t,e) = do e <- return $ runReader (g e) Set.empty tt <- return $ runReader (boxify (tvrType t)) Set.empty return (t {tvrType = tt},e) _tv t = t { tvrType = boxify (tvrType t) } g e = do emapEG g (boxify) e -- (\e -> do putStrLn ("box: " ++ pprint e) ; return $ boxify e) e -- boxify t | Just e <- followAlias (progDataTable prog) t = boxify e boxify (from_unsafeCoerce -> Just (e,t)) = do t' <- boxify t e' <- boxify e case typesCompatable t' (getType e') of Just () -> return e _ -> return $ prim_unsafeCoerce e' t' boxify (EPi t e) = local (Set.insert (tvrIdent t)) $ do nt <- boxify $ tvrType t ne <- boxify e return $ EPi t { tvrType = nt } ne boxify v@(EVar vr) | canBeBox v = do s <- ask if tvrIdent vr `Set.member` s then return v else return $ mktBox (tvrType vr) boxify (ELit lc) = do na <- mapM boxify (litArgs lc) return $ ELit lc { litArgs = na } -- boxify v@(EAp _ _) | canBeBox v = mktBox (getType v) -- boxify (EAp (ELam t b) e) = boxify (subst t e b) -- boxify (EAp a b) = EAp (boxify a) b -- TODO there should be no applications at the type level by now (boxify b) boxify (EAp a b) = liftM2 eAp (boxify a) (boxify b) boxify s@ESort {} = return s boxify x = error $ "boxify: " ++ show x -- | get rid of unused bindings cleanupE :: E -> E cleanupE e = runIdentity (f e) where f (ELam t@TVr { tvrIdent = v } e) | v /= emptyId, v `notMember` freeIds e = f (ELam t { tvrIdent = emptyId } e) f (EPi t@TVr { tvrIdent = v } e) | v /= emptyId, v `notMember` freeIds e = f (EPi t { tvrIdent = emptyId } e) f ec@ECase { eCaseBind = t@TVr { tvrIdent = v } } | v /= emptyId, v `notMember` (freeVars (caseBodies ec)::IdSet) = f ec { eCaseBind = t { tvrIdent = emptyId } } f e = emapEG f f e