{-|
Module      : Idris.Elab.Clause
Description : Code to elaborate clauses.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Elab.Clause where

import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.WHNF
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq ()
import Idris.Delaborate
import Idris.Docstrings hiding (Unchecked)
import Idris.Elab.AsPat
import Idris.Elab.Term
import Idris.Elab.Transform
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Error
import Idris.Options
import Idris.Output (iWarn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Termination
import Idris.Transforms

import Util.Pretty hiding ((<$>))

import Prelude hiding (id, (.))

import Control.Category
import Control.DeepSeq
import Control.Monad
import qualified Control.Monad.State.Lazy as LState
import Control.Monad.State.Strict as State
import Data.List
import Data.Maybe
import qualified Data.Set as S
import Data.Word
import Debug.Trace
import Numeric

-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
-- top-level definition.
elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
elabClauses info' :: ElabInfo
info' fc :: FC
fc opts :: FnOpts
opts n_in :: Name
n_in cs :: [PClause]
cs =
      do let n :: Name
n    = ElabInfo -> Name -> Name
liftname ElabInfo
info Name
n_in
             info :: ElabInfo
info = ElabInfo
info' { elabFC :: Maybe FC
elabFC = FC -> Maybe FC
forall a. a -> Maybe a
Just FC
fc }
         Context
ctxt <- Idris Context
getContext
         IState
ist  <- Idris IState
getIState
         [Optimisation]
optimise <- Idris [Optimisation]
getOptimise
         let petrans :: Bool
petrans = Optimisation
PETransform Optimisation -> [Optimisation] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Optimisation]
optimise
         [Int]
inacc <- ((Int, Name) -> Int) -> [(Int, Name)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Name) -> Int
forall a b. (a, b) -> a
fst ([(Int, Name)] -> [Int])
-> StateT IState (ExceptT Err IO) [(Int, Name)]
-> StateT IState (ExceptT Err IO) [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, Name)]
-> StateT IState (ExceptT Err IO) [(Int, Name)]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field OptInfo [(Int, Name)]
opt_inaccessible Field OptInfo [(Int, Name)]
-> Field IState OptInfo -> Field IState [(Int, Name)]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n)

         -- Check n actually exists, with no definition yet
         let tys :: [Type]
tys = Name -> Context -> [Type]
lookupTy Name
n Context
ctxt
         let reflect :: Bool
reflect = FnOpt
Reflection FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
reflect Bool -> Bool -> Bool
&& LanguageExt
FCReflection LanguageExt -> [LanguageExt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` IState -> [LanguageExt]
idris_language_extensions IState
ist) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
           Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> Err -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Err
forall t. String -> Err' t
Msg "You must turn on the FirstClassReflection extension to use %reflection")
         Name -> Context -> Idris ()
checkUndefined Name
n Context
ctxt
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
           Type
fty <- case [Type]
tys of
              [] -> -- TODO: turn into a CAF if there's no arguments
                    -- question: CAFs in where blocks?
                    TC Type -> Idris Type
forall a. TC a -> Idris a
tclift (TC Type -> Idris Type) -> TC Type -> Idris Type
forall a b. (a -> b) -> a -> b
$ Err -> TC Type
forall a. Err -> TC a
tfail (Err -> TC Type) -> Err -> TC Type
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Name -> Err
forall t. Name -> Err' t
NoTypeDecl Name
n)
              [ty :: Type
ty] -> Type -> Idris Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
           let atys_in :: [Type]
atys_in = ((Name, Type) -> Type) -> [(Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Type
forall a b. (a, b) -> b
snd (Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
fty))
           let atys :: [(Type, Bool)]
atys = (Type -> (Type, Bool)) -> [Type] -> [(Type, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: Type
x -> (Type
x, Type -> Context -> Bool
isCanonical Type
x Context
ctxt)) [Type]
atys_in
           [(Either Type (Type, Type), PTerm)]
cs_elab <- ((Int, PClause)
 -> StateT
      IState (ExceptT Err IO) (Either Type (Type, Type), PTerm))
-> [(Int, PClause)]
-> StateT
     IState (ExceptT Err IO) [(Either Type (Type, Type), PTerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ElabInfo
-> FnOpts
-> (Int, PClause)
-> StateT IState (ExceptT Err IO) (Either Type (Type, Type), PTerm)
elabClause ElabInfo
info FnOpts
opts)
                           ([Int] -> [PClause] -> [(Int, PClause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [PClause]
cs)
           Context
ctxt <- Idris Context
getContext
           -- pats_raw is the basic type checked version, no PE or forcing
           let optinfo :: Ctxt OptInfo
optinfo = IState -> Ctxt OptInfo
idris_optimisation IState
ist
           let (pats_in :: [Either Type (Type, Type)]
pats_in, cs_full :: [PTerm]
cs_full) = [(Either Type (Type, Type), PTerm)]
-> ([Either Type (Type, Type)], [PTerm])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Either Type (Type, Type), PTerm)]
cs_elab
           let pats_raw :: [Either Type (Type, Type)]
pats_raw = (Either Type (Type, Type) -> Either Type (Type, Type))
-> [Either Type (Type, Type)] -> [Either Type (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Context -> Either Type (Type, Type) -> Either Type (Type, Type)
forall a b. Context -> Either a (Type, b) -> Either a (Type, b)
simple_lhs Context
ctxt) [Either Type (Type, Type)]
pats_in
           -- We'll apply forcing to the left hand side here, so that we don't
           -- do any unnecessary case splits
           let pats_forced :: [Either Type (Type, Type)]
pats_forced = (Either Type (Type, Type) -> Either Type (Type, Type))
-> [Either Type (Type, Type)] -> [Either Type (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Ctxt OptInfo
-> Either Type (Type, Type) -> Either Type (Type, Type)
forall a b.
Ctxt OptInfo -> Either a (Type, b) -> Either a (Type, b)
force_lhs Ctxt OptInfo
optinfo) [Either Type (Type, Type)]
pats_raw

           Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborated patterns:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Either Type (Type, Type)] -> String
forall a. Show a => a -> String
show [Either Type (Type, Type)]
pats_raw
           Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Forced patterns:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Either Type (Type, Type)] -> String
forall a. Show a => a -> String
show [Either Type (Type, Type)]
pats_forced

           FC -> Name -> Idris ()
solveDeferred FC
fc Name
n

           -- just ensure that the structure exists
           Field IState OptInfo -> (OptInfo -> OptInfo) -> Idris ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState (Name -> Field IState OptInfo
ist_optimisation Name
n) OptInfo -> OptInfo
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
           IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
n)

           IState
ist <- Idris IState
getIState
           Context
ctxt <- Idris Context
getContext
           -- Don't apply rules if this is a partial evaluation definition,
           -- or we'll make something that just runs itself!
           let tpats :: [Either Type (Type, Type)]
tpats = case FnOpts -> Maybe [(Name, Maybe Int)]
specNames FnOpts
opts of
                            Nothing -> IState -> [Either Type (Type, Type)] -> [Either Type (Type, Type)]
transformPats IState
ist [Either Type (Type, Type)]
pats_in
                            _ -> [Either Type (Type, Type)]
pats_in

           -- If the definition is specialisable, this reduces the
           -- RHS
           [Either Type (Type, Type)]
pe_tm <- IState
-> [Either Type (Type, Type)]
-> StateT IState (ExceptT Err IO) [Either Type (Type, Type)]
doPartialEval IState
ist [Either Type (Type, Type)]
tpats

           let pats_pe :: [Either Type (Type, Type)]
pats_pe = if Bool
petrans
                            then (Either Type (Type, Type) -> Either Type (Type, Type))
-> [Either Type (Type, Type)] -> [Either Type (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Ctxt OptInfo
-> Either Type (Type, Type) -> Either Type (Type, Type)
forall a b.
Ctxt OptInfo -> Either a (Type, b) -> Either a (Type, b)
force_lhs Ctxt OptInfo
optinfo (Either Type (Type, Type) -> Either Type (Type, Type))
-> (Either Type (Type, Type) -> Either Type (Type, Type))
-> Either Type (Type, Type)
-> Either Type (Type, Type)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Context -> Either Type (Type, Type) -> Either Type (Type, Type)
forall a b. Context -> Either a (Type, b) -> Either a (Type, b)
simple_lhs Context
ctxt) [Either Type (Type, Type)]
pe_tm
                            else [Either Type (Type, Type)]
pats_forced

           let tcase :: Bool
tcase = IOption -> Bool
opt_typecase (IState -> IOption
idris_options IState
ist)

           -- Look for 'static' names and generate new specialised
           -- definitions for them, as well as generating rewrite rules
           -- for partially evaluated definitions
           [[(Type, Type)]]
newrules <- if Bool
petrans
                          then (Either Type (Type, Type)
 -> StateT IState (ExceptT Err IO) [(Type, Type)])
-> [Either Type (Type, Type)]
-> StateT IState (ExceptT Err IO) [[(Type, Type)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ e :: Either Type (Type, Type)
e -> case Either Type (Type, Type)
e of
                                            Left _ -> [(Type, Type)] -> StateT IState (ExceptT Err IO) [(Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                                            Right (l :: Type
l, r :: Type
r) -> ElabInfo
-> FC
-> Name
-> Type
-> StateT IState (ExceptT Err IO) [(Type, Type)]
elabPE ElabInfo
info FC
fc Name
n Type
r) [Either Type (Type, Type)]
pats_pe
                          else [[(Type, Type)]] -> StateT IState (ExceptT Err IO) [[(Type, Type)]]
forall (m :: * -> *) a. Monad m => a -> m a
return []

           -- Redo transforms with the newly generated transformations, so
           -- that the specialised application we've just made gets
           -- used in place of the general one
           IState
ist <- Idris IState
getIState
           let pats_transformed :: [Either Type (Type, Type)]
pats_transformed = if Bool
petrans
                                     then IState -> [Either Type (Type, Type)] -> [Either Type (Type, Type)]
transformPats IState
ist [Either Type (Type, Type)]
pats_pe
                                     else [Either Type (Type, Type)]
pats_pe

           -- Summary of what's about to happen: Definitions go:
           --
           -- pats_in -> pats -> pdef -> pdef'

           -- addCaseDef builds case trees from <pdef> and <pdef'>

           -- pdef is the compile-time pattern definition, after forcing
           -- optimisation applied to LHS
           let pdef :: [([Name], Type, Type)]
pdef = (([(Name, Type)], Type, Type) -> ([Name], Type, Type))
-> [([(Name, Type)], Type, Type)] -> [([Name], Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\(ns :: [(Name, Type)]
ns, lhs :: Type
lhs, rhs :: Type
rhs) -> (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
ns, Type
lhs, Type
rhs)) ([([(Name, Type)], Type, Type)] -> [([Name], Type, Type)])
-> [([(Name, Type)], Type, Type)] -> [([Name], Type, Type)]
forall a b. (a -> b) -> a -> b
$
                          (Either Type (Type, Type) -> ([(Name, Type)], Type, Type))
-> [Either Type (Type, Type)] -> [([(Name, Type)], Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Either Type (Type, Type) -> ([(Name, Type)], Type, Type)
forall n n. Either (TT n) (TT n, TT n) -> ([(n, TT n)], TT n, TT n)
debind [Either Type (Type, Type)]
pats_forced
           -- pdef_pe is the one which will get further optimised
           -- for run-time, with no forcing optimisation of the LHS because
           -- the affects erasure. Also, it's partially evaluated
           let pdef_pe :: [([(Name, Type)], Type, Type)]
pdef_pe = (Either Type (Type, Type) -> ([(Name, Type)], Type, Type))
-> [Either Type (Type, Type)] -> [([(Name, Type)], Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Either Type (Type, Type) -> ([(Name, Type)], Type, Type)
forall n n. Either (TT n) (TT n, TT n) -> ([(n, TT n)], TT n, TT n)
debind [Either Type (Type, Type)]
pats_transformed

           Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Initial typechecked patterns:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Either Type (Type, Type)] -> String
forall a. Show a => a -> String
show [Either Type (Type, Type)]
pats_raw
           Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Initial typechecked pattern def:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [([Name], Type, Type)] -> String
forall a. Show a => a -> String
show [([Name], Type, Type)]
pdef

           -- NOTE: Need to store original definition so that proofs which
           -- rely on its structure aren't affected by any changes to the
           -- inliner. Just use the inlined version to generate pdef' and to
           -- help with later inlinings.

           IState
ist <- Idris IState
getIState
           Int
numArgs <- TC Int -> Idris Int
forall a. TC a -> Idris a
tclift (TC Int -> Idris Int) -> TC Int -> Idris Int
forall a b. (a -> b) -> a -> b
$ [([Name], Type, Type)] -> TC Int
forall a n c. [(a, TT n, c)] -> TC Int
sameLength [([Name], Type, Type)]
pdef

           case FnOpts -> Maybe [(Name, Maybe Int)]
specNames FnOpts
opts of
                Just _ ->
                   do Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Partially evaluated:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Either Type (Type, Type)] -> String
forall a. Show a => a -> String
show [Either Type (Type, Type)]
pats_pe
                _ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Transformed:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Either Type (Type, Type)] -> String
forall a. Show a => a -> String
show [Either Type (Type, Type)]
pats_transformed

           Name -> [Int]
erInfo <- IState -> Name -> [Int]
getErasureInfo (IState -> Name -> [Int])
-> Idris IState -> StateT IState (ExceptT Err IO) (Name -> [Int])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
           tree :: CaseDef
tree@(CaseDef scargs :: [Name]
scargs sc :: SC
sc _) <- TC CaseDef -> Idris CaseDef
forall a. TC a -> Idris a
tclift (TC CaseDef -> Idris CaseDef) -> TC CaseDef -> Idris CaseDef
forall a b. (a -> b) -> a -> b
$
                 Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Type, Bool)]
-> [([Name], Type, Type)]
-> (Name -> [Int])
-> TC CaseDef
simpleCase Bool
tcase (String -> SC
forall t. String -> SC' t
UnmatchedCase "Error") Bool
reflect Phase
CompileTime FC
fc [Int]
inacc [(Type, Bool)]
atys [([Name], Type, Type)]
pdef Name -> [Int]
erInfo
           Bool
cov <- Idris Bool
coverage
           [PTerm]
pmissing <-
                   if Bool
cov Bool -> Bool -> Bool
&& Bool -> Bool
not ([Either Type (Type, Type)] -> Bool
forall a a b. Eq a => [Either a (TT a, b)] -> Bool
hasDefault [Either Type (Type, Type)]
pats_raw)
                      then do -- Generate clauses from the given possible cases
                              [PTerm]
missing <- FC -> Name -> [([Name], Type)] -> [PTerm] -> Idris [PTerm]
genClauses FC
fc Name
n
                                                 ((([Name], Type, Type) -> ([Name], Type))
-> [([Name], Type, Type)] -> [([Name], Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ns :: [Name]
ns,tm :: Type
tm,_) -> ([Name]
ns, Type
tm)) [([Name], Type, Type)]
pdef)
                                                 [PTerm]
cs_full
                              -- missing <- genMissing n scargs sc
                              [PTerm]
missing' <- ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]
checkPossibles ElabInfo
info FC
fc Bool
True Name
n [PTerm]
missing
                              -- Filter out the ones which match one of the
                              -- given cases (including impossible ones)
                              Int -> String -> Idris ()
logElab 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Must be unreachable (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([PTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PTerm]
missing') String -> String -> String
forall a. [a] -> [a] -> [a]
++ "):\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                          String -> [String] -> String
showSep "\n" ((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
missing') String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                         "\nAgainst: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                          String -> [String] -> String
showSep "\n" ((Type -> String) -> [Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\t :: Type
t -> PTerm -> String
showTmImpls (IState -> Type -> PTerm
delab IState
ist Type
t)) ((([Name], Type, Type) -> Type) -> [([Name], Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ([Name], Type, Type) -> Type
forall a b c. (a, b, c) -> b
getLHS [([Name], Type, Type)]
pdef))
                              -- filter out anything in missing' which is
                              -- matched by any of clhs. This might happen since
                              -- unification may force a variable to take a
                              -- particular form, rather than force a case
                              -- to be impossible.
                              [PTerm] -> Idris [PTerm]
forall (m :: * -> *) a. Monad m => a -> m a
return [PTerm]
missing' -- (filter (noMatch ist clhs) missing')
                      else [PTerm] -> Idris [PTerm]
forall (m :: * -> *) a. Monad m => a -> m a
return []
           let pcover :: Bool
pcover = [PTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
pmissing

           -- pdef' is the version that gets compiled for run-time,
           -- so we start from the partially evaluated version
           [([Name], Type, Type)]
pdef_in' <- [([Name], Type, Type)] -> Idris [([Name], Type, Type)]
forall term. Optimisable term => term -> Idris term
applyOpts ([([Name], Type, Type)] -> Idris [([Name], Type, Type)])
-> [([Name], Type, Type)] -> Idris [([Name], Type, Type)]
forall a b. (a -> b) -> a -> b
$ (([(Name, Type)], Type, Type) -> ([Name], Type, Type))
-> [([(Name, Type)], Type, Type)] -> [([Name], Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\(ns :: [(Name, Type)]
ns, lhs :: Type
lhs, rhs :: Type
rhs) -> (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
ns, Type
lhs, Type
rhs)) [([(Name, Type)], Type, Type)]
pdef_pe
           Context
ctxt <- Idris Context
getContext
           let pdef' :: [([Name], Type, Type)]
pdef' = (([Name], Type, Type) -> ([Name], Type, Type))
-> [([Name], Type, Type)] -> [([Name], Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Context -> ([Name], Type, Type) -> ([Name], Type, Type)
forall b. Context -> ([Name], b, Type) -> ([Name], b, Type)
simple_rt Context
ctxt) [([Name], Type, Type)]
pdef_in'

           Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "After data structure transformations:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [([Name], Type, Type)] -> String
forall a. Show a => a -> String
show [([Name], Type, Type)]
pdef'

           IState
ist <- Idris IState
getIState
           let tot :: Totality
tot | Bool
pcover = Totality
Unchecked -- finish later
                   | FnOpt
AssertTotal FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts = [Int] -> Totality
Total []
                   | FnOpt
PEGenerated FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts = Totality
Generated
                   | Bool
otherwise = PReason -> Totality
Partial PReason
NotCovering -- already know it's not total

           case CaseDef
tree of
               CaseDef _ _ [] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               CaseDef _ _ xs :: [Type]
xs -> (Type -> Idris ()) -> [Type] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\x :: Type
x ->
                   FC -> OutputDoc -> Idris ()
iWarn FC
fc (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> OutputDoc
forall a. String -> Doc a
text "Unreachable case:" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
</> String -> OutputDoc
forall a. String -> Doc a
text (PTerm -> String
forall a. Show a => a -> String
show (IState -> Type -> PTerm
delab IState
ist Type
x))
                   ) [Type]
xs
           let knowncovering :: Bool
knowncovering = (Bool
pcover Bool -> Bool -> Bool
&& Bool
cov) Bool -> Bool -> Bool
|| FnOpt
AssertTotal FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts
           let defaultcase :: SC' (TT n)
defaultcase = if Bool
knowncovering
                                then TT n -> SC' (TT n)
forall t. t -> SC' t
STerm TT n
forall n. TT n
Erased
                                else String -> SC' (TT n)
forall t. String -> SC' t
UnmatchedCase (String -> SC' (TT n)) -> String -> SC' (TT n)
forall a b. (a -> b) -> a -> b
$ "*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                      FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                       ":unmatched case in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                       " ***"

           CaseDef
tree' <- TC CaseDef -> Idris CaseDef
forall a. TC a -> Idris a
tclift (TC CaseDef -> Idris CaseDef) -> TC CaseDef -> Idris CaseDef
forall a b. (a -> b) -> a -> b
$ Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Type, Bool)]
-> [([Name], Type, Type)]
-> (Name -> [Int])
-> TC CaseDef
simpleCase Bool
tcase SC
forall n. SC' (TT n)
defaultcase Bool
reflect
                                        Phase
RunTime FC
fc [Int]
inacc [(Type, Bool)]
atys [([Name], Type, Type)]
pdef' Name -> [Int]
erInfo
           Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Unoptimised " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CaseDef -> String
forall a. Show a => a -> String
show CaseDef
tree
           Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Optimised: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CaseDef -> String
forall a. Show a => a -> String
show CaseDef
tree'
           Context
ctxt <- Idris Context
getContext
           IState
ist <- Idris IState
getIState
           IState -> Idris ()
putIState (IState
ist { idris_patdefs :: Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
idris_patdefs = Name
-> ([([(Name, Type)], Type, Type)], [PTerm])
-> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
-> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n ([([(Name, Type)], Type, Type)] -> [([(Name, Type)], Type, Type)]
forall a. NFData a => a -> a
force [([(Name, Type)], Type, Type)]
pdef_pe, [PTerm] -> [PTerm]
forall a. NFData a => a -> a
force [PTerm]
pmissing)
                                                (IState -> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
idris_patdefs IState
ist) })
           let caseInfo :: CaseInfo
caseInfo = Bool -> Bool -> Bool -> CaseInfo
CaseInfo (FnOpts -> Bool
inlinable FnOpts
opts) (FnOpts -> Bool
inlinable FnOpts
opts) (FnOpts -> Bool
dictionary FnOpts
opts)

           case Name -> Context -> Maybe Type
lookupTyExact Name
n Context
ctxt of
               Just ty :: Type
ty ->
                   do Context
ctxt' <- do Context
ctxt <- Idris Context
getContext
                                  TC Context -> Idris Context
forall a. TC a -> Idris a
tclift (TC Context -> Idris Context) -> TC Context -> Idris Context
forall a b. (a -> b) -> a -> b
$
                                    Name
-> (Name -> [Int])
-> CaseInfo
-> Bool
-> SC
-> Bool
-> Bool
-> [(Type, Bool)]
-> [Int]
-> [Either Type (Type, Type)]
-> [([Name], Type, Type)]
-> [([Name], Type, Type)]
-> Type
-> Context
-> TC Context
addCasedef Name
n Name -> [Int]
erInfo CaseInfo
caseInfo
                                                   Bool
tcase SC
forall n. SC' (TT n)
defaultcase
                                                   Bool
reflect
                                                   (FnOpt
AssertTotal FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts)
                                                   [(Type, Bool)]
atys
                                                   [Int]
inacc
                                                   [Either Type (Type, Type)]
pats_forced
                                                   [([Name], Type, Type)]
pdef
                                                   [([Name], Type, Type)]
pdef' Type
ty
                                                   Context
ctxt
                      Context -> Idris ()
setContext Context
ctxt'
                      IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
                      Name -> Idris ()
addDefinedName Name
n
                      Name -> Totality -> Idris ()
setTotality Name
n Totality
tot
                      Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
reflect Bool -> Bool -> Bool
&& FnOpt
PEGenerated FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
                                           do (FC, Name) -> Idris ()
totcheck (FC
fc, Name
n)
                                              (FC, Name) -> Idris ()
defer_totcheck (FC
fc, Name
n)
                      Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Totality
tot Totality -> Totality -> Bool
forall a. Eq a => a -> a -> Bool
/= Totality
Unchecked) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ IBCWrite -> Idris ()
addIBC (Name -> Totality -> IBCWrite
IBCTotal Name
n Totality
tot)
                      IState
i <- Idris IState
getIState
                      Context
ctxt <- Idris Context
getContext
                      case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
                          (CaseOp _ _ _ _ _ cd :: CaseDefs
cd : _) ->
                            let (scargs :: [Name]
scargs, sc :: SC
sc) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd in
                              do let calls :: [Name]
calls = ((Name, [[Name]]) -> Name) -> [(Name, [[Name]])] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [[Name]]) -> Name
forall a b. (a, b) -> a
fst ([(Name, [[Name]])] -> [Name]) -> [(Name, [[Name]])] -> [Name]
forall a b. (a -> b) -> a -> b
$ SC -> [Name] -> [(Name, [[Name]])]
findCalls SC
sc [Name]
scargs
                                 -- let scg = buildSCG i sc scargs
                                 -- add SCG later, when checking totality
                                 Int -> String -> Idris ()
logElab 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Called names: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
calls
                                 -- if the definition is public, make sure
                                 -- it only uses public names
                                 Maybe Accessibility
nvis <- Name -> Idris (Maybe Accessibility)
getFromHideList Name
n
                                 case Maybe Accessibility
nvis of
                                      Just Public -> (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()
checkVisibility FC
fc Name
n Accessibility
Public Accessibility
Public) [Name]
calls
                                      _ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                 Name -> [Name] -> Idris ()
addCalls Name
n [Name]
calls
                                 let rig :: RigCount
rig = if Type -> Bool
linearArg (Context -> Env -> Type -> Type
whnfArgs Context
ctxt [] Type
ty)
                                              then RigCount
Rig1
                                              else RigCount
RigW
                                 (Context -> Context) -> Idris ()
updateContext (Name -> RigCount -> Context -> Context
setRigCount Name
n (Context -> RigCount -> [Name] -> RigCount
minRig Context
ctxt RigCount
rig [Name]
calls))
                                 IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCCG Name
n)
                          _ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                      () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  --                         addIBC (IBCTotal n tot)
               _ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           -- Check it's covering, if 'covering' option is used. Chase
           -- all called functions, and fail if any of them are also
           -- 'Partial NotCovering'
           Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
CoveringFn FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> [Name] -> Name -> Name -> Idris ()
checkAllCovering FC
fc [] Name
n Name
n
           -- Add the 'AllGuarded' flag if it's guaranteed that every
           -- 'Inf' argument will be guarded by constructors in the result
           -- (allows productivity check to go under this function)
           Name -> Idris ()
checkIfGuarded Name
n
           -- If this has %static arguments, cache the names of functions
           -- it calls for partial evaluation later
           IState
ist <- Idris IState
getIState
           let statics :: [Bool]
statics = case Name -> Ctxt [Bool] -> Maybe [Bool]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
ist) of
                              Just ns :: [Bool]
ns -> [Bool]
ns
                              Nothing -> []
           Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
statics) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do Name -> Idris [Name]
getAllNames Name
n
                                  () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  where
    checkUndefined :: Name -> Context -> Idris ()
checkUndefined n :: Name
n ctxt :: Context
ctxt = case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
                                 [] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                 [TyDecl _ _] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                 _ -> TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Name -> Err
forall t. Name -> Err' t
AlreadyDefined Name
n))

    debind :: Either (TT n) (TT n, TT n) -> ([(n, TT n)], TT n, TT n)
debind (Right (x :: TT n
x, y :: TT n
y)) = let (vs :: [(n, TT n)]
vs, x' :: TT n
x') = [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
forall n. [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
depat [] TT n
x
                                (_, y' :: TT n
y') = [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
forall n. [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
depat [] TT n
y in
                                ([(n, TT n)]
vs, TT n
x', TT n
y')
    debind (Left x :: TT n
x)       = let (vs :: [(n, TT n)]
vs, x' :: TT n
x') = [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
forall n. [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
depat [] TT n
x in
                                ([(n, TT n)]
vs, TT n
x', TT n
forall n. TT n
Impossible)

    depat :: [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
depat acc :: [(n, TT n)]
acc (Bind n :: n
n (PVar rig :: RigCount
rig t :: TT n
t) sc :: TT n
sc) = [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
depat ((n
n, TT n
t) (n, TT n) -> [(n, TT n)] -> [(n, TT n)]
forall a. a -> [a] -> [a]
: [(n, TT n)]
acc) (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n TT n
t) TT n
sc)
    depat acc :: [(n, TT n)]
acc x :: TT n
x = ([(n, TT n)]
acc, TT n
x)


    getPVs :: TT a -> ([a], TT a)
getPVs (Bind x :: a
x (PVar rig :: RigCount
rig _) tm :: TT a
tm) = let (vs :: [a]
vs, tm' :: TT a
tm') = TT a -> ([a], TT a)
getPVs TT a
tm
                                          in (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
vs, TT a
tm')
    getPVs tm :: TT a
tm = ([], TT a
tm)

    isPatVar :: t a -> TT a -> Bool
isPatVar vs :: t a
vs (P Bound n :: a
n _) = a
n a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
vs
    isPatVar _ _ = Bool
False

    hasDefault :: [Either a (TT a, b)] -> Bool
hasDefault cs :: [Either a (TT a, b)]
cs | (Right (lhs :: TT a
lhs, rhs :: b
rhs) : _) <- [Either a (TT a, b)] -> [Either a (TT a, b)]
forall a. [a] -> [a]
reverse [Either a (TT a, b)]
cs
                  , (pvs :: [a]
pvs, tm :: TT a
tm) <- TT a -> ([a], TT a)
forall a. TT a -> ([a], TT a)
getPVs (TT a -> TT a
forall n. TT n -> TT n
explicitNames TT a
lhs)
                  , (f :: TT a
f, args :: [TT a]
args) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
tm = (TT a -> Bool) -> [TT a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([a] -> TT a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => t a -> TT a -> Bool
isPatVar [a]
pvs) [TT a]
args
    hasDefault _ = Bool
False

    getLHS :: (a, b, c) -> b
getLHS (_, l :: b
l, _) = b
l

    -- Simplify the left hand side of a definition, to remove any lets
    -- that may have arisen during elaboration
    simple_lhs :: Context -> Either a (Type, b) -> Either a (Type, b)
simple_lhs ctxt :: Context
ctxt (Right (x :: Type
x, y :: b
y))
        = (Type, b) -> Either a (Type, b)
forall a b. b -> Either a b
Right (Context -> Env -> Type -> Type
Idris.Core.Evaluate.simplify Context
ctxt [] Type
x, b
y)
    simple_lhs ctxt :: Context
ctxt t :: Either a (Type, b)
t = Either a (Type, b)
t

    force_lhs :: Ctxt OptInfo -> Either a (Type, b) -> Either a (Type, b)
force_lhs opts :: Ctxt OptInfo
opts (Right (x :: Type
x, y :: b
y)) = (Type, b) -> Either a (Type, b)
forall a b. b -> Either a b
Right (Ctxt OptInfo -> Type -> Type
forceWith Ctxt OptInfo
opts Type
x, b
y)
    force_lhs opts :: Ctxt OptInfo
opts t :: Either a (Type, b)
t = Either a (Type, b)
t

    simple_rt :: Context -> ([Name], b, Type) -> ([Name], b, Type)
simple_rt ctxt :: Context
ctxt (p :: [Name]
p, x :: b
x, y :: Type
y) = ([Name]
p, b
x, Type -> Type
forall a. NFData a => a -> a
force ([Name] -> Type -> Type
uniqueBinders [Name]
p
                                                (Context -> Env -> Type -> Type
rt_simplify Context
ctxt [] Type
y)))

    specNames :: FnOpts -> Maybe [(Name, Maybe Int)]
specNames [] = Maybe [(Name, Maybe Int)]
forall a. Maybe a
Nothing
    specNames (Specialise ns :: [(Name, Maybe Int)]
ns : _) = [(Name, Maybe Int)] -> Maybe [(Name, Maybe Int)]
forall a. a -> Maybe a
Just [(Name, Maybe Int)]
ns
    specNames (_ : xs :: FnOpts
xs) = FnOpts -> Maybe [(Name, Maybe Int)]
specNames FnOpts
xs

    sameLength :: [(a, TT n, c)] -> TC Int
sameLength ((_, x :: TT n
x, _) : xs :: [(a, TT n, c)]
xs)
        = do Int
l <- [(a, TT n, c)] -> TC Int
sameLength [(a, TT n, c)]
xs
             let (_, as :: [TT n]
as) = TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
x
             if ([(a, TT n, c)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(a, TT n, c)]
xs Bool -> Bool -> Bool
|| Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TT n] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT n]
as) then Int -> TC Int
forall (m :: * -> *) a. Monad m => a -> m a
return ([TT n] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT n]
as)
                else Err -> TC Int
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Err
forall t. String -> Err' t
Msg "Clauses have differing numbers of arguments "))
    sameLength [] = Int -> TC Int
forall (m :: * -> *) a. Monad m => a -> m a
return 0

    -- Partially evaluate, if the definition is marked as specialisable
    doPartialEval :: IState
-> [Either Type (Type, Type)]
-> StateT IState (ExceptT Err IO) [Either Type (Type, Type)]
doPartialEval ist :: IState
ist pats :: [Either Type (Type, Type)]
pats =
           case FnOpts -> Maybe [(Name, Maybe Int)]
specNames FnOpts
opts of
                Nothing -> [Either Type (Type, Type)]
-> StateT IState (ExceptT Err IO) [Either Type (Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [Either Type (Type, Type)]
pats
                Just ns :: [(Name, Maybe Int)]
ns -> case Context
-> [(Name, Maybe Int)]
-> [Either Type (Type, Type)]
-> Maybe [Either Type (Type, Type)]
partial_eval (IState -> Context
tt_ctxt IState
ist) [(Name, Maybe Int)]
ns [Either Type (Type, Type)]
pats of
                                Just t :: [Either Type (Type, Type)]
t -> [Either Type (Type, Type)]
-> StateT IState (ExceptT Err IO) [Either Type (Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [Either Type (Type, Type)]
t
                                Nothing -> Err -> StateT IState (ExceptT Err IO) [Either Type (Type, Type)]
forall a. Err -> Idris a
ierror (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Err
forall t. String -> Err' t
Msg "No specialisation achieved"))

    minRig :: Context -> RigCount -> [Name] -> RigCount
    minRig :: Context -> RigCount -> [Name] -> RigCount
minRig c :: Context
c minr :: RigCount
minr [] = RigCount
minr
    minRig c :: Context
c minr :: RigCount
minr (r :: Name
r : rs :: [Name]
rs) = case Name -> Context -> Maybe RigCount
lookupRigCountExact Name
r Context
c of
                                  Nothing -> Context -> RigCount -> [Name] -> RigCount
minRig Context
c RigCount
minr [Name]
rs
                                  Just rc :: RigCount
rc -> Context -> RigCount -> [Name] -> RigCount
minRig Context
c (RigCount -> RigCount -> RigCount
forall a. Ord a => a -> a -> a
min RigCount
minr RigCount
rc) [Name]
rs

forceWith :: Ctxt OptInfo -> Term -> Term
forceWith :: Ctxt OptInfo -> Type -> Type
forceWith opts :: Ctxt OptInfo
opts lhs :: Type
lhs = -- trace (show lhs ++ "\n==>\n" ++ show (force lhs) ++ "\n----") $
                      Type -> Type
force Type
lhs
  where
    -- If there's forced arguments, erase them
    force :: Type -> Type
force ap :: Type
ap@(App _ _ _)
       | (fn :: Type
fn@(P _ c :: Name
c _), args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
         Just copt :: OptInfo
copt <- Name -> Ctxt OptInfo -> Maybe OptInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
c Ctxt OptInfo
opts
            = let args' :: [Type]
args' = Int -> [Int] -> [Type] -> [Type]
forall (t :: * -> *) a n.
(Foldable t, Eq a, Num a) =>
a -> t a -> [TT n] -> [TT n]
eraseArg 0 (OptInfo -> [Int]
forceable OptInfo
copt) [Type]
args in
                  Type -> [Type] -> Type
forall n. TT n -> [TT n] -> TT n
mkApp Type
fn ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
force [Type]
args')
    force (App t :: AppStatus Name
t f :: Type
f a :: Type
a)
       = AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
t (Type -> Type
force Type
f) (Type -> Type
force Type
a)
    -- We might have pat bindings, so go under them
    force (Bind n :: Name
n b :: Binder Type
b sc :: Type
sc) = Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Type
b (Type -> Type
force Type
sc)
    -- Everything else, leave it alone
    force t :: Type
t = Type
t

    eraseArg :: a -> t a -> [TT n] -> [TT n]
eraseArg i :: a
i fs :: t a
fs (n :: TT n
n : ns :: [TT n]
ns) | a
i a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
fs = TT n
forall n. TT n
Erased TT n -> [TT n] -> [TT n]
forall a. a -> [a] -> [a]
: a -> t a -> [TT n] -> [TT n]
eraseArg (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) t a
fs [TT n]
ns
                           | Bool
otherwise = TT n
n TT n -> [TT n] -> [TT n]
forall a. a -> [a] -> [a]
: a -> t a -> [TT n] -> [TT n]
eraseArg (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) t a
fs [TT n]
ns
    eraseArg i :: a
i _ [] = []


-- | Find 'static' applications in a term and partially evaluate them.
-- Return any new transformation rules
elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]
-- Don't go deeper than 5 nested partially evaluated definitions in one go
-- (make this configurable? It's a good limit for most cases, certainly for
-- interfaces and polymorphic definitions, but maybe not for DSLs and
-- interpreters in complicated cases.
-- Possibly only worry about the limit if we've specialised the same function
-- a number of times in one go.)
elabPE :: ElabInfo
-> FC
-> Name
-> Type
-> StateT IState (ExceptT Err IO) [(Type, Type)]
elabPE info :: ElabInfo
info fc :: FC
fc caller :: Name
caller r :: Type
r | ElabInfo -> Int
pe_depth ElabInfo
info Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 5 = [(Type, Type)] -> StateT IState (ExceptT Err IO) [(Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
elabPE info :: ElabInfo
info fc :: FC
fc caller :: Name
caller r :: Type
r =
  do IState
ist <- Idris IState
getIState
     let sa :: [(Name, [(PEArgType, Type)])]
sa = ((Name, [(PEArgType, Type)]) -> Bool)
-> [(Name, [(PEArgType, Type)])] -> [(Name, [(PEArgType, Type)])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ap :: (Name, [(PEArgType, Type)])
ap -> (Name, [(PEArgType, Type)]) -> Name
forall a b. (a, b) -> a
fst (Name, [(PEArgType, Type)])
ap Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
caller) ([(Name, [(PEArgType, Type)])] -> [(Name, [(PEArgType, Type)])])
-> [(Name, [(PEArgType, Type)])] -> [(Name, [(PEArgType, Type)])]
forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> Type -> [(Name, [(PEArgType, Type)])]
getSpecApps IState
ist [] Type
r
     [[(Type, Type)]]
rules <- ((Name, [(PEArgType, Type)])
 -> StateT IState (ExceptT Err IO) [(Type, Type)])
-> [(Name, [(PEArgType, Type)])]
-> StateT IState (ExceptT Err IO) [[(Type, Type)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, [(PEArgType, Type)])
-> StateT IState (ExceptT Err IO) [(Type, Type)]
mkSpecialised [(Name, [(PEArgType, Type)])]
sa
     [(Type, Type)] -> StateT IState (ExceptT Err IO) [(Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Type, Type)] -> StateT IState (ExceptT Err IO) [(Type, Type)])
-> [(Type, Type)] -> StateT IState (ExceptT Err IO) [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ [[(Type, Type)]] -> [(Type, Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Type, Type)]]
rules
  where
    -- Make a specialised version of the application, and
    -- add a PTerm level transformation rule, which is basically the
    -- new definition in reverse (before specialising it).
    -- RHS => LHS where implicit arguments are left blank in the
    -- transformation.

    -- Transformation rules are applied after every PClause elaboration

    mkSpecialised :: (Name, [(PEArgType, Term)]) -> Idris [(Term, Term)]
    mkSpecialised :: (Name, [(PEArgType, Type)])
-> StateT IState (ExceptT Err IO) [(Type, Type)]
mkSpecialised specapp_in :: (Name, [(PEArgType, Type)])
specapp_in = do
        IState
ist <- Idris IState
getIState
        Context
ctxt <- Idris Context
getContext
        (specTy :: PTerm
specTy, specapp :: (Name, [(PEArgType, Type)])
specapp) <- IState
-> (Name, [(PEArgType, Type)])
-> StateT
     IState (ExceptT Err IO) (PTerm, (Name, [(PEArgType, Type)]))
getSpecTy IState
ist (Name, [(PEArgType, Type)])
specapp_in
        let (n :: Name
n, newnm :: Name
newnm, specdecl :: PEDecl
specdecl) = IState
-> (Name, [(PEArgType, Type)]) -> PTerm -> (Name, Name, PEDecl)
getSpecClause IState
ist (Name, [(PEArgType, Type)])
specapp PTerm
specTy
        let lhs :: PTerm
lhs = PEDecl -> PTerm
pe_app PEDecl
specdecl
        let rhs :: PTerm
rhs = PEDecl -> PTerm
pe_def PEDecl
specdecl
        let undef :: Bool
undef = case Name -> Context -> Maybe Def
lookupDefExact Name
newnm Context
ctxt of
                         Nothing -> Bool
True
                         _ -> Bool
False
        Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ (Name, Bool, [Bool]) -> String
forall a. Show a => a -> String
show (Name
newnm, Bool
undef, ((PEArgType, Type) -> Bool) -> [(PEArgType, Type)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> (PEArgType, Type) -> Bool
concreteArg IState
ist) ((Name, [(PEArgType, Type)]) -> [(PEArgType, Type)]
forall a b. (a, b) -> b
snd (Name, [(PEArgType, Type)])
specapp))
        StateT IState (ExceptT Err IO) [(Type, Type)]
-> (Err -> StateT IState (ExceptT Err IO) [(Type, Type)])
-> StateT IState (ExceptT Err IO) [(Type, Type)]
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
          (if (Bool
undef Bool -> Bool -> Bool
&& ((PEArgType, Type) -> Bool) -> [(PEArgType, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (IState -> (PEArgType, Type) -> Bool
concreteArg IState
ist) ((Name, [(PEArgType, Type)]) -> [(PEArgType, Type)]
forall a b. (a, b) -> b
snd (Name, [(PEArgType, Type)])
specapp)) then do
                [Name]
cgns <- Name -> Idris [Name]
getAllNames Name
n
                -- on the RHS of the new definition, we should reduce
                -- everything that's not itself static (because we'll
                -- want to be a PE version of those next)
                let cgns' :: [Name]
cgns' = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (\x :: Name
x -> Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
n Bool -> Bool -> Bool
&&
                                          IState -> Name -> Bool
notStatic IState
ist Name
x) [Name]
cgns
                -- set small reduction limit on partial/productive things
                let maxred :: Int
maxred = case Name -> Context -> [Totality]
lookupTotal Name
n Context
ctxt of
                                  [Total _] -> 65536
                                  [Productive] -> 16
                                  _ -> 1
                let specnames :: [(Name, Maybe Int)]
specnames = ((PEArgType, Type) -> Maybe (Name, Maybe Int))
-> [(PEArgType, Type)] -> [(Name, Maybe Int)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Bool -> (PEArgType, Type) -> Maybe (Name, Maybe Int)
forall a a.
Num a =>
Bool -> (PEArgType, TT a) -> Maybe (a, Maybe a)
specName (PEDecl -> Bool
pe_simple PEDecl
specdecl))
                                         ((Name, [(PEArgType, Type)]) -> [(PEArgType, Type)]
forall a b. (a, b) -> b
snd (Name, [(PEArgType, Type)])
specapp)
                [[(Name, Maybe Int)]]
descs <- (Name -> StateT IState (ExceptT Err IO) [(Name, Maybe Int)])
-> [Name] -> StateT IState (ExceptT Err IO) [[(Name, Maybe Int)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> StateT IState (ExceptT Err IO) [(Name, Maybe Int)]
getStaticsFrom (((Name, Maybe Int) -> Name) -> [(Name, Maybe Int)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Maybe Int) -> Name
forall a b. (a, b) -> a
fst [(Name, Maybe Int)]
specnames)

                let opts :: FnOpts
opts = [[(Name, Maybe Int)] -> FnOpt
Specialise ((if PEDecl -> Bool
pe_simple PEDecl
specdecl
                                            then (Name -> (Name, Maybe Int)) -> [Name] -> [(Name, Maybe Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: Name
x -> (Name
x, Maybe Int
forall a. Maybe a
Nothing)) [Name]
cgns'
                                            else []) [(Name, Maybe Int)] -> [(Name, Maybe Int)] -> [(Name, Maybe Int)]
forall a. [a] -> [a] -> [a]
++
                                         (Name
n, Int -> Maybe Int
forall a. a -> Maybe a
Just Int
maxred) (Name, Maybe Int) -> [(Name, Maybe Int)] -> [(Name, Maybe Int)]
forall a. a -> [a] -> [a]
: [(Name, Maybe Int)]
specnames [(Name, Maybe Int)] -> [(Name, Maybe Int)] -> [(Name, Maybe Int)]
forall a. [a] -> [a] -> [a]
++
                                             [[(Name, Maybe Int)]] -> [(Name, Maybe Int)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Name, Maybe Int)]]
descs)]
                Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Specialising application: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name, [(PEArgType, Type)]) -> String
forall a. Show a => a -> String
show (Name, [(PEArgType, Type)])
specapp
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n in \n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
caller String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              "\n with \n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FnOpts -> String
forall a. Show a => a -> String
show FnOpts
opts
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nCalling: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
cgns
                Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "New name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
newnm
                Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "PE definition type : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (PTerm -> String
forall a. Show a => a -> String
show PTerm
specTy)
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FnOpts -> String
forall a. Show a => a -> String
show FnOpts
opts
                Int -> String -> Idris ()
logElab 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "PE definition " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
newnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                             String -> [String] -> String
showSep "\n"
                                (((PTerm, PTerm) -> String) -> [(PTerm, PTerm)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (lhs :: PTerm
lhs, rhs :: PTerm
rhs) ->
                                  (PTerm -> String
showTmImpls PTerm
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                   PTerm -> String
showTmImpls PTerm
rhs)) (PEDecl -> [(PTerm, PTerm)]
pe_clauses PEDecl
specdecl))

                Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " transformation rule: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                           PTerm -> String
showTmImpls PTerm
rhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " ==> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs

                ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Type
elabType ElabInfo
info SyntaxInfo
defaultSyntax Docstring (Either Err PTerm)
forall a. Docstring a
emptyDocstring [] FC
fc FnOpts
opts Name
newnm FC
NoFC PTerm
specTy
                let def :: [PClause]
def = ((PTerm, PTerm) -> PClause) -> [(PTerm, PTerm)] -> [PClause]
forall a b. (a -> b) -> [a] -> [b]
map (\(lhs :: PTerm
lhs, rhs :: PTerm
rhs) ->
                                 let lhs' :: PTerm
lhs' = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
hiddenToPH (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState -> PTerm -> PTerm
stripUnmatchable IState
ist PTerm
lhs in
                                  FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl' PTerm] -> PClause
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
newnm PTerm
lhs' [] PTerm
rhs [])
                              (PEDecl -> [(PTerm, PTerm)]
pe_clauses PEDecl
specdecl)
                (Type, Type)
trans <- ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Type, Type)
elabTransform ElabInfo
info FC
fc Bool
False PTerm
rhs PTerm
lhs
                ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
elabClauses (ElabInfo
info {pe_depth :: Int
pe_depth = ElabInfo -> Int
pe_depth ElabInfo
info Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1}) FC
fc
                            (FnOpt
PEGeneratedFnOpt -> FnOpts -> FnOpts
forall a. a -> [a] -> [a]
:FnOpts
opts) Name
newnm [PClause]
def
                [(Type, Type)] -> StateT IState (ExceptT Err IO) [(Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Type, Type)
trans]
             else [(Type, Type)] -> StateT IState (ExceptT Err IO) [(Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
          -- if it doesn't work, just don't specialise. Could happen for lots
          -- of valid reasons (e.g. local variables in scope which can't be
          -- lifted out).
          (\e :: Err
e -> do Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Couldn't specialise: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (IState -> Err -> String
pshow IState
ist Err
e)
                    [(Type, Type)] -> StateT IState (ExceptT Err IO) [(Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [])

    hiddenToPH :: PTerm -> PTerm
hiddenToPH (PHidden _) = PTerm
Placeholder
    hiddenToPH x :: PTerm
x = PTerm
x

    specName :: Bool -> (PEArgType, TT a) -> Maybe (a, Maybe a)
specName simpl :: Bool
simpl (ImplicitS _, tm :: TT a
tm)
        | (P Ref n :: a
n _, _) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
tm = (a, Maybe a) -> Maybe (a, Maybe a)
forall a. a -> Maybe a
Just (a
n, a -> Maybe a
forall a. a -> Maybe a
Just (if Bool
simpl then 1 else 0))
    specName simpl :: Bool
simpl (ExplicitS, tm :: TT a
tm)
        | (P Ref n :: a
n _, _) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
tm = (a, Maybe a) -> Maybe (a, Maybe a)
forall a. a -> Maybe a
Just (a
n, a -> Maybe a
forall a. a -> Maybe a
Just (if Bool
simpl then 1 else 0))
    specName simpl :: Bool
simpl (ConstraintS, tm :: TT a
tm)
        | (P Ref n :: a
n _, _) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
tm = (a, Maybe a) -> Maybe (a, Maybe a)
forall a. a -> Maybe a
Just (a
n, a -> Maybe a
forall a. a -> Maybe a
Just (if Bool
simpl then 1 else 0))
    specName simpl :: Bool
simpl _ = Maybe (a, Maybe a)
forall a. Maybe a
Nothing

    -- get the descendants of the name 'n' which are marked %static
    -- Marking a function %static essentially means it's used to construct
    -- programs, so should be evaluated by the partial evaluator
    getStaticsFrom :: Name -> Idris [(Name, Maybe Int)]
    getStaticsFrom :: Name -> StateT IState (ExceptT Err IO) [(Name, Maybe Int)]
getStaticsFrom n :: Name
n = do [Name]
ns <- Name -> Idris [Name]
getAllNames Name
n
                          IState
i <- Idris IState
getIState
                          let statics :: [Name]
statics = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (IState -> Name -> Bool
staticFn IState
i) [Name]
ns
                          [(Name, Maybe Int)]
-> StateT IState (ExceptT Err IO) [(Name, Maybe Int)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name -> (Name, Maybe Int)) -> [Name] -> [(Name, Maybe Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\n :: Name
n -> (Name
n, Maybe Int
forall a. Maybe a
Nothing)) [Name]
statics)

    staticFn :: IState -> Name -> Bool
    staticFn :: IState -> Name -> Bool
staticFn i :: IState
i n :: Name
n =  case Name -> Ctxt FnOpts -> [FnOpts]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt FnOpts
idris_flags IState
i) of
                            [opts :: FnOpts
opts] -> FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FnOpt
StaticFn FnOpts
opts
                            _ -> Bool
False

    notStatic :: IState -> Name -> Bool
notStatic ist :: IState
ist n :: Name
n = case Name -> Ctxt [Bool] -> Maybe [Bool]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
ist) of
                           Just s :: [Bool]
s -> Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
s)
                           _ -> Bool
True

    concreteArg :: IState -> (PEArgType, Type) -> Bool
concreteArg ist :: IState
ist (ImplicitS _, tm :: Type
tm) = IState -> Type -> Bool
concreteTm IState
ist Type
tm
    concreteArg ist :: IState
ist (ExplicitS, tm :: Type
tm) = IState -> Type -> Bool
concreteTm IState
ist Type
tm
    concreteArg ist :: IState
ist _ = Bool
True

    concreteTm :: IState -> Type -> Bool
concreteTm ist :: IState
ist tm :: Type
tm | (P _ n :: Name
n _, _) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
tm =
        case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
             [] -> Bool
False
             _ -> Bool
True
    concreteTm ist :: IState
ist (Constant _) = Bool
True
    concreteTm ist :: IState
ist (Bind n :: Name
n (Lam _ _) sc :: Type
sc) = Bool
True
    concreteTm ist :: IState
ist (Bind n :: Name
n (Pi _ _ _ _) sc :: Type
sc) = Bool
True
    concreteTm ist :: IState
ist (Bind n :: Name
n (Let _ _ _) sc :: Type
sc) = IState -> Type -> Bool
concreteTm IState
ist Type
sc
    concreteTm ist :: IState
ist _ = Bool
False

    -- get the type of a specialised application
    getSpecTy :: IState
-> (Name, [(PEArgType, Type)])
-> StateT
     IState (ExceptT Err IO) (PTerm, (Name, [(PEArgType, Type)]))
getSpecTy ist :: IState
ist (n :: Name
n, args :: [(PEArgType, Type)]
args)
       = case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
              [ty :: Type
ty] -> let (specty_in :: Type
specty_in, args' :: [(PEArgType, Type)]
args') = [(PEArgType, Type)] -> Type -> (Type, [(PEArgType, Type)])
specType [(PEArgType, Type)]
args (Type -> Type
forall n. TT n -> TT n
explicitNames Type
ty)
                          specty :: Type
specty = Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) [] (Type -> Type
forall n. Eq n => TT n -> TT n
finalise Type
specty_in)
                          t :: PTerm
t = IState -> [(PEArgType, Type)] -> Type -> PTerm
mkPE_TyDecl IState
ist [(PEArgType, Type)]
args' (Type -> Type
forall n. TT n -> TT n
explicitNames Type
specty) in
                          (PTerm, (Name, [(PEArgType, Type)]))
-> StateT
     IState (ExceptT Err IO) (PTerm, (Name, [(PEArgType, Type)]))
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
t, (Name
n, [(PEArgType, Type)]
args'))
--                             (normalise (tt_ctxt ist) [] (specType args ty))
              _ -> String
-> StateT
     IState (ExceptT Err IO) (PTerm, (Name, [(PEArgType, Type)]))
forall a. String -> Idris a
ifail (String
 -> StateT
      IState (ExceptT Err IO) (PTerm, (Name, [(PEArgType, Type)])))
-> String
-> StateT
     IState (ExceptT Err IO) (PTerm, (Name, [(PEArgType, Type)]))
forall a b. (a -> b) -> a -> b
$ "Ambiguous name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (getSpecTy)"

    -- get the clause of a specialised application
    getSpecClause :: IState
-> (Name, [(PEArgType, Type)]) -> PTerm -> (Name, Name, PEDecl)
getSpecClause ist :: IState
ist (n :: Name
n, args :: [(PEArgType, Type)]
args) specTy :: PTerm
specTy
       = let newnm :: Name
newnm = String -> Name
sUN ("PE_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show (Name -> Name
nsroot Name
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                               Word64 -> String -> String
qhash 5381 (String -> [String] -> String
showSep "_" (((PEArgType, Type) -> String) -> [(PEArgType, Type)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (PEArgType, Type) -> String
forall a. Show a => (PEArgType, TT a) -> String
showArg [(PEArgType, Type)]
args))) in
                               -- UN (show n ++ show (map snd args)) in
             (Name
n, Name
newnm, IState -> Name -> Name -> PTerm -> [(PEArgType, Type)] -> PEDecl
mkPE_TermDecl IState
ist Name
newnm Name
n PTerm
specTy [(PEArgType, Type)]
args)
      where showArg :: (PEArgType, TT a) -> String
showArg (ExplicitS, n :: TT a
n) = TT a -> String
forall a. Show a => TT a -> String
qshow TT a
n
            showArg (ImplicitS _, n :: TT a
n) = TT a -> String
forall a. Show a => TT a -> String
qshow TT a
n
            showArg _ = ""

            qshow :: TT a -> String
qshow (Bind _ _ _) = "fn"
            qshow (App _ f :: TT a
f a :: TT a
a) = TT a -> String
qshow TT a
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ TT a -> String
qshow TT a
a
            qshow (P _ n :: a
n _) = a -> String
forall a. Show a => a -> String
show a
n
            qshow (Constant c :: Const
c) = Const -> String
forall a. Show a => a -> String
show Const
c
            qshow _ = ""

            -- Simple but effective string hashing...
            -- Keep it to 32 bits for readability/debuggability
            qhash :: Word64 -> String -> String
            qhash :: Word64 -> String -> String
qhash hash :: Word64
hash [] = Word64 -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
showHex (Word64 -> Word64
forall a. Num a => a -> a
abs Word64
hash Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`mod` 0xffffffff) ""
            qhash hash :: Word64
hash (x :: Char
x:xs :: String
xs) = Word64 -> String -> String
qhash (Word64
hash Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* 33 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral(Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
x)) String
xs

-- | Checks if the clause is a possible left hand side.
-- NOTE: A lot of this is repeated for reflected definitions in Idris.Elab.Term
-- One day, these should be merged, but until then remember that if you edit
-- this you might need to edit the other version...
checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossible info :: ElabInfo
info fc :: FC
fc tcgen :: Bool
tcgen fname :: Name
fname lhs_in :: PTerm
lhs_in
   = do Context
ctxt <- Idris Context
getContext
        IState
i <- Idris IState
getIState
        let lhs :: PTerm
lhs = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in
        Int -> String -> Idris ()
logElab 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Trying missing case: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs
        -- if the LHS type checks, it is possible
        case String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> EState
-> Elab' EState ElabResult
-> TC (ElabResult, String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN 0 "patLHS") Type
infP EState
initEState
                            (FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> [Name]
-> PTerm
-> Elab' EState ElabResult
buildTC IState
i ElabInfo
info ElabMode
EImpossible [] Name
fname
                                                (PTerm -> [Name]
allNamesIn PTerm
lhs_in)
                                                (PTerm -> PTerm
infTerm PTerm
lhs))) of
            OK (ElabResult lhs' :: Type
lhs' _ _ ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: Int
newGName, _) ->
               do Context -> Idris ()
setContext Context
ctxt'
                  ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
                  Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
                  (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
                  let lhs_tm :: Type
lhs_tm = Context -> Env -> Type -> Type
normalise Context
ctxt [] (Type -> Type
orderPats (Type -> Type
getInferTerm Type
lhs'))
                  let emptyPat :: Bool
emptyPat = Context -> Ctxt TypeInfo -> Type -> Bool
hasEmptyPat Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) Type
lhs_tm
                  if Bool
emptyPat then
                     do Int -> String -> Idris ()
logElab 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Empty type in pattern "
                        Maybe PTerm -> Idris (Maybe PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe PTerm
forall a. Maybe a
Nothing
                    else
                      case String -> Context -> Env -> Raw -> Type -> TC (Type, Type, UCs)
recheck (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt' [] (Type -> Raw
forget Type
lhs_tm) Type
lhs_tm of
                           OK (tm :: Type
tm, _, _) ->
                                    do Int -> String -> Idris ()
logElab 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Valid " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
                                                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
lhs
                                       Maybe PTerm -> Idris (Maybe PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> Maybe PTerm
forall a. a -> Maybe a
Just (IState -> Type -> Bool -> Bool -> PTerm
delab' IState
i Type
tm Bool
True Bool
True))
                           err :: TC (Type, Type, UCs)
err -> do Int -> String -> Idris ()
logElab 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Conversion failure"
                                     Maybe PTerm -> Idris (Maybe PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe PTerm
forall a. Maybe a
Nothing
            -- if it's a recoverable error, the case may become possible
            Error err :: Err
err -> do Int -> String -> Idris ()
logLvl 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Impossible case " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (IState -> Err -> String
pshow IState
i Err
err)
                                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Bool, Bool) -> String
forall a. Show a => a -> String
show (Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
err,
                                                  Context -> Err -> Bool
validCoverageCase Context
ctxt Err
err)
                            -- tcgen means that it was generated by genClauses,
                            -- so only looking for an error. Otherwise, it
                            -- needs to be the right kind of error (a type mismatch
                            -- in the same family).
                            if Bool
tcgen then IState -> Err -> Bool -> Idris (Maybe PTerm)
returnTm IState
i Err
err (Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
err)
                                  else IState -> Err -> Bool -> Idris (Maybe PTerm)
returnTm IState
i Err
err (Context -> Err -> Bool
validCoverageCase Context
ctxt Err
err Bool -> Bool -> Bool
||
                                                 Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
err)
  where returnTm :: IState -> Err -> Bool -> Idris (Maybe PTerm)
returnTm i :: IState
i err :: Err
err True = do Int -> String -> Idris ()
logLvl 10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Possibly resolvable error on " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                    IState -> Err -> String
pshow IState
i ((Type -> Type) -> Err -> Err
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
i) []) Err
err)
                                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ " on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs_in
                                 Maybe PTerm -> Idris (Maybe PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe PTerm -> Idris (Maybe PTerm))
-> Maybe PTerm -> Idris (Maybe PTerm)
forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe PTerm
forall a. a -> Maybe a
Just PTerm
lhs_in
        returnTm i :: IState
i err :: Err
err False = Maybe PTerm -> Idris (Maybe PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe PTerm -> Idris (Maybe PTerm))
-> Maybe PTerm -> Idris (Maybe PTerm)
forall a b. (a -> b) -> a -> b
$ Maybe PTerm
forall a. Maybe a
Nothing

-- Filter out the terms which are not well type left hand sides. Whenever we
-- eliminate one, also eliminate later ones which match it without checking,
-- because they're obviously going to have the same result
checkPossibles :: ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]
checkPossibles :: ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]
checkPossibles info :: ElabInfo
info fc :: FC
fc tcgen :: Bool
tcgen fname :: Name
fname (lhs :: PTerm
lhs : rest :: [PTerm]
rest)
   = do Maybe PTerm
ok <- ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossible ElabInfo
info FC
fc Bool
tcgen Name
fname PTerm
lhs
        IState
i <- Idris IState
getIState
        -- Hypothesis: any we can remove will be within the next few, because
        -- leftmost patterns tend to change less
        -- Since the match could take a while if there's a lot of cases to
        -- check, just remove from the next batch
        let rest' :: [PTerm]
rest' = (PTerm -> Bool) -> [PTerm] -> [PTerm]
forall a. (a -> Bool) -> [a] -> [a]
filter (\x :: PTerm
x -> Bool -> Bool
not (PTerm -> PTerm -> Bool
qmatch PTerm
x PTerm
lhs)) (Int -> [PTerm] -> [PTerm]
forall a. Int -> [a] -> [a]
take 200 [PTerm]
rest) [PTerm] -> [PTerm] -> [PTerm]
forall a. [a] -> [a] -> [a]
++ Int -> [PTerm] -> [PTerm]
forall a. Int -> [a] -> [a]
drop 200 [PTerm]
rest
        [PTerm]
restpos <- ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]
checkPossibles ElabInfo
info FC
fc Bool
tcgen Name
fname [PTerm]
rest'
        case Maybe PTerm
ok of
             Nothing -> [PTerm] -> Idris [PTerm]
forall (m :: * -> *) a. Monad m => a -> m a
return [PTerm]
restpos
             Just lhstm :: PTerm
lhstm -> [PTerm] -> Idris [PTerm]
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
lhstm PTerm -> [PTerm] -> [PTerm]
forall a. a -> [a] -> [a]
: [PTerm]
restpos)
  where
    qmatch :: PTerm -> PTerm -> Bool
qmatch _ Placeholder = Bool
True
    qmatch (PApp _ f :: PTerm
f args :: [PArg]
args) (PApp _ f' :: PTerm
f' args' :: [PArg]
args')
       | [PArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PArg]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [PArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PArg]
args'
            = PTerm -> PTerm -> Bool
qmatch PTerm
f PTerm
f' Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((PTerm -> PTerm -> Bool) -> [PTerm] -> [PTerm] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PTerm -> PTerm -> Bool
qmatch ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
args)
                                                 ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
args'))
    qmatch (PRef _ _ n :: Name
n) (PRef _ _ n' :: Name
n') = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
    qmatch (PPair _ _ _ l :: PTerm
l r :: PTerm
r) (PPair _ _ _ l' :: PTerm
l' r' :: PTerm
r') = PTerm -> PTerm -> Bool
qmatch PTerm
l PTerm
l' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
qmatch PTerm
r PTerm
r'
    qmatch (PDPair _ _ _ l :: PTerm
l t :: PTerm
t r :: PTerm
r) (PDPair _ _ _ l' :: PTerm
l' t' :: PTerm
t' r' :: PTerm
r')
          = PTerm -> PTerm -> Bool
qmatch PTerm
l PTerm
l' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
qmatch PTerm
t PTerm
t' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
qmatch PTerm
r PTerm
r'
    qmatch x :: PTerm
x y :: PTerm
y = PTerm
x PTerm -> PTerm -> Bool
forall a. Eq a => a -> a -> Bool
== PTerm
y
checkPossibles _ _ _ _ [] = [PTerm] -> Idris [PTerm]
forall (m :: * -> *) a. Monad m => a -> m a
return []

findUnique :: Context -> Env -> Term -> [Name]
findUnique :: Context -> Env -> Type -> [Name]
findUnique ctxt :: Context
ctxt env :: Env
env (Bind n :: Name
n b :: Binder Type
b sc :: Type
sc)
   = let rawTy :: Raw
rawTy = [Name] -> Type -> Raw
forgetEnv (((Name, RigCount, Binder Type) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Type) -> Name
forall a b c. (a, b, c) -> a
fstEnv Env
env) (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)
         uniq :: Bool
uniq = case Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
rawTy of
                     OK (_, UType UniqueType) -> Bool
True
                     OK (_, UType NullType) -> Bool
True
                     OK (_, UType AllTypes) -> Bool
True
                     _ -> Bool
False in
         if Bool
uniq then Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: Context -> Env -> Type -> [Name]
findUnique Context
ctxt ((Name
n, RigCount
RigW, Binder Type
b) (Name, RigCount, Binder Type) -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env) Type
sc
                 else Context -> Env -> Type -> [Name]
findUnique Context
ctxt ((Name
n, RigCount
RigW, Binder Type
b) (Name, RigCount, Binder Type) -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env) Type
sc
findUnique _ _ _ = []

-- | Return the elaborated LHS/RHS, and the original LHS with implicits added
elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
              Idris (Either Term (Term, Term), PTerm)
elabClause :: ElabInfo
-> FnOpts
-> (Int, PClause)
-> StateT IState (ExceptT Err IO) (Either Type (Type, Type), PTerm)
elabClause info :: ElabInfo
info opts :: FnOpts
opts (_, PClause fc :: FC
fc fname :: Name
fname lhs_in :: PTerm
lhs_in [] PImpossible [])
   = do let tcgen :: Bool
tcgen = FnOpt
Dictionary FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts
        IState
i <- Idris IState
forall s (m :: * -> *). MonadState s m => m s
get
        let lhs :: PTerm
lhs = [Name] -> IState -> PTerm -> PTerm
addImpl [] IState
i PTerm
lhs_in
        Maybe PTerm
b <- ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossible ElabInfo
info FC
fc Bool
tcgen Name
fname PTerm
lhs_in
        case Maybe PTerm
b of
            Just _ -> TC (Either Type (Type, Type), PTerm)
-> StateT IState (ExceptT Err IO) (Either Type (Type, Type), PTerm)
forall a. TC a -> Idris a
tclift (TC (Either Type (Type, Type), PTerm)
 -> StateT
      IState (ExceptT Err IO) (Either Type (Type, Type), PTerm))
-> TC (Either Type (Type, Type), PTerm)
-> StateT IState (ExceptT Err IO) (Either Type (Type, Type), PTerm)
forall a b. (a -> b) -> a -> b
$ Err -> TC (Either Type (Type, Type), PTerm)
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc
                                 (String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> String -> Err
forall a b. (a -> b) -> a -> b
$ PTerm -> String
forall a. Show a => a -> String
show PTerm
lhs_in String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is a valid case"))
            Nothing -> do Type
ptm <- PTerm -> Idris Type
mkPatTm PTerm
lhs_in
                          Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborated impossible case " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                      "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ptm
                          (Either Type (Type, Type), PTerm)
-> StateT IState (ExceptT Err IO) (Either Type (Type, Type), PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either Type (Type, Type)
forall a b. a -> Either a b
Left Type
ptm, PTerm
lhs)
elabClause info :: ElabInfo
info opts :: FnOpts
opts (cnum :: Int
cnum, PClause fc :: FC
fc fname :: Name
fname lhs_in_as :: PTerm
lhs_in_as withs :: [PTerm]
withs rhs_in_as :: PTerm
rhs_in_as whereblock_as :: [PDecl' PTerm]
whereblock_as)
   = do Name -> Bool -> Idris ()
push_estack Name
fname Bool
False
        Context
ctxt <- Idris Context
getContext
        let (lhs_in :: PTerm
lhs_in, rhs_in :: PTerm
rhs_in, whereblock :: [PDecl' PTerm]
whereblock) = PTerm -> PTerm -> [PDecl' PTerm] -> (PTerm, PTerm, [PDecl' PTerm])
desugarAs PTerm
lhs_in_as PTerm
rhs_in_as [PDecl' PTerm]
whereblock_as

        -- Build the LHS as an "Infer", and pull out its type and
        -- pattern bindings
        IState
i <- Idris IState
getIState
        Bool
inf <- Name -> Idris Bool
isTyInferred Name
fname

        -- Check if we have extra "with" patterns
        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [PTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
withs) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
            Err -> Idris ()
forall a. Err -> Idris a
ierror (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At (FC -> Maybe FC -> FC
forall a. a -> Maybe a -> a
fromMaybe FC
NoFC (Maybe FC -> FC) -> Maybe FC -> FC
forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe FC
highestFC PTerm
lhs_in_as)
                       (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating "left hand side of " Name
fname Maybe Type
forall a. Maybe a
Nothing
                        (String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> String -> Err
forall a b. (a -> b) -> a -> b
$ if PTerm -> Bool
isOutsideWith PTerm
lhs_in
                               then "unexpected patterns outside of \"with\" block"
                               else "unexpected extra \"with\" patterns")))

        -- get the parameters first, to pass through to any where block
        let fn_ty :: Type
fn_ty = case Name -> Context -> [Type]
lookupTy Name
fname Context
ctxt of
                         [t :: Type
t] -> Type
t
                         _ -> String -> Type
forall a. HasCallStack => String -> a
error "Can't happen (elabClause function type)"
        let fn_is :: [PArg]
fn_is = case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
fname (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                         [t :: [PArg]
t] -> [PArg]
t
                         _ -> []
        let norm_ty :: Type
norm_ty = Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
fn_ty
        let params :: [Name]
params = IState -> [Name] -> [PArg] -> Type -> [Name]
getParamsInType IState
i [] [PArg]
fn_is Type
norm_ty
        let tcparams :: [Name]
tcparams = IState -> [Name] -> [PArg] -> Type -> [Name]
getTCParamsInType IState
i [] [PArg]
fn_is Type
norm_ty

        let lhs :: PTerm
lhs = PTerm -> PTerm
mkLHSapp (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState -> PTerm -> PTerm
stripLinear IState
i (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState -> PTerm -> PTerm
stripUnmatchable IState
i (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                    IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
propagateParams IState
i [Name]
params Type
norm_ty (PTerm -> [Name]
allNamesIn PTerm
lhs_in) (IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in)

--         let lhs = mkLHSapp $
--                     propagateParams i params fn_ty (addImplPat i lhs_in)
        Int -> String -> Idris ()
logElab 10 (([Name], Type) -> String
forall a. Show a => a -> String
show ([Name]
params, Type
fn_ty) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls (IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in))
        Int -> String -> Idris ()
logElab 5 ("LHS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FnOpts -> String
forall a. Show a => a -> String
show FnOpts
opts String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs)
        Int -> String -> Idris ()
logElab 4 ("Fixed parameters: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
params String -> String -> String
forall a. [a] -> [a] -> [a]
++ " from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs_in String -> String -> String
forall a. [a] -> [a] -> [a]
++
                  "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Type, [PArg]) -> String
forall a. Show a => a -> String
show (Type
fn_ty, [PArg]
fn_is))

        ((ElabResult lhs' :: Type
lhs' dlhs :: [(Name, (Int, Maybe Name, Type, [Name]))]
dlhs [] ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: Int
newGName, probs :: Fails
probs, inj :: [Name]
inj), _) <-
           TC ((ElabResult, Fails, [Name]), String)
-> Idris ((ElabResult, Fails, [Name]), String)
forall a. TC a -> Idris a
tclift (TC ((ElabResult, Fails, [Name]), String)
 -> Idris ((ElabResult, Fails, [Name]), String))
-> TC ((ElabResult, Fails, [Name]), String)
-> Idris ((ElabResult, Fails, [Name]), String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> EState
-> Elab' EState (ElabResult, Fails, [Name])
-> TC ((ElabResult, Fails, [Name]), String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN 0 "patLHS") Type
infP EState
initEState
                    (do ElabResult
res <- String
-> Name
-> Maybe Type
-> Elab' EState ElabResult
-> Elab' EState ElabResult
forall aux a.
String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
errAt "left hand side of " Name
fname Maybe Type
forall a. Maybe a
Nothing
                                 (FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun (FC -> Maybe FC -> FC
forall a. a -> Maybe a -> a
fromMaybe FC
NoFC (Maybe FC -> FC) -> Maybe FC -> FC
forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe FC
highestFC PTerm
lhs_in_as)
                                       (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> [Name]
-> PTerm
-> Elab' EState ElabResult
buildTC IState
i ElabInfo
info ElabMode
ELHS FnOpts
opts Name
fname
                                          (PTerm -> [Name]
allNamesIn PTerm
lhs_in)
                                          (PTerm -> PTerm
infTerm PTerm
lhs)))
                        Fails
probs <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
                        [Name]
inj <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_inj
                        (ElabResult, Fails, [Name])
-> Elab' EState (ElabResult, Fails, [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return (ElabResult
res, Fails
probs, [Name]
inj))
        Context -> Idris ()
setContext Context
ctxt'
        ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
        Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
        (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }

        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
inf (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> [(Type, Type)] -> Idris ()
addTyInfConstraints FC
fc (((Type, Type, Bool, Env, Err, [FailContext], FailAt)
 -> (Type, Type))
-> Fails -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: Type
x,y :: Type
y,_,_,_,_,_) -> (Type
x,Type
y)) Fails
probs)

        let lhs_tm :: Type
lhs_tm = Type -> Type
orderPats (Type -> Type
getInferTerm Type
lhs')
        let lhs_ty :: Type
lhs_ty = Type -> Type
getInferType Type
lhs'
        let static_names :: [Name]
static_names = IState -> Type -> [Name]
getStaticNames IState
i Type
lhs_tm

        Int -> String -> Idris ()
logElab 3 ("Elaborated: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
lhs_tm)
        Int -> String -> Idris ()
logElab 3 ("Elaborated type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
lhs_ty)
        Int -> String -> Idris ()
logElab 5 ("Injective: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
fname String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
inj)

        -- If we're inferring metavariables in the type, don't recheck,
        -- because we're only doing this to try to work out those metavariables
        Context
ctxt <- Idris Context
getContext
        (clhs_c :: Type
clhs_c, clhsty :: Type
clhsty) <- if Bool -> Bool
not Bool
inf
                               then Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err -> Err)
-> Env
-> Type
-> Idris (Type, Type)
recheckC_borrowing Bool
False (FnOpt
PEGenerated FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts)
                                                       [] (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc Err -> Err
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Type
lhs_tm
                               else (Type, Type) -> Idris (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
lhs_tm, Type
lhs_ty)
        let clhs :: Type
clhs = Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
clhs_c
        -- These are the names we're not allowed to use on the RHS, because
        -- they're UniqueTypes and borrowed from another function.
        let borrowed :: [Name]
borrowed = [Name] -> Type -> [Name]
borrowedNames [] Type
clhs

        Int -> String -> Idris ()
logElab 3 ("Normalised LHS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls (IState -> Type -> PTerm
delabMV IState
i Type
clhs))

        Bool
rep <- Idris Bool
useREPL
        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
rep (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
          String -> Int -> PTerm -> Idris ()
addInternalApp (FC -> String
fc_fname FC
fc) ((Int, Int) -> Int
forall a b. (a, b) -> a
fst ((Int, Int) -> Int) -> (FC -> (Int, Int)) -> FC -> Int
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> (Int, Int)
fc_start (FC -> Int) -> FC -> Int
forall a b. (a -> b) -> a -> b
$ FC
fc) (IState -> Type -> PTerm
delabMV IState
i Type
clhs) -- TODO: Should use span instead of line and filename?
        IBCWrite -> Idris ()
addIBC (String -> Int -> PTerm -> IBCWrite
IBCLineApp (FC -> String
fc_fname FC
fc) ((Int, Int) -> Int
forall a b. (a, b) -> a
fst ((Int, Int) -> Int) -> (FC -> (Int, Int)) -> FC -> Int
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> (Int, Int)
fc_start (FC -> Int) -> FC -> Int
forall a b. (a -> b) -> a -> b
$ FC
fc) (IState -> Type -> PTerm
delabMV IState
i Type
clhs))

        Int -> String -> Idris ()
logElab 5 ("Checked " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
clhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
clhsty)
        -- Elaborate where block
        IState
ist <- Idris IState
getIState
        Context
ctxt <- Idris Context
getContext

        Int
windex <- Idris Int
getName
        let decls :: [Name]
decls = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ((PDecl' PTerm -> [Name]) -> [PDecl' PTerm] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl' PTerm -> [Name]
declared [PDecl' PTerm]
whereblock)
        let defs :: [Name]
defs = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name]
decls [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (PDecl' PTerm -> [Name]) -> [PDecl' PTerm] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl' PTerm -> [Name]
defined [PDecl' PTerm]
whereblock)
        let newargs_all :: [(Name, PTerm)]
newargs_all = IState -> Type -> [(Name, PTerm)]
pvars IState
ist Type
lhs_tm

        -- Unique arguments must be passed to the where block explicitly
        -- (since we can't control "usage" easlily otherwise). Remove them
        -- from newargs here
        let uniqargs :: [Name]
uniqargs = Context -> Env -> Type -> [Name]
findUnique Context
ctxt [] Type
lhs_tm
        let newargs :: [(Name, PTerm)]
newargs = ((Name, PTerm) -> Bool) -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(n :: Name
n,_) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
uniqargs) [(Name, PTerm)]
newargs_all

        let winfo :: ElabInfo
winfo = (ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
pinfo ElabInfo
info [(Name, PTerm)]
newargs [Name]
defs Int
windex) { elabFC :: Maybe FC
elabFC = FC -> Maybe FC
forall a. a -> Maybe a
Just FC
fc }
        let wb :: [PDecl' PTerm]
wb = (PDecl' PTerm -> PDecl' PTerm) -> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> PDecl' PTerm -> PDecl' PTerm
mkStatic [Name]
static_names) ([PDecl' PTerm] -> [PDecl' PTerm])
-> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> a -> b
$
                 (PDecl' PTerm -> PDecl' PTerm) -> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (IState
-> (Name -> Name)
-> [(Name, PTerm)]
-> [Name]
-> PDecl' PTerm
-> PDecl' PTerm
forall p1 p2 t p3.
p1 -> p2 -> [(Name, t)] -> p3 -> PDecl' t -> PDecl' t
expandImplementationScope IState
ist Name -> Name
decorate [(Name, PTerm)]
newargs [Name]
defs) ([PDecl' PTerm] -> [PDecl' PTerm])
-> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> a -> b
$
                 (PDecl' PTerm -> PDecl' PTerm) -> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> IState
-> (Name -> Name)
-> [(Name, PTerm)]
-> [Name]
-> PDecl' PTerm
-> PDecl' PTerm
expandParamsD Bool
False IState
ist Name -> Name
decorate [(Name, PTerm)]
newargs [Name]
defs) [PDecl' PTerm]
whereblock

        -- Split the where block into declarations with a type, and those
        -- without
        -- Elaborate those with a type *before* RHS, those without *after*
        let (wbefore :: [PDecl' PTerm]
wbefore, wafter :: [PDecl' PTerm]
wafter) = [PDecl' PTerm] -> ([PDecl' PTerm], [PDecl' PTerm])
forall t. [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks [PDecl' PTerm]
wb

        Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Where block:\n " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl' PTerm] -> String
forall a. Show a => a -> String
show [PDecl' PTerm]
wbefore String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl' PTerm] -> String
forall a. Show a => a -> String
show [PDecl' PTerm]
wafter
        (PDecl' PTerm -> Idris ()) -> [PDecl' PTerm] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl' PTerm -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
winfo) [PDecl' PTerm]
wbefore
        -- Now build the RHS, using the type of the LHS as the goal.
        IState
i <- Idris IState
getIState -- new implicits from where block
        Int -> String -> Idris ()
logElab 5 (PTerm -> String
showTmImpls ((Name -> Name)
-> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTerm
expandParams Name -> Name
decorate [(Name, PTerm)]
newargs [Name]
defs ([Name]
defs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
decls) PTerm
rhs_in))
        let rhs :: PTerm
rhs = ElabInfo -> PTerm -> PTerm
rhs_trans ElabInfo
info (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                   IState -> [Name] -> [Name] -> PTerm -> PTerm
addImplBoundInf IState
i (((Name, PTerm) -> Name) -> [(Name, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, PTerm)]
newargs_all) ([Name]
defs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
decls)
                                 ((Name -> Name)
-> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTerm
expandParams Name -> Name
decorate [(Name, PTerm)]
newargs [Name]
defs ([Name]
defs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
decls) PTerm
rhs_in)
        Int -> String -> Idris ()
logElab 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "RHS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (((Name, PTerm) -> Name) -> [(Name, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, PTerm)]
newargs_all) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs
        Context
ctxt <- Idris Context
getContext -- new context with where block added
        Int -> String -> Idris ()
logElab 5 "STARTING CHECK"
        ((rhsElab :: Type
rhsElab, defer :: [(Name, (Int, Maybe Name, Type, [Name]))]
defer, holes :: [Name]
holes, is :: [PDecl' PTerm]
is, probs :: Fails
probs, ctxt' :: Context
ctxt', newDecls :: [RDeclInstructions]
newDecls, highlights :: Set (FC', OutputAnnotation)
highlights, newGName :: Int
newGName), _) <-
           TC
  ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
    [PDecl' PTerm], Fails, Context, [RDeclInstructions],
    Set (FC', OutputAnnotation), Int),
   String)
-> Idris
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
       [PDecl' PTerm], Fails, Context, [RDeclInstructions],
       Set (FC', OutputAnnotation), Int),
      String)
forall a. TC a -> Idris a
tclift (TC
   ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
     [PDecl' PTerm], Fails, Context, [RDeclInstructions],
     Set (FC', OutputAnnotation), Int),
    String)
 -> Idris
      ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
        [PDecl' PTerm], Fails, Context, [RDeclInstructions],
        Set (FC', OutputAnnotation), Int),
       String))
-> TC
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
       [PDecl' PTerm], Fails, Context, [RDeclInstructions],
       Set (FC', OutputAnnotation), Int),
      String)
-> Idris
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
       [PDecl' PTerm], Fails, Context, [RDeclInstructions],
       Set (FC', OutputAnnotation), Int),
      String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> EState
-> Elab'
     EState
     (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
      [PDecl' PTerm], Fails, Context, [RDeclInstructions],
      Set (FC', OutputAnnotation), Int)
-> TC
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
       [PDecl' PTerm], Fails, Context, [RDeclInstructions],
       Set (FC', OutputAnnotation), Int),
      String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN 0 "patRHS") Type
clhsty EState
initEState
                    (do IState -> Type -> ElabD ()
pbinds IState
ist Type
lhs_tm
                        -- proof search can use explicitly written names
                        (Name -> ElabD ()) -> [Name] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> ElabD ()
forall aux. Name -> Elab' aux ()
addPSname (PTerm -> [Name]
allNamesIn PTerm
lhs_in)
                        Bool
ulog <- Elab' EState Bool
forall aux. Elab' aux Bool
getUnifyLog
                        Bool -> String -> ElabD () -> ElabD ()
forall p. Bool -> String -> p -> p
traceWhen Bool
ulog ("Setting injective: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show ([Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name]
tcparams [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
inj))) (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$
                          (Name -> ElabD ()) -> [Name] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> ElabD ()
forall aux. Name -> Elab' aux ()
setinj ([Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name]
tcparams [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
inj))
                        ElabD ()
forall aux. Elab' aux ()
setNextName
                        (ElabResult _ _ is :: [PDecl' PTerm]
is ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: Int
newGName) <-
                          String
-> Name
-> Maybe Type
-> Elab' EState ElabResult
-> Elab' EState ElabResult
forall aux a.
String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
errAt "right hand side of " Name
fname (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
clhsty)
                                (FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> Elab' EState ElabResult
build IState
i ElabInfo
winfo ElabMode
ERHS FnOpts
opts Name
fname PTerm
rhs))
                        String -> Name -> Maybe Type -> ElabD () -> ElabD ()
forall aux a.
String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
errAt "right hand side of " Name
fname (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
clhsty)
                              (FC -> ElabD () -> ElabD ()
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ Type -> ElabD ()
forall n aux. TT n -> StateT (ElabState aux) TC ()
psolve Type
lhs_tm)
                        Type
tt <- Elab' EState Type
forall aux. Elab' aux Type
get_term
                        EState
aux <- Elab' EState EState
forall aux. Elab' aux aux
getAux
                        let (tm :: Type
tm, ds :: [(Name, (Int, Maybe Name, Type, [Name]))]
ds) = State [(Name, (Int, Maybe Name, Type, [Name]))] Type
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> (Type, [(Name, (Int, Maybe Name, Type, [Name]))])
forall s a. State s a -> s -> (a, s)
runState (Maybe Name
-> [Name]
-> Context
-> Type
-> State [(Name, (Int, Maybe Name, Type, [Name]))] Type
collectDeferred (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
fname)
                                                     (((Name, PDecl' PTerm) -> Name) -> [(Name, PDecl' PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PDecl' PTerm) -> Name
forall a b. (a, b) -> a
fst ([(Name, PDecl' PTerm)] -> [Name])
-> [(Name, PDecl' PTerm)] -> [Name]
forall a b. (a -> b) -> a -> b
$ EState -> [(Name, PDecl' PTerm)]
case_decls EState
aux) Context
ctxt Type
tt) []
                        Fails
probs <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
                        [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                        (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
 [PDecl' PTerm], Fails, Context, [RDeclInstructions],
 Set (FC', OutputAnnotation), Int)
-> Elab'
     EState
     (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [Name],
      [PDecl' PTerm], Fails, Context, [RDeclInstructions],
      Set (FC', OutputAnnotation), Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tm, [(Name, (Int, Maybe Name, Type, [Name]))]
ds, [Name]
hs, [PDecl' PTerm]
is, Fails
probs, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName))
        Context -> Idris ()
setContext Context
ctxt'
        ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
        Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
        (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }

        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
inf (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> [(Type, Type)] -> Idris ()
addTyInfConstraints FC
fc (((Type, Type, Bool, Env, Err, [FailContext], FailAt)
 -> (Type, Type))
-> Fails -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: Type
x,y :: Type
y,_,_,_,_,_) -> (Type
x,Type
y)) Fails
probs)

        Int -> String -> Idris ()
logElab 3 "DONE CHECK"
        Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "---> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
rhsElab
        Context
ctxt <- Idris Context
getContext

        let rhs' :: Type
rhs' = Type
rhsElab

        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([(Name, (Int, Maybe Name, Type, [Name]))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, (Int, Maybe Name, Type, [Name]))]
defer)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> String -> Idris ()
logElab 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "DEFERRED " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                    [(Name, Type)] -> String
forall a. Show a => a -> String
show (((Name, (Int, Maybe Name, Type, [Name])) -> (Name, Type))
-> [(Name, (Int, Maybe Name, Type, [Name]))] -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: Name
n, (_,_,t :: Type
t,_)) -> (Name
n, Type
t)) [(Name, (Int, Maybe Name, Type, [Name]))]
defer)

        -- If there's holes, set the metavariables as undefinable
        [(Name, (Int, Maybe Name, Type, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkDef ElabInfo
info FC
fc (\n :: Name
n -> String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating "deferred type of " Name
n Maybe Type
forall a. Maybe a
Nothing) ([Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
holes) [(Name, (Int, Maybe Name, Type, [Name]))]
defer
        let def'' :: [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def'' = ((Name, (Int, Maybe Name, Type, [Name]))
 -> (Name, (Int, Maybe Name, Type, [Name], Bool, Bool)))
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, (i :: Int
i, top :: Maybe Name
top, t :: Type
t, ns :: [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Type
t, [Name]
ns, Bool
False, [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
holes))) [(Name, (Int, Maybe Name, Type, [Name]))]
def'
        [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def''

        ((Name, (Int, Maybe Name, Type, [Name], Bool, Bool)) -> Idris ())
-> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
-> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(n :: Name
n, _) -> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)) [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def''

        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([(Name, (Int, Maybe Name, Type, [Name]))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, (Int, Maybe Name, Type, [Name]))]
def')) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
           ((FC, Name) -> Idris ()) -> [(FC, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
defer_totcheck (((Name, (Int, Maybe Name, Type, [Name], Bool, Bool)) -> (FC, Name))
-> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
-> [(FC, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: (Name, (Int, Maybe Name, Type, [Name], Bool, Bool))
x -> (FC
fc, (Name, (Int, Maybe Name, Type, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (Name, (Int, Maybe Name, Type, [Name], Bool, Bool))
x)) [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def'')

        -- Now the remaining deferred (i.e. no type declarations) clauses
        -- from the where block

        (PDecl' PTerm -> Idris ()) -> [PDecl' PTerm] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl' PTerm -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
winfo) [PDecl' PTerm]
wafter
        (PDecl' PTerm -> Idris ()) -> [PDecl' PTerm] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> FnOpts -> PDecl' PTerm -> Idris ()
elabCaseBlock ElabInfo
winfo FnOpts
opts) [PDecl' PTerm]
is

        Context
ctxt <- Idris Context
getContext
        Int -> String -> Idris ()
logElab 5 "Rechecking"
        Int -> String -> Idris ()
logElab 6 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ " ==> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Raw -> String
forall a. Show a => a -> String
show (Type -> Raw
forget Type
rhs')

        (crhs :: Type
crhs, crhsty :: Type
crhsty) -- if there's holes && deferred things, it's okay
                       -- but we'll need to freeze the definition and not
                       -- allow the deferred things to be definable
                       -- (this is just to allow users to inspect intermediate
                       -- things)
             <- if ([Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
holes Bool -> Bool -> Bool
|| [(Name, (Int, Maybe Name, Type, [Name]))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, (Int, Maybe Name, Type, [Name]))]
def') Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
inf
                   then Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err -> Err)
-> Env
-> Type
-> Idris (Type, Type)
recheckC_borrowing Bool
True (FnOpt
PEGenerated FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts)
                                       [Name]
borrowed (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc Err -> Err
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Type
rhs'
                   else (Type, Type) -> Idris (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
rhs', Type
clhsty)

        Int -> String -> Idris ()
logElab 6 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ " ==> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Env -> Type -> String
forall a.
(Show a, Eq a) =>
[(a, RigCount, Binder (TT a))] -> TT a -> String
showEnvDbg [] Type
crhsty String -> String -> String
forall a. [a] -> [a] -> [a]
++ "   against   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Env -> Type -> String
forall a.
(Show a, Eq a) =>
[(a, RigCount, Binder (TT a))] -> TT a -> String
showEnvDbg [] Type
clhsty

        -- If there's holes, make sure this definition is frozen
        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
holes)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
           Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Making " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
fname String -> String -> String
forall a. [a] -> [a] -> [a]
++ " frozen due to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
holes
           Name -> Accessibility -> Idris ()
setAccessibility Name
fname Accessibility
Frozen

        Context
ctxt <- Idris Context
getContext
        let constv :: Int
constv = Context -> Int
next_tvar Context
ctxt
        Bool
tit <- Idris Bool
typeInType
        case StateT UCs TC () -> UCs -> TC ((), UCs)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LState.runStateT (Context -> Env -> Type -> Type -> StateT UCs TC ()
convertsC Context
ctxt [] Type
crhsty Type
clhsty) (Int
constv, []) of
            OK (_, cs :: UCs
cs) -> Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
PEGenerated FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
tit) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
                             FC -> UCs -> Idris ()
addConstraints FC
fc UCs
cs
                             (UConstraint -> Idris ()) -> [UConstraint] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\c :: UConstraint
c -> IBCWrite -> Idris ()
addIBC (FC -> UConstraint -> IBCWrite
IBCConstraint FC
fc UConstraint
c)) (UCs -> [UConstraint]
forall a b. (a, b) -> b
snd UCs
cs)
                             Int -> String -> Idris ()
logElab 6 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "CONSTRAINTS ADDED: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UCs -> String
forall a. Show a => a -> String
show UCs
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Type, Type) -> String
forall a. Show a => a -> String
show (Type
clhsty, Type
crhsty)
                             () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Error e :: Err
e -> Err -> Idris ()
forall a. Err -> Idris a
ierror (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Bool
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> Err
-> [(Name, Type)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (Type
clhsty, Maybe Provenance
forall a. Maybe a
Nothing) (Type
crhsty, Maybe Provenance
forall a. Maybe a
Nothing) Err
e [] 0))
        IState
i <- Idris IState
getIState
        FC -> PTerm -> PTerm -> Idris ()
checkInferred FC
fc (IState -> Type -> Bool -> Bool -> PTerm
delab' IState
i Type
crhs Bool
True Bool
True) PTerm
rhs
        -- if the function is declared '%error_reverse',
        -- then we'll try running it in reverse to improve error messages
        -- Also if the type is '%error_reverse' and the LHS is smaller than
        -- the RHS
        let (ret_fam :: Type
ret_fam, _) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
crhsty)
        Bool
rev <- case Type
ret_fam of
                    P _ rfamn :: Name
rfamn _ ->
                        case Name -> Ctxt TypeInfo -> [TypeInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
rfamn (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
                             [TI _ _ dopts :: DataOpts
dopts _ _ _] ->
                                 Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (DataOpt
DataErrRev DataOpt -> DataOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` DataOpts
dopts Bool -> Bool -> Bool
&&
                                         Type -> Int
forall a. Sized a => a -> Int
size Type
clhs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Type -> Int
forall a. Sized a => a -> Int
size Type
crhs)
                             _ -> Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    _ -> Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
rev Bool -> Bool -> Bool
|| FnOpt
ErrorReverse FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
           IBCWrite -> Idris ()
addIBC ((Type, Type) -> IBCWrite
IBCErrRev (Type
crhs, Type
clhs))
           (Type, Type) -> Idris ()
addErrRev (Type
crhs, Type
clhs)
        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
rev Bool -> Bool -> Bool
|| FnOpt
ErrorReduce FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
           IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCErrReduce Name
fname)
           Name -> Idris ()
addErrReduce Name
fname
        Idris ()
pop_estack
        (Either Type (Type, Type), PTerm)
-> StateT IState (ExceptT Err IO) (Either Type (Type, Type), PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type) -> Either Type (Type, Type)
forall a b. b -> Either a b
Right (Type
clhs, Type
crhs), PTerm
lhs)
  where
    pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
    pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
pinfo info :: ElabInfo
info ns :: [(Name, PTerm)]
ns ds :: [Name]
ds i :: Int
i
          = let newps :: [(Name, PTerm)]
newps = ElabInfo -> [(Name, PTerm)]
params ElabInfo
info [(Name, PTerm)] -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ns
                dsParams :: [(Name, [Name])]
dsParams = (Name -> (Name, [Name])) -> [Name] -> [(Name, [Name])]
forall a b. (a -> b) -> [a] -> [b]
map (\n :: Name
n -> (Name
n, ((Name, PTerm) -> Name) -> [(Name, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, PTerm)]
newps)) [Name]
ds
                newb :: Ctxt [Name]
newb = [(Name, [Name])] -> Ctxt [Name] -> Ctxt [Name]
forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, [Name])]
dsParams (ElabInfo -> Ctxt [Name]
inblock ElabInfo
info) in
                ElabInfo
info { params :: [(Name, PTerm)]
params = [(Name, PTerm)]
newps,
                       inblock :: Ctxt [Name]
inblock = Ctxt [Name]
newb,
                       liftname :: Name -> Name
liftname = Name -> Name
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id -- (\n -> case lookupCtxt n newb of
                                     --      Nothing -> n
                                     --      _ -> MN i (show n)) . l
                     }

    -- Find the variable names which appear under a 'Ownership.Read' so that
    -- we know they can't be used on the RHS
    borrowedNames :: [Name] -> Term -> [Name]
    borrowedNames :: [Name] -> Type -> [Name]
borrowedNames env :: [Name]
env (App _ (App _ (P _ (NS (UN lend :: Text
lend) [owner :: Text
owner]) _) _) arg :: Type
arg)
        | Text
owner Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Ownership" Bool -> Bool -> Bool
&&
          (Text
lend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "lend" Bool -> Bool -> Bool
|| Text
lend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Read") = Type -> [Name]
forall n. TT n -> [Name]
getVs Type
arg
       where
         getVs :: TT n -> [Name]
getVs (V i :: Int
i) = [[Name]
env[Name] -> Int -> Name
forall a. [a] -> Int -> a
!!Int
i]
         getVs (App _ f :: TT n
f a :: TT n
a) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ TT n -> [Name]
getVs TT n
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ TT n -> [Name]
getVs TT n
a
         getVs _ = []
    borrowedNames env :: [Name]
env (App _ f :: Type
f a :: Type
a) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> Type -> [Name]
borrowedNames [Name]
env Type
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name] -> Type -> [Name]
borrowedNames [Name]
env Type
a
    borrowedNames env :: [Name]
env (Bind n :: Name
n b :: Binder Type
b sc :: Type
sc) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Binder Type -> [Name]
borrowedB Binder Type
b [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name] -> Type -> [Name]
borrowedNames (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env) Type
sc
       where borrowedB :: Binder Type -> [Name]
borrowedB (Let _ t :: Type
t v :: Type
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> Type -> [Name]
borrowedNames [Name]
env Type
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name] -> Type -> [Name]
borrowedNames [Name]
env Type
v
             borrowedB b :: Binder Type
b = [Name] -> Type -> [Name]
borrowedNames [Name]
env (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)
    borrowedNames _ _ = []

    mkLHSapp :: PTerm -> PTerm
mkLHSapp t :: PTerm
t@(PRef _ _ _) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
t []
    mkLHSapp t :: PTerm
t = PTerm
t

    decorate :: Name -> Name
decorate (NS x :: Name
x ns :: [Text]
ns)
       = Name -> [Text] -> Name
NS (SpecialName -> Name
SN (Int -> Name -> Name -> SpecialName
WhereN Int
cnum Name
fname Name
x)) [Text]
ns
    decorate x :: Name
x
       = SpecialName -> Name
SN (Int -> Name -> Name -> SpecialName
WhereN Int
cnum Name
fname Name
x)

    sepBlocks :: [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks bs :: [PDecl' t]
bs = [Name] -> [PDecl' t] -> ([PDecl' t], [PDecl' t])
forall t. [Name] -> [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks' [] [PDecl' t]
bs where
      sepBlocks' :: [Name] -> [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks' ns :: [Name]
ns (d :: PDecl' t
d@(PTy _ _ _ _ _ n :: Name
n _ t :: t
t) : bs :: [PDecl' t]
bs)
            = let (bf :: [PDecl' t]
bf, af :: [PDecl' t]
af) = [Name] -> [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks' (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
ns) [PDecl' t]
bs in
                  (PDecl' t
d PDecl' t -> [PDecl' t] -> [PDecl' t]
forall a. a -> [a] -> [a]
: [PDecl' t]
bf, [PDecl' t]
af)
      sepBlocks' ns :: [Name]
ns (d :: PDecl' t
d@(PClauses _ _ n :: Name
n _) : bs :: [PDecl' t]
bs)
         | Bool -> Bool
not (Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns) = let (bf :: [PDecl' t]
bf, af :: [PDecl' t]
af) = [Name] -> [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks' [Name]
ns [PDecl' t]
bs in
                                   ([PDecl' t]
bf, PDecl' t
d PDecl' t -> [PDecl' t] -> [PDecl' t]
forall a. a -> [a] -> [a]
: [PDecl' t]
af)
      sepBlocks' ns :: [Name]
ns (b :: PDecl' t
b : bs :: [PDecl' t]
bs) = let (bf :: [PDecl' t]
bf, af :: [PDecl' t]
af) = [Name] -> [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks' [Name]
ns [PDecl' t]
bs in
                                   (PDecl' t
b PDecl' t -> [PDecl' t] -> [PDecl' t]
forall a. a -> [a] -> [a]
: [PDecl' t]
bf, [PDecl' t]
af)
      sepBlocks' ns :: [Name]
ns [] = ([], [])

    -- term is not within "with" block
    isOutsideWith :: PTerm -> Bool
    isOutsideWith :: PTerm -> Bool
isOutsideWith (PApp _ (PRef _ _ (SN (WithN _ _))) _) = Bool
False
    isOutsideWith _ = Bool
True

elabClause info :: ElabInfo
info opts :: FnOpts
opts (_, PWith fc :: FC
fc fname :: Name
fname lhs_in :: PTerm
lhs_in withs :: [PTerm]
withs wval_in :: PTerm
wval_in pn_in :: Maybe (Name, FC)
pn_in withblock :: [PDecl' PTerm]
withblock)
   = do Context
ctxt <- Idris Context
getContext
        -- Build the LHS as an "Infer", and pull out its type and
        -- pattern bindings
        IState
i <- Idris IState
getIState
        -- get the parameters first, to pass through to any where block
        let fn_ty :: Type
fn_ty = case Name -> Context -> [Type]
lookupTy Name
fname Context
ctxt of
                         [t :: Type
t] -> Type
t
                         _ -> String -> Type
forall a. HasCallStack => String -> a
error "Can't happen (elabClause function type)"
        let fn_is :: [PArg]
fn_is = case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
fname (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                         [t :: [PArg]
t] -> [PArg]
t
                         _ -> []
        let params :: [Name]
params = IState -> [Name] -> [PArg] -> Type -> [Name]
getParamsInType IState
i [] [PArg]
fn_is (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
fn_ty)
        let lhs :: PTerm
lhs = IState -> PTerm -> PTerm
stripLinear IState
i (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState -> PTerm -> PTerm
stripUnmatchable IState
i (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                   IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
propagateParams IState
i [Name]
params Type
fn_ty (PTerm -> [Name]
allNamesIn PTerm
lhs_in)
                    (IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in)
        Int -> String -> Idris ()
logElab 2 ("LHS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
lhs)
        (ElabResult lhs' :: Type
lhs' dlhs :: [(Name, (Int, Maybe Name, Type, [Name]))]
dlhs [] ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: Int
newGName, _) <-
            TC (ElabResult, String) -> Idris (ElabResult, String)
forall a. TC a -> Idris a
tclift (TC (ElabResult, String) -> Idris (ElabResult, String))
-> TC (ElabResult, String) -> Idris (ElabResult, String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> EState
-> Elab' EState ElabResult
-> TC (ElabResult, String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN 0 "patLHS") Type
infP EState
initEState
              (String
-> Name
-> Maybe Type
-> Elab' EState ElabResult
-> Elab' EState ElabResult
forall aux a.
String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
errAt "left hand side of with in " Name
fname Maybe Type
forall a. Maybe a
Nothing
                (FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun (FC -> Maybe FC -> FC
forall a. a -> Maybe a -> a
fromMaybe FC
NoFC (Maybe FC -> FC) -> Maybe FC -> FC
forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe FC
highestFC PTerm
lhs_in)
                      (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> [Name]
-> PTerm
-> Elab' EState ElabResult
buildTC IState
i ElabInfo
info ElabMode
ELHS FnOpts
opts Name
fname
                                  (PTerm -> [Name]
allNamesIn PTerm
lhs_in)
                                  (PTerm -> PTerm
infTerm PTerm
lhs))) )
        Context -> Idris ()
setContext Context
ctxt'
        ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
        Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
        (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }

        Context
ctxt <- Idris Context
getContext
        let lhs_tm :: Type
lhs_tm = Type -> Type
orderPats (Type -> Type
getInferTerm Type
lhs')
        let lhs_ty :: Type
lhs_ty = Type -> Type
getInferType Type
lhs'
        let ret_ty :: Type
ret_ty = Type -> Type
forall n. TT n -> TT n
getRetTy (Type -> Type
forall n. TT n -> TT n
explicitNames (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
lhs_ty))
        let static_names :: [Name]
static_names = IState -> Type -> [Name]
getStaticNames IState
i Type
lhs_tm
        Int -> String -> Idris ()
logElab 5 (Type -> String
forall a. Show a => a -> String
show Type
lhs_tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
static_names)
        (clhs_c :: Type
clhs_c, clhsty :: Type
clhsty) <- String -> FC -> (Err -> Err) -> Env -> Type -> Idris (Type, Type)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc Err -> Err
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Type
lhs_tm
        let clhs :: Type
clhs = Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
clhs_c

        Int -> String -> Idris ()
logElab 5 ("Checked " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
clhs)
        let bargs :: [(Name, Type)]
bargs = Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getPBtys (Type -> Type
forall n. TT n -> TT n
explicitNames (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
lhs_tm))
        PTerm
wval <- case PTerm
wval_in of
                     Placeholder -> Err -> Idris PTerm
forall a. Err -> Idris a
ierror (Err -> Idris PTerm) -> Err -> Idris PTerm
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Err -> Err) -> Err -> Err
forall a b. (a -> b) -> a -> b
$
                          String -> Err
forall t. String -> Err' t
Msg "No expression for the with block to inspect.\nYou need to replace the _ with an expression."
                     _ -> PTerm -> Idris PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> Idris PTerm) -> PTerm -> Idris PTerm
forall a b. (a -> b) -> a -> b
$
                            ElabInfo -> PTerm -> PTerm
rhs_trans ElabInfo
info (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                              IState -> [Name] -> PTerm -> PTerm
addImplBound IState
i (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
bargs) PTerm
wval_in
        Int -> String -> Idris ()
logElab 5 ("Checking " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
wval)
        -- Elaborate wval in this context
        ((wvalElab :: Type
wvalElab, defer :: [(Name, (Int, Maybe Name, Type, [Name]))]
defer, is :: [PDecl' PTerm]
is, ctxt' :: Context
ctxt', newDecls :: [RDeclInstructions]
newDecls, highlights :: Set (FC', OutputAnnotation)
highlights, newGName :: Int
newGName), _) <-
            TC
  ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
    Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
   String)
-> Idris
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
       Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
      String)
forall a. TC a -> Idris a
tclift (TC
   ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
     Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
    String)
 -> Idris
      ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
        Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
       String))
-> TC
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
       Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
      String)
-> Idris
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
       Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
      String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> EState
-> Elab'
     EState
     (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
      Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int)
-> TC
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
       Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
      String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN 0 "withRHS")
                        ((Type -> Binder Type) -> [(Name, Type)] -> Type -> Type
forall n. (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
bindTyArgs Type -> Binder Type
forall b. b -> Binder b
PVTy [(Name, Type)]
bargs Type
infP) EState
initEState
                        (do IState -> Type -> ElabD ()
pbinds IState
i Type
lhs_tm
                            -- proof search can use explicitly written names
                            (Name -> ElabD ()) -> [Name] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> ElabD ()
forall aux. Name -> Elab' aux ()
addPSname (PTerm -> [Name]
allNamesIn PTerm
lhs_in)
                            ElabD ()
forall aux. Elab' aux ()
setNextName
                            -- TODO: may want where here - see winfo abpve
                            (ElabResult _ d :: [(Name, (Int, Maybe Name, Type, [Name]))]
d is :: [PDecl' PTerm]
is ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: Int
newGName) <- String
-> Name
-> Maybe Type
-> Elab' EState ElabResult
-> Elab' EState ElabResult
forall aux a.
String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
errAt "with value in " Name
fname Maybe Type
forall a. Maybe a
Nothing
                              (FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> Elab' EState ElabResult
build IState
i ElabInfo
info ElabMode
ERHS FnOpts
opts Name
fname (PTerm -> PTerm
infTerm PTerm
wval)))
                            FC -> ElabD () -> ElabD ()
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ Type -> ElabD ()
forall n aux. TT n -> StateT (ElabState aux) TC ()
psolve Type
lhs_tm
                            Type
tt <- Elab' EState Type
forall aux. Elab' aux Type
get_term
                            (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
 Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int)
-> Elab'
     EState
     (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
      Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tt, [(Name, (Int, Maybe Name, Type, [Name]))]
d, [PDecl' PTerm]
is, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName))
        Context -> Idris ()
setContext Context
ctxt'
        ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
        Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
        (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }

        [(Name, (Int, Maybe Name, Type, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkDef ElabInfo
info FC
fc Name -> Err -> Err
iderr Bool
True [(Name, (Int, Maybe Name, Type, [Name]))]
defer
        let def'' :: [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def'' = ((Name, (Int, Maybe Name, Type, [Name]))
 -> (Name, (Int, Maybe Name, Type, [Name], Bool, Bool)))
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, (i :: Int
i, top :: Maybe Name
top, t :: Type
t, ns :: [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Type
t, [Name]
ns, Bool
False, Bool
True))) [(Name, (Int, Maybe Name, Type, [Name]))]
def'
        [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def''
        (PDecl' PTerm -> Idris ()) -> [PDecl' PTerm] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> FnOpts -> PDecl' PTerm -> Idris ()
elabCaseBlock ElabInfo
info FnOpts
opts) [PDecl' PTerm]
is

        let wval' :: Type
wval' = Type
wvalElab
        Int -> String -> Idris ()
logElab 5 ("Checked wval " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
wval')

        Context
ctxt <- Idris Context
getContext
        (cwval :: Type
cwval, cwvalty :: Type
cwvalty) <- String -> FC -> (Err -> Err) -> Env -> Type -> Idris (Type, Type)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc Err -> Err
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] (Type -> Type
getInferTerm Type
wval')
        let cwvaltyN :: Type
cwvaltyN = Type -> Type
forall n. TT n -> TT n
explicitNames (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
cwvalty)
        let cwvalN :: Type
cwvalN = Type -> Type
forall n. TT n -> TT n
explicitNames (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
cwval)
        Int -> String -> Idris ()
logElab 3 ("With type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
cwvalty String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nRet type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ret_ty)
        -- We're going to assume the with type is not a function shortly,
        -- so report an error if it is (you can't match on a function anyway
        -- so this doesn't lose anything)
        case Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys Type
cwvaltyN of
             [] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
             (_:_) -> Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> Err -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Type -> Err
forall t. t -> Err' t
WithFnType Type
cwvalty)

        let pvars :: [Name]
pvars = ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst (Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getPBtys Type
cwvalty)
        -- we need the unelaborated term to get the names it depends on
        -- rather than a de Bruijn index.
        let pdeps :: [Name]
pdeps = [Name] -> IState -> PTerm -> [Name]
usedNamesIn [Name]
pvars IState
i (IState -> Type -> PTerm
delab IState
i Type
cwvalty)
        let (bargs_pre :: [(Name, Type)]
bargs_pre, bargs_post :: [(Name, Type)]
bargs_post) = [Name]
-> [(Name, Type)]
-> [(Name, Type)]
-> ([(Name, Type)], [(Name, Type)])
forall a b.
Eq a =>
[a] -> [(a, b)] -> [(a, b)] -> ([(a, b)], [(a, b)])
split [Name]
pdeps [(Name, Type)]
bargs []

        let mpn :: Maybe Name
mpn = case Maybe (Name, FC)
pn_in of
                       Nothing -> Maybe Name
forall a. Maybe a
Nothing
                       Just (n :: Name
n, nfc :: FC
nfc) -> Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> [Name] -> Name
uniqueName Name
n (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
bargs))

        -- Highlight explicit proofs
        Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList [(FC -> FC'
FC' FC
fc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
n Bool
False) | (n :: Name
n, fc :: FC
fc) <- Maybe (Name, FC) -> [(Name, FC)]
forall a. Maybe a -> [a]
maybeToList Maybe (Name, FC)
pn_in]

        Int -> String -> Idris ()
logElab 10 ("With type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show (Type -> Type
forall n. TT n -> TT n
getRetTy Type
cwvaltyN) String -> String -> String
forall a. [a] -> [a] -> [a]
++
                  " depends on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
pdeps String -> String -> String
forall a. [a] -> [a] -> [a]
++ " from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
pvars)
        Int -> String -> Idris ()
logElab 10 ("Pre " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, Type)] -> String
forall a. Show a => a -> String
show [(Name, Type)]
bargs_pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nPost " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, Type)] -> String
forall a. Show a => a -> String
show [(Name, Type)]
bargs_post)
        Int
windex <- Idris Int
getName
        -- build a type declaration for the new function:
        -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
        let wargval :: Type
wargval = Type -> Type
forall n. TT n -> TT n
getRetTy Type
cwvalN
        let wargtype :: Type
wargtype = Type -> Type
forall n. TT n -> TT n
getRetTy Type
cwvaltyN
        let wargname :: Name
wargname = Int -> String -> Name
sMN Int
windex "warg"

        Int -> String -> Idris ()
logElab 5 ("Abstract over " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
wargval String -> String -> String
forall a. [a] -> [a] -> [a]
++ " in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
wargtype)
        let wtype :: Type
wtype = (Type -> Binder Type) -> [(Name, Type)] -> Type -> Type
forall n. (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
bindTyArgs ((Type -> Type -> Binder Type) -> Type -> Type -> Binder Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip (RigCount -> Maybe ImplicitInfo -> Type -> Type -> Binder Type
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing) (UExp -> Type
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] 0))) ([(Name, Type)]
bargs_pre [(Name, Type)] -> [(Name, Type)] -> [(Name, Type)]
forall a. [a] -> [a] -> [a]
++
                     (Name
wargname, Type
wargtype) (Name, Type) -> [(Name, Type)] -> [(Name, Type)]
forall a. a -> [a] -> [a]
:
                     ((Name, Type) -> (Name, Type)) -> [(Name, Type)] -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type -> Type -> (Name, Type) -> (Name, Type)
forall n a. Eq n => n -> TT n -> TT n -> (a, TT n) -> (a, TT n)
abstract Name
wargname Type
wargval Type
wargtype) [(Name, Type)]
bargs_post [(Name, Type)] -> [(Name, Type)] -> [(Name, Type)]
forall a. [a] -> [a] -> [a]
++
                     case Maybe Name
mpn of
                          Just pn :: Name
pn -> [(Name
pn, Type -> [Type] -> Type
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
eqTy Type
forall n. TT n
Erased)
                                       [Type
wargtype, Type
wargtype,
                                         NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
wargname Type
forall n. TT n
Erased, Type
wargval])]
                          Nothing -> [])
                     (Type -> Type -> Type -> Type
forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm Type
wargval (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
wargname Type
wargtype) Type
ret_ty)
        Int -> String -> Idris ()
logElab 3 ("New function type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
wtype)
        let wname :: Name
wname = SpecialName -> Name
SN (Int -> Name -> SpecialName
WithN Int
windex Name
fname)

        let imps :: [PArg]
imps = Type -> [PArg]
forall n. TT n -> [PArg]
getImps Type
wtype -- add to implicits context
        IState -> Idris ()
putIState (IState
i { idris_implicits :: Ctxt [PArg]
idris_implicits = Name -> [PArg] -> Ctxt [PArg] -> Ctxt [PArg]
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
wname [PArg]
imps (IState -> Ctxt [PArg]
idris_implicits IState
i) })
        let statics :: [Bool]
statics = [Name] -> Type -> [Bool]
getStatics [Name]
static_names Type
wtype
        Int -> String -> Idris ()
logElab 5 ("Static positions " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Bool] -> String
forall a. Show a => a -> String
show [Bool]
statics)
        IState
i <- Idris IState
getIState
        IState -> Idris ()
putIState (IState
i { idris_statics :: Ctxt [Bool]
idris_statics = Name -> [Bool] -> Ctxt [Bool] -> Ctxt [Bool]
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
wname [Bool]
statics (IState -> Ctxt [Bool]
idris_statics IState
i) })

        IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
wname)
        IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCImp Name
wname)
        IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCStatic Name
wname)

        [(Name, (Int, Maybe Name, Type, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkDef ElabInfo
info FC
fc Name -> Err -> Err
iderr Bool
True [(Name
wname, (-1, Maybe Name
forall a. Maybe a
Nothing, Type
wtype, []))]
        let def'' :: [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def'' = ((Name, (Int, Maybe Name, Type, [Name]))
 -> (Name, (Int, Maybe Name, Type, [Name], Bool, Bool)))
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, (i :: Int
i, top :: Maybe Name
top, t :: Type
t, ns :: [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Type
t, [Name]
ns, Bool
False, Bool
True))) [(Name, (Int, Maybe Name, Type, [Name]))]
def'
        [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def''

        -- in the subdecls, lhs becomes:
        --         fname  pats | wpat [rest]
        --    ==>  fname' ps   wpat [rest], match pats against toplevel for ps
        [PDecl' PTerm]
wb <- (PDecl' PTerm -> StateT IState (ExceptT Err IO) (PDecl' PTerm))
-> [PDecl' PTerm] -> StateT IState (ExceptT Err IO) [PDecl' PTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PDecl' PTerm
-> StateT IState (ExceptT Err IO) (PDecl' PTerm)
mkAuxC Maybe Name
mpn Name
wname PTerm
lhs (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
bargs_pre) (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
bargs_post))
                       [PDecl' PTerm]
withblock
        Int -> String -> Idris ()
logElab 3 ("with block " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl' PTerm] -> String
forall a. Show a => a -> String
show [PDecl' PTerm]
wb)
        Name -> FnOpts -> Idris ()
setFlags Name
wname [FnOpt
Inlinable]
        Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
AssertTotal FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
           Name -> FnOpts -> Idris ()
setFlags Name
wname [FnOpt
Inlinable, FnOpt
AssertTotal]
        IState
i <- Idris IState
getIState
        let rhstrans' :: PTerm -> PTerm
rhstrans' = IState
-> Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PTerm
-> PTerm
updateWithTerm IState
i Maybe Name
mpn Name
wname PTerm
lhs (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
bargs_pre) (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst ([(Name, Type)]
bargs_post))
                             (PTerm -> PTerm) -> (PTerm -> PTerm) -> PTerm -> PTerm
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ElabInfo -> PTerm -> PTerm
rhs_trans ElabInfo
info
        (PDecl' PTerm -> Idris ()) -> [PDecl' PTerm] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl' PTerm -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll (ElabInfo
info { rhs_trans :: PTerm -> PTerm
rhs_trans = PTerm -> PTerm
rhstrans' })) [PDecl' PTerm]
wb

        -- rhs becomes: fname' ps_pre wval ps_post Refl
        let rhs :: PTerm
rhs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
wname)
                    (((Name, Type) -> PArg) -> [(Name, Type)] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> PArg
forall t. t -> PArg' t
pexp (PTerm -> PArg) -> ((Name, Type) -> PTerm) -> (Name, Type) -> PArg
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (FC -> [FC] -> Name -> PTerm
PRef FC
fc []) (Name -> PTerm) -> ((Name, Type) -> Name) -> (Name, Type) -> PTerm
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst) [(Name, Type)]
bargs_pre [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++
                        PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
wval PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
:
                    (((Name, Type) -> PArg) -> [(Name, Type)] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> PArg
forall t. t -> PArg' t
pexp (PTerm -> PArg) -> ((Name, Type) -> PTerm) -> (Name, Type) -> PArg
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (FC -> [FC] -> Name -> PTerm
PRef FC
fc []) (Name -> PTerm) -> ((Name, Type) -> Name) -> (Name, Type) -> PTerm
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst) [(Name, Type)]
bargs_post) [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++
                    case Maybe Name
mpn of
                         Nothing -> []
                         Just _ -> [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> PTerm -> [PArg] -> PTerm
PApp FC
NoFC (FC -> [FC] -> Name -> PTerm
PRef FC
NoFC [] Name
eqCon)
                                               [ Name -> PTerm -> Bool -> PArg
forall t. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN "A") PTerm
Placeholder Bool
False
                                               , Name -> PTerm -> Bool -> PArg
forall t. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN "x") PTerm
Placeholder Bool
False
                                               ])])
        Int -> String -> Idris ()
logElab 5 ("New RHS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs)
        Context
ctxt <- Idris Context
getContext -- New context with block added
        IState
i <- Idris IState
getIState
        ((rhsElab :: Type
rhsElab, defer :: [(Name, (Int, Maybe Name, Type, [Name]))]
defer, is :: [PDecl' PTerm]
is, ctxt' :: Context
ctxt', newDecls :: [RDeclInstructions]
newDecls, highlights :: Set (FC', OutputAnnotation)
highlights, newGName :: Int
newGName), _) <-
           TC
  ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
    Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
   String)
-> Idris
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
       Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
      String)
forall a. TC a -> Idris a
tclift (TC
   ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
     Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
    String)
 -> Idris
      ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
        Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
       String))
-> TC
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
       Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
      String)
-> Idris
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
       Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
      String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> EState
-> Elab'
     EState
     (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
      Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int)
-> TC
     ((Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
       Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int),
      String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN 0 "wpatRHS") Type
clhsty EState
initEState
                    (do IState -> Type -> ElabD ()
pbinds IState
i Type
lhs_tm
                        ElabD ()
forall aux. Elab' aux ()
setNextName
                        (ElabResult _ d :: [(Name, (Int, Maybe Name, Type, [Name]))]
d is :: [PDecl' PTerm]
is ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: Int
newGName) <-
                           FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> Elab' EState ElabResult
build IState
i ElabInfo
info ElabMode
ERHS FnOpts
opts Name
fname PTerm
rhs)
                        Type -> ElabD ()
forall n aux. TT n -> StateT (ElabState aux) TC ()
psolve Type
lhs_tm
                        Type
tt <- Elab' EState Type
forall aux. Elab' aux Type
get_term
                        (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
 Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int)
-> Elab'
     EState
     (Type, [(Name, (Int, Maybe Name, Type, [Name]))], [PDecl' PTerm],
      Context, [RDeclInstructions], Set (FC', OutputAnnotation), Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tt, [(Name, (Int, Maybe Name, Type, [Name]))]
d, [PDecl' PTerm]
is, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName))
        Context -> Idris ()
setContext Context
ctxt'

        ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
        Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
        (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }

        Context
ctxt <- Idris Context
getContext
        let rhs' :: Type
rhs' = Type
rhsElab

        [(Name, (Int, Maybe Name, Type, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkDef ElabInfo
info FC
fc Name -> Err -> Err
iderr Bool
True [(Name, (Int, Maybe Name, Type, [Name]))]
defer
        let def'' :: [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def'' = ((Name, (Int, Maybe Name, Type, [Name]))
 -> (Name, (Int, Maybe Name, Type, [Name], Bool, Bool)))
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, (i :: Int
i, top :: Maybe Name
top, t :: Type
t, ns :: [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Type
t, [Name]
ns, Bool
False, Bool
True))) [(Name, (Int, Maybe Name, Type, [Name]))]
def'
        [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
def''
        (PDecl' PTerm -> Idris ()) -> [PDecl' PTerm] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> FnOpts -> PDecl' PTerm -> Idris ()
elabCaseBlock ElabInfo
info FnOpts
opts) [PDecl' PTerm]
is
        Int -> String -> Idris ()
logElab 5 ("Checked RHS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
rhs')
        (crhs :: Type
crhs, crhsty :: Type
crhsty) <- String -> FC -> (Err -> Err) -> Env -> Type -> Idris (Type, Type)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc Err -> Err
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Type
rhs'
        (Either Type (Type, Type), PTerm)
-> StateT IState (ExceptT Err IO) (Either Type (Type, Type), PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type) -> Either Type (Type, Type)
forall a b. b -> Either a b
Right (Type
clhs, Type
crhs), PTerm
lhs)
  where
    getImps :: TT n -> [PArg]
getImps (Bind n :: n
n (Pi _ _ _ _) t :: TT n
t) = PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
Placeholder PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: TT n -> [PArg]
getImps TT n
t
    getImps _ = []

    mkAuxC :: Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PDecl' PTerm
-> StateT IState (ExceptT Err IO) (PDecl' PTerm)
mkAuxC pn :: Maybe Name
pn wname :: Name
wname lhs :: PTerm
lhs ns :: [Name]
ns ns' :: [Name]
ns' (PClauses fc :: FC
fc o :: FnOpts
o n :: Name
n cs :: [PClause]
cs)
                = do [PClause]
cs' <- (PClause -> StateT IState (ExceptT Err IO) PClause)
-> [PClause] -> StateT IState (ExceptT Err IO) [PClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PClause
-> StateT IState (ExceptT Err IO) PClause
mkAux Maybe Name
pn Name
wname PTerm
lhs [Name]
ns [Name]
ns') [PClause]
cs
                     PDecl' PTerm -> StateT IState (ExceptT Err IO) (PDecl' PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (PDecl' PTerm -> StateT IState (ExceptT Err IO) (PDecl' PTerm))
-> PDecl' PTerm -> StateT IState (ExceptT Err IO) (PDecl' PTerm)
forall a b. (a -> b) -> a -> b
$ FC -> FnOpts -> Name -> [PClause] -> PDecl' PTerm
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
o Name
wname [PClause]
cs'
    mkAuxC pn :: Maybe Name
pn wname :: Name
wname lhs :: PTerm
lhs ns :: [Name]
ns ns' :: [Name]
ns' d :: PDecl' PTerm
d = PDecl' PTerm -> StateT IState (ExceptT Err IO) (PDecl' PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl' PTerm
d

    mkAux :: Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PClause
-> StateT IState (ExceptT Err IO) PClause
mkAux pn :: Maybe Name
pn wname :: Name
wname toplhs :: PTerm
toplhs ns :: [Name]
ns ns' :: [Name]
ns' (PClause fc :: FC
fc n :: Name
n tm_in :: PTerm
tm_in (w :: PTerm
w:ws :: [PTerm]
ws) rhs :: PTerm
rhs wheres :: [PDecl' PTerm]
wheres)
        = do IState
i <- Idris IState
getIState
             let tm :: PTerm
tm = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
tm_in
             Int -> String -> Idris ()
logElab 2 ("Matching " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " against " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                      PTerm -> String
showTmImpls PTerm
toplhs)
             case IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause IState
i PTerm
toplhs PTerm
tm of
                Left (a :: PTerm
a,b :: PTerm
b) -> String -> StateT IState (ExceptT Err IO) PClause
forall a. String -> Idris a
ifail (String -> StateT IState (ExceptT Err IO) PClause)
-> String -> StateT IState (ExceptT Err IO) PClause
forall a b. (a -> b) -> a -> b
$ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":with clause does not match top level"
                Right mvars :: [(Name, PTerm)]
mvars ->
                    do Int -> String -> Idris ()
logElab 3 ("Match vars : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)] -> String
forall a. Show a => a -> String
show [(Name, PTerm)]
mvars)
                       PTerm
lhs <- Name
-> Maybe Name
-> Name
-> [(Name, PTerm)]
-> [Name]
-> [Name]
-> PTerm
-> PTerm
-> Idris PTerm
forall (m :: * -> *) t.
Monad m =>
t
-> Maybe Name
-> Name
-> [(Name, PTerm)]
-> [Name]
-> [Name]
-> PTerm
-> PTerm
-> m PTerm
updateLHS Name
n Maybe Name
pn Name
wname [(Name, PTerm)]
mvars [Name]
ns [Name]
ns' (PTerm -> PTerm
fullApp PTerm
tm) PTerm
w
                       PClause -> StateT IState (ExceptT Err IO) PClause
forall (m :: * -> *) a. Monad m => a -> m a
return (PClause -> StateT IState (ExceptT Err IO) PClause)
-> PClause -> StateT IState (ExceptT Err IO) PClause
forall a b. (a -> b) -> a -> b
$ FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl' PTerm] -> PClause
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
wname PTerm
lhs [PTerm]
ws PTerm
rhs [PDecl' PTerm]
wheres
    mkAux pn :: Maybe Name
pn wname :: Name
wname toplhs :: PTerm
toplhs ns :: [Name]
ns ns' :: [Name]
ns' (PWith fc :: FC
fc n :: Name
n tm_in :: PTerm
tm_in (w :: PTerm
w:ws :: [PTerm]
ws) wval :: PTerm
wval pn' :: Maybe (Name, FC)
pn' withs :: [PDecl' PTerm]
withs)
        = do IState
i <- Idris IState
getIState
             let tm :: PTerm
tm = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
tm_in
             Int -> String -> Idris ()
logElab 2 ("Matching " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " against " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                      PTerm -> String
showTmImpls PTerm
toplhs)
             [PDecl' PTerm]
withs' <- (PDecl' PTerm -> StateT IState (ExceptT Err IO) (PDecl' PTerm))
-> [PDecl' PTerm] -> StateT IState (ExceptT Err IO) [PDecl' PTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PDecl' PTerm
-> StateT IState (ExceptT Err IO) (PDecl' PTerm)
mkAuxC Maybe Name
pn Name
wname PTerm
toplhs [Name]
ns [Name]
ns') [PDecl' PTerm]
withs
             case IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause IState
i PTerm
toplhs PTerm
tm of
                Left (a :: PTerm
a,b :: PTerm
b) -> String
-> StateT IState (ExceptT Err IO) PClause
-> StateT IState (ExceptT Err IO) PClause
forall a. String -> a -> a
trace ("matchClause: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " =/= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
b) (String -> StateT IState (ExceptT Err IO) PClause
forall a. String -> Idris a
ifail (String -> StateT IState (ExceptT Err IO) PClause)
-> String -> StateT IState (ExceptT Err IO) PClause
forall a b. (a -> b) -> a -> b
$ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ "with clause does not match top level")
                Right mvars :: [(Name, PTerm)]
mvars ->
                    do PTerm
lhs <- Name
-> Maybe Name
-> Name
-> [(Name, PTerm)]
-> [Name]
-> [Name]
-> PTerm
-> PTerm
-> Idris PTerm
forall (m :: * -> *) t.
Monad m =>
t
-> Maybe Name
-> Name
-> [(Name, PTerm)]
-> [Name]
-> [Name]
-> PTerm
-> PTerm
-> m PTerm
updateLHS Name
n Maybe Name
pn Name
wname [(Name, PTerm)]
mvars [Name]
ns [Name]
ns' (PTerm -> PTerm
fullApp PTerm
tm) PTerm
w
                       PClause -> StateT IState (ExceptT Err IO) PClause
forall (m :: * -> *) a. Monad m => a -> m a
return (PClause -> StateT IState (ExceptT Err IO) PClause)
-> PClause -> StateT IState (ExceptT Err IO) PClause
forall a b. (a -> b) -> a -> b
$ FC
-> Name
-> PTerm
-> [PTerm]
-> PTerm
-> Maybe (Name, FC)
-> [PDecl' PTerm]
-> PClause
forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc Name
wname PTerm
lhs [PTerm]
ws PTerm
wval Maybe (Name, FC)
pn' [PDecl' PTerm]
withs'
    mkAux pn :: Maybe Name
pn wname :: Name
wname toplhs :: PTerm
toplhs ns :: [Name]
ns ns' :: [Name]
ns' c :: PClause
c
        = String -> StateT IState (ExceptT Err IO) PClause
forall a. String -> Idris a
ifail (String -> StateT IState (ExceptT Err IO) PClause)
-> String -> StateT IState (ExceptT Err IO) PClause
forall a b. (a -> b) -> a -> b
$ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":badly formed with clause"

    -- ns, arguments which don't depend on the with argument
    -- ns', arguments which do
    updateLHS :: t
-> Maybe Name
-> Name
-> [(Name, PTerm)]
-> [Name]
-> [Name]
-> PTerm
-> PTerm
-> m PTerm
updateLHS n :: t
n pn :: Maybe Name
pn wname :: Name
wname mvars :: [(Name, PTerm)]
mvars ns_in :: [Name]
ns_in ns_in' :: [Name]
ns_in' (PApp fc :: FC
fc (PRef fc' :: FC
fc' hls' :: [FC]
hls' n' :: Name
n') args :: [PArg]
args) w :: PTerm
w
        = let ns :: [PTerm]
ns = (Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> FC -> Name -> PTerm
forall (t :: * -> *). Foldable t => t Name -> FC -> Name -> PTerm
keepMvar (((Name, PTerm) -> Name) -> [(Name, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, PTerm)]
mvars) FC
fc') [Name]
ns_in
              ns' :: [PTerm]
ns' = (Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> FC -> Name -> PTerm
forall (t :: * -> *). Foldable t => t Name -> FC -> Name -> PTerm
keepMvar (((Name, PTerm) -> Name) -> [(Name, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, PTerm)]
mvars) FC
fc') [Name]
ns_in' in
              PTerm -> m PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> m PTerm) -> PTerm -> m PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, PTerm)] -> PTerm -> PTerm
substMatches [(Name, PTerm)]
mvars (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                  FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc' [] Name
wname)
                      ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall t. t -> PArg' t
pexp [PTerm]
ns [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
w PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall t. t -> PArg' t
pexp [PTerm]
ns') [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++
                        case Maybe Name
pn of
                             Nothing -> []
                             Just pnm :: Name
pnm -> [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pnm)])
    updateLHS n :: t
n pn :: Maybe Name
pn wname :: Name
wname mvars :: [(Name, PTerm)]
mvars ns_in :: [Name]
ns_in ns_in' :: [Name]
ns_in' tm :: PTerm
tm w :: PTerm
w
        = t
-> Maybe Name
-> Name
-> [(Name, PTerm)]
-> [Name]
-> [Name]
-> PTerm
-> PTerm
-> m PTerm
updateLHS t
n Maybe Name
pn Name
wname [(Name, PTerm)]
mvars [Name]
ns_in [Name]
ns_in' (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
tm []) PTerm
w

    -- Only keep a var as a pattern variable in the with block if it's
    -- matched in the top level pattern
    keepMvar :: t Name -> FC -> Name -> PTerm
keepMvar mvs :: t Name
mvs fc :: FC
fc v :: Name
v | Name
v Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
mvs = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
v
                      | Bool
otherwise = PTerm
Placeholder

    updateWithTerm :: IState -> Maybe Name -> Name -> PTerm -> [Name] -> [Name] -> PTerm -> PTerm
    updateWithTerm :: IState
-> Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PTerm
-> PTerm
updateWithTerm ist :: IState
ist pn :: Maybe Name
pn wname :: Name
wname toplhs :: PTerm
toplhs ns_in :: [Name]
ns_in ns_in' :: [Name]
ns_in' tm :: PTerm
tm
          = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
updateApp PTerm
tm
       where
         currentFn :: Name -> PTerm -> PTerm
currentFn fname :: Name
fname (PAlternative _ _ as :: [PTerm]
as)
              | Just tm :: PTerm
tm <- [PTerm] -> Maybe PTerm
getApp [PTerm]
as = PTerm
tm
            where getApp :: [PTerm] -> Maybe PTerm
getApp (tm :: PTerm
tm@(PApp _ (PRef _ _ f :: Name
f) _) : as :: [PTerm]
as)
                      | Name
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
fname = PTerm -> Maybe PTerm
forall a. a -> Maybe a
Just PTerm
tm
                  getApp (_ : as :: [PTerm]
as) = [PTerm] -> Maybe PTerm
getApp [PTerm]
as
                  getApp [] = Maybe PTerm
forall a. Maybe a
Nothing
         currentFn _ tm :: PTerm
tm = PTerm
tm

         updateApp :: PTerm -> PTerm
updateApp wtm :: PTerm
wtm@(PWithApp fcw :: FC
fcw tm_in :: PTerm
tm_in warg :: PTerm
warg) =
           let tm :: PTerm
tm = Name -> PTerm -> PTerm
currentFn Name
fname PTerm
tm_in in
              case IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause IState
ist PTerm
toplhs PTerm
tm of
                Left _ -> Err -> PTerm
PElabError (String -> Err
forall t. String -> Err' t
Msg (FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":with application does not match top level "))
                Right mvars :: [(Name, PTerm)]
mvars ->
                   let ns :: [PTerm]
ns = (Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> FC -> Name -> PTerm
forall (t :: * -> *). Foldable t => t Name -> FC -> Name -> PTerm
keepMvar (((Name, PTerm) -> Name) -> [(Name, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, PTerm)]
mvars) FC
fcw) [Name]
ns_in
                       ns' :: [PTerm]
ns' = (Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> FC -> Name -> PTerm
forall (t :: * -> *). Foldable t => t Name -> FC -> Name -> PTerm
keepMvar (((Name, PTerm) -> Name) -> [(Name, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, PTerm)]
mvars) FC
fcw) [Name]
ns_in'
                       wty :: Maybe Type
wty = Name -> Context -> Maybe Type
lookupTyExact Name
wname (IState -> Context
tt_ctxt IState
ist)
                       res :: PTerm
res = [(Name, PTerm)] -> PTerm -> PTerm
substMatches [(Name, PTerm)]
mvars (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                          FC -> PTerm -> [PArg] -> PTerm
PApp FC
fcw (FC -> [FC] -> Name -> PTerm
PRef FC
fcw [] Name
wname)
                            ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall t. t -> PArg' t
pexp [PTerm]
ns [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
warg PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall t. t -> PArg' t
pexp [PTerm]
ns') [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++
                                case Maybe Name
pn of
                                     Nothing -> []
                                     Just pnm :: Name
pnm -> [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pnm)]) in
                          case Maybe Type
wty of
                               Nothing -> PTerm
res -- can't happen!
                               Just ty :: Type
ty -> Type -> PTerm -> PTerm
addResolves Type
ty PTerm
res
         updateApp tm :: PTerm
tm = PTerm
tm

         addResolves :: Type -> PTerm -> PTerm
addResolves ty :: Type
ty (PApp fc :: FC
fc f :: PTerm
f args :: [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f (FC -> Type -> [PArg] -> [PArg]
addResolvesArgs FC
fc Type
ty [PArg]
args)
         addResolves ty :: Type
ty tm :: PTerm
tm = PTerm
tm

         -- if an argument's type is an interface, and is otherwise to
         -- be inferred, then resolve it with implementation search
         -- This is something of a hack, because matching on the top level
         -- application won't find this information for us
         addResolvesArgs :: FC -> Term -> [PArg] -> [PArg]
         addResolvesArgs :: FC -> Type -> [PArg] -> [PArg]
addResolvesArgs fc :: FC
fc (Bind n :: Name
n (Pi _ _ ty :: Type
ty _) sc :: Type
sc) (a :: PArg
a : args :: [PArg]
args)
             | (P _ cn :: Name
cn _, _) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty,
               PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
a PTerm -> PTerm -> Bool
forall a. Eq a => a -> a -> Bool
== PTerm
Placeholder
                 = case Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
cn (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
                        Just _ -> PArg
a { getTm :: PTerm
getTm = FC -> PTerm
PResolveTC FC
fc } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: FC -> Type -> [PArg] -> [PArg]
addResolvesArgs FC
fc Type
sc [PArg]
args
                        Nothing -> PArg
a PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: FC -> Type -> [PArg] -> [PArg]
addResolvesArgs FC
fc Type
sc [PArg]
args
         addResolvesArgs fc :: FC
fc (Bind n :: Name
n (Pi _ _ ty :: Type
ty _) sc :: Type
sc) (a :: PArg
a : args :: [PArg]
args)
                 = PArg
a PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: FC -> Type -> [PArg] -> [PArg]
addResolvesArgs FC
fc Type
sc [PArg]
args
         addResolvesArgs fc :: FC
fc _ args :: [PArg]
args = [PArg]
args

    fullApp :: PTerm -> PTerm
fullApp (PApp _ (PApp fc :: FC
fc f :: PTerm
f args :: [PArg]
args) xs :: [PArg]
xs) = PTerm -> PTerm
fullApp (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f ([PArg]
args [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ [PArg]
xs))
    fullApp x :: PTerm
x = PTerm
x

    split :: [a] -> [(a, b)] -> [(a, b)] -> ([(a, b)], [(a, b)])
split [] rest :: [(a, b)]
rest pre :: [(a, b)]
pre = ([(a, b)] -> [(a, b)]
forall a. [a] -> [a]
reverse [(a, b)]
pre, [(a, b)]
rest)
    split deps :: [a]
deps ((n :: a
n, ty :: b
ty) : rest :: [(a, b)]
rest) pre :: [(a, b)]
pre
          | a
n a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
deps = [a] -> [(a, b)] -> [(a, b)] -> ([(a, b)], [(a, b)])
split ([a]
deps [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a
n]) [(a, b)]
rest ((a
n, b
ty) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
pre)
          | Bool
otherwise = [a] -> [(a, b)] -> [(a, b)] -> ([(a, b)], [(a, b)])
split [a]
deps [(a, b)]
rest ((a
n, b
ty) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
pre)
    split deps :: [a]
deps [] pre :: [(a, b)]
pre = ([(a, b)] -> [(a, b)]
forall a. [a] -> [a]
reverse [(a, b)]
pre, [])

    abstract :: n -> TT n -> TT n -> (a, TT n) -> (a, TT n)
abstract wn :: n
wn wv :: TT n
wv wty :: TT n
wty (n :: a
n, argty :: TT n
argty) = (a
n, TT n -> TT n -> TT n -> TT n
forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm TT n
wv (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
wn TT n
wty) TT n
argty)

-- | Apply a transformation to all RHSes and nested RHSs
mapRHS :: (PTerm -> PTerm) -> PClause -> PClause
mapRHS :: (PTerm -> PTerm) -> PClause -> PClause
mapRHS f :: PTerm -> PTerm
f (PClause fc :: FC
fc n :: Name
n lhs :: PTerm
lhs args :: [PTerm]
args rhs :: PTerm
rhs ws :: [PDecl' PTerm]
ws)
    = FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl' PTerm] -> PClause
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n PTerm
lhs [PTerm]
args (PTerm -> PTerm
f PTerm
rhs) ((PDecl' PTerm -> PDecl' PTerm) -> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PDecl' PTerm -> PDecl' PTerm
mapRHSdecl PTerm -> PTerm
f) [PDecl' PTerm]
ws)
mapRHS f :: PTerm -> PTerm
f (PWith fc :: FC
fc n :: Name
n lhs :: PTerm
lhs args :: [PTerm]
args warg :: PTerm
warg prf :: Maybe (Name, FC)
prf ws :: [PDecl' PTerm]
ws)
    = FC
-> Name
-> PTerm
-> [PTerm]
-> PTerm
-> Maybe (Name, FC)
-> [PDecl' PTerm]
-> PClause
forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc Name
n PTerm
lhs [PTerm]
args (PTerm -> PTerm
f PTerm
warg) Maybe (Name, FC)
prf ((PDecl' PTerm -> PDecl' PTerm) -> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PDecl' PTerm -> PDecl' PTerm
mapRHSdecl PTerm -> PTerm
f) [PDecl' PTerm]
ws)
mapRHS f :: PTerm -> PTerm
f (PClauseR fc :: FC
fc args :: [PTerm]
args rhs :: PTerm
rhs ws :: [PDecl' PTerm]
ws)
    = FC -> [PTerm] -> PTerm -> [PDecl' PTerm] -> PClause
forall t. FC -> [t] -> t -> [PDecl' t] -> PClause' t
PClauseR FC
fc [PTerm]
args (PTerm -> PTerm
f PTerm
rhs) ((PDecl' PTerm -> PDecl' PTerm) -> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PDecl' PTerm -> PDecl' PTerm
mapRHSdecl PTerm -> PTerm
f) [PDecl' PTerm]
ws)
mapRHS f :: PTerm -> PTerm
f (PWithR fc :: FC
fc args :: [PTerm]
args warg :: PTerm
warg prf :: Maybe (Name, FC)
prf ws :: [PDecl' PTerm]
ws)
    = FC
-> [PTerm]
-> PTerm
-> Maybe (Name, FC)
-> [PDecl' PTerm]
-> PClause
forall t.
FC -> [t] -> t -> Maybe (Name, FC) -> [PDecl' t] -> PClause' t
PWithR FC
fc [PTerm]
args (PTerm -> PTerm
f PTerm
warg) Maybe (Name, FC)
prf ((PDecl' PTerm -> PDecl' PTerm) -> [PDecl' PTerm] -> [PDecl' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PDecl' PTerm -> PDecl' PTerm
mapRHSdecl PTerm -> PTerm
f) [PDecl' PTerm]
ws)

mapRHSdecl :: (PTerm -> PTerm) -> PDecl -> PDecl
mapRHSdecl :: (PTerm -> PTerm) -> PDecl' PTerm -> PDecl' PTerm
mapRHSdecl f :: PTerm -> PTerm
f (PClauses fc :: FC
fc opt :: FnOpts
opt n :: Name
n cs :: [PClause]
cs)
    = FC -> FnOpts -> Name -> [PClause] -> PDecl' PTerm
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
opt Name
n ((PClause -> PClause) -> [PClause] -> [PClause]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PClause -> PClause
mapRHS PTerm -> PTerm
f) [PClause]
cs)
mapRHSdecl f :: PTerm -> PTerm
f t :: PDecl' PTerm
t = PDecl' PTerm
t