mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 03:34:13 +03:00
Merge remote-tracking branch 'refs/remotes/upstream/master' into library-reorg
Conflicts: CHANGELOG libs/prelude/Prelude/Applicative.idr libs/prelude/Prelude/Functor.idr libs/prelude/Prelude/Monad.idr
This commit is contained in:
David Raymond Christiansen
commit
5ddd0244be
@ -43,6 +43,8 @@ New in 0.9.17:
|
||||
* New package 'contrib' containing things that are less mature or less used
|
||||
than the contents of 'base'. 'contrib' is not available by default, so you
|
||||
may need to add '-p contrib' to your .ipkg file or Idris command line.
|
||||
* Arguments to class instances are now checked for injectivity.
|
||||
Unification assumes this, so we need to check when instances are defined.
|
||||
|
||||
New in 0.9.16:
|
||||
--------------
|
||||
|
||||
@ -270,6 +270,7 @@ instance Show Err where
|
||||
show (NoTypeDecl n) = "NoTypeDecl " ++ show n
|
||||
show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'
|
||||
show (CantResolve tm) = "CantResolve " ++ show tm
|
||||
show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"
|
||||
show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
|
||||
show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
|
||||
show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm
|
||||
|
||||
@ -29,6 +29,7 @@ data Err = Msg String
|
||||
| NoTypeDecl TTName
|
||||
| NotInjective TT TT TT
|
||||
| CantResolve TT
|
||||
| InvalidTCArg TTName TT
|
||||
| CantResolveAlts (List TTName)
|
||||
| IncompleteTerm TT
|
||||
| NoEliminator String TT
|
||||
|
||||
@ -15,10 +15,6 @@ class Functor f => Applicative (f : Type -> Type) where
|
||||
pure : a -> f a
|
||||
(<*>) : f (a -> b) -> f a -> f b
|
||||
|
||||
instance Applicative id where
|
||||
pure a = a
|
||||
f <*> a = f a
|
||||
|
||||
infixl 2 <*
|
||||
(<*) : Applicative f => f a -> f b -> f a
|
||||
a <* b = map const a <*> b
|
||||
|
||||
@ -18,5 +18,3 @@ infixl 4 <$>
|
||||
(<$>) : Functor f => (m : a -> b) -> f a -> f b
|
||||
m <$> x = map m x
|
||||
|
||||
instance Functor id where
|
||||
map f a = f a
|
||||
|
||||
@ -14,9 +14,6 @@ infixl 5 >>=
|
||||
class Applicative m => Monad (m : Type -> Type) where
|
||||
(>>=) : m a -> (a -> m b) -> m b
|
||||
|
||||
instance Monad id where
|
||||
a >>= f = f a
|
||||
|
||||
||| Also called `join` or mu
|
||||
flatten : Monad m => m (m a) -> m a
|
||||
flatten a = a >>= id
|
||||
|
||||
@ -112,19 +112,8 @@ void idris_gc(VM* vm) {
|
||||
if (vm->heap.old != NULL)
|
||||
free(vm->heap.old);
|
||||
|
||||
char* newheap = malloc(vm->heap.size);
|
||||
char* oldheap = vm->heap.heap;
|
||||
|
||||
vm->heap.heap = newheap;
|
||||
#ifdef FORCE_ALIGNMENT
|
||||
if (((i_int)(vm->heap.heap)&1) == 1) {
|
||||
vm->heap.next = newheap + 1;
|
||||
} else
|
||||
#endif
|
||||
{
|
||||
vm->heap.next = newheap;
|
||||
}
|
||||
vm->heap.end = newheap + vm->heap.size;
|
||||
/* Allocate swap heap. */
|
||||
alloc_heap(&vm->heap, vm->heap.size, vm->heap.growth, vm->heap.heap);
|
||||
|
||||
VAL* root;
|
||||
|
||||
@ -139,6 +128,7 @@ void idris_gc(VM* vm) {
|
||||
msg->msg = copy(vm, msg->msg);
|
||||
}
|
||||
#endif
|
||||
|
||||
vm->ret = copy(vm, vm->ret);
|
||||
vm->reg1 = copy(vm, vm->reg1);
|
||||
|
||||
@ -150,7 +140,6 @@ void idris_gc(VM* vm) {
|
||||
if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) {
|
||||
vm->heap.size += vm->heap.growth;
|
||||
}
|
||||
vm->heap.old = oldheap;
|
||||
|
||||
STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)
|
||||
HEAP_CHECK(vm)
|
||||
|
||||
@ -5,7 +5,9 @@
|
||||
#include <stddef.h>
|
||||
#include <stdio.h>
|
||||
|
||||
void alloc_heap(Heap * h, size_t heap_size)
|
||||
|
||||
/* Used for initializing the heap. */
|
||||
void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)
|
||||
{
|
||||
char * mem = malloc(heap_size);
|
||||
if (mem == NULL) {
|
||||
@ -27,9 +29,9 @@ void alloc_heap(Heap * h, size_t heap_size)
|
||||
h->end = h->heap + heap_size;
|
||||
|
||||
h->size = heap_size;
|
||||
h->growth = heap_size;
|
||||
h->growth = growth;
|
||||
|
||||
h->old = NULL;
|
||||
h->old = old;
|
||||
}
|
||||
|
||||
void free_heap(Heap * h) {
|
||||
@ -40,6 +42,7 @@ void free_heap(Heap * h) {
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// TODO: more testing
|
||||
/******************** Heap testing ********************************************/
|
||||
void heap_check_underflow(Heap * heap) {
|
||||
|
||||
@ -14,7 +14,7 @@ typedef struct {
|
||||
} Heap;
|
||||
|
||||
|
||||
void alloc_heap(Heap * heap, size_t heap_size);
|
||||
void alloc_heap(Heap * heap, size_t heap_size, size_t growth, char * old);
|
||||
void free_heap(Heap * heap);
|
||||
|
||||
|
||||
|
||||
@ -29,7 +29,7 @@ VM* init_vm(int stack_size, size_t heap_size,
|
||||
vm->valstack_base = valstack;
|
||||
vm->stack_max = valstack + stack_size;
|
||||
|
||||
alloc_heap(&(vm->heap), heap_size);
|
||||
alloc_heap(&(vm->heap), heap_size, heap_size, NULL);
|
||||
|
||||
vm->ret = NULL;
|
||||
vm->reg1 = NULL;
|
||||
|
||||
@ -149,6 +149,9 @@ instance Binary a => Binary (Err' a) where
|
||||
put (NoEliminator s t) = do putWord8 37
|
||||
put s
|
||||
put t
|
||||
put (InvalidTCArg n t) = do putWord8 38
|
||||
put n
|
||||
put t
|
||||
|
||||
get = do i <- getWord8
|
||||
case i of
|
||||
@ -211,6 +214,9 @@ instance Binary a => Binary (Err' a) where
|
||||
37 -> do x1 <- get
|
||||
x2 <- get
|
||||
return (NoEliminator x1 x2)
|
||||
38 -> do x1 <- get
|
||||
x2 <- get
|
||||
return (InvalidTCArg x1 x2)
|
||||
_ -> error "Corrupted binary data for Err'"
|
||||
----- Generated by 'derive'
|
||||
|
||||
|
||||
@ -81,6 +81,7 @@ instance NFData Err where
|
||||
rnf (NotInjective x1 x2 x3)
|
||||
= rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
|
||||
rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (CantResolveAlts x1) = rnf x1 `seq` ()
|
||||
rnf (IncompleteTerm x1) = rnf x1 `seq` ()
|
||||
rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
|
||||
@ -157,6 +157,7 @@ data Err' t
|
||||
| NotInjective t t t
|
||||
| CantResolve Bool -- True if postponed, False if fatal
|
||||
t
|
||||
| InvalidTCArg Name t
|
||||
| CantResolveAlts [Name]
|
||||
| IncompleteTerm t
|
||||
| NoEliminator String t
|
||||
@ -1170,17 +1171,33 @@ unList tm = case unApply tm of
|
||||
forget :: TT Name -> Raw
|
||||
forget tm = forgetEnv [] tm
|
||||
|
||||
safeForget :: TT Name -> Maybe Raw
|
||||
safeForget tm = safeForgetEnv [] tm
|
||||
|
||||
forgetEnv :: [Name] -> TT Name -> Raw
|
||||
forgetEnv env (P _ n _) = Var n
|
||||
forgetEnv env (V i) = Var (env !! i)
|
||||
forgetEnv env (Bind n b sc) = let n' = uniqueName n env in
|
||||
RBind n' (fmap (forgetEnv env) b)
|
||||
(forgetEnv (n':env) sc)
|
||||
forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)
|
||||
forgetEnv env (Constant c) = RConstant c
|
||||
forgetEnv env (TType i) = RType
|
||||
forgetEnv env (UType u) = RUType u
|
||||
forgetEnv env Erased = RConstant Forgot
|
||||
forgetEnv env tm = case safeForgetEnv env tm of
|
||||
Just t' -> t'
|
||||
Nothing -> error $ "Scope error in " ++ show tm
|
||||
|
||||
|
||||
safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
|
||||
safeForgetEnv env (P _ n _) = Just $ Var n
|
||||
safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)
|
||||
| otherwise = Nothing
|
||||
safeForgetEnv env (Bind n b sc)
|
||||
= do let n' = uniqueName n env
|
||||
b' <- safeForgetEnvB env b
|
||||
sc' <- safeForgetEnv (n':env) sc
|
||||
Just $ RBind n' b' sc'
|
||||
where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)
|
||||
(safeForgetEnv env v)
|
||||
safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
|
||||
Just $ fmap (\_ -> ty') b
|
||||
safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
|
||||
safeForgetEnv env (Constant c) = Just $ RConstant c
|
||||
safeForgetEnv env (TType i) = Just RType
|
||||
safeForgetEnv env (UType u) = Just $ RUType u
|
||||
safeForgetEnv env Erased = Just $ RConstant Forgot
|
||||
|
||||
-- | Introduce a 'Bind' into the given term for each element of the
|
||||
-- given list of (name, binder) pairs.
|
||||
|
||||
@ -290,6 +290,10 @@ pprintErr' i (NotInjective p x y) =
|
||||
text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>
|
||||
annTm y (pprintTerm i (delab i y))
|
||||
pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
|
||||
pprintErr' i (InvalidTCArg n t)
|
||||
= annTm t (pprintTerm i (delab i t)) <+> text " cannot be a parameter of "
|
||||
<> annName n <$>
|
||||
text "(Type class arguments must be injective)"
|
||||
pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
|
||||
align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))
|
||||
pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
|
||||
|
||||
@ -603,7 +603,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
|
||||
-- If we're inferring metavariables in the type, don't recheck,
|
||||
-- because we're only doing this to try to work out those metavariables
|
||||
(clhs_c, clhsty) <- if not inf
|
||||
then recheckC fc [] lhs_tm
|
||||
then recheckC fc id [] lhs_tm
|
||||
else return (lhs_tm, lhs_ty)
|
||||
let clhs = normalise ctxt [] clhs_c
|
||||
let borrowed = borrowedNames [] clhs
|
||||
@ -681,7 +681,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
|
||||
logLvl 4 $ "---> " ++ show rhs'
|
||||
when (not (null defer)) $ iLOG $ "DEFERRED " ++
|
||||
show (map (\ (n, (_,_,t)) -> (n, t)) defer)
|
||||
def' <- checkDef fc defer
|
||||
def' <- checkDef fc (Elaborating "deferred type of ") defer
|
||||
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
|
||||
addDeferred def''
|
||||
mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
|
||||
@ -700,7 +700,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
|
||||
logLvl 6 $ " ==> " ++ show (forget rhs')
|
||||
|
||||
(crhs, crhsty) <- if not inf
|
||||
then recheckC_borrowing True borrowed fc [] rhs'
|
||||
then recheckC_borrowing True borrowed fc id [] rhs'
|
||||
else return (rhs', clhsty)
|
||||
logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
|
||||
ctxt <- getContext
|
||||
@ -828,7 +828,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
|
||||
let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
|
||||
let static_names = getStaticNames i lhs_tm
|
||||
logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)
|
||||
(clhs, clhsty) <- recheckC fc [] lhs_tm
|
||||
(clhs, clhsty) <- recheckC fc id [] lhs_tm
|
||||
logLvl 5 ("Checked " ++ show clhs)
|
||||
let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
|
||||
let wval = addImplBound i (map fst bargs) wval_in
|
||||
@ -847,12 +847,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
|
||||
return (tt, d, is, ctxt', newDecls))
|
||||
setContext ctxt'
|
||||
processTacticDecls newDecls
|
||||
def' <- checkDef fc defer
|
||||
def' <- checkDef fc iderr defer
|
||||
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
|
||||
addDeferred def''
|
||||
mapM_ (elabCaseBlock info opts) is
|
||||
logLvl 5 ("Checked wval " ++ show wval')
|
||||
(cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
|
||||
(cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')
|
||||
let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
|
||||
let cwvalN = explicitNames (normalise ctxt [] cwval)
|
||||
logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
|
||||
@ -907,7 +907,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
|
||||
addIBC (IBCImp wname)
|
||||
addIBC (IBCStatic wname)
|
||||
|
||||
def' <- checkDef fc [(wname, (-1, Nothing, wtype))]
|
||||
def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]
|
||||
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
|
||||
addDeferred def''
|
||||
|
||||
@ -943,12 +943,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
|
||||
setContext ctxt'
|
||||
processTacticDecls newDecls
|
||||
|
||||
def' <- checkDef fc defer
|
||||
def' <- checkDef fc iderr defer
|
||||
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
|
||||
addDeferred def''
|
||||
mapM_ (elabCaseBlock info opts) is
|
||||
logLvl 5 ("Checked RHS " ++ show rhs')
|
||||
(crhs, crhsty) <- recheckC fc [] rhs'
|
||||
(crhs, crhsty) <- recheckC fc id [] rhs'
|
||||
return $ (Right (clhs, crhs), lhs)
|
||||
where
|
||||
getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t
|
||||
|
||||
@ -135,6 +135,8 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
|
||||
[PClause fc iname lhs [] rhs wb]]
|
||||
iLOG (show idecls)
|
||||
mapM_ (rec_elabDecl info EAll info) idecls
|
||||
ist <- getIState
|
||||
checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))
|
||||
addIBC (IBCInstance intInst n iname)
|
||||
|
||||
where
|
||||
@ -175,7 +177,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
|
||||
setContext ctxt'
|
||||
processTacticDecls newDecls
|
||||
ctxt <- getContext
|
||||
(cty, _) <- recheckC fc [] tyT
|
||||
(cty, _) <- recheckC fc id [] tyT
|
||||
let nty = normalise ctxt [] cty
|
||||
return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)
|
||||
|
||||
@ -276,3 +278,28 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
|
||||
clauseFor m iname ns (PClauses _ _ m' _)
|
||||
= decorate ns iname m == decorate ns iname m'
|
||||
clauseFor m iname ns _ = False
|
||||
|
||||
checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
|
||||
checkInjectiveArgs fc n ds Nothing = return ()
|
||||
checkInjectiveArgs fc n ds (Just ty)
|
||||
= do ist <- getIState
|
||||
let (_, args) = unApply (instantiateRetTy ty)
|
||||
ci 0 ist args
|
||||
where
|
||||
ci i ist (a : as) | i `elem` ds
|
||||
= if isInj ist a then ci (i + 1) ist as
|
||||
else tclift $ tfail (At fc (InvalidTCArg n a))
|
||||
ci i ist (a : as) = ci (i + 1) ist as
|
||||
ci i ist [] = return ()
|
||||
|
||||
isInj i (P Bound n _) = True
|
||||
isInj i (P _ n _) = isConName n (tt_ctxt i)
|
||||
isInj i (App f a) = isInj i f && isInj i a
|
||||
isInj i (V _) = True
|
||||
isInj i (Bind n b sc) = isInj i sc
|
||||
isInj _ _ = True
|
||||
|
||||
instantiateRetTy (Bind n (Pi _ _ _) sc)
|
||||
= substV (P Bound n Erased) (instantiateRetTy sc)
|
||||
instantiateRetTy t = t
|
||||
|
||||
|
||||
@ -63,7 +63,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
|
||||
let lhs_ty = getInferType lhs'
|
||||
let newargs = pvars i lhs_tm
|
||||
|
||||
(clhs_tm_in, clhs_ty) <- recheckC fc [] lhs_tm
|
||||
(clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm
|
||||
let clhs_tm = renamepats pnames clhs_tm_in
|
||||
logLvl 3 ("Transform LHS " ++ show clhs_tm)
|
||||
|
||||
@ -80,7 +80,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
|
||||
setContext ctxt'
|
||||
processTacticDecls newDecls
|
||||
|
||||
(crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'
|
||||
(crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'
|
||||
let crhs_tm = renamepats pnames crhs_tm_in
|
||||
logLvl 3 ("Transform RHS " ++ show crhs_tm)
|
||||
|
||||
|
||||
@ -75,7 +75,7 @@ buildType info syn fc opts n ty' = do
|
||||
|
||||
logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'
|
||||
|
||||
ds <- checkAddDef True False fc defer
|
||||
ds <- checkAddDef True False fc iderr defer
|
||||
-- if the type is not complete, note that we'll need to infer
|
||||
-- things later (for solving metavariables)
|
||||
when (not (null ds)) $ addTyInferred n
|
||||
@ -85,7 +85,7 @@ buildType info syn fc opts n ty' = do
|
||||
logLvl 5 $ "Rechecking"
|
||||
logLvl 6 $ show tyT
|
||||
logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT
|
||||
(cty, ckind) <- recheckC fc [] tyT
|
||||
(cty, ckind) <- recheckC fc id [] tyT
|
||||
|
||||
-- record the implicit and inaccessible arguments
|
||||
i <- getIState
|
||||
@ -154,7 +154,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
|
||||
-- Productivity checking now via checking for guarded 'Delay'
|
||||
let opts' = opts -- if corec then (Coinductive : opts) else opts
|
||||
let usety = if norm then nty' else nty
|
||||
ds <- checkDef fc [(n, (-1, Nothing, usety))]
|
||||
ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]
|
||||
addIBC (IBCDef n)
|
||||
let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
|
||||
addDeferred ds'
|
||||
|
||||
@ -24,30 +24,36 @@ import qualified Data.Map as Map
|
||||
|
||||
recheckC = recheckC_borrowing False []
|
||||
|
||||
recheckC_borrowing uniq_check bs fc env t
|
||||
recheckC_borrowing uniq_check bs fc mkerr env t
|
||||
= do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
|
||||
ctxt <- getContext
|
||||
(tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of
|
||||
Error e -> tfail (At fc e)
|
||||
t' <- case safeForget t of
|
||||
Just ft -> return ft
|
||||
Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))
|
||||
(tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of
|
||||
Error e -> tfail (At fc (mkerr e))
|
||||
OK x -> return x
|
||||
logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs
|
||||
addConstraints fc cs
|
||||
return (tm, ty)
|
||||
|
||||
checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]
|
||||
-> Idris [(Name, (Int, Maybe Name, Type))]
|
||||
checkDef fc ns = checkAddDef False True fc ns
|
||||
iderr :: Name -> Err -> Err
|
||||
iderr _ e = e
|
||||
|
||||
checkAddDef :: Bool -> Bool -> FC
|
||||
checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]
|
||||
-> Idris [(Name, (Int, Maybe Name, Type))]
|
||||
checkDef fc mkerr ns = checkAddDef False True fc mkerr ns
|
||||
|
||||
checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)
|
||||
-> [(Name, (Int, Maybe Name, Type))]
|
||||
-> Idris [(Name, (Int, Maybe Name, Type))]
|
||||
checkAddDef add toplvl fc [] = return []
|
||||
checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
|
||||
checkAddDef add toplvl fc mkerr [] = return []
|
||||
checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns)
|
||||
= do ctxt <- getContext
|
||||
(t', _) <- recheckC fc [] t
|
||||
(t', _) <- recheckC fc (mkerr n) [] t
|
||||
when add $ do addDeferred [(n, (i, top, t, toplvl))]
|
||||
addIBC (IBCDef n)
|
||||
ns' <- checkAddDef add toplvl fc ns
|
||||
ns' <- checkAddDef add toplvl fc mkerr ns
|
||||
return ((n, (i, top, t')) : ns')
|
||||
|
||||
-- | Get the list of (index, name) of inaccessible arguments from an elaborated
|
||||
|
||||
@ -73,13 +73,13 @@ elabValBind info aspat norm tm_in
|
||||
|
||||
let vtm = orderPats (getInferTerm tm')
|
||||
|
||||
def' <- checkDef (fileFC "(input)") defer
|
||||
def' <- checkDef (fileFC "(input)") iderr defer
|
||||
let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
|
||||
addDeferred def''
|
||||
mapM_ (elabCaseBlock info []) is
|
||||
|
||||
logLvl 3 ("Value: " ++ show vtm)
|
||||
(vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm
|
||||
(vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm
|
||||
|
||||
let vtm = if norm then normalise (tt_ctxt i) [] vtm_in
|
||||
else vtm_in
|
||||
|
||||
@ -57,7 +57,7 @@ processTacticDecls info =
|
||||
updateIState $ \i -> i { idris_implicits =
|
||||
addDef n impls (idris_implicits i) }
|
||||
addIBC (IBCImp n)
|
||||
ds <- checkDef fc [(n, (-1, Nothing, ty))]
|
||||
ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]
|
||||
addIBC (IBCDef n)
|
||||
let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
|
||||
addDeferred ds'
|
||||
@ -1375,9 +1375,12 @@ findInstances :: IState -> Term -> [Name]
|
||||
findInstances ist t
|
||||
| (P _ n _, _) <- unApply t
|
||||
= case lookupCtxt n (idris_classes ist) of
|
||||
[CI _ _ _ _ _ ins _] -> ins
|
||||
[CI _ _ _ _ _ ins _] -> filter accessible ins
|
||||
_ -> []
|
||||
| otherwise = []
|
||||
where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
|
||||
Just (_, Hidden) -> False
|
||||
_ -> True
|
||||
|
||||
-- Try again to solve auto implicits
|
||||
solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()
|
||||
@ -2708,6 +2711,7 @@ reflectErr (NotInjective t1 t2 t3) =
|
||||
, reflect t3
|
||||
]
|
||||
reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
|
||||
reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
|
||||
reflectErr (CantResolveAlts ss) =
|
||||
raw_apply (Var $ reflErrName "CantResolveAlts")
|
||||
[rawList (Var $ reflm "TTName") (map reflectName ss)]
|
||||
|
||||
@ -78,7 +78,7 @@ prove opt ctxt lit n ty
|
||||
putIState (i { proof_list = (n, prf) : proofs })
|
||||
let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
|
||||
logLvl 3 (show tree)
|
||||
(ptm, pty) <- recheckC (fileFC "proof") [] tm
|
||||
(ptm, pty) <- recheckC (fileFC "proof") id [] tm
|
||||
logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
|
||||
"Expected type:" ++ show ty)
|
||||
case converts ctxt [] ty pty of
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))
|
||||
--------------
|
||||
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 48))) (TType (UVar 50))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 52))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 54)))))
|
||||
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 32))) (TType (UVar 34))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 36))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 38)))))
|
||||
--------------
|
||||
(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48))))
|
||||
(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32))))
|
||||
|
||||
@ -17,4 +17,4 @@ with
|
||||
unique001b.idr:16:7:Borrowed name xs must not be used on RHS
|
||||
unique001c.idr:46:6:Unique name f is used more than once
|
||||
unique001d.idr:3:7:Borrowed name x must not be used on RHS
|
||||
unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not
|
||||
unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not
|
||||
|
||||
Loading…
Reference in New Issue
Block a user