@@ -39,9 +39,9 @@ module Idris.Core.TT(
3939 , discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname
4040 , fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv
4141 , freeNames, getArgTys, getRetTy, implicitable, instantiate
42− , intTyName, isInjective, isTypeConst, liftPats, lookupCtxt
42+ , intTyName, isInjective, isTypeConst, lookupCtxt
4343 , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth
44− , nextName, noOccurrence, nsroot, occurrences, orderPats
44+ , nextName, noOccurrence, nsroot, occurrences
4545 , pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV
4646 , pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget
4747 , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep
@@ -853,7 +853,8 @@ deriving instance Binary Raw
853853deriving instance NFData Raw
854854!-}
855855
856−data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool }
856+data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool,
857+ machine_gen :: Bool }
857858 deriving (Show, Eq, Ord, Data, Typeable)
858859
859860{-!
@@ -1698,30 +1699,6 @@ weakenEnv env = wk (length env - 1) env
16981699weakenTmEnv :: Int -> EnvTT n -> EnvTT n
16991700weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
17001701
1701−-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1702−-- them in a canonical order
1703−orderPats :: Term -> Term
1704−orderPats tm = op [] tm
1705− where
1706− op [] (App s f a) = App s f (op [] a) -- for Infer terms
1707−
1708− op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc
1709− op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc
1710− op ps (Bind n (Pi i t k) sc) = op ((n, Pi i t k) : ps) sc
1711− op ps sc = bindAll (sortP ps) sc
1712−
1713− sortP ps = pick [] (reverse ps)
1714−
1715− pick acc [] = reverse acc
1716− pick acc ((n, t) : ps) = pick (insert n t acc) ps
1717−
1718− insert n t [] = [(n, t)]
1719− insert n t ((n',t') : ps)
1720− | n `elem` (refsIn (binderTy t') ++
1721− concatMap refsIn (map (binderTy . snd) ps))
1722− = (n', t') : insert n t ps
1723− | otherwise = (n,t):(n',t'):ps
1724−
17251702refsIn :: TT Name -> [Name]
17261703refsIn (P _ n _) = [n]
17271704refsIn (Bind n b t) = nub $ nb b ++ refsIn t
@@ -1731,45 +1708,6 @@ refsIn (Bind n b t) = nub $ nb b ++ refsIn t
17311708refsIn (App s f a) = nub (refsIn f ++ refsIn a)
17321709refsIn _ = []
17331710
1734−-- Make sure all the pattern bindings are as far out as possible
1735−liftPats :: Term -> Term
1736−liftPats tm = let (tm', ps) = runState (getPats tm) [] in
1737− orderPats $ bindPats (reverse ps) tm'
1738− where
1739− bindPats [] tm = tm
1740− bindPats ((n, t):ps) tm
1741− | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)
1742− | otherwise = bindPats ps tm
1743−
1744− getPats :: Term -> State [(Name, Type)] Term
1745− getPats (Bind n (PVar t) sc) = do ps <- get
1746− put ((n, t) : ps)
1747− getPats sc
1748− getPats (Bind n (Guess t v) sc) = do t' <- getPats t
1749− v' <- getPats v
1750− sc' <- getPats sc
1751− return (Bind n (Guess t' v') sc')
1752− getPats (Bind n (Let t v) sc) = do t' <- getPats t
1753− v' <- getPats v
1754− sc' <- getPats sc
1755− return (Bind n (Let t' v') sc')
1756− getPats (Bind n (Pi i t k) sc) = do t' <- getPats t
1757− k' <- getPats k
1758− sc' <- getPats sc
1759− return (Bind n (Pi i t' k') sc')
1760− getPats (Bind n (Lam t) sc) = do t' <- getPats t
1761− sc' <- getPats sc
1762− return (Bind n (Lam t') sc')
1763− getPats (Bind n (Hole t) sc) = do t' <- getPats t
1764− sc' <- getPats sc
1765− return (Bind n (Hole t') sc')
1766−
1767−
1768− getPats (App s f a) = do f' <- getPats f
1769− a' <- getPats a
1770− return (App s f' a')
1771− getPats t = return t
1772−
17731711allTTNames :: Eq n => TT n -> [n]
17741712allTTNames = nub . allNamesIn
17751713 where allNamesIn (P _ n _) = [n]