idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of https://github.com/idris-lang/Idris2 into master

Browse Source
This commit is contained in:
russoul 2020-09-29 12:58:28 +03:00
commit af62955e07
199 changed files with 2795 additions and 1115 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
docs/source/faq/faq.rst
View File

@ -32,11 +32,12 @@ is a very convenient way to bootstrap.
Can Idris 2 generate Javascript? What about plug-in code generators?
====================================================================
Not yet, but there is a Javascript code generator in development.
Yes! A `JavaScript code generator <https://idris2.readthedocs.io/en/latest/backends/javascript.html/>`_
is built in, and can target either the browser or NodeJS.
Like Idris 1, Idris 2 will support plug-in code generation to allow you to
write a back end for the platform of your choice, but this is not yet
implemented.
Like Idris 1, Idris 2
`supports plug-in code generation <https://idris2.readthedocs.io/en/latest/backends/custom.html>`_
to allow you to write a back end for the platform of your choice.
What are the main differences between Idris 1 and Idris 2?
==========================================================

25
docs/source/ffi/ffi.rst
View File

@ -27,8 +27,29 @@ the library. In this document, we will assume the default Chez Scheme code
generator (the examples also work with the Racket or Gambit code generator) and
that the foreign language is C.
Example
-------
Scheme Sidenote
---------------
Scheme foreign specifiers can be written to target particular flavors.
The following example shows a foreign declaration that allocates memory in a
way specific to the choice of code generator. In this example there is no
general scheme specifier present that matches every flavor, e.g.
``scheme:foo``, so it will only match the specific flavors listed:
.. code-block:: idris
%foreign "scheme,chez:foreign-alloc"
"scheme,racket:malloc"
"C:malloc,libc"
allocMem : (bytes : Int) -> PrimIO AnyPtr
.. note::
If your backend (code generator) is not specified but defines a C FFI
it will be able to make use of the ``C:malloc,libc`` specifier.
FFI Example
-----------
As a running example, we are going to work with a small C file. Save the
following content to a file ``smallc.c``

2
docs/source/typedd/typedd.rst
View File

@ -346,6 +346,8 @@ arguments ``div`` and ``rem``.
In ``ArithState.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO``
also have to be ``export``.
evalState from Control.Monad.State now takes the ``stateType`` argument first.
Chapter 13
----------

4
idris2api.ipkg
View File

@ -32,6 +32,8 @@ modules =
Core.CaseTree,
Core.CompileExpr,
Core.Context,
Core.Context.Data,
Core.Context.Log,
Core.Core,
Core.Coverage,
Core.Directory,
@ -43,6 +45,7 @@ modules =
Core.LinearCheck,
Core.Metadata,
Core.Name,
Core.Name.Namespace,
Core.Normalise,
Core.Options,
Core.Options.Log,
@ -78,6 +81,7 @@ modules =
Idris.ModTree,
Idris.Package,
Idris.Parser,
Idris.Parser.Let,
Idris.Pretty,
Idris.ProcessIdr,
Idris.REPL,

16
libs/base/Control/Monad/Reader.idr
View File

@ -14,9 +14,9 @@ interface Monad m => MonadReader stateType (m : Type -> Type) | m where
||| The transformer on which the Reader monad is based
public export
record ReaderT (stateType : Type) (m: Type -> Type) (a: Type) where
record ReaderT (stateType : Type) (m : Type -> Type) (a : Type) where
constructor MkReaderT
runReaderT : stateType -> m a
runReaderT' : stateType -> m a
public export
implementation Functor f => Functor (ReaderT stateType f) where
@ -64,12 +64,18 @@ public export
asks : MonadReader stateType m => (stateType -> a) -> m a
asks f = ask >>= pure . f
||| Unwrap and apply a ReaderT monad computation
public export
%inline
runReaderT : stateType -> ReaderT stateType m a -> m a
runReaderT s action = runReaderT' action s
||| The Reader monad. The ReaderT transformer applied to the Identity monad.
public export
Reader : (stateType : Type) -> (a : Type) -> Type
Reader s a = ReaderT s Identity a
||| Executes a Reader computation given a context.
||| Unwrap and apply a Reader monad computation
public export
runReader : Reader stateType a -> stateType -> a
runReader action = runIdentity . runReaderT action
runReader : stateType -> Reader stateType a -> a
runReader s = runIdentity . runReaderT s

46
libs/base/Control/Monad/State.idr
View File

@ -15,43 +15,41 @@ interface Monad m => MonadState stateType (m : Type -> Type) | m where
public export
record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
constructor ST
runStateT : stateType -> m (a, stateType)
runStateT' : stateType -> m (stateType, a)
public export
implementation Functor f => Functor (StateT stateType f) where
map f (ST g) = ST (\st => map (mapFst f) (g st)) where
mapFst : (a -> x) -> (a, s) -> (x, s)
mapFst fn (a, b) = (fn a, b)
map f (ST g) = ST (\st => map (map f) (g st)) where
public export
implementation Monad f => Applicative (StateT stateType f) where
pure x = ST (\st => pure (x, st))
pure x = ST (\st => pure (st, x))
(ST f) <*> (ST a)
= ST (\st =>
do (g, r) <- f st
(b, t) <- a r
pure (g b, t))
do (r, g) <- f st
(t, b) <- a r
pure (t, g b))
public export
implementation Monad m => Monad (StateT stateType m) where
(ST f) >>= k
= ST (\st =>
do (v, st') <- f st
do (st', v) <- f st
let ST kv = k v
kv st')
public export
implementation Monad m => MonadState stateType (StateT stateType m) where
get = ST (\x => pure (x, x))
put x = ST (\y => pure ((), x))
put x = ST (\y => pure (x, ()))
public export
implementation MonadTrans (StateT stateType) where
lift x
= ST (\st =>
do r <- x
pure (r, st))
pure (st, r))
public export
implementation (Monad f, Alternative f) => Alternative (StateT st f) where
@ -60,7 +58,7 @@ implementation (Monad f, Alternative f) => Alternative (StateT st f) where
public export
implementation HasIO m => HasIO (StateT stateType m) where
liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (a, s)
liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (s, a)
||| Apply a function to modify the context of this computation
public export
@ -76,22 +74,28 @@ gets f
= do s <- get
pure (f s)
||| Unwrap and apply a StateT monad computation.
public export
%inline
runStateT : stateType -> StateT stateType m a -> m (stateType, a)
runStateT s act = runStateT' act s
||| The State monad. See the MonadState interface
public export
State : (stateType : Type) -> (ty : Type) -> Type
State = \s, a => StateT s Identity a
||| Unwrap a State monad computation.
||| Unwrap and apply a State monad computation.
public export
runState : StateT stateType Identity a -> stateType -> (a, stateType)
runState act = runIdentity . runStateT act
runState : stateType -> StateT stateType Identity a -> (stateType, a)
runState s act = runIdentity (runStateT s act)
||| Unwrap a State monad computation, but discard the final state.
||| Unwrap and apply a State monad computation, but discard the final state.
public export
evalState : State stateType a -> stateType -> a
evalState m = fst . runState m
evalState : stateType -> State stateType a -> a
evalState s = snd . runState s
||| Unwrap a State monad computation, but discard the resulting value.
||| Unwrap and apply a State monad computation, but discard the resulting value.
public export
execState : State stateType a -> stateType -> stateType
execState m = snd . runState m
execState : stateType -> State stateType a -> stateType
execState s = fst . runState s

59
libs/base/Data/Either.idr
View File

@ -1,7 +1,24 @@
module Data.Either
import Data.List1
%default total
--------------------------------------------------------------------------------
-- Checking for a specific constructor
||| Extract the Left value, if possible
public export
getLeft : Either a b -> Maybe a
getLeft (Left a) = Just a
getLeft _ = Nothing
||| Extract the Right value, if possible
public export
getRight : Either a b -> Maybe b
getRight (Right b) = Just b
getRight _ = Nothing
||| True if the argument is Left, False otherwise
public export
isLeft : Either a b -> Bool
@ -14,6 +31,35 @@ isRight : Either a b -> Bool
isRight (Left _) = False
isRight (Right _) = True
--------------------------------------------------------------------------------
-- Grouping values
mutual
||| Compress the list of Lefts and Rights by accumulating
||| all of the lefts and rights into non-empty blocks.
export
compress : List (Either a b) -> List (Either (List1 a) (List1 b))
compress [] = []
compress (Left a :: abs) = compressLefts (singleton a) abs
compress (Right b :: abs) = compressRights (singleton b) abs
compressLefts : List1 a -> List (Either a b) -> List (Either (List1 a) (List1 b))
compressLefts acc (Left a :: abs) = compressLefts (cons a acc) abs
compressLefts acc abs = Left (reverse acc) :: compress abs
compressRights : List1 b -> List (Either a b) -> List (Either (List1 a) (List1 b))
compressRights acc (Right b :: abs) = compressRights (cons b acc) abs
compressRights acc abs = Right (reverse acc) :: compress abs
||| Decompress a compressed list. This is the left inverse of `compress` but not its
||| right inverse because nothing forces the input to be maximally compressed!
export
decompress : List (Either (List1 a) (List1 b)) -> List (Either a b)
decompress = concatMap $ \ abs => case abs of
Left as => map Left $ forget as
Right bs => map Right $ forget bs
||| Keep the payloads of all Left constructors in a list of Eithers
public export
lefts : List (Either a b) -> List a
@ -45,6 +91,19 @@ mirror : Either a b -> Either b a
mirror (Left x) = Right x
mirror (Right x) = Left x
--------------------------------------------------------------------------------
-- Bifunctor
export
bimap : (a -> c) -> (b -> d) -> Either a b -> Either c d
bimap l r (Left a) = Left (l a)
bimap l r (Right b) = Right (r b)
export
pushInto : c -> Either a b -> Either (c, a) (c, b)
pushInto c = bimap (\ a => (c, a)) (\ b => (c, b))
-- ^ not using sections to keep it backwards compatible
--------------------------------------------------------------------------------
-- Conversions
--------------------------------------------------------------------------------

30
libs/base/Data/List.idr
View File

@ -174,13 +174,20 @@ public export
union : Eq a => List a -> List a -> List a
union = unionBy (==)
public export
spanBy : (a -> Maybe b) -> List a -> (List b, List a)
spanBy p [] = ([], [])
spanBy p (x :: xs) = case p x of
Nothing => ([], x :: xs)
Just y => let (ys, zs) = spanBy p xs in (y :: ys, zs)
public export
span : (a -> Bool) -> List a -> (List a, List a)
span p [] = ([], [])
span p (x::xs) =
if p x then
let (ys, zs) = span p xs in
(x::ys, zs)
(x::ys, zs)
else
([], x::xs)
@ -192,8 +199,8 @@ public export
split : (a -> Bool) -> List a -> List1 (List a)
split p xs =
case break p xs of
(chunk, []) => [chunk]
(chunk, (c :: rest)) => chunk :: toList (split p (assert_smaller xs rest))
(chunk, []) => singleton chunk
(chunk, (c :: rest)) => cons chunk (split p (assert_smaller xs rest))
public export
splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
@ -284,6 +291,15 @@ export
intersect : Eq a => List a -> List a -> List a
intersect = intersectBy (==)
export
intersectAllBy : (a -> a -> Bool) -> List (List a) -> List a
intersectAllBy eq [] = []
intersectAllBy eq (xs :: xss) = filter (\x => all (elemBy eq x) xss) xs
export
intersectAll : Eq a => List (List a) -> List a
intersectAll = intersectAllBy (==)
||| Combine two lists elementwise using some function.
|||
||| If the lists are different lengths, the result is truncated to the
@ -345,7 +361,7 @@ public export
last : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
last [] impossible
last [x] = x
last (x::y::ys) = last (y::ys)
last (_::x::xs) = List.last (x::xs)
||| Return all but the last element of a non-empty list.
||| @ ok proof the list is non-empty
@ -451,19 +467,19 @@ public export
foldr1 : (a -> a -> a) -> (l : List a) -> {auto 0 ok : NonEmpty l} -> a
foldr1 f [] impossible
foldr1 f [x] = x
foldr1 f (x::y::ys) = f x (foldr1 f (y::ys))
foldr1 f (x::y::ys) = f x (List.foldr1 f (y::ys))
||| Foldl without seeding the accumulator. If the list is empty, return `Nothing`.
public export
foldl1' : (a -> a -> a) -> List a -> Maybe a
foldl1' f [] = Nothing
foldl1' f xs@(_::_) = Just (foldl1 f xs)
foldl1' f xs@(_::_) = Just (List.foldl1 f xs)
||| Foldr without seeding the accumulator. If the list is empty, return `Nothing`.
public export
foldr1' : (a -> a -> a) -> List a -> Maybe a
foldr1' f [] = Nothing
foldr1' f xs@(_::_) = Just (foldr1 f xs)
foldr1' f xs@(_::_) = Just (List.foldr1 f xs)
--------------------------------------------------------------------------------
-- Sorting

131
libs/base/Data/List1.idr
View File

@ -2,60 +2,137 @@ module Data.List1
%default total
infixr 7 :::
public export
record List1 a where
constructor (::)
constructor (:::)
head : a
tail : List a
public export
toList : (1 xs : List1 a) -> List a
toList (x :: xs) = x :: xs
------------------------------------------------------------------------
-- Conversion
||| Forget that a list is non-empty
public export
reverseOnto : (1 acc : List1 a) -> (1 xs : List a) -> List1 a
reverseOnto acc [] = acc
reverseOnto acc (x :: xs) = reverseOnto (x :: toList acc) xs
public export
reverse : (1 xs : List1 a) -> List1 a
reverse (x :: xs) = reverseOnto [x] xs
forget : (1 xs : List1 a) -> List a
forget (x ::: xs) = x :: xs
||| Check whether a list is non-empty
export
fromList : (1 xs : List a) -> Maybe (List1 a)
fromList [] = Nothing
fromList (x :: xs) = Just (x :: xs)
fromList (x :: xs) = Just (x ::: xs)
------------------------------------------------------------------------
-- Basic functions
public export
singleton : (1 x : a) -> List1 a
singleton a = a ::: []
export
last : List1 a -> a
last (x ::: xs) = loop x xs where
loop : a -> List a -> a
loop x [] = x
loop _ (x :: xs) = loop x xs
export
foldr1' : (a -> b -> b) -> (a -> b) -> List1 a -> b
foldr1' c n (x ::: xs) = loop x xs where
loop : a -> List a -> b
loop a [] = n a
loop a (x :: xs) = c a (loop x xs)
export
foldr1 : (a -> a -> a) -> List1 a -> a
foldr1 c = foldr1' c id
export
foldl1 : (a -> b) -> (b -> a -> b) -> List1 a -> b
foldl1 n c (x ::: xs) = foldl c (n x) xs
------------------------------------------------------------------------
-- Append
export
appendl : (1 xs : List1 a) -> (1 ys : List a) -> List1 a
appendl (x :: xs) ys = x :: xs ++ ys
appendl (x ::: xs) ys = x ::: xs ++ ys
export
append : (1 xs, ys : List1 a) -> List1 a
append xs ys = appendl xs (toList ys)
append xs ys = appendl xs (forget ys)
export
lappend : (1 xs : List a) -> (1 ys : List1 a) -> List1 a
lappend [] ys = ys
lappend (x :: xs) ys = append (x :: xs) ys
lappend (x :: xs) ys = append (x ::: xs) ys
------------------------------------------------------------------------
-- Cons/Snoc
public export
cons : (1 x : a) -> (1 xs : List1 a) -> List1 a
cons x xs = x ::: forget xs
export
snoc : (1 xs : List1 a) -> (1 x : a) -> List1 a
snoc xs x = append xs (singleton x)
------------------------------------------------------------------------
-- Reverse
public export
reverseOnto : (1 acc : List1 a) -> (1 xs : List a) -> List1 a
reverseOnto acc [] = acc
reverseOnto acc (x :: xs) = reverseOnto (x ::: forget acc) xs
public export
reverse : (1 xs : List1 a) -> List1 a
reverse (x ::: xs) = reverseOnto (singleton x) xs
------------------------------------------------------------------------
-- Instances
export
Semigroup (List1 a) where
(<+>) = append
export
Functor List1 where
map f (x :: xs) = f x :: map f xs
export
Foldable List1 where
foldr c n (x :: xs) = c x (foldr c n xs)
export
Show a => Show (List1 a) where
show = show . toList
map f (x ::: xs) = f x ::: map f xs
export
Applicative List1 where
pure x = [x]
f :: fs <*> xs = appendl (map f xs) (fs <*> toList xs)
pure x = singleton x
f ::: fs <*> xs = appendl (map f xs) (fs <*> forget xs)
export
Monad List1 where
(x :: xs) >>= f = appendl (f x) (xs >>= toList . f)
(x ::: xs) >>= f = appendl (f x) (xs >>= forget . f)
export
Foldable List1 where
foldr c n (x ::: xs) = c x (foldr c n xs)
export
Show a => Show (List1 a) where
show = show . forget
export
Eq a => Eq (List1 a) where
(x ::: xs) == (y ::: ys) = x == y && xs == ys
export
Ord a => Ord (List1 a) where
compare xs ys = compare (forget xs) (forget ys)
------------------------------------------------------------------------
-- Properties
export
consInjective : the (List1 a) (x ::: xs) === (y ::: ys) -> (x === y, xs === ys)
consInjective Refl = (Refl, Refl)

6
libs/base/Data/Nat.idr
View File

@ -159,7 +159,7 @@ maximum (S n) (S m) = S (maximum n m)
-- Proofs on S
export
eqSucc : (left, right : Nat) -> left = right -> S left = S right
eqSucc : (0 left, right : Nat) -> left = right -> S left = S right
eqSucc _ _ Refl = Refl
export
@ -187,11 +187,13 @@ export partial
modNat : Nat -> Nat -> Nat
modNat left (S right) = modNatNZ left (S right) SIsNotZ
export partial
-- 'public' to allow type-level division
public export total
divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
divNatNZ left Z p = void (p Refl)
divNatNZ left (S right) _ = div' left left right
where
public export
div' : Nat -> Nat -> Nat -> Nat
div' Z centre right = Z
div' (S left) centre right =

2
libs/base/Data/Nat/Order.idr
View File

@ -47,7 +47,7 @@ total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
zeroAlwaysSmaller = LTEZero
public export
total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void
total ltesuccinjective : {0 n : Nat} -> {0 m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void
ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = void (disprf nLTEm)
ltesuccinjective {n} {m} disprf LTEZero impossible

1
libs/base/Data/Rel.idr
View File

@ -31,6 +31,7 @@ All (t :: ts) p = (x : t) -> All ts (p x)
||| ```
||| Which is the type of a pair of natural numbers along with a proof that the first
||| is smaller or equal than the second.
public export
Ex : (ts : Vect n Type) -> (p : Rel ts) -> Type
Ex [] p = p
Ex (t :: ts) p = (x : t ** Ex ts (p x))

14
libs/base/Data/Strings.idr
View File

@ -301,29 +301,29 @@ parseDouble = mkDouble . wfe . trim
wfe : String -> Maybe (Double, Double, Integer)
wfe cs = case split (== '.') cs of
(wholeAndExp :: []) =>
(wholeAndExp ::: []) =>
case split (\c => c == 'e' || c == 'E') wholeAndExp of
(whole::exp::[]) =>
(whole:::exp::[]) =>
do
w <- cast {from=Integer} <$> parseInteger whole
e <- parseInteger exp
pure (w, 0, e)
(whole::[]) =>
(whole:::[]) =>
do
w <- cast {from=Integer} <$> parseInteger whole
pure (w, 0, 0)
_ => Nothing
(whole::fracAndExp::[]) =>
(whole:::fracAndExp::[]) =>
case split (\c => c == 'e' || c == 'E') fracAndExp of
(""::exp::[]) => Nothing
(frac::exp::[]) =>
("":::exp::[]) => Nothing
(frac:::exp::[]) =>
do
w <- cast {from=Integer} <$> parseInteger whole
f <- (/ (natpow 10 (length frac))) <$>
(cast <$> parseNumWithoutSign (unpack frac) 0)
e <- parseInteger exp
pure (w, if w < 0 then (-f) else f, e)
(frac::[]) =>
(frac:::[]) =>
do
w <- cast {from=Integer} <$> parseInteger whole
f <- (/ (natpow 10 (length frac))) <$>

8
libs/base/Data/Vect.idr
View File

@ -219,6 +219,14 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
-- Conversion from list (toList is provided by Foldable)
--------------------------------------------------------------------------------
public export
toVect : (n : Nat) -> List a -> Maybe (Vect n a)
toVect Z [] = Just []
toVect (S k) (x :: xs)
= do xs' <- toVect k xs
pure (x :: xs')
toVect _ _ = Nothing
public export
fromList' : (1 xs : Vect len elem) -> (1 l : List elem) -> Vect (length l + len) elem
fromList' ys [] = ys

1
libs/base/Decidable/Decidable.idr
View File

@ -4,6 +4,7 @@ import Data.Rel
import Data.Fun
||| Interface for decidable n-ary Relations
public export
interface Decidable (ts : Vect k Type) (p : Rel ts) where

15
libs/base/Decidable/Equality.idr
View File

@ -4,6 +4,7 @@ import Data.Maybe
import Data.Either
import Data.Nat
import Data.List
import Data.List1
%default total
@ -134,6 +135,20 @@ DecEq a => DecEq (List a) where
decEq (x :: xs) (x :: ys) | (Yes Refl) | (No contra) =
No $ contra . snd . consInjective
--------------------------------------------------------------------------------
-- List1
--------------------------------------------------------------------------------
export
DecEq a => DecEq (List1 a) where
decEq (x ::: xs) (y ::: ys) with (decEq x y)
decEq (x ::: xs) (y ::: ys) | No contra = No (contra . fst . consInjective)
decEq (x ::: xs) (y ::: ys) | Yes eqxy with (decEq xs ys)
decEq (x ::: xs) (y ::: ys) | Yes eqxy | No contra = No (contra . snd . consInjective)
decEq (x ::: xs) (y ::: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (:::) eqxy eqxsys)
-- TODO: Other prelude data types
-- For the primitives, we have to cheat because we don't have access to their

23
libs/base/Language/Reflection/TT.idr
View File

@ -46,20 +46,28 @@ data Constant
| DoubleType
| WorldType
public export
data Namespace = MkNS (List String) -- namespace, stored in reverse order
export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
export
Show Namespace where
show (MkNS ns) = showSep "." (reverse ns)
public export
data Name = UN String -- user defined name
| MN String Int -- machine generated name
| NS (List String) Name -- name in a namespace
| NS Namespace Name -- name in a namespace
| DN String Name -- a name and how to display it
export
Show Name where
show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n
where
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
show (NS ns n) = show ns ++ "." ++ show n
show (UN x) = x
show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
show (DN str y) = str
@ -107,4 +115,3 @@ data TotalReq = Total | CoveringOnly | PartialOK
public export
data Visibility = Private | Export | Public

2
libs/base/Language/Reflection/TTImp.idr
View File

@ -97,7 +97,7 @@ mutual
GlobalHint : Bool -> FnOpt
ExternFn : FnOpt
-- Defined externally, list calling conventions
ForeignFn : List String -> FnOpt
ForeignFn : List TTImp -> FnOpt
-- assume safe to cancel arguments in unification
Invertible : FnOpt
Totalty : TotalReq -> FnOpt

116
libs/contrib/Data/Fun/Extra.idr Normal file
View File

@ -0,0 +1,116 @@
module Data.Fun.Extra
import Data.Fun
import Data.Rel
import Data.HVect
%default total
||| Apply an n-ary function to an n-ary tuple of inputs
public export
uncurry : {0 n : Nat} -> {0 ts : Vect n Type} -> Fun ts cod -> HVect ts -> cod
uncurry f [] = f
uncurry f (x::xs) = uncurry (f x) xs
||| Apply an n-ary function to an n-ary tuple of inputs
public export
curry : {n : Nat} -> {0 ts : Vect n Type} -> (HVect ts -> cod) -> Fun ts cod
curry {ts = [] } f = f []
curry {ts = _ :: _} f = \x => curry (\xs => f (x :: xs))
{-
The higher kind Type -> Type has a monoid structure given by
composition and the identity (Cayley). The type (n : Nat ** Vect n a)
has a monoid structure given by `(n, rs) * (m, ss) := (n + m, rs +
ss)` and `(0,[])`.
`Fun' : (n : Nat ** Vect n Type) -> Type -> Type`
is then a monoid homomorphism between them. I guess this is some
instance of Cayley's theorem, but because of extensionality we can't
show we have an isomorphism.
-}
public export
homoFunNeut_ext : Fun [] cod -> id cod
homoFunNeut_ext x = x
public export
homoFunMult_ext : {n : Nat} -> {0 rs : Vect n Type} -> Fun (rs ++ ss) cod -> (Fun rs . Fun ss) cod
homoFunMult_ext {rs = [] } gs = gs
homoFunMult_ext {rs = t :: ts} fgs = \x => homoFunMult_ext (fgs x)
public export
homoFunNeut_inv : id cod -> Fun [] cod
homoFunNeut_inv x = x
public export
homoFunMult_inv : {n : Nat} -> {0 rs : Vect n Type} -> (Fun rs . Fun ss) cod -> Fun (rs ++ ss) cod
homoFunMult_inv {rs = [] } gs = gs
homoFunMult_inv {rs = t :: ts} fgs = \x => homoFunMult_inv (fgs x)
||| Apply an n-ary function to an n-ary tuple of inputs
public export
applyPartially : {n : Nat} -> {0 ts : Vect n Type}
-> Fun (ts ++ ss) cod -> (HVect ts -> Fun ss cod)
applyPartially fgs = uncurry {ts} {cod = Fun ss cod} (homoFunMult_ext {rs=ts} {ss} fgs)
{- -------- (slightly) dependent versions of the above ---------------
As usual, type dependencies make everything complicated -}
||| Apply an n-ary dependent function to its tuple of inputs (given by an HVect)
public export
uncurryAll : {0 n : Nat} -> {0 ts : Vect n Type} -> {0 cod : Fun ts Type}
-> All ts cod -> (xs : HVect ts) -> uncurry cod xs
uncurryAll f [] = f
uncurryAll {ts = t :: ts} f (x :: xs) = uncurryAll {cod= cod x} (f x) xs
public export
curryAll : {n : Nat} -> {0 ts : Vect n Type} -> {0 cod : Fun ts Type}
-> ((xs : HVect ts) -> uncurry cod xs)
-> All ts cod
curryAll {ts = [] } f = f []
curryAll {ts = t :: ts} f = \x => curryAll (\ xs => f (x:: xs))
chainGenUncurried : {n : Nat} -> {0 ts : Vect n Type} -> {0 cod,cod' : Fun ts Type} ->
((xs : HVect ts) -> uncurry cod xs -> uncurry cod' xs) ->
All ts cod -> All ts cod'
chainGenUncurried {ts = []} f gs = f [] gs
chainGenUncurried {ts = (t :: ts)} f gs = \x => chainGenUncurried (\u => f (x :: u)) (gs x)
public export
homoAllNeut_ext : Fun [] cod -> id cod
homoAllNeut_ext x = x
-- Not sure it's worth it getting the rest of Cayley's theorem to work
public export
extractWitness : {n : Nat} -> {0 ts : Vect n Type} -> {0 r : Rel ts} -> Ex ts r -> HVect ts
extractWitness {ts = [] } _ = []
extractWitness {ts = t :: ts} (w ** f) = w :: extractWitness f
public export
extractWitnessCorrect : {n : Nat} -> {0 ts : Vect n Type} -> {0 r : Rel ts} -> (f : Ex ts r) ->
uncurry {ts} r (extractWitness {r} f)
extractWitnessCorrect {ts = [] } f = f
extractWitnessCorrect {ts = t :: ts} (w ** f) = extractWitnessCorrect f
public export
introduceWitness : {0 r : Rel ts} -> (witness : HVect ts) ->
uncurry {ts} r witness -> Ex ts r
introduceWitness [] f = f
introduceWitness (w :: witness) f = (w ** introduceWitness witness f)
----------------------------------------------------------------------
public export
data Pointwise : (r : a -> b -> Type) -> (ts : Vect n a) -> (ss : Vect n b) -> Type where
Nil : Pointwise r [] []
(::) : {0 ss, ts : Vect n Type} ->
(f : r t s) -> Pointwise r ts ss -> Pointwise r (t::ts) (s::ss)
public export
precompose : Pointwise (\a,b => a -> b) ts ss -> Fun ss cod -> Fun ts cod
precompose [] h = h
precompose (f :: fs) h = \x => precompose fs (h (f x))

4
libs/contrib/Data/HVect.idr
View File

@ -79,11 +79,11 @@ public export
(x :: xs) == (y :: ys) = x == y && xs == ys
public export
consInjective1 : {xs, ys: HVect ts} -> {x, y: a} -> (1 _ : x :: xs = y :: ys) -> x = y
consInjective1 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (1 _ : x :: xs = y :: ys) -> x = y
consInjective1 Refl = Refl
public export
consInjective2 : {xs, ys: HVect ts} -> {x, y: a} -> (1 _ : x :: xs = y :: ys) -> xs = ys
consInjective2 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (1 _ : x :: xs = y :: ys) -> xs = ys
consInjective2 Refl = Refl
public export

2
libs/contrib/Data/List/TailRec.idr
View File

@ -122,7 +122,7 @@ break_ext p xs = span_ext (not . p) xs
splitOnto : List (List a) -> (a -> Bool) -> List a -> List1 (List a)
splitOnto acc p xs =
case Data.List.break p xs of
(chunk, [] ) => reverseOnto [chunk] acc
(chunk, [] ) => reverseOnto (chunk ::: []) acc
(chunk, (c::rest)) => splitOnto (chunk::acc) p rest
export

2
libs/contrib/Data/String/Parser/Expression.idr
View File

@ -116,6 +116,6 @@ buildExpressionParser a operators simpleExpr =
rassocP = mkRassocP amLeft amNon rassocOp termP
lassocP = mkLassocP amRight amNon lassocOp termP
nassocP = mkNassocP amRight amLeft amNon nassocOp termP
in
in
do x <- termP
rassocP x <|> lassocP x <|> nassocP x <|> pure x <?> "operator"

9
libs/contrib/Data/Void.idr Normal file
View File

@ -0,0 +1,9 @@
module Data.Void
export
absurdity : Uninhabited t => (0 _ : t) -> s
absurdity x = void (uninhabited x)
export
contradiction : (Uninhabited t) => (0 _ : x -> t) -> (x -> s)
contradiction since x = absurdity (since x)

50
libs/contrib/Decidable/Decidable/Extra.idr Normal file
View File

@ -0,0 +1,50 @@
module Decidable.Decidable.Extra
import Data.Rel
import Data.Fun
import Data.Vect
import Data.HVect
import Data.Fun.Extra
import Decidable.Decidable
public export
NotNot : {n : Nat} -> {ts : Vect n Type} -> (r : Rel ts) -> Rel ts
NotNot r = map @{Nary} (Not . Not) r
[DecidablePartialApplication] {x : t} -> (tts : Decidable (t :: ts) r) => Decidable ts (r x) where
decide = decide @{tts} x
public export
doubleNegationElimination : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
(witness : HVect ts) ->
uncurry (NotNot {ts} r) witness ->
uncurry r witness
doubleNegationElimination {ts = [] } @{dec} [] prfnn =
case decide @{dec} of
Yes prf => prf
No prfn => absurd $ prfnn prfn
doubleNegationElimination {ts = t :: ts} @{dec} (w :: witness) prfnn =
doubleNegationElimination {ts} {r = r w} @{ DecidablePartialApplication @{dec} } witness prfnn
doubleNegationForall : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
All ts (NotNot {ts} r) -> All ts r
doubleNegationForall @{dec} forall_prf =
let prfnn : (witness : HVect ts) -> uncurry (NotNot {ts} r) witness
prfnn = uncurryAll forall_prf
prf : (witness : HVect ts) -> uncurry r witness
prf witness = doubleNegationElimination @{dec} witness (prfnn witness)
in curryAll prf
public export
doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
Ex ts (NotNot {ts} r) ->
Ex ts r
doubleNegationExists {ts} {r} @{dec} nnxs =
let witness : HVect ts
witness = extractWitness nnxs
witnessingnn : uncurry (NotNot {ts} r) witness
witnessingnn = extractWitnessCorrect nnxs
witnessing : uncurry r witness
witnessing = doubleNegationElimination @{dec} witness witnessingnn
in introduceWitness witness witnessing

84
libs/contrib/Decidable/Order/Strict.idr Normal file
View File

@ -0,0 +1,84 @@
||| An strict preorder (sometimes known as a quasi-order, or an
||| ordering) is what you get when you remove the diagonal `{(a,b) | a
||| r b , b r a}` from a preorder. For example a < b is an ordering.
||| This module extends base's Decidable.Order with the strict versions.
||| The interface system seems to struggle a bit with some of the constructions,
||| so I hacked them a bit. Sorry.
module Decidable.Order.Strict
import Decidable.Order
import Decidable.Equality
%default total
public export
interface StrictPreorder t (spo : t -> t -> Type) where
transitive : (a, b, c : t) -> a `spo` b -> b `spo` c -> a `spo` c
irreflexive : (a : t) -> Not (a `spo` a)
public export
asymmetric : StrictPreorder t spo => (a, b : t) -> a `spo` b -> Not (b `spo` a)
asymmetric a b aLTb bLTa = irreflexive a $
Strict.transitive a b a aLTb bLTa
public export
EqOr : (spo : t -> t -> Type) -> StrictPreorder t spo => (a,b : t) -> Type
EqOr spo a b = Either (a = b) (a `spo` b)
-- Can generalise to an arbitrary equivalence, I belive
public export
[MkPreorder] {spo : t -> t -> Type} -> StrictPreorder t spo => Preorder t (EqOr spo) where
reflexive a = Left Refl
transitive a _ c (Left Refl) bLTEc = bLTEc
transitive a b _ (Right aLTb) (Left Refl) = Right aLTb
transitive a b c (Right aLTb) (Right bLTc) = Right $ Strict.transitive a b c aLTb bLTc
[MkPoset] {antisym : (a,b : t) -> a `leq` b -> b `leq` a -> a = b} -> Preorder t leq => Poset t leq where
antisymmetric = antisym
%hint
public export
InferPoset : {t : Type} -> {spo : t -> t -> Type} -> StrictPreorder t spo => Poset t (EqOr spo)
InferPoset {t} {spo} = MkPoset @{MkPreorder} {antisym = antisym}
where
antisym : (a,b : t) -> EqOr spo a b -> EqOr spo b a -> a = b
antisym a a (Left Refl) (Left Refl) = Refl
antisym a a (Left Refl) (Right bLTa) = absurd (irreflexive a bLTa)
antisym b b (Right aLTb) (Left Refl) = absurd (irreflexive b aLTb)
antisym a b (Right aLTb) (Right bLTa) = absurd (asymmetric a b aLTb bLTa)
public export
data DecOrdering : {lt : t -> t -> Type} -> (a,b : t) -> Type where
DecLT : forall lt . (a `lt` b) -> DecOrdering {lt = lt} a b
DecEQ : forall lt . (a = b) -> DecOrdering {lt = lt} a b
DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b
public export
interface StrictPreorder t spo => StrictOrdered t (spo : t -> t -> Type) where
order : (a,b : t) -> DecOrdering {lt = spo} a b
[MkOrdered] {ord : (a,b : t) -> Either (a `leq` b) (b `leq` a)} -> Poset t leq => Ordered t leq where
order = ord
%hint
public export
InferOrder : {t : Type} -> {spo : t -> t -> Type} -> StrictOrdered t spo => Ordered t (EqOr spo)
InferOrder {t} {spo} @{so} = MkOrdered @{InferPoset} {ord = ord}
where
ord : (a,b : t) -> Either (EqOr spo a b) (EqOr spo b a)
ord a b with (Strict.order @{so} a b)
ord a _ | DecEQ Refl = Left (Left Refl)
ord a b | DecLT aLTb = Left (Right aLTb)
ord a b | DecGT bLTa = Right (Right bLTa)
public export
(tot : StrictOrdered t lt) => (pre : StrictPreorder t lt) => DecEq t where
decEq x y = case order @{tot} x y of
DecEQ x_eq_y => Yes x_eq_y
DecLT xlty => No $ \x_eq_y => absurd $ irreflexive @{pre} y
$ replace {p = \u => u `lt` y} x_eq_y xlty
-- Similarly
DecGT yltx => No $ \x_eq_y => absurd $ irreflexive @{pre} y
$ replace {p = \u => y `lt` u} x_eq_y yltx

7
libs/contrib/contrib.ipkg
View File

@ -25,6 +25,8 @@ modules = Control.ANSI,
Data.Fin.Extra,
Data.Fun.Extra,
Data.Logic.Propositional,
Data.Morphisms.Algebra,
@ -46,10 +48,15 @@ modules = Control.ANSI,
Data.Vect.Sort,
Data.Void,
Data.HVect,
Debug.Buffer,
Decidable.Order.Strict,
Decidable.Decidable.Extra,
Language.JSON,
Language.JSON.Data,
Language.JSON.Lexer,

4
libs/network/Network/Socket/Data.idr
View File

@ -186,8 +186,8 @@ export
parseIPv4 : String -> SocketAddress
parseIPv4 str =
case splitted of
(i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
otherwise => InvalidAddress
(i1 ::: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
_ => InvalidAddress
where
toInt' : String -> Integer
toInt' = cast

6
libs/prelude/Prelude/Basics.idr
View File

@ -107,6 +107,12 @@ public export
(||) True x = True
(||) False x = x
||| Non-dependent if-then-else
public export
ifThenElse : (1 b : Bool) -> Lazy a -> Lazy a -> a
ifThenElse True l r = l
ifThenElse False l r = r
%inline
public export
intToBool : Int -> Bool

4
libs/prelude/Prelude/EqOrd.idr
View File

@ -106,6 +106,10 @@ interface Eq ty => Ord ty where
min : ty -> ty -> ty
min x y = if (x < y) then x else y
export
comparing : Ord a => (b -> a) -> b -> b -> Ordering
comparing p x y = compare (p x) (p y)
public export
Ord Void where
compare _ _ impossible

28
libs/prelude/Prelude/Interfaces.idr
View File

@ -2,6 +2,7 @@ module Prelude.Interfaces
import Builtin
import Prelude.Basics
import Prelude.EqOrd
import Prelude.Num
import Prelude.Ops
@ -33,6 +34,33 @@ public export
interface Semigroup ty => Monoid ty where
neutral : ty
public export
Semigroup () where
_ <+> _ = ()
public export
Monoid () where
neutral = ()
public export
Semigroup Ordering where
LT <+> _ = LT
GT <+> _ = GT
EQ <+> o = o
public export
Monoid Ordering where
neutral = EQ
public export
Semigroup b => Semigroup (a -> b) where
(f <+> g) x = f x <+> g x
public export
Monoid b => Monoid (a -> b) where
neutral _ = neutral
export
shiftL : Int -> Int -> Int
shiftL = prim__shl_Int

5
libs/prelude/PrimIO.idr
View File

@ -62,11 +62,6 @@ data GCAnyPtr : Type where [external]
public export
data ThreadID : Type where [external]
public export
data FArgList : Type where
Nil : FArgList
(::) : {a : Type} -> (1 arg : a) -> (1 args : FArgList) -> FArgList
export %inline
fromPrim : (1 fn : (1 x : %World) -> IORes a) -> IO a
fromPrim op = MkIO op

4
src/Algebra.idr
View File

@ -9,3 +9,7 @@ import public Algebra.Preorder
public export
RigCount : Type
RigCount = ZeroOneOmega
export
showCount : RigCount -> String
showCount = elimSemi "0 " "1 " (const "")

6
src/Compiler/ANF.idr
View File

@ -156,12 +156,6 @@ letBind fc args f
= ALet fc i t (doBind (ALocal i :: vs) xs)
doBind vs ((var, _) :: xs) = doBind (var :: vs) xs
toVect : (n : Nat) -> List a -> Maybe (Vect n a)
toVect Z [] = Just []
toVect (S k) (x :: xs)
= do xs' <- toVect k xs
pure (x :: xs')
toVect _ _ = Nothing
mlet : {auto v : Ref Next Int} ->
FC -> ANF -> (AVar -> ANF) -> Core ANF

5
src/Compiler/Common.idr
View File

@ -7,6 +7,7 @@ import Compiler.LambdaLift
import Compiler.VMCode
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Options
import Core.TT
@ -179,8 +180,8 @@ natHackNames
= [UN "prim__add_Integer",
UN "prim__sub_Integer",
UN "prim__mul_Integer",
NS ["Prelude"] (UN "natToInteger"),
NS ["Prelude"] (UN "integerToNat")]
NS preludeNS (UN "natToInteger"),
NS preludeNS (UN "integerToNat")]
-- Hmm, these dump functions are all very similar aren't they...
dumpCases : Defs -> String -> List Name ->

115
src/Compiler/CompileExpr.idr
View File

@ -135,38 +135,73 @@ mkDropSubst i es rest (x :: xs)
-- NOTE: Make sure that names mentioned here are listed in 'natHackNames' in
-- Common.idr, so that they get compiled, as they won't be spotted by the
-- usual calls to 'getRefs'.
data Magic : Type where
MagicCCon : Namespace -> String -> (arity : Nat) -> -- checks
(FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> -- translation
Magic
MagicCRef : Namespace -> String -> (arity : Nat) -> -- checks
(FC -> FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> --translation
Magic
magic : List Magic -> CExp vars -> CExp vars
magic ms (CLam fc x exp) = CLam fc x (magic ms exp)
magic ms e = go ms e where
fire : Magic -> CExp vars -> Maybe (CExp vars)
fire (MagicCCon ns n arity f) (CCon fc (NS ns' (UN n')) _ es)
= do guard (n == n' && ns == ns')
map (f fc) (toVect arity es)
fire (MagicCRef ns n arity f) (CApp fc (CRef fc' (NS ns' (UN n'))) es)
= do guard (n == n' && ns == ns')
map (f fc fc') (toVect arity es)
fire _ _ = Nothing
go : List Magic -> CExp vars -> CExp vars
go [] e = e
go (m :: ms) e = case fire m e of
Nothing => go ms e
Just e' => e'
natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
natMinus fc fc' [m,n] = CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, n]
natHack : CExp vars -> CExp vars
natHack (CCon fc (NS ["Types", "Prelude"] (UN "Z")) _ []) = CPrimVal fc (BI 0)
natHack (CCon fc (NS ["Types", "Prelude"] (UN "S")) _ [k])
= CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k]
natHack (CApp fc (CRef _ (NS ["Types", "Prelude"] (UN "natToInteger"))) [k]) = k
natHack (CApp fc (CRef _ (NS ["Types", "Prelude"] (UN "integerToNat"))) [k]) = k
natHack (CApp fc (CRef fc' (NS ["Types", "Prelude"] (UN "plus"))) args)
= CApp fc (CRef fc' (UN "prim__add_Integer")) args
natHack (CApp fc (CRef fc' (NS ["Types", "Prelude"] (UN "mult"))) args)
= CApp fc (CRef fc' (UN "prim__mul_Integer")) args
natHack (CApp fc (CRef fc' (NS ["Nat", "Data"] (UN "minus"))) args)
= CApp fc (CRef fc' (UN "prim__sub_Integer")) args
natHack (CLam fc x exp) = CLam fc x (natHack exp)
natHack t = t
natHack = magic
[ MagicCCon typesNS "Z" 0
(\ fc, [] => CPrimVal fc (BI 0))
, MagicCCon typesNS "S" 1
(\ fc, [k] => CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k])
, MagicCRef typesNS "natToINteger" 1
(\ _, _, [k] => k)
, MagicCRef typesNS "integerToNat" 1
(\ _, _, [k] => k)
, MagicCRef typesNS "plus" 2
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n])
, MagicCRef typesNS "mult" 2
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n])
, MagicCRef natNS "minus" 2 natMinus
]
isNatCon : Name -> Bool
isNatCon (NS ["Types", "Prelude"] (UN "Z")) = True
isNatCon (NS ["Types", "Prelude"] (UN "S")) = True
isNatCon (NS ns (UN n))
= (n == "Z" || n == "S") && ns == typesNS
isNatCon _ = False
natBranch : CConAlt vars -> Bool
natBranch (MkConAlt n _ _ _) = isNatCon n
trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
trySBranch n (MkConAlt (NS ["Types", "Prelude"] (UN "S")) _ [arg] sc)
= let fc = getFC n in
Just (CLet fc arg True (CApp fc (CRef fc (UN "prim__sub_Integer"))
[n, CPrimVal fc (BI 1)]) sc)
trySBranch n (MkConAlt (NS ns (UN nm)) _ [arg] sc)
= do guard (nm == "S" && ns == typesNS)
let fc = getFC n
pure (CLet fc arg True (natMinus fc fc [n, CPrimVal fc (BI 1)]) sc)
trySBranch _ _ = Nothing
tryZBranch : CConAlt vars -> Maybe (CExp vars)
tryZBranch (MkConAlt (NS ["Types", "Prelude"] (UN "Z")) _ [] sc) = Just sc
tryZBranch (MkConAlt (NS ns (UN n)) _ [] sc)
= do guard (n == "Z" && ns == typesNS)
pure sc
tryZBranch _ = Nothing
getSBranch : CExp vars -> List (CConAlt vars) -> Maybe (CExp vars)
@ -189,7 +224,13 @@ natHackTree (CConCase fc sc alts def)
natHackTree t = t
-- Rewrite case trees on Bool/Ord to be case trees on Integer
-- TODO: Generalise to all enumerations
-- TODO: Generalise to all finite enumerations
isFiniteEnum : Name -> Bool
isFiniteEnum (NS ns (UN n))
= ((n == "True" || n == "False") && ns == basicsNS) -- booleans
|| ((n == "LT" || n == "EQ" || n == "GT") && ns == eqOrdNS) -- comparison
isFiniteEnum _ = False
boolHackTree : CExp vars -> CExp vars
boolHackTree (CConCase fc sc alts def)
= let x = traverse toBool alts
@ -198,16 +239,9 @@ boolHackTree (CConCase fc sc alts def)
CConstCase fc sc alts' def
where
toBool : CConAlt vars -> Maybe (CConstAlt vars)
toBool (MkConAlt (NS ["Basics", "Prelude"] (UN "True")) (Just tag) [] sc)
= Just $ MkConstAlt (I tag) sc
toBool (MkConAlt (NS ["Basics", "Prelude"] (UN "False")) (Just tag) [] sc)
= Just $ MkConstAlt (I tag) sc
toBool (MkConAlt (NS ["EqOrd", "Prelude"] (UN "LT")) (Just tag) [] sc)
= Just $ MkConstAlt (I tag) sc
toBool (MkConAlt (NS ["EqOrd", "Prelude"] (UN "EQ")) (Just tag) [] sc)
= Just $ MkConstAlt (I tag) sc
toBool (MkConAlt (NS ["EqOrd", "Prelude"] (UN "GT")) (Just tag) [] sc)
= Just $ MkConstAlt (I tag) sc
toBool (MkConAlt nm (Just tag) [] sc)
= do guard (isFiniteEnum nm)
pure $ MkConstAlt (I tag) sc
toBool _ = Nothing
boolHackTree t = t
@ -217,21 +251,12 @@ mutual
Name -> Term vars -> Core (CExp vars)
toCExpTm n (Local fc _ _ prf)
= pure $ CLocal fc prf
-- TMP HACK: extend this to all types which look like enumerations
-- after erasure
toCExpTm n (Ref fc (DataCon tag Z) (NS ["Basics", "Prelude"] (UN "True")))
= pure $ CPrimVal fc (I tag)
toCExpTm n (Ref fc (DataCon tag Z) (NS ["Basics", "Prelude"] (UN "False")))
= pure $ CPrimVal fc (I tag)
toCExpTm n (Ref fc (DataCon tag Z) (NS ["EqOrd", "Prelude"] (UN "LT")))
= pure $ CPrimVal fc (I tag)
toCExpTm n (Ref fc (DataCon tag Z) (NS ["EqOrd", "Prelude"] (UN "EQ")))
= pure $ CPrimVal fc (I tag)
toCExpTm n (Ref fc (DataCon tag Z) (NS ["EqOrd", "Prelude"] (UN "GT")))
= pure $ CPrimVal fc (I tag)
-- TMP HACK: extend this to all types which look like enumerations after erasure
toCExpTm n (Ref fc (DataCon tag arity) fn)
= -- get full name for readability, and the Nat hack
pure $ CCon fc !(getFullName fn) (Just tag) []
= if arity == Z && isFiniteEnum fn
then pure $ CPrimVal fc (I tag)
else -- get full name for readability, and the Nat hack
pure $ CCon fc !(getFullName fn) (Just tag) []
toCExpTm n (Ref fc (TyCon tag arity) fn)
= pure $ CCon fc fn Nothing []
toCExpTm n (Ref fc _ fn)

3
src/Compiler/ES/ES.idr
View File

@ -87,7 +87,7 @@ keywordSafe "var" = "var_"
keywordSafe s = s
jsName : Name -> String
jsName (NS ns n) = showSep "_" (reverse ns) ++ "_" ++ jsName n
jsName (NS ns n) = showNSWithSep "_" ns ++ "_" ++ jsName n
jsName (UN n) = keywordSafe $ jsIdent n
jsName (MN n i) = jsIdent n ++ "_" ++ show i
jsName (PV n d) = "pat__" ++ jsName n
@ -416,7 +416,6 @@ mutual
static_preamble : List String
static_preamble =
[ "class IdrisError extends Error { }"
, "function __prim_idris2js_FArgList(x){if(x.h === 0){return []}else{return x.a2.concat(__prim_idris2js_FArgList(x.a3))}}"
, "function __prim_js2idris_array(x){if(x.length ===0){return {h:0}}else{return {h:1,a1:x[0],a2: __prim_js2idris_array(x.slice(1))}}}"
, "function __prim_idris2js_array(x){const result = Array();while (x.h != 0) {result.push(x.a1); x = x.a2;}return result;}"
]

3
src/Compiler/ES/Imperative.idr
View File

@ -54,9 +54,6 @@ genName =
pure $ MN "imp_gen" i
mutual
ifThenElse : Bool -> a -> a -> a
ifThenElse True t e = t
ifThenElse False t e = e
pairToReturn : (toReturn : Bool) -> (ImperativeStatement, ImperativeExp) ->
Core (ifThenElse toReturn ImperativeStatement (ImperativeStatement, ImperativeExp))

37
src/Compiler/Inline.idr
View File

@ -4,10 +4,12 @@ import Compiler.CompileExpr
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.FC
import Core.TT
import Data.LengthMatch
import Data.Maybe
import Data.NameMap
import Data.List
import Data.Vect
@ -145,24 +147,25 @@ mutual
-- in case they duplicate work. We should fix that, to decide more accurately
-- whether they're safe to inline, but until then this gives such a huge
-- boost by removing unnecessary lambdas that we'll keep the special case.
eval rec env (_ :: _ :: act :: cont :: world :: stk)
(CRef fc (NS ["PrimIO"] (UN "io_bind")))
= do xn <- genName "act"
sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])
pure $ unload stk $
CLet fc xn False (CApp fc act [world])
(refToLocal xn xn sc)
eval rec env stk (CRef fc n)
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure (unload stk (CRef fc n))
let Just def = compexpr gdef
| Nothing => pure (unload stk (CRef fc n))
let arity = getArity def
if (Inline `elem` flags gdef) && (not (n `elem` rec))
then do ap <- tryApply (n :: rec) stk env def
pure $ maybe (unloadApp arity stk (CRef fc n)) id ap
else pure $ unloadApp arity stk (CRef fc n)
= case (n == NS primIONS (UN "io_bind"), stk) of
(True, _ :: _ :: act :: cont :: world :: stk) =>
do xn <- genName "act"
sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])
pure $ unload stk $
CLet fc xn False (CApp fc act [world])
(refToLocal xn xn sc)
(_,_) =>
do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure (unload stk (CRef fc n))
let Just def = compexpr gdef
| Nothing => pure (unload stk (CRef fc n))
let arity = getArity def
if (Inline `elem` flags gdef) && (not (n `elem` rec))
then do ap <- tryApply (n :: rec) stk env def
pure $ fromMaybe (unloadApp arity stk (CRef fc n)) ap
else pure $ unloadApp arity stk (CRef fc n)
eval {vars} {free} rec env [] (CLam fc x sc)
= do xn <- genName "lamv"
sc' <- eval rec (CRef fc xn :: env) [] sc

11
src/Compiler/Scheme/Chez.idr
View File

@ -6,6 +6,7 @@ import Compiler.Inline
import Compiler.Scheme.Common
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Name
import Core.Options
@ -30,7 +31,7 @@ import System.Info
pathLookup : IO String
pathLookup
= do path <- getEnv "PATH"
let pathList = List1.toList $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
let candidates = [p ++ "/" ++ x | p <- pathList,
x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
e <- firstExists candidates
@ -269,11 +270,13 @@ schemeCall fc sfn argns ret
useCC : {auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
String -> FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
useCC appdir fc [] args ret
= throw (GenericMsg fc "No recognised foreign calling convention")
useCC appdir fc [] args ret = throw (NoForeignCC fc)
useCC appdir fc (cc :: ccs) args ret
= case parseCC cc of
Nothing => useCC appdir fc ccs args ret
Just ("scheme,chez", [sfn]) =>
do body <- schemeCall fc sfn (map fst args) ret
pure ("", body)
Just ("scheme", [sfn]) =>
do body <- schemeCall fc sfn (map fst args) ret
pure ("", body)
@ -344,7 +347,7 @@ startChez appdir target = unlines
, " ;; "
, "esac "
, ""
, "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" ++ appdir ++ "\"\""
, "export LD_LIBRARY_PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$LD_LIBRARY_PATH\""
, "\"`dirname \"$DIR\"`\"/\"" ++ target ++ "\" \"$@\""
]

2
src/Compiler/Scheme/Common.idr
View File

@ -31,7 +31,7 @@ schString s = concatMap okchar (unpack s)
export
schName : Name -> String
schName (NS ns n) = showSep "-" ns ++ "-" ++ schName n
schName (NS ns n) = showNSWithSep "-" ns ++ "-" ++ schName n
schName (UN n) = schString n
schName (MN n i) = schString n ++ "-" ++ show i
schName (PV n d) = "pat--" ++ schName n

4
src/Compiler/Scheme/Gambit.idr
View File

@ -291,11 +291,11 @@ schemeCall fc sfn argns ret
useCC : {auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
FC -> List String -> List (Name, CFType) -> CFType -> Core (Maybe String, (String, String))
useCC fc [] args ret
= throw (GenericMsg fc "No recognised foreign calling convention")
useCC fc [] args ret = throw (NoForeignCC fc)
useCC fc (cc :: ccs) args ret
= case parseCC cc of
Nothing => useCC fc ccs args ret
Just ("scheme,gambit", [sfn]) => pure (Nothing, (!(schemeCall fc sfn (map fst args) ret), ""))
Just ("scheme", [sfn]) => pure (Nothing, (!(schemeCall fc sfn (map fst args) ret), ""))
Just ("C", [cfn, clib]) => pure (Just clib, !(cCall fc cfn (fnWrapName cfn) clib args ret))
Just ("C", [cfn, clib, chdr]) => pure (Just clib, !(cCall fc cfn (fnWrapName cfn) clib args ret))

7
src/Compiler/Scheme/Racket.idr
View File

@ -7,6 +7,7 @@ import Compiler.Scheme.Common
import Core.Options
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Name
import Core.TT
@ -250,11 +251,13 @@ useCC : {auto f : Ref Done (List String) } ->
{auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
String -> FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
useCC appdir fc [] args ret
= throw (GenericMsg fc "No recognised foreign calling convention")
useCC appdir fc [] args ret = throw (NoForeignCC fc)
useCC appdir fc (cc :: ccs) args ret
= case parseCC cc of
Nothing => useCC appdir fc ccs args ret
Just ("scheme,racket", [sfn]) =>
do body <- schemeCall fc sfn (map fst args) ret
pure ("", body)
Just ("scheme", [sfn]) =>
do body <- schemeCall fc sfn (map fst args) ret
pure ("", body)

3
src/Core/AutoSearch.idr
View File

@ -1,6 +1,7 @@
module Core.AutoSearch
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Normalise
@ -410,7 +411,7 @@ searchNames fc rigc defaults trying depth defining topty env ambig (n :: ns) tar
else exactlyOne fc env topty target elabs
where
visible : Context ->
List (List String) -> Name -> Core (Maybe (Name, GlobalDef))
List Namespace -> Name -> Core (Maybe (Name, GlobalDef))
visible gam nspace n
= do Just def <- lookupCtxtExact n gam
| Nothing => pure Nothing

45
src/Core/Binary.idr
View File

@ -1,6 +1,7 @@
module Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Hash
import Core.Normalise
@ -41,15 +42,15 @@ record TTCFile extra where
constructor MkTTCFile
version : Int
ifaceHash : Int
importHashes : List (List String, Int)
importHashes : List (Namespace, Int)
context : List (Name, Binary)
userHoles : List Name
autoHints : List (Name, Bool)
typeHints : List (Name, Name, Bool)
imported : List (List String, Bool, List String)
imported : List (ModuleIdent, Bool, Namespace)
nextVar : Int
currentNS : List String
nestedNS : List (List String)
currentNS : Namespace
nestedNS : List Namespace
pairnames : Maybe PairNames
rewritenames : Maybe RewriteNames
primnames : PrimNames
@ -191,7 +192,7 @@ writeTTCFile b file_in
readTTCFile : TTC extra =>
{auto c : Ref Ctxt Defs} ->
String -> Maybe (List String) ->
String -> Maybe (Namespace) ->
Ref Bin Binary -> Core (TTCFile extra)
readTTCFile file as b
= do hdr <- fromBuf b
@ -274,7 +275,7 @@ writeToTTC extradata fname
pure ()
addGlobalDef : {auto c : Ref Ctxt Defs} ->
(modns : List String) -> (importAs : Maybe (List String)) ->
(modns : ModuleIdent) -> (importAs : Maybe Namespace) ->
(Name, Binary) -> Core ()
addGlobalDef modns asm (n, def)
= do defs <- get Ctxt
@ -290,7 +291,7 @@ addGlobalDef modns asm (n, def)
else do addContextEntry n def
pure ()
maybe (pure ())
(\as => addContextAlias (asName modns as n) n)
(\ as => addContextAlias (asName modns as n) n)
asm
where
-- If the definition already exists, don't overwrite it with an empty
@ -382,8 +383,8 @@ updateTransforms ((n, t) :: ts)
put Ctxt (record { transforms $= insert n (t :: ts) } defs)
getNSas : (String, (List String, Bool, List String)) ->
(List String, List String)
getNSas : (String, (ModuleIdent, Bool, Namespace)) ->
(ModuleIdent, Namespace)
getNSas (a, (b, c, d)) = (b, d)
-- Add definitions from a binary file to the current context
@ -399,10 +400,10 @@ readFromTTC : TTC extra =>
FC ->
Bool -> -- importing as public
(fname : String) -> -- file containing the module
(modNS : List String) -> -- module namespace
(importAs : List String) -> -- namespace to import as
(modNS : ModuleIdent) -> -- module namespace
(importAs : Namespace) -> -- namespace to import as
Core (Maybe (extra, Int,
List (List String, Bool, List String)))
List (ModuleIdent, Bool, Namespace)))
readFromTTC nestedns loc reexp fname modNS importAs
= do defs <- get Ctxt
-- If it's already in the context, with the same visibility flag,
@ -415,7 +416,7 @@ readFromTTC nestedns loc reexp fname modNS importAs
Right buffer <- coreLift $ readFromFile fname
| Left err => throw (InternalError (fname ++ ": " ++ show err))
bin <- newRef Bin buffer -- for reading the file into
let as = if importAs == modNS
let as = if importAs == miAsNamespace modNS
then Nothing
else Just importAs
ttc <- readTTCFile fname as bin
@ -433,7 +434,7 @@ readFromTTC nestedns loc reexp fname modNS importAs
when nestedns $ setNestedNS (nestedNS ttc)
-- Only do the next batch if the module hasn't been loaded
-- in any form
when (not (modNS `elem` map (fst . getNSas) (allImported defs))) $
unless (modNS `elem` map (fst . getNSas) (allImported defs)) $
-- Set up typeHints and autoHints based on the loaded data
do traverse_ (addTypeHint loc) (typeHints ttc)
traverse_ addAutoHint (autoHints ttc)
@ -454,20 +455,20 @@ readFromTTC nestedns loc reexp fname modNS importAs
put UST (record { nextName = nextVar ttc } ust)
pure (Just (ex, ifaceHash ttc, imported ttc))
where
alreadyDone : List String -> List String ->
List (String, (List String, Bool, List String)) ->
alreadyDone : ModuleIdent -> Namespace ->
List (String, (ModuleIdent, Bool, Namespace)) ->
Bool
alreadyDone modns importAs [] = False
-- If we've already imported 'modns' as 'importAs', or we're importing
-- 'modns' as itself and it's already imported as anything, then no
-- need to load again.
-- If we've already imported 'modns' as 'importAs', or we're importing
-- 'modns' as itself and it's already imported as anything, then no
-- need to load again.
alreadyDone modns importAs ((_, (m, _, a)) :: rest)
= (modns == m && importAs == a)
|| (modns == m && modns == importAs)
|| (modns == m && miAsNamespace modns == importAs)
|| alreadyDone modns importAs rest
getImportHashes : String -> Ref Bin Binary ->
Core (List (List String, Int))
Core (List (Namespace, Int))
getImportHashes file b
= do hdr <- fromBuf {a = String} b
when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
@ -497,7 +498,7 @@ readIFaceHash fname
export
readImportHashes : (fname : String) -> -- file containing the module
Core (List (List String, Int))
Core (List (Namespace, Int))
readImportHashes fname
= do Right buffer <- coreLift $ readFromFile fname
| Left err => pure []

1
src/Core/CaseBuilder.idr
View File

@ -2,6 +2,7 @@ module Core.CaseBuilder
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Normalise

36
src/Core/CaseTree.idr
View File

@ -6,6 +6,8 @@ import Data.Bool.Extra
import Data.List
import Data.NameMap
import Text.PrettyPrint.Prettyprinter.Doc
%default covering
mutual
@ -60,8 +62,8 @@ mutual
export
{vars : _} -> Show (CaseTree vars) where
show (Case {name} idx prf ty alts)
= "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of { " ++
showSep " | " (assert_total (map show alts)) ++ " }"
= "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of\n { " ++
showSep "\n | " (assert_total (map show alts)) ++ "\n }"
show (STerm i tm) = "[" ++ show i ++ "] " ++ show tm
show (Unmatched msg) = "Error: " ++ show msg
show Impossible = "Impossible"
@ -69,15 +71,41 @@ mutual
export
{vars : _} -> Show (CaseAlt vars) where
show (ConCase n tag args sc)
= show n ++ " " ++ showSep " " (map show args) ++ " => " ++
= showSep " " (map show (n :: args)) ++ " => " ++
show sc
show (DelayCase _ arg sc)
= "Delay " ++ show arg ++ " => " ++ show sc
show (ConstCase c sc)
= show c ++ " => " ++ show sc
= "Constant " ++ show c ++ " => " ++ show sc
show (DefaultCase sc)
= "_ => " ++ show sc
mutual
export
{vars : _} -> Pretty (CaseTree vars) where
pretty (Case {name} idx prf ty alts)
= "case" <++> pretty name <++> ":" <++> pretty ty <++> "of"
<+> nest 2 (hardline
<+> vsep (assert_total (map pretty alts)))
pretty (STerm i tm) = pretty tm
pretty (Unmatched msg) = pretty "Error:" <++> pretty msg
pretty Impossible = pretty "Impossible"
export
{vars : _} -> Pretty (CaseAlt vars) where
pretty (ConCase n tag args sc)
= hsep (map pretty (n :: args)) <++> pretty "=>"
<+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
pretty (DelayCase _ arg sc) =
pretty "Delay" <++> pretty arg <++> pretty "=>"
<+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
pretty (ConstCase c sc) =
pretty c <++> pretty "=>"
<+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
pretty (DefaultCase sc) =
pretty "_ =>"
<+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
mutual
export
eqTree : CaseTree vs -> CaseTree vs' -> Bool

341
src/Core/Context.idr
View File

@ -19,7 +19,6 @@ import Data.NameMap
import Data.StringMap
import System
import System.Clock
import System.Directory
%default covering
@ -288,6 +287,12 @@ export
refersToRuntime : GlobalDef -> NameMap Bool
refersToRuntime def = maybe empty id (refersToRuntimeM def)
export
findSetTotal : List DefFlag -> Maybe TotalReq
findSetTotal [] = Nothing
findSetTotal (SetTotal t :: _) = Just t
findSetTotal (_ :: xs) = findSetTotal xs
-- Label for array references
export
data Arr : Type where
@ -330,7 +335,7 @@ record Context where
-- This only matters during evaluation and type checking, to control
-- access in a program - in all other cases, we'll assume everything is
-- visible
visibleNS : List (List String)
visibleNS : List Namespace
allPublic : Bool -- treat everything as public. This is only intended
-- for checking partially evaluated definitions
inlineOnly : Bool -- only return things with the 'alwaysReduce' flag
@ -356,7 +361,7 @@ initCtxtS : Int -> Core Context
initCtxtS s
= do arr <- coreLift $ newArray s
aref <- newRef Arr arr
pure (MkContext 0 0 empty empty aref 0 empty [["_PE"]] False False empty)
pure (MkContext 0 0 empty empty aref 0 empty [partialEvalNS] False False empty)
export
initCtxt : Core Context
@ -523,10 +528,6 @@ lookupCtxtName n ctxt
| Nothing => pure []
lookupPossibles [] ps
where
matches : Name -> Name -> Bool
matches (NS ns _) (NS cns _) = ns `isPrefixOf` cns
matches (NS _ _) _ = True -- no in library name, so root doesn't match
matches _ _ = True -- no prefix, so root must match, so good
resn : (Name, Int, GlobalDef) -> Int
resn (_, i, _) = i
@ -873,8 +874,8 @@ record Defs where
constructor MkDefs
gamma : Context
mutData : List Name -- Currently declared but undefined data types
currentNS : List String -- namespace for current definitions
nestedNS : List (List String) -- other nested namespaces we can look in
currentNS : Namespace -- namespace for current definitions
nestedNS : List Namespace -- other nested namespaces we can look in
options : Options
toSave : NameMap ()
nextTag : Int
@ -902,11 +903,11 @@ record Defs where
saveTransforms : List (Name, Transform)
namedirectives : NameMap (List String)
ifaceHash : Int
importHashes : List (List String, Int)
importHashes : List (Namespace, Int)
-- ^ interface hashes of imported modules
imported : List (List String, Bool, List String)
imported : List (ModuleIdent, Bool, Namespace)
-- ^ imported modules, whether to rexport, as namespace
allImported : List (String, (List String, Bool, List String))
allImported : List (String, (ModuleIdent, Bool, Namespace))
-- ^ all imported filenames/namespaces, just to avoid loading something
-- twice unnecessarily (this is a record of all the things we've
-- called 'readFromTTC' with, in practice)
@ -943,7 +944,7 @@ export
initDefs : Core Defs
initDefs
= do gam <- initCtxt
pure (MkDefs gam [] ["Main"] [] defaults empty 100
pure (MkDefs gam [] mainNS [] defaults empty 100
empty empty empty [] [] empty []
empty 5381 [] [] [] [] [] empty empty empty empty [])
@ -1254,24 +1255,23 @@ lookupDefTyExact = lookupExactBy (\g => (definition g, type g))
-- private names are only visible in this namespace if their namespace
-- is the current namespace (or an outer one)
-- that is: given that most recent namespace is first in the list,
-- the namespace of 'n' is a suffix of nspace
visibleIn : (nspace : List String) -> Name -> Visibility -> Bool
visibleIn nspace (NS ns n) Private = isSuffixOf ns nspace
-- that is: the namespace of 'n' is a parent of nspace
visibleIn : Namespace -> Name -> Visibility -> Bool
visibleIn nspace (NS ns n) Private = isParentOf ns nspace
-- Public and Export names are always visible
visibleIn nspace n _ = True
export
visibleInAny : (nspace : List (List String)) -> Name -> Visibility -> Bool
visibleInAny : List Namespace -> Name -> Visibility -> Bool
visibleInAny nss n vis = any (\ns => visibleIn ns n vis) nss
reducibleIn : (nspace : List String) -> Name -> Visibility -> Bool
reducibleIn nspace (NS ns (UN n)) Export = isSuffixOf ns nspace
reducibleIn nspace (NS ns (UN n)) Private = isSuffixOf ns nspace
reducibleIn : Namespace -> Name -> Visibility -> Bool
reducibleIn nspace (NS ns (UN n)) Export = isParentOf ns nspace
reducibleIn nspace (NS ns (UN n)) Private = isParentOf ns nspace
reducibleIn nspace n _ = True
export
reducibleInAny : (nspace : List (List String)) -> Name -> Visibility -> Bool
reducibleInAny : List Namespace -> Name -> Visibility -> Bool
reducibleInAny nss n vis = any (\ns => reducibleIn ns n vis) nss
export
@ -1663,7 +1663,7 @@ clearSavedHints
-- Set the default namespace for new definitions
export
setNS : {auto c : Ref Ctxt Defs} ->
List String -> Core ()
Namespace -> Core ()
setNS ns
= do defs <- get Ctxt
put Ctxt (record { currentNS = ns } defs)
@ -1671,7 +1671,7 @@ setNS ns
-- Set the nested namespaces we're allowed to look inside
export
setNestedNS : {auto c : Ref Ctxt Defs} ->
List (List String) -> Core ()
List Namespace -> Core ()
setNestedNS ns
= do defs <- get Ctxt
put Ctxt (record { nestedNS = ns } defs)
@ -1679,7 +1679,7 @@ setNestedNS ns
-- Get the default namespace for new definitions
export
getNS : {auto c : Ref Ctxt Defs} ->
Core (List String)
Core Namespace
getNS
= do defs <- get Ctxt
pure (currentNS defs)
@ -1687,7 +1687,7 @@ getNS
-- Get the nested namespaces we're allowed to look inside
export
getNestedNS : {auto c : Ref Ctxt Defs} ->
Core (List (List String))
Core (List Namespace)
getNestedNS
= do defs <- get Ctxt
pure (nestedNS defs)
@ -1698,14 +1698,14 @@ getNestedNS
-- "import X as [current namespace]")
export
addImported : {auto c : Ref Ctxt Defs} ->
(List String, Bool, List String) -> Core ()
(ModuleIdent, Bool, Namespace) -> Core ()
addImported mod
= do defs <- get Ctxt
put Ctxt (record { imported $= (mod ::) } defs)
export
getImported : {auto c : Ref Ctxt Defs} ->
Core (List (List String, Bool, List String))
Core (List (ModuleIdent, Bool, Namespace))
getImported
= do defs <- get Ctxt
pure (imported defs)
@ -1732,6 +1732,7 @@ getDirectives cg
getDir : (CG, String) -> Maybe String
getDir (x', str) = if cg == x' then Just str else Nothing
export
getNextTypeTag : {auto c : Ref Ctxt Defs} ->
Core Int
getNextTypeTag
@ -1739,126 +1740,16 @@ getNextTypeTag
put Ctxt (record { nextTag $= (+1) } defs)
pure (nextTag defs)
-- If a name appears more than once in an argument list, only the first is
-- considered a parameter
dropReps : List (Maybe (Term vars)) -> List (Maybe (Term vars))
dropReps [] = []
dropReps {vars} (Just (Local fc r x p) :: xs)
= Just (Local fc r x p) :: assert_total (dropReps (map toNothing xs))
where
toNothing : Maybe (Term vars) -> Maybe (Term vars)
toNothing tm@(Just (Local _ _ v' _))
= if x == v' then Nothing else tm
toNothing tm = tm
dropReps (x :: xs) = x :: dropReps xs
updateParams : Maybe (List (Maybe (Term vars))) ->
-- arguments to the type constructor which could be
-- parameters
-- Nothing, as an argument, means this argument can't
-- be a parameter position
List (Term vars) ->
-- arguments to an application
List (Maybe (Term vars))
updateParams Nothing args = dropReps $ map couldBeParam args
where
couldBeParam : Term vars -> Maybe (Term vars)
couldBeParam (Local fc r v p) = Just (Local fc r v p)
couldBeParam _ = Nothing
updateParams (Just args) args' = dropReps $ zipWith mergeArg args args'
where
mergeArg : Maybe (Term vars) -> Term vars -> Maybe (Term vars)
mergeArg (Just (Local fc r x p)) (Local _ _ y _)
= if x == y then Just (Local fc r x p) else Nothing
mergeArg _ _ = Nothing
getPs : {vars : _} ->
Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
Maybe (List (Maybe (Term vars)))
getPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
= let scPs = getPs (Prelude.map (Prelude.map (Prelude.map weaken)) acc) tyn sc in
map (map shrink) scPs
where
shrink : Maybe (Term (x :: vars)) -> Maybe (Term vars)
shrink Nothing = Nothing
shrink (Just tm) = shrinkTerm tm (DropCons SubRefl)
getPs acc tyn tm
= case getFnArgs tm of
(Ref _ _ n, args) =>
if n == tyn
then Just (updateParams acc args)
else acc
_ => acc
toPos : Maybe (List (Maybe a)) -> List Nat
toPos Nothing = []
toPos (Just ns) = justPos 0 ns
where
justPos : Nat -> List (Maybe a) -> List Nat
justPos i [] = []
justPos i (Just x :: xs) = i :: justPos (1 + i) xs
justPos i (Nothing :: xs) = justPos (1 + i) xs
getConPs : {vars : _} ->
Maybe (List (Maybe (Term vars))) -> Name -> Term vars -> List Nat
getConPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
= let bacc = getPs acc tyn ty in
getConPs (map (map (map weaken)) bacc) tyn sc
getConPs acc tyn tm = toPos (getPs acc tyn tm)
combinePos : Eq a => List (List a) -> List a
combinePos [] = []
combinePos (xs :: xss) = filter (\x => all (elem x) xss) xs
paramPos : Name -> (dcons : List ClosedTerm) ->
List Nat
paramPos tyn dcons = combinePos (map (getConPs Nothing tyn) dcons)
export
addData : {auto c : Ref Ctxt Defs} ->
List Name -> Visibility -> Int -> DataDef -> Core Int
addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
= do defs <- get Ctxt
tag <- getNextTypeTag
let tydef = newDef dfc tyn top vars tycon vis
(TCon tag arity
(paramPos (Resolved tidx) (map type datacons))
(allDet arity)
defaultFlags [] (map name datacons) Nothing)
(idx, gam') <- addCtxt tyn tydef (gamma defs)
gam'' <- addDataConstructors 0 datacons gam'
put Ctxt (record { gamma = gam'' } defs)
pure idx
where
allDet : Nat -> List Nat
allDet Z = []
allDet (S k) = [0..k]
conVisibility : Visibility -> Visibility
conVisibility Export = Private
conVisibility x = x
addDataConstructors : (tag : Int) -> List Constructor ->
Context -> Core Context
addDataConstructors tag [] gam = pure gam
addDataConstructors tag (MkCon fc n a ty :: cs) gam
= do let condef = newDef fc n top vars ty (conVisibility vis) (DCon tag a Nothing)
(idx, gam') <- addCtxt n condef gam
-- Check 'n' is undefined
Nothing <- lookupCtxtExact n gam
| Just gdef => throw (AlreadyDefined fc n)
addDataConstructors (tag + 1) cs gam'
-- Add a new nested namespace to the current namespace for new definitions
-- e.g. extendNS ["Data"] when namespace is "Prelude.List" leads to
-- current namespace of "Prelude.List.Data"
-- Inner namespaces go first, for ease of name lookup
export
extendNS : {auto c : Ref Ctxt Defs} ->
List String -> Core ()
Namespace -> Core ()
extendNS ns
= do defs <- get Ctxt
put Ctxt (record { currentNS $= ((reverse ns) ++) } defs)
put Ctxt (record { currentNS $= (<.> ns) } defs)
-- Get the name as it would be defined in the current namespace
-- i.e. if it doesn't have an explicit namespace already, add it,
@ -1888,14 +1779,14 @@ inCurrentNS n = pure n
export
setVisible : {auto c : Ref Ctxt Defs} ->
(nspace : List String) -> Core ()
Namespace -> Core ()
setVisible nspace
= do defs <- get Ctxt
put Ctxt (record { gamma->visibleNS $= (nspace ::) } defs)
export
getVisible : {auto c : Ref Ctxt Defs} ->
Core (List (List String))
Core (List Namespace)
getVisible
= do defs <- get Ctxt
pure (visibleNS (gamma defs))
@ -1921,21 +1812,18 @@ isAllPublic
-- the namespace itself, and any namespace it's nested inside)
export
isVisible : {auto c : Ref Ctxt Defs} ->
(nspace : List String) -> Core Bool
Namespace -> Core Bool
isVisible nspace
= do defs <- get Ctxt
pure (any visible (allParents (currentNS defs) ++
nestedNS defs ++
visibleNS (gamma defs)))
where
allParents : List String -> List (List String)
allParents [] = []
allParents (n :: ns) = (n :: ns) :: allParents ns
-- Visible if any visible namespace is a suffix of the namespace we're
where
-- Visible if any visible namespace is a parent of the namespace we're
-- asking about
visible : List String -> Bool
visible visns = isSuffixOf visns nspace
visible : Namespace -> Bool
visible visns = isParentOf visns nspace
-- Get the next entry id in the context (this is for recording where to go
-- back to when backtracking in the elaborator)
@ -2314,156 +2202,3 @@ recordWarning : {auto c : Ref Ctxt Defs} ->
recordWarning w
= do defs <- get Ctxt
put Ctxt (record { warnings $= (w ::) } defs)
-- Log message with a term, translating back to human readable names first
export
logTerm : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> Term vars -> Core ()
logTerm str n msg tm
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
then do tm' <- toFullNames tm
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
++ ": " ++ show tm'
else pure ()
export
log' : {auto c : Ref Ctxt Defs} ->
LogLevel -> Lazy String -> Core ()
log' lvl msg
= do opts <- getSession
if keepLog lvl (logLevel opts)
then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()
export
log : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> Core ()
log str n msg
= do let lvl = mkLogLevel str n
log' lvl msg
export
logC : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Core String -> Core ()
logC str n cmsg
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
then do msg <- cmsg
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()
export
logTimeOver : Integer -> Core String -> Core a -> Core a
logTimeOver nsecs str act
= do clock <- coreLift (clockTime Process)
let nano = 1000000000
let t = seconds clock * nano + nanoseconds clock
res <- act
clock <- coreLift (clockTime Process)
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
when (time > nsecs) $
assert_total $ -- We're not dividing by 0
do str' <- str
coreLift $ putStrLn $ "TIMING " ++ str' ++ ": " ++
show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
"s"
pure res
where
addZeros : List Char -> String
addZeros [] = "000"
addZeros [x] = "00" ++ cast x
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
export
logTimeWhen : {auto c : Ref Ctxt Defs} ->
Bool -> Lazy String -> Core a -> Core a
logTimeWhen p str act
= if p
then do clock <- coreLift (clockTime Process)
let nano = 1000000000
let t = seconds clock * nano + nanoseconds clock
res <- act
clock <- coreLift (clockTime Process)
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
assert_total $ -- We're not dividing by 0
coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
"s"
pure res
else act
where
addZeros : List Char -> String
addZeros [] = "000"
addZeros [x] = "00" ++ cast x
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
logTimeRecord' : {auto c : Ref Ctxt Defs} ->
String -> Core a -> Core a
logTimeRecord' key act
= do clock <- coreLift (clockTime Process)
let nano = 1000000000
let t = seconds clock * nano + nanoseconds clock
res <- act
clock <- coreLift (clockTime Process)
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
defs <- get Ctxt
let tot = case lookup key (timings defs) of
Nothing => 0
Just (_, t) => t
put Ctxt (record { timings $= insert key (False, tot + time) } defs)
pure res
-- for ad-hoc profiling, record the time the action takes and add it
-- to the time for the given category
export
logTimeRecord : {auto c : Ref Ctxt Defs} ->
String -> Core a -> Core a
logTimeRecord key act
= do defs <- get Ctxt
-- Only record if we're not currently recording that key
case lookup key (timings defs) of
Just (True, t) => act
Just (False, t)
=> do put Ctxt (record { timings $= insert key (True, t) } defs)
logTimeRecord' key act
Nothing
=> logTimeRecord' key act
export
showTimeRecord : {auto c : Ref Ctxt Defs} ->
Core ()
showTimeRecord
= do defs <- get Ctxt
traverse_ showTimeLog (toList (timings defs))
where
addZeros : List Char -> String
addZeros [] = "000"
addZeros [x] = "00" ++ cast x
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
showTimeLog : (String, (Bool, Integer)) -> Core ()
showTimeLog (key, (_, time))
= do coreLift $ putStr (key ++ ": ")
let nano = 1000000000
assert_total $ -- We're not dividing by 0
coreLift $ putStrLn $ show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
"s"
export
logTime : {auto c : Ref Ctxt Defs} ->
Lazy String -> Core a -> Core a
logTime str act
= do opts <- getSession
logTimeWhen (logTimings opts) str act

132
src/Core/Context/Data.idr Normal file
View File

@ -0,0 +1,132 @@
-- Computing the parameters
module Core.Context.Data
import Core.Context
import Core.Context.Log
import Core.Normalise
import Data.List
import Data.Maybe
%default covering
-- If a name appears more than once in an argument list, only the first is
-- considered a parameter
dropReps : List (Maybe (Term vars)) -> List (Maybe (Term vars))
dropReps [] = []
dropReps {vars} (Just (Local fc r x p) :: xs)
= Just (Local fc r x p) :: assert_total (dropReps (map toNothing xs))
where
toNothing : Maybe (Term vars) -> Maybe (Term vars)
toNothing tm@(Just (Local _ _ v' _))
= if x == v' then Nothing else tm
toNothing tm = tm
dropReps (x :: xs) = x :: dropReps xs
updateParams : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
Maybe (List (Maybe (Term vars))) ->
-- arguments to the type constructor which could be
-- parameters
-- Nothing, as an argument, means this argument can't
-- be a parameter position
List (Term vars) ->
-- arguments to an application
Core (List (Maybe (Term vars)))
updateParams Nothing args = dropReps <$> traverse couldBeParam args
where
couldBeParam : Term vars -> Core (Maybe (Term vars))
couldBeParam tm = pure $ case !(etaContract tm) of
Local fc r v p => Just (Local fc r v p)
_ => Nothing
updateParams (Just args) args' = pure $ dropReps $ zipWith mergeArg args args'
where
mergeArg : Maybe (Term vars) -> Term vars -> Maybe (Term vars)
mergeArg (Just (Local fc r x p)) (Local _ _ y _)
= if x == y then Just (Local fc r x p) else Nothing
mergeArg _ _ = Nothing
getPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
Core (Maybe (List (Maybe (Term vars))))
getPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
= do scPs <- getPs (map (map (map weaken)) acc) tyn sc
pure $ map (map shrink) scPs
where
shrink : Maybe (Term (x :: vars)) -> Maybe (Term vars)
shrink Nothing = Nothing
shrink (Just tm) = shrinkTerm tm (DropCons SubRefl)
getPs acc tyn tm
= case getFnArgs tm of
(Ref _ _ n, args) =>
if n == tyn
then Just <$> updateParams acc args
else pure acc
_ => pure acc
toPos : Maybe (List (Maybe a)) -> List Nat
toPos Nothing = []
toPos (Just ns) = justPos 0 ns
where
justPos : Nat -> List (Maybe a) -> List Nat
justPos i [] = []
justPos i (Just x :: xs) = i :: justPos (1 + i) xs
justPos i (Nothing :: xs) = justPos (1 + i) xs
getConPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
Core (List Nat)
getConPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
= do bacc <- getPs acc tyn ty
getConPs (map (map (map weaken)) bacc) tyn sc
getConPs acc tyn (Bind _ x (Let _ _ v ty) sc)
= getConPs acc tyn (subst v sc)
getConPs acc tyn tm = toPos <$> getPs acc tyn tm
paramPos : {auto _ : Ref Ctxt Defs} -> Name -> (dcons : List ClosedTerm) ->
Core (Maybe (List Nat))
paramPos tyn [] = pure Nothing -- no constructor!
paramPos tyn dcons = do
candidates <- traverse (getConPs Nothing tyn) dcons
pure $ Just $ intersectAll candidates
export
addData : {auto c : Ref Ctxt Defs} ->
List Name -> Visibility -> Int -> DataDef -> Core Int
addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
= do defs <- get Ctxt
tag <- getNextTypeTag
let allPos = allDet arity
-- In case there are no constructors, all the positions are parameter positions!
let paramPositions = fromMaybe allPos !(paramPos (Resolved tidx) (map type datacons))
log "declare.data.parameters" 20 $
"Positions of parameters for datatype" ++ show tyn ++
": [" ++ showSep ", " (map show paramPositions) ++ "]"
let tydef = newDef dfc tyn top vars tycon vis
(TCon tag arity
paramPositions
allPos
defaultFlags [] (map name datacons) Nothing)
(idx, gam') <- addCtxt tyn tydef (gamma defs)
gam'' <- addDataConstructors 0 datacons gam'
put Ctxt (record { gamma = gam'' } defs)
pure idx
where
allDet : Nat -> List Nat
allDet Z = []
allDet (S k) = [0..k]
conVisibility : Visibility -> Visibility
conVisibility Export = Private
conVisibility x = x
addDataConstructors : (tag : Int) -> List Constructor ->
Context -> Core Context
addDataConstructors tag [] gam = pure gam
addDataConstructors tag (MkCon fc n a ty :: cs) gam
= do let condef = newDef fc n top vars ty (conVisibility vis) (DCon tag a Nothing)
(idx, gam') <- addCtxt n condef gam
-- Check 'n' is undefined
Nothing <- lookupCtxtExact n gam
| Just gdef => throw (AlreadyDefined fc n)
addDataConstructors (tag + 1) cs gam'

163
src/Core/Context/Log.idr Normal file
View File

@ -0,0 +1,163 @@
module Core.Context.Log
import Core.Context
import Core.Options
import Data.StringMap
import System.Clock
%default covering
-- Log message with a term, translating back to human readable names first
export
logTerm : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> Term vars -> Core ()
logTerm str n msg tm
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
then do tm' <- toFullNames tm
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
++ ": " ++ show tm'
else pure ()
export
log' : {auto c : Ref Ctxt Defs} ->
LogLevel -> Lazy String -> Core ()
log' lvl msg
= do opts <- getSession
if keepLog lvl (logLevel opts)
then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()
export
log : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Lazy String -> Core ()
log str n msg
= do let lvl = mkLogLevel str n
log' lvl msg
export
logC : {auto c : Ref Ctxt Defs} ->
String -> Nat -> Core String -> Core ()
logC str n cmsg
= do opts <- getSession
let lvl = mkLogLevel str n
if keepLog lvl (logLevel opts)
then do msg <- cmsg
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()
export
logTimeOver : Integer -> Core String -> Core a -> Core a
logTimeOver nsecs str act
= do clock <- coreLift (clockTime Process)
let nano = 1000000000
let t = seconds clock * nano + nanoseconds clock
res <- act
clock <- coreLift (clockTime Process)
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
when (time > nsecs) $
assert_total $ -- We're not dividing by 0
do str' <- str
coreLift $ putStrLn $ "TIMING " ++ str' ++ ": " ++
show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
"s"
pure res
where
addZeros : List Char -> String
addZeros [] = "000"
addZeros [x] = "00" ++ cast x
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
export
logTimeWhen : {auto c : Ref Ctxt Defs} ->
Bool -> Lazy String -> Core a -> Core a
logTimeWhen p str act
= if p
then do clock <- coreLift (clockTime Process)
let nano = 1000000000
let t = seconds clock * nano + nanoseconds clock
res <- act
clock <- coreLift (clockTime Process)
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
assert_total $ -- We're not dividing by 0
coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
"s"
pure res
else act
where
addZeros : List Char -> String
addZeros [] = "000"
addZeros [x] = "00" ++ cast x
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
logTimeRecord' : {auto c : Ref Ctxt Defs} ->
String -> Core a -> Core a
logTimeRecord' key act
= do clock <- coreLift (clockTime Process)
let nano = 1000000000
let t = seconds clock * nano + nanoseconds clock
res <- act
clock <- coreLift (clockTime Process)
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
defs <- get Ctxt
let tot = case lookup key (timings defs) of
Nothing => 0
Just (_, t) => t
put Ctxt (record { timings $= insert key (False, tot + time) } defs)
pure res
-- for ad-hoc profiling, record the time the action takes and add it
-- to the time for the given category
export
logTimeRecord : {auto c : Ref Ctxt Defs} ->
String -> Core a -> Core a
logTimeRecord key act
= do defs <- get Ctxt
-- Only record if we're not currently recording that key
case lookup key (timings defs) of
Just (True, t) => act
Just (False, t)
=> do put Ctxt (record { timings $= insert key (True, t) } defs)
logTimeRecord' key act
Nothing
=> logTimeRecord' key act
export
showTimeRecord : {auto c : Ref Ctxt Defs} ->
Core ()
showTimeRecord
= do defs <- get Ctxt
traverse_ showTimeLog (toList (timings defs))
where
addZeros : List Char -> String
addZeros [] = "000"
addZeros [x] = "00" ++ cast x
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
showTimeLog : (String, (Bool, Integer)) -> Core ()
showTimeLog (key, (_, time))
= do coreLift $ putStr (key ++ ": ")
let nano = 1000000000
assert_total $ -- We're not dividing by 0
coreLift $ putStrLn $ show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
"s"
export
logTime : {auto c : Ref Ctxt Defs} ->
Lazy String -> Core a -> Core a
logTime str act
= do opts <- getSession
logTimeWhen (logTimings opts) str act

49
src/Core/Core.idr
View File

@ -72,7 +72,7 @@ data Error : Type where
ValidCase : {vars : _} ->
FC -> Env Term vars -> Either (Term vars) Error -> Error
UndefinedName : FC -> Name -> Error
InvisibleName : FC -> Name -> Maybe (List String) -> Error
InvisibleName : FC -> Name -> Maybe Namespace -> Error
BadTypeConType : FC -> Name -> Error
BadDataConType : FC -> Name -> Name -> Error
NotCovering : FC -> Name -> Covering -> Error
@ -136,11 +136,12 @@ data Error : Type where
FileErr : String -> FileError -> Error
ParseFail : (Show token, Pretty token) =>
FC -> ParseError token -> Error
ModuleNotFound : FC -> List String -> Error
CyclicImports : List (List String) -> Error
ModuleNotFound : FC -> ModuleIdent -> Error
CyclicImports : List ModuleIdent -> Error
ForceNeeded : Error
InternalError : String -> Error
UserError : String -> Error
NoForeignCC : FC -> Error
InType : FC -> Name -> Error -> Error
InCon : FC -> Name -> Error -> Error
@ -184,7 +185,7 @@ Show Error where
show (UndefinedName fc x) = show fc ++ ":Undefined name " ++ show x
show (InvisibleName fc x (Just ns))
= show fc ++ ":Name " ++ show x ++ " is inaccessible since " ++
showSep "." (reverse ns) ++ " is not explicitly imported"
show ns ++ " is not explicitly imported"
show (InvisibleName fc x _) = show fc ++ ":Name " ++ show x ++ " is private"
show (BadTypeConType fc n)
= show fc ++ ":Return type of " ++ show n ++ " must be Type"
@ -299,15 +300,14 @@ Show Error where
show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err
show (ParseFail fc err) = "Parse error (" ++ show err ++ ")"
show (ModuleNotFound fc ns)
= show fc ++ ":" ++ showSep "." (reverse ns) ++ " not found"
= show fc ++ ":" ++ show ns ++ " not found"
show (CyclicImports ns)
= "Module imports form a cycle: " ++ showSep " -> " (map showMod ns)
where
showMod : List String -> String
showMod ns = showSep "." (reverse ns)
= "Module imports form a cycle: " ++ showSep " -> " (map show ns)
show ForceNeeded = "Internal error when resolving implicit laziness"
show (InternalError str) = "INTERNAL ERROR: " ++ str
show (UserError str) = "Error: " ++ str
show (NoForeignCC fc) = show fc ++
":The given specifier was not accepted by any available backend."
show (InType fc n err)
= show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++
@ -383,6 +383,7 @@ getErrorLoc (CyclicImports _) = Nothing
getErrorLoc ForceNeeded = Nothing
getErrorLoc (InternalError _) = Nothing
getErrorLoc (UserError _) = Nothing
getErrorLoc (NoForeignCC loc) = Just loc
getErrorLoc (InType _ _ err) = getErrorLoc err
getErrorLoc (InCon _ _ err) = getErrorLoc err
getErrorLoc (InLHS _ _ err) = getErrorLoc err
@ -450,6 +451,12 @@ export %inline
Left err => pure (Left err)
Right val => runCore (f val)))
-- Flipped bind
infixr 1 =<<
export %inline
(=<<) : (a -> Core b) -> Core a -> Core b
(=<<) = flip (>>=)
-- Applicative (specialised)
export %inline
pure : a -> Core a
@ -500,7 +507,7 @@ for = flip traverse
export
traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
traverseList1 f (x :: xs) = [| f x :: traverse f xs |]
traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |]
export
traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
@ -530,7 +537,7 @@ sequence [] = pure []
export
traverseList1_ : (a -> Core b) -> List1 a -> Core ()
traverseList1_ f (x :: xs) = do
traverseList1_ f (x ::: xs) = do
f x
traverse_ f xs
@ -552,6 +559,26 @@ namespace Binder
traverse f (PLet fc c val ty) = pure $ PLet fc c !(f val) !(f ty)
traverse f (PVTy fc c ty) = pure $ PVTy fc c !(f ty)
export
mapTermM : ({vars : _} -> Term vars -> Core (Term vars)) ->
({vars : _} -> Term vars -> Core (Term vars))
mapTermM f = goTerm where
goTerm : {vars : _} -> Term vars -> Core (Term vars)
goTerm tm@(Local _ _ _ _) = f tm
goTerm tm@(Ref _ _ _) = f tm
goTerm (Meta fc n i args) = f =<< Meta fc n i <$> traverse goTerm args
goTerm (Bind fc x bd sc) = f =<< Bind fc x <$> traverse goTerm bd <*> goTerm sc
goTerm (App fc fn arg) = f =<< App fc <$> goTerm fn <*> goTerm arg
goTerm (As fc u as pat) = f =<< As fc u <$> goTerm as <*> goTerm pat
goTerm (TDelayed fc la d) = f =<< TDelayed fc la <$> goTerm d
goTerm (TDelay fc la ty arg) = f =<< TDelay fc la <$> goTerm ty <*> goTerm arg
goTerm (TForce fc la t) = f =<< TForce fc la <$> goTerm t
goTerm tm@(PrimVal _ _) = f tm
goTerm tm@(Erased _ _) = f tm
goTerm tm@(TType _) = f tm
export
anyM : (a -> Core Bool) -> List a -> Core Bool
anyM f [] = pure False

18
src/Core/Directory.idr
View File

@ -59,10 +59,10 @@ findLibraryFile fname
-- looking first in the build directory then in the extra_dirs
export
nsToPath : {auto c : Ref Ctxt Defs} ->
FC -> List String -> Core (Either Error String)
FC -> ModuleIdent -> Core (Either Error String)
nsToPath loc ns
= do d <- getDirs
let fnameBase = joinPath (reverse ns)
let fnameBase = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
let fs = map (\p => p </> fnameBase <.> "ttc")
((build_dir d </> "ttc") :: extra_dirs d)
Just f <- firstAvailable fs
@ -73,10 +73,10 @@ nsToPath loc ns
-- exists in the working directory)
export
nsToSource : {auto c : Ref Ctxt Defs} ->
FC -> List String -> Core String
FC -> ModuleIdent -> Core String
nsToSource loc ns
= do d <- getDirs
let fnameOrig = joinPath (reverse ns)
let fnameOrig = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
let fs = map (\ext => fnameBase <.> ext)
[".idr", ".lidr", ".yaff", ".org", ".md"]
@ -87,7 +87,7 @@ nsToSource loc ns
-- Given a filename in the working directory + source directory, return the correct
-- namespace for it
export
pathToNS : String -> Maybe String -> String -> Core (List String)
pathToNS : String -> Maybe String -> String -> Core ModuleIdent
pathToNS wdir sdir fname
= let sdir = fromMaybe "" sdir
base = if isAbsolute fname then wdir </> sdir else sdir
@ -96,7 +96,7 @@ pathToNS wdir sdir fname
Nothing => throw (UserError ("Source file " ++ show fname
++ " is not in the source directory "
++ show (wdir </> sdir)))
Just p => pure $ map show $ reverse $ (parse (p <.> "")).body
Just p => pure $ unsafeFoldModuleIdent $ map show $ reverse $ (parse (p <.> "")).body
dirExists : String -> IO Bool
dirExists dir = do Right d <- openDir dir
@ -124,11 +124,11 @@ mkdirAll dir = if parse dir == emptyPath
export
covering
makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
List String -> Core ()
ModuleIdent -> Core ()
makeBuildDirectory ns
= do d <- getDirs
let bdir = build_dir d </> "ttc"
let ns = reverse $ fromMaybe [] (tail' ns) -- first item is file name
let ns = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns -- first item is file name
let ndir = joinPath ns
Right _ <- coreLift $ mkdirAll (bdir </> ndir)
| Left err => throw (FileErr (build_dir d </> ndir) err)
@ -152,7 +152,7 @@ getTTCFileName inp ext
-- Get its namespace from the file relative to the working directory
-- and generate the ttc file from that
ns <- pathToNS (working_dir d) (source_dir d) inp
let fname = joinPath (reverse ns) <.> ext
let fname = joinPath (reverse $ unsafeUnfoldModuleIdent ns) <.> ext
let bdir = build_dir d
pure $ bdir </> "ttc" </> fname

33
src/Core/FC.idr
View File

@ -1,9 +1,13 @@
module Core.FC
import Text.Bounded
import Text.PrettyPrint.Prettyprinter
%default total
------------------------------------------------------------------------
-- Types
public export
FilePos : Type
FilePos = (Int, Int)
@ -20,11 +24,8 @@ public export
data FC = MkFC FileName FilePos FilePos
| EmptyFC
export
Eq FC where
(==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e'
(==) EmptyFC EmptyFC = True
(==) _ _ = False
------------------------------------------------------------------------
-- Projections
export
file : FC -> FileName
@ -41,6 +42,16 @@ endPos : FC -> FilePos
endPos (MkFC _ _ e) = e
endPos EmptyFC = (0, 0)
------------------------------------------------------------------------
-- Smart constructor
export
boundToFC : FileName -> WithBounds t -> FC
boundToFC fname b = MkFC fname (start b) (end b)
------------------------------------------------------------------------
-- Predicates
-- Return whether a given file position is within the file context (assuming we're
-- in the right file)
export
@ -57,6 +68,9 @@ onLine x (MkFC _ start end)
= x >= fst start && x <= fst end
onLine _ _ = False
------------------------------------------------------------------------
-- Constant values
export
emptyFC : FC
emptyFC = EmptyFC
@ -67,6 +81,15 @@ toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0)
%name FC fc
------------------------------------------------------------------------
-- Instances
export
Eq FC where
(==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e'
(==) EmptyFC EmptyFC = True
(==) _ _ = False
export
Show FC where
show loc = file loc ++ ":" ++

9
src/Core/Hash.idr
View File

@ -4,6 +4,7 @@ import Core.CaseTree
import Core.TT
import Data.List
import Data.List1
import Data.Strings
%default covering
@ -44,6 +45,10 @@ Hashable a => Hashable (List a) where
hashWithSalt h [] = abs h
hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs
export
Hashable a => Hashable (List1 a) where
hashWithSalt h (x ::: xs) = hashWithSalt (h * 33 + hash x) xs
export
Hashable a => Hashable (Maybe a) where
hashWithSalt h Nothing = abs h
@ -61,6 +66,10 @@ Hashable String where
else hashChars (h * 33 + cast (strIndex str p))
(p + 1) len str
export
Hashable Namespace where
hashWithSalt h ns = hashWithSalt h (unsafeUnfoldNamespace ns)
export
Hashable Name where
hashWithSalt h (MN s _) = hashWithSalt h s

1
src/Core/LinearCheck.idr
View File

@ -2,6 +2,7 @@ module Core.LinearCheck
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Normalise

52
src/Core/Name.idr
View File

@ -1,15 +1,20 @@
module Core.Name
import Data.List
import Data.Strings
import Decidable.Equality
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Util
import public Core.Name.Namespace
%default total
||| Name helps us track a name's structure as well as its origin:
||| was it user-provided or machine-manufactured? For what reason?
public export
data Name : Type where
NS : List String -> Name -> Name -- in a namespace
NS : Namespace -> Name -> Name -- in a namespace
UN : String -> Name -- user defined name
MN : String -> Int -> Name -- machine generated name
PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id
@ -19,22 +24,32 @@ data Name : Type where
WithBlock : String -> Int -> Name -- with block nested in (resolved) name
Resolved : Int -> Name -- resolved, index into context
export
mkNamespacedName : Maybe Namespace -> String -> Name
mkNamespacedName Nothing nm = UN nm
mkNamespacedName (Just ns) nm = NS ns (UN nm)
||| `matches a b` checks that the name `a` matches `b` assuming
||| the name roots are already known to be matching.
||| For instance, both `reverse` and `List.reverse` match the fully
||| qualified name `Data.List.reverse`.
export
matches : Name -> Name -> Bool
matches (NS ns _) (NS cns _) = isApproximationOf ns cns
matches (NS _ _) _
-- gallais: I don't understand this case but that's what was there.
= True -- no in library name, so root doesn't match
matches _ _ = True -- no prefix, so root must match, so good
-- Update a name imported with 'import as', for creating an alias
export
asName : List String -> -- Initial module name
List String -> -- 'as' module name
asName : ModuleIdent -> -- Initial module name
Namespace -> -- 'as' module name
Name -> -- identifier
Name
asName mod ns (DN s n) = DN s (asName mod ns n)
asName mod ns (NS oldns n)
= NS (updateNS mod oldns) n
where
updateNS : List String -> List String -> List String
updateNS mod (m :: ms)
= if mod == m :: ms
then ns
else m :: updateNS mod ms
updateNS mod [] = []
asName old new (DN s n) = DN s (asName old new n)
asName old new (NS ns n)
= NS (replace old new ns) n
asName _ _ n = n
export
@ -76,15 +91,9 @@ dropAllNS : Name -> Name
dropAllNS (NS _ n) = dropAllNS n
dropAllNS n = n
export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
export
Show Name where
show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n
show (NS ns n) = show ns ++ "." ++ show n
show (UN x) = x
show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
@ -97,7 +106,7 @@ Show Name where
export
Pretty Name where
pretty (NS ns n) = concatWith (surround dot) (pretty <$> reverse ns) <+> dot <+> pretty n
pretty (NS ns n) = pretty ns <+> dot <+> pretty n
pretty (UN x) = pretty x
pretty (MN x y) = braces (pretty x <+> colon <+> pretty y)
pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d)
@ -171,6 +180,7 @@ Ord Name where
compare x y = compare (nameTag x) (nameTag y)
export
nameEq : (x : Name) -> (y : Name) -> Maybe (x = y)
nameEq (NS xs x) (NS ys y) with (decEq xs ys)

271
src/Core/Name/Namespace.idr Normal file
View File

@ -0,0 +1,271 @@
module Core.Name.Namespace
import Data.List
import Data.List1
import Data.Strings
import Decidable.Equality
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Util
%default total
-------------------------------------------------------------------------------------
-- TYPES
-------------------------------------------------------------------------------------
||| Nested namespaces are stored in reverse order.
||| i.e. `X.Y.Z.foo` will be represented as `NS [Z,Y,X] foo`
||| As a consequence we hide the representation behind an opaque type alias
||| and force users to manufacture and manipulate namespaces via the safe
||| functions we provide.
export
data Namespace : Type where
MkNS : List String -> Namespace
||| A Module Identifier is, similarly to a namespace, stored inside out.
export
data ModuleIdent : Type where
MkMI : List String -> ModuleIdent
||| Sometimes we need to convert a module identifier to the corresponding
||| namespace. It is still useful to have them as distinct types as it
||| clarifies the distinct roles of X.Y.Z as a module name vs. S.T.U as a
||| namespace in `import X.Y.Z as S.T.U`.
export
miAsNamespace : ModuleIdent -> Namespace
miAsNamespace (MkMI mi) = MkNS mi
||| Sometimes we need to convert a namespace to the corresponding
||| module identifier. It is still useful to have them as distinct types as
||| it clarifies the distinct roles of X.Y.Z as a module name vs. S.T.U as a
||| namespace in `import X.Y.Z as S.T.U`.
export
nsAsModuleIdent : Namespace -> ModuleIdent
nsAsModuleIdent (MkNS ns) = MkMI ns
-------------------------------------------------------------------------------------
-- SMART CONSTRUCTORS
-------------------------------------------------------------------------------------
export
mkNamespacedIdent : String -> (Maybe Namespace, String)
mkNamespacedIdent str = case reverse (split (== '.') str) of
(name ::: []) => (Nothing, name)
(name ::: ns) => (Just (MkNS ns), name)
export
mkNestedNamespace : Maybe Namespace -> String -> Namespace
mkNestedNamespace Nothing n = MkNS [n]
mkNestedNamespace (Just (MkNS ns)) n = MkNS (n :: ns)
export
mkNamespace : String -> Namespace
mkNamespace "" = MkNS []
mkNamespace str = uncurry mkNestedNamespace (mkNamespacedIdent str)
export
mkModuleIdent : Maybe Namespace -> String -> ModuleIdent
mkModuleIdent Nothing n = MkMI [n]
mkModuleIdent (Just (MkNS ns)) n = MkMI (n :: ns)
-------------------------------------------------------------------------------------
-- MANIPULATING NAMESPACES
-------------------------------------------------------------------------------------
infixl 5 <.>
||| Extend an existing namespace with additional name parts to form a more local one.
||| e.g. `X.Y.Z <.> S.T.U` to get `X.Y.Z.S.T.U`.
export
(<.>) : (existing, local : Namespace) -> Namespace
(MkNS existing) <.> (MkNS local)
-- The namespaces are stored in reverse order so the local should end up at
-- the front of the existing one
= MkNS (local ++ existing)
export
replace : (old : ModuleIdent) -> (new, ns : Namespace) -> Namespace
replace (MkMI old) (MkNS new) (MkNS ns) = MkNS (go ns) where
go : List String -> List String
go [] = []
go (m :: ms)
= if old == (m :: ms)
then new
else m :: go ms
||| Use at your own risks!
export
unsafeUnfoldNamespace : Namespace -> List String
unsafeUnfoldNamespace (MkNS ns) = ns
export
unsafeFoldNamespace : List String -> Namespace
unsafeFoldNamespace = MkNS
export
unsafeUnfoldModuleIdent : ModuleIdent -> List String
unsafeUnfoldModuleIdent (MkMI ns) = ns
export
unsafeFoldModuleIdent : List String -> ModuleIdent
unsafeFoldModuleIdent = MkMI
-------------------------------------------------------------------------------------
-- HIERARCHICAL STRUCTURE
-------------------------------------------------------------------------------------
-- We don't use the prefix/suffix terminology as it is confusing: are we talking
-- about the namespaces or their representation? Instead our library is structured
-- around the parent/child relation induced by nested namespaces.
||| Nested namespaces naturally give rise to a hierarchical structure. In particular
||| from a given namespace we can compute all of the parent (aka englobing) ones.
||| For instance `allParents Data.List.Properties` should yield a set containing
||| both `Data.List` and `Data` (no guarantee is given on the order).
export
allParents : Namespace -> List Namespace
allParents (MkNS ns) = go ns where
go : List String -> List Namespace
go [] = []
go (n :: ns) = MkNS (n :: ns) :: go ns
||| We can check whether a given namespace is a parent (aka englobing) namespace
||| of a candidate namespace.
||| We expect that `all (\ p => isParentOf p ns) (allParents ns)` holds true.
export
isParentOf : (given, candidate : Namespace) -> Bool
isParentOf (MkNS ms) (MkNS ns)
-- This is not a typo: namespaces are stored in reverse order so a namespace is
-- a prefix of another if its reversed list of identifiers is a suffix of that
-- other's list of identifiers
= isSuffixOf ms ns
||| When writing qualified names users often do not want to spell out the full
||| namespace, rightly considering that an unambiguous segment should be enough.
||| This function checks whether a candidate is an approximation of a given
||| namespace.
||| We expect `isApproximationOf List.Properties Data.List.Properties` to hold true
||| while `isApproximationOf Data.List Data.List.Properties` should not.
export
isApproximationOf : (given, candidate : Namespace) -> Bool
isApproximationOf (MkNS ms) (MkNS ns)
-- This is not a typo: namespaces are stored in reverse order so a namespace matches
-- the end of another if its representation as a list of identifiers is a prefix of
-- the other's.
= isPrefixOf ms ns
-------------------------------------------------------------------------------------
-- INSTANCES
-------------------------------------------------------------------------------------
export
Eq Namespace where
(MkNS ms) == (MkNS ns) = ms == ns
export
Eq ModuleIdent where
(MkMI ms) == (MkMI ns) = ms == ns
export
Ord Namespace where
compare (MkNS ms) (MkNS ns) = compare ms ns
mkNSInjective : MkNS ms === MkNS ns -> ms === ns
mkNSInjective Refl = Refl
export
DecEq Namespace where
decEq (MkNS ms) (MkNS ns) with (decEq ms ns)
decEq (MkNS ms) (MkNS ns) | No contra = No (contra . mkNSInjective)
decEq (MkNS ms) (MkNS ns) | Yes eqmsns = Yes (cong MkNS eqmsns)
-- TODO: move somewhere more appropriate
export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
export
showNSWithSep : String -> Namespace -> String
showNSWithSep sep (MkNS ns) = showSep sep (reverse ns)
export
Show Namespace where
show = showNSWithSep "."
export
Show ModuleIdent where
show = showNSWithSep "." . miAsNamespace
export
Pretty Namespace where
pretty (MkNS ns) = concatWith (surround dot) (pretty <$> reverse ns)
export
Pretty ModuleIdent where
pretty = pretty . miAsNamespace
-------------------------------------------------------------------------------------
-- CONSTANTS
-------------------------------------------------------------------------------------
||| This is used when evaluating things in the REPL
export
emptyNS : Namespace
emptyNS = mkNamespace ""
export
mainNS : Namespace
mainNS = mkNamespace "Main"
export
partialEvalNS : Namespace
partialEvalNS = mkNamespace "_PE"
export
builtinNS : Namespace
builtinNS = mkNamespace "Builtin"
export
preludeNS : Namespace
preludeNS = mkNamespace "Prelude"
export
typesNS : Namespace
typesNS = mkNamespace "Prelude.Types"
export
basicsNS : Namespace
basicsNS = mkNamespace "Prelude.Basics"
export
eqOrdNS : Namespace
eqOrdNS = mkNamespace "Prelude.EqOrd"
export
primIONS : Namespace
primIONS = mkNamespace "PrimIO"
export
reflectionNS : Namespace
reflectionNS = mkNamespace "Language.Reflection"
export
reflectionTTNS : Namespace
reflectionTTNS = mkNamespace "Language.Reflection.TT"
export
reflectionTTImpNS : Namespace
reflectionTTImpNS = mkNamespace "Language.Reflection.TTImp"
export
dpairNS : Namespace
dpairNS = mkNamespace "Builtin.DPair"
export
natNS : Namespace
natNS = mkNamespace "Data.Nat"

49
src/Core/Normalise.idr
View File

@ -2,6 +2,7 @@ module Core.Normalise
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Options
@ -290,8 +291,8 @@ parameters (defs : Defs, topopts : EvalOpts)
then evalConAlt env loc opts fc stk args args' sc
else pure NoMatch
-- Primitive type matching, in typecase
tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase (UN x) tag [] sc)
= if show c == x
tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase nm tag [] sc)
= if UN (show c) == nm
then evalTree env loc opts fc stk sc
else pure NoMatch
-- Type of type matching, in typecase
@ -332,11 +333,16 @@ parameters (defs : Defs, topopts : EvalOpts)
LocalEnv free args -> EvalOpts -> FC ->
Stack free -> NF free -> List (CaseAlt args) ->
Core (CaseResult (NF free))
findAlt env loc opts fc stk val [] = pure GotStuck
findAlt env loc opts fc stk val [] = do
log "eval.casetree.stuck" 2 "Ran out of alternatives"
pure GotStuck
findAlt env loc opts fc stk val (x :: xs)
= do Result val <- tryAlt env loc opts fc stk val x
| NoMatch => findAlt env loc opts fc stk val xs
| GotStuck => pure GotStuck
| GotStuck => do
logC "eval.casetree.stuck" 5 $
pure $ "Got stuck matching " ++ show val ++ " against " ++ show !(toFullNames x)
pure GotStuck
pure (Result val)
evalTree : {auto c : Ref Ctxt Defs} ->
@ -344,8 +350,11 @@ parameters (defs : Defs, topopts : EvalOpts)
EvalOpts -> FC ->
Stack free -> CaseTree args ->
Core (CaseResult (NF free))
evalTree env loc opts fc stk (Case idx x _ alts)
evalTree env loc opts fc stk (Case {name} idx x _ alts)
= do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
-- we have not defined quote yet (it depends on eval itself) so we show the NF
-- i.e. only the top-level constructor.
log "eval.casetree" 5 $ "Evaluated " ++ show name ++ " to " ++ show xval
let loc' = updateLocal idx (varExtend x) loc xval
findAlt env loc' opts fc stk xval alts
evalTree env loc opts fc stk (STerm _ tm)
@ -725,6 +734,36 @@ normaliseScope defs env (Bind fc n b sc)
= pure $ Bind fc n b !(normaliseScope defs (b :: env) sc)
normaliseScope defs env tm = normalise defs env tm
export
etaContract : {auto _ : Ref Ctxt Defs} ->
{vars : _} -> Term vars -> Core (Term vars)
etaContract tm = do
defs <- get Ctxt
logTerm "eval.eta" 5 "Attempting to eta contract subterms of" tm
nf <- normalise defs (mkEnv EmptyFC _) tm
logTerm "eval.eta" 5 "Evaluated to" nf
res <- mapTermM act tm
logTerm "eval.eta" 5 "Result of eta-contraction" res
pure res
where
act : {vars : _} -> Term vars -> Core (Term vars)
act tm = do
logTerm "eval.eta" 10 " Considering" tm
case tm of
(Bind _ x (Lam _ _ _ _) (App _ fn (Local _ _ Z _))) => do
logTerm "eval.eta" 10 " Shrinking candidate" fn
let shrunk = shrinkTerm fn (DropCons SubRefl)
case shrunk of
Nothing => do
log "eval.eta" 10 " Failure!"
pure tm
Just tm' => do
logTerm "eval.eta" 10 " Success!" tm'
pure tm'
_ => pure tm
public export
interface Convert (tm : List Name -> Type) where
convert : {auto c : Ref Ctxt Defs} ->

6
src/Core/Options/Log.idr
View File

@ -44,7 +44,7 @@ data LogLevel : Type where
||| non-empty topics we can safely make a `LogLevel`.
export
mkLogLevel' : Maybe (List1 String) -> Nat -> LogLevel
mkLogLevel' ps n = MkLogLevel (maybe [] List1.toList ps) n
mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n
||| The smart constructor makes sure that the empty string is mapped to the empty
||| list. This bypasses the fact that the function `split` returns a non-empty
@ -94,8 +94,8 @@ export
parseLogLevel : String -> Maybe LogLevel
parseLogLevel str = do
(c, n) <- case split (== ':') str of
[n] => pure (MkLogLevel [], n)
[ps,n] => pure (mkLogLevel ps, n)
n ::: [] => pure (MkLogLevel [], n)
ps ::: [n] => pure (mkLogLevel ps, n)
_ => Nothing
lvl <- parsePositive n
pure $ c (fromInteger lvl)

49
src/Core/Reflect.idr
View File

@ -1,6 +1,7 @@
module Core.Reflect
import Algebra.Semiring
import Data.List1
import Core.Context
import Core.Env
@ -41,31 +42,31 @@ appCon fc defs n args
export
preludetypes : String -> Name
preludetypes n = NS ["Types", "Prelude"] (UN n)
preludetypes n = NS typesNS (UN n)
export
basics : String -> Name
basics n = NS ["Basics", "Prelude"] (UN n)
basics n = NS basicsNS (UN n)
export
builtin : String -> Name
builtin n = NS ["Builtin"] (UN n)
builtin n = NS builtinNS (UN n)
export
primio : String -> Name
primio n = NS ["PrimIO"] (UN n)
primio n = NS primIONS (UN n)
export
reflection : String -> Name
reflection n = NS ["Reflection", "Language"] (UN n)
reflection n = NS reflectionNS (UN n)
export
reflectiontt : String -> Name
reflectiontt n = NS ["TT", "Reflection", "Language"] (UN n)
reflectiontt n = NS reflectionTTNS (UN n)
export
reflectionttimp : String -> Name
reflectionttimp n = NS ["TTImp", "Reflection", "Language"] (UN n)
reflectionttimp n = NS reflectionTTImpNS (UN n)
export
cantReify : NF vars -> String -> Core a
@ -182,6 +183,24 @@ Reflect a => Reflect (List a) where
xs' <- reflect fc defs lhs env xs
appCon fc defs (preludetypes "::") [Erased fc False, x', xs']
export
Reify a => Reify (List1 a) where
reify defs val@(NDCon _ n _ _ [_, x, xs])
= case !(full (gamma defs) n) of
NS _ (UN ":::")
=> do x' <- reify defs !(evalClosure defs x)
xs' <- reify defs !(evalClosure defs xs)
pure (x' ::: xs')
_ => cantReify val "List1"
reify defs val = cantReify val "List1"
export
Reflect a => Reflect (List1 a) where
reflect fc defs lhs env (x ::: xs)
= do x' <- reflect fc defs lhs env x
xs' <- reflect fc defs lhs env xs
appCon fc defs (NS (mkNamespace "Data.List1") (UN ":::")) [Erased fc False, x', xs']
export
Reify a => Reify (Maybe a) where
reify defs val@(NDCon _ n _ _ args)
@ -218,6 +237,22 @@ export
y' <- reflect fc defs lhs env y
appCon fc defs (builtin "MkPair") [Erased fc False, Erased fc False, x', y']
export
Reify Namespace where
reify defs val@(NDCon _ n _ _ [ns])
= case (!(full (gamma defs) n)) of
NS _ (UN "MkNS")
=> do ns' <- reify defs !(evalClosure defs ns)
pure (unsafeFoldNamespace ns')
_ => cantReify val "Namespace"
reify defs val = cantReify val "Namespace"
export
Reflect Namespace where
reflect fc defs lhs env ns
= do ns' <- reflect fc defs lhs env (unsafeUnfoldNamespace ns)
appCon fc defs (reflectiontt "MkNS") [ns']
export
Reify Name where
reify defs val@(NDCon _ n _ _ args)

50
src/Core/TT.idr
View File

@ -358,9 +358,6 @@ setMultiplicity (PVar fc _ p ty) c = PVar fc c p ty
setMultiplicity (PLet fc _ val ty) c = PLet fc c val ty
setMultiplicity (PVTy fc _ ty) c = PVTy fc c ty
showCount : RigCount -> String
showCount = elimSemi "0 " "1 " (const "")
Show ty => Show (Binder ty) where
show (Lam _ c _ t) = "\\" ++ showCount c ++ show t
show (Pi _ c _ t) = "Pi " ++ showCount c ++ show t
@ -1398,44 +1395,36 @@ nameAt : {vars : _} -> {idx : Nat} -> (0 p : IsVar n idx vars) -> Name
nameAt {vars = n :: ns} First = n
nameAt {vars = n :: ns} (Later p) = nameAt p
export
withPiInfo : Show t => PiInfo t -> String -> String
withPiInfo Explicit tm = "(" ++ tm ++ ")"
withPiInfo Implicit tm = "{" ++ tm ++ "}"
withPiInfo AutoImplicit tm = "{auto " ++ tm ++ "}"
withPiInfo (DefImplicit t) tm = "{default " ++ show t ++ " " ++ tm ++ "}"
export
{vars : _} -> Show (Term vars) where
show tm = let (fn, args) = getFnArgs tm in showApp fn args
where
showApp : {vars : _} -> Term vars -> List (Term vars) -> String
showApp (Local {name} _ c idx p) []
showApp (Local _ c idx p) []
= show (nameAt p) ++ "[" ++ show idx ++ "]"
showApp (Ref _ _ n) [] = show n
showApp (Meta _ n i args) []
showApp (Meta _ n _ args) []
= "?" ++ show n ++ "_" ++ show args
showApp (Bind _ x (Lam _ c p ty) sc) []
= "\\" ++ showCount c ++ show x ++ " : " ++ show ty ++
showApp (Bind _ x (Lam _ c info ty) sc) []
= "\\" ++ withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++
" => " ++ show sc
showApp (Bind _ x (Let _ c val ty) sc) []
= "let " ++ showCount c ++ show x ++ " : " ++ show ty ++
" = " ++ show val ++ " in " ++ show sc
showApp (Bind _ x (Pi _ c Explicit ty) sc) []
= "((" ++ showCount c ++ show x ++ " : " ++ show ty ++
") -> " ++ show sc ++ ")"
showApp (Bind _ x (Pi _ c Implicit ty) sc) []
= "{" ++ showCount c ++ show x ++ " : " ++ show ty ++
"} -> " ++ show sc
showApp (Bind _ x (Pi _ c AutoImplicit ty) sc) []
= "{auto " ++ showCount c ++ show x ++ " : " ++ show ty ++
"} -> " ++ show sc
showApp (Bind _ x (Pi _ c (DefImplicit tm) ty) sc) []
= "{default " ++ show tm ++ " "
++ showCount c ++ show x ++ " : " ++ show ty ++
"} -> " ++ show sc
showApp (Bind _ x (PVar _ c Explicit ty) sc) []
= "pat " ++ showCount c ++ show x ++ " : " ++ show ty ++
showApp (Bind _ x (Pi _ c info ty) sc) []
= withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++
" -> " ++ show sc ++ ")"
showApp (Bind _ x (PVar _ c info ty) sc) []
= withPiInfo info ("pat " ++ showCount c ++ show x ++ " : " ++ show ty) ++
" => " ++ show sc
showApp (Bind _ x (PVar _ c Implicit ty) sc) []
= "{pat " ++ showCount c ++ show x ++ " : " ++ show ty ++
"} => " ++ show sc
showApp (Bind _ x (PVar _ c AutoImplicit ty) sc) []
= "{auto pat " ++ showCount c ++ show x ++ " : " ++ show ty ++
"} => " ++ show sc
showApp (Bind _ x (PLet _ c val ty) sc) []
= "plet " ++ showCount c ++ show x ++ " : " ++ show ty ++
" = " ++ show val ++ " in " ++ show sc
@ -1454,3 +1443,8 @@ export
showApp f args = "(" ++ assert_total (show f) ++ " " ++
assert_total (showSep " " (map show args))
++ ")"
export
{vars : _} -> Pretty (Term vars) where
pretty = pretty . show
-- TODO: prettier output

9
src/Core/TTC.idr
View File

@ -30,6 +30,15 @@ TTC FC where
pure (MkFC f s e)
1 => pure EmptyFC
_ => corrupt "FC"
export
TTC Namespace where
toBuf b = toBuf b . unsafeUnfoldNamespace
fromBuf = Core.map unsafeFoldNamespace . fromBuf
export
TTC ModuleIdent where
toBuf b = toBuf b . unsafeUnfoldModuleIdent
fromBuf = Core.map unsafeFoldModuleIdent . fromBuf
export
TTC Name where

52
src/Core/Termination.idr
View File

@ -2,6 +2,7 @@ module Core.Termination
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Env
import Core.Normalise
import Core.TT
@ -42,7 +43,8 @@ export
checkIfGuarded : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core ()
checkIfGuarded fc n
= do defs <- get Ctxt
= do log "totality.termination.guarded" 6 $ "Check if Guarded: " ++ show n
defs <- get Ctxt
Just (PMDef _ _ _ _ pats) <- lookupDefExact n (gamma defs)
| _ => pure ()
t <- allGuarded pats
@ -361,9 +363,9 @@ mutual
= do Just gdef <- lookupCtxtExact fn_in (gamma defs)
| Nothing => throw (UndefinedName fc fn_in)
let fn = fullname gdef
log "termination" 10 $ "Looking under " ++ show fn
aSmaller <- resolved (gamma defs) (NS ["Builtin"] (UN "assert_smaller"))
cond [(fn == NS ["Builtin"] (UN "assert_total"), pure []),
log "totality.termination.sizechange" 10 $ "Looking under " ++ show fn
aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller"))
cond [(fn == NS builtinNS (UN "assert_total"), pure []),
(caseFn fn,
do mps <- getCasePats defs fn pats args
case mps of
@ -381,10 +383,10 @@ mutual
(vs ** (Env Term vs, List (Nat, Term vs), Term vs)) ->
Core (List SCCall)
findInCase defs g (_ ** (env, pats, tm))
= do logC "termination" 10 $
= do logC "totality" 10 $
do ps <- traverse toFullNames (map snd pats)
pure ("Looking in case args " ++ show ps)
logTermNF "termination" 10 " =" env tm
logTermNF "totality" 10 " =" env tm
rhs <- normaliseOpts tcOnly defs env tm
findSC defs env g pats (delazy defs rhs)
@ -408,7 +410,8 @@ export
calculateSizeChange : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core (List SCCall)
calculateSizeChange loc n
= do defs <- get Ctxt
= do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show n
defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName loc n)
getSC defs (definition def)
@ -444,12 +447,16 @@ checkSC : {auto a : Ref APos Arg} ->
List (Name, List (Maybe Arg)) -> -- calls we've seen so far
Core Terminating
checkSC defs f args path
= let pos = (f, map (map Builtin.fst) args) in
if pos `elem` path
then toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
else case !(lookupCtxtExact f (gamma defs)) of
Nothing => pure IsTerminating
Just def => continue (sizeChange def) (pos :: path)
= do log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show f
let pos = (f, map (map Builtin.fst) args)
if pos `elem` path
then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show f
toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
else case !(lookupCtxtExact f (gamma defs)) of
Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show f
pure IsTerminating
Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show f
continue (sizeChange def) (pos :: path)
where
-- Look for something descending in the list of size changes
checkDesc : List SizeChange -> List (Name, List (Maybe Arg)) -> Terminating
@ -485,6 +492,7 @@ checkSC defs f args path
let Unchecked = isTerminating (totality gdef)
| IsTerminating => pure IsTerminating
| _ => pure (NotTerminating (BadCall [fnCall sc]))
log "totality.termination.sizechange.checkCall" 8 $ "CheckCall Size Change Graph: " ++ show (fnCall sc)
term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path
if not inpath
then case term of
@ -493,10 +501,13 @@ checkSC defs f args path
-- was mutually recursive, so start again with new
-- arguments (that is, where we'd start if the
-- function was the top level thing we were checking)
do args' <- initArgs (length (fnArgs sc))
do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show (fnCall sc)
args' <- initArgs (length (fnArgs sc))
checkSC defs (fnCall sc) args' path
t => pure t
else pure term
t => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show (fnCall sc)
pure t
else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show (fnCall sc)
pure term
getWorst : Terminating -> List Terminating -> Terminating
getWorst term [] = term
@ -513,6 +524,7 @@ calcTerminating : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core Terminating
calcTerminating loc n
= do defs <- get Ctxt
log "totality.termination.calc" 7 $ "Calculating termination: " ++ show n
case !(lookupCtxtExact n (gamma defs)) of
Nothing => throw (UndefinedName loc n)
Just def =>
@ -546,6 +558,7 @@ checkTerminating : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core Terminating
checkTerminating loc n
= do tot <- getTotality loc n
log "totality.termination" 6 $ "Checking termination: " ++ show n
case isTerminating tot of
Unchecked =>
do tot' <- calcTerminating loc n
@ -584,8 +597,8 @@ posArg defs tyns (NTCon _ tc _ _ args)
= case !(lookupDefExact tc (gamma defs)) of
Just (TCon _ _ params _ _ _ _ _) =>
dropParams 0 params args
_ => args in
if !(anyM (nameIn defs tyns)
_ => args
in if !(anyM (nameIn defs tyns)
!(traverse (evalClosure defs) testargs))
then pure (NotTerminating NotStrictlyPositive)
else pure IsTerminating
@ -638,6 +651,7 @@ calcPositive : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core (Terminating, List Name)
calcPositive loc n
= do defs <- get Ctxt
log "totality.positivity" 6 $ "Calculating positivity: " ++ show n
case !(lookupDefTyExact n (gamma defs)) of
Just (TCon _ _ _ _ _ tns dcons _, ty) =>
case !(totRefsIn defs ty) of
@ -656,6 +670,7 @@ checkPositive : {auto c : Ref Ctxt Defs} ->
checkPositive loc n_in
= do n <- toResolvedNames n_in
tot <- getTotality loc n
log "totality.positivity" 6 $ "Checking positivity: " ++ show n
case isTerminating tot of
Unchecked =>
do (tot', cons) <- calcPositive loc n
@ -675,6 +690,7 @@ checkTotal loc n_in
| Nothing => throw (UndefinedName loc n_in)
let n = Resolved nidx
tot <- getTotality loc n
log "totality" 5 $ "Checking totality: " ++ show n
defs <- get Ctxt
case isTerminating tot of
Unchecked =>

5
src/Core/Unify.idr
View File

@ -2,6 +2,7 @@ module Core.Unify
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.GetType
@ -1360,10 +1361,6 @@ Eq SolveMode where
_ == _ = False
ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e
retry : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
UnifyInfo -> Int -> Core UnifyResult

1
src/Core/UnifyState.idr
View File

@ -2,6 +2,7 @@ module Core.UnifyState
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.FC

36
src/Core/Value.idr
View File

@ -102,3 +102,39 @@ getLoc (NPrimVal fc _) = fc
getLoc (NErased fc i) = fc
getLoc (NType fc) = fc
export
{free : _} -> Show (NHead free) where
show (NLocal _ idx p) = show (nameAt p) ++ "[" ++ show idx ++ "]"
show (NRef _ n) = show n
show (NMeta n _ args) = "?" ++ show n ++ "_[" ++ show (length args) ++ " closures]"
export
{free : _} -> Show (NF free) where
show (NBind _ x (Lam _ c info ty) _)
= "\\" ++ withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++
" => [closure]"
show (NBind _ x (Let _ c val ty) _)
= "let " ++ showCount c ++ show x ++ " : " ++ show ty ++
" = " ++ show val ++ " in [closure]"
show (NBind _ x (Pi _ c info ty) _)
= withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++
" -> [closure]"
show (NBind _ x (PVar _ c info ty) _)
= withPiInfo info ("pat " ++ showCount c ++ show x ++ " : " ++ show ty) ++
" => [closure]"
show (NBind _ x (PLet _ c val ty) _)
= "plet " ++ showCount c ++ show x ++ " : " ++ show ty ++
" = " ++ show val ++ " in [closure]"
show (NBind _ x (PVTy _ c ty) _)
= "pty " ++ showCount c ++ show x ++ " : " ++ show ty ++
" => [closure]"
show (NApp _ hd args) = show hd ++ " [" ++ show (length args) ++ " closures]"
show (NDCon _ n _ _ args) = show n ++ " [" ++ show (length args) ++ " closures]"
show (NTCon _ n _ _ args) = show n ++ " [" ++ show (length args) ++ " closures]"
show (NAs _ _ n tm) = show n ++ "@" ++ show tm
show (NDelayed _ _ tm) = "%Delayed " ++ show tm
show (NDelay _ _ _ _) = "%Delay [closure]"
show (NForce _ _ tm args) = "%Force " ++ show tm ++ " [" ++ show (length args) ++ " closures]"
show (NPrimVal _ c) = show c
show (NErased _ _) = "[__]"
show (NType _) = "Type"

11
src/Data/ANameMap.idr
View File

@ -36,17 +36,10 @@ lookupName n dict
Just res => [(n, res)]
Just r => case lookup r (hierarchy dict) of
Nothing => []
Just ns => filter (matches n) ns
where
-- Name matches if a prefix of the namespace matches a prefix of the
-- namespace in the context
matches : Name -> (Name, a) -> Bool
matches (NS ns _) (NS cns _, _) = ns `isPrefixOf` cns
matches (NS _ _) _ = True -- no in library name, so root doesn't match
matches _ _ = True -- no prefix, so root must match, so good
Just ns => filter (matches n . fst) ns
addToHier : Name -> a ->
StringMap (List (Name, a)) -> StringMap (List (Name, a))
StringMap (List (Name, a)) -> StringMap (List (Name, a))
addToHier n val hier
-- Only add user defined names. Machine generated names can only be
-- found with the exactNames

30
src/Idris/Desugar.idr
View File

@ -50,10 +50,6 @@ import Data.List
public export
data Side = LHS | AnyExpr
ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e
export
extendSyn : {auto s : Ref Syn SyntaxInfo} ->
SyntaxInfo -> Core ()
@ -118,6 +114,8 @@ bindBangs ((n, fc, btm) :: bs) tm
(Implicit fc False) tm)
idiomise : FC -> RawImp -> RawImp
idiomise fc (IAlternative afc u alts)
= IAlternative afc (mapAltType (idiomise afc) u) (idiomise afc <$> alts)
idiomise fc (IApp afc f a)
= IApp fc (IApp fc (IVar fc (UN "<*>"))
(idiomise afc f))
@ -125,16 +123,16 @@ idiomise fc (IApp afc f a)
idiomise fc fn = IApp fc (IVar fc (UN "pure")) fn
pairname : Name
pairname = NS ["Builtin"] (UN "Pair")
pairname = NS builtinNS (UN "Pair")
mkpairname : Name
mkpairname = NS ["Builtin"] (UN "MkPair")
mkpairname = NS builtinNS (UN "MkPair")
dpairname : Name
dpairname = NS ["DPair", "Builtin"] (UN "DPair")
dpairname = NS dpairNS (UN "DPair")
mkdpairname : Name
mkdpairname = NS ["DPair", "Builtin"] (UN "MkDPair")
mkdpairname = NS dpairNS (UN "MkDPair")
data Bang : Type where
@ -285,7 +283,10 @@ mutual
pure (IVar fc bn)
desugarB side ps (PIdiom fc term)
= do itm <- desugarB side ps term
pure (idiomise fc itm)
logRaw "desugar.idiom" 10 "Desugaring idiom for" itm
let val = idiomise fc itm
logRaw "desugar.idiom" 10 "Desugared to" val
pure val
desugarB side ps (PList fc args)
= expandList side ps fc args
desugarB side ps (PPair fc l r)
@ -414,7 +415,7 @@ mutual
= pure $ apply (IVar fc (UN "::"))
[!(desugarB side ps x), !(expandList side ps fc xs)]
addNS : Maybe (List String) -> Name -> Name
addNS : Maybe Namespace -> Name -> Name
addNS (Just ns) n@(NS _ _) = n
addNS (Just ns) n = NS ns n
addNS _ n = n
@ -423,7 +424,7 @@ mutual
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} ->
Side -> List Name -> FC -> Maybe (List String) -> List PDo -> Core RawImp
Side -> List Name -> FC -> Maybe Namespace -> List PDo -> Core RawImp
expandDo side ps fc ns [] = throw (GenericMsg fc "Do block cannot be empty")
expandDo side ps _ _ [DoExp fc tm] = desugar side ps tm
expandDo side ps fc ns [e]
@ -578,7 +579,7 @@ mutual
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} ->
List Name -> List String -> PField ->
List Name -> Namespace -> PField ->
Core IField
desugarField ps ns (MkField fc doc rig p n ty)
= do addDocStringNS ns n doc
@ -801,13 +802,14 @@ mutual
let paramsb = map (\ (n, c, p, tm) => (n, c, p, doBind bnames tm)) params'
let _ = the (List (Name, RigCount, PiInfo RawImp, RawImp)) paramsb
let recName = nameRoot tn
fields' <- traverse (desugarField (ps ++ map fname fields ++
map fst params) [nameRoot tn])
map fst params) (mkNamespace recName))
fields
let _ = the (List IField) fields'
let conname = maybe (mkConName tn) id conname_in
let _ = the Name conname
pure [IRecord fc (Just (nameRoot tn))
pure [IRecord fc (Just recName)
vis (MkImpRecord fc tn paramsb conname fields')]
where
fname : PField -> Name

6
src/Idris/DocString.idr
View File

@ -33,12 +33,12 @@ addDocString n_in doc
export
addDocStringNS : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
List String -> Name -> String ->
Namespace -> Name -> String ->
Core ()
addDocStringNS ns n_in doc
= do n <- inCurrentNS n_in
let n' = case n of
NS old root => NS (ns ++ old) root
NS old root => NS (old <.> ns) root
root => NS ns root
syn <- get Syn
put Syn (record { docstrings $= addName n' doc,
@ -171,7 +171,7 @@ summarise n -- n is fully qualified
export
getContents : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
List String -> Core (List String)
Namespace -> Core (List String)
getContents ns
= -- Get all the names, filter by any that match the given namespace
-- and are visible, then display with their type

1
src/Idris/Driver.idr
View File

@ -2,6 +2,7 @@ module Idris.Driver
import Compiler.Common
import Core.Context.Log
import Core.Core
import Core.InitPrimitives
import Core.Metadata

3
src/Idris/Elab/Implementation.idr
View File

@ -2,6 +2,7 @@ module Idris.Elab.Implementation
import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
@ -346,7 +347,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- parameters
let upds' = !(traverse (applyCon impName) allmeths)
let mty_in = substNames vars upds' mty_in
let (mty_in, upds) = runState (renameIBinds impsp (findImplicits mty_in) mty_in) []
let (upds, mty_in) = runState [] (renameIBinds impsp (findImplicits mty_in) mty_in)
-- Finally update the method type so that implicits from the
-- parameters are passed through to any earlier methods which
-- appear in the type

1
src/Idris/Elab/Interface.idr
View File

@ -2,6 +2,7 @@ module Idris.Elab.Interface
import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

16
src/Idris/Error.idr
View File

@ -36,9 +36,6 @@ pShowMN t env acc = case t of
_ => acc
_ => acc
joinNs : List String -> Doc (IdrisAnn)
joinNs ns = concatWith (surround dot) (pretty <$> reverse ns)
pshow : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -197,7 +194,7 @@ perror (UndefinedName fc x)
= pure $ errorDesc (reflow "Undefined name" <++> code (pretty x) <+> dot) <++> line <+> !(ploc fc)
perror (InvisibleName fc n (Just ns))
= pure $ errorDesc ("Name" <++> code (pretty n) <++> reflow "is inaccessible since"
<++> code (joinNs ns) <++> reflow "is not explicitly imported.")
<++> code (pretty ns) <++> reflow "is not explicitly imported.")
<+> line <+> !(ploc fc)
<+> line <+> reflow "Suggestion: add an explicit" <++> keyword "export" <++> "or" <++> keyword ("public" <++> "export")
<++> reflow "modifier. By default, all names are" <++> keyword "private" <++> reflow "in namespace blocks."
@ -419,12 +416,19 @@ perror (FileErr fname err)
perror (ParseFail _ err)
= pure $ pretty err
perror (ModuleNotFound fc ns)
= pure $ errorDesc ("Module" <++> annotate FileCtxt (joinNs ns) <++> reflow "not found") <+> line <+> !(ploc fc)
= pure $ errorDesc ("Module" <++> annotate FileCtxt (pretty ns) <++> reflow "not found") <+> line <+> !(ploc fc)
perror (CyclicImports ns)
= pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround (pretty " -> ")) (joinNs <$> ns)
= pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround (pretty " -> ")) (pretty <$> ns)
perror ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness")
perror (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty str
perror (UserError str) = pure $ errorDesc (pretty "Error" <+> colon) <++> pretty str
perror (NoForeignCC fc) = do
let cgs = fst <$> availableCGs (options !(get Ctxt))
let res = vsep [ errorDesc (reflow "The given specifier was not accepted by any backend. Available backends" <+> colon)
, indent 2 (concatWith (\x,y => x <+> ", " <+> y) (map reflow cgs))
, reflow "Some backends have additional specifier rules, refer to their documentation."
] <+> line <+> !(ploc fc)
pure res
perror (InType fc n err)
= pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty !(prettyName n))) <+> dot

10
src/Idris/IDEMode/Holes.idr
View File

@ -51,12 +51,6 @@ showName (UN "_") = False
showName (MN _ _) = False
showName _ = True
showCount : RigCount -> String
showCount = elimSemi
" 0 "
" 1 "
(const " ")
impBracket : Bool -> String -> String
impBracket False str = str
impBracket True str = "{" ++ str ++ "}"
@ -126,7 +120,7 @@ showHole defs env fn args ty
case hdata.context of
[] => pure $ show (hdata.name) ++ " : " ++ show hdata.type
_ => pure $ concat
(map (\premise => showCount premise.multiplicity
(map (\premise => " " ++ showCount premise.multiplicity ++ " "
++ (impBracket premise.isImplicit $
tidy premise.name ++ " : " ++ (show premise.type) ++ "\n" )
) hdata.context)
@ -158,7 +152,7 @@ prettyHole defs env fn args ty
sexpPremise : HolePremise -> SExp
sexpPremise premise =
SExpList [StringAtom $ showCount premise.multiplicity
SExpList [StringAtom $ " " ++ showCount premise.multiplicity ++ " "
++ (impBracket premise.isImplicit $
tidy premise.name)
,StringAtom $ show premise.type

4
src/Idris/IDEMode/Parser.idr
View File

@ -5,10 +5,12 @@ module Idris.IDEMode.Parser
import Idris.IDEMode.Commands
import Data.Maybe
import Data.List
import Data.Strings
import Parser.Lexer.Source
import Parser.Source
import Parser.Support
import Text.Lexer
import Text.Parser
import Utils.Either
@ -26,7 +28,7 @@ ideTokens : TokenMap Token
ideTokens =
map (\x => (exact x, Symbol)) symbols ++
[(digits, \x => IntegerLit (cast x)),
(stringLit, \x => StringLit (stripQuotes x)),
(stringLit, \x => StringLit (fromMaybe "" (escape (stripQuotes x)))),
(identAllowDashes, \x => Ident x),
(space, Comment)]

2
src/Idris/IDEMode/REPL.idr
View File

@ -200,7 +200,7 @@ process (CallsWho n)
= do todoCmd "calls-who"
pure $ NameList []
process (BrowseNamespace ns)
= replWrap $ Idris.REPL.process (Browse (List1.toList $ reverse (split (=='.') ns)))
= replWrap $ Idris.REPL.process (Browse (mkNamespace ns))
process (NormaliseTerm tm)
= do todoCmd "normalise-term"
pure $ Term tm

31
src/Idris/ModTree.idr
View File

@ -2,6 +2,7 @@ module Idris.ModTree
import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.Metadata
@ -30,7 +31,7 @@ import Utils.Either
record ModTree where
constructor MkModTree
nspace : List String
nspace : ModuleIdent
sourceFile : Maybe String
deps : List ModTree
@ -49,25 +50,23 @@ public export
record BuildMod where
constructor MkBuildMod
buildFile : String
buildNS : List String
imports : List (List String)
buildNS : ModuleIdent
imports : List ModuleIdent
export
Show BuildMod where
show t = buildFile t ++ " [" ++ showSep ", " (map showNS (imports t)) ++ "]"
where
showNS : List String -> String
showNS ns = showSep "." (reverse ns)
show t = buildFile t ++ " [" ++ showSep ", " (map show (imports t)) ++ "]"
data AllMods : Type where
mkModTree : {auto c : Ref Ctxt Defs} ->
{auto a : Ref AllMods (List (List String, ModTree))} ->
{auto a : Ref AllMods (List (ModuleIdent, ModTree))} ->
FC ->
(done : List (List String)) -> -- if 'mod' is here we have a cycle
(mod : List String) ->
(done : List ModuleIdent) -> -- if 'mod' is here we have a cycle
(modFP : Maybe FileName) -> -- Sometimes we know already know what the file name is
(mod : ModuleIdent) -> -- Otherwise we'll compute it from the module name
Core ModTree
mkModTree loc done mod
mkModTree loc done modFP mod
= if mod `elem` done
then throw (CyclicImports (done ++ [mod]))
else
@ -77,10 +76,10 @@ mkModTree loc done mod
-- If we've seen it before, reuse what we found
case lookup mod all of
Nothing =>
do file <- nsToSource loc mod
do file <- maybe (nsToSource loc mod) pure modFP
modInfo <- readHeader file
let imps = map path (imports modInfo)
ms <- traverse (mkModTree loc (mod :: done)) imps
ms <- traverse (mkModTree loc (mod :: done) Nothing) imps
let mt = MkModTree mod (Just file) ms
all <- get AllMods
put AllMods ((mod, mt) :: all)
@ -133,7 +132,7 @@ getBuildMods loc done fname
if fname_ns `elem` map buildNS done
then pure []
else
do t <- mkModTree {a} loc [] fname_ns
do t <- mkModTree {a} loc [] (Just fname) fname_ns
dm <- newRef DoneMod empty
o <- newRef BuildOrder []
mkBuildMods {d=dm} {o} t
@ -180,11 +179,9 @@ buildMod loc num len mod
m <- newRef MD initMetadata
put Syn initSyntax
let showMod : Doc IdrisAnn = concatWith (surround dot) (pretty <$> reverse mod.buildNS)
if needsBuilding
then do let msg : Doc IdrisAnn = pretty num <+> slash <+> pretty len <+> colon
<++> pretty "Building" <++> showMod <++> parens (pretty src)
<++> pretty "Building" <++> pretty mod.buildNS <++> parens (pretty src)
[] <- process {u} {m} msg src
| errs => do emitWarnings
traverse emitError errs

56
src/Idris/Package.idr
View File

@ -10,7 +10,6 @@ import Core.Options
import Core.Unify
import Data.List
import Data.List1
import Data.Maybe
import Data.So
import Data.StringMap
@ -54,8 +53,8 @@ record PkgDesc where
sourceloc : Maybe String
bugtracker : Maybe String
depends : List String -- packages to add to search path
modules : List (List1 String, String) -- modules to install (namespace, filename)
mainmod : Maybe (List1 String, String) -- main file (i.e. file to load at REPL)
modules : List (ModuleIdent, String) -- modules to install (namespace, filename)
mainmod : Maybe (ModuleIdent, String) -- main file (i.e. file to load at REPL)
executable : Maybe String -- name of executable
options : Maybe (FC, String)
sourcedir : Maybe String
@ -113,8 +112,8 @@ data DescField : Type where
PSourceLoc : FC -> String -> DescField
PBugTracker : FC -> String -> DescField
PDepends : List String -> DescField
PModules : List (FC, List1 String) -> DescField
PMainMod : FC -> List1 String -> DescField
PModules : List (FC, ModuleIdent) -> DescField
PMainMod : FC -> ModuleIdent -> DescField
PExec : String -> DescField
POpts : FC -> String -> DescField
PSourceDir : FC -> String -> DescField
@ -163,7 +162,7 @@ field fname
<|> do exactProperty "main"
equals
start <- location
m <- namespacedIdent
m <- moduleIdent
end <- location
pure (PMainMod (MkFC fname start end) m)
<|> do exactProperty "executable"
@ -192,8 +191,8 @@ data ParsedMods : Type where
data MainMod : Type where
addField : {auto c : Ref Ctxt Defs} ->
{auto p : Ref ParsedMods (List (FC, List1 String))} ->
{auto m : Ref MainMod (Maybe (FC, List1 String))} ->
{auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->
{auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->
DescField -> PkgDesc -> Core PkgDesc
addField (PVersion fc n) pkg = pure $ record { version = n } pkg
addField (PAuthors fc a) pkg = pure $ record { authors = a } pkg
@ -235,10 +234,10 @@ addFields xs desc = do p <- newRef ParsedMods []
, mainmod = !(traverseOpt toSource mmod)
} added
where
toSource : (FC, List1 String) -> Core (List1 String, String)
toSource (loc, ns) = pure (ns, !(nsToSource loc (List1.toList ns)))
go : {auto p : Ref ParsedMods (List (FC, List1 String))} ->
{auto m : Ref MainMod (Maybe (FC, List1 String))} ->
toSource : (FC, ModuleIdent) -> Core (ModuleIdent, String)
toSource (loc, ns) = pure (ns, !(nsToSource loc ns))
go : {auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->
{auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->
List DescField -> PkgDesc -> Core PkgDesc
go [] dsc = pure dsc
go (x :: xs) dsc = go xs !(addField x dsc)
@ -314,7 +313,7 @@ build pkg opts
Just exec =>
do let Just (mainNS, mainFile) = mainmod pkg
| Nothing => throw (GenericMsg emptyFC "No main module given")
let mainName = NS (List1.toList mainNS) (UN "main")
let mainName = NS (miAsNamespace mainNS) (UN "main")
compileMain mainName mainFile exec
runScript (postbuild pkg)
@ -327,14 +326,18 @@ copyFile src dest
writeToFile dest buf
installFrom : {auto c : Ref Ctxt Defs} ->
String -> String -> String -> List1 String -> Core ()
installFrom pname builddir destdir ns@(m :: dns)
= do let ttcfile = joinPath (List1.toList $ reverse ns)
String -> String -> String -> ModuleIdent -> Core ()
installFrom pname builddir destdir ns
= do let ttcfile = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
let destPath = destdir </> joinPath (reverse dns)
let modPath = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns
let destNest = joinPath modPath
let destPath = destdir </> destNest
let destFile = destdir </> ttcfile <.> "ttc"
Right _ <- coreLift $ mkdirAll $ joinPath (reverse dns)
| Left err => throw (InternalError ("Can't make directories " ++ show (reverse dns)))
Right _ <- coreLift $ mkdirAll $ destNest
| Left err => throw (InternalError ("Can't make directories " ++ show modPath))
coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
Right _ <- coreLift $ copyFile ttcPath destFile
| Left err => throw (InternalError ("Can't copy file " ++ ttcPath ++ " to " ++ destPath))
@ -418,12 +421,6 @@ foldWithKeysC {a} {b} fk fv = go []
(StringMap.toList sm))
nd
Semigroup () where
(<+>) _ _ = ()
Monoid () where
neutral = ()
clean : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc ->
@ -437,15 +434,18 @@ clean pkg opts -- `opts` is not used but might be in the future
(\m => fst m :: map fst (modules pkg))
(mainmod pkg)
let toClean : List (List String, String)
= map (\ (x :: xs) => (xs, x)) pkgmods
= mapMaybe (\ mod => case unsafeUnfoldModuleIdent mod of
[] => Nothing
(x :: xs) => Just(xs, x))
pkgmods
Just srcdir <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
let d = dirs (options defs)
let builddir = srcdir </> build_dir d </> "ttc"
let outputdir = srcdir </> outputDirWithDefault d
-- the usual pair syntax breaks with `No such variable a` here for some reason
let pkgTrie = the (StringTrie (List String)) $
foldl (\trie, ksv =>
let pkgTrie : StringTrie (List String)
= foldl (\trie, ksv =>
let ks = Builtin.fst ksv
v = Builtin.snd ksv
in

226
src/Idris/Parser.idr
View File

@ -7,11 +7,15 @@ import Parser.Lexer.Source
import TTImp.TTImp
import public Text.Parser
import Data.Either
import Data.List
import Data.List.Views
import Data.List1
import Data.Maybe
import Data.Strings
import Utils.String
import Idris.Parser.Let
%default covering
@ -48,9 +52,6 @@ plhs = MkParseOpts False False
%hide Prelude.pure
%hide Core.Core.pure
boundToFC : String -> WithBounds t -> FC
boundToFC fname b = MkFC fname (start b) (end b)
atom : FileName -> Rule PTerm
atom fname
= do x <- bounds $ exactIdent "Type"
@ -211,7 +212,7 @@ mutual
pure (x, ty))
(x, ty) <- pure loc.val
(do symbol "**"
rest <- bounds ((nestedDpair fname loc indents <|> expr pdef fname indents) <* symbol ")")
rest <- bounds (nestedDpair fname loc indents <|> expr pdef fname indents)
pure (PDPair (boundToFC fname (mergeBounds start rest))
(PRef (boundToFC fname loc) (UN x))
ty
@ -223,7 +224,7 @@ mutual
= dpairType fname start indents
<|> do l <- expr pdef fname indents
loc <- bounds (symbol "**")
rest <- bounds (nestedDpair fname loc indents <* symbol ")")
rest <- bounds (nestedDpair fname loc indents <|> expr pdef fname indents)
pure (PDPair (boundToFC fname (mergeBounds start rest))
l
(PImplicit (boundToFC fname (mergeBounds start rest)))
@ -249,9 +250,8 @@ mutual
<|> do b <- bounds (continueWith indents ")")
pure (PUnit (boundToFC fname (mergeBounds s b)))
-- dependent pairs with type annotation (so, the type form)
<|> do dpairType fname s indents
<|> do here <- location
e <- bounds (expr pdef fname indents)
<|> do dpairType fname s indents <* symbol ")"
<|> do e <- bounds (expr pdef fname indents)
-- dependent pairs with no type annotation
(do loc <- bounds (symbol "**")
rest <- bounds ((nestedDpair fname loc indents <|> expr pdef fname indents) <* symbol ")")
@ -265,6 +265,11 @@ mutual
<|>
-- all the other bracketed expressions
tuple fname s indents e.val))
<|> do here <- location
let fc = MkFC fname here here
let var = PRef fc (MN "__leftTupleSection" 0)
ts <- bounds (nonEmptyTuple fname s indents var)
pure (PLam fc top Explicit var (PInfer fc) ts.val)
getInitRange : List PTerm -> SourceEmptyRule (PTerm, Maybe PTerm)
getInitRange [x] = pure (x, Nothing)
@ -297,20 +302,44 @@ mutual
<|> (do b <- bounds (symbol "]")
pure (PList (boundToFC fname (mergeBounds s b)) xs))
nonEmptyTuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
nonEmptyTuple fname s indents e
= do rest <- bounds (some (bounds (symbol "," *> optional (bounds (expr pdef fname indents))))
<* continueWith indents ")")
pure $ buildOutput rest (mergePairs 0 rest rest.val)
where
lams : List (FC, PTerm) -> PTerm -> PTerm
lams [] e = e
lams ((fc, var) :: vars) e
= PLam fc top Explicit var (PInfer fc)
$ lams vars e
buildOutput : WithBounds t' -> (List (FC, PTerm), PTerm) -> PTerm
buildOutput rest (vars, scope) = lams vars $ PPair (boundToFC fname (mergeBounds s rest)) e scope
optionalPair : Int -> WithBounds (Maybe (WithBounds PTerm)) -> (Int, (List (FC, PTerm), PTerm))
optionalPair i exp = case exp.val of
Just e => (i, ([], e.val))
Nothing => let fc = boundToFC fname exp in
let var = PRef fc (MN "__infixTupleSection" i) in
(i+1, ([(fc, var)], var))
mergePairs : Int -> WithBounds t' -> List (WithBounds (Maybe (WithBounds PTerm))) ->
(List (FC, PTerm), PTerm)
mergePairs _ end [] = ([], PUnit (boundToFC fname (mergeBounds s end)))
mergePairs i end [exp] = snd (optionalPair i exp)
mergePairs i end (exp :: rest)
= let (j, (var, t)) = optionalPair i exp in
let (vars, ts) = mergePairs j end rest in
(var ++ vars, PPair (boundToFC fname (mergeBounds exp end)) t ts)
-- A pair, dependent pair, or just a single expression
tuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
tuple fname s indents e
= do rest <- bounds (some (symbol "," *> bounds (expr pdef fname indents)) <* continueWith indents ")")
pure (PPair (boundToFC fname (mergeBounds s rest)) e
(mergePairs rest rest.val))
= nonEmptyTuple fname s indents e
<|> do end <- bounds (continueWith indents ")")
pure (PBracketed (boundToFC fname (mergeBounds s end)) e)
where
mergePairs : WithBounds t' -> List (WithBounds PTerm) -> PTerm
mergePairs end [] = PUnit (boundToFC fname (mergeBounds s end))
mergePairs end [exp] = exp.val
mergePairs end (exp :: rest)
= PPair (boundToFC fname (mergeBounds exp end)) exp.val (mergePairs end rest)
postfixApp : FileName -> IndentInfo -> Rule PTerm
postfixApp fname indents
@ -364,7 +393,7 @@ mutual
<|> do b <- bounds (pragma "runElab" *> expr pdef fname indents)
pure (PRunElab (boundToFC fname b) b.val)
<|> do b <- bounds $ do pragma "logging"
topic <- optional ((::) <$> unqualifiedName <*> many aDotIdent)
topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
lvl <- intLit
e <- expr pdef fname indents
pure (MkPair (mkLogLevel' topic (integerToNat lvl)) e)
@ -506,63 +535,31 @@ mutual
= PLam (boundToFC fname pat) rig Explicit pat.val ty
(bindAll rest scope)
letBinder : FileName -> IndentInfo ->
Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
letBinder fname indents
= do b <- bounds (do s <- bounds (MkPair <$> multiplicity <*> expr plhs fname indents)
(rigc, pat) <- pure s.val
ty <- option (PImplicit (boundToFC fname s))
(do symbol ":"
typeExpr (pnoeq pdef) fname indents)
symbol "="
val <- expr pnowith fname indents
alts <- block (patAlt fname)
rig <- getMult rigc
pure (rig, pat, ty, val, alts))
(rig, pat, ty, val, alts) <- the (SourceEmptyRule (RigCount, PTerm, PTerm, PTerm, List PClause)) (pure b.val)
pure (start b, end b, rig, pat, ty, val, alts)
letBlock : FileName -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
letBlock fname indents = bounds (letBinder <||> letDecl) where
buildLets : FileName ->
List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) ->
PTerm -> PTerm
buildLets fname [] sc = sc
buildLets fname ((start, end, rig, pat, ty, val, alts) :: rest) sc
= let fc = MkFC fname start end in
PLet fc rig pat ty val
(buildLets fname rest sc) alts
letBinder : Rule LetBinder
letBinder = do s <- bounds (MkPair <$> multiplicity <*> expr plhs fname indents)
(rigc, pat) <- pure s.val
ty <- option (PImplicit (boundToFC fname s))
(symbol ":" *> typeExpr (pnoeq pdef) fname indents)
(symbol "=" <|> symbol ":=")
val <- expr pnowith fname indents
alts <- block (patAlt fname)
rig <- getMult rigc
pure (MkLetBinder rig pat ty val alts)
buildDoLets : FileName ->
List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) ->
List PDo
buildDoLets fname [] = []
buildDoLets fname ((start, end, rig, PRef fc' (UN n), ty, val, []) :: rest)
= let fc = MkFC fname start end in
if lowerFirst n
then DoLet fc (UN n) rig ty val :: buildDoLets fname rest
else DoLetPat fc (PRef fc' (UN n)) ty val []
:: buildDoLets fname rest
buildDoLets fname ((start, end, rig, pat, ty, val, alts) :: rest)
= let fc = MkFC fname start end in
DoLetPat fc pat ty val alts :: buildDoLets fname rest
letDecl : Rule LetDecl
letDecl = collectDefs . concat <$> nonEmptyBlock (try . topDecl fname)
let_ : FileName -> IndentInfo -> Rule PTerm
let_ fname indents
= do b <- bounds (do keyword "let"
res <- nonEmptyBlock (letBinder fname)
commitKeyword indents "in"
scope <- typeExpr pdef fname indents
pure (res, scope))
(res, scope) <- pure b.val
pure (buildLets fname res scope)
<|> do b <- bounds (do keyword "let"
commit
ds <- nonEmptyBlock (topDecl fname)
commitKeyword indents "in"
scope <- typeExpr pdef fname indents
pure (ds, scope))
(ds, scope) <- pure b.val
pure (PLocal (boundToFC fname b) (collectDefs (concat ds)) scope)
= do keyword "let"
commit
res <- nonEmptyBlock (letBlock fname)
commitKeyword indents "in"
scope <- typeExpr pdef fname indents
pure (mkLets fname res scope)
case_ : FileName -> IndentInfo -> Rule PTerm
case_ fname indents
@ -673,19 +670,17 @@ mutual
doBlock fname indents
= do b <- bounds (do keyword "do"
block (doAct fname))
commit
pure (PDoBlock (boundToFC fname b) Nothing (concat b.val))
<|> do nsdo <- bounds namespacedIdent
the (SourceEmptyRule PTerm) $ case nsdo.val of
("do" :: ns) =>
do actions <- bounds (block (doAct fname))
(ns, "do") =>
do commit
actions <- bounds (block (doAct fname))
pure (PDoBlock (boundToFC fname (mergeBounds nsdo actions))
(Just ns) (concat actions.val))
ns (concat actions.val))
_ => fail "Not a namespaced 'do'"
lowerFirst : String -> Bool
lowerFirst "" = False
lowerFirst str = assert_total (isLower (prim__strHead str))
validPatternVar : Name -> SourceEmptyRule ()
validPatternVar (UN n)
= if lowerFirst n then pure ()
@ -705,12 +700,10 @@ mutual
(n, val) <- pure b.val
pure [DoBind (boundToFC fname b) n val]
<|> do keyword "let"
res <- block (letBinder fname)
commit
res <- nonEmptyBlock (letBlock fname)
atEnd indents
pure (buildDoLets fname res)
<|> do b <- bounds (keyword "let" *> block (topDecl fname))
atEnd indents
pure [DoLetLocal (boundToFC fname b) (concat b.val)]
pure (mkDoLets fname res)
<|> do b <- bounds (keyword "rewrite" *> expr pdef fname indents)
atEnd indents
pure [DoRewrite (boundToFC fname b) b.val]
@ -818,17 +811,13 @@ mutual
symbol "("
wval <- bracketedExpr fname flags indents
ws <- nonEmptyBlock (clause (S withArgs) fname)
pure (flags, wval, ws))
pure (flags, wval, forget ws))
(flags, wval, ws) <- pure b.val
pure (MkWithClause (boundToFC fname (mergeBounds start b)) lhs wval flags.val ws)
<|> do end <- bounds (keyword "impossible")
atEnd indents
pure (MkImpossible (boundToFC fname (mergeBounds start end)) lhs)
ifThenElse : Bool -> Lazy t -> Lazy t -> t
ifThenElse True t e = t
ifThenElse False t e = e
clause : Nat -> FileName -> IndentInfo -> Rule PClause
clause withArgs fname indents
= do b <- bounds (do col <- column
@ -981,7 +970,7 @@ directive fname indents
-- atEnd indents
-- pure (Hide True n)
<|> do pragma "logging"
topic <- optional ((::) <$> unqualifiedName <*> many aDotIdent)
topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
lvl <- intLit
atEnd indents
pure (Logging (mkLogLevel' topic (fromInteger lvl)))
@ -1053,8 +1042,8 @@ fix
<|> (keyword "infix" *> pure Infix)
<|> (keyword "prefix" *> pure Prefix)
namespaceHead : Rule (List1 String)
namespaceHead = keyword "namespace" *> commit *> namespacedIdent
namespaceHead : Rule Namespace
namespaceHead = keyword "namespace" *> commit *> namespaceId
namespaceDecl : FileName -> IndentInfo -> Rule PDecl
namespaceDecl fname indents
@ -1064,7 +1053,7 @@ namespaceDecl fname indents
ds <- blockAfter col (topDecl fname)
pure (doc, ns, ds))
(doc, ns, ds) <- pure b.val
pure (PNamespace (boundToFC fname b) (List1.toList ns) (concat ds))
pure (PNamespace (boundToFC fname b) ns (concat ds))
transformDecl : FileName -> IndentInfo -> Rule PDecl
transformDecl fname indents
@ -1168,10 +1157,6 @@ getVisibility (Just vis) (Left x :: xs)
= fatalError "Multiple visibility modifiers"
getVisibility v (_ :: xs) = getVisibility v xs
getRight : Either a b -> Maybe b
getRight (Left _) = Nothing
getRight (Right v) = Just v
constraints : FileName -> IndentInfo -> SourceEmptyRule (List (Maybe Name, PTerm))
constraints fname indents
= do tm <- appExpr pdef fname indents
@ -1202,16 +1187,16 @@ implBinds fname indents
pure ((n, rig, tm) :: more)
<|> pure []
ifaceParam : FileName -> IndentInfo -> Rule (Name, PTerm)
ifaceParam : FileName -> IndentInfo -> Rule (List Name, PTerm)
ifaceParam fname indents
= do symbol "("
n <- name
ns <- sepBy1 (symbol ",") name
symbol ":"
tm <- expr pdef fname indents
symbol ")"
pure (n, tm)
pure (ns, tm)
<|> do n <- bounds name
pure (n.val, PInfer (boundToFC fname n))
pure ([n.val], PInfer (boundToFC fname n))
ifaceDecl : FileName -> IndentInfo -> Rule PDecl
ifaceDecl fname indents
@ -1222,7 +1207,8 @@ ifaceDecl fname indents
commit
cons <- constraints fname indents
n <- name
params <- many (ifaceParam fname indents)
paramss <- many (ifaceParam fname indents)
let params = concatMap (\ (ns, t) => map (\ n => (n, t)) ns) paramss
det <- option []
(do symbol "|"
sepBy (symbol ",") name)
@ -1417,16 +1403,9 @@ topDecl fname indents
-- collectDefs : List PDecl -> List PDecl
collectDefs [] = []
collectDefs (PDef annot cs :: ds)
= let (cs', rest) = spanMap isClause ds in
PDef annot (cs ++ cs') :: assert_total (collectDefs rest)
= let (cs', rest) = spanBy isClause ds in
PDef annot (cs ++ concat cs') :: assert_total (collectDefs rest)
where
spanMap : (a -> Maybe (List b)) -> List a -> (List b, List a)
spanMap f [] = ([], [])
spanMap f (x :: xs) = case f x of
Nothing => ([], x :: xs)
Just y => case spanMap f xs of
(ys, zs) => (y ++ ys, zs)
isClause : PDecl -> Maybe (List PClause)
isClause (PDef annot cs)
= Just cs
@ -1444,40 +1423,41 @@ import_ fname indents
= do b <- bounds (do keyword "import"
reexp <- option False (do keyword "public"
pure True)
ns <- namespacedIdent
nsAs <- option ns (do exactIdent "as"
namespacedIdent)
ns <- moduleIdent
nsAs <- option (miAsNamespace ns)
(do exactIdent "as"
namespaceId)
pure (reexp, ns, nsAs))
atEnd indents
(reexp, ns, nsAs) <- pure b.val
pure (MkImport (boundToFC fname b) reexp (List1.toList ns) (List1.toList nsAs))
pure (MkImport (boundToFC fname b) reexp ns nsAs)
export
prog : FileName -> SourceEmptyRule Module
prog fname
= do b <- bounds (do doc <- option "" documentation
nspace <- option ["Main"]
nspace <- option (nsAsModuleIdent mainNS)
(do keyword "module"
namespacedIdent)
moduleIdent)
imports <- block (import_ fname)
pure (doc, nspace, imports))
ds <- block (topDecl fname)
(doc, nspace, imports) <- pure b.val
pure (MkModule (boundToFC fname b)
(List1.toList nspace) imports doc (collectDefs (concat ds)))
nspace imports doc (collectDefs (concat ds)))
export
progHdr : FileName -> SourceEmptyRule Module
progHdr fname
= do b <- bounds (do doc <- option "" documentation
nspace <- option ["Main"]
nspace <- option (nsAsModuleIdent mainNS)
(do keyword "module"
namespacedIdent)
moduleIdent)
imports <- block (import_ fname)
pure (doc, nspace, imports))
(doc, nspace, imports) <- pure b.val
pure (MkModule (boundToFC fname b)
(List1.toList nspace) imports doc [])
nspace imports doc [])
parseMode : Rule REPLEval
parseMode
@ -1687,7 +1667,7 @@ stringArgCmd parseCmd command doc = (names, StringArg, doc, parse)
s <- strLit
pure (command s)
moduleArgCmd : ParseCmd -> (List String -> REPLCmd) -> String -> CommandDefinition
moduleArgCmd : ParseCmd -> (ModuleIdent -> REPLCmd) -> String -> CommandDefinition
moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse)
where
names : List String
@ -1698,7 +1678,7 @@ moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse)
symbol ":"
runParseCmd parseCmd
n <- moduleIdent
pure (command (List1.toList n))
pure (command n)
exprArgCmd : ParseCmd -> (PTerm -> REPLCmd) -> String -> CommandDefinition
exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
@ -1801,7 +1781,7 @@ loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, p
parse = do
symbol ":"
runParseCmd parseCmd
topic <- optional ((::) <$> unqualifiedName <*> many aDotIdent)
topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
lvl <- intLit
pure (command (mkLogLevel' topic (fromInteger lvl)))
@ -1824,7 +1804,7 @@ parserCommandsForHelp =
, nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"
, nameArgCmd (ParseKeywordCmd "total") Total "Check the totality of a name"
, nameArgCmd (ParseIdentCmd "doc") Doc "Show documentation for a name"
, moduleArgCmd (ParseIdentCmd "browse") Browse "Browse contents of a namespace"
, moduleArgCmd (ParseIdentCmd "browse") (Browse . miAsNamespace) "Browse contents of a namespace"
, loggingArgCmd (ParseREPLCmd ["log", "logging"]) SetLog "Set logging level"
, autoNumberArgCmd (ParseREPLCmd ["consolewidth"]) SetConsoleWidth "Set the width of the console output (0 for unbounded) (auto by default)"
, onOffArgCmd (ParseREPLCmd ["color", "colour"]) SetColor "Whether to use color for the console output (enabled by default)"

90
src/Idris/Parser/Let.idr Normal file
View File

@ -0,0 +1,90 @@
module Idris.Parser.Let
import Idris.Syntax
import Text.Bounded
import Data.Either
import Data.List1
import Utils.String
%default total
------------------------------------------------------------------------
-- Types
-- `let ... in ...` is used for two different notions:
-- * pattern-matching let binders to locally take an expression apart
-- * Local definitions that can be recursive
public export
record LetBinder where
constructor MkLetBinder
letUsage : RigCount
letPattern : PTerm
letBoundType : PTerm
letBoundTerm : PTerm
letUnhappy : List PClause
public export
LetDecl : Type
LetDecl = List PDecl
------------------------------------------------------------------------
-- Let-binding functions
letFactory : (List (WithBounds LetBinder) -> a -> a) ->
(WithBounds LetDecl -> a -> a) ->
List1 (WithBounds (Either LetBinder LetDecl)) ->
a -> a
letFactory letBind letDeclare blocks scope = foldr mkLet scope groups where
LetBlock : Type
LetBlock = Either (List1 (WithBounds LetBinder)) (List1 (WithBounds LetDecl))
groups : List LetBlock
groups = compress (forget $ map (\ b => bimap (<$ b) (<$ b) b.val) blocks)
mkLet : LetBlock -> a -> a
mkLet (Left letBinds) = letBind (forget letBinds)
mkLet (Right letDecls) =
let bounds = mergeBounds (head letDecls) (last letDecls)
in letDeclare (concatMap val letDecls <$ bounds)
export
mkLets : FileName ->
List1 (WithBounds (Either LetBinder LetDecl)) ->
PTerm -> PTerm
mkLets fname = letFactory buildLets
(\ decls, scope => PLocal (boundToFC fname decls) decls.val scope)
where
buildLets : List (WithBounds LetBinder) -> PTerm -> PTerm
buildLets [] sc = sc
buildLets (b :: rest) sc
= let (MkLetBinder rig pat ty val alts) = b.val
fc = boundToFC fname b
in PLet fc rig pat ty val (buildLets rest sc) alts
export
mkDoLets : FileName ->
List1 (WithBounds (Either LetBinder LetDecl)) ->
List PDo
mkDoLets fname lets = letFactory
(\ binds, rest => buildDoLets binds ++ rest)
(\ decls, rest => DoLetLocal (boundToFC fname decls) decls.val :: rest)
lets
[]
where
buildDoLets : List (WithBounds LetBinder) -> List PDo
buildDoLets [] = []
buildDoLets (b :: rest) = let fc = boundToFC fname b in case b.val of
(MkLetBinder rig (PRef fc' (UN n)) ty val []) =>
(if lowerFirst n
then DoLet fc (UN n) rig ty val
else DoLetPat fc (PRef fc' (UN n)) ty val []
) :: buildDoLets rest
(MkLetBinder rig pat ty val alts) => DoLetPat fc pat ty val alts :: buildDoLets rest

35
src/Idris/ProcessIdr.idr
View File

@ -4,6 +4,7 @@ import Compiler.Inline
import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Env
import Core.Hash
@ -63,23 +64,23 @@ readModule : {auto c : Ref Ctxt Defs} ->
(full : Bool) -> -- load everything transitively (needed for REPL and compiling)
FC ->
(visible : Bool) -> -- Is import visible to top level module?
(imp : List String) -> -- Module name to import
(as : List String) -> -- Namespace to import into
(imp : ModuleIdent) -> -- Module name to import
(as : Namespace) -> -- Namespace to import into
Core ()
readModule full loc vis imp as
= do defs <- get Ctxt
let False = (imp, vis, as) `elem` map snd (allImported defs)
| True => when vis (setVisible imp)
| True => when vis (setVisible (miAsNamespace imp))
Right fname <- nsToPath loc imp
| Left err => throw err
Just (syn, hash, more) <- readFromTTC False {extra = SyntaxInfo}
loc vis fname imp as
| Nothing => when vis (setVisible imp) -- already loaded, just set visibility
| Nothing => when vis (setVisible (miAsNamespace imp)) -- already loaded, just set visibility
extendSyn syn
defs <- get Ctxt
modNS <- getNS
when vis $ setVisible imp
when vis $ setVisible (miAsNamespace imp)
traverse_ (\ mimp =>
do let m = fst mimp
let reexp = fst (snd mimp)
@ -108,7 +109,7 @@ addImport imp
readHash : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Import -> Core (Bool, (List String, Int))
Import -> Core (Bool, (Namespace, Int))
readHash imp
= do Right fname <- nsToPath (loc imp) (path imp)
| Left err => throw err
@ -117,7 +118,7 @@ readHash imp
prelude : Import
prelude = MkImport (MkFC "(implicit)" (0, 0) (0, 0)) False
["Prelude"] ["Prelude"]
(nsAsModuleIdent preludeNS) preludeNS
export
readPrelude : {auto c : Ref Ctxt Defs} ->
@ -126,7 +127,7 @@ readPrelude : {auto c : Ref Ctxt Defs} ->
Bool -> Core ()
readPrelude full
= do readImport full prelude
setNS ["Main"]
setNS mainNS
-- Import a TTC for use as the main file (e.g. at the REPL)
export
@ -136,7 +137,7 @@ readAsMain : {auto c : Ref Ctxt Defs} ->
(fname : String) -> Core ()
readAsMain fname
= do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo}
True toplevelFC True fname [] []
True toplevelFC True fname (nsAsModuleIdent emptyNS) emptyNS
| Nothing => throw (InternalError "Already loaded")
replNS <- getNS
replNestedNS <- getNestedNS
@ -154,7 +155,7 @@ readAsMain fname
-- also load the prelude, if required, so that we have access to it
-- at the REPL.
when (not (noprelude !getSession)) $
readModule True emptyFC True ["Prelude"] ["Prelude"]
readModule True emptyFC True (nsAsModuleIdent preludeNS) preludeNS
-- We're in the namespace from the first TTC, so use the next name
-- from that for the fresh metavariable name generation
@ -168,7 +169,7 @@ readAsMain fname
addPrelude : List Import -> List Import
addPrelude imps
= if not (["Prelude"] `elem` map path imps)
= if not (nsAsModuleIdent preludeNS `elem` map path imps)
then prelude :: imps
else imps
@ -218,7 +219,7 @@ gc = primIO $ prim__gc 4
export
addPublicHash : {auto c : Ref Ctxt Defs} ->
(Bool, (List String, Int)) -> Core ()
(Bool, (Namespace, Int)) -> Core ()
addPublicHash (True, (mod, h)) = do addHash mod; addHash h
addPublicHash _ = pure ()
@ -241,7 +242,7 @@ processMod srcf ttcf msg sourcecode
modh <- readHeader srcf
-- Add an implicit prelude import
let imps =
if (noprelude !getSession || moduleNS modh == ["Prelude"])
if (noprelude !getSession || moduleNS modh == nsAsModuleIdent preludeNS)
then imports modh
else addPrelude (imports modh)
@ -264,7 +265,7 @@ processMod srcf ttcf msg sourcecode
if (sort (map snd hs) == sort imphs && srctime <= ttctime)
then -- Hashes the same, source up to date, just set the namespace
-- for the REPL
do setNS ns
do setNS (miAsNamespace ns)
pure Nothing
else -- needs rebuilding
do iputStrLn msg
@ -274,13 +275,13 @@ processMod srcf ttcf msg sourcecode
initHash
traverse addPublicHash (sort hs)
resetNextVar
when (ns /= ["Main"]) $
when (ns /= nsAsModuleIdent mainNS) $
do let MkFC fname _ _ = headerloc mod
d <- getDirs
ns' <- pathToNS (working_dir d) (source_dir d) fname
when (ns /= ns') $
throw (GenericMsg (headerloc mod)
("Module name " ++ showSep "." (reverse ns) ++
("Module name " ++ show ns ++
" does not match file name " ++ fname))
-- read import ttcs in full here
@ -295,7 +296,7 @@ processMod srcf ttcf msg sourcecode
-- names are set to private (TODO, maybe if we want this?)
-- defs <- get Ctxt
-- traverse (\x => setVisibility emptyFC x Private) (hiddenNames defs)
setNS ns
setNS (miAsNamespace ns)
errs <- logTime "++ Processing decls" $
processDecls (decls mod)
-- coreLift $ gc

13
src/Idris/REPL.idr
View File

@ -11,6 +11,7 @@ import Core.AutoSearch
import Core.CaseTree
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Env
import Core.InitPrimitives
import Core.LinearCheck
@ -628,8 +629,8 @@ process (Eval itm)
-- foreign argument lists. TODO: once the new FFI is fully
-- up and running we won't need this. Also, if we add
-- 'with' disambiguation we can use that instead.
catch (do hide replFC (NS ["PrimIO"] (UN "::"))
hide replFC (NS ["PrimIO"] (UN "Nil")))
catch (do hide replFC (NS primIONS (UN "::"))
hide replFC (NS primIONS (UN "Nil")))
(\err => pure ())
(tm, gty) <- elabTerm inidx (emode (evalMode opts)) [] (MkNested [])
[] ttimp Nothing
@ -687,9 +688,9 @@ process (Load f)
-- Clear the context and load again
loadMainFile f
process (ImportMod m)
= do catch (do addImport (MkImport emptyFC False m m)
pure $ ModuleLoaded (showSep "." (reverse m)))
(\err => pure $ ErrorLoadingModule (showSep "." (reverse m)) err)
= do catch (do addImport (MkImport emptyFC False m (miAsNamespace m))
pure $ ModuleLoaded (show m))
(\err => pure $ ErrorLoadingModule (show m) err)
process (CD dir)
= do setWorkingDir dir
workDir <- getWorkingDir
@ -889,7 +890,7 @@ mutual
repl
= do ns <- getNS
opts <- get ROpts
coreLift (putStr (prompt (evalMode opts) ++ showSep "." (reverse ns) ++ "> "))
coreLift (putStr (prompt (evalMode opts) ++ show ns ++ "> "))
inp <- coreLift getLine
end <- coreLift $ fEOF stdin
if end

41
src/Idris/Resugar.idr
View File

@ -96,14 +96,14 @@ unbracket tm = tm
||| Attempt to extract a constant natural number
extractNat : Nat -> PTerm -> Maybe Nat
extractNat acc tm = case tm of
PRef _ (NS ["Types", "Prelude"] (UN "Z"))
=> pure acc
PApp _ (PRef _ (NS ["Types", "Prelude"] (UN "S"))) k
=> extractNat (1 + acc) k
PRef _ (NS ["Prelude"] (UN "Z"))
=> pure acc
PApp _ (PRef _ (NS ["Prelude"] (UN "S"))) k
=> extractNat (1 + acc) k
PRef _ (NS ns (UN n)) =>
do guard (n == "Z")
guard (ns == typesNS || ns == preludeNS)
pure acc
PApp _ (PRef _ (NS ns (UN n))) k => do
do guard (n == "S")
guard (ns == typesNS || ns == preludeNS)
extractNat (1 + acc) k
PPrimVal _ (BI n) => pure (acc + integerToNat n)
PBracketed _ k => extractNat acc k
_ => Nothing
@ -127,22 +127,17 @@ mutual
PList fc xs => pure $ PList fc (unbracketApp l :: xs)
_ => Nothing
_ => Nothing
sugarAppM tm =
-- refolding natural numbers if the expression is a constant
-- we might see either Prelude.Types.Nat or Prelude.Nat, depending on whether
-- unelaboration used the canonical name or not
sugarAppM (PRef fc (NS ["Types", "Prelude"] (UN "Z"))) = pure $ PPrimVal fc (BI 0)
sugarAppM (PApp fc (PRef _ (NS ["Types", "Prelude"] (UN "S"))) k) =
PPrimVal fc . BI . cast <$> extractNat 1 k
sugarAppM (PRef fc (NS ["Prelude"] (UN "Z"))) = pure $ PPrimVal fc (BI 0)
sugarAppM (PApp fc (PRef _ (NS ["Prelude"] (UN "S"))) k) =
PPrimVal fc . BI . cast <$> extractNat 1 k
-- NB: this needs to come after the case for Z, otherwise it will shadow it.
sugarAppM (PRef fc nm) = case nameRoot nm of
"Nil" => pure $ PList fc []
"Unit" => pure $ PUnit fc
"MkUnit" => pure $ PUnit fc
_ => Nothing
sugarAppM tm = Nothing
case extractNat 0 tm of
Just k => pure $ PPrimVal (getPTermLoc tm) (BI (cast k))
Nothing => case tm of
PRef fc nm => case nameRoot nm of
"Nil" => pure $ PList fc []
"Unit" => pure $ PUnit fc
"MkUnit" => pure $ PUnit fc
_ => Nothing
_ => Nothing
||| Put the special names (Nil, ::, Pair, Z, S, etc.) back as syntax

8
src/Idris/SetOptions.idr
View File

@ -8,6 +8,7 @@ import Core.Unify
import Utils.Path
import Idris.CommandLine
import Idris.Error
import Idris.REPL
import Idris.Syntax
import Idris.Version
@ -147,9 +148,10 @@ postOptions res (OutputFile outfile :: rest)
postOptions res rest
pure False
postOptions res (ExecFn str :: rest)
= do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
postOptions res rest
pure False
= catch (do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
postOptions res rest
pure False)
(\err => do perror err >>= printError; pure False)
postOptions res (CheckOnly :: rest)
= do postOptions res rest
pure False

34
src/Idris/Syntax.idr
View File

@ -81,7 +81,7 @@ mutual
-- Syntactic sugar
PDoBlock : FC -> Maybe (List String) -> List PDo -> PTerm
PDoBlock : FC -> Maybe Namespace -> List PDo -> PTerm
PBang : FC -> PTerm -> PTerm
PIdiom : FC -> PTerm -> PTerm
PList : FC -> List PTerm -> PTerm
@ -313,7 +313,7 @@ mutual
-- TODO: POpen (for opening named interfaces)
PMutual : FC -> List PDecl -> PDecl
PFixity : FC -> Fixity -> Nat -> OpStr -> PDecl
PNamespace : FC -> List String -> List PDecl -> PDecl
PNamespace : FC -> Namespace -> List PDecl -> PDecl
PTransform : FC -> String -> PTerm -> PTerm -> PDecl
PRunElabDecl : FC -> PTerm -> PDecl
PDirective : FC -> Directive -> PDecl
@ -419,7 +419,7 @@ data REPLCmd : Type where
PrintDef : Name -> REPLCmd
Reload : REPLCmd
Load : String -> REPLCmd
ImportMod : List String -> REPLCmd
ImportMod : ModuleIdent -> REPLCmd
Edit : REPLCmd
Compile : PTerm -> String -> REPLCmd
Exec : PTerm -> REPLCmd
@ -434,7 +434,7 @@ data REPLCmd : Type where
Missing : Name -> REPLCmd
Total : Name -> REPLCmd
Doc : Name -> REPLCmd
Browse : List String -> REPLCmd
Browse : Namespace -> REPLCmd
SetLog : LogLevel -> REPLCmd
SetConsoleWidth : Maybe Nat -> REPLCmd
SetColor : Bool -> REPLCmd
@ -449,24 +449,18 @@ record Import where
constructor MkImport
loc : FC
reexport : Bool
path : List String
nameAs : List String
path : ModuleIdent
nameAs : Namespace
public export
record Module where
constructor MkModule
headerloc : FC
moduleNS : List String
moduleNS : ModuleIdent
imports : List Import
documentation : String
decls : List PDecl
showCount : RigCount -> String
showCount = elimSemi
("0 ")
("1 ")
(const "")
mutual
showAlt : PClause -> String
showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";"
@ -497,11 +491,11 @@ mutual
showPrec d (PPi _ rig Explicit Nothing arg ret)
= showPrec d arg ++ " -> " ++ showPrec d ret
showPrec d (PPi _ rig Explicit (Just n) arg ret)
= "(" ++ Syntax.showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ ") -> " ++ showPrec d ret
= "(" ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ ") -> " ++ showPrec d ret
showPrec d (PPi _ rig Implicit Nothing arg ret) -- shouldn't happen
= "{" ++ Syntax.showCount rig ++ "_ : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret
= "{" ++ showCount rig ++ "_ : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret
showPrec d (PPi _ rig Implicit (Just n) arg ret)
= "{" ++ Syntax.showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret
= "{" ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret
showPrec d (PPi _ top AutoImplicit Nothing arg ret)
= showPrec d arg ++ " => " ++ showPrec d ret
showPrec d (PPi _ rig AutoImplicit (Just n) arg ret)
@ -511,13 +505,13 @@ mutual
showPrec d (PPi _ rig (DefImplicit t) (Just n) arg ret)
= "{default " ++ showPrec App t ++ " " ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret
showPrec d (PLam _ rig _ n (PImplicit _) sc)
= "\\" ++ Syntax.showCount rig ++ showPrec d n ++ " => " ++ showPrec d sc
= "\\" ++ showCount rig ++ showPrec d n ++ " => " ++ showPrec d sc
showPrec d (PLam _ rig _ n ty sc)
= "\\" ++ Syntax.showCount rig ++ showPrec d n ++ " : " ++ showPrec d ty ++ " => " ++ showPrec d sc
= "\\" ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d ty ++ " => " ++ showPrec d sc
showPrec d (PLet _ rig n (PImplicit _) val sc alts)
= "let " ++ Syntax.showCount rig ++ showPrec d n ++ " = " ++ showPrec d val ++ " in " ++ showPrec d sc
= "let " ++ showCount rig ++ showPrec d n ++ " = " ++ showPrec d val ++ " in " ++ showPrec d sc
showPrec d (PLet _ rig n ty val sc alts)
= "let " ++ Syntax.showCount rig ++ showPrec d n ++ " : " ++ showPrec d ty ++ " = "
= "let " ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d ty ++ " = "
++ showPrec d val ++ concatMap showAlt alts ++
" in " ++ showPrec d sc
where

15
src/Parser/Lexer/Package.idr
View File

@ -12,6 +12,8 @@ import Data.Strings
import Data.String.Extra
import Utils.String
import Core.Name.Namespace
%default total
public export
@ -19,7 +21,7 @@ data Token
= Comment String
| EndOfInput
| Equals
| DotSepIdent (List1 String)
| DotSepIdent (Maybe Namespace) String
| Separator
| Space
| StringLit String
@ -29,7 +31,7 @@ Show Token where
show (Comment str) = "Comment: " ++ str
show EndOfInput = "EndOfInput"
show Equals = "Equals"
show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (List1.toList dsid)
show (DotSepIdent ns n) = "DotSepIdentifier: " ++ show ns ++ "." ++ show n
show Separator = "Separator"
show Space = "Space"
show (StringLit s) = "StringLit: " ++ s
@ -39,7 +41,7 @@ Pretty Token where
pretty (Comment str) = "Comment:" <++> pretty str
pretty EndOfInput = "EndOfInput"
pretty Equals = "Equals"
pretty (DotSepIdent dsid) = "DotSepIdentifier:" <++> concatWith (surround dot) (pretty <$> List1.toList dsid)
pretty (DotSepIdent ns n) = "DotSepIdentifier:" <++> pretty ns <+> dot <+> pretty n
pretty Separator = "Separator"
pretty Space = "Space"
pretty (StringLit s) = "StringLit:" <++> pretty s
@ -54,15 +56,12 @@ rawTokens : TokenMap Token
rawTokens =
[ (equals, const Equals)
, (comment, Comment . drop 2)
, (namespacedIdent, DotSepIdent . splitNamespace)
, (identAllowDashes, DotSepIdent . pure)
, (namespacedIdent, uncurry DotSepIdent . mkNamespacedIdent)
, (identAllowDashes, DotSepIdent Nothing)
, (separator, const Separator)
, (spacesOrNewlines, const Space)
, (stringLit, \s => StringLit (stripQuotes s))
]
where
splitNamespace : String -> List1 String
splitNamespace = Data.Strings.split (== '.')
export
lex : String -> Either (Int, Int, String) (List (WithBounds Token))

20
src/Parser/Lexer/Source.idr
View File

@ -14,6 +14,8 @@ import Utils.Hex
import Utils.Octal
import Utils.String
import Core.Name
%default total
public export
@ -26,8 +28,8 @@ data Token
-- Identifiers
| HoleIdent String
| Ident String
| DotSepIdent (List1 String) -- ident.ident
| DotIdent String -- .ident
| DotSepIdent Namespace String -- ident.ident
| DotIdent String -- .ident
| Symbol String
-- Comments
| Comment String
@ -49,7 +51,7 @@ Show Token where
-- Identifiers
show (HoleIdent x) = "hole identifier " ++ x
show (Ident x) = "identifier " ++ x
show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (List1.toList $ reverse xs)
show (DotSepIdent ns n) = "namespaced identifier " ++ show ns ++ "." ++ show n
show (DotIdent x) = "dot+identifier " ++ x
show (Symbol x) = "symbol " ++ x
-- Comments
@ -72,7 +74,7 @@ Pretty Token where
-- Identifiers
pretty (HoleIdent x) = reflow "hole identifier" <++> pretty x
pretty (Ident x) = pretty "identifier" <++> pretty x
pretty (DotSepIdent xs) = reflow "namespaced identifier" <++> concatWith (surround dot) (pretty <$> reverse (List1.toList xs))
pretty (DotSepIdent ns n) = reflow "namespaced identifier" <++> pretty ns <+> dot <+> pretty n
pretty (DotIdent x) = pretty "dot+identifier" <++> pretty x
pretty (Symbol x) = pretty "symbol" <++> pretty x
-- Comments
@ -123,7 +125,7 @@ mutual
||| comment unless the series of uninterrupted dashes is ended with
||| a closing brace in which case it is a closing delimiter.
doubleDash : (k : Nat) -> Lexer
doubleDash k = many (is '-') <+> choice {t = List} -- absorb all dashes
doubleDash k = many (is '-') <+> choice -- absorb all dashes
[ is '}' <+> toEndComment k -- closing delimiter
, many (isNot '\n') <+> toEndComment (S k) -- line comment
]
@ -200,7 +202,7 @@ export
reservedSymbols : List String
reservedSymbols
= symbols ++
["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!",
["%", "\\", ":", "=", ":=", "|", "|||", "<-", "->", "=>", "?", "!",
"&", "**", "..", "~"]
fromBinLit : String -> Integer
@ -262,9 +264,9 @@ rawTokens =
parseIdent x = if x `elem` keywords then Keyword x
else Ident x
parseNamespace : String -> Token
parseNamespace ns = case List1.reverse . split (== '.') $ ns of
[ident] => parseIdent ident
ns => DotSepIdent ns
parseNamespace ns = case mkNamespacedIdent ns of
(Nothing, ident) => parseIdent ident
(Just ns, n) => DotSepIdent ns n
export
lexTo : (WithBounds Token -> Bool) ->

15
src/Parser/Rule/Package.idr
View File

@ -4,7 +4,8 @@ import public Parser.Lexer.Package
import public Parser.Rule.Common
import Data.List
import Data.List1
import Core.Name.Namespace
%default total
@ -34,7 +35,7 @@ export
exactProperty : String -> Rule String
exactProperty p = terminal ("Expected property " ++ p)
(\x => case x.val of
DotSepIdent [p'] =>
DotSepIdent Nothing p' =>
if p == p' then Just p
else Nothing
_ => Nothing)
@ -47,24 +48,24 @@ stringLit = terminal "Expected string"
_ => Nothing)
export
namespacedIdent : Rule (List1 String)
namespacedIdent : Rule (Maybe Namespace, String)
namespacedIdent = terminal "Expected namespaced identifier"
(\x => case x.val of
DotSepIdent nsid => Just $ reverse nsid
DotSepIdent ns n => Just (ns, n)
_ => Nothing)
export
moduleIdent : Rule (List1 String)
moduleIdent : Rule ModuleIdent
moduleIdent = terminal "Expected module identifier"
(\x => case x.val of
DotSepIdent m => Just $ reverse m
DotSepIdent ns m => Just $ nsAsModuleIdent (mkNestedNamespace ns m)
_ => Nothing)
export
packageName : Rule String
packageName = terminal "Expected package name"
(\x => case x.val of
DotSepIdent [str] =>
DotSepIdent Nothing str =>
if isIdent AllowDashes str then Just str
else Nothing
_ => Nothing)

45
src/Parser/Rule/Source.idr
View File

@ -156,21 +156,25 @@ identPart
_ => Nothing)
export
namespacedIdent : Rule (List1 String)
namespacedIdent : Rule (Maybe Namespace, String)
namespacedIdent
= terminal "Expected namespaced name"
(\x => case x.val of
DotSepIdent ns => Just ns
Ident i => Just [i]
DotSepIdent ns n => Just (Just ns, n)
Ident i => Just (Nothing, i)
_ => Nothing)
export
moduleIdent : Rule (List1 String)
namespaceId : Rule Namespace
namespaceId = map (uncurry mkNestedNamespace) namespacedIdent
export
moduleIdent : Rule ModuleIdent
moduleIdent
= terminal "Expected module identifier"
(\x => case x.val of
DotSepIdent ns => Just ns
Ident i => Just [i]
DotSepIdent ns n => Just (mkModuleIdent (Just ns) n)
Ident i => Just (mkModuleIdent Nothing i)
_ => Nothing)
export
@ -193,31 +197,32 @@ reservedNames
export
name : Rule Name
name = opNonNS <|> do
ns <- namespacedIdent
opNS ns <|> nameNS ns
nsx <- namespacedIdent
-- writing (ns, x) <- namespacedIdent leads to an unsoled constraint.
-- I tried to write a minimised test case but could not reproduce the error
-- on a simplified example.
let ns = fst nsx
let x = snd nsx
opNS (mkNestedNamespace ns x) <|> nameNS ns x
where
reserved : String -> Bool
reserved n = n `elem` reservedNames
nameNS : List1 String -> SourceEmptyRule Name
nameNS [x] =
nameNS : Maybe Namespace -> String -> SourceEmptyRule Name
nameNS ns x =
if reserved x
then fail $ "can't use reserved name " ++ x
else pure $ UN x
nameNS (x :: xs) =
if reserved x
then fail $ "can't use reserved name " ++ x
else pure $ NS xs (UN x)
else pure $ mkNamespacedName ns x
opNonNS : Rule Name
opNonNS = symbol "(" *> operator <* symbol ")"
opNS : List1 String -> Rule Name
opNS : Namespace -> Rule Name
opNS ns = do
symbol ".("
n <- operator
symbol ")"
pure (NS (toList ns) n)
pure (NS ns n)
export
IndentInfo : Type
@ -427,15 +432,15 @@ blockWithOptHeaderAfter {ty} mincol header item
pure (Nothing, ps)
export
nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List1 ty)
nonEmptyBlock item
= do symbol "{"
commit
res <- blockEntry AnyIndent item
ps <- blockEntries (snd res) item
symbol "}"
pure (fst res :: ps)
pure (fst res ::: ps)
<|> do col <- column
res <- blockEntry (AtPos col) item
ps <- blockEntries (snd res) item
pure (fst res :: ps)
pure (fst res ::: ps)

6
src/TTImp/BindImplicits.idr
View File

@ -105,11 +105,7 @@ doBind ns (IQuote fc tm)
doBind ns (IUnquote fc tm)
= IUnquote fc (doBind ns tm)
doBind ns (IAlternative fc u alts)
= IAlternative fc (doBindAlt u) (map (doBind ns) alts)
where
doBindAlt : AltType -> AltType
doBindAlt (UniqueDefault t) = UniqueDefault (doBind ns t)
doBindAlt u = u
= IAlternative fc (mapAltType (doBind ns) u) (map (doBind ns) alts)
doBind ns tm = tm
export

1
src/TTImp/Elab.idr
View File

@ -1,6 +1,7 @@
module TTImp.Elab
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.LinearCheck

1
src/TTImp/Elab/Ambiguity.idr
View File

@ -1,6 +1,7 @@
module TTImp.Elab.Ambiguity
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

1
src/TTImp/Elab/App.idr
View File

@ -2,6 +2,7 @@ module TTImp.Elab.App
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

1
src/TTImp/Elab/As.idr
View File

@ -1,6 +1,7 @@
module TTImp.Elab.As
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

1
src/TTImp/Elab/Case.idr
View File

@ -1,6 +1,7 @@
module TTImp.Elab.Case
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

1
src/TTImp/Elab/Check.idr
View File

@ -4,6 +4,7 @@ module TTImp.Elab.Check
-- reading and writing elaboration state
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

1
src/TTImp/Elab/Delayed.idr
View File

@ -2,6 +2,7 @@ module TTImp.Elab.Delayed
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

1
src/TTImp/Elab/Hole.idr
View File

@ -1,6 +1,7 @@
module TTImp.Elab.Hole
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

1
src/TTImp/Elab/ImplicitBind.idr
View File

@ -3,6 +3,7 @@ module TTImp.Elab.ImplicitBind
-- variables or unbound implicits as type variables)
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

3
src/TTImp/Elab/Local.idr
View File

@ -2,6 +2,7 @@ module TTImp.Elab.Local
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
@ -42,7 +43,7 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
if vis == Public
then map setPublic nestdecls_in
else nestdecls_in
let defNames = definedInBlock [] nestdecls
let defNames = definedInBlock emptyNS nestdecls
names' <- traverse (applyEnv f)
(nub defNames) -- binding names must be unique
-- fixes bug #115

1
src/TTImp/Elab/Record.idr
View File

@ -1,6 +1,7 @@
module TTImp.Elab.Record
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata

Some files were not shown because too many files have changed in this diff Show More