mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-13 05:48:39 +03:00
Merge branch 'master' of https://github.com/idris-lang/Idris2 into master
This commit is contained in:
russoul
commit
50ac934747
157
libs/base/Control/Monad/Either.idr
Normal file
157
libs/base/Control/Monad/Either.idr
Normal file
@ -0,0 +1,157 @@
|
||||
module Control.Monad.Either
|
||||
|
||||
-------------------------------------------------
|
||||
-- The monad transformer `EitherT e m a` equips a monad with the ability to
|
||||
-- return a choice of two values.
|
||||
|
||||
-- Sequenced actions of `Either e m a` produce a value `a` only if none of the
|
||||
-- actions in the sequence returned `e`. Because returning `e` exits the
|
||||
-- computation early, this can be seen as equipping a monad with the ability to
|
||||
-- throw an exception.
|
||||
|
||||
-- This is more powerful than MaybeT which instead equips a monad with the
|
||||
-- ability to not return a result.
|
||||
-------------------------------------------------
|
||||
|
||||
import Control.Monad.Trans
|
||||
import Control.Monad.Reader
|
||||
import Control.Monad.State
|
||||
|
||||
public export
|
||||
data EitherT : (e : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
|
||||
MkEitherT : (1 _ : m (Either e a)) -> EitherT e m a
|
||||
|
||||
export
|
||||
%inline
|
||||
runEitherT : EitherT e m a -> m (Either e a)
|
||||
runEitherT (MkEitherT x) = x
|
||||
|
||||
export
|
||||
eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT a m b -> m c
|
||||
eitherT f g x = runEitherT x >>= either f g
|
||||
|
||||
||| map the underlying computation
|
||||
||| The basic 'unwrap, apply, rewrap' of this transformer.
|
||||
export
|
||||
%inline
|
||||
mapEitherT : (m (Either e a) -> n (Either e' a')) -> EitherT e m a -> EitherT e' n a'
|
||||
mapEitherT f = MkEitherT . f . runEitherT
|
||||
|
||||
export
|
||||
bimapEitherT : Functor m => (a -> c) -> (b -> d)
|
||||
-> EitherT a m b -> EitherT c m d
|
||||
bimapEitherT f g x = mapEitherT (map (either (Left . f) (Right . g))) x
|
||||
|
||||
||| Analogous to Left, aka throwE
|
||||
export
|
||||
%inline
|
||||
left : Applicative m => e -> EitherT e m a
|
||||
left = MkEitherT . pure . Left
|
||||
|
||||
||| Analogous to Right, aka pure for EitherT
|
||||
export
|
||||
%inline
|
||||
right : Applicative m => a -> EitherT e m a
|
||||
right = MkEitherT . pure . Right
|
||||
|
||||
export
|
||||
swapEitherT : Functor m => EitherT e m a -> EitherT a m e
|
||||
swapEitherT = mapEitherT (map (either Right Left))
|
||||
|
||||
-------------------------------------------------
|
||||
-- Methods of the 'exception' theme
|
||||
-------------------------------------------------
|
||||
|
||||
||| aka `left`
|
||||
export
|
||||
%inline
|
||||
throwE : Applicative m => e -> EitherT e m a
|
||||
throwE = MkEitherT . pure . Left
|
||||
|
||||
export
|
||||
catchE : Monad m => EitherT e m a -> (e -> EitherT e' m a) -> EitherT e' m a
|
||||
catchE et f
|
||||
= MkEitherT $ runEitherT et >>= either (runEitherT . f) (pure . Right)
|
||||
|
||||
|
||||
-------------------------------------------------
|
||||
-- Interface Implementations
|
||||
-------------------------------------------------
|
||||
|
||||
on : (b -> b -> c) -> (a -> b) -> a -> a -> c
|
||||
on f g x y = g x `f` g y
|
||||
|
||||
public export
|
||||
Eq (m (Either e a)) => Eq (EitherT e m a) where
|
||||
(==) = (==) `on` runEitherT
|
||||
|
||||
public export
|
||||
Ord (m (Either e a)) => Ord (EitherT e m a) where
|
||||
compare = compare `on` runEitherT
|
||||
|
||||
public export
|
||||
Show (m (Either e a)) => Show (EitherT e m a) where
|
||||
showPrec d (MkEitherT x) = showCon d "MkEitherT" $ showArg x
|
||||
|
||||
-- I'm not actually confident about having this instance but it is a sane
|
||||
-- default and since idris has named implementations it can be swapped out at
|
||||
-- the use site.
|
||||
public export
|
||||
Monad m => Semigroup (EitherT e m a) where
|
||||
MkEitherT x <+> MkEitherT y = MkEitherT $ do
|
||||
r@(Right _) <- x
|
||||
| Left _ => y
|
||||
pure r
|
||||
|
||||
public export
|
||||
Functor m => Functor (EitherT e m) where
|
||||
map f e = MkEitherT $ map f <$> runEitherT e
|
||||
|
||||
public export
|
||||
Foldable m => Foldable (EitherT e m) where
|
||||
foldr f acc (MkEitherT e)
|
||||
= foldr (\x,xs => either (const acc) (`f` xs) x) acc e
|
||||
|
||||
public export
|
||||
Traversable m => Traversable (EitherT e m) where
|
||||
traverse f (MkEitherT x)
|
||||
= MkEitherT <$> traverse (either (pure . Left) (map Right . f)) x
|
||||
|
||||
public export
|
||||
Applicative m => Applicative (EitherT e m) where
|
||||
pure = MkEitherT . pure . Right
|
||||
f <*> x = MkEitherT [| runEitherT f <*> runEitherT x |]
|
||||
|
||||
public export
|
||||
Monad m => Monad (EitherT e m) where
|
||||
x >>= k = MkEitherT $ runEitherT x >>= either (pure . Left) (runEitherT . k)
|
||||
|
||||
||| Alternative instance that collects left results, allowing you to try
|
||||
||| multiple possibilities and combine failures.
|
||||
public export
|
||||
(Monad m, Monoid e) => Alternative (EitherT e m) where
|
||||
empty = left neutral
|
||||
MkEitherT x <|> MkEitherT y = MkEitherT $ do
|
||||
Left l <- x
|
||||
| Right r => pure (Right r)
|
||||
Left l' <- y
|
||||
| Right r => pure (Right r)
|
||||
pure (Left (l <+> l'))
|
||||
|
||||
public export
|
||||
MonadTrans (EitherT e) where
|
||||
lift = MkEitherT . map Right
|
||||
|
||||
public export
|
||||
HasIO m => HasIO (EitherT e m) where
|
||||
liftIO act = MkEitherT $ liftIO (io_bind act (pure . Right))
|
||||
|
||||
public export
|
||||
MonadReader r m => MonadReader r (EitherT e m) where
|
||||
ask = lift ask
|
||||
local f (MkEitherT x) = MkEitherT (local f x)
|
||||
|
||||
public export
|
||||
MonadState s m => MonadState s (EitherT e m) where
|
||||
get = lift get
|
||||
put = lift . put
|
||||
@ -16,15 +16,19 @@ partial
|
||||
foldl1 : (a -> a -> a) -> List a -> a
|
||||
foldl1 f (x::xs) = foldl f x xs
|
||||
|
||||
-- This works quickly because when string-append builds the result, it allocates
|
||||
-- This works quickly because when string-concat builds the result, it allocates
|
||||
-- enough room in advance so there's only one allocation, rather than lots!
|
||||
%foreign
|
||||
"scheme:string-concat"
|
||||
"javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
|
||||
export
|
||||
fastConcat : List String -> String
|
||||
|
||||
-- This is a deprecated alias for fastConcat for backwards compatibility
|
||||
-- (unfortunately, we don't have %deprecated yet).
|
||||
export
|
||||
fastAppend : List String -> String
|
||||
fastAppend xs = unsafePerformIO (schemeCall String "string-append" (toFArgs xs))
|
||||
where
|
||||
toFArgs : List String -> FArgList
|
||||
toFArgs [] = []
|
||||
toFArgs (x :: xs) = x :: toFArgs xs
|
||||
fastAppend = fastConcat
|
||||
|
||||
||| Splits a character list into a list of whitespace separated character lists.
|
||||
|||
|
||||
|
||||
@ -4,6 +4,7 @@ modules = Control.App,
|
||||
Control.App.Console,
|
||||
Control.App.FileIO,
|
||||
|
||||
Control.Monad.Either,
|
||||
Control.Monad.Identity,
|
||||
Control.Monad.Reader,
|
||||
Control.Monad.ST,
|
||||
|
||||
@ -247,6 +247,16 @@ Monad (Either e) where
|
||||
(Left n) >>= _ = Left n
|
||||
(Right r) >>= f = f r
|
||||
|
||||
public export
|
||||
Foldable (Either e) where
|
||||
foldr f acc (Left _) = acc
|
||||
foldr f acc (Right x) = f x acc
|
||||
|
||||
public export
|
||||
Traversable (Either e) where
|
||||
traverse f (Left x) = pure (Left x)
|
||||
traverse f (Right x) = Right <$> f x
|
||||
|
||||
-----------
|
||||
-- LISTS --
|
||||
-----------
|
||||
|
||||
@ -337,9 +337,7 @@ jsPrim (NS _ (UN "prim__os")) [] =
|
||||
sysos <- addConstToPreamble "sysos" (oscalc ++ "(" ++ os ++ ".platform())")
|
||||
pure sysos
|
||||
jsPrim (NS _ (UN "prim__schemeCall"))[_, fn, args, _] =
|
||||
case fn of
|
||||
"'string-append'" => pure $ "''.concat(...__prim_idris2js_FArgList("++ args ++"))"
|
||||
o => throw (InternalError $ "schemeCall not implemented " ++ show o)
|
||||
throw (InternalError $ "schemeCall not implemented " ++ show (fn, args))
|
||||
jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x)
|
||||
|
||||
tag2es : Either Int String -> String
|
||||
|
||||
@ -61,6 +61,12 @@
|
||||
(define cast-string-double
|
||||
(lambda (x)
|
||||
(cast-num (string->number (destroy-prefix x)))))
|
||||
|
||||
(define (from-idris-list xs)
|
||||
(if (= (vector-ref xs 0) 0)
|
||||
'()
|
||||
(cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
|
||||
(define (string-concat xs) (apply string-append (from-idris-list xs)))
|
||||
(define string-cons (lambda (x y) (string-append (string x) y)))
|
||||
(define get-tag (lambda (x) (vector-ref x 0)))
|
||||
(define string-reverse (lambda (x)
|
||||
|
||||
@ -68,6 +68,13 @@
|
||||
(define-macro (cast-string-int x)
|
||||
`(floor (cast-string-double ,x)))
|
||||
|
||||
(define (from-idris-list xs)
|
||||
(if (= (vector-ref xs 0) 0)
|
||||
'()
|
||||
(cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
|
||||
(define-macro (string-concat xs)
|
||||
`(apply string-append (from-idris-list ,xs)))
|
||||
|
||||
(define-macro (string-cons x y)
|
||||
`(string-append (string ,x) ,y))
|
||||
|
||||
|
||||
@ -55,6 +55,11 @@
|
||||
(define cast-string-double
|
||||
(lambda (x)
|
||||
(cast-num (string->number (destroy-prefix x)))))
|
||||
(define (from-idris-list xs)
|
||||
(if (= (vector-ref xs 0) 0)
|
||||
'()
|
||||
(cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
|
||||
(define (string-concat xs) (apply string-append (from-idris-list xs)))
|
||||
(define string-cons (lambda (x y) (string-append (string x) y)))
|
||||
(define get-tag (lambda (x) (vector-ref x 0)))
|
||||
(define string-reverse (lambda (x)
|
||||
|
||||
@ -21,11 +21,11 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:1677}, (Term.idr:11:15--11:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:1677}, (Term.idr:11:19--11:23, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:11:15--11:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:11:19--11:23, Rig0))
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:1680}, (Term.idr:12:15--12:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:1680}, (Term.idr:12:19--12:23, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:12:15--12:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:12:19--12:23, Rig0))
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG declare.data:1: Processing Term.Chk
|
||||
@ -33,14 +33,14 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:1683}, (Term.idr:16:15--16:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:1683}, (Term.idr:16:19--16:23, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:16:15--16:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:16:19--16:23, Rig0))
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:1686}, (Term.idr:17:15--17:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:1686}, (Term.idr:17:19--17:23, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:n:1686}, (Term.idr:17:35--17:36, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:17:15--17:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:17:19--17:23, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:n:N}, (Term.idr:17:35--17:36, Rig0))
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG declare.data:1: Processing Term.Syn
|
||||
@ -48,25 +48,25 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:1690}, (Term.idr:22:15--22:19, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:1690}, (Term.idr:22:27--22:30, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:22:15--22:19, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:22:27--22:30, Rig0))
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:1693}, (Term.idr:23:15--23:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:1693}, (Term.idr:23:19--23:23, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:23:15--23:18, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:23:19--23:23, Rig0))
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:1696}, (Term.idr:24:20--24:24, Rig0))
|
||||
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:24:20--24:24, Rig0))
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG declare.def.lhs:3: LHS term: Term.Typ
|
||||
LOG unify.equal:10: Skipped unification (equal already): ((vars : $resolved736) -> Type) and ((vars : $resolved736) -> Type)
|
||||
LOG unify.equal:10: Skipped unification (equal already): ((vars : $resolvedN) -> Type) and ((vars : $resolvedN) -> Type)
|
||||
LOG declare.def.clause:3: RHS term: Term.Chk
|
||||
LOG declare.def:2: Case tree for Term.Typ: [0] Term.Chk
|
||||
LOG declare.def:3: Working from [0] Term.Chk
|
||||
LOG declare.def:3: Catch all case in 1676
|
||||
LOG declare.def:3: Catch all case in N
|
||||
LOG declare.def:3: Initially missing in Term.Typ:
|
||||
|
||||
LOG declare.type:1: Processing Term.Term
|
||||
@ -78,7 +78,7 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.True)
|
||||
LOG declare.def:2: Case tree for Term.Term: [0] (Term.Chk Prelude.Basics.True)
|
||||
LOG declare.def:3: Working from [0] (Term.Chk Prelude.Basics.True)
|
||||
LOG declare.def:3: Catch all case in 1698
|
||||
LOG declare.def:3: Catch all case in N
|
||||
LOG declare.def:3: Initially missing in Term.Term:
|
||||
|
||||
LOG declare.type:1: Processing Term.NF
|
||||
@ -90,43 +90,43 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
|
||||
LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.False)
|
||||
LOG declare.def:2: Case tree for Term.NF: [0] (Term.Chk Prelude.Basics.False)
|
||||
LOG declare.def:3: Working from [0] (Term.Chk Prelude.Basics.False)
|
||||
LOG declare.def:3: Catch all case in 1699
|
||||
LOG declare.def:3: Catch all case in N
|
||||
LOG declare.def:3: Initially missing in Term.NF:
|
||||
|
||||
Term> Bye for now!
|
||||
1/1: Building Vec (Vec.idr)
|
||||
LOG declare.type:1: Processing Vec.Vec
|
||||
LOG declare.def:2: Case tree for Vec.Vec: [0] (({arg:427} : (Data.Fin.Fin {arg:1}[1])) -> {arg:0}[1])
|
||||
LOG declare.def:2: Case tree for Vec.Vec: [0] (({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1])
|
||||
LOG declare.type:1: Processing Vec.Nil
|
||||
LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:0}[0] ?Vec.{t:431}_[{arg:0}[0]] Data.Fin.Uninhabited implementation at Data/Fin.idr:19:1--24:7)
|
||||
LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] ?Vec.{t:N}_[{arg:N}[0]] Data.Fin.Uninhabited implementation at Data/Fin.idr:19:1--24:7)
|
||||
LOG declare.type:1: Processing Vec.::
|
||||
LOG declare.def:2: Case tree for Vec.::: case {arg:4}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:0}[0])) of { Data.Fin.FZ {e:0} => [0] {arg:2}[3] | Data.Fin.FS {e:1} {e:2} => [1] ({arg:3}[5] {e:2}[1]) }
|
||||
LOG declare.def:2: Case tree for Vec.::: case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of { Data.Fin.FZ {e:N} => [0] {arg:N}[3] | Data.Fin.FS {e:N} {e:N} => [1] ({arg:N}[5] {e:N}[1]) }
|
||||
LOG declare.type:1: Processing Vec.test
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolved1648 2), ($resolved948 2)] at Vec.idr:20:23--20:24
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolvedN 2), ($resolvedN 2)] at Vec.idr:20:23--20:24
|
||||
With default. Target type : Prelude.Types.Nat
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [(($resolved1683 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)), (($resolved1477 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)), (($resolved745 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)), (($resolved744 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))] at Vec.idr:21:8--21:17
|
||||
Target type : (({arg:427} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) -> (Prelude.Types.List Prelude.Types.Nat))
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [$resolved1676, $resolved1468, $resolved735] at Vec.idr:21:9--21:11
|
||||
Target type : ?Vec.{a:455}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [(($resolved1683 ((:: (fromInteger 0)) Nil)) Nil), (($resolved1477 ((:: (fromInteger 0)) Nil)) Nil), (($resolved745 ((:: (fromInteger 0)) Nil)) Nil), (($resolved744 ((:: (fromInteger 0)) Nil)) Nil)] at Vec.idr:21:8--21:17
|
||||
Target type : (({arg:427} : (Data.Fin.Fin ?Vec.{n:454}_[])) -> ?Vec.{a:455}_[])
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [(($resolved1683 (fromInteger 0)) Nil), (($resolved1477 (fromInteger 0)) Nil), (($resolved745 (fromInteger 0)) Nil), (($resolved744 (fromInteger 0)) Nil)] at Vec.idr:21:13--21:16
|
||||
Target type : ?Vec.{a:458}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolved1648 0), ($resolved948 0)] at Vec.idr:21:14--21:15
|
||||
With default. Target type : ?Vec.{a:460}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [$resolved1676, $resolved1468, $resolved735] at Vec.idr:21:13--21:16
|
||||
Target type : (({arg:427} : (Data.Fin.Fin ?Vec.{n:459}_[])) -> ?Vec.{a:460}_[])
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolved1648 0), ($resolved948 0)] at Vec.idr:21:14--21:15
|
||||
With default. Target type : ?Vec.{a:459}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolved1648 0), ($resolved948 0)] at Vec.idr:21:14--21:15
|
||||
With default. Target type : ?Vec.{a:459}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [$resolved1676, $resolved1468, $resolved735] at Vec.idr:21:8--21:17
|
||||
Target type : (({arg:427} : (Data.Fin.Fin ?Vec.{n:457}_[])) -> ?Vec.{a:458}_[])
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration True [(($resolved744 (fromInteger 0)) Nil)] at Vec.idr:21:13--21:16
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)), (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)), (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)), (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))] at Vec.idr:21:8--21:17
|
||||
Target type : (({arg:N} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) -> (Prelude.Types.List Prelude.Types.Nat))
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [$resolvedN, $resolvedN, $resolvedN] at Vec.idr:21:9--21:11
|
||||
Target type : ?Vec.{a:N}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [(($resolvedN ((:: (fromInteger 0)) Nil)) Nil), (($resolvedN ((:: (fromInteger 0)) Nil)) Nil), (($resolvedN ((:: (fromInteger 0)) Nil)) Nil), (($resolvedN ((:: (fromInteger 0)) Nil)) Nil)] at Vec.idr:21:8--21:17
|
||||
Target type : (({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [(($resolvedN (fromInteger 0)) Nil), (($resolvedN (fromInteger 0)) Nil), (($resolvedN (fromInteger 0)) Nil), (($resolvedN (fromInteger 0)) Nil)] at Vec.idr:21:13--21:16
|
||||
Target type : ?Vec.{a:N}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolvedN 0), ($resolvedN 0)] at Vec.idr:21:14--21:15
|
||||
With default. Target type : ?Vec.{a:N}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [$resolvedN, $resolvedN, $resolvedN] at Vec.idr:21:13--21:16
|
||||
Target type : (({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolvedN 0), ($resolvedN 0)] at Vec.idr:21:14--21:15
|
||||
With default. Target type : ?Vec.{a:N}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolvedN 0), ($resolvedN 0)] at Vec.idr:21:14--21:15
|
||||
With default. Target type : ?Vec.{a:N}_[]
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration False [$resolvedN, $resolvedN, $resolvedN] at Vec.idr:21:8--21:17
|
||||
Target type : (({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration True [(($resolvedN (fromInteger 0)) Nil)] at Vec.idr:21:13--21:16
|
||||
Target type : (Prelude.Types.List Prelude.Types.Nat)
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolved1648 0), ($resolved948 0)] at Vec.idr:21:14--21:15
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration [($resolvedN 0), ($resolvedN 0)] at Vec.idr:21:14--21:15
|
||||
With default. Target type : Prelude.Types.Nat
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration True [$resolved735] at Vec.idr:21:9--21:11
|
||||
LOG elab.ambiguous:5: Ambiguous elaboration True [$resolvedN] at Vec.idr:21:9--21:11
|
||||
Target type : (Prelude.Types.List Prelude.Types.Nat)
|
||||
LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: ?Vec.{n:454}_[] ?Vec.{a:455}_[] (Prelude.Types.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z ?Vec.{a:455}_[] (Prelude.Types.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Types.Nil Prelude.Types.Nat)) (Vec.Nil ?Vec.{a:455}_[])))
|
||||
LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: ?Vec.{n:N}_[] ?Vec.{a:N}_[] (Prelude.Types.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z ?Vec.{a:N}_[] (Prelude.Types.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Types.Nil Prelude.Types.Nat)) (Vec.Nil ?Vec.{a:N}_[])))
|
||||
Vec> Bye for now!
|
||||
|
||||
@ -1,4 +1,6 @@
|
||||
echo ":q" | $1 --no-banner --no-color --console-width 0 --log unify.equal:10 --log unify:5 Term.idr
|
||||
echo ":q" | $1 --no-banner --no-color --console-width 0 --log unify:3 --log elab.ambiguous:5 Vec.idr
|
||||
echo ":q" | $1 --no-banner --no-color --console-width 0 --log unify.equal:10 --log unify:5 Term.idr \
|
||||
| sed -E "s/[0-9]+}/N}/g" | sed -E "s/resolved([0-9]+)/resolvedN/g" | sed -E "s/case in ([0-9]+)/case in N/g"
|
||||
echo ":q" | $1 --no-banner --no-color --console-width 0 --log unify:3 --log elab.ambiguous:5 Vec.idr \
|
||||
| sed -E "s/[0-9]+}/N}/g" | sed -E "s/resolved([0-9]+)/resolvedN/g" | sed -E "s/case in ([0-9]+)/case in N/g"
|
||||
|
||||
rm -rf build
|
||||
Loading…
Reference in New Issue
Block a user