{-# 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
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 :: Maybe FC
elabFC = forall a. a -> Maybe a
Just FC
fc }
Context
ctxt <- Idris Context
getContext
IState
ist <- Idris IState
getIState
[Optimisation]
optimise <- Idris [Optimisation]
getOptimise
let petrans :: Bool
petrans = Optimisation
PETransform forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Optimisation]
optimise
[Int]
inacc <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field OptInfo [(Int, Name)]
opt_inaccessible forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n)
let tys :: [Term]
tys = Name -> Context -> [Term]
lookupTy Name
n Context
ctxt
let reflect :: Bool
reflect = FnOpt
Reflection forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
reflect Bool -> Bool -> Bool
&& LanguageExt
FCReflection forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` IState -> [LanguageExt]
idris_language_extensions IState
ist) forall a b. (a -> b) -> a -> b
$
forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"You must turn on the FirstClassReflection extension to use %reflection")
Name -> Context -> Idris ()
checkUndefined Name
n Context
ctxt
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
tys forall a. Ord a => a -> a -> Bool
> Int
1) forall a b. (a -> b) -> a -> b
$ do
Term
fty <- case [Term]
tys of
[] ->
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. Name -> Err' t
NoTypeDecl Name
n)
[Term
ty] -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
ty
let atys_in :: [Term]
atys_in = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall n. TT n -> [(n, TT n)]
getArgTys (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
fty))
let atys :: [(Term, Bool)]
atys = forall a b. (a -> b) -> [a] -> [b]
map (\Term
x -> (Term
x, Term -> Context -> Bool
isCanonical Term
x Context
ctxt)) [Term]
atys_in
[(Either Term (Term, Term), PTerm)]
cs_elab <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ElabInfo
-> FnOpts
-> (Int, PClause)
-> Idris (Either Term (Term, Term), PTerm)
elabClause ElabInfo
info FnOpts
opts)
(forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [PClause]
cs)
Context
ctxt <- Idris Context
getContext
let optinfo :: Ctxt OptInfo
optinfo = IState -> Ctxt OptInfo
idris_optimisation IState
ist
let ([Either Term (Term, Term)]
pats_in, [PTerm]
cs_full) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Either Term (Term, Term), PTerm)]
cs_elab
let pats_raw :: [Either Term (Term, Term)]
pats_raw = forall a b. (a -> b) -> [a] -> [b]
map (forall {a} {b}. Context -> Either a (Term, b) -> Either a (Term, b)
simple_lhs Context
ctxt) [Either Term (Term, Term)]
pats_in
let pats_forced :: [Either Term (Term, Term)]
pats_forced = forall a b. (a -> b) -> [a] -> [b]
map (forall {a} {b}.
Ctxt OptInfo -> Either a (Term, b) -> Either a (Term, b)
force_lhs Ctxt OptInfo
optinfo) [Either Term (Term, Term)]
pats_raw
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Elaborated patterns:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Either Term (Term, Term)]
pats_raw
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Forced patterns:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Either Term (Term, Term)]
pats_forced
FC -> Name -> Idris ()
solveDeferred FC
fc Name
n
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState (Name -> Field IState OptInfo
ist_optimisation Name
n) forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
n)
IState
ist <- Idris IState
getIState
Context
ctxt <- Idris Context
getContext
let tpats :: [Either Term (Term, Term)]
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
[Either Term (Term, Term)]
pe_tm <- IState
-> [Either Term (Term, Term)]
-> StateT IState (ExceptT Err IO) [Either Term (Term, Term)]
doPartialEval IState
ist [Either Term (Term, Term)]
tpats
let pats_pe :: [Either Term (Term, Term)]
pats_pe = if Bool
petrans
then forall a b. (a -> b) -> [a] -> [b]
map (forall {a} {b}.
Ctxt OptInfo -> Either a (Term, b) -> Either a (Term, b)
force_lhs Ctxt OptInfo
optinfo forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 :: Bool
tcase = IOption -> Bool
opt_typecase (IState -> IOption
idris_options IState
ist)
[[(Term, Term)]]
newrules <- if Bool
petrans
then forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Either Term (Term, Term)
e -> case Either Term (Term, Term)
e of
Left Term
_ -> 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) [Either Term (Term, Term)]
pats_pe
else forall (m :: * -> *) a. Monad m => a -> m a
return []
IState
ist <- Idris IState
getIState
let pats_transformed :: [Either Term (Term, Term)]
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
let pdef :: [([Name], Term, Term)]
pdef = forall a b. (a -> b) -> [a] -> [b]
map (\([(Name, Term)]
ns, Term
lhs, Term
rhs) -> (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns, Term
lhs, Term
rhs)) forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map forall {n} {n}.
Either (TT n) (TT n, TT n) -> ([(n, TT n)], TT n, TT n)
debind [Either Term (Term, Term)]
pats_forced
let pdef_pe :: [([(Name, Term)], Term, Term)]
pdef_pe = forall a b. (a -> b) -> [a] -> [b]
map forall {n} {n}.
Either (TT n) (TT n, TT n) -> ([(n, TT n)], TT n, TT n)
debind [Either Term (Term, Term)]
pats_transformed
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Initial typechecked patterns:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Either Term (Term, Term)]
pats_raw
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Initial typechecked pattern def:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [([Name], Term, Term)]
pdef
IState
ist <- Idris IState
getIState
Int
numArgs <- forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall {a} {n} {c}. [(a, TT n, c)] -> TC Int
sameLength [([Name], Term, Term)]
pdef
case FnOpts -> Maybe [(Name, Maybe Int)]
specNames FnOpts
opts of
Just [(Name, Maybe Int)]
_ ->
do Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Partially evaluated:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Either Term (Term, Term)]
pats_pe
Maybe [(Name, Maybe Int)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Transformed:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Either Term (Term, Term)]
pats_transformed
Name -> [Int]
erInfo <- IState -> Name -> [Int]
getErasureInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
tree :: CaseDef
tree@(CaseDef [Name]
scargs SC
sc [Term]
_) <- forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$
Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Term, Bool)]
-> [([Name], Term, Term)]
-> (Name -> [Int])
-> TC CaseDef
simpleCase Bool
tcase (forall t. String -> SC' t
UnmatchedCase String
"Error") Bool
reflect Phase
CompileTime FC
fc [Int]
inacc [(Term, Bool)]
atys [([Name], Term, Term)]
pdef Name -> [Int]
erInfo
Bool
cov <- Idris Bool
coverage
[PTerm]
pmissing <-
if Bool
cov Bool -> Bool -> Bool
&& Bool -> Bool
not (forall {a} {a} {b}. Eq a => [Either a (TT a, b)] -> Bool
hasDefault [Either Term (Term, Term)]
pats_raw)
then do
[PTerm]
missing <- FC
-> Name
-> [([Name], Term)]
-> [PTerm]
-> StateT IState (ExceptT Err IO) [PTerm]
genClauses FC
fc Name
n
(forall a b. (a -> b) -> [a] -> [b]
map (\ ([Name]
ns,Term
tm,Term
_) -> ([Name]
ns, Term
tm)) [([Name], Term, Term)]
pdef)
[PTerm]
cs_full
[PTerm]
missing' <- ElabInfo
-> FC
-> Bool
-> Name
-> [PTerm]
-> StateT IState (ExceptT Err IO) [PTerm]
checkPossibles ElabInfo
info FC
fc Bool
True Name
n [PTerm]
missing
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"Must be unreachable (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [PTerm]
missing') forall a. [a] -> [a] -> [a]
++ String
"):\n" forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
showSep String
"\n" (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
missing') forall a. [a] -> [a] -> [a]
++
String
"\nAgainst: " forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
showSep String
"\n" (forall a b. (a -> b) -> [a] -> [b]
map (\Term
t -> PTerm -> String
showTmImpls (IState -> Term -> PTerm
delab IState
ist Term
t)) (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c}. (a, b, c) -> b
getLHS [([Name], Term, Term)]
pdef))
forall (m :: * -> *) a. Monad m => a -> m a
return [PTerm]
missing'
else forall (m :: * -> *) a. Monad m => a -> m a
return []
let pcover :: Bool
pcover = forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
pmissing
[([Name], Term, Term)]
pdef_in' <- forall term. Optimisable term => term -> Idris term
applyOpts forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\([(Name, Term)]
ns, Term
lhs, Term
rhs) -> (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns, Term
lhs, Term
rhs)) [([(Name, Term)], Term, Term)]
pdef_pe
Context
ctxt <- Idris Context
getContext
let pdef' :: [([Name], Term, Term)]
pdef' = forall a b. (a -> b) -> [a] -> [b]
map (forall {b}. Context -> ([Name], b, Term) -> ([Name], b, Term)
simple_rt Context
ctxt) [([Name], Term, Term)]
pdef_in'
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"After data structure transformations:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [([Name], Term, Term)]
pdef'
IState
ist <- Idris IState
getIState
let tot :: Totality
tot | Bool
pcover = Totality
Unchecked
| FnOpt
AssertTotal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts = [Int] -> Totality
Total []
| FnOpt
PEGenerated forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts = Totality
Generated
| Bool
otherwise = PReason -> Totality
Partial PReason
NotCovering
case CaseDef
tree of
CaseDef [Name]
_ SC
_ [] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
CaseDef [Name]
_ SC
_ [Term]
xs -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Term
x ->
FC -> OutputDoc -> Idris ()
iWarn FC
fc forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
text String
"Unreachable case:" forall a. Doc a -> Doc a -> Doc a
</> forall a. String -> Doc a
text (forall a. Show a => a -> String
show (IState -> Term -> PTerm
delab IState
ist Term
x))
) [Term]
xs
let knowncovering :: Bool
knowncovering = (Bool
pcover Bool -> Bool -> Bool
&& Bool
cov) Bool -> Bool -> Bool
|| FnOpt
AssertTotal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts
let defaultcase :: SC' (TT n)
defaultcase = if Bool
knowncovering
then forall t. t -> SC' t
STerm forall n. TT n
Erased
else forall t. String -> SC' t
UnmatchedCase forall a b. (a -> b) -> a -> b
$ String
"*** " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++
String
":unmatched case in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++
String
" ***"
CaseDef
tree' <- forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Term, Bool)]
-> [([Name], Term, Term)]
-> (Name -> [Int])
-> TC CaseDef
simpleCase Bool
tcase forall {n}. SC' (TT n)
defaultcase Bool
reflect
Phase
RunTime FC
fc [Int]
inacc [(Term, Bool)]
atys [([Name], Term, Term)]
pdef' Name -> [Int]
erInfo
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Unoptimised " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CaseDef
tree
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Optimised: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CaseDef
tree'
Context
ctxt <- Idris Context
getContext
IState
ist <- Idris IState
getIState
IState -> Idris ()
putIState (IState
ist { idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (forall a. NFData a => a -> a
force [([(Name, Term)], Term, Term)]
pdef_pe, forall a. NFData a => a -> a
force [PTerm]
pmissing)
(IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
ist) })
let caseInfo :: CaseInfo
caseInfo = Bool -> Bool -> Bool -> CaseInfo
CaseInfo (FnOpts -> Bool
inlinable FnOpts
opts) (FnOpts -> Bool
inlinable FnOpts
opts) (FnOpts -> Bool
dictionary FnOpts
opts)
case Name -> Context -> Maybe Term
lookupTyExact Name
n Context
ctxt of
Just Term
ty ->
do Context
ctxt' <- do Context
ctxt <- Idris Context
getContext
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$
Name
-> (Name -> [Int])
-> CaseInfo
-> Bool
-> SC
-> Bool
-> Bool
-> [(Term, Bool)]
-> [Int]
-> [Either Term (Term, Term)]
-> [([Name], Term, Term)]
-> [([Name], Term, Term)]
-> Term
-> Context
-> TC Context
addCasedef Name
n Name -> [Int]
erInfo CaseInfo
caseInfo
Bool
tcase forall {n}. SC' (TT n)
defaultcase
Bool
reflect
(FnOpt
AssertTotal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts)
[(Term, Bool)]
atys
[Int]
inacc
[Either Term (Term, Term)]
pats_forced
[([Name], Term, Term)]
pdef
[([Name], Term, Term)]
pdef' Term
ty
Context
ctxt
Context -> Idris ()
setContext Context
ctxt'
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
Name -> Idris ()
addDefinedName Name
n
Name -> Totality -> Idris ()
setTotality Name
n Totality
tot
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
reflect Bool -> Bool -> Bool
&& FnOpt
PEGenerated forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts) forall a b. (a -> b) -> a -> b
$
do (FC, Name) -> Idris ()
totcheck (FC
fc, Name
n)
(FC, Name) -> Idris ()
defer_totcheck (FC
fc, Name
n)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Totality
tot forall a. Eq a => a -> a -> Bool
/= Totality
Unchecked) forall a b. (a -> b) -> a -> b
$ IBCWrite -> Idris ()
addIBC (Name -> Totality -> IBCWrite
IBCTotal Name
n Totality
tot)
IState
i <- Idris IState
getIState
Context
ctxt <- Idris Context
getContext
case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
(CaseOp 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ SC -> [Name] -> [(Name, [[Name]])]
findCalls SC
sc [Name]
scargs
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"Called names: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
calls
Maybe Accessibility
nvis <- Name -> Idris (Maybe Accessibility)
getFromHideList Name
n
case Maybe Accessibility
nvis of
Just Accessibility
Public -> 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Name -> [Name] -> Idris ()
addCalls Name
n [Name]
calls
let rig :: RigCount
rig = if Term -> Bool
linearArg (Context -> Env -> Term -> Term
whnfArgs Context
ctxt [] Term
ty)
then RigCount
Rig1
else RigCount
RigW
(Context -> Context) -> Idris ()
updateContext (Name -> RigCount -> Context -> Context
setRigCount Name
n (Context -> RigCount -> [Name] -> RigCount
minRig Context
ctxt RigCount
rig [Name]
calls))
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCCG Name
n)
[Def]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
CoveringFn forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) forall a b. (a -> b) -> a -> b
$ FC -> [Name] -> Name -> Name -> Idris ()
checkAllCovering FC
fc [] Name
n Name
n
Name -> Idris ()
checkIfGuarded Name
n
IState
ist <- Idris IState
getIState
let statics :: [Bool]
statics = case 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 -> []
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
statics) forall a b. (a -> b) -> a -> b
$ do Name -> Idris [Name]
getAllNames Name
n
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
checkUndefined :: Name -> Context -> Idris ()
checkUndefined Name
n Context
ctxt = case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[TyDecl NameType
_ Term
_] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Def]
_ -> forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (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') = forall {n}. [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
depat [] TT n
x
([(n, TT n)]
_, TT n
y') = 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') = forall {n}. [(n, TT n)] -> TT n -> ([(n, TT n)], TT n)
depat [] TT n
x in
([(n, TT n)]
vs, TT n
x', 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) forall a. a -> [a] -> [a]
: [(n, TT n)]
acc) (forall n. TT n -> TT n -> TT n
instantiate (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
xforall 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 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)]
_) <- forall a. [a] -> [a]
reverse [Either a (TT a, b)]
cs
, ([a]
pvs, TT a
tm) <- forall {a}. TT a -> ([a], TT a)
getPVs (forall n. TT n -> TT n
explicitNames TT a
lhs)
, (TT a
f, [TT a]
args) <- forall n. TT n -> (TT n, [TT n])
unApply TT a
tm = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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
simple_lhs :: Context -> Either a (Term, b) -> Either a (Term, b)
simple_lhs Context
ctxt (Right (Term
x, b
y))
= 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)) = 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, 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 [] = forall a. Maybe a
Nothing
specNames (Specialise [(Name, Maybe Int)]
ns : FnOpts
_) = 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 Int
l <- [(a, TT n, c)] -> TC Int
sameLength [(a, TT n, c)]
xs
let (TT n
_, [TT n]
as) = forall n. TT n -> (TT n, [TT n])
unApply TT n
x
if (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(a, TT n, c)]
xs Bool -> Bool -> Bool
|| Int
l forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT n]
as) then forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT n]
as)
else forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"Clauses have differing numbers of arguments "))
sameLength [] = forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
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 -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return [Either Term (Term, Term)]
t
Maybe [Either Term (Term, Term)]
Nothing -> forall a. Err -> Idris a
ierror (forall t. FC -> Err' t -> Err' t
At FC
fc (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 (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 =
Term -> Term
force Term
lhs
where
force :: Term -> Term
force ap :: Term
ap@(App AppStatus Name
_ Term
_ Term
_)
| (fn :: Term
fn@(P NameType
_ Name
c Term
_), [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Just OptInfo
copt <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
c Ctxt OptInfo
opts
= let args' :: [Term]
args' = 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
forall n. TT n -> [TT n] -> TT n
mkApp Term
fn (forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
force [Term]
args')
force (App AppStatus Name
t Term
f Term
a)
= forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
t (Term -> Term
force Term
f) (Term -> Term
force Term
a)
force (Bind Name
n Binder Term
b Term
sc) = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b (Term -> Term
force Term
sc)
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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t t
fs = forall n. TT n
Erased forall a. a -> [a] -> [a]
: t -> t t -> [TT n] -> [TT n]
eraseArg (t
i forall a. Num a => a -> a -> a
+ t
1) t t
fs [TT n]
ns
| Bool
otherwise = TT n
n forall a. a -> [a] -> [a]
: t -> t t -> [TT n] -> [TT n]
eraseArg (t
i forall a. Num a => a -> a -> a
+ t
1) t t
fs [TT n]
ns
eraseArg t
i t t
_ [] = []
elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]
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 forall a. Ord a => a -> a -> Bool
> Int
5 = forall (m :: * -> *) a. Monad m => a -> m a
return []
elabPE ElabInfo
info FC
fc Name
caller Term
r =
do IState
ist <- Idris IState
getIState
let sa :: [(Name, [(PEArgType, Term)])]
sa = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name, [(PEArgType, Term)])
ap -> forall a b. (a, b) -> a
fst (Name, [(PEArgType, Term)])
ap forall a. Eq a => a -> a -> Bool
/= Name
caller) forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> Term -> [(Name, [(PEArgType, Term)])]
getSpecApps IState
ist [] Term
r
[[(Term, Term)]]
rules <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, [(PEArgType, Term)])
-> StateT IState (ExceptT Err IO) [(Term, Term)]
mkSpecialised [(Name, [(PEArgType, Term)])]
sa
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Term, Term)]]
rules
where
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
IState
ist <- Idris IState
getIState
Context
ctxt <- Idris Context
getContext
(PTerm
specTy, (Name, [(PEArgType, Term)])
specapp) <- IState
-> (Name, [(PEArgType, Term)])
-> StateT
IState (ExceptT Err IO) (PTerm, (Name, [(PEArgType, Term)]))
getSpecTy IState
ist (Name, [(PEArgType, Term)])
specapp_in
let (Name
n, Name
newnm, PEDecl
specdecl) = IState
-> (Name, [(PEArgType, Term)]) -> PTerm -> (Name, Name, PEDecl)
getSpecClause IState
ist (Name, [(PEArgType, Term)])
specapp PTerm
specTy
let lhs :: PTerm
lhs = PEDecl -> PTerm
pe_app PEDecl
specdecl
let rhs :: PTerm
rhs = PEDecl -> PTerm
pe_def PEDecl
specdecl
let undef :: Bool
undef = case Name -> Context -> Maybe Def
lookupDefExact Name
newnm Context
ctxt of
Maybe Def
Nothing -> Bool
True
Maybe Def
_ -> Bool
False
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show (Name
newnm, Bool
undef, forall a b. (a -> b) -> [a] -> [b]
map (IState -> (PEArgType, Term) -> Bool
concreteArg IState
ist) (forall a b. (a, b) -> b
snd (Name, [(PEArgType, Term)])
specapp))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(if (Bool
undef Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (IState -> (PEArgType, Term) -> Bool
concreteArg IState
ist) (forall a b. (a, b) -> b
snd (Name, [(PEArgType, Term)])
specapp)) then do
[Name]
cgns <- Name -> Idris [Name]
getAllNames Name
n
let cgns' :: [Name]
cgns' = forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
x -> Name
x forall a. Eq a => a -> a -> Bool
/= Name
n Bool -> Bool -> Bool
&&
IState -> Name -> Bool
notStatic IState
ist Name
x) [Name]
cgns
let maxred :: Int
maxred = case Name -> Context -> [Totality]
lookupTotal Name
n Context
ctxt of
[Total [Int]
_] -> Int
65536
[Totality
Productive] -> Int
16
[Totality]
_ -> Int
1
let specnames :: [(Name, Maybe Int)]
specnames = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {a} {n}.
Num a =>
Bool -> (PEArgType, TT n) -> Maybe (n, Maybe a)
specName (PEDecl -> Bool
pe_simple PEDecl
specdecl))
(forall a b. (a, b) -> b
snd (Name, [(PEArgType, Term)])
specapp)
[[(Name, Maybe Int)]]
descs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> Idris [(Name, Maybe Int)]
getStaticsFrom (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Maybe Int)]
specnames)
let opts :: FnOpts
opts = [[(Name, Maybe Int)] -> FnOpt
Specialise ((if PEDecl -> Bool
pe_simple PEDecl
specdecl
then forall a b. (a -> b) -> [a] -> [b]
map (\Name
x -> (Name
x, forall a. Maybe a
Nothing)) [Name]
cgns'
else []) forall a. [a] -> [a] -> [a]
++
(Name
n, forall a. a -> Maybe a
Just Int
maxred) forall a. a -> [a] -> [a]
: [(Name, Maybe Int)]
specnames forall a. [a] -> [a] -> [a]
++
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Name, Maybe Int)]]
descs)]
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Specialising application: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name, [(PEArgType, Term)])
specapp
forall a. [a] -> [a] -> [a]
++ String
"\n in \n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
caller forall a. [a] -> [a] -> [a]
++
String
"\n with \n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FnOpts
opts
forall a. [a] -> [a] -> [a]
++ String
"\nCalling: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
cgns
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"New name: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
newnm
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"PE definition type : " forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show PTerm
specTy)
forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FnOpts
opts
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"PE definition " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
newnm forall a. [a] -> [a] -> [a]
++ String
":\n" forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
showSep String
"\n"
(forall a b. (a -> b) -> [a] -> [b]
map (\ (PTerm
lhs, PTerm
rhs) ->
(PTerm -> String
showTmImpls PTerm
lhs forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++
PTerm -> String
showTmImpls PTerm
rhs)) (PEDecl -> [(PTerm, PTerm)]
pe_clauses PEDecl
specdecl))
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" transformation rule: " forall a. [a] -> [a] -> [a]
++
PTerm -> String
showTmImpls PTerm
rhs forall a. [a] -> [a] -> [a]
++ String
" ==> " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs
ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> StateT IState (ExceptT Err IO) Term
elabType ElabInfo
info SyntaxInfo
defaultSyntax forall a. Docstring a
emptyDocstring [] FC
fc FnOpts
opts Name
newnm FC
NoFC PTerm
specTy
let def :: [PClause]
def = forall a b. (a -> b) -> [a] -> [b]
map (\(PTerm
lhs, PTerm
rhs) ->
let lhs' :: PTerm
lhs' = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
hiddenToPH forall a b. (a -> b) -> a -> b
$ IState -> PTerm -> PTerm
stripUnmatchable IState
ist PTerm
lhs in
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)
(Term, Term)
trans <- ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
elabTransform ElabInfo
info FC
fc Bool
False PTerm
rhs PTerm
lhs
ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
elabClauses (ElabInfo
info {pe_depth :: Int
pe_depth = ElabInfo -> Int
pe_depth ElabInfo
info forall a. Num a => a -> a -> a
+ Int
1}) FC
fc
(FnOpt
PEGeneratedforall a. a -> [a] -> [a]
:FnOpts
opts) Name
newnm [PClause]
def
forall (m :: * -> *) a. Monad m => a -> m a
return [(Term, Term)
trans]
else forall (m :: * -> *) a. Monad m => a -> m a
return [])
(\Err
e -> do Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Couldn't specialise: " forall a. [a] -> [a] -> [a]
++ (IState -> Err -> String
pshow IState
ist Err
e)
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]
_) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = forall a. a -> Maybe a
Just (n
n, 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]
_) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = forall a. a -> Maybe a
Just (n
n, 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]
_) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = forall a. a -> Maybe a
Just (n
n, forall a. a -> Maybe a
Just (if Bool
simpl then a
1 else a
0))
specName Bool
simpl (PEArgType, TT n)
_ = forall a. Maybe a
Nothing
getStaticsFrom :: Name -> Idris [(Name, Maybe Int)]
getStaticsFrom :: Name -> Idris [(Name, Maybe Int)]
getStaticsFrom Name
n = do [Name]
ns <- Name -> Idris [Name]
getAllNames Name
n
IState
i <- Idris IState
getIState
let statics :: [Name]
statics = forall a. (a -> Bool) -> [a] -> [a]
filter (IState -> Name -> Bool
staticFn IState
i) [Name]
ns
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, forall a. Maybe a
Nothing)) [Name]
statics)
staticFn :: IState -> Name -> Bool
staticFn :: IState -> Name -> Bool
staticFn IState
i Name
n = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt FnOpts
idris_flags IState
i) of
[FnOpts
opts] -> 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 forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
ist) of
Just [Bool]
s -> Bool -> Bool
not (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]
_) <- 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
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 (forall n. TT n -> TT n
explicitNames Term
ty)
specty :: Term
specty = Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] (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' (forall n. TT n -> TT n
explicitNames Term
specty) in
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
t, (Name
n, [(PEArgType, Term)]
args'))
[Term]
_ -> forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ String
"Ambiguous name " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" (getSpecTy)"
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_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name -> Name
nsroot Name
n) forall a. [a] -> [a] -> [a]
++ String
"_" forall a. [a] -> [a] -> [a]
++
Word64 -> String -> String
qhash Word64
5381 (String -> [String] -> String
showSep String
"_" (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Show a => (PEArgType, TT a) -> String
showArg [(PEArgType, Term)]
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) = forall {a}. Show a => TT a -> String
qshow TT a
n
showArg (ImplicitS Name
_, TT a
n) = 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 forall a. [a] -> [a] -> [a]
++ TT a -> String
qshow TT a
a
qshow (P NameType
_ a
n TT a
_) = forall a. Show a => a -> String
show a
n
qshow (Constant Const
c) = forall a. Show a => a -> String
show Const
c
qshow TT a
_ = String
""
qhash :: Word64 -> String -> String
qhash :: Word64 -> String -> String
qhash Word64
hash [] = forall a. (Integral a, Show a) => a -> String -> String
showHex (forall a. Num a => a -> a
abs Word64
hash forall a. Integral a => a -> a -> a
`mod` Word64
0xffffffff) String
""
qhash Word64
hash (Char
x:String
xs) = Word64 -> String -> String
qhash (Word64
hash forall a. Num a => a -> a -> a
* Word64
33 forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral(forall a. Enum a => a -> Int
fromEnum Char
x)) String
xs
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 Context
ctxt <- Idris Context
getContext
IState
i <- Idris IState
getIState
let lhs :: PTerm
lhs = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in
Int -> String -> Idris ()
logElab Int
10 forall a b. (a -> b) -> a -> b
$ String
"Trying missing case: " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs
case forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN Int
0 String
"patLHS") Term
infP EState
initEState
(forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> [Name]
-> PTerm
-> ElabD ElabResult
buildTC IState
i ElabInfo
info ElabMode
EImpossible [] Name
fname
(PTerm -> [Name]
allNamesIn PTerm
lhs_in)
(PTerm -> PTerm
infTerm PTerm
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 forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
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 forall a b. (a -> b) -> a -> b
$ String
"Empty type in pattern "
forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a b. (a -> b) -> a -> b
$ String
"Valid " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
"\n"
forall a. [a] -> [a] -> [a]
++ String
" from " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
lhs
forall (m :: * -> *) a. Monad m => a -> m a
return (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 forall a b. (a -> b) -> a -> b
$ String
"Conversion failure"
forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Error Err
err -> do Int -> String -> Idris ()
logLvl Int
10 forall a b. (a -> b) -> a -> b
$ String
"Impossible case " forall a. [a] -> [a] -> [a]
++ (IState -> Err -> String
pshow IState
i Err
err)
forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Context -> Err -> Bool
recoverableCoverage Context
ctxt Err
err,
Context -> Err -> Bool
validCoverageCase Context
ctxt Err
err)
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 forall a b. (a -> b) -> a -> b
$ String
"Possibly resolvable error on " forall a. [a] -> [a] -> [a]
++
IState -> Err -> String
pshow IState
i (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)
forall a. [a] -> [a] -> [a]
++ String
" on " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs_in
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just PTerm
lhs_in
returnTm IState
i Err
err Bool
False = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
checkPossibles :: ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]
checkPossibles :: ElabInfo
-> FC
-> Bool
-> Name
-> [PTerm]
-> StateT IState (ExceptT Err IO) [PTerm]
checkPossibles ElabInfo
info FC
fc Bool
tcgen Name
fname (PTerm
lhs : [PTerm]
rest)
= do Maybe PTerm
ok <- ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossible ElabInfo
info FC
fc Bool
tcgen Name
fname PTerm
lhs
IState
i <- Idris IState
getIState
let rest' :: [PTerm]
rest' = forall a. (a -> Bool) -> [a] -> [a]
filter (\PTerm
x -> Bool -> Bool
not (PTerm -> PTerm -> Bool
qmatch PTerm
x PTerm
lhs)) (forall a. Int -> [a] -> [a]
take Int
200 [PTerm]
rest) forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
drop Int
200 [PTerm]
rest
[PTerm]
restpos <- ElabInfo
-> FC
-> Bool
-> Name
-> [PTerm]
-> StateT IState (ExceptT Err IO) [PTerm]
checkPossibles ElabInfo
info FC
fc Bool
tcgen Name
fname [PTerm]
rest'
case Maybe PTerm
ok of
Maybe PTerm
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return [PTerm]
restpos
Just PTerm
lhstm -> forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
lhstm 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')
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [PArg]
args forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [PArg]
args'
= PTerm -> PTerm -> Bool
qmatch PTerm
f PTerm
f' Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PTerm -> PTerm -> Bool
qmatch (forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg]
args)
(forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg]
args'))
qmatch (PRef FC
_ [FC]
_ Name
n) (PRef FC
_ [FC]
_ Name
n') = Name
n 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 forall a. Eq a => a -> a -> Bool
== PTerm
y
checkPossibles ElabInfo
_ FC
_ Bool
_ Name
_ [] = 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 (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) (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 forall a. a -> [a] -> [a]
: Context -> Env -> Term -> [Name]
findUnique Context
ctxt ((Name
n, RigCount
RigW, Binder Term
b) forall a. a -> [a] -> [a]
: Env
env) Term
sc
else Context -> Env -> Term -> [Name]
findUnique Context
ctxt ((Name
n, RigCount
RigW, Binder Term
b) forall a. a -> [a] -> [a]
: Env
env) Term
sc
findUnique Context
_ Env
_ Term
_ = []
elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
Idris (Either Term (Term, Term), PTerm)
elabClause :: ElabInfo
-> FnOpts
-> (Int, PClause)
-> Idris (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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts
IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
let lhs :: PTerm
lhs = [Name] -> IState -> PTerm -> PTerm
addImpl [] IState
i PTerm
lhs_in
Maybe PTerm
b <- ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossible ElabInfo
info FC
fc Bool
tcgen Name
fname PTerm
lhs_in
case Maybe PTerm
b of
Just PTerm
_ -> forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc
(forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show PTerm
lhs_in forall a. [a] -> [a] -> [a]
++ String
" is a valid case"))
Maybe PTerm
Nothing -> do Term
ptm <- PTerm -> StateT IState (ExceptT Err IO) Term
mkPatTm PTerm
lhs_in
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Elaborated impossible case " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs forall a. [a] -> [a] -> [a]
++
String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
ptm
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Term
ptm, PTerm
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
Context
ctxt <- Idris Context
getContext
let (PTerm
lhs_in, PTerm
rhs_in, [PDecl' PTerm]
whereblock) = PTerm -> PTerm -> [PDecl' PTerm] -> (PTerm, PTerm, [PDecl' PTerm])
desugarAs PTerm
lhs_in_as PTerm
rhs_in_as [PDecl' PTerm]
whereblock_as
IState
i <- Idris IState
getIState
Bool
inf <- Name -> Idris Bool
isTyInferred Name
fname
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PTerm]
withs) forall a b. (a -> b) -> a -> b
$
forall a. Err -> Idris a
ierror (forall t. FC -> Err' t -> Err' t
At (forall a. a -> Maybe a -> a
fromMaybe FC
NoFC forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe FC
highestFC PTerm
lhs_in_as)
(forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"left hand side of " Name
fname forall a. Maybe a
Nothing
(forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ if PTerm -> Bool
isOutsideWith PTerm
lhs_in
then String
"unexpected patterns outside of \"with\" block"
else String
"unexpected extra \"with\" patterns")))
let fn_ty :: Term
fn_ty = case Name -> Context -> [Term]
lookupTy Name
fname Context
ctxt of
[Term
t] -> Term
t
[Term]
_ -> forall a. HasCallStack => String -> a
error String
"Can't happen (elabClause function type)"
let fn_is :: [PArg]
fn_is = case 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 :: Term
norm_ty = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
fn_ty
let params :: [Name]
params = IState -> [Name] -> [PArg] -> Term -> [Name]
getParamsInType IState
i [] [PArg]
fn_is Term
norm_ty
let tcparams :: [Name]
tcparams = IState -> [Name] -> [PArg] -> Term -> [Name]
getTCParamsInType IState
i [] [PArg]
fn_is Term
norm_ty
let lhs :: PTerm
lhs = PTerm -> PTerm
mkLHSapp forall a b. (a -> b) -> a -> b
$ IState -> PTerm -> PTerm
stripLinear IState
i forall a b. (a -> b) -> a -> b
$ IState -> PTerm -> PTerm
stripUnmatchable IState
i 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)
Int -> String -> Idris ()
logElab Int
10 (forall a. Show a => a -> String
show ([Name]
params, Term
fn_ty) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls (IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in))
Int -> String -> Idris ()
logElab Int
5 (String
"LHS: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FnOpts
opts forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs)
Int -> String -> Idris ()
logElab Int
4 (String
"Fixed parameters: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
params forall a. [a] -> [a] -> [a]
++ String
" from " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs_in forall a. [a] -> [a] -> [a]
++
String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term
fn_ty, [PArg]
fn_is))
((ElabResult Term
lhs' [(Name, (Int, Maybe Name, Term, [Name]))]
dlhs [] Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName, Fails
probs, [Name]
inj), String
_) <-
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN Int
0 String
"patLHS") Term
infP EState
initEState
(do ElabResult
res <- forall aux a.
String -> Name -> Maybe Term -> Elab' aux a -> Elab' aux a
errAt String
"left hand side of " Name
fname forall a. Maybe a
Nothing
(forall aux a. FC -> Elab' aux a -> Elab' aux a
erun (forall a. a -> Maybe a -> a
fromMaybe FC
NoFC forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe FC
highestFC PTerm
lhs_in_as)
(IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> [Name]
-> PTerm
-> ElabD ElabResult
buildTC IState
i ElabInfo
info ElabMode
ELHS FnOpts
opts Name
fname
(PTerm -> [Name]
allNamesIn PTerm
lhs_in)
(PTerm -> PTerm
infTerm PTerm
lhs)))
Fails
probs <- forall aux. Elab' aux Fails
get_probs
[Name]
inj <- forall aux. Elab' aux [Name]
get_inj
forall (m :: * -> *) a. Monad m => a -> m a
return (ElabResult
res, Fails
probs, [Name]
inj))
Context -> Idris ()
setContext Context
ctxt'
ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
(IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
inf forall a b. (a -> b) -> a -> b
$ FC -> [(Term, Term)] -> Idris ()
addTyInfConstraints FC
fc (forall a b. (a -> b) -> [a] -> [b]
map (\(Term
x,Term
y,Bool
_,Env
_,Err
_,[FailContext]
_,FailAt
_) -> (Term
x,Term
y)) Fails
probs)
let lhs_tm :: Term
lhs_tm = Term -> Term
orderPats (Term -> Term
getInferTerm Term
lhs')
let lhs_ty :: Term
lhs_ty = Term -> Term
getInferType Term
lhs'
let static_names :: [Name]
static_names = IState -> Term -> [Name]
getStaticNames IState
i Term
lhs_tm
Int -> String -> Idris ()
logElab Int
3 (String
"Elaborated: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
lhs_tm)
Int -> String -> Idris ()
logElab Int
3 (String
"Elaborated type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
lhs_ty)
Int -> String -> Idris ()
logElab Int
5 (String
"Injective: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
fname forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
inj)
Context
ctxt <- Idris Context
getContext
(Term
clhs_c, Term
clhsty) <- if Bool -> Bool
not Bool
inf
then Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err -> Err)
-> Env
-> Term
-> Idris (Term, Term)
recheckC_borrowing Bool
False (FnOpt
PEGenerated forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts)
[] (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Term
lhs_tm
else forall (m :: * -> *) a. Monad m => a -> m a
return (Term
lhs_tm, Term
lhs_ty)
let clhs :: Term
clhs = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
clhs_c
let borrowed :: [Name]
borrowed = [Name] -> Term -> [Name]
borrowedNames [] Term
clhs
Int -> String -> Idris ()
logElab Int
3 (String
"Normalised LHS: " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls (IState -> Term -> PTerm
delabMV IState
i Term
clhs))
Bool
rep <- Idris Bool
useREPL
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
rep forall a b. (a -> b) -> a -> b
$ do
String -> Int -> PTerm -> Idris ()
addInternalApp (FC -> String
fc_fname FC
fc) (forall a b. (a, b) -> a
fst forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> (Int, Int)
fc_start forall a b. (a -> b) -> a -> b
$ FC
fc) (IState -> Term -> PTerm
delabMV IState
i Term
clhs)
IBCWrite -> Idris ()
addIBC (String -> Int -> PTerm -> IBCWrite
IBCLineApp (FC -> String
fc_fname FC
fc) (forall a b. (a, b) -> a
fst forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> (Int, Int)
fc_start forall a b. (a -> b) -> a -> b
$ FC
fc) (IState -> Term -> PTerm
delabMV IState
i Term
clhs))
Int -> String -> Idris ()
logElab Int
5 (String
"Checked " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
clhs forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
clhsty)
IState
ist <- Idris IState
getIState
Context
ctxt <- Idris Context
getContext
Int
windex <- Idris Int
getName
let decls :: [Name]
decls = forall a. Eq a => [a] -> [a]
nub (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl' PTerm -> [Name]
declared [PDecl' PTerm]
whereblock)
let defs :: [Name]
defs = forall a. Eq a => [a] -> [a]
nub ([Name]
decls forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl' PTerm -> [Name]
defined [PDecl' PTerm]
whereblock)
let newargs_all :: [(Name, PTerm)]
newargs_all = IState -> Term -> [(Name, PTerm)]
pvars IState
ist Term
lhs_tm
let uniqargs :: [Name]
uniqargs = Context -> Env -> Term -> [Name]
findUnique Context
ctxt [] Term
lhs_tm
let newargs :: [(Name, PTerm)]
newargs = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n,PTerm
_) -> Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
uniqargs) [(Name, PTerm)]
newargs_all
let winfo :: ElabInfo
winfo = (ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
pinfo ElabInfo
info [(Name, PTerm)]
newargs [Name]
defs Int
windex) { elabFC :: Maybe FC
elabFC = forall a. a -> Maybe a
Just FC
fc }
let wb :: [PDecl' PTerm]
wb = forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> PDecl' PTerm -> PDecl' PTerm
mkStatic [Name]
static_names) forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map (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) forall a b. (a -> b) -> a -> b
$
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
let ([PDecl' PTerm]
wbefore, [PDecl' PTerm]
wafter) = forall {t}. [PDecl' t] -> ([PDecl' t], [PDecl' t])
sepBlocks [PDecl' PTerm]
wb
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Where block:\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl' PTerm]
wbefore forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl' PTerm]
wafter
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl' PTerm -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
winfo) [PDecl' PTerm]
wbefore
IState
i <- Idris IState
getIState
Int -> String -> Idris ()
logElab Int
5 (PTerm -> String
showTmImpls ((Name -> Name)
-> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTerm
expandParams Name -> Name
decorate [(Name, PTerm)]
newargs [Name]
defs ([Name]
defs forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
decls) PTerm
rhs_in))
let rhs :: PTerm
rhs = ElabInfo -> PTerm -> PTerm
rhs_trans ElabInfo
info forall a b. (a -> b) -> a -> b
$
IState -> [Name] -> [Name] -> PTerm -> PTerm
addImplBoundInf IState
i (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PTerm)]
newargs_all) ([Name]
defs 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 forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
decls) PTerm
rhs_in)
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"RHS: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PTerm)]
newargs_all) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs
Context
ctxt <- Idris Context
getContext
Int -> String -> Idris ()
logElab Int
5 String
"STARTING CHECK"
((Term
rhsElab, [(Name, (Int, Maybe Name, Term, [Name]))]
defer, [Name]
holes, [PDecl' PTerm]
is, Fails
probs, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName), String
_) <-
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN Int
0 String
"patRHS") Term
clhsty EState
initEState
(do IState -> Term -> ElabD ()
pbinds IState
ist Term
lhs_tm
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall aux. Name -> Elab' aux ()
addPSname (PTerm -> [Name]
allNamesIn PTerm
lhs_in)
Bool
ulog <- forall aux. Elab' aux Bool
getUnifyLog
forall {a}. Bool -> String -> a -> a
traceWhen Bool
ulog (String
"Setting injective: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Eq a => [a] -> [a]
nub ([Name]
tcparams forall a. [a] -> [a] -> [a]
++ [Name]
inj))) forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall aux. Name -> Elab' aux ()
setinj (forall a. Eq a => [a] -> [a]
nub ([Name]
tcparams forall a. [a] -> [a] -> [a]
++ [Name]
inj))
forall aux. Elab' aux ()
setNextName
(ElabResult Term
_ [(Name, (Int, Maybe Name, Term, [Name]))]
_ [PDecl' PTerm]
is Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName) <-
forall aux a.
String -> Name -> Maybe Term -> Elab' aux a -> Elab' aux a
errAt String
"right hand side of " Name
fname (forall a. a -> Maybe a
Just Term
clhsty)
(forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> ElabD ElabResult
build IState
i ElabInfo
winfo ElabMode
ERHS FnOpts
opts Name
fname PTerm
rhs))
forall aux a.
String -> Name -> Maybe Term -> Elab' aux a -> Elab' aux a
errAt String
"right hand side of " Name
fname (forall a. a -> Maybe a
Just Term
clhsty)
(forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc forall a b. (a -> b) -> a -> b
$ forall {n} {aux}. TT n -> StateT (ElabState aux) TC ()
psolve Term
lhs_tm)
Term
tt <- forall aux. Elab' aux Term
get_term
EState
aux <- forall aux. Elab' aux aux
getAux
let (Term
tm, [(Name, (Int, Maybe Name, Term, [Name]))]
ds) = forall s a. State s a -> s -> (a, s)
runState (Maybe Name
-> [Name]
-> Context
-> Term
-> State [(Name, (Int, Maybe Name, Term, [Name]))] Term
collectDeferred (forall a. a -> Maybe a
Just Name
fname)
(forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ EState -> [(Name, PDecl' PTerm)]
case_decls EState
aux) Context
ctxt Term
tt) []
Fails
probs <- forall aux. Elab' aux Fails
get_probs
[Name]
hs <- forall aux. Elab' aux [Name]
get_holes
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, [(Name, (Int, Maybe Name, Term, [Name]))]
ds, [Name]
hs, [PDecl' PTerm]
is, Fails
probs, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName))
Context -> Idris ()
setContext Context
ctxt'
ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
(IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
inf forall a b. (a -> b) -> a -> b
$ FC -> [(Term, Term)] -> Idris ()
addTyInfConstraints FC
fc (forall a b. (a -> b) -> [a] -> [b]
map (\(Term
x,Term
y,Bool
_,Env
_,Err
_,[FailContext]
_,FailAt
_) -> (Term
x,Term
y)) Fails
probs)
Int -> String -> Idris ()
logElab Int
3 String
"DONE CHECK"
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"---> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
rhsElab
Context
ctxt <- Idris Context
getContext
let rhs' :: Term
rhs' = Term
rhsElab
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, (Int, Maybe Name, Term, [Name]))]
defer)) forall a b. (a -> b) -> a -> b
$ Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"DEFERRED " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, (Int
_,Maybe Name
_,Term
t,[Name]
_)) -> (Name
n, Term
t)) [(Name, (Int, Maybe Name, Term, [Name]))]
defer)
[(Name, (Int, Maybe Name, Term, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Term, [Name]))]
checkDef ElabInfo
info FC
fc (\Name
n -> forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"deferred type of " Name
n forall a. Maybe a
Nothing) (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
holes) [(Name, (Int, Maybe Name, Term, [Name]))]
defer
let def'' :: [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def'' = 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, forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
holes))) [(Name, (Int, Maybe Name, Term, [Name]))]
def'
[(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def''
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Name
n, (Int, Maybe Name, Term, [Name], Bool, Bool)
_) -> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)) [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def''
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, (Int, Maybe Name, Term, [Name]))]
def')) forall a b. (a -> b) -> a -> b
$ do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
defer_totcheck (forall a b. (a -> b) -> [a] -> [b]
map (\(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))
x -> (FC
fc, forall a b. (a, b) -> a
fst (Name, (Int, Maybe Name, Term, [Name], Bool, Bool))
x)) [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def'')
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl' PTerm -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
winfo) [PDecl' PTerm]
wafter
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> FnOpts -> PDecl' PTerm -> Idris ()
elabCaseBlock ElabInfo
winfo FnOpts
opts) [PDecl' PTerm]
is
Context
ctxt <- Idris Context
getContext
Int -> String -> Idris ()
logElab Int
5 String
"Rechecking"
Int -> String -> Idris ()
logElab Int
6 forall a b. (a -> b) -> a -> b
$ String
" ==> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term -> Raw
forget Term
rhs')
(Term
crhs, Term
crhsty)
<- if (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
holes Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, (Int, Maybe Name, Term, [Name]))]
def') Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
inf
then Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err -> Err)
-> Env
-> Term
-> Idris (Term, Term)
recheckC_borrowing Bool
True (FnOpt
PEGenerated forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts)
[Name]
borrowed (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Term
rhs'
else forall (m :: * -> *) a. Monad m => a -> m a
return (Term
rhs', Term
clhsty)
Int -> String -> Idris ()
logElab Int
6 forall a b. (a -> b) -> a -> b
$ String
" ==> " forall a. [a] -> [a] -> [a]
++ forall {a}.
(Show a, Eq a) =>
[(a, RigCount, Binder (TT a))] -> TT a -> String
showEnvDbg [] Term
crhsty forall a. [a] -> [a] -> [a]
++ String
" against " forall a. [a] -> [a] -> [a]
++ forall {a}.
(Show a, Eq a) =>
[(a, RigCount, Binder (TT a))] -> TT a -> String
showEnvDbg [] Term
clhsty
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
holes)) forall a b. (a -> b) -> a -> b
$ do
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Making " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
fname forall a. [a] -> [a] -> [a]
++ String
" frozen due to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
holes
Name -> Accessibility -> Idris ()
setAccessibility Name
fname Accessibility
Frozen
Context
ctxt <- Idris Context
getContext
let constv :: Int
constv = Context -> Int
next_tvar Context
ctxt
Bool
tit <- Idris Bool
typeInType
case forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LState.runStateT (Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC Context
ctxt [] Term
crhsty Term
clhsty) (Int
constv, []) of
OK (()
_, UCs
cs) -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
PEGenerated forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
tit) forall a b. (a -> b) -> a -> b
$ do
FC -> UCs -> Idris ()
addConstraints FC
fc UCs
cs
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)) (forall a b. (a, b) -> b
snd UCs
cs)
Int -> String -> Idris ()
logElab Int
6 forall a b. (a -> b) -> a -> b
$ String
"CONSTRAINTS ADDED: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UCs
cs forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term
clhsty, Term
crhsty)
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Error Err
e -> forall a. Err -> Idris a
ierror (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (Term
clhsty, forall a. Maybe a
Nothing) (Term
crhsty, forall a. Maybe a
Nothing) Err
e [] Int
0))
IState
i <- Idris IState
getIState
FC -> PTerm -> PTerm -> Idris ()
checkInferred FC
fc (IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
crhs Bool
True Bool
True) PTerm
rhs
let (Term
ret_fam, [Term]
_) = forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
getRetTy Term
crhsty)
Bool
rev <- case Term
ret_fam of
P NameType
_ Name
rfamn Term
_ ->
case 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
_] ->
forall (m :: * -> *) a. Monad m => a -> m a
return (DataOpt
DataErrRev forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` DataOpts
dopts Bool -> Bool -> Bool
&&
forall a. Sized a => a -> Int
size Term
clhs forall a. Ord a => a -> a -> Bool
<= forall a. Sized a => a -> Int
size Term
crhs)
[TypeInfo]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
rev Bool -> Bool -> Bool
|| FnOpt
ErrorReverse forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) forall a b. (a -> b) -> a -> b
$ do
IBCWrite -> Idris ()
addIBC ((Term, Term) -> IBCWrite
IBCErrRev (Term
crhs, Term
clhs))
(Term, Term) -> Idris ()
addErrRev (Term
crhs, Term
clhs)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
rev Bool -> Bool -> Bool
|| FnOpt
ErrorReduce forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) forall a b. (a -> b) -> a -> b
$ do
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCErrReduce Name
fname)
Name -> Idris ()
addErrReduce Name
fname
Idris ()
pop_estack
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Term
clhs, Term
crhs), PTerm
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 forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ns
dsParams :: [(Name, [Name])]
dsParams = forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PTerm)]
newps)) [Name]
ds
newb :: Ctxt [Name]
newb = forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, [Name])]
dsParams (ElabInfo -> Ctxt [Name]
inblock ElabInfo
info) in
ElabInfo
info { params :: [(Name, PTerm)]
params = [(Name, PTerm)]
newps,
inblock :: Ctxt [Name]
inblock = Ctxt [Name]
newb,
liftname :: Name -> Name
liftname = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
}
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 forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Ownership" Bool -> Bool -> Bool
&&
(Text
lend forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"lend" Bool -> Bool -> Bool
|| Text
lend forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Read") = forall {n}. TT n -> [Name]
getVs Term
arg
where
getVs :: TT n -> [Name]
getVs (V Int
i) = [[Name]
envforall a. [a] -> Int -> a
!!Int
i]
getVs (App AppStatus n
_ TT n
f TT n
a) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ TT n -> [Name]
getVs TT n
f 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) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ [Name] -> Term -> [Name]
borrowedNames [Name]
env Term
f forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [Name]
borrowedNames [Name]
env Term
a
borrowedNames [Name]
env (Bind Name
n Binder Term
b Term
sc) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Binder Term -> [Name]
borrowedB Binder Term
b forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [Name]
borrowedNames (Name
nforall a. a -> [a] -> [a]
:[Name]
env) Term
sc
where borrowedB :: Binder Term -> [Name]
borrowedB (Let RigCount
_ Term
t Term
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ [Name] -> Term -> [Name]
borrowedNames [Name]
env Term
t forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [Name]
borrowedNames [Name]
env Term
v
borrowedB Binder Term
b = [Name] -> Term -> [Name]
borrowedNames [Name]
env (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 = 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 forall a. a -> [a] -> [a]
: [Name]
ns) [PDecl' t]
bs in
(PDecl' t
d 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 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 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 forall a. a -> [a] -> [a]
: [PDecl' t]
bf, [PDecl' t]
af)
sepBlocks' [Name]
ns [] = ([], [])
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 Context
ctxt <- Idris Context
getContext
IState
i <- Idris IState
getIState
let fn_ty :: Term
fn_ty = case Name -> Context -> [Term]
lookupTy Name
fname Context
ctxt of
[Term
t] -> Term
t
[Term]
_ -> forall a. HasCallStack => String -> a
error String
"Can't happen (elabClause function type)"
let fn_is :: [PArg]
fn_is = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
fname (IState -> Ctxt [PArg]
idris_implicits IState
i) of
[[PArg]
t] -> [PArg]
t
[[PArg]]
_ -> []
let params :: [Name]
params = IState -> [Name] -> [PArg] -> Term -> [Name]
getParamsInType IState
i [] [PArg]
fn_is (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
fn_ty)
let lhs :: PTerm
lhs = IState -> PTerm -> PTerm
stripLinear IState
i forall a b. (a -> b) -> a -> b
$ IState -> PTerm -> PTerm
stripUnmatchable IState
i 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)
Int -> String -> Idris ()
logElab Int
2 (String
"LHS: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
lhs)
(ElabResult Term
lhs' [(Name, (Int, Maybe Name, Term, [Name]))]
dlhs [] Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName, String
_) <-
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN Int
0 String
"patLHS") Term
infP EState
initEState
(forall aux a.
String -> Name -> Maybe Term -> Elab' aux a -> Elab' aux a
errAt String
"left hand side of with in " Name
fname forall a. Maybe a
Nothing
(forall aux a. FC -> Elab' aux a -> Elab' aux a
erun (forall a. a -> Maybe a -> a
fromMaybe FC
NoFC forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe FC
highestFC PTerm
lhs_in)
(IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> [Name]
-> PTerm
-> ElabD ElabResult
buildTC IState
i ElabInfo
info ElabMode
ELHS FnOpts
opts Name
fname
(PTerm -> [Name]
allNamesIn PTerm
lhs_in)
(PTerm -> PTerm
infTerm PTerm
lhs))) )
Context -> Idris ()
setContext Context
ctxt'
ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
(IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
Context
ctxt <- Idris Context
getContext
let lhs_tm :: Term
lhs_tm = Term -> Term
orderPats (Term -> Term
getInferTerm Term
lhs')
let lhs_ty :: Term
lhs_ty = Term -> Term
getInferType Term
lhs'
let ret_ty :: Term
ret_ty = forall n. TT n -> TT n
getRetTy (forall n. TT n -> TT n
explicitNames (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
lhs_ty))
let static_names :: [Name]
static_names = IState -> Term -> [Name]
getStaticNames IState
i Term
lhs_tm
Int -> String -> Idris ()
logElab Int
5 (forall a. Show a => a -> String
show Term
lhs_tm forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
static_names)
(Term
clhs_c, Term
clhsty) <- String -> FC -> (Err -> Err) -> Env -> Term -> Idris (Term, Term)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Term
lhs_tm
let clhs :: Term
clhs = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
clhs_c
Int -> String -> Idris ()
logElab Int
5 (String
"Checked " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
clhs)
let bargs :: [(Name, Term)]
bargs = forall n. TT n -> [(n, TT n)]
getPBtys (forall n. TT n -> TT n
explicitNames (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
lhs_tm))
PTerm
wval <- case PTerm
wval_in of
PTerm
Placeholder -> forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc forall a b. (a -> b) -> a -> b
$
forall t. String -> Err' t
Msg String
"No expression for the with block to inspect.\nYou need to replace the _ with an expression."
PTerm
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
ElabInfo -> PTerm -> PTerm
rhs_trans ElabInfo
info forall a b. (a -> b) -> a -> b
$
IState -> [Name] -> PTerm -> PTerm
addImplBound IState
i (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
bargs) PTerm
wval_in
Int -> String -> Idris ()
logElab Int
5 (String
"Checking " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
wval)
((Term
wvalElab, [(Name, (Int, Maybe Name, Term, [Name]))]
defer, [PDecl' PTerm]
is, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName), String
_) <-
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN Int
0 String
"withRHS")
(forall n. (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
bindTyArgs forall b. b -> Binder b
PVTy [(Name, Term)]
bargs Term
infP) EState
initEState
(do IState -> Term -> ElabD ()
pbinds IState
i Term
lhs_tm
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall aux. Name -> Elab' aux ()
addPSname (PTerm -> [Name]
allNamesIn PTerm
lhs_in)
forall aux. Elab' aux ()
setNextName
(ElabResult Term
_ [(Name, (Int, Maybe Name, Term, [Name]))]
d [PDecl' PTerm]
is Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName) <- forall aux a.
String -> Name -> Maybe Term -> Elab' aux a -> Elab' aux a
errAt String
"with value in " Name
fname forall a. Maybe a
Nothing
(forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> ElabD ElabResult
build IState
i ElabInfo
info ElabMode
ERHS FnOpts
opts Name
fname (PTerm -> PTerm
infTerm PTerm
wval)))
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc forall a b. (a -> b) -> a -> b
$ forall {n} {aux}. TT n -> StateT (ElabState aux) TC ()
psolve Term
lhs_tm
Term
tt <- forall aux. Elab' aux Term
get_term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tt, [(Name, (Int, Maybe Name, Term, [Name]))]
d, [PDecl' PTerm]
is, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName))
Context -> Idris ()
setContext Context
ctxt'
ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
(IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
[(Name, (Int, Maybe Name, Term, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Term, [Name]))]
checkDef ElabInfo
info FC
fc Name -> Err -> Err
iderr Bool
True [(Name, (Int, Maybe Name, Term, [Name]))]
defer
let def'' :: [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def'' = 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'
[(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def''
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> FnOpts -> PDecl' PTerm -> Idris ()
elabCaseBlock ElabInfo
info FnOpts
opts) [PDecl' PTerm]
is
let wval' :: Term
wval' = Term
wvalElab
Int -> String -> Idris ()
logElab Int
5 (String
"Checked wval " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
wval')
Context
ctxt <- Idris Context
getContext
(Term
cwval, Term
cwvalty) <- String -> FC -> (Err -> Err) -> Env -> Term -> Idris (Term, Term)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] (Term -> Term
getInferTerm Term
wval')
let cwvaltyN :: Term
cwvaltyN = forall n. TT n -> TT n
explicitNames (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
cwvalty)
let cwvalN :: Term
cwvalN = forall n. TT n -> TT n
explicitNames (Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
cwval)
Int -> String -> Idris ()
logElab Int
3 (String
"With type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
cwvalty forall a. [a] -> [a] -> [a]
++ String
"\nRet type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
ret_ty)
case forall n. TT n -> [(n, TT n)]
getArgTys Term
cwvaltyN of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
((Name, Term)
_:[(Name, Term)]
_) -> forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. t -> Err' t
WithFnType Term
cwvalty)
let pvars :: [Name]
pvars = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall n. TT n -> [(n, TT n)]
getPBtys Term
cwvalty)
let pdeps :: [Name]
pdeps = [Name] -> IState -> PTerm -> [Name]
usedNamesIn [Name]
pvars IState
i (IState -> Term -> PTerm
delab IState
i Term
cwvalty)
let ([(Name, Term)]
bargs_pre, [(Name, Term)]
bargs_post) = forall {a} {b}.
Eq a =>
[a] -> [(a, b)] -> [(a, b)] -> ([(a, b)], [(a, b)])
split [Name]
pdeps [(Name, Term)]
bargs []
let mpn :: Maybe Name
mpn = case Maybe (Name, FC)
pn_in of
Maybe (Name, FC)
Nothing -> forall a. Maybe a
Nothing
Just (Name
n, FC
nfc) -> forall a. a -> Maybe a
Just (Name -> [Name] -> Name
uniqueName Name
n (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
bargs))
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList [(FC -> FC'
FC' FC
fc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
n Bool
False) | (Name
n, FC
fc) <- forall a. Maybe a -> [a]
maybeToList Maybe (Name, FC)
pn_in]
Int -> String -> Idris ()
logElab Int
10 (String
"With type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall n. TT n -> TT n
getRetTy Term
cwvaltyN) forall a. [a] -> [a] -> [a]
++
String
" depends on " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
pdeps forall a. [a] -> [a] -> [a]
++ String
" from " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
pvars)
Int -> String -> Idris ()
logElab Int
10 (String
"Pre " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Term)]
bargs_pre forall a. [a] -> [a] -> [a]
++ String
"\nPost " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Term)]
bargs_post)
Int
windex <- Idris Int
getName
let wargval :: Term
wargval = forall n. TT n -> TT n
getRetTy Term
cwvalN
let wargtype :: Term
wargtype = forall n. TT n -> TT n
getRetTy Term
cwvaltyN
let wargname :: Name
wargname = Int -> String -> Name
sMN Int
windex String
"warg"
Int -> String -> Idris ()
logElab Int
5 (String
"Abstract over " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
wargval forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
wargtype)
let wtype :: Term
wtype = forall n. (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
bindTyArgs (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) ([(Name, Term)]
bargs_pre forall a. [a] -> [a] -> [a]
++
(Name
wargname, Term
wargtype) forall a. a -> [a] -> [a]
:
forall a b. (a -> b) -> [a] -> [b]
map (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 forall a. [a] -> [a] -> [a]
++
case Maybe Name
mpn of
Just Name
pn -> [(Name
pn, forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
eqTy forall n. TT n
Erased)
[Term
wargtype, Term
wargtype,
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
wargname forall n. TT n
Erased, Term
wargval])]
Maybe Name
Nothing -> [])
(forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm Term
wargval (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
wargname Term
wargtype) Term
ret_ty)
Int -> String -> Idris ()
logElab Int
3 (String
"New function type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
wtype)
let wname :: Name
wname = SpecialName -> Name
SN (Int -> Name -> SpecialName
WithN Int
windex Name
fname)
let imps :: [PArg]
imps = forall {n}. TT n -> [PArg]
getImps Term
wtype
IState -> Idris ()
putIState (IState
i { idris_implicits :: Ctxt [PArg]
idris_implicits = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
wname [PArg]
imps (IState -> Ctxt [PArg]
idris_implicits IState
i) })
let statics :: [Bool]
statics = [Name] -> Term -> [Bool]
getStatics [Name]
static_names Term
wtype
Int -> String -> Idris ()
logElab Int
5 (String
"Static positions " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Bool]
statics)
IState
i <- Idris IState
getIState
IState -> Idris ()
putIState (IState
i { idris_statics :: Ctxt [Bool]
idris_statics = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
wname [Bool]
statics (IState -> Ctxt [Bool]
idris_statics IState
i) })
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
wname)
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCImp Name
wname)
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCStatic Name
wname)
[(Name, (Int, Maybe Name, Term, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Term, [Name]))]
checkDef ElabInfo
info FC
fc Name -> Err -> Err
iderr Bool
True [(Name
wname, (-Int
1, forall a. Maybe a
Nothing, Term
wtype, []))]
let def'' :: [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def'' = 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'
[(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def''
[PDecl' PTerm]
wb <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PDecl' PTerm
-> StateT IState (ExceptT Err IO) (PDecl' PTerm)
mkAuxC Maybe Name
mpn Name
wname PTerm
lhs (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
bargs_pre) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
bargs_post))
[PDecl' PTerm]
withblock
Int -> String -> Idris ()
logElab Int
3 (String
"with block " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl' PTerm]
wb)
Name -> FnOpts -> Idris ()
setFlags Name
wname [FnOpt
Inlinable]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
AssertTotal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) forall a b. (a -> b) -> a -> b
$
Name -> FnOpts -> Idris ()
setFlags Name
wname [FnOpt
Inlinable, FnOpt
AssertTotal]
IState
i <- Idris IState
getIState
let rhstrans' :: PTerm -> PTerm
rhstrans' = IState
-> Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PTerm
-> PTerm
updateWithTerm IState
i Maybe Name
mpn Name
wname PTerm
lhs (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
bargs_pre) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst ([(Name, Term)]
bargs_post))
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
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl' PTerm -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll (ElabInfo
info { rhs_trans :: PTerm -> PTerm
rhs_trans = PTerm -> PTerm
rhstrans' })) [PDecl' PTerm]
wb
let rhs :: PTerm
rhs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
wname)
(forall a b. (a -> b) -> [a] -> [b]
map (forall {t}. t -> PArg' t
pexp 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 []) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> a
fst) [(Name, Term)]
bargs_pre forall a. [a] -> [a] -> [a]
++
forall {t}. t -> PArg' t
pexp PTerm
wval forall a. a -> [a] -> [a]
:
(forall a b. (a -> b) -> [a] -> [b]
map (forall {t}. t -> PArg' t
pexp 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 []) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> a
fst) [(Name, Term)]
bargs_post) forall a. [a] -> [a] -> [a]
++
case Maybe Name
mpn of
Maybe Name
Nothing -> []
Just Name
_ -> [forall {t}. t -> PArg' t
pexp (FC -> PTerm -> [PArg] -> PTerm
PApp FC
NoFC (FC -> [FC] -> Name -> PTerm
PRef FC
NoFC [] Name
eqCon)
[ forall {t}. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN String
"A") PTerm
Placeholder Bool
False
, forall {t}. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN String
"x") PTerm
Placeholder Bool
False
])])
Int -> String -> Idris ()
logElab Int
5 (String
"New RHS " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs)
Context
ctxt <- Idris Context
getContext
IState
i <- Idris IState
getIState
((Term
rhsElab, [(Name, (Int, Maybe Name, Term, [Name]))]
defer, [PDecl' PTerm]
is, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName), String
_) <-
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN Int
0 String
"wpatRHS") Term
clhsty EState
initEState
(do IState -> Term -> ElabD ()
pbinds IState
i Term
lhs_tm
forall aux. Elab' aux ()
setNextName
(ElabResult Term
_ [(Name, (Int, Maybe Name, Term, [Name]))]
d [PDecl' PTerm]
is Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName) <-
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> ElabD ElabResult
build IState
i ElabInfo
info ElabMode
ERHS FnOpts
opts Name
fname PTerm
rhs)
forall {n} {aux}. TT n -> StateT (ElabState aux) TC ()
psolve Term
lhs_tm
Term
tt <- forall aux. Elab' aux Term
get_term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tt, [(Name, (Int, Maybe Name, Term, [Name]))]
d, [PDecl' PTerm]
is, Context
ctxt', [RDeclInstructions]
newDecls, Set (FC', OutputAnnotation)
highlights, Int
newGName))
Context -> Idris ()
setContext Context
ctxt'
ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
(IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
Context
ctxt <- Idris Context
getContext
let rhs' :: Term
rhs' = Term
rhsElab
[(Name, (Int, Maybe Name, Term, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Term, [Name]))]
checkDef ElabInfo
info FC
fc Name -> Err -> Err
iderr Bool
True [(Name, (Int, Maybe Name, Term, [Name]))]
defer
let def'' :: [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def'' = 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'
[(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def''
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> FnOpts -> PDecl' PTerm -> Idris ()
elabCaseBlock ElabInfo
info FnOpts
opts) [PDecl' PTerm]
is
Int -> String -> Idris ()
logElab Int
5 (String
"Checked RHS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
rhs')
(Term
crhs, Term
crhsty) <- String -> FC -> (Err -> Err) -> Env -> Term -> Idris (Term, Term)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Term
rhs'
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Term
clhs, Term
crhs), PTerm
lhs)
where
getImps :: TT n -> [PArg]
getImps (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
_ TT n
_) TT n
t) = forall {t}. t -> PArg' t
pexp PTerm
Placeholder 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 [PClause]
cs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PClause
-> StateT IState (ExceptT Err IO) PClause
mkAux Maybe Name
pn Name
wname PTerm
lhs [Name]
ns [Name]
ns') [PClause]
cs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
o Name
wname [PClause]
cs'
mkAuxC Maybe Name
pn Name
wname PTerm
lhs [Name]
ns [Name]
ns' PDecl' PTerm
d = 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 IState
i <- Idris IState
getIState
let tm :: PTerm
tm = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
tm_in
Int -> String -> Idris ()
logElab Int
2 (String
"Matching " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
tm forall a. [a] -> [a] -> [a]
++ String
" against " forall a. [a] -> [a] -> [a]
++
PTerm -> String
showTmImpls PTerm
toplhs)
case IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause IState
i PTerm
toplhs PTerm
tm of
Left (PTerm
a,PTerm
b) -> forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show FC
fc 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 : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, PTerm)]
mvars)
PTerm
lhs <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
wname PTerm
lhs [PTerm]
ws PTerm
rhs [PDecl' PTerm]
wheres
mkAux 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 IState
i <- Idris IState
getIState
let tm :: PTerm
tm = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
tm_in
Int -> String -> Idris ()
logElab Int
2 (String
"Matching " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
tm forall a. [a] -> [a] -> [a]
++ String
" against " forall a. [a] -> [a] -> [a]
++
PTerm -> String
showTmImpls PTerm
toplhs)
[PDecl' PTerm]
withs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Name
-> Name
-> PTerm
-> [Name]
-> [Name]
-> PDecl' PTerm
-> StateT IState (ExceptT Err IO) (PDecl' PTerm)
mkAuxC Maybe Name
pn Name
wname PTerm
toplhs [Name]
ns [Name]
ns') [PDecl' PTerm]
withs
case IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause IState
i PTerm
toplhs PTerm
tm of
Left (PTerm
a,PTerm
b) -> forall a. String -> a -> a
trace (String
"matchClause: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
a forall a. [a] -> [a] -> [a]
++ String
" =/= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
b) (forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++ String
"with clause does not match top level")
Right [(Name, PTerm)]
mvars ->
do PTerm
lhs <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc Name
wname PTerm
lhs [PTerm]
ws PTerm
wval Maybe (Name, FC)
pn' [PDecl' PTerm]
withs'
mkAux Maybe Name
pn Name
wname PTerm
toplhs [Name]
ns [Name]
ns' PClause
c
= forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++ String
":badly formed with clause"
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 = forall a b. (a -> b) -> [a] -> [b]
map (forall {t :: * -> *}. Foldable t => t Name -> FC -> Name -> PTerm
keepMvar (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PTerm)]
mvars) FC
fc') [Name]
ns_in
ns' :: [PTerm]
ns' = forall a b. (a -> b) -> [a] -> [b]
map (forall {t :: * -> *}. Foldable t => t Name -> FC -> Name -> PTerm
keepMvar (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PTerm)]
mvars) FC
fc') [Name]
ns_in' in
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(Name, PTerm)] -> PTerm -> PTerm
substMatches [(Name, PTerm)]
mvars forall a b. (a -> b) -> a -> b
$
FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc' [] Name
wname)
(forall a b. (a -> b) -> [a] -> [b]
map forall {t}. t -> PArg' t
pexp [PTerm]
ns forall a. [a] -> [a] -> [a]
++ forall {t}. t -> PArg' t
pexp PTerm
w forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map forall {t}. t -> PArg' t
pexp [PTerm]
ns') forall a. [a] -> [a] -> [a]
++
case Maybe Name
pn of
Maybe Name
Nothing -> []
Just Name
pnm -> [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
keepMvar :: t Name -> FC -> Name -> PTerm
keepMvar t Name
mvs FC
fc Name
v | Name
v 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 forall a. Eq a => a -> a -> Bool
== Name
fname = forall a. a -> Maybe a
Just PTerm
tm
getApp (PTerm
_ : [PTerm]
as) = [PTerm] -> Maybe PTerm
getApp [PTerm]
as
getApp [] = 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 (forall t. String -> Err' t
Msg (forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++ String
":with application does not match top level "))
Right [(Name, PTerm)]
mvars ->
let ns :: [PTerm]
ns = forall a b. (a -> b) -> [a] -> [b]
map (forall {t :: * -> *}. Foldable t => t Name -> FC -> Name -> PTerm
keepMvar (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PTerm)]
mvars) FC
fcw) [Name]
ns_in
ns' :: [PTerm]
ns' = forall a b. (a -> b) -> [a] -> [b]
map (forall {t :: * -> *}. Foldable t => t Name -> FC -> Name -> PTerm
keepMvar (forall a b. (a -> b) -> [a] -> [b]
map 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 forall a b. (a -> b) -> a -> b
$
FC -> PTerm -> [PArg] -> PTerm
PApp FC
fcw (FC -> [FC] -> Name -> PTerm
PRef FC
fcw [] Name
wname)
(forall a b. (a -> b) -> [a] -> [b]
map forall {t}. t -> PArg' t
pexp [PTerm]
ns forall a. [a] -> [a] -> [a]
++ forall {t}. t -> PArg' t
pexp PTerm
warg forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map forall {t}. t -> PArg' t
pexp [PTerm]
ns') forall a. [a] -> [a] -> [a]
++
case Maybe Name
pn of
Maybe Name
Nothing -> []
Just Name
pnm -> [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
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
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]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ty,
forall t. PArg' t -> t
getTm PArg
a forall a. Eq a => a -> a -> Bool
== PTerm
Placeholder
= case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
cn (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
Just InterfaceInfo
_ -> PArg
a { getTm :: PTerm
getTm = FC -> PTerm
PResolveTC FC
fc } forall a. a -> [a] -> [a]
: FC -> Term -> [PArg] -> [PArg]
addResolvesArgs FC
fc Term
sc [PArg]
args
Maybe InterfaceInfo
Nothing -> PArg
a 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 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 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 = (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 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 forall a. Eq a => [a] -> [a] -> [a]
\\ [a
n]) [(a, b)]
rest ((a
n, b
ty) 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) forall a. a -> [a] -> [a]
: [(a, b)]
pre)
split [a]
deps [] [(a, b)]
pre = (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, forall n. Eq n => TT n -> TT n -> TT n -> TT n
substTerm TT n
wv (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
wn TT n
wty) TT n
argty)
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)
= 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) (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)
= 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 (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)
= forall t. FC -> [t] -> t -> [PDecl' t] -> PClause' t
PClauseR FC
fc [PTerm]
args (PTerm -> PTerm
f PTerm
rhs) (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)
= 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 (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)
= forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
opt Name
n (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