{- |
    Module      :  $Header$
    Description :  Lifting of lambda-expressions and local functions
    Copyright   :  (c) 2001 - 2003 Wolfgang Lux
                       2011 - 2015 Björn Peemöller
                       2016 - 2017 Finn Teegen
    License     :  BSD-3-clause

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

   After desugaring and simplifying the code, the compiler lifts all local
   function declarations to the top-level keeping only local variable
   declarations. The algorithm used here is similar to Johnsson's, consisting
   of two phases. First, we abstract each local function declaration,
   adding its free variables as initial parameters and update all calls
   to take these variables into account. Second, all local function
   declarations are collected and lifted to the top-level.
-}
{-# LANGUAGE CPP #-}
module Transformations.Lift (lift) where

#if __GLASGOW_HASKELL__ < 710
import           Control.Applicative        ((<$>), (<*>))
#endif
import           Control.Arrow              (first)
import qualified Control.Monad.State as S   (State, runState, gets, modify)
import           Data.List
import qualified Data.Map            as Map (Map, empty, insert, lookup)
import           Data.Maybe                 (mapMaybe, fromJust)
import qualified Data.Set            as Set (fromList, toList, unions)

import Curry.Base.Ident
import Curry.Base.SpanInfo
import Curry.Syntax

import Base.AnnotExpr
import Base.Expr
import Base.Messages                        (internalError)
import Base.SCC
import Base.Types
import Base.TypeSubst
import Base.Typing
import Base.Utils

import Env.Value

lift :: ValueEnv -> Module Type -> (Module Type, ValueEnv)
lift :: ValueEnv -> Module Type -> (Module Type, ValueEnv)
lift vEnv :: ValueEnv
vEnv (Module spi :: SpanInfo
spi li :: LayoutInfo
li ps :: [ModulePragma]
ps m :: ModuleIdent
m es :: Maybe ExportSpec
es is :: [ImportDecl]
is ds :: [Decl Type]
ds) = (Module Type
lifted, LiftState -> ValueEnv
valueEnv LiftState
s')
  where
  (ds' :: [Decl Type]
ds', s' :: LiftState
s') = State LiftState [Decl Type]
-> LiftState -> ([Decl Type], LiftState)
forall s a. State s a -> s -> (a, s)
S.runState ((Decl Type -> StateT LiftState Identity (Decl Type))
-> [Decl Type] -> State LiftState [Decl Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String
-> [Ident] -> Decl Type -> StateT LiftState Identity (Decl Type)
absDecl "" []) [Decl Type]
ds) LiftState
initState
  initState :: LiftState
initState = ModuleIdent -> ValueEnv -> AbstractEnv -> LiftState
LiftState ModuleIdent
m ValueEnv
vEnv AbstractEnv
forall k a. Map k a
Map.empty
  lifted :: Module Type
lifted    = SpanInfo
-> LayoutInfo
-> [ModulePragma]
-> ModuleIdent
-> Maybe ExportSpec
-> [ImportDecl]
-> [Decl Type]
-> Module Type
forall a.
SpanInfo
-> LayoutInfo
-> [ModulePragma]
-> ModuleIdent
-> Maybe ExportSpec
-> [ImportDecl]
-> [Decl a]
-> Module a
Module SpanInfo
spi LayoutInfo
li [ModulePragma]
ps ModuleIdent
m Maybe ExportSpec
es [ImportDecl]
is ([Decl Type] -> Module Type) -> [Decl Type] -> Module Type
forall a b. (a -> b) -> a -> b
$ (Decl Type -> [Decl Type]) -> [Decl Type] -> [Decl Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Decl Type -> [Decl Type]
forall a. Eq a => Decl a -> [Decl a]
liftFunDecl [Decl Type]
ds'

-- -----------------------------------------------------------------------------
-- Abstraction
-- -----------------------------------------------------------------------------

-- Besides adding the free variables to every (local) function, the
-- abstraction pass also has to update the type environment in order to
-- reflect the new types of the abstracted functions. As usual, we use a
-- state monad transformer in order to pass the type environment
-- through. The environment constructed in the abstraction phase maps
-- each local function declaration onto its replacement expression,
-- i.e. the function applied to its free variables. In order to generate
-- correct type annotations for an inserted replacement expression, we also
-- save a function's original type. The original type is later unified with
-- the concrete type of the replaced expression to obtain a type substitution
-- which is then applied to the replacement expression.

type AbstractEnv = Map.Map Ident (Expression Type, Type)

data LiftState = LiftState
  { LiftState -> ModuleIdent
moduleIdent :: ModuleIdent
  , LiftState -> ValueEnv
valueEnv    :: ValueEnv
  , LiftState -> AbstractEnv
abstractEnv :: AbstractEnv
  }

type LiftM a = S.State LiftState a

getModuleIdent :: LiftM ModuleIdent
getModuleIdent :: LiftM ModuleIdent
getModuleIdent = (LiftState -> ModuleIdent) -> LiftM ModuleIdent
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets LiftState -> ModuleIdent
moduleIdent

getValueEnv :: LiftM ValueEnv
getValueEnv :: LiftM ValueEnv
getValueEnv = (LiftState -> ValueEnv) -> LiftM ValueEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets LiftState -> ValueEnv
valueEnv

modifyValueEnv :: (ValueEnv -> ValueEnv) -> LiftM ()
modifyValueEnv :: (ValueEnv -> ValueEnv) -> LiftM ()
modifyValueEnv f :: ValueEnv -> ValueEnv
f = (LiftState -> LiftState) -> LiftM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify ((LiftState -> LiftState) -> LiftM ())
-> (LiftState -> LiftState) -> LiftM ()
forall a b. (a -> b) -> a -> b
$ \s :: LiftState
s -> LiftState
s { valueEnv :: ValueEnv
valueEnv = ValueEnv -> ValueEnv
f (ValueEnv -> ValueEnv) -> ValueEnv -> ValueEnv
forall a b. (a -> b) -> a -> b
$ LiftState -> ValueEnv
valueEnv LiftState
s }

getAbstractEnv :: LiftM AbstractEnv
getAbstractEnv :: LiftM AbstractEnv
getAbstractEnv = (LiftState -> AbstractEnv) -> LiftM AbstractEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets LiftState -> AbstractEnv
abstractEnv

withLocalAbstractEnv :: AbstractEnv -> LiftM a -> LiftM a
withLocalAbstractEnv :: AbstractEnv -> LiftM a -> LiftM a
withLocalAbstractEnv ae :: AbstractEnv
ae act :: LiftM a
act = do
  AbstractEnv
old <- LiftM AbstractEnv
getAbstractEnv
  (LiftState -> LiftState) -> LiftM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify ((LiftState -> LiftState) -> LiftM ())
-> (LiftState -> LiftState) -> LiftM ()
forall a b. (a -> b) -> a -> b
$ \s :: LiftState
s -> LiftState
s { abstractEnv :: AbstractEnv
abstractEnv = AbstractEnv
ae }
  a
res <- LiftM a
act
  (LiftState -> LiftState) -> LiftM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify ((LiftState -> LiftState) -> LiftM ())
-> (LiftState -> LiftState) -> LiftM ()
forall a b. (a -> b) -> a -> b
$ \s :: LiftState
s -> LiftState
s { abstractEnv :: AbstractEnv
abstractEnv = AbstractEnv
old }
  a -> LiftM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res

absDecl :: String -> [Ident] -> Decl Type -> LiftM (Decl Type)
absDecl :: String
-> [Ident] -> Decl Type -> StateT LiftState Identity (Decl Type)
absDecl _   lvs :: [Ident]
lvs (FunctionDecl p :: SpanInfo
p ty :: Type
ty f :: Ident
f eqs :: [Equation Type]
eqs) = SpanInfo -> Type -> Ident -> [Equation Type] -> Decl Type
forall a. SpanInfo -> a -> Ident -> [Equation a] -> Decl a
FunctionDecl SpanInfo
p Type
ty Ident
f
                                            ([Equation Type] -> Decl Type)
-> StateT LiftState Identity [Equation Type]
-> StateT LiftState Identity (Decl Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Equation Type -> StateT LiftState Identity (Equation Type))
-> [Equation Type] -> StateT LiftState Identity [Equation Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Ident]
-> Equation Type -> StateT LiftState Identity (Equation Type)
absEquation [Ident]
lvs) [Equation Type]
eqs
absDecl pre :: String
pre lvs :: [Ident]
lvs (PatternDecl     p :: SpanInfo
p t :: Pattern Type
t rhs :: Rhs Type
rhs) = SpanInfo -> Pattern Type -> Rhs Type -> Decl Type
forall a. SpanInfo -> Pattern a -> Rhs a -> Decl a
PatternDecl SpanInfo
p Pattern Type
t
                                            (Rhs Type -> Decl Type)
-> StateT LiftState Identity (Rhs Type)
-> StateT LiftState Identity (Decl Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [Ident] -> Rhs Type -> StateT LiftState Identity (Rhs Type)
absRhs String
pre [Ident]
lvs Rhs Type
rhs
absDecl _   _   d :: Decl Type
d                         = Decl Type -> StateT LiftState Identity (Decl Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Decl Type
d

absEquation :: [Ident] -> Equation Type -> LiftM (Equation Type)
absEquation :: [Ident]
-> Equation Type -> StateT LiftState Identity (Equation Type)
absEquation lvs :: [Ident]
lvs (Equation p :: SpanInfo
p lhs :: Lhs Type
lhs@(FunLhs _ f :: Ident
f ts :: [Pattern Type]
ts) rhs :: Rhs Type
rhs) =
  SpanInfo -> Lhs Type -> Rhs Type -> Equation Type
forall a. SpanInfo -> Lhs a -> Rhs a -> Equation a
Equation SpanInfo
p Lhs Type
lhs (Rhs Type -> Equation Type)
-> StateT LiftState Identity (Rhs Type)
-> StateT LiftState Identity (Equation Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [Ident] -> Rhs Type -> StateT LiftState Identity (Rhs Type)
absRhs (Ident -> String
idName Ident
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".") [Ident]
lvs' Rhs Type
rhs
  where lvs' :: [Ident]
lvs' = [Ident]
lvs [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ [Pattern Type] -> [Ident]
forall e. QuantExpr e => e -> [Ident]
bv [Pattern Type]
ts
absEquation _ _ = String -> StateT LiftState Identity (Equation Type)
forall a. HasCallStack => String -> a
error "Lift.absEquation: no pattern match"

absRhs :: String -> [Ident] -> Rhs Type -> LiftM (Rhs Type)
absRhs :: String
-> [Ident] -> Rhs Type -> StateT LiftState Identity (Rhs Type)
absRhs pre :: String
pre lvs :: [Ident]
lvs (SimpleRhs p :: SpanInfo
p _ e :: Expression Type
e _) = SpanInfo -> Expression Type -> Rhs Type
forall a. SpanInfo -> Expression a -> Rhs a
simpleRhs SpanInfo
p (Expression Type -> Rhs Type)
-> StateT LiftState Identity (Expression Type)
-> StateT LiftState Identity (Rhs Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [Ident]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absExpr String
pre [Ident]
lvs Expression Type
e
absRhs _   _   _                   = String -> StateT LiftState Identity (Rhs Type)
forall a. HasCallStack => String -> a
error "Lift.absRhs: no simple RHS"

-- Within a declaration group we have to split the list of declarations
-- into the function and value declarations. Only the function
-- declarations are affected by the abstraction algorithm; the value
-- declarations are left unchanged except for abstracting their right
-- hand sides.

-- The abstraction of a recursive declaration group is complicated by the
-- fact that not all functions need to call each in a recursive
-- declaration group. E.g., in the following example neither 'g' nor 'h'
-- call each other.
--
--   f = g True
--     where x = h 1
--           h z = y + z
--           y = g False
--           g z = if z then x else 0
--
-- Because of this fact, 'g' and 'h' can be abstracted separately by adding
-- only 'y' to 'h' and 'x' to 'g'. On the other hand, in the following example
--
--   f x y = g 4
--     where g p = h p + x
--           h q = k + y + q
--           k = g x
--
-- the local function 'g' uses 'h', so the free variables
-- of 'h' have to be added to 'g' as well. However, because
-- 'h' does not call 'g' it is sufficient to add only
-- 'k' and 'y' (and not 'x') to its definition. We handle this by computing
-- the dependency graph between the functions and splitting this graph into
-- its strongly connected components. Each component is then processed
-- separately, adding the free variables in the group to its functions.

-- We have to be careful with local declarations within desugared case
-- expressions. If some of the cases have guards, e.g.,
--
--   case e of
--     x | x < 1 -> 1
--     x -> let double y = y * y in double x
--
-- the desugarer at present may duplicate code. While there is no problem
-- with local variable declaration being duplicated, we must avoid to
-- lift local function declarations more than once. Therefore
-- 'absFunDecls' transforms only those function declarations
-- that have not been lifted and discards the other declarations. Note
-- that it is easy to check whether a function has been lifted by
-- checking whether an entry for its transformed name is present
-- in the value environment.

absDeclGroup :: String -> [Ident] -> [Decl Type] -> Expression Type
             -> LiftM (Expression Type)
absDeclGroup :: String
-> [Ident]
-> [Decl Type]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absDeclGroup pre :: String
pre lvs :: [Ident]
lvs ds :: [Decl Type]
ds e :: Expression Type
e = do
  ModuleIdent
m <- LiftM ModuleIdent
getModuleIdent
  String
-> [Ident]
-> [[Decl Type]]
-> [Decl Type]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absFunDecls String
pre [Ident]
lvs' ((Decl Type -> [Ident])
-> (Decl Type -> [Ident]) -> [Decl Type] -> [[Decl Type]]
forall b a. Eq b => (a -> [b]) -> (a -> [b]) -> [a] -> [[a]]
scc Decl Type -> [Ident]
forall e. QuantExpr e => e -> [Ident]
bv (ModuleIdent -> Decl Type -> [Ident]
forall e. QualExpr e => ModuleIdent -> e -> [Ident]
qfv ModuleIdent
m) [Decl Type]
fds) [Decl Type]
vds Expression Type
e
  where lvs' :: [Ident]
lvs' = [Ident]
lvs [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ [Decl Type] -> [Ident]
forall e. QuantExpr e => e -> [Ident]
bv [Decl Type]
vds
        (fds :: [Decl Type]
fds, vds :: [Decl Type]
vds) = (Decl Type -> Bool) -> [Decl Type] -> ([Decl Type], [Decl Type])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Decl Type -> Bool
forall a. Decl a -> Bool
isFunDecl [Decl Type]
ds

absFunDecls :: String -> [Ident] -> [[Decl Type]] -> [Decl Type]
            -> Expression Type -> LiftM (Expression Type)
absFunDecls :: String
-> [Ident]
-> [[Decl Type]]
-> [Decl Type]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absFunDecls pre :: String
pre lvs :: [Ident]
lvs []         vds :: [Decl Type]
vds e :: Expression Type
e = do
  [Decl Type]
vds' <- (Decl Type -> StateT LiftState Identity (Decl Type))
-> [Decl Type] -> State LiftState [Decl Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String
-> [Ident] -> Decl Type -> StateT LiftState Identity (Decl Type)
absDecl String
pre [Ident]
lvs) [Decl Type]
vds
  Expression Type
e' <- String
-> [Ident]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absExpr String
pre [Ident]
lvs Expression Type
e
  Expression Type -> StateT LiftState Identity (Expression Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl Type] -> Expression Type -> Expression Type
forall a. [Decl a] -> Expression a -> Expression a
mkLet [Decl Type]
vds' Expression Type
e')
absFunDecls pre :: String
pre lvs :: [Ident]
lvs (fds :: [Decl Type]
fds:fdss :: [[Decl Type]]
fdss) vds :: [Decl Type]
vds e :: Expression Type
e = do
  ModuleIdent
m <- LiftM ModuleIdent
getModuleIdent
  AbstractEnv
env <- LiftM AbstractEnv
getAbstractEnv
  ValueEnv
vEnv <- LiftM ValueEnv
getValueEnv
  let -- defined functions
      fs :: [Ident]
fs      = [Decl Type] -> [Ident]
forall e. QuantExpr e => e -> [Ident]
bv [Decl Type]
fds
      -- function types
      ftys :: [(Ident, Type)]
ftys    = (Decl Type -> (Ident, Type)) -> [Decl Type] -> [(Ident, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Decl Type -> (Ident, Type)
forall a. Typeable a => Decl a -> (Ident, Type)
extractFty [Decl Type]
fds
      extractFty :: Decl a -> (Ident, Type)
extractFty (FunctionDecl _ _ f :: Ident
f (Equation _ (FunLhs _ _ ts :: [Pattern a]
ts) rhs :: Rhs a
rhs : _)) =
        (Ident
f, (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
TypeArrow (Rhs a -> Type
forall a. Typeable a => a -> Type
typeOf Rhs a
rhs) ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Pattern a -> Type) -> [Pattern a] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Pattern a -> Type
forall a. Typeable a => a -> Type
typeOf [Pattern a]
ts)
      extractFty _                                                         =
        String -> (Ident, Type)
forall a. String -> a
internalError "Lift.absFunDecls.extractFty"
      -- typed free variables on the right-hand sides
      fvsRhs :: Set (Type, Ident)
fvsRhs  = [Set (Type, Ident)] -> Set (Type, Ident)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
                  [ [(Type, Ident)] -> Set (Type, Ident)
forall a. Ord a => [a] -> Set a
Set.fromList (((Type, Ident) -> Bool) -> [(Type, Ident)] -> [(Type, Ident)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Type, Ident) -> Bool) -> (Type, Ident) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isDummyType (Type -> Bool) -> ((Type, Ident) -> Type) -> (Type, Ident) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Ident) -> Type
forall a b. (a, b) -> a
fst)
                                         ([(Type, Ident)]
-> ((Expression Type, Type) -> [(Type, Ident)])
-> Maybe (Expression Type, Type)
-> [(Type, Ident)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(Type
ty, Ident
v)]
                                                (Type -> (Expression Type, Type) -> [(Type, Ident)]
forall (e :: * -> *).
QualAnnotExpr e =>
Type -> (e Type, Type) -> [(Type, Ident)]
qafv' Type
ty)
                                                (Ident -> AbstractEnv -> Maybe (Expression Type, Type)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
v AbstractEnv
env)))
                  | (ty :: Type
ty, v :: Ident
v) <- (Decl Type -> [(Type, Ident)]) -> [Decl Type] -> [(Type, Ident)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ModuleIdent -> Decl Type -> [(Type, Ident)]
forall (e :: * -> *).
QualAnnotExpr e =>
ModuleIdent -> e Type -> [(Type, Ident)]
qafv ModuleIdent
m) [Decl Type]
fds ]
      -- !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      -- !!! HACK: When calculating the typed free variables on the     !!!
      -- !!! right-hand side, we have to filter out the ones annotated  !!!
      -- !!! with dummy types (see below). Additionally, we have to be  !!!
      -- !!! careful when we calculate the typed free variables in a    !!!
      -- !!! replacement expression: We have to unify the original      !!!
      -- !!! function type with the instantiated function type in order !!!
      -- !!! to obtain a type substitution that can then be applied to  !!!
      -- !!! the typed free variables in the replacement expression.    !!!
      -- !!! This is analogous to the procedure when inserting a        !!!
      -- !!! replacement expression with a correct type annotation      !!!
      -- !!! (see 'absType' in 'absExpr' below).                        !!!
      -- !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      qafv' :: Type -> (e Type, Type) -> [(Type, Ident)]
qafv' ty :: Type
ty (re :: e Type
re, fty :: Type
fty) =
        let unifier :: TypeSubst
unifier = Type -> Type -> TypeSubst -> TypeSubst
matchType Type
fty Type
ty TypeSubst
forall a b. Subst a b
idSubst
        in  ((Type, Ident) -> (Type, Ident))
-> [(Type, Ident)] -> [(Type, Ident)]
forall a b. (a -> b) -> [a] -> [b]
map (\(ty' :: Type
ty', v :: Ident
v) -> (TypeSubst -> Type -> Type
forall a. SubstType a => TypeSubst -> a -> a
subst TypeSubst
unifier Type
ty', Ident
v)) ([(Type, Ident)] -> [(Type, Ident)])
-> [(Type, Ident)] -> [(Type, Ident)]
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> e Type -> [(Type, Ident)]
forall (e :: * -> *).
QualAnnotExpr e =>
ModuleIdent -> e Type -> [(Type, Ident)]
qafv ModuleIdent
m e Type
re
      -- free variables that are local
      fvs :: [(Type, Ident)]
fvs     = ((Type, Ident) -> Bool) -> [(Type, Ident)] -> [(Type, Ident)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ident]
lvs) (Ident -> Bool)
-> ((Type, Ident) -> Ident) -> (Type, Ident) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Ident) -> Ident
forall a b. (a, b) -> b
snd) (Set (Type, Ident) -> [(Type, Ident)]
forall a. Set a -> [a]
Set.toList Set (Type, Ident)
fvsRhs)
      -- extended abstraction environment
      env' :: AbstractEnv
env'    = (Ident -> AbstractEnv -> AbstractEnv)
-> AbstractEnv -> [Ident] -> AbstractEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ident -> AbstractEnv -> AbstractEnv
bindF AbstractEnv
env [Ident]
fs
      -- !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      -- !!! HACK: Since we do not know how to annotate the function    !!!
      -- !!! call within the replacement expression until the replace-  !!!                          !!!
      -- !!! ment expression is actually inserted (see 'absType' in     !!!
      -- !!! 'absExpr' below), we use a dummy type for this. In turn,   !!!
      -- !!! this dummy type has to be filtered out when calculating    !!!
      -- !!! the typed free variables on right-hand sides (see above).  !!!                                             !!!
      -- !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      bindF :: Ident -> AbstractEnv -> AbstractEnv
bindF f :: Ident
f =
        Ident -> (Expression Type, Type) -> AbstractEnv -> AbstractEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
f ( Expression Type -> [Expression Type] -> Expression Type
forall a. Expression a -> [Expression a] -> Expression a
apply (ModuleIdent -> String -> Type -> Ident -> Expression Type
forall a. ModuleIdent -> String -> a -> Ident -> Expression a
mkFun ModuleIdent
m String
pre Type
dummyType Ident
f) (((Type, Ident) -> Expression Type)
-> [(Type, Ident)] -> [Expression Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Ident -> Expression Type)
-> (Type, Ident) -> Expression Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Ident -> Expression Type
forall a. a -> Ident -> Expression a
mkVar) [(Type, Ident)]
fvs)
                     , Maybe Type -> Type
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Type -> Type) -> Maybe Type -> Type
forall a b. (a -> b) -> a -> b
$ Ident -> [(Ident, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
f [(Ident, Type)]
ftys )
      -- newly abstracted functions
      fs' :: [Ident]
fs'     = (Ident -> Bool) -> [Ident] -> [Ident]
forall a. (a -> Bool) -> [a] -> [a]
filter (\f :: Ident
f -> [ValueInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([ValueInfo] -> Bool) -> [ValueInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ Ident -> ValueEnv -> [ValueInfo]
lookupValue (String -> Ident -> Ident
liftIdent String
pre Ident
f) ValueEnv
vEnv) [Ident]
fs
  AbstractEnv
-> StateT LiftState Identity (Expression Type)
-> StateT LiftState Identity (Expression Type)
forall a. AbstractEnv -> LiftM a -> LiftM a
withLocalAbstractEnv AbstractEnv
env' (StateT LiftState Identity (Expression Type)
 -> StateT LiftState Identity (Expression Type))
-> StateT LiftState Identity (Expression Type)
-> StateT LiftState Identity (Expression Type)
forall a b. (a -> b) -> a -> b
$ do
    -- add variables to functions
    [Decl Type]
fds' <- (Decl Type -> StateT LiftState Identity (Decl Type))
-> [Decl Type] -> State LiftState [Decl Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String
-> [(Type, Ident)]
-> [Ident]
-> Decl Type
-> StateT LiftState Identity (Decl Type)
absFunDecl String
pre [(Type, Ident)]
fvs [Ident]
lvs) [Decl Type
d | Decl Type
d <- [Decl Type]
fds, (Ident -> Bool) -> [Ident] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ident]
fs') (Decl Type -> [Ident]
forall e. QuantExpr e => e -> [Ident]
bv Decl Type
d)]
    -- abstract remaining declarations
    Expression Type
e'   <- String
-> [Ident]
-> [[Decl Type]]
-> [Decl Type]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absFunDecls String
pre [Ident]
lvs [[Decl Type]]
fdss [Decl Type]
vds Expression Type
e
    Expression Type -> StateT LiftState Identity (Expression Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl Type] -> Expression Type -> Expression Type
forall a. [Decl a] -> Expression a -> Expression a
mkLet [Decl Type]
fds' Expression Type
e')

-- When the free variables of a function are abstracted, the type of the
-- function must be changed as well.

absFunDecl :: String -> [(Type, Ident)] -> [Ident] -> Decl Type
           -> LiftM (Decl Type)
absFunDecl :: String
-> [(Type, Ident)]
-> [Ident]
-> Decl Type
-> StateT LiftState Identity (Decl Type)
absFunDecl pre :: String
pre fvs :: [(Type, Ident)]
fvs lvs :: [Ident]
lvs (FunctionDecl p :: SpanInfo
p _ f :: Ident
f eqs :: [Equation Type]
eqs) = do
  ModuleIdent
m <- LiftM ModuleIdent
getModuleIdent
  Decl Type
d <- String
-> [Ident] -> Decl Type -> StateT LiftState Identity (Decl Type)
absDecl String
pre [Ident]
lvs (Decl Type -> StateT LiftState Identity (Decl Type))
-> Decl Type -> StateT LiftState Identity (Decl Type)
forall a b. (a -> b) -> a -> b
$ SpanInfo -> Type -> Ident -> [Equation Type] -> Decl Type
forall a. SpanInfo -> a -> Ident -> [Equation a] -> Decl a
FunctionDecl SpanInfo
p Type
forall a. HasCallStack => a
undefined Ident
f' [Equation Type]
eqs'
  let FunctionDecl _ _ _ eqs'' :: [Equation Type]
eqs'' = Decl Type
d
  (ValueEnv -> ValueEnv) -> LiftM ()
modifyValueEnv ((ValueEnv -> ValueEnv) -> LiftM ())
-> (ValueEnv -> ValueEnv) -> LiftM ()
forall a b. (a -> b) -> a -> b
$ (QualIdent -> TypeScheme -> ValueInfo)
-> ModuleIdent -> Ident -> TypeScheme -> ValueEnv -> ValueEnv
forall a.
(QualIdent -> a -> ValueInfo)
-> ModuleIdent -> Ident -> a -> ValueEnv -> ValueEnv
bindGlobalInfo
    (\qf :: QualIdent
qf tySc :: TypeScheme
tySc -> QualIdent -> Maybe QualIdent -> Int -> TypeScheme -> ValueInfo
Value QualIdent
qf Maybe QualIdent
forall a. Maybe a
Nothing (Equation Type -> Int
forall a. Equation a -> Int
eqnArity (Equation Type -> Int) -> Equation Type -> Int
forall a b. (a -> b) -> a -> b
$ [Equation Type] -> Equation Type
forall a. [a] -> a
head [Equation Type]
eqs') TypeScheme
tySc) ModuleIdent
m Ident
f' (TypeScheme -> ValueEnv -> ValueEnv)
-> TypeScheme -> ValueEnv -> ValueEnv
forall a b. (a -> b) -> a -> b
$
                 Type -> TypeScheme
polyType Type
ty''
  Decl Type -> StateT LiftState Identity (Decl Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl Type -> StateT LiftState Identity (Decl Type))
-> Decl Type -> StateT LiftState Identity (Decl Type)
forall a b. (a -> b) -> a -> b
$ SpanInfo -> Type -> Ident -> [Equation Type] -> Decl Type
forall a. SpanInfo -> a -> Ident -> [Equation a] -> Decl a
FunctionDecl SpanInfo
p Type
ty'' Ident
f' [Equation Type]
eqs''
  where f' :: Ident
f' = String -> Ident -> Ident
liftIdent String
pre Ident
f
        ty' :: Type
ty' = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
TypeArrow (Rhs Type -> Type
forall a. Typeable a => a -> Type
typeOf Rhs Type
rhs') ((Pattern Type -> Type) -> [Pattern Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Pattern Type -> Type
forall a. Typeable a => a -> Type
typeOf [Pattern Type]
ts')
          where Equation _ (FunLhs _ _ ts' :: [Pattern Type]
ts') rhs' :: Rhs Type
rhs' = [Equation Type] -> Equation Type
forall a. [a] -> a
head [Equation Type]
eqs'
        ty'' :: Type
ty'' = Type -> Type
forall t. (SubstType t, IsType t) => t -> t
genType Type
ty'
        eqs' :: [Equation Type]
eqs' = (Equation Type -> Equation Type)
-> [Equation Type] -> [Equation Type]
forall a b. (a -> b) -> [a] -> [b]
map Equation Type -> Equation Type
addVars [Equation Type]
eqs
        genType :: t -> t
genType ty''' :: t
ty''' = TypeSubst -> t -> t
forall a. SubstType a => TypeSubst -> a -> a
subst ((Int -> Type -> TypeSubst -> TypeSubst)
-> TypeSubst -> [Int] -> [Type] -> TypeSubst
forall a b c. (a -> b -> c -> c) -> c -> [a] -> [b] -> c
foldr2 Int -> Type -> TypeSubst -> TypeSubst
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst TypeSubst
forall a b. Subst a b
idSubst [Int]
tvs [Type]
tvs') t
ty'''
          where tvs :: [Int]
tvs = [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub (t -> [Int]
forall t. IsType t => t -> [Int]
typeVars t
ty''')
                tvs' :: [Type]
tvs' = (Int -> Type) -> [Int] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Type
TypeVariable [0 ..]
        addVars :: Equation Type -> Equation Type
addVars (Equation p' :: SpanInfo
p' (FunLhs _ _ ts :: [Pattern Type]
ts) rhs :: Rhs Type
rhs) =
          SpanInfo -> Lhs Type -> Rhs Type -> Equation Type
forall a. SpanInfo -> Lhs a -> Rhs a -> Equation a
Equation SpanInfo
p' (SpanInfo -> Ident -> [Pattern Type] -> Lhs Type
forall a. SpanInfo -> Ident -> [Pattern a] -> Lhs a
FunLhs SpanInfo
NoSpanInfo
            Ident
f' (((Type, Ident) -> Pattern Type)
-> [(Type, Ident)] -> [Pattern Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Ident -> Pattern Type) -> (Type, Ident) -> Pattern Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SpanInfo -> Type -> Ident -> Pattern Type
forall a. SpanInfo -> a -> Ident -> Pattern a
VariablePattern SpanInfo
NoSpanInfo)) [(Type, Ident)]
fvs [Pattern Type] -> [Pattern Type] -> [Pattern Type]
forall a. [a] -> [a] -> [a]
++ [Pattern Type]
ts)) Rhs Type
rhs
        addVars _ = String -> Equation Type
forall a. HasCallStack => String -> a
error "Lift.absFunDecl.addVars: no pattern match"
absFunDecl pre :: String
pre _ _ (ExternalDecl p :: SpanInfo
p vs :: [Var Type]
vs) = SpanInfo -> [Var Type] -> Decl Type
forall a. SpanInfo -> [Var a] -> Decl a
ExternalDecl SpanInfo
p ([Var Type] -> Decl Type)
-> StateT LiftState Identity [Var Type]
-> StateT LiftState Identity (Decl Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var Type -> StateT LiftState Identity (Var Type))
-> [Var Type] -> StateT LiftState Identity [Var Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Var Type -> StateT LiftState Identity (Var Type)
absVar String
pre) [Var Type]
vs
absFunDecl _ _ _ _ = String -> StateT LiftState Identity (Decl Type)
forall a. HasCallStack => String -> a
error "Lift.absFunDecl: no pattern match"

absVar :: String -> Var Type -> LiftM (Var Type)
absVar :: String -> Var Type -> StateT LiftState Identity (Var Type)
absVar pre :: String
pre (Var ty :: Type
ty f :: Ident
f) = do
  ModuleIdent
m <- LiftM ModuleIdent
getModuleIdent
  (ValueEnv -> ValueEnv) -> LiftM ()
modifyValueEnv ((ValueEnv -> ValueEnv) -> LiftM ())
-> (ValueEnv -> ValueEnv) -> LiftM ()
forall a b. (a -> b) -> a -> b
$ (QualIdent -> TypeScheme -> ValueInfo)
-> ModuleIdent -> Ident -> TypeScheme -> ValueEnv -> ValueEnv
forall a.
(QualIdent -> a -> ValueInfo)
-> ModuleIdent -> Ident -> a -> ValueEnv -> ValueEnv
bindGlobalInfo
    (\qf :: QualIdent
qf tySc :: TypeScheme
tySc -> QualIdent -> Maybe QualIdent -> Int -> TypeScheme -> ValueInfo
Value QualIdent
qf Maybe QualIdent
forall a. Maybe a
Nothing (Type -> Int
arrowArity Type
ty) TypeScheme
tySc) ModuleIdent
m Ident
f' (TypeScheme -> ValueEnv -> ValueEnv)
-> TypeScheme -> ValueEnv -> ValueEnv
forall a b. (a -> b) -> a -> b
$ Type -> TypeScheme
polyType Type
ty
  Var Type -> StateT LiftState Identity (Var Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Var Type -> StateT LiftState Identity (Var Type))
-> Var Type -> StateT LiftState Identity (Var Type)
forall a b. (a -> b) -> a -> b
$ Type -> Ident -> Var Type
forall a. a -> Ident -> Var a
Var Type
ty Ident
f'
  where f' :: Ident
f' = String -> Ident -> Ident
liftIdent String
pre Ident
f

absExpr :: String -> [Ident] -> Expression Type -> LiftM (Expression Type)
absExpr :: String
-> [Ident]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absExpr _   _   l :: Expression Type
l@(Literal     _ _ _) = Expression Type -> StateT LiftState Identity (Expression Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Expression Type
l
absExpr pre :: String
pre lvs :: [Ident]
lvs var :: Expression Type
var@(Variable _ ty :: Type
ty v :: QualIdent
v)
  | QualIdent -> Bool
isQualified QualIdent
v = Expression Type -> StateT LiftState Identity (Expression Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Expression Type
var
  | Bool
otherwise     = do
    LiftM AbstractEnv
getAbstractEnv LiftM AbstractEnv
-> (AbstractEnv -> StateT LiftState Identity (Expression Type))
-> StateT LiftState Identity (Expression Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \env :: AbstractEnv
env -> case Ident -> AbstractEnv -> Maybe (Expression Type, Type)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (QualIdent -> Ident
unqualify QualIdent
v) AbstractEnv
env of
      Nothing       -> Expression Type -> StateT LiftState Identity (Expression Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Expression Type
var
      Just (e :: Expression Type
e, fty :: Type
fty) -> let unifier :: TypeSubst
unifier = Type -> Type -> TypeSubst -> TypeSubst
matchType Type
fty Type
ty TypeSubst
forall a b. Subst a b
idSubst
                       in  String
-> [Ident]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absExpr String
pre [Ident]
lvs (Expression Type -> StateT LiftState Identity (Expression Type))
-> Expression Type -> StateT LiftState Identity (Expression Type)
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> Expression Type -> Expression Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeSubst -> Type -> Type
forall a. SubstType a => TypeSubst -> a -> a
subst TypeSubst
unifier) (Expression Type -> Expression Type)
-> Expression Type -> Expression Type
forall a b. (a -> b) -> a -> b
$ Type -> Expression Type -> Expression Type
absType Type
ty Expression Type
e
  where -- !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
        -- !!! HACK: When inserting the replacement expression for an     !!!
        -- !!! abstracted function, we have to unify the original         !!!
        -- !!! function type with the instantiated function type in order !!!
        -- !!! to obtain a type substitution that can then be applied to  !!!
        -- !!! the type annotations in the replacement expression.        !!!
        -- !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
        absType :: Type -> Expression Type -> Expression Type
absType ty' :: Type
ty' (Variable spi :: SpanInfo
spi _ v' :: QualIdent
v') = SpanInfo -> Type -> QualIdent -> Expression Type
forall a. SpanInfo -> a -> QualIdent -> Expression a
Variable SpanInfo
spi Type
ty' QualIdent
v'
        absType ty' :: Type
ty' (Apply   spi :: SpanInfo
spi e1 :: Expression Type
e1 e2 :: Expression Type
e2) =
          SpanInfo -> Expression Type -> Expression Type -> Expression Type
forall a. SpanInfo -> Expression a -> Expression a -> Expression a
Apply SpanInfo
spi (Type -> Expression Type -> Expression Type
absType (Type -> Type -> Type
TypeArrow (Expression Type -> Type
forall a. Typeable a => a -> Type
typeOf Expression Type
e2) Type
ty') Expression Type
e1) Expression Type
e2
        absType _ _ = String -> Expression Type
forall a. String -> a
internalError "Lift.absExpr.absType"
absExpr _   _   c :: Expression Type
c@(Constructor _ _ _) = Expression Type -> StateT LiftState Identity (Expression Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Expression Type
c
absExpr pre :: String
pre lvs :: [Ident]
lvs (Apply       spi :: SpanInfo
spi e1 :: Expression Type
e1 e2 :: Expression Type
e2) = SpanInfo -> Expression Type -> Expression Type -> Expression Type
forall a. SpanInfo -> Expression a -> Expression a -> Expression a
Apply SpanInfo
spi (Expression Type -> Expression Type -> Expression Type)
-> StateT LiftState Identity (Expression Type)
-> StateT LiftState Identity (Expression Type -> Expression Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [Ident]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absExpr String
pre [Ident]
lvs Expression Type
e1
                                                    StateT LiftState Identity (Expression Type -> Expression Type)
-> StateT LiftState Identity (Expression Type)
-> StateT LiftState Identity (Expression Type)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String
-> [Ident]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absExpr String
pre [Ident]
lvs Expression Type
e2
absExpr pre :: String
pre lvs :: [Ident]
lvs (Let          _ _ ds :: [Decl Type]
ds e :: Expression Type
e) = String
-> [Ident]
-> [Decl Type]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absDeclGroup String
pre [Ident]
lvs [Decl Type]
ds Expression Type
e
absExpr pre :: String
pre lvs :: [Ident]
lvs (Case      _ _ ct :: CaseType
ct e :: Expression Type
e bs :: [Alt Type]
bs) =
  CaseType -> Expression Type -> [Alt Type] -> Expression Type
forall a. CaseType -> Expression a -> [Alt a] -> Expression a
mkCase CaseType
ct (Expression Type -> [Alt Type] -> Expression Type)
-> StateT LiftState Identity (Expression Type)
-> StateT LiftState Identity ([Alt Type] -> Expression Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [Ident]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absExpr String
pre [Ident]
lvs Expression Type
e StateT LiftState Identity ([Alt Type] -> Expression Type)
-> StateT LiftState Identity [Alt Type]
-> StateT LiftState Identity (Expression Type)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Alt Type -> StateT LiftState Identity (Alt Type))
-> [Alt Type] -> StateT LiftState Identity [Alt Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String
-> [Ident] -> Alt Type -> StateT LiftState Identity (Alt Type)
absAlt String
pre [Ident]
lvs) [Alt Type]
bs
absExpr pre :: String
pre lvs :: [Ident]
lvs (Typed        spi :: SpanInfo
spi e :: Expression Type
e ty :: QualTypeExpr
ty) =
  (Expression Type -> QualTypeExpr -> Expression Type)
-> QualTypeExpr -> Expression Type -> Expression Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip (SpanInfo -> Expression Type -> QualTypeExpr -> Expression Type
forall a. SpanInfo -> Expression a -> QualTypeExpr -> Expression a
Typed SpanInfo
spi) QualTypeExpr
ty (Expression Type -> Expression Type)
-> StateT LiftState Identity (Expression Type)
-> StateT LiftState Identity (Expression Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [Ident]
-> Expression Type
-> StateT LiftState Identity (Expression Type)
absExpr String
pre [Ident]
lvs Expression Type
e
absExpr _   _   e :: Expression Type
e                   = String -> StateT LiftState Identity (Expression Type)
forall a. String -> a
internalError (String -> StateT LiftState Identity (Expression Type))
-> String -> StateT LiftState Identity (Expression Type)
forall a b. (a -> b) -> a -> b
$ "Lift.absExpr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expression Type -> String
forall a. Show a => a -> String
show Expression Type
e

absAlt :: String -> [Ident] -> Alt Type -> LiftM (Alt Type)
absAlt :: String
-> [Ident] -> Alt Type -> StateT LiftState Identity (Alt Type)
absAlt pre :: String
pre lvs :: [Ident]
lvs (Alt p :: SpanInfo
p t :: Pattern Type
t rhs :: Rhs Type
rhs) = SpanInfo -> Pattern Type -> Rhs Type -> Alt Type
forall a. SpanInfo -> Pattern a -> Rhs a -> Alt a
Alt SpanInfo
p Pattern Type
t (Rhs Type -> Alt Type)
-> StateT LiftState Identity (Rhs Type)
-> StateT LiftState Identity (Alt Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [Ident] -> Rhs Type -> StateT LiftState Identity (Rhs Type)
absRhs String
pre [Ident]
lvs' Rhs Type
rhs
  where lvs' :: [Ident]
lvs' = [Ident]
lvs [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ Pattern Type -> [Ident]
forall e. QuantExpr e => e -> [Ident]
bv Pattern Type
t

-- -----------------------------------------------------------------------------
-- Lifting
-- -----------------------------------------------------------------------------

-- After the abstraction pass, all local function declarations are lifted
-- to the top-level.

liftFunDecl :: Eq a => Decl a -> [Decl a]
liftFunDecl :: Decl a -> [Decl a]
liftFunDecl (FunctionDecl p :: SpanInfo
p a :: a
a f :: Ident
f eqs :: [Equation a]
eqs) =
  SpanInfo -> a -> Ident -> [Equation a] -> Decl a
forall a. SpanInfo -> a -> Ident -> [Equation a] -> Decl a
FunctionDecl SpanInfo
p a
a Ident
f [Equation a]
eqs' Decl a -> [Decl a] -> [Decl a]
forall a. a -> [a] -> [a]
: (Decl a -> Decl a) -> [Decl a] -> [Decl a]
forall a b. (a -> b) -> [a] -> [b]
map Decl a -> Decl a
forall a. Eq a => Decl a -> Decl a
renameFunDecl ([[Decl a]] -> [Decl a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Decl a]]
dss')
  where (eqs' :: [Equation a]
eqs', dss' :: [[Decl a]]
dss') = [(Equation a, [Decl a])] -> ([Equation a], [[Decl a]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Equation a, [Decl a])] -> ([Equation a], [[Decl a]]))
-> [(Equation a, [Decl a])] -> ([Equation a], [[Decl a]])
forall a b. (a -> b) -> a -> b
$ (Equation a -> (Equation a, [Decl a]))
-> [Equation a] -> [(Equation a, [Decl a])]
forall a b. (a -> b) -> [a] -> [b]
map Equation a -> (Equation a, [Decl a])
forall a. Eq a => Equation a -> (Equation a, [Decl a])
liftEquation [Equation a]
eqs
liftFunDecl d :: Decl a
d                        = [Decl a
d]

liftVarDecl :: Eq a => Decl a -> (Decl a, [Decl a])
liftVarDecl :: Decl a -> (Decl a, [Decl a])
liftVarDecl (PatternDecl   p :: SpanInfo
p t :: Pattern a
t rhs :: Rhs a
rhs) = (SpanInfo -> Pattern a -> Rhs a -> Decl a
forall a. SpanInfo -> Pattern a -> Rhs a -> Decl a
PatternDecl SpanInfo
p Pattern a
t Rhs a
rhs', [Decl a]
ds')
  where (rhs' :: Rhs a
rhs', ds' :: [Decl a]
ds') = Rhs a -> (Rhs a, [Decl a])
forall a. Eq a => Rhs a -> (Rhs a, [Decl a])
liftRhs Rhs a
rhs
liftVarDecl ex :: Decl a
ex@(FreeDecl       _ _) = (Decl a
ex, [])
liftVarDecl _ = String -> (Decl a, [Decl a])
forall a. HasCallStack => String -> a
error "Lift.liftVarDecl: no pattern match"

liftEquation :: Eq a => Equation a -> (Equation a, [Decl a])
liftEquation :: Equation a -> (Equation a, [Decl a])
liftEquation (Equation p :: SpanInfo
p lhs :: Lhs a
lhs rhs :: Rhs a
rhs) = (SpanInfo -> Lhs a -> Rhs a -> Equation a
forall a. SpanInfo -> Lhs a -> Rhs a -> Equation a
Equation SpanInfo
p Lhs a
lhs Rhs a
rhs', [Decl a]
ds')
  where (rhs' :: Rhs a
rhs', ds' :: [Decl a]
ds') = Rhs a -> (Rhs a, [Decl a])
forall a. Eq a => Rhs a -> (Rhs a, [Decl a])
liftRhs Rhs a
rhs

liftRhs :: Eq a => Rhs a -> (Rhs a, [Decl a])
liftRhs :: Rhs a -> (Rhs a, [Decl a])
liftRhs (SimpleRhs p :: SpanInfo
p _ e :: Expression a
e _) = (Expression a -> Rhs a)
-> (Expression a, [Decl a]) -> (Rhs a, [Decl a])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (SpanInfo -> Expression a -> Rhs a
forall a. SpanInfo -> Expression a -> Rhs a
simpleRhs SpanInfo
p) (Expression a -> (Expression a, [Decl a])
forall a. Eq a => Expression a -> (Expression a, [Decl a])
liftExpr Expression a
e)
liftRhs _                   = String -> (Rhs a, [Decl a])
forall a. HasCallStack => String -> a
error "Lift.liftRhs: no pattern match"

liftDeclGroup :: Eq a => [Decl a] -> ([Decl a], [Decl a])
liftDeclGroup :: [Decl a] -> ([Decl a], [Decl a])
liftDeclGroup ds :: [Decl a]
ds = ([Decl a]
vds', [[Decl a]] -> [Decl a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Decl a -> [Decl a]) -> [Decl a] -> [[Decl a]]
forall a b. (a -> b) -> [a] -> [b]
map Decl a -> [Decl a]
forall a. Eq a => Decl a -> [Decl a]
liftFunDecl [Decl a]
fds [[Decl a]] -> [[Decl a]] -> [[Decl a]]
forall a. [a] -> [a] -> [a]
++ [[Decl a]]
dss'))
  where (fds :: [Decl a]
fds , vds :: [Decl a]
vds ) = (Decl a -> Bool) -> [Decl a] -> ([Decl a], [Decl a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Decl a -> Bool
forall a. Decl a -> Bool
isFunDecl [Decl a]
ds
        (vds' :: [Decl a]
vds', dss' :: [[Decl a]]
dss') = [(Decl a, [Decl a])] -> ([Decl a], [[Decl a]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Decl a, [Decl a])] -> ([Decl a], [[Decl a]]))
-> [(Decl a, [Decl a])] -> ([Decl a], [[Decl a]])
forall a b. (a -> b) -> a -> b
$ (Decl a -> (Decl a, [Decl a])) -> [Decl a] -> [(Decl a, [Decl a])]
forall a b. (a -> b) -> [a] -> [b]
map Decl a -> (Decl a, [Decl a])
forall a. Eq a => Decl a -> (Decl a, [Decl a])
liftVarDecl [Decl a]
vds

liftExpr :: Eq a => Expression a -> (Expression a, [Decl a])
liftExpr :: Expression a -> (Expression a, [Decl a])
liftExpr l :: Expression a
l@(Literal     _ _ _) = (Expression a
l, [])
liftExpr v :: Expression a
v@(Variable    _ _ _) = (Expression a
v, [])
liftExpr c :: Expression a
c@(Constructor _ _ _) = (Expression a
c, [])
liftExpr (Apply       spi :: SpanInfo
spi e1 :: Expression a
e1 e2 :: Expression a
e2) = (SpanInfo -> Expression a -> Expression a -> Expression a
forall a. SpanInfo -> Expression a -> Expression a -> Expression a
Apply SpanInfo
spi Expression a
e1' Expression a
e2', [Decl a]
ds1 [Decl a] -> [Decl a] -> [Decl a]
forall a. [a] -> [a] -> [a]
++ [Decl a]
ds2)
  where (e1' :: Expression a
e1', ds1 :: [Decl a]
ds1) = Expression a -> (Expression a, [Decl a])
forall a. Eq a => Expression a -> (Expression a, [Decl a])
liftExpr Expression a
e1
        (e2' :: Expression a
e2', ds2 :: [Decl a]
ds2) = Expression a -> (Expression a, [Decl a])
forall a. Eq a => Expression a -> (Expression a, [Decl a])
liftExpr Expression a
e2
liftExpr (Let        _ _ ds :: [Decl a]
ds e :: Expression a
e) = ([Decl a] -> Expression a -> Expression a
forall a. [Decl a] -> Expression a -> Expression a
mkLet [Decl a]
ds' Expression a
e', [Decl a]
ds1 [Decl a] -> [Decl a] -> [Decl a]
forall a. [a] -> [a] -> [a]
++ [Decl a]
ds2)
  where (ds' :: [Decl a]
ds', ds1 :: [Decl a]
ds1) = [Decl a] -> ([Decl a], [Decl a])
forall a. Eq a => [Decl a] -> ([Decl a], [Decl a])
liftDeclGroup [Decl a]
ds
        (e' :: Expression a
e' , ds2 :: [Decl a]
ds2) = Expression a -> (Expression a, [Decl a])
forall a. Eq a => Expression a -> (Expression a, [Decl a])
liftExpr Expression a
e
liftExpr (Case    _ _ ct :: CaseType
ct e :: Expression a
e alts :: [Alt a]
alts) = (CaseType -> Expression a -> [Alt a] -> Expression a
forall a. CaseType -> Expression a -> [Alt a] -> Expression a
mkCase CaseType
ct Expression a
e' [Alt a]
alts', [[Decl a]] -> [Decl a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Decl a]] -> [Decl a]) -> [[Decl a]] -> [Decl a]
forall a b. (a -> b) -> a -> b
$ [Decl a]
ds' [Decl a] -> [[Decl a]] -> [[Decl a]]
forall a. a -> [a] -> [a]
: [[Decl a]]
dss')
  where (e' :: Expression a
e'   , ds' :: [Decl a]
ds' ) = Expression a -> (Expression a, [Decl a])
forall a. Eq a => Expression a -> (Expression a, [Decl a])
liftExpr Expression a
e
        (alts' :: [Alt a]
alts', dss' :: [[Decl a]]
dss') = [(Alt a, [Decl a])] -> ([Alt a], [[Decl a]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Alt a, [Decl a])] -> ([Alt a], [[Decl a]]))
-> [(Alt a, [Decl a])] -> ([Alt a], [[Decl a]])
forall a b. (a -> b) -> a -> b
$ (Alt a -> (Alt a, [Decl a])) -> [Alt a] -> [(Alt a, [Decl a])]
forall a b. (a -> b) -> [a] -> [b]
map Alt a -> (Alt a, [Decl a])
forall a. Eq a => Alt a -> (Alt a, [Decl a])
liftAlt [Alt a]
alts
liftExpr (Typed        spi :: SpanInfo
spi e :: Expression a
e ty :: QualTypeExpr
ty) =
  (SpanInfo -> Expression a -> QualTypeExpr -> Expression a
forall a. SpanInfo -> Expression a -> QualTypeExpr -> Expression a
Typed SpanInfo
spi Expression a
e' QualTypeExpr
ty, [Decl a]
ds) where (e' :: Expression a
e', ds :: [Decl a]
ds) = Expression a -> (Expression a, [Decl a])
forall a. Eq a => Expression a -> (Expression a, [Decl a])
liftExpr Expression a
e
liftExpr _ = String -> (Expression a, [Decl a])
forall a. String -> a
internalError "Lift.liftExpr"

liftAlt :: Eq a => Alt a -> (Alt a, [Decl a])
liftAlt :: Alt a -> (Alt a, [Decl a])
liftAlt (Alt p :: SpanInfo
p t :: Pattern a
t rhs :: Rhs a
rhs) = (SpanInfo -> Pattern a -> Rhs a -> Alt a
forall a. SpanInfo -> Pattern a -> Rhs a -> Alt a
Alt SpanInfo
p Pattern a
t Rhs a
rhs', [Decl a]
ds') where (rhs' :: Rhs a
rhs', ds' :: [Decl a]
ds') = Rhs a -> (Rhs a, [Decl a])
forall a. Eq a => Rhs a -> (Rhs a, [Decl a])
liftRhs Rhs a
rhs

-- -----------------------------------------------------------------------------
-- Renaming
-- -----------------------------------------------------------------------------

-- After all local function declarations have been lifted to top-level, we
-- may have to rename duplicate function arguments. Due to polymorphic let
-- declarations it could happen that an argument was added multiple times
-- instantiated with different types during the abstraction pass beforehand.

type RenameMap a = [((a, Ident), Ident)]

renameFunDecl :: Eq a => Decl a -> Decl a
renameFunDecl :: Decl a -> Decl a
renameFunDecl (FunctionDecl p :: SpanInfo
p a :: a
a f :: Ident
f eqs :: [Equation a]
eqs) =
  SpanInfo -> a -> Ident -> [Equation a] -> Decl a
forall a. SpanInfo -> a -> Ident -> [Equation a] -> Decl a
FunctionDecl SpanInfo
p a
a Ident
f ((Equation a -> Equation a) -> [Equation a] -> [Equation a]
forall a b. (a -> b) -> [a] -> [b]
map Equation a -> Equation a
forall a. Eq a => Equation a -> Equation a
renameEquation [Equation a]
eqs)
renameFunDecl d :: Decl a
d                        = Decl a
d

renameEquation :: Eq a => Equation a -> Equation a
renameEquation :: Equation a -> Equation a
renameEquation (Equation p :: SpanInfo
p lhs :: Lhs a
lhs rhs :: Rhs a
rhs) = SpanInfo -> Lhs a -> Rhs a -> Equation a
forall a. SpanInfo -> Lhs a -> Rhs a -> Equation a
Equation SpanInfo
p Lhs a
lhs' (RenameMap a -> Rhs a -> Rhs a
forall a. Eq a => RenameMap a -> Rhs a -> Rhs a
renameRhs RenameMap a
rm Rhs a
rhs)
  where (rm :: RenameMap a
rm, lhs' :: Lhs a
lhs') = Lhs a -> (RenameMap a, Lhs a)
forall a. Eq a => Lhs a -> (RenameMap a, Lhs a)
renameLhs Lhs a
lhs

renameLhs :: Eq a => Lhs a -> (RenameMap a, Lhs a)
renameLhs :: Lhs a -> (RenameMap a, Lhs a)
renameLhs (FunLhs spi :: SpanInfo
spi f :: Ident
f ts :: [Pattern a]
ts) = (RenameMap a
rm, SpanInfo -> Ident -> [Pattern a] -> Lhs a
forall a. SpanInfo -> Ident -> [Pattern a] -> Lhs a
FunLhs SpanInfo
spi Ident
f [Pattern a]
ts')
  where (rm :: RenameMap a
rm, ts' :: [Pattern a]
ts') = (Pattern a
 -> (RenameMap a, [Pattern a]) -> (RenameMap a, [Pattern a]))
-> (RenameMap a, [Pattern a])
-> [Pattern a]
-> (RenameMap a, [Pattern a])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Pattern a
-> (RenameMap a, [Pattern a]) -> (RenameMap a, [Pattern a])
forall a.
Eq a =>
Pattern a
-> (RenameMap a, [Pattern a]) -> (RenameMap a, [Pattern a])
renamePattern ([], []) [Pattern a]
ts
renameLhs _             = String -> (RenameMap a, Lhs a)
forall a. HasCallStack => String -> a
error "Lift.renameLhs"

renamePattern :: Eq a => Pattern a -> (RenameMap a, [Pattern a])
              -> (RenameMap a, [Pattern a])
renamePattern :: Pattern a
-> (RenameMap a, [Pattern a]) -> (RenameMap a, [Pattern a])
renamePattern (VariablePattern spi :: SpanInfo
spi a :: a
a v :: Ident
v) (rm :: RenameMap a
rm, ts :: [Pattern a]
ts)
  | Ident
v Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Pattern a] -> [Ident]
forall a. [Pattern a] -> [Ident]
varPatNames [Pattern a]
ts =
    let v' :: Ident
v' = (String -> String) -> Ident -> Ident
updIdentName (String -> String -> String
forall a. [a] -> [a] -> [a]
++ ("." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (RenameMap a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length RenameMap a
rm))) Ident
v
    in  (((a
a, Ident
v), Ident
v') ((a, Ident), Ident) -> RenameMap a -> RenameMap a
forall a. a -> [a] -> [a]
: RenameMap a
rm, SpanInfo -> a -> Ident -> Pattern a
forall a. SpanInfo -> a -> Ident -> Pattern a
VariablePattern SpanInfo
spi a
a Ident
v' Pattern a -> [Pattern a] -> [Pattern a]
forall a. a -> [a] -> [a]
: [Pattern a]
ts)
renamePattern t :: Pattern a
t                     (rm :: RenameMap a
rm, ts :: [Pattern a]
ts) = (RenameMap a
rm, Pattern a
t Pattern a -> [Pattern a] -> [Pattern a]
forall a. a -> [a] -> [a]
: [Pattern a]
ts)

renameRhs :: Eq a => RenameMap a -> Rhs a -> Rhs a
renameRhs :: RenameMap a -> Rhs a -> Rhs a
renameRhs rm :: RenameMap a
rm (SimpleRhs p :: SpanInfo
p _ e :: Expression a
e _) = SpanInfo -> Expression a -> Rhs a
forall a. SpanInfo -> Expression a -> Rhs a
simpleRhs SpanInfo
p (RenameMap a -> Expression a -> Expression a
forall a. Eq a => RenameMap a -> Expression a -> Expression a
renameExpr RenameMap a
rm Expression a
e)
renameRhs _  _                   = String -> Rhs a
forall a. HasCallStack => String -> a
error "Lift.renameRhs"

renameExpr :: Eq a => RenameMap a -> Expression a -> Expression a
renameExpr :: RenameMap a -> Expression a -> Expression a
renameExpr _  l :: Expression a
l@(Literal       _ _ _) = Expression a
l
renameExpr rm :: RenameMap a
rm v :: Expression a
v@(Variable   spi :: SpanInfo
spi a :: a
a v' :: QualIdent
v')
  | QualIdent -> Bool
isQualified QualIdent
v' = Expression a
v
  | Bool
otherwise      = case (a, Ident) -> RenameMap a -> Maybe Ident
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (a
a, QualIdent -> Ident
unqualify QualIdent
v') RenameMap a
rm of
                       Just v'' :: Ident
v'' -> SpanInfo -> a -> QualIdent -> Expression a
forall a. SpanInfo -> a -> QualIdent -> Expression a
Variable SpanInfo
spi a
a (Ident -> QualIdent
qualify Ident
v'')
                       _        -> Expression a
v
renameExpr _  c :: Expression a
c@(Constructor _ _ _) = Expression a
c
renameExpr rm :: RenameMap a
rm (Typed       spi :: SpanInfo
spi e :: Expression a
e ty :: QualTypeExpr
ty) = SpanInfo -> Expression a -> QualTypeExpr -> Expression a
forall a. SpanInfo -> Expression a -> QualTypeExpr -> Expression a
Typed SpanInfo
spi (RenameMap a -> Expression a -> Expression a
forall a. Eq a => RenameMap a -> Expression a -> Expression a
renameExpr RenameMap a
rm Expression a
e) QualTypeExpr
ty
renameExpr rm :: RenameMap a
rm (Apply       spi :: SpanInfo
spi e1 :: Expression a
e1 e2 :: Expression a
e2) =
  SpanInfo -> Expression a -> Expression a -> Expression a
forall a. SpanInfo -> Expression a -> Expression a -> Expression a
Apply SpanInfo
spi (RenameMap a -> Expression a -> Expression a
forall a. Eq a => RenameMap a -> Expression a -> Expression a
renameExpr RenameMap a
rm Expression a
e1) (RenameMap a -> Expression a -> Expression a
forall a. Eq a => RenameMap a -> Expression a -> Expression a
renameExpr RenameMap a
rm Expression a
e2)
renameExpr rm :: RenameMap a
rm (Let       _ _ ds :: [Decl a]
ds e :: Expression a
e) =
  [Decl a] -> Expression a -> Expression a
forall a. [Decl a] -> Expression a -> Expression a
mkLet ((Decl a -> Decl a) -> [Decl a] -> [Decl a]
forall a b. (a -> b) -> [a] -> [b]
map (RenameMap a -> Decl a -> Decl a
forall a. Eq a => RenameMap a -> Decl a -> Decl a
renameDecl RenameMap a
rm) [Decl a]
ds) (RenameMap a -> Expression a -> Expression a
forall a. Eq a => RenameMap a -> Expression a -> Expression a
renameExpr RenameMap a
rm Expression a
e)
renameExpr rm :: RenameMap a
rm (Case    _ _ ct :: CaseType
ct e :: Expression a
e alts :: [Alt a]
alts) =
  CaseType -> Expression a -> [Alt a] -> Expression a
forall a. CaseType -> Expression a -> [Alt a] -> Expression a
mkCase CaseType
ct (RenameMap a -> Expression a -> Expression a
forall a. Eq a => RenameMap a -> Expression a -> Expression a
renameExpr RenameMap a
rm Expression a
e) ((Alt a -> Alt a) -> [Alt a] -> [Alt a]
forall a b. (a -> b) -> [a] -> [b]
map (RenameMap a -> Alt a -> Alt a
forall a. Eq a => RenameMap a -> Alt a -> Alt a
renameAlt RenameMap a
rm) [Alt a]
alts)
renameExpr _  _                   = String -> Expression a
forall a. HasCallStack => String -> a
error "Lift.renameExpr"

renameDecl :: Eq a => RenameMap a -> Decl a -> Decl a
renameDecl :: RenameMap a -> Decl a -> Decl a
renameDecl rm :: RenameMap a
rm (PatternDecl p :: SpanInfo
p t :: Pattern a
t rhs :: Rhs a
rhs) = SpanInfo -> Pattern a -> Rhs a -> Decl a
forall a. SpanInfo -> Pattern a -> Rhs a -> Decl a
PatternDecl SpanInfo
p Pattern a
t (RenameMap a -> Rhs a -> Rhs a
forall a. Eq a => RenameMap a -> Rhs a -> Rhs a
renameRhs RenameMap a
rm Rhs a
rhs)
renameDecl _  d :: Decl a
d                     = Decl a
d

renameAlt :: Eq a => RenameMap a -> Alt a -> Alt a
renameAlt :: RenameMap a -> Alt a -> Alt a
renameAlt rm :: RenameMap a
rm (Alt p :: SpanInfo
p t :: Pattern a
t rhs :: Rhs a
rhs) = SpanInfo -> Pattern a -> Rhs a -> Alt a
forall a. SpanInfo -> Pattern a -> Rhs a -> Alt a
Alt SpanInfo
p Pattern a
t (RenameMap a -> Rhs a -> Rhs a
forall a. Eq a => RenameMap a -> Rhs a -> Rhs a
renameRhs RenameMap a
rm Rhs a
rhs)

-- ---------------------------------------------------------------------------
-- Auxiliary definitions
-- ---------------------------------------------------------------------------

isFunDecl :: Decl a -> Bool
isFunDecl :: Decl a -> Bool
isFunDecl (FunctionDecl _ _ _ _) = Bool
True
isFunDecl (ExternalDecl _ _    ) = Bool
True
isFunDecl _                      = Bool
False

mkFun :: ModuleIdent -> String -> a -> Ident -> Expression a
mkFun :: ModuleIdent -> String -> a -> Ident -> Expression a
mkFun m :: ModuleIdent
m pre :: String
pre a :: a
a = SpanInfo -> a -> QualIdent -> Expression a
forall a. SpanInfo -> a -> QualIdent -> Expression a
Variable SpanInfo
NoSpanInfo a
a (QualIdent -> Expression a)
-> (Ident -> QualIdent) -> Ident -> Expression a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m (Ident -> QualIdent) -> (Ident -> Ident) -> Ident -> QualIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Ident -> Ident
liftIdent String
pre

liftIdent :: String -> Ident -> Ident
liftIdent :: String -> Ident -> Ident
liftIdent prefix :: String
prefix x :: Ident
x = Ident -> Integer -> Ident
renameIdent (String -> Ident
mkIdent (String -> Ident) -> String -> Ident
forall a b. (a -> b) -> a -> b
$ String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ident -> String
showIdent Ident
x) (Integer -> Ident) -> Integer -> Ident
forall a b. (a -> b) -> a -> b
$ Ident -> Integer
idUnique Ident
x

varPatNames :: [Pattern a] -> [Ident]
varPatNames :: [Pattern a] -> [Ident]
varPatNames = (Pattern a -> Maybe Ident) -> [Pattern a] -> [Ident]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Pattern a -> Maybe Ident
forall a. Pattern a -> Maybe Ident
varPatName

varPatName :: Pattern a -> Maybe Ident
varPatName :: Pattern a -> Maybe Ident
varPatName (VariablePattern _ _ i :: Ident
i) = Ident -> Maybe Ident
forall a. a -> Maybe a
Just Ident
i
varPatName _                     = Maybe Ident
forall a. Maybe a
Nothing

dummyType :: Type
dummyType :: Type
dummyType = [Int] -> Type -> Type
TypeForall [] Type
forall a. HasCallStack => a
undefined

isDummyType :: Type -> Bool
isDummyType :: Type -> Bool
isDummyType (TypeForall [] _) = Bool
True
isDummyType _                 = Bool
False