{-|
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 ElabInfo
info' FC
fc FnOpts
opts Name
n_in [PClause]
cs =
      do let n :: Name
n    = ElabInfo -> Name -> Name
liftname ElabInfo
info Name
n_in
             info :: ElabInfo
info = ElabInfo
info' { elabFC = Just fc }
         ctxt <- Idris Context
getContext
         ist  <- getIState
         optimise <- getOptimise
         let petrans = Optimisation
PETransform Optimisation -> [Optimisation] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Optimisation]
optimise
         inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)

         -- Check n actually exists, with no definition yet
         let tys = Name -> Context -> [Term]
lookupTy Name
n Context
ctxt
         let reflect = FnOpt
Reflection FnOpt -> FnOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts
         when (reflect && FCReflection `notElem` idris_language_extensions ist) $
           ierror $ At fc (Msg "You must turn on the FirstClassReflection extension to use %reflection")
         checkUndefined n ctxt
         unless (length tys > 1) $ do
           fty <- case tys of
              [] -> -- TODO: turn into a CAF if there's no arguments
                    -- question: CAFs in where blocks?
                    TC Term -> StateT IState (ExceptT Err IO) Term
forall a. TC a -> Idris a
tclift (TC Term -> StateT IState (ExceptT Err IO) Term)
-> TC Term -> StateT IState (ExceptT Err IO) Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Err -> TC Term) -> Err -> TC Term
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)
              [Term
ty] -> Term -> StateT IState (ExceptT Err IO) Term
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
ty
           let atys_in = ((Name, Term) -> Term) -> [(Name, Term)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Term
forall a b. (a, b) -> b
snd (Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
fty))
           let atys = (Term -> (Term, Bool)) -> [Term] -> [(Term, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\Term
x -> (Term
x, Term -> Context -> Bool
isCanonical Term
x Context
ctxt)) [Term]
atys_in
           cs_elab <- mapM (elabClause info opts)
                           (zip [0..] cs)
           ctxt <- getContext
           -- pats_raw is the basic type checked version, no PE or forcing
           let optinfo = IState -> Ctxt OptInfo
idris_optimisation IState
ist
           let (pats_in, cs_full) = unzip cs_elab
           let pats_raw = (Either Term (Term, Term) -> Either Term (Term, Term))
-> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (Context -> Either Term (Term, Term) -> Either Term (Term, Term)
forall {a} {b}. Context -> Either a (Term, b) -> Either a (Term, b)
simple_lhs Context
ctxt) [Either Term (Term, Term)]
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 Term (Term, Term) -> Either Term (Term, Term))
-> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (Ctxt OptInfo
-> Either Term (Term, Term) -> Either Term (Term, Term)
forall {a} {b}.
Ctxt OptInfo -> Either a (Term, b) -> Either a (Term, b)
force_lhs Ctxt OptInfo
optinfo) [Either Term (Term, Term)]
pats_raw

           logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw
           logElab 5 $ "Forced patterns:\n" ++ show pats_forced

           solveDeferred fc n

           -- just ensure that the structure exists
           fmodifyState (ist_optimisation n) id
           addIBC (IBCOpt n)

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

           -- If the definition is specialisable, this reduces the
           -- RHS
           pe_tm <- doPartialEval ist tpats

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

           let 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
           newrules <- if petrans
                          then mapM (\ Either Term (Term, Term)
e -> case Either Term (Term, Term)
e of
                                            Left Term
_ -> [(Term, Term)] -> StateT IState (ExceptT Err IO) [(Term, Term)]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
                                            Right (Term
l, Term
r) -> ElabInfo
-> FC
-> Name
-> Term
-> StateT IState (ExceptT Err IO) [(Term, Term)]
elabPE ElabInfo
info FC
fc Name
n Term
r) pats_pe
                          else 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
           ist <- getIState
           let pats_transformed = if Bool
petrans
                                     then IState -> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
transformPats IState
ist [Either Term (Term, Term)]
pats_pe
                                     else [Either Term (Term, Term)]
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, Term)], Term, Term) -> ([Name], Term, Term))
-> [([(Name, Term)], Term, Term)] -> [([Name], Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\([(Name, Term)]
ns, Term
lhs, Term
rhs) -> (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
ns, Term
lhs, Term
rhs)) ([([(Name, Term)], Term, Term)] -> [([Name], Term, Term)])
-> [([(Name, Term)], Term, Term)] -> [([Name], Term, Term)]
forall a b. (a -> b) -> a -> b
$
                          (Either Term (Term, Term) -> ([(Name, Term)], Term, Term))
-> [Either Term (Term, Term)] -> [([(Name, Term)], Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map Either Term (Term, Term) -> ([(Name, Term)], Term, Term)
forall {n} {n}.
Either (TT n) (TT n, TT n) -> ([(n, TT n)], TT n, TT n)
debind [Either Term (Term, Term)]
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 = (Either Term (Term, Term) -> ([(Name, Term)], Term, Term))
-> [Either Term (Term, Term)] -> [([(Name, Term)], Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map Either Term (Term, Term) -> ([(Name, Term)], Term, Term)
forall {n} {n}.
Either (TT n) (TT n, TT n) -> ([(n, TT n)], TT n, TT n)
debind [Either Term (Term, Term)]
pats_transformed

           logElab 5 $ "Initial typechecked patterns:\n" ++ show pats_raw
           logElab 5 $ "Initial typechecked pattern def:\n" ++ show 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.

           ist <- getIState
           numArgs <- tclift $ sameLength pdef

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

           erInfo <- getErasureInfo <$> getIState
           tree@(CaseDef scargs sc _) <- tclift $
                 simpleCase tcase (UnmatchedCase "Error") reflect CompileTime fc inacc atys pdef erInfo
           cov <- coverage
           pmissing <-
                   if cov && not (hasDefault pats_raw)
                      then do -- Generate clauses from the given possible cases
                              missing <- genClauses fc n
                                                 (map (\ ([Name]
ns,Term
tm,Term
_) -> ([Name]
ns, Term
tm)) pdef)
                                                 cs_full
                              -- missing <- genMissing n scargs sc
                              missing' <- checkPossibles info fc True n missing
                              -- Filter out the ones which match one of the
                              -- given cases (including impossible ones)
                              logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++
                                          showSep "\n" (map showTmImpls missing') ++
                                         "\nAgainst: " ++
                                          showSep "\n" (map (\Term
t -> PTerm -> String
showTmImpls (IState -> Term -> PTerm
delab IState
ist Term
t)) (map getLHS 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.
                              return missing' -- (filter (noMatch ist clhs) missing')
                      else return []
           let pcover = [PTerm] -> Bool
forall a. [a] -> 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
           pdef_in' <- applyOpts $ map (\([(Name, Term)]
ns, Term
lhs, Term
rhs) -> (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
ns, Term
lhs, Term
rhs)) pdef_pe
           ctxt <- getContext
           let pdef' = (([Name], Term, Term) -> ([Name], Term, Term))
-> [([Name], Term, Term)] -> [([Name], Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (Context -> ([Name], Term, Term) -> ([Name], Term, Term)
forall {b}. Context -> ([Name], b, Term) -> ([Name], b, Term)
simple_rt Context
ctxt) [([Name], Term, Term)]
pdef_in'

           logElab 5 $ "After data structure transformations:\n" ++ show pdef'

           ist <- getIState
           let tot | Bool
pcover = Totality
Unchecked -- finish later
                   | FnOpt
AssertTotal FnOpt -> FnOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts = [Int] -> Totality
Total []
                   | FnOpt
PEGenerated FnOpt -> FnOpts -> Bool
forall a. Eq a => a -> [a] -> 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 tree of
               CaseDef [Name]
_ SC
_ [] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               CaseDef [Name]
_ SC
_ [Term]
xs -> (Term -> Idris ()) -> [Term] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Term
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 String
"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 -> Term -> PTerm
delab IState
ist Term
x))
                   ) [Term]
xs
           let knowncovering = (Bool
pcover Bool -> Bool -> Bool
&& Bool
cov) Bool -> Bool -> Bool
|| FnOpt
AssertTotal FnOpt -> FnOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts
           let 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 -> 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
":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]
++
                                       String
" ***"

           tree' <- tclift $ simpleCase tcase defaultcase reflect
                                        RunTime fc inacc atys pdef' erInfo
           logElab 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree
           logElab 3 $ "Optimised: " ++ show tree'
           ctxt <- getContext
           ist <- getIState
           putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)
                                                (idris_patdefs ist) })
           let caseInfo = Bool -> Bool -> Bool -> CaseInfo
CaseInfo (FnOpts -> Bool
inlinable FnOpts
opts) (FnOpts -> Bool
inlinable FnOpts
opts) (FnOpts -> Bool
dictionary FnOpts
opts)

           case lookupTyExact n ctxt of
               Just Term
ty ->
                   do ctxt' <- do ctxt <- Idris Context
getContext
                                  tclift $
                                    addCasedef n erInfo caseInfo
                                                   tcase defaultcase
                                                   reflect
                                                   (AssertTotal `elem` opts)
                                                   atys
                                                   inacc
                                                   pats_forced
                                                   pdef
                                                   pdef' ty
                                                   ctxt
                      setContext ctxt'
                      addIBC (IBCDef n)
                      addDefinedName n
                      setTotality n tot
                      when (not reflect && PEGenerated `notElem` opts) $
                                           do totcheck (fc, n)
                                              defer_totcheck (fc, n)
                      when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
                      i <- getIState
                      ctxt <- getContext
                      case lookupDef n ctxt of
                          (CaseOp CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
cd : [Def]
_) ->
                            let ([Name]
scargs, 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 Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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
                                 nvis <- Name -> Idris (Maybe Accessibility)
getFromHideList Name
n
                                 case nvis of
                                      Just Accessibility
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
                                      Maybe Accessibility
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                 addCalls n calls
                                 let rig = if Term -> Bool
linearArg (Context -> Env -> Term -> Term
whnfArgs Context
ctxt [] Term
ty)
                                              then RigCount
Rig1
                                              else RigCount
RigW
                                 updateContext (setRigCount n (minRig ctxt rig calls))
                                 addIBC (IBCCG n)
                          [Def]
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                      return ()
  --                         addIBC (IBCTotal n tot)
               Maybe Term
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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'
           when (CoveringFn `elem` opts) $ checkAllCovering fc [] n 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)
           checkIfGuarded n
           -- If this has %static arguments, cache the names of functions
           -- it calls for partial evaluation later
           ist <- getIState
           let 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 [Bool]
ns -> [Bool]
ns
                              Maybe [Bool]
Nothing -> []
           when (or statics) $ do getAllNames n
                                  return ()

  where
    checkUndefined :: Name -> Context -> Idris ()
checkUndefined Name
n Context
ctxt = case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
                                 [] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                 [TyDecl NameType
_ Term
_] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                 [Def]
_ -> 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 (TT n
x, TT n
y)) = let ([(n, TT n)]
vs, 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
                                ([(n, TT n)]
_, 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 TT n
x)       = let ([(n, TT n)]
vs, 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 [(n, TT n)]
acc (Bind n
n (PVar RigCount
rig TT n
t) 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 [(n, TT n)]
acc TT n
x = ([(n, TT n)]
acc, TT n
x)


    getPVs :: TT a -> ([a], TT a)
getPVs (Bind a
x (PVar RigCount
rig TT a
_) TT a
tm) = let ([a]
vs, 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 TT a
tm = ([], TT a
tm)

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

    hasDefault :: [Either a (TT a, b)] -> Bool
hasDefault [Either a (TT a, b)]
cs | (Right (TT a
lhs, b
rhs) : [Either a (TT a, b)]
_) <- [Either a (TT a, b)] -> [Either a (TT a, b)]
forall a. [a] -> [a]
reverse [Either a (TT a, b)]
cs
                  , ([a]
pvs, 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)
                  , (TT a
f, [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 [Either a (TT a, b)]
_ = Bool
False

    getLHS :: (a, b, c) -> b
getLHS (a
_, b
l, c
_) = 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 (Term, b) -> Either a (Term, b)
simple_lhs Context
ctxt (Right (Term
x, b
y))
        = (Term, b) -> Either a (Term, b)
forall a b. b -> Either a b
Right (Context -> Env -> Term -> Term
Idris.Core.Evaluate.simplify Context
ctxt [] Term
x, b
y)
    simple_lhs Context
ctxt Either a (Term, b)
t = Either a (Term, b)
t

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

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

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

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

    -- Partially evaluate, if the definition is marked as specialisable
    doPartialEval :: IState
-> [Either Term (Term, Term)]
-> StateT IState (ExceptT Err IO) [Either Term (Term, Term)]
doPartialEval IState
ist [Either Term (Term, Term)]
pats =
           case FnOpts -> Maybe [(Name, Maybe Int)]
specNames FnOpts
opts of
                Maybe [(Name, Maybe Int)]
Nothing -> [Either Term (Term, Term)]
-> StateT IState (ExceptT Err IO) [Either Term (Term, Term)]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Either Term (Term, Term)]
pats
                Just [(Name, Maybe Int)]
ns -> case Context
-> [(Name, Maybe Int)]
-> [Either Term (Term, Term)]
-> Maybe [Either Term (Term, Term)]
partial_eval (IState -> Context
tt_ctxt IState
ist) [(Name, Maybe Int)]
ns [Either Term (Term, Term)]
pats of
                                Just [Either Term (Term, Term)]
t -> [Either Term (Term, Term)]
-> StateT IState (ExceptT Err IO) [Either Term (Term, Term)]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Either Term (Term, Term)]
t
                                Maybe [Either Term (Term, Term)]
Nothing -> Err -> StateT IState (ExceptT Err IO) [Either Term (Term, Term)]
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 String
"No specialisation achieved"))

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

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


-- | 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
-> Term
-> StateT IState (ExceptT Err IO) [(Term, Term)]
elabPE ElabInfo
info FC
fc Name
caller Term
r | ElabInfo -> Int
pe_depth ElabInfo
info Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5 = [(Term, Term)] -> StateT IState (ExceptT Err IO) [(Term, Term)]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
elabPE ElabInfo
info FC
fc Name
caller Term
r =
  do ist <- Idris IState
getIState
     let sa = ((Name, [(PEArgType, Term)]) -> Bool)
-> [(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name, [(PEArgType, Term)])
ap -> (Name, [(PEArgType, Term)]) -> Name
forall a b. (a, b) -> a
fst (Name, [(PEArgType, Term)])
ap Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
caller) ([(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])])
-> [(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])]
forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> Term -> [(Name, [(PEArgType, Term)])]
getSpecApps IState
ist [] Term
r
     rules <- mapM mkSpecialised sa
     return $ concat 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, Term)])
-> StateT IState (ExceptT Err IO) [(Term, Term)]
mkSpecialised (Name, [(PEArgType, Term)])
specapp_in = do
        ist <- Idris IState
getIState
        ctxt <- getContext
        (specTy, specapp) <- getSpecTy ist specapp_in
        let (n, newnm, specdecl) = getSpecClause ist specapp specTy
        let lhs = PEDecl -> PTerm
pe_app PEDecl
specdecl
        let rhs = PEDecl -> PTerm
pe_def PEDecl
specdecl
        let undef = case Name -> Context -> Maybe Def
lookupDefExact Name
newnm Context
ctxt of
                         Maybe Def
Nothing -> Bool
True
                         Maybe Def
_ -> Bool
False
        logElab 5 $ show (newnm, undef, map (concreteArg ist) (snd specapp))
        idrisCatch
          (if (undef && all (concreteArg ist) (snd specapp)) then do
                cgns <- getAllNames 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 -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (\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 = case Name -> Context -> [Totality]
lookupTotal Name
n Context
ctxt of
                                  [Total [Int]
_] -> Int
65536
                                  [Totality
Productive] -> Int
16
                                  [Totality]
_ -> Int
1
                let specnames = ((PEArgType, Term) -> Maybe (Name, Maybe Int))
-> [(PEArgType, Term)] -> [(Name, Maybe Int)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Bool -> (PEArgType, Term) -> Maybe (Name, Maybe Int)
forall {a} {n}.
Num a =>
Bool -> (PEArgType, TT n) -> Maybe (n, Maybe a)
specName (PEDecl -> Bool
pe_simple PEDecl
specdecl))
                                         ((Name, [(PEArgType, Term)]) -> [(PEArgType, Term)]
forall a b. (a, b) -> b
snd (Name, [(PEArgType, Term)])
specapp)
                descs <- mapM getStaticsFrom (map fst specnames)

                let 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 (\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)]
                logElab 3 $ "Specialising application: " ++ show specapp
                              ++ "\n in \n" ++ show caller ++
                              "\n with \n" ++ show opts
                              ++ "\nCalling: " ++ show cgns
                logElab 3 $ "New name: " ++ show newnm
                logElab 3 $ "PE definition type : " ++ (show specTy)
                            ++ "\n" ++ show opts
                logElab 2 $ "PE definition " ++ show newnm ++ ":\n" ++
                             showSep "\n"
                                (map (\ (PTerm
lhs, PTerm
rhs) ->
                                  (PTerm -> String
showTmImpls PTerm
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                   PTerm -> String
showTmImpls PTerm
rhs)) (pe_clauses specdecl))

                logElab 5 $ show n ++ " transformation rule: " ++
                           showTmImpls rhs ++ " ==> " ++ showTmImpls lhs

                elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy
                let def = ((PTerm, PTerm) -> PClause) -> [(PTerm, PTerm)] -> [PClause]
forall a b. (a -> b) -> [a] -> [b]
map (\(PTerm
lhs, 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)
                trans <- elabTransform info fc False rhs lhs
                elabClauses (info {pe_depth = pe_depth info + 1}) fc
                            (PEGenerated:opts) newnm def
                return [trans]
             else 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).
          (\Err
e -> do Int -> String -> Idris ()
logElab Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Couldn't specialise: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (IState -> Err -> String
pshow IState
ist Err
e)
                    [(Term, Term)] -> StateT IState (ExceptT Err IO) [(Term, Term)]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [])

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

    specName :: Bool -> (PEArgType, TT n) -> Maybe (n, Maybe a)
specName Bool
simpl (ImplicitS Name
_, TT n
tm)
        | (P NameType
Ref n
n TT n
_, [TT n]
_) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = (n, Maybe a) -> Maybe (n, Maybe a)
forall a. a -> Maybe a
Just (n
n, a -> Maybe a
forall a. a -> Maybe a
Just (if Bool
simpl then a
1 else a
0))
    specName Bool
simpl (PEArgType
ExplicitS, TT n
tm)
        | (P NameType
Ref n
n TT n
_, [TT n]
_) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = (n, Maybe a) -> Maybe (n, Maybe a)
forall a. a -> Maybe a
Just (n
n, a -> Maybe a
forall a. a -> Maybe a
Just (if Bool
simpl then a
1 else a
0))
    specName Bool
simpl (PEArgType
ConstraintS, TT n
tm)
        | (P NameType
Ref n
n TT n
_, [TT n]
_) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = (n, Maybe a) -> Maybe (n, Maybe a)
forall a. a -> Maybe a
Just (n
n, a -> Maybe a
forall a. a -> Maybe a
Just (if Bool
simpl then a
1 else a
0))
    specName Bool
simpl (PEArgType, TT n)
_ = Maybe (n, 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 Name
n = do ns <- Name -> Idris [Name]
getAllNames Name
n
                          i <- getIState
                          let statics = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (IState -> Name -> Bool
staticFn IState
i) [Name]
ns
                          return (map (\Name
n -> (Name
n, Maybe Int
forall a. Maybe a
Nothing)) statics)

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

    notStatic :: IState -> Name -> Bool
notStatic IState
ist 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 [Bool]
s -> Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
s)
                           Maybe [Bool]
_ -> Bool
True

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

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

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

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

            qshow :: TT a -> String
qshow (Bind a
_ Binder (TT a)
_ TT a
_) = String
"fn"
            qshow (App AppStatus a
_ TT a
f 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 NameType
_ a
n TT a
_) = a -> String
forall a. Show a => a -> String
show a
n
            qshow (Constant Const
c) = Const -> String
forall a. Show a => a -> String
show Const
c
            qshow TT a
_ = String
""

            -- Simple but effective string hashing...
            -- Keep it to 32 bits for readability/debuggability
            qhash :: Word64 -> String -> String
            qhash :: Word64 -> String -> String
qhash Word64
hash [] = Word64 -> String -> String
forall a. Integral 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` Word64
0xffffffff) String
""
            qhash Word64
hash (Char
x:String
xs) = Word64 -> String -> String
qhash (Word64
hash Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
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 ElabInfo
info FC
fc Bool
tcgen Name
fname PTerm
lhs_in
   = do ctxt <- Idris Context
getContext
        i <- getIState
        let lhs = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in
        logElab 10 $ "Trying missing case: " ++ showTmImpls lhs
        -- if the LHS type checks, it is possible
        case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
                            (erun fc (buildTC i info EImpossible [] fname
                                                (allNamesIn lhs_in)
                                                (infTerm lhs))) of
            OK (ElabResult Term
lhs' [(Name, (Int, Maybe Name, Term, [Name]))]
_ [PDecl' PTerm]
_ Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName, String
_) ->
               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
$ \IState
i -> IState
i { idris_name = newGName }
                  let lhs_tm :: Term
lhs_tm = Context -> Env -> Term -> Term
normalise Context
ctxt [] (Term -> Term
orderPats (Term -> Term
getInferTerm Term
lhs'))
                  let emptyPat :: Bool
emptyPat = Context -> Ctxt TypeInfo -> Term -> Bool
hasEmptyPat Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) Term
lhs_tm
                  if Bool
emptyPat then
                     do Int -> String -> Idris ()
logElab Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Empty type in pattern "
                        Maybe PTerm -> Idris (Maybe PTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe PTerm
forall a. Maybe a
Nothing
                    else
                      case String -> Context -> Env -> Raw -> Term -> TC (Term, Term, UCs)
recheck (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt' [] (Term -> Raw
forget Term
lhs_tm) Term
lhs_tm of
                           OK (Term
tm, Term
_, UCs
_) ->
                                    do Int -> String -> Idris ()
logElab Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Valid " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
                                                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> Maybe PTerm
forall a. a -> Maybe a
Just (IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
tm Bool
True Bool
True))
                           TC (Term, Term, UCs)
err -> do Int -> String -> Idris ()
logElab Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Conversion failure"
                                     Maybe PTerm -> Idris (Maybe PTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
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 -> do Int -> String -> Idris ()
logLvl Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
"\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 IState
i Err
err Bool
True = do Int -> String -> Idris ()
logLvl Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Possibly resolvable error on " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                    IState -> Err -> String
pshow IState
i ((Term -> Term) -> Err -> Err
forall a b. (a -> b) -> Err' a -> Err' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
i) []) Err
err)
                                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs_in
                                 Maybe PTerm -> Idris (Maybe PTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
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 IState
i Err
err Bool
False = Maybe PTerm -> Idris (Maybe PTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
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 ElabInfo
info FC
fc Bool
tcgen Name
fname (PTerm
lhs : [PTerm]
rest)
   = do ok <- ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossible ElabInfo
info FC
fc Bool
tcgen Name
fname PTerm
lhs
        i <- 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 -> Bool) -> [PTerm] -> [PTerm]
forall a. (a -> Bool) -> [a] -> [a]
filter (\PTerm
x -> Bool -> Bool
not (PTerm -> PTerm -> Bool
qmatch PTerm
x PTerm
lhs)) (Int -> [PTerm] -> [PTerm]
forall a. Int -> [a] -> [a]
take Int
200 [PTerm]
rest) [PTerm] -> [PTerm] -> [PTerm]
forall a. [a] -> [a] -> [a]
++ Int -> [PTerm] -> [PTerm]
forall a. Int -> [a] -> [a]
drop Int
200 [PTerm]
rest
        restpos <- checkPossibles info fc tcgen fname rest'
        case ok of
             Maybe PTerm
Nothing -> [PTerm] -> Idris [PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [PTerm]
restpos
             Just PTerm
lhstm -> [PTerm] -> Idris [PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
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 PTerm
_ PTerm
Placeholder = Bool
True
    qmatch (PApp FC
_ PTerm
f [PArg]
args) (PApp FC
_ PTerm
f' [PArg]
args')
       | [PArg] -> Int
forall a. [a] -> 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 a. [a] -> 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 FC
_ [FC]
_ Name
n) (PRef FC
_ [FC]
_ Name
n') = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
    qmatch (PPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
r) (PPair FC
_ [FC]
_ PunInfo
_ PTerm
l' PTerm
r') = PTerm -> PTerm -> Bool
qmatch PTerm
l PTerm
l' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
qmatch PTerm
r PTerm
r'
    qmatch (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
t PTerm
r) (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
l' PTerm
t' 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 PTerm
x PTerm
y = PTerm
x PTerm -> PTerm -> Bool
forall a. Eq a => a -> a -> Bool
== PTerm
y
checkPossibles ElabInfo
_ FC
_ Bool
_ Name
_ [] = [PTerm] -> Idris [PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []

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

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

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

        -- Check if we have extra "with" patterns
        when (not $ null withs) $
            ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)
                       (Elaborating "left hand side of " fname Nothing
                        (Msg $ if isOutsideWith 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 = case Name -> Context -> [Term]
lookupTy Name
fname Context
ctxt of
                         [Term
t] -> Term
t
                         [Term]
_ -> String -> Term
forall a. HasCallStack => String -> a
error String
"Can't happen (elabClause function type)"
        let fn_is = case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
fname (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                         [[PArg]
t] -> [PArg]
t
                         [[PArg]]
_ -> []
        let norm_ty = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
fn_ty
        let params = IState -> [Name] -> [PArg] -> Term -> [Name]
getParamsInType IState
i [] [PArg]
fn_is Term
norm_ty
        let tcparams = IState -> [Name] -> [PArg] -> Term -> [Name]
getTCParamsInType IState
i [] [PArg]
fn_is Term
norm_ty

        let 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] -> Term -> [Name] -> PTerm -> PTerm
propagateParams IState
i [Name]
params Term
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)
        logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))
        logElab 5 ("LHS: " ++ show opts ++ "\n" ++ show fc ++ " " ++ showTmImpls lhs)
        logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ showTmImpls lhs_in ++
                  "\n" ++ show (fn_ty, fn_is))

        ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-
           tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
                    (do res <- errAt "left hand side of " fname Nothing
                                 (erun (fromMaybe NoFC $ highestFC lhs_in_as)
                                       (buildTC i info ELHS opts fname
                                          (allNamesIn lhs_in)
                                          (infTerm lhs)))
                        probs <- get_probs
                        inj <- get_inj
                        return (res, probs, inj))
        setContext ctxt'
        processTacticDecls info newDecls
        sendHighlighting highlights
        updateIState $ \IState
i -> IState
i { idris_name = newGName }

        when inf $ addTyInfConstraints fc (map (\(Term
x,Term
y,Bool
_,Env
_,Err
_,[FailContext]
_,FailAt
_) -> (Term
x,Term
y)) probs)

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

        logElab 3 ("Elaborated: " ++ show lhs_tm)
        logElab 3 ("Elaborated type: " ++ show lhs_ty)
        logElab 5 ("Injective: " ++ show fname ++ " " ++ show 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
        ctxt <- getContext
        (clhs_c, clhsty) <- if not inf
                               then recheckC_borrowing False (PEGenerated `notElem` opts)
                                                       [] (constraintNS info) fc id [] lhs_tm
                               else return (lhs_tm, lhs_ty)
        let clhs = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
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] -> Term -> [Name]
borrowedNames [] Term
clhs

        logElab 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

        rep <- useREPL
        when rep $ do
          addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?
        addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))

        logElab 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
        -- Elaborate where block
        ist <- getIState
        ctxt <- getContext

        windex <- getName
        let 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] -> [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 = IState -> Term -> [(Name, PTerm)]
pvars IState
ist Term
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 = Context -> Env -> Term -> [Name]
findUnique Context
ctxt [] Term
lhs_tm
        let newargs = ((Name, PTerm) -> Bool) -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n,PTerm
_) -> 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 -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
pinfo ElabInfo
info [(Name, PTerm)]
newargs [Name]
defs Int
windex) { elabFC = Just fc }
        let 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, wafter) = sepBlocks wb

        logElab 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
        mapM_ (rec_elabDecl info EAll winfo) wbefore
        -- Now build the RHS, using the type of the LHS as the goal.
        i <- getIState -- new implicits from where block
        logElab 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
        let 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)
        logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
        ctxt <- getContext -- new context with where block added
        logElab 5 "STARTING CHECK"
        ((rhsElab, defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-
           tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState
                    (do pbinds ist lhs_tm
                        -- proof search can use explicitly written names
                        mapM_ addPSname (allNamesIn lhs_in)
                        ulog <- getUnifyLog
                        traceWhen ulog ("Setting injective: " ++ show (nub (tcparams ++ inj))) $
                          mapM_ setinj (nub (tcparams ++ inj))
                        setNextName
                        (ElabResult _ _ is ctxt' newDecls highlights newGName) <-
                          errAt "right hand side of " fname (Just clhsty)
                                (erun fc (build i winfo ERHS opts fname rhs))
                        errAt "right hand side of " fname (Just clhsty)
                              (erun fc $ psolve lhs_tm)
                        tt <- get_term
                        aux <- getAux
                        let (tm, ds) = runState (collectDeferred (Just fname)
                                                     (map fst $ case_decls aux) ctxt tt) []
                        probs <- get_probs
                        hs <- get_holes
                        return (tm, ds, hs, is, probs, ctxt', newDecls, highlights, newGName))
        setContext ctxt'
        processTacticDecls info newDecls
        sendHighlighting highlights
        updateIState $ \IState
i -> IState
i { idris_name = newGName }

        when inf $ addTyInfConstraints fc (map (\(Term
x,Term
y,Bool
_,Env
_,Err
_,[FailContext]
_,FailAt
_) -> (Term
x,Term
y)) probs)

        logElab 3 "DONE CHECK"
        logElab 3 $ "---> " ++ show rhsElab
        ctxt <- getContext

        let rhs' = Term
rhsElab

        when (not (null defer)) $ logElab 2 $ "DEFERRED " ++
                    show (map (\ (Name
n, (Int
_,Maybe Name
_,Term
t,[Name]
_)) -> (Name
n, Term
t)) defer)

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

        mapM_ (\(Name
n, (Int, Maybe Name, Term, [Name], Bool, Bool)
_) -> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)) def''

        when (not (null def')) $ do
           mapM_ defer_totcheck (map (\(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))
x -> (FC
fc, (Name, (Int, Maybe Name, Term, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (Name, (Int, Maybe Name, Term, [Name], Bool, Bool))
x)) def'')

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

        mapM_ (rec_elabDecl info EAll winfo) wafter
        mapM_ (elabCaseBlock winfo opts) is

        ctxt <- getContext
        logElab 5 "Rechecking"
        logElab 6 $ " ==> " ++ show (forget rhs')

        (crhs, 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 (null holes || null def') && not inf
                   then recheckC_borrowing True (PEGenerated `notElem` opts)
                                       borrowed (constraintNS info) fc id [] rhs'
                   else return (rhs', clhsty)

        logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ "   against   " ++ showEnvDbg [] clhsty

        -- If there's holes, make sure this definition is frozen
        when (not (null holes)) $ do
           logElab 5 $ "Making " ++ show fname ++ " frozen due to " ++ show holes
           setAccessibility fname Frozen

        ctxt <- getContext
        let constv = Context -> Int
next_tvar Context
ctxt
        tit <- typeInType
        case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of
            OK (()
_, 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_ (\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 Int
6 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
forall a. Show a => a -> String
show (Term
clhsty, Term
crhsty)
                             () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Error Err
e -> Err -> Idris ()
forall a. Err -> Idris a
ierror (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Bool
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> Err
-> [(Name, Term)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (Term
clhsty, Maybe Provenance
forall a. Maybe a
Nothing) (Term
crhsty, Maybe Provenance
forall a. Maybe a
Nothing) Err
e [] Int
0))
        i <- getIState
        checkInferred fc (delab' i crhs True True) 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, _) = unApply (getRetTy crhsty)
        rev <- case ret_fam of
                    P NameType
_ Name
rfamn Term
_ ->
                        case Name -> Ctxt TypeInfo -> [TypeInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
rfamn (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
                             [TI [Name]
_ Bool
_ DataOpts
dopts [Int]
_ [Name]
_ Bool
_] ->
                                 Bool -> Idris Bool
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DataOpt
DataErrRev DataOpt -> DataOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` DataOpts
dopts Bool -> Bool -> Bool
&&
                                         Term -> Int
forall a. Sized a => a -> Int
size Term
clhs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Term -> Int
forall a. Sized a => a -> Int
size Term
crhs)
                             [TypeInfo]
_ -> Bool -> Idris Bool
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    Term
_ -> Bool -> Idris Bool
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

        when (rev || ErrorReverse `elem` opts) $ do
           addIBC (IBCErrRev (crhs, clhs))
           addErrRev (crhs, clhs)
        when (rev || ErrorReduce `elem` opts) $ do
           addIBC (IBCErrReduce fname)
           addErrReduce fname
        pop_estack
        return (Right (clhs, crhs), lhs)
  where
    pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
    pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
pinfo ElabInfo
info [(Name, PTerm)]
ns [Name]
ds 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 (\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 = newps,
                       inblock = newb,
                       liftname = 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] -> Term -> [Name]
borrowedNames [Name]
env (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ (NS (UN Text
lend) [Text
owner]) Term
_) Term
_) Term
arg)
        | Text
owner Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Ownership" Bool -> Bool -> Bool
&&
          (Text
lend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"lend" Bool -> Bool -> Bool
|| Text
lend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Read") = Term -> [Name]
forall {n}. TT n -> [Name]
getVs Term
arg
       where
         getVs :: TT n -> [Name]
getVs (V Int
i) = [[Name]
env[Name] -> Int -> Name
forall a. HasCallStack => [a] -> Int -> a
!!Int
i]
         getVs (App AppStatus n
_ TT n
f 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 TT n
_ = []
    borrowedNames [Name]
env (App AppStatus Name
_ Term
f Term
a) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> Term -> [Name]
borrowedNames [Name]
env Term
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [Name]
borrowedNames [Name]
env Term
a
    borrowedNames [Name]
env (Bind Name
n Binder Term
b Term
sc) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Binder Term -> [Name]
borrowedB Binder Term
b [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [Name]
borrowedNames (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env) Term
sc
       where borrowedB :: Binder Term -> [Name]
borrowedB (Let RigCount
_ Term
t Term
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> Term -> [Name]
borrowedNames [Name]
env Term
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [Name]
borrowedNames [Name]
env Term
v
             borrowedB Binder Term
b = [Name] -> Term -> [Name]
borrowedNames [Name]
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
    borrowedNames [Name]
_ Term
_ = []

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

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

    sepBlocks :: [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks [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' [Name]
ns (d :: PDecl' t
d@(PTy Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ FnOpts
_ Name
n FC
_ t
t) : [PDecl' t]
bs)
            = let ([PDecl' t]
bf, [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' [Name]
ns (d :: PDecl' t
d@(PClauses FC
_ FnOpts
_ Name
n [PClause' t]
_) : [PDecl' t]
bs)
         | Bool -> Bool
not (Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns) = let ([PDecl' t]
bf, [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' [Name]
ns (PDecl' t
b : [PDecl' t]
bs) = let ([PDecl' t]
bf, [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' [Name]
ns [] = ([], [])

    -- term is not within "with" block
    isOutsideWith :: PTerm -> Bool
    isOutsideWith :: PTerm -> Bool
isOutsideWith (PApp FC
_ (PRef FC
_ [FC]
_ (SN (WithN Int
_ Name
_))) [PArg]
_) = Bool
False
    isOutsideWith PTerm
_ = Bool
True

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

        ctxt <- getContext
        let lhs_tm = Term -> Term
orderPats (Term -> Term
getInferTerm Term
lhs')
        let lhs_ty = Term -> Term
getInferType Term
lhs'
        let ret_ty = Term -> Term
forall n. TT n -> TT n
getRetTy (Term -> Term
forall n. TT n -> TT n
explicitNames (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
lhs_ty))
        let static_names = IState -> Term -> [Name]
getStaticNames IState
i Term
lhs_tm
        logElab 5 (show lhs_tm ++ "\n" ++ show static_names)
        (clhs_c, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm
        let clhs = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
clhs_c

        logElab 5 ("Checked " ++ show clhs)
        let bargs = Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getPBtys (Term -> Term
forall n. TT n -> TT n
explicitNames (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
lhs_tm))
        wval <- case wval_in of
                     PTerm
Placeholder -> Err -> StateT IState (ExceptT Err IO) PTerm
forall a. Err -> Idris a
ierror (Err -> StateT IState (ExceptT Err IO) PTerm)
-> Err -> StateT IState (ExceptT Err IO) 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 String
"No expression for the with block to inspect.\nYou need to replace the _ with an expression."
                     PTerm
_ -> PTerm -> StateT IState (ExceptT Err IO) PTerm
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> StateT IState (ExceptT Err IO) PTerm)
-> PTerm -> StateT IState (ExceptT Err IO) 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, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
bargs) PTerm
wval_in
        logElab 5 ("Checking " ++ showTmImpls wval)
        -- Elaborate wval in this context
        ((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-
            tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")
                        (bindTyArgs PVTy bargs infP) initEState
                        (do pbinds i lhs_tm
                            -- proof search can use explicitly written names
                            mapM_ addPSname (allNamesIn lhs_in)
                            setNextName
                            -- TODO: may want where here - see winfo abpve
                            (ElabResult _ d is ctxt' newDecls highlights newGName) <- errAt "with value in " fname Nothing
                              (erun fc (build i info ERHS opts fname (infTerm wval)))
                            erun fc $ psolve lhs_tm
                            tt <- get_term
                            return (tt, d, is, ctxt', newDecls, highlights, newGName))
        setContext ctxt'
        processTacticDecls info newDecls
        sendHighlighting highlights
        updateIState $ \IState
i -> IState
i { idris_name = newGName }

        def' <- checkDef info fc iderr True defer
        let def'' = ((Name, (Int, Maybe Name, Term, [Name]))
 -> (Name, (Int, Maybe Name, Term, [Name], Bool, Bool)))
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, (Int
i, Maybe Name
top, Term
t, [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Term
t, [Name]
ns, Bool
False, Bool
True))) [(Name, (Int, Maybe Name, Term, [Name]))]
def'
        addDeferred def''
        mapM_ (elabCaseBlock info opts) is

        let wval' = Term
wvalElab
        logElab 5 ("Checked wval " ++ show wval')

        ctxt <- getContext
        (cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')
        let cwvaltyN = Term -> Term
forall n. TT n -> TT n
explicitNames (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
cwvalty)
        let cwvalN = Term -> Term
forall n. TT n -> TT n
explicitNames (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
cwval)
        logElab 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show 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 getArgTys cwvaltyN of
             [] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
             ((Name, Term)
_:[(Name, Term)]
_) -> 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 (Term -> Err
forall t. t -> Err' t
WithFnType Term
cwvalty)

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

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

        -- Highlight explicit proofs
        sendHighlighting $ S.fromList [(FC' fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

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

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

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

        addIBC (IBCDef wname)
        addIBC (IBCImp wname)
        addIBC (IBCStatic wname)

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

        -- in the subdecls, lhs becomes:
        --         fname  pats | wpat [rest]
        --    ==>  fname' ps   wpat [rest], match pats against toplevel for ps
        wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))
                       withblock
        logElab 3 ("with block " ++ show wb)
        setFlags wname [Inlinable]
        when (AssertTotal `elem` opts) $
           setFlags wname [Inlinable, AssertTotal]
        i <- getIState
        let rhstrans' = IState
-> Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PTerm
-> PTerm
updateWithTerm IState
i Maybe Name
mpn Name
wname PTerm
lhs (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
bargs_pre) (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst ([(Name, Term)]
bargs_post))
                             (PTerm -> PTerm) -> (PTerm -> PTerm) -> PTerm -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
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
        mapM_ (rec_elabDecl info EAll (info { rhs_trans = rhstrans' })) wb

        -- rhs becomes: fname' ps_pre wval ps_post Refl
        let rhs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
wname)
                    (((Name, Term) -> PArg) -> [(Name, Term)] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> PArg
forall {t}. t -> PArg' t
pexp (PTerm -> PArg) -> ((Name, Term) -> PTerm) -> (Name, Term) -> PArg
forall b c a. (b -> c) -> (a -> b) -> a -> c
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, Term) -> Name) -> (Name, Term) -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, Term) -> Name
forall a b. (a, b) -> a
fst) [(Name, Term)]
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, Term) -> PArg) -> [(Name, Term)] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> PArg
forall {t}. t -> PArg' t
pexp (PTerm -> PArg) -> ((Name, Term) -> PTerm) -> (Name, Term) -> PArg
forall b c a. (b -> c) -> (a -> b) -> a -> c
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, Term) -> Name) -> (Name, Term) -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, Term) -> Name
forall a b. (a, b) -> a
fst) [(Name, Term)]
bargs_post) [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++
                    case Maybe Name
mpn of
                         Maybe Name
Nothing -> []
                         Just Name
_ -> [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 String
"A") PTerm
Placeholder Bool
False
                                               , Name -> PTerm -> Bool -> PArg
forall {t}. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN String
"x") PTerm
Placeholder Bool
False
                                               ])])
        logElab 5 ("New RHS " ++ showTmImpls rhs)
        ctxt <- getContext -- New context with block added
        i <- getIState
        ((rhsElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-
           tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState
                    (do pbinds i lhs_tm
                        setNextName
                        (ElabResult _ d is ctxt' newDecls highlights newGName) <-
                           erun fc (build i info ERHS opts fname rhs)
                        psolve lhs_tm
                        tt <- get_term
                        return (tt, d, is, ctxt', newDecls, highlights, newGName))
        setContext ctxt'

        processTacticDecls info newDecls
        sendHighlighting highlights
        updateIState $ \IState
i -> IState
i { idris_name = newGName }

        ctxt <- getContext
        let rhs' = Term
rhsElab

        def' <- checkDef info fc iderr True defer
        let def'' = ((Name, (Int, Maybe Name, Term, [Name]))
 -> (Name, (Int, Maybe Name, Term, [Name], Bool, Bool)))
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, (Int
i, Maybe Name
top, Term
t, [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Term
t, [Name]
ns, Bool
False, Bool
True))) [(Name, (Int, Maybe Name, Term, [Name]))]
def'
        addDeferred def''
        mapM_ (elabCaseBlock info opts) is
        logElab 5 ("Checked RHS " ++ show rhs')
        (crhs, crhsty) <- recheckC (constraintNS info) fc id [] rhs'
        return (Right (clhs, crhs), lhs)
  where
    getImps :: TT n -> [PArg]
getImps (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
_ TT n
_) 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 TT n
_ = []

    mkAuxC :: Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PDecl' PTerm
-> StateT IState (ExceptT Err IO) (PDecl' PTerm)
mkAuxC Maybe Name
pn Name
wname PTerm
lhs [Name]
ns [Name]
ns' (PClauses FC
fc FnOpts
o Name
n [PClause]
cs)
                = do 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
                     return $ PClauses fc o wname cs'
    mkAuxC Maybe Name
pn Name
wname PTerm
lhs [Name]
ns [Name]
ns' PDecl' PTerm
d = PDecl' PTerm -> StateT IState (ExceptT Err IO) (PDecl' PTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
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 Maybe Name
pn Name
wname PTerm
toplhs [Name]
ns [Name]
ns' (PClause FC
fc Name
n PTerm
tm_in (PTerm
w:[PTerm]
ws) PTerm
rhs [PDecl' PTerm]
wheres)
        = do i <- Idris IState
getIState
             let tm = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
tm_in
             logElab 2 ("Matching " ++ showTmImpls tm ++ " against " ++
                                      showTmImpls toplhs)
             case matchClause i toplhs tm of
                Left (PTerm
a,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]
++ String
":with clause does not match top level"
                Right [(Name, PTerm)]
mvars ->
                    do Int -> String -> Idris ()
logElab Int
3 (String
"Match vars : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)] -> String
forall a. Show a => a -> String
show [(Name, PTerm)]
mvars)
                       lhs <- Name
-> Maybe Name
-> Name
-> [(Name, PTerm)]
-> [Name]
-> [Name]
-> PTerm
-> PTerm
-> StateT IState (ExceptT Err IO) 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
                       return $ PClause fc wname lhs ws rhs wheres
    mkAux Maybe Name
pn Name
wname PTerm
toplhs [Name]
ns [Name]
ns' (PWith FC
fc Name
n PTerm
tm_in (PTerm
w:[PTerm]
ws) PTerm
wval Maybe (Name, FC)
pn' [PDecl' PTerm]
withs)
        = do i <- Idris IState
getIState
             let tm = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
tm_in
             logElab 2 ("Matching " ++ showTmImpls tm ++ " against " ++
                                      showTmImpls toplhs)
             withs' <- mapM (mkAuxC pn wname toplhs ns ns') withs
             case matchClause i toplhs tm of
                Left (PTerm
a,PTerm
b) -> String
-> StateT IState (ExceptT Err IO) PClause
-> StateT IState (ExceptT Err IO) PClause
forall a. String -> a -> a
trace (String
"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 -> 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]
++ String
"with clause does not match top level")
                Right [(Name, PTerm)]
mvars ->
                    do lhs <- Name
-> Maybe Name
-> Name
-> [(Name, PTerm)]
-> [Name]
-> [Name]
-> PTerm
-> PTerm
-> StateT IState (ExceptT Err IO) 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
                       return $ PWith fc wname lhs ws wval pn' withs'
    mkAux Maybe Name
pn Name
wname PTerm
toplhs [Name]
ns [Name]
ns' 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]
++ String
":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 t
n Maybe Name
pn Name
wname [(Name, PTerm)]
mvars [Name]
ns_in [Name]
ns_in' (PApp FC
fc (PRef FC
fc' [FC]
hls' Name
n') [PArg]
args) 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 a. a -> m a
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
                             Maybe Name
Nothing -> []
                             Just Name
pnm -> [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pnm)])
    updateLHS t
n Maybe Name
pn Name
wname [(Name, PTerm)]
mvars [Name]
ns_in [Name]
ns_in' PTerm
tm 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 t Name
mvs FC
fc Name
v | Name
v Name -> t Name -> Bool
forall a. Eq a => a -> t a -> 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 IState
ist Maybe Name
pn Name
wname PTerm
toplhs [Name]
ns_in [Name]
ns_in' PTerm
tm
          = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
updateApp PTerm
tm
       where
         currentFn :: Name -> PTerm -> PTerm
currentFn Name
fname (PAlternative [(Name, Name)]
_ PAltType
_ [PTerm]
as)
              | Just PTerm
tm <- [PTerm] -> Maybe PTerm
getApp [PTerm]
as = PTerm
tm
            where getApp :: [PTerm] -> Maybe PTerm
getApp (tm :: PTerm
tm@(PApp FC
_ (PRef FC
_ [FC]
_ Name
f) [PArg]
_) : [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 (PTerm
_ : [PTerm]
as) = [PTerm] -> Maybe PTerm
getApp [PTerm]
as
                  getApp [] = Maybe PTerm
forall a. Maybe a
Nothing
         currentFn Name
_ PTerm
tm = PTerm
tm

         updateApp :: PTerm -> PTerm
updateApp wtm :: PTerm
wtm@(PWithApp FC
fcw PTerm
tm_in 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 (PTerm, PTerm)
_ -> 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]
++ String
":with application does not match top level "))
                Right [(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 Term
wty = Name -> Context -> Maybe Term
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
                                     Maybe Name
Nothing -> []
                                     Just Name
pnm -> [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pnm)]) in
                          case Maybe Term
wty of
                               Maybe Term
Nothing -> PTerm
res -- can't happen!
                               Just Term
ty -> Term -> PTerm -> PTerm
addResolves Term
ty PTerm
res
         updateApp PTerm
tm = PTerm
tm

         addResolves :: Term -> PTerm -> PTerm
addResolves Term
ty (PApp FC
fc PTerm
f [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f (FC -> Term -> [PArg] -> [PArg]
addResolvesArgs FC
fc Term
ty [PArg]
args)
         addResolves Term
ty 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 -> Term -> [PArg] -> [PArg]
addResolvesArgs FC
fc (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc) (PArg
a : [PArg]
args)
             | (P NameType
_ Name
cn Term
_, [Term]
_) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
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 InterfaceInfo
_ -> PArg
a { getTm = PResolveTC fc } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: FC -> Term -> [PArg] -> [PArg]
addResolvesArgs FC
fc Term
sc [PArg]
args
                        Maybe InterfaceInfo
Nothing -> PArg
a PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: FC -> Term -> [PArg] -> [PArg]
addResolvesArgs FC
fc Term
sc [PArg]
args
         addResolvesArgs FC
fc (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc) (PArg
a : [PArg]
args)
                 = PArg
a PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: FC -> Term -> [PArg] -> [PArg]
addResolvesArgs FC
fc Term
sc [PArg]
args
         addResolvesArgs FC
fc Term
_ [PArg]
args = [PArg]
args

    fullApp :: PTerm -> PTerm
fullApp (PApp FC
_ (PApp FC
fc PTerm
f [PArg]
args) [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 PTerm
x = PTerm
x

    split :: [a] -> [(a, b)] -> [(a, b)] -> ([(a, b)], [(a, b)])
split [] [(a, b)]
rest [(a, b)]
pre = ([(a, b)] -> [(a, b)]
forall a. [a] -> [a]
reverse [(a, b)]
pre, [(a, b)]
rest)
    split [a]
deps ((a
n, b
ty) : [(a, b)]
rest) [(a, b)]
pre
          | a
n a -> [a] -> Bool
forall a. Eq a => 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 [a]
deps [] [(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 n
wn TT n
wv TT n
wty (a
n, 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 PTerm -> PTerm
f (PClause FC
fc Name
n PTerm
lhs [PTerm]
args PTerm
rhs [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 PTerm -> PTerm
f (PWith FC
fc Name
n PTerm
lhs [PTerm]
args PTerm
warg Maybe (Name, FC)
prf [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 PTerm -> PTerm
f (PClauseR FC
fc [PTerm]
args PTerm
rhs [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 PTerm -> PTerm
f (PWithR FC
fc [PTerm]
args PTerm
warg Maybe (Name, FC)
prf [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 PTerm -> PTerm
f (PClauses FC
fc FnOpts
opt Name
n [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 PTerm -> PTerm
f PDecl' PTerm
t = PDecl' PTerm
t