-- |
-- Module      :  Cryptol.Transform.MonoValues
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This module implements a transformation, which tries to avoid exponential
-- slow down in some cases.  What's the problem?  Consider the following (common)
-- patterns:
--
--     fibs = [0,1] # [ x + y | x <- fibs, y <- drop`{1} fibs ]
--
-- The type of `fibs` is:
--
--     {a} (a >= 1, fin a) => [inf][a]
--
-- Here `a` is the number of bits to be used in the values computed by `fibs`.
-- When we evaluate `fibs`, `a` becomes a parameter to `fibs`, which works
-- except that now `fibs` is a function, and we don't get any of the memoization
-- we might expect!  What looked like an efficient implementation has all
-- of a sudden become exponential!
--
-- Note that this is only a problem for polymorphic values: if `fibs` was
-- already a function, it would not be that surprising that it does not
-- get cached.
--
-- So, to avoid this, we try to spot recursive polymorphic values,
-- where the recursive occurrences have the exact same type parameters
-- as the definition.  For example, this is the case in `fibs`: each
-- recursive call to `fibs` is instantiated with exactly the same
-- type parameter (i.e., `a`).  The rewrite we do is as follows:
--
--     fibs : {a} (a >= 1, fin a) => [inf][a]
--     fibs = \{a} (a >= 1, fin a) -> fibs'
--       where fibs' : [inf][a]
--             fibs' = [0,1] # [ x + y | x <- fibs', y <- drop`{1} fibs' ]
--
-- After the rewrite, the recursion is monomorphic (i.e., we are always using
-- the same type).  As a result, `fibs'` is an ordinary recursive value,
-- where we get the benefit of caching.
--
-- The rewrite is a bit more complex, when there are multiple mutually
-- recursive functions.  Here is an example:
--
--     zig : {a} (a >= 2, fin a) => [inf][a]
--     zig = [1] # zag
--
--     zag : {a} (a >= 2, fin a) => [inf][a]
--     zag = [2] # zig
--
-- This gets rewritten to:
--
--     newName : {a} (a >= 2, fin a) => ([inf][a], [inf][a])
--     newName = \{a} (a >= 2, fin a) -> (zig', zag')
--       where
--       zig' : [inf][a]
--       zig' = [1] # zag'
--
--       zag' : [inf][a]
--       zag' = [2] # zig'
--
--     zig : {a} (a >= 2, fin a) => [inf][a]
--     zig = \{a} (a >= 2, fin a) -> (newName a <> <> ).1
--
--     zag : {a} (a >= 2, fin a) => [inf][a]
--     zag = \{a} (a >= 2, fin a) -> (newName a <> <> ).2
--
-- NOTE:  We are assuming that no capture would occur with binders.
-- For values, this is because we replaces things with freshly chosen variables.
-- For types, this should be because there should be no shadowing in the types.
-- XXX: Make sure that this really is the case for types!!

{-# LANGUAGE PatternGuards, FlexibleInstances, MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.Transform.MonoValues (rewModule) where

import Cryptol.ModuleSystem.Name
        (SupplyT,liftSupply,Supply,mkDeclared,NameSource(..))
import Cryptol.Parser.Position (emptyRange)
import Cryptol.TypeCheck.AST hiding (splitTApp) -- XXX: just use this one
import Cryptol.TypeCheck.TypeMap
import Cryptol.Utils.Ident (ModName)
import Data.List(sortBy,groupBy)
import Data.Either(partitionEithers)
import Data.Map (Map)
import MonadLib hiding (mapM)

import Prelude ()
import Prelude.Compat

{- (f,t,n) |--> x  means that when we spot instantiations of `f` with `ts` and
`n` proof argument, we should replace them with `Var x` -}
newtype RewMap' a = RM (Map Name (TypesMap (Map Int a)))
type RewMap = RewMap' Name

instance TrieMap RewMap' (Name,[Type],Int) where
  emptyTM :: RewMap' a
emptyTM  = Map Name (TypesMap (Map Int a)) -> RewMap' a
forall a. Map Name (TypesMap (Map Int a)) -> RewMap' a
RM Map Name (TypesMap (Map Int a))
forall (m :: * -> *) k a. TrieMap m k => m a
emptyTM

  nullTM :: RewMap' a -> Bool
nullTM (RM m :: Map Name (TypesMap (Map Int a))
m) = Map Name (TypesMap (Map Int a)) -> Bool
forall (m :: * -> *) k a. TrieMap m k => m a -> Bool
nullTM Map Name (TypesMap (Map Int a))
m

  lookupTM :: (Name, [Type], Int) -> RewMap' a -> Maybe a
lookupTM (x :: Name
x,ts :: [Type]
ts,n :: Int
n) (RM m :: Map Name (TypesMap (Map Int a))
m) = do TypesMap (Map Int a)
tM <- Name
-> Map Name (TypesMap (Map Int a)) -> Maybe (TypesMap (Map Int a))
forall (m :: * -> *) k a. TrieMap m k => k -> m a -> Maybe a
lookupTM Name
x Map Name (TypesMap (Map Int a))
m
                                Map Int a
tP <- [Type] -> TypesMap (Map Int a) -> Maybe (Map Int a)
forall (m :: * -> *) k a. TrieMap m k => k -> m a -> Maybe a
lookupTM [Type]
ts TypesMap (Map Int a)
tM
                                Int -> Map Int a -> Maybe a
forall (m :: * -> *) k a. TrieMap m k => k -> m a -> Maybe a
lookupTM Int
n Map Int a
tP

  alterTM :: (Name, [Type], Int)
-> (Maybe a -> Maybe a) -> RewMap' a -> RewMap' a
alterTM (x :: Name
x,ts :: [Type]
ts,n :: Int
n) f :: Maybe a -> Maybe a
f (RM m :: Map Name (TypesMap (Map Int a))
m) = Map Name (TypesMap (Map Int a)) -> RewMap' a
forall a. Map Name (TypesMap (Map Int a)) -> RewMap' a
RM (Name
-> (Maybe (TypesMap (Map Int a)) -> Maybe (TypesMap (Map Int a)))
-> Map Name (TypesMap (Map Int a))
-> Map Name (TypesMap (Map Int a))
forall (m :: * -> *) k a.
TrieMap m k =>
k -> (Maybe a -> Maybe a) -> m a -> m a
alterTM Name
x Maybe (TypesMap (Map Int a)) -> Maybe (TypesMap (Map Int a))
forall (m :: * -> *) (m :: * -> *).
(TrieMap m [Type], TrieMap m Int) =>
Maybe (m (m a)) -> Maybe (m (m a))
f1 Map Name (TypesMap (Map Int a))
m)
    where
    f1 :: Maybe (m (m a)) -> Maybe (m (m a))
f1 Nothing   = do a
a <- Maybe a -> Maybe a
f Maybe a
forall a. Maybe a
Nothing
                      m (m a) -> Maybe (m (m a))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> m a -> m (m a) -> m (m a)
forall (m :: * -> *) k a. TrieMap m k => k -> a -> m a -> m a
insertTM [Type]
ts (Int -> a -> m a -> m a
forall (m :: * -> *) k a. TrieMap m k => k -> a -> m a -> m a
insertTM Int
n a
a m a
forall (m :: * -> *) k a. TrieMap m k => m a
emptyTM) m (m a)
forall (m :: * -> *) k a. TrieMap m k => m a
emptyTM)

    f1 (Just tM :: m (m a)
tM) = m (m a) -> Maybe (m (m a))
forall a. a -> Maybe a
Just ([Type] -> (Maybe (m a) -> Maybe (m a)) -> m (m a) -> m (m a)
forall (m :: * -> *) k a.
TrieMap m k =>
k -> (Maybe a -> Maybe a) -> m a -> m a
alterTM [Type]
ts Maybe (m a) -> Maybe (m a)
forall (m :: * -> *). TrieMap m Int => Maybe (m a) -> Maybe (m a)
f2 m (m a)
tM)

    f2 :: Maybe (m a) -> Maybe (m a)
f2 Nothing   = do a
a <- Maybe a -> Maybe a
f Maybe a
forall a. Maybe a
Nothing
                      m a -> Maybe (m a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> a -> m a -> m a
forall (m :: * -> *) k a. TrieMap m k => k -> a -> m a -> m a
insertTM Int
n a
a m a
forall (m :: * -> *) k a. TrieMap m k => m a
emptyTM)

    f2 (Just pM :: m a
pM) = m a -> Maybe (m a)
forall a. a -> Maybe a
Just (Int -> (Maybe a -> Maybe a) -> m a -> m a
forall (m :: * -> *) k a.
TrieMap m k =>
k -> (Maybe a -> Maybe a) -> m a -> m a
alterTM Int
n Maybe a -> Maybe a
f m a
pM)

  unionTM :: (a -> a -> a) -> RewMap' a -> RewMap' a -> RewMap' a
unionTM f :: a -> a -> a
f (RM a :: Map Name (TypesMap (Map Int a))
a) (RM b :: Map Name (TypesMap (Map Int a))
b) = Map Name (TypesMap (Map Int a)) -> RewMap' a
forall a. Map Name (TypesMap (Map Int a)) -> RewMap' a
RM ((TypesMap (Map Int a)
 -> TypesMap (Map Int a) -> TypesMap (Map Int a))
-> Map Name (TypesMap (Map Int a))
-> Map Name (TypesMap (Map Int a))
-> Map Name (TypesMap (Map Int a))
forall (m :: * -> *) k a.
TrieMap m k =>
(a -> a -> a) -> m a -> m a -> m a
unionTM ((Map Int a -> Map Int a -> Map Int a)
-> TypesMap (Map Int a)
-> TypesMap (Map Int a)
-> TypesMap (Map Int a)
forall (m :: * -> *) k a.
TrieMap m k =>
(a -> a -> a) -> m a -> m a -> m a
unionTM ((a -> a -> a) -> Map Int a -> Map Int a -> Map Int a
forall (m :: * -> *) k a.
TrieMap m k =>
(a -> a -> a) -> m a -> m a -> m a
unionTM a -> a -> a
f)) Map Name (TypesMap (Map Int a))
a Map Name (TypesMap (Map Int a))
b)

  toListTM :: RewMap' a -> [((Name, [Type], Int), a)]
toListTM (RM m :: Map Name (TypesMap (Map Int a))
m) = [ ((Name
x,[Type]
ts,Int
n),a
y) | (x :: Name
x,tM :: TypesMap (Map Int a)
tM)  <- Map Name (TypesMap (Map Int a)) -> [(Name, TypesMap (Map Int a))]
forall (m :: * -> *) k a. TrieMap m k => m a -> [(k, a)]
toListTM Map Name (TypesMap (Map Int a))
m
                                   , (ts :: [Type]
ts,pM :: Map Int a
pM) <- TypesMap (Map Int a) -> [([Type], Map Int a)]
forall (m :: * -> *) k a. TrieMap m k => m a -> [(k, a)]
toListTM TypesMap (Map Int a)
tM
                                   , (n :: Int
n,y :: a
y)   <- Map Int a -> [(Int, a)]
forall (m :: * -> *) k a. TrieMap m k => m a -> [(k, a)]
toListTM Map Int a
pM ]

  mapMaybeWithKeyTM :: ((Name, [Type], Int) -> a -> Maybe b) -> RewMap' a -> RewMap' b
mapMaybeWithKeyTM f :: (Name, [Type], Int) -> a -> Maybe b
f (RM m :: Map Name (TypesMap (Map Int a))
m) =
    Map Name (TypesMap (Map Int b)) -> RewMap' b
forall a. Map Name (TypesMap (Map Int a)) -> RewMap' a
RM ((Name -> TypesMap (Map Int a) -> TypesMap (Map Int b))
-> Map Name (TypesMap (Map Int a))
-> Map Name (TypesMap (Map Int b))
forall (m :: * -> *) k a b.
TrieMap m k =>
(k -> a -> b) -> m a -> m b
mapWithKeyTM      (\qn :: Name
qn  tm :: TypesMap (Map Int a)
tm ->
        ([Type] -> Map Int a -> Map Int b)
-> TypesMap (Map Int a) -> TypesMap (Map Int b)
forall (m :: * -> *) k a b.
TrieMap m k =>
(k -> a -> b) -> m a -> m b
mapWithKeyTM      (\tys :: [Type]
tys is :: Map Int a
is ->
        (Int -> a -> Maybe b) -> Map Int a -> Map Int b
forall (m :: * -> *) k a b.
TrieMap m k =>
(k -> a -> Maybe b) -> m a -> m b
mapMaybeWithKeyTM (\i :: Int
i   a :: a
a  -> (Name, [Type], Int) -> a -> Maybe b
f (Name
qn,[Type]
tys,Int
i) a
a) Map Int a
is) TypesMap (Map Int a)
tm) Map Name (TypesMap (Map Int a))
m)

-- | Note that this assumes that this pass will be run only once for each
-- module, otherwise we will get name collisions.
rewModule :: Supply -> Module -> (Module,Supply)
rewModule :: Supply -> Module -> (Module, Supply)
rewModule s :: Supply
s m :: Module
m = ReaderT RO (SupplyT Id) Module -> RO -> Supply -> (Module, Supply)
forall (m :: * -> *) a r. RunM m a r => m a -> r
runM ReaderT RO (SupplyT Id) Module
body (Module -> RO
mName Module
m) Supply
s
  where
  body :: ReaderT RO (SupplyT Id) Module
body = do [DeclGroup]
ds <- (DeclGroup -> ReaderT RO (SupplyT Id) DeclGroup)
-> [DeclGroup] -> ReaderT RO (SupplyT Id) [DeclGroup]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RewMap -> DeclGroup -> ReaderT RO (SupplyT Id) DeclGroup
rewDeclGroup RewMap
forall (m :: * -> *) k a. TrieMap m k => m a
emptyTM) (Module -> [DeclGroup]
mDecls Module
m)
            Module -> ReaderT RO (SupplyT Id) Module
forall (m :: * -> *) a. Monad m => a -> m a
return Module
m { mDecls :: [DeclGroup]
mDecls = [DeclGroup]
ds }

--------------------------------------------------------------------------------

type M  = ReaderT RO (SupplyT Id)
type RO = ModName

-- | Produce a fresh top-level name.
newName :: M Name
newName :: M Name
newName  =
  do RO
ns <- ReaderT RO (SupplyT Id) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     (Supply -> (Name, Supply)) -> M Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (RO
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
mkDeclared RO
ns NameSource
SystemName "$mono" Maybe Fixity
forall a. Maybe a
Nothing Range
emptyRange)

newTopOrLocalName :: M Name
newTopOrLocalName :: M Name
newTopOrLocalName  = M Name
newName

-- | Not really any distinction between global and local, all names get the
-- module prefix added, and a unique id.
inLocal :: M a -> M a
inLocal :: M a -> M a
inLocal  = M a -> M a
forall a. a -> a
id



--------------------------------------------------------------------------------
rewE :: RewMap -> Expr -> M Expr   -- XXX: not IO
rewE :: RewMap -> Expr -> M Expr
rewE rews :: RewMap
rews = Expr -> M Expr
go

  where
  tryRewrite :: (Expr, [Type], Int) -> Maybe Expr
tryRewrite (EVar x :: Name
x,tps :: [Type]
tps,n :: Int
n) =
     do Name
y <- (Name, [Type], Int) -> RewMap -> Maybe Name
forall (m :: * -> *) k a. TrieMap m k => k -> m a -> Maybe a
lookupTM (Name
x,[Type]
tps,Int
n) RewMap
rews
        Expr -> Maybe Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr
EVar Name
y)
  tryRewrite _ = Maybe Expr
forall a. Maybe a
Nothing

  go :: Expr -> M Expr
go expr :: Expr
expr =
    case Expr
expr of

      -- Interesting cases
      ETApp e :: Expr
e t :: Type
t      -> case (Expr, [Type], Int) -> Maybe Expr
tryRewrite (Expr -> Int -> (Expr, [Type], Int)
splitTApp Expr
expr 0) of
                          Nothing  -> Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr)
-> M Expr -> ReaderT RO (SupplyT Id) (Type -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e ReaderT RO (SupplyT Id) (Type -> Expr)
-> ReaderT RO (SupplyT Id) Type -> M Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReaderT RO (SupplyT Id) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
                          Just yes :: Expr
yes -> Expr -> M Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
yes
      EProofApp e :: Expr
e    -> case (Expr, [Type], Int) -> Maybe Expr
tryRewrite (Expr -> Int -> (Expr, [Type], Int)
splitTApp Expr
e 1) of
                          Nothing  -> Expr -> Expr
EProofApp (Expr -> Expr) -> M Expr -> M Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e
                          Just yes :: Expr
yes -> Expr -> M Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
yes

      EList es :: [Expr]
es t :: Type
t      -> [Expr] -> Type -> Expr
EList   ([Expr] -> Type -> Expr)
-> ReaderT RO (SupplyT Id) [Expr]
-> ReaderT RO (SupplyT Id) (Type -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> M Expr) -> [Expr] -> ReaderT RO (SupplyT Id) [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr -> M Expr
go [Expr]
es ReaderT RO (SupplyT Id) (Type -> Expr)
-> ReaderT RO (SupplyT Id) Type -> M Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ReaderT RO (SupplyT Id) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
      ETuple es :: [Expr]
es       -> [Expr] -> Expr
ETuple  ([Expr] -> Expr) -> ReaderT RO (SupplyT Id) [Expr] -> M Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> M Expr) -> [Expr] -> ReaderT RO (SupplyT Id) [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr -> M Expr
go [Expr]
es
      ERec fs :: [(Ident, Expr)]
fs         -> [(Ident, Expr)] -> Expr
ERec    ([(Ident, Expr)] -> Expr)
-> ReaderT RO (SupplyT Id) [(Ident, Expr)] -> M Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(Ident, Expr)]
-> ((Ident, Expr) -> ReaderT RO (SupplyT Id) (Ident, Expr))
-> ReaderT RO (SupplyT Id) [(Ident, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ident, Expr)]
fs (((Ident, Expr) -> ReaderT RO (SupplyT Id) (Ident, Expr))
 -> ReaderT RO (SupplyT Id) [(Ident, Expr)])
-> ((Ident, Expr) -> ReaderT RO (SupplyT Id) (Ident, Expr))
-> ReaderT RO (SupplyT Id) [(Ident, Expr)]
forall a b. (a -> b) -> a -> b
$ \(f :: Ident
f,e :: Expr
e) -> do Expr
e1 <- Expr -> M Expr
go Expr
e
                                                             (Ident, Expr) -> ReaderT RO (SupplyT Id) (Ident, Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident
f,Expr
e1))
      ESel e :: Expr
e s :: Selector
s        -> Expr -> Selector -> Expr
ESel    (Expr -> Selector -> Expr)
-> M Expr -> ReaderT RO (SupplyT Id) (Selector -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e  ReaderT RO (SupplyT Id) (Selector -> Expr)
-> ReaderT RO (SupplyT Id) Selector -> M Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Selector -> ReaderT RO (SupplyT Id) Selector
forall (m :: * -> *) a. Monad m => a -> m a
return Selector
s
      ESet e :: Expr
e s :: Selector
s v :: Expr
v      -> Expr -> Selector -> Expr -> Expr
ESet    (Expr -> Selector -> Expr -> Expr)
-> M Expr -> ReaderT RO (SupplyT Id) (Selector -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e  ReaderT RO (SupplyT Id) (Selector -> Expr -> Expr)
-> ReaderT RO (SupplyT Id) Selector
-> ReaderT RO (SupplyT Id) (Expr -> Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Selector -> ReaderT RO (SupplyT Id) Selector
forall (m :: * -> *) a. Monad m => a -> m a
return Selector
s ReaderT RO (SupplyT Id) (Expr -> Expr) -> M Expr -> M Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> M Expr
go Expr
v
      EIf e1 :: Expr
e1 e2 :: Expr
e2 e3 :: Expr
e3    -> Expr -> Expr -> Expr -> Expr
EIf     (Expr -> Expr -> Expr -> Expr)
-> M Expr -> ReaderT RO (SupplyT Id) (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e1 ReaderT RO (SupplyT Id) (Expr -> Expr -> Expr)
-> M Expr -> ReaderT RO (SupplyT Id) (Expr -> Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> M Expr
go Expr
e2 ReaderT RO (SupplyT Id) (Expr -> Expr) -> M Expr -> M Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> M Expr
go Expr
e3

      EComp len :: Type
len t :: Type
t e :: Expr
e mss :: [[Match]]
mss -> Type -> Type -> Expr -> [[Match]] -> Expr
EComp Type
len Type
t (Expr -> [[Match]] -> Expr)
-> M Expr -> ReaderT RO (SupplyT Id) ([[Match]] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e  ReaderT RO (SupplyT Id) ([[Match]] -> Expr)
-> ReaderT RO (SupplyT Id) [[Match]] -> M Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Match] -> ReaderT RO (SupplyT Id) [Match])
-> [[Match]] -> ReaderT RO (SupplyT Id) [[Match]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Match -> ReaderT RO (SupplyT Id) Match)
-> [Match] -> ReaderT RO (SupplyT Id) [Match]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RewMap -> Match -> ReaderT RO (SupplyT Id) Match
rewM RewMap
rews)) [[Match]]
mss
      EVar _          -> Expr -> M Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
expr

      ETAbs x :: TParam
x e :: Expr
e       -> TParam -> Expr -> Expr
ETAbs TParam
x  (Expr -> Expr) -> M Expr -> M Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e

      EApp e1 :: Expr
e1 e2 :: Expr
e2      -> Expr -> Expr -> Expr
EApp     (Expr -> Expr -> Expr)
-> M Expr -> ReaderT RO (SupplyT Id) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e1 ReaderT RO (SupplyT Id) (Expr -> Expr) -> M Expr -> M Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> M Expr
go Expr
e2
      EAbs x :: Name
x t :: Type
t e :: Expr
e      -> Name -> Type -> Expr -> Expr
EAbs Name
x Type
t (Expr -> Expr) -> M Expr -> M Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e

      EProofAbs x :: Type
x e :: Expr
e   -> Type -> Expr -> Expr
EProofAbs Type
x (Expr -> Expr) -> M Expr -> M Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e

      EWhere e :: Expr
e dgs :: [DeclGroup]
dgs    -> Expr -> [DeclGroup] -> Expr
EWhere      (Expr -> [DeclGroup] -> Expr)
-> M Expr -> ReaderT RO (SupplyT Id) ([DeclGroup] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> M Expr
go Expr
e ReaderT RO (SupplyT Id) ([DeclGroup] -> Expr)
-> ReaderT RO (SupplyT Id) [DeclGroup] -> M Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT RO (SupplyT Id) [DeclGroup]
-> ReaderT RO (SupplyT Id) [DeclGroup]
forall a. M a -> M a
inLocal
                                                  ((DeclGroup -> ReaderT RO (SupplyT Id) DeclGroup)
-> [DeclGroup] -> ReaderT RO (SupplyT Id) [DeclGroup]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RewMap -> DeclGroup -> ReaderT RO (SupplyT Id) DeclGroup
rewDeclGroup RewMap
rews) [DeclGroup]
dgs)


rewM :: RewMap -> Match -> M Match
rewM :: RewMap -> Match -> ReaderT RO (SupplyT Id) Match
rewM rews :: RewMap
rews ma :: Match
ma =
  case Match
ma of
    From x :: Name
x len :: Type
len t :: Type
t e :: Expr
e -> Name -> Type -> Type -> Expr -> Match
From Name
x Type
len Type
t (Expr -> Match) -> M Expr -> ReaderT RO (SupplyT Id) Match
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewMap -> Expr -> M Expr
rewE RewMap
rews Expr
e

    -- These are not recursive.
    Let d :: Decl
d      -> Decl -> Match
Let (Decl -> Match)
-> ReaderT RO (SupplyT Id) Decl -> ReaderT RO (SupplyT Id) Match
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewMap -> Decl -> ReaderT RO (SupplyT Id) Decl
rewD RewMap
rews Decl
d


rewD :: RewMap -> Decl -> M Decl
rewD :: RewMap -> Decl -> ReaderT RO (SupplyT Id) Decl
rewD rews :: RewMap
rews d :: Decl
d = do DeclDef
e <- RewMap -> DeclDef -> M DeclDef
rewDef RewMap
rews (Decl -> DeclDef
dDefinition Decl
d)
                 Decl -> ReaderT RO (SupplyT Id) Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
d { dDefinition :: DeclDef
dDefinition = DeclDef
e }

rewDef :: RewMap -> DeclDef -> M DeclDef
rewDef :: RewMap -> DeclDef -> M DeclDef
rewDef rews :: RewMap
rews (DExpr e :: Expr
e) = Expr -> DeclDef
DExpr (Expr -> DeclDef) -> M Expr -> M DeclDef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewMap -> Expr -> M Expr
rewE RewMap
rews Expr
e
rewDef _    DPrim     = DeclDef -> M DeclDef
forall (m :: * -> *) a. Monad m => a -> m a
return DeclDef
DPrim

rewDeclGroup :: RewMap -> DeclGroup -> M DeclGroup
rewDeclGroup :: RewMap -> DeclGroup -> ReaderT RO (SupplyT Id) DeclGroup
rewDeclGroup rews :: RewMap
rews dg :: DeclGroup
dg =
  case DeclGroup
dg of
    NonRecursive d :: Decl
d -> Decl -> DeclGroup
NonRecursive (Decl -> DeclGroup)
-> ReaderT RO (SupplyT Id) Decl
-> ReaderT RO (SupplyT Id) DeclGroup
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewMap -> Decl -> ReaderT RO (SupplyT Id) Decl
rewD RewMap
rews Decl
d
    Recursive ds :: [Decl]
ds ->
      do let (leave :: [Decl]
leave,rew :: [(Decl, [TParam], [Type], Expr)]
rew) = [Either Decl (Decl, [TParam], [Type], Expr)]
-> ([Decl], [(Decl, [TParam], [Type], Expr)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ((Decl -> Either Decl (Decl, [TParam], [Type], Expr))
-> [Decl] -> [Either Decl (Decl, [TParam], [Type], Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Either Decl (Decl, [TParam], [Type], Expr)
consider [Decl]
ds)
             rewGroups :: [[(Decl, [TParam], [Type], Expr)]]
rewGroups   = ((Decl, [TParam], [Type], Expr)
 -> (Decl, [TParam], [Type], Expr) -> Bool)
-> [(Decl, [TParam], [Type], Expr)]
-> [[(Decl, [TParam], [Type], Expr)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Decl, [TParam], [Type], Expr)
-> (Decl, [TParam], [Type], Expr) -> Bool
forall a a a d a d.
(Eq a, Eq a) =>
(a, a, a, d) -> (a, a, a, d) -> Bool
sameTParams
                         ([(Decl, [TParam], [Type], Expr)]
 -> [[(Decl, [TParam], [Type], Expr)]])
-> [(Decl, [TParam], [Type], Expr)]
-> [[(Decl, [TParam], [Type], Expr)]]
forall a b. (a -> b) -> a -> b
$ ((Decl, [TParam], [Type], Expr)
 -> (Decl, [TParam], [Type], Expr) -> Ordering)
-> [(Decl, [TParam], [Type], Expr)]
-> [(Decl, [TParam], [Type], Expr)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Decl, [TParam], [Type], Expr)
-> (Decl, [TParam], [Type], Expr) -> Ordering
forall a b a d a d.
(Ord a, Ord b) =>
(a, b, a, d) -> (a, b, a, d) -> Ordering
compareTParams [(Decl, [TParam], [Type], Expr)]
rew
         [Decl]
ds1 <- (Decl -> ReaderT RO (SupplyT Id) Decl)
-> [Decl] -> ReaderT RO (SupplyT Id) [Decl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RewMap -> Decl -> ReaderT RO (SupplyT Id) Decl
rewD RewMap
rews) [Decl]
leave
         [[Decl]]
ds2 <- ([(Decl, [TParam], [Type], Expr)]
 -> ReaderT RO (SupplyT Id) [Decl])
-> [[(Decl, [TParam], [Type], Expr)]]
-> ReaderT RO (SupplyT Id) [[Decl]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [(Decl, [TParam], [Type], Expr)] -> ReaderT RO (SupplyT Id) [Decl]
rewSame [[(Decl, [TParam], [Type], Expr)]]
rewGroups
         DeclGroup -> ReaderT RO (SupplyT Id) DeclGroup
forall (m :: * -> *) a. Monad m => a -> m a
return (DeclGroup -> ReaderT RO (SupplyT Id) DeclGroup)
-> DeclGroup -> ReaderT RO (SupplyT Id) DeclGroup
forall a b. (a -> b) -> a -> b
$ [Decl] -> DeclGroup
Recursive ([Decl]
ds1 [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Decl]]
ds2)

  where
  sameTParams :: (a, a, a, d) -> (a, a, a, d) -> Bool
sameTParams    (_,tps1 :: a
tps1,x :: a
x,_) (_,tps2 :: a
tps2,y :: a
y,_) = a
tps1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
tps2 Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
  compareTParams :: (a, b, a, d) -> (a, b, a, d) -> Ordering
compareTParams (_,tps1 :: b
tps1,x :: a
x,_) (_,tps2 :: b
tps2,y :: a
y,_) = (a, b) -> (a, b) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a
x,b
tps1) (a
y,b
tps2)

  consider :: Decl -> Either Decl (Decl, [TParam], [Type], Expr)
consider d :: Decl
d   =
    case Decl -> DeclDef
dDefinition Decl
d of
      DPrim   -> Decl -> Either Decl (Decl, [TParam], [Type], Expr)
forall a b. a -> Either a b
Left Decl
d
      DExpr e :: Expr
e -> let (tps :: [TParam]
tps,props :: [Type]
props,e' :: Expr
e') = Expr -> ([TParam], [Type], Expr)
splitTParams Expr
e
                 in if Bool -> Bool
not ([TParam] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TParam]
tps) Bool -> Bool -> Bool
&& Expr -> Bool
notFun Expr
e'
                     then (Decl, [TParam], [Type], Expr)
-> Either Decl (Decl, [TParam], [Type], Expr)
forall a b. b -> Either a b
Right (Decl
d, [TParam]
tps, [Type]
props, Expr
e')
                     else Decl -> Either Decl (Decl, [TParam], [Type], Expr)
forall a b. a -> Either a b
Left Decl
d

  rewSame :: [(Decl, [TParam], [Type], Expr)] -> ReaderT RO (SupplyT Id) [Decl]
rewSame ds :: [(Decl, [TParam], [Type], Expr)]
ds =
     do [(Decl, Name, Expr)]
new <- [(Decl, [TParam], [Type], Expr)]
-> ((Decl, [TParam], [Type], Expr)
    -> ReaderT RO (SupplyT Id) (Decl, Name, Expr))
-> ReaderT RO (SupplyT Id) [(Decl, Name, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Decl, [TParam], [Type], Expr)]
ds (((Decl, [TParam], [Type], Expr)
  -> ReaderT RO (SupplyT Id) (Decl, Name, Expr))
 -> ReaderT RO (SupplyT Id) [(Decl, Name, Expr)])
-> ((Decl, [TParam], [Type], Expr)
    -> ReaderT RO (SupplyT Id) (Decl, Name, Expr))
-> ReaderT RO (SupplyT Id) [(Decl, Name, Expr)]
forall a b. (a -> b) -> a -> b
$ \(d :: Decl
d,_,_,e :: Expr
e) ->
                 do Name
x <- M Name
newName
                    (Decl, Name, Expr) -> ReaderT RO (SupplyT Id) (Decl, Name, Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl
d, Name
x, Expr
e)
        let (_,tps :: [TParam]
tps,props :: [Type]
props,_) : _ = [(Decl, [TParam], [Type], Expr)]
ds
            tys :: [Type]
tys            = (TParam -> Type) -> [TParam] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Type
TVar (TVar -> Type) -> (TParam -> TVar) -> TParam -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar) [TParam]
tps
            proofNum :: Int
proofNum       = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
props
            addRew :: (Decl, a, c) -> m a -> m a
addRew (d :: Decl
d,x :: a
x,_) = (Name, [Type], Int) -> a -> m a -> m a
forall (m :: * -> *) k a. TrieMap m k => k -> a -> m a -> m a
insertTM (Decl -> Name
dName Decl
d,[Type]
tys,Int
proofNum) a
x
            newRews :: RewMap
newRews        = ((Decl, Name, Expr) -> RewMap -> RewMap)
-> RewMap -> [(Decl, Name, Expr)] -> RewMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Decl, Name, Expr) -> RewMap -> RewMap
forall (m :: * -> *) a c.
TrieMap m (Name, [Type], Int) =>
(Decl, a, c) -> m a -> m a
addRew RewMap
rews [(Decl, Name, Expr)]
new

        [(Decl, Decl)]
newDs <- [(Decl, Name, Expr)]
-> ((Decl, Name, Expr) -> ReaderT RO (SupplyT Id) (Decl, Decl))
-> ReaderT RO (SupplyT Id) [(Decl, Decl)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Decl, Name, Expr)]
new (((Decl, Name, Expr) -> ReaderT RO (SupplyT Id) (Decl, Decl))
 -> ReaderT RO (SupplyT Id) [(Decl, Decl)])
-> ((Decl, Name, Expr) -> ReaderT RO (SupplyT Id) (Decl, Decl))
-> ReaderT RO (SupplyT Id) [(Decl, Decl)]
forall a b. (a -> b) -> a -> b
$ \(d :: Decl
d,newN :: Name
newN,e :: Expr
e) ->
                   do Expr
e1 <- RewMap -> Expr -> M Expr
rewE RewMap
newRews Expr
e
                      (Decl, Decl) -> ReaderT RO (SupplyT Id) (Decl, Decl)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Decl
d
                             , Decl
d { dName :: Name
dName        = Name
newN
                                 , dSignature :: Schema
dSignature   = (Decl -> Schema
dSignature Decl
d)
                                         { sVars :: [TParam]
sVars = [], sProps :: [Type]
sProps = [] }
                                 , dDefinition :: DeclDef
dDefinition  = Expr -> DeclDef
DExpr Expr
e1
                                 }
                             )

        case [(Decl, Decl)]
newDs of
          [(f :: Decl
f,f' :: Decl
f')] ->
              [Decl] -> ReaderT RO (SupplyT Id) [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return  [ Decl
f { dDefinition :: DeclDef
dDefinition =
                                let newBody :: Expr
newBody = Name -> Expr
EVar (Decl -> Name
dName Decl
f')
                                    newE :: Expr
newE = Expr -> [DeclGroup] -> Expr
EWhere Expr
newBody
                                              [ [Decl] -> DeclGroup
Recursive [Decl
f'] ]
                                in Expr -> DeclDef
DExpr (Expr -> DeclDef) -> Expr -> DeclDef
forall a b. (a -> b) -> a -> b
$ (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs
                                   ((Type -> Expr -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Expr -> Expr
EProofAbs Expr
newE [Type]
props) [TParam]
tps
                            }
                      ]

          _ -> do Name
tupName <- M Name
newTopOrLocalName
                  let (polyDs :: [Decl]
polyDs,monoDs :: [Decl]
monoDs) = [(Decl, Decl)] -> ([Decl], [Decl])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Decl, Decl)]
newDs

                      tupAr :: Int
tupAr  = [Decl] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Decl]
monoDs
                      addTPs :: Expr -> Expr
addTPs = (Expr -> [TParam] -> Expr) -> [TParam] -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs)     [TParam]
tps
                             (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [Type] -> Expr) -> [Type] -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Type -> Expr -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Expr -> Expr
EProofAbs) [Type]
props

                      -- tuple = \{a} p -> (f',g')
                      --                where f' = ...
                      --                      g' = ...
                      tupD :: Decl
tupD = $WDecl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe String
-> Decl
Decl
                        { dName :: Name
dName       = Name
tupName
                        , dSignature :: Schema
dSignature  =
                            [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
tps [Type]
props (Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
$
                               TCon -> [Type] -> Type
TCon (TC -> TCon
TC (Int -> TC
TCTuple Int
tupAr))
                                    ((Decl -> Type) -> [Decl] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Schema -> Type
sType (Schema -> Type) -> (Decl -> Schema) -> Decl -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decl -> Schema
dSignature) [Decl]
monoDs)

                        , dDefinition :: DeclDef
dDefinition =
                            Expr -> DeclDef
DExpr  (Expr -> DeclDef) -> Expr -> DeclDef
forall a b. (a -> b) -> a -> b
$
                            Expr -> Expr
addTPs (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$
                            Expr -> [DeclGroup] -> Expr
EWhere ([Expr] -> Expr
ETuple [ Name -> Expr
EVar (Decl -> Name
dName Decl
d) | Decl
d <- [Decl]
monoDs ])
                                   [ [Decl] -> DeclGroup
Recursive [Decl]
monoDs ]

                        , dPragmas :: [Pragma]
dPragmas    = [] -- ?

                        , dInfix :: Bool
dInfix = Bool
False
                        , dFixity :: Maybe Fixity
dFixity = Maybe Fixity
forall a. Maybe a
Nothing
                        , dDoc :: Maybe String
dDoc = Maybe String
forall a. Maybe a
Nothing
                        }

                      mkProof :: Expr -> p -> Expr
mkProof e :: Expr
e _ = Expr -> Expr
EProofApp Expr
e

                      -- f = \{a} (p) -> (tuple @a p). n

                      mkFunDef :: Int -> Decl -> Decl
mkFunDef n :: Int
n f :: Decl
f =
                        Decl
f { dDefinition :: DeclDef
dDefinition =
                              Expr -> DeclDef
DExpr  (Expr -> DeclDef) -> Expr -> DeclDef
forall a b. (a -> b) -> a -> b
$
                              Expr -> Expr
addTPs (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Selector -> Expr
ESel ( (Expr -> [Type] -> Expr) -> [Type] -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Type -> Expr
forall p. Expr -> p -> Expr
mkProof) [Type]
props
                                            (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> [Type] -> Expr) -> [Type] -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Type -> Expr
ETApp) [Type]
tys
                                            (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
EVar Name
tupName
                                            ) (Int -> Maybe Int -> Selector
TupleSel Int
n (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
tupAr))
                          }

                  [Decl] -> ReaderT RO (SupplyT Id) [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl
tupD Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
: (Int -> Decl -> Decl) -> [Int] -> [Decl] -> [Decl]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Decl -> Decl
mkFunDef [ 0 .. ] [Decl]
polyDs)


--------------------------------------------------------------------------------
splitTParams :: Expr -> ([TParam], [Prop], Expr)
splitTParams :: Expr -> ([TParam], [Type], Expr)
splitTParams e :: Expr
e = let (tps :: [TParam]
tps, e1 :: Expr
e1)   = (Expr -> Maybe (TParam, Expr)) -> Expr -> ([TParam], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (TParam, Expr)
splitTAbs Expr
e
                     (props :: [Type]
props, e2 :: Expr
e2) = (Expr -> Maybe (Type, Expr)) -> Expr -> ([Type], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Type, Expr)
splitProofAbs Expr
e1
                 in ([TParam]
tps,[Type]
props,Expr
e2)

-- returns type instantitaion and how many "proofs" were there
splitTApp :: Expr -> Int -> (Expr, [Type], Int)
splitTApp :: Expr -> Int -> (Expr, [Type], Int)
splitTApp (EProofApp e :: Expr
e) n :: Int
n = Expr -> Int -> (Expr, [Type], Int)
splitTApp Expr
e (Int -> (Expr, [Type], Int)) -> Int -> (Expr, [Type], Int)
forall a b. (a -> b) -> a -> b
$! (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
splitTApp e0 :: Expr
e0 n :: Int
n            = let (e1 :: Expr
e1,ts :: [Type]
ts) = Expr -> [Type] -> (Expr, [Type])
splitTy Expr
e0 []
                            in (Expr
e1, [Type]
ts, Int
n)
  where
  splitTy :: Expr -> [Type] -> (Expr, [Type])
splitTy (ETApp e :: Expr
e t :: Type
t) ts :: [Type]
ts = Expr -> [Type] -> (Expr, [Type])
splitTy Expr
e (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts)
  splitTy e :: Expr
e ts :: [Type]
ts           = (Expr
e,[Type]
ts)

notFun :: Expr -> Bool
notFun :: Expr -> Bool
notFun (EAbs {})       = Bool
False
notFun (EProofAbs _ e :: Expr
e) = Expr -> Bool
notFun Expr
e
notFun _               = Bool
True