idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Rui Barreiro 2020-07-07 14:18:00 +01:00
commit 2feb4b8299
23 changed files with 263 additions and 259 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1,34 +1,32 @@
module Data.Either
%default total
||| True if the argument is Left, False otherwise
public export
isLeft : Either a b -> Bool
isLeft (Left l) = True
isLeft (Right r) = False
isLeft (Left _) = True
isLeft (Right _) = False
||| True if the argument is Right, False otherwise
public export
isRight : Either a b -> Bool
isRight (Left l) = False
isRight (Right r) = True
isRight (Left _) = False
isRight (Right _) = True
||| Keep the payloads of all Left constructors in a list of Eithers
public export
lefts : List (Either a b) -> List a
lefts [] = []
lefts (x::xs) =
case x of
Left l => l :: lefts xs
Right r => lefts xs
lefts [] = []
lefts (Left l :: xs) = l :: lefts xs
lefts (Right _ :: xs) = lefts xs
||| Keep the payloads of all Right constructors in a list of Eithers
public export
rights : List (Either a b) -> List b
rights [] = []
rights (x::xs) =
case x of
Left l => rights xs
Right r => r :: rights xs
rights [] = []
rights (Left _ :: xs) = rights xs
rights (Right r :: xs) = r :: rights xs
||| Split a list of Eithers into a list of the left elements and a list of the right elements
public export
@ -64,21 +62,12 @@ eitherToMaybe : Either e a -> Maybe a
eitherToMaybe (Left _) = Nothing
eitherToMaybe (Right x) = Just x
-- Injectivity of constructors
||| Left is injective
total
leftInjective : {b : Type}
-> {x : a}
-> {y : a}
-> (Left {b = b} x = Left {b = b} y) -> (x = y)
leftInjective : Left x = Left y -> x = y
leftInjective Refl = Refl
||| Right is injective
total
rightInjective : {a : Type}
-> {x : b}
-> {y : b}
-> (Right {a = a} x = Right {a = a} y) -> (x = y)
rightInjective : Right x = Right y -> x = y
rightInjective Refl = Refl

84
libs/base/Data/Fin.idr
View File

@ -4,6 +4,8 @@ import public Data.Maybe
import Data.Nat
import Decidable.Equality
%default total
||| Numbers strictly less than some bound. The name comes from "finite sets".
|||
||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
@ -15,47 +17,46 @@ data Fin : (n : Nat) -> Type where
FS : Fin k -> Fin (S k)
export
implementation Uninhabited (Fin Z) where
Uninhabited (Fin Z) where
uninhabited FZ impossible
uninhabited (FS f) impossible
export
FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n
FSInjective left _ Refl = Refl
Uninhabited (FZ = FS k) where
uninhabited Refl impossible
export
implementation Eq (Fin n) where
Uninhabited (FS k = FZ) where
uninhabited Refl impossible
export
fsInjective : FS m = FS n -> m = n
fsInjective Refl = Refl
export
Eq (Fin n) where
(==) FZ FZ = True
(==) (FS k) (FS k') = k == k'
(==) _ _ = False
||| There are no elements of `Fin Z`
export
FinZAbsurd : Fin Z -> Void
FinZAbsurd FZ impossible
export
FinZElim : Fin Z -> a
FinZElim x = void (FinZAbsurd x)
||| Convert a Fin to a Nat
public export
finToNat : Fin n -> Nat
finToNat FZ = Z
finToNat (FS k) = S (finToNat k)
finToNat (FS k) = S $ finToNat k
||| `finToNat` is injective
export
finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
finToNatInjective (FS m) FZ Refl impossible
finToNatInjective FZ (FS n) Refl impossible
finToNatInjective FZ FZ _ = Refl
finToNatInjective (FS _) FZ Refl impossible
finToNatInjective FZ (FS _) Refl impossible
finToNatInjective (FS m) (FS n) prf =
cong FS (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
finToNatInjective FZ FZ Refl = Refl
cong FS $ finToNatInjective m n $ succInjective (finToNat m) (finToNat n) prf
export
implementation Cast (Fin n) Nat where
cast x = finToNat x
Cast (Fin n) Nat where
cast = finToNat
||| Convert a Fin to an Integer
public export
@ -64,37 +65,37 @@ finToInteger FZ = 0
finToInteger (FS k) = 1 + finToInteger k
export
implementation Cast (Fin n) Integer where
cast x = finToInteger x
Cast (Fin n) Integer where
cast = finToInteger
||| Weaken the bound on a Fin by 1
public export
weaken : Fin n -> Fin (S n)
weaken FZ = FZ
weaken (FS k) = FS (weaken k)
weaken (FS k) = FS $ weaken k
||| Weaken the bound on a Fin by some amount
public export
weakenN : (n : Nat) -> Fin m -> Fin (m + n)
weakenN n FZ = FZ
weakenN n (FS f) = FS (weakenN n f)
weakenN n (FS f) = FS $ weakenN n f
||| Weaken the bound on a Fin using a constructive comparison
public export
weakenLTE : Fin n -> LTE n m -> Fin m
weakenLTE FZ LTEZero impossible
weakenLTE (FS _) LTEZero impossible
weakenLTE FZ (LTESucc y) = FZ
weakenLTE FZ (LTESucc _) = FZ
weakenLTE (FS x) (LTESucc y) = FS $ weakenLTE x y
||| Attempt to tighten the bound on a Fin.
||| Return `Left` if the bound could not be tightened, or `Right` if it could.
export
strengthen : {n : _} -> Fin (S n) -> Either (Fin (S n)) (Fin n)
strengthen {n = S k} FZ = Right FZ
strengthen {n = S k} (FS i) with (strengthen i)
strengthen (FS i) | Left x = Left (FS x)
strengthen (FS i) | Right x = Right (FS x)
strengthen {n = S _} FZ = Right FZ
strengthen {n = S _} (FS i) with (strengthen i)
strengthen (FS _) | Left x = Left $ FS x
strengthen (FS _) | Right x = Right $ FS x
strengthen f = Left f
||| Add some natural number to a Fin, extending the bound accordingly
@ -103,7 +104,7 @@ strengthen f = Left f
public export
shift : (m : Nat) -> Fin n -> Fin (m + n)
shift Z f = f
shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)
shift (S m) f = FS $ shift m f
||| The largest element of some Fin type
public export
@ -111,22 +112,16 @@ last : {n : _} -> Fin (S n)
last {n=Z} = FZ
last {n=S _} = FS last
public export total
FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
FSinjective Refl = Refl
export
implementation Ord (Fin n) where
Ord (Fin n) where
compare FZ FZ = EQ
compare FZ (FS _) = LT
compare (FS _) FZ = GT
compare (FS x) (FS y) = compare x y
-- Construct a Fin from an integer literal which must fit in the given Fin
public export
natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
natToFin Z (S j) = Just FZ
natToFin Z (S _) = Just FZ
natToFin (S k) (S j)
= case natToFin k j of
Just k' => Just (FS k')
@ -165,17 +160,12 @@ restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in
-- DecEq
--------------------------------------------------------------------------------
export total
FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
FZNotFS Refl impossible
export
implementation DecEq (Fin n) where
DecEq (Fin n) where
decEq FZ FZ = Yes Refl
decEq FZ (FS f) = No FZNotFS
decEq (FS f) FZ = No $ negEqSym FZNotFS
decEq FZ (FS f) = No absurd
decEq (FS f) FZ = No absurd
decEq (FS f) (FS f')
= case decEq f f' of
Yes p => Yes $ cong FS p
No p => No $ \h => p $ FSinjective {f = f} {f' = f'} h
No p => No $ p . fsInjective

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

@ -1,7 +1,5 @@
module Data.List
import Decidable.Equality
public export
isNil : List a -> Bool
isNil [] = True
@ -19,13 +17,12 @@ snoc xs x = xs ++ [x]
public export
length : List a -> Nat
length [] = Z
length (x::xs) = S (length xs)
length (x::xs) = S $ length xs
public export
take : Nat -> List a -> List a
take Z xs = []
take (S k) [] = []
take (S k) (x :: xs) = x :: take k xs
take _ _ = []
public export
drop : (n : Nat) -> (xs : List a) -> List a
@ -57,8 +54,7 @@ inBounds Z (x :: xs) = Yes InFirst
inBounds (S k) (x :: xs) with (inBounds k xs)
inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)
inBounds (S k) (x :: xs) | (No contra)
= No (\p => case p of
InLater y => contra y)
= No $ \(InLater y) => contra y
||| Find a particular element of a list.
|||
@ -105,12 +101,11 @@ find p (x::xs) = if p x then Just x else find p xs
public export
lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
lookupBy p e [] = Nothing
lookupBy p e (x::xs) =
let (l, r) = x in
if p e l then
Just r
else
lookupBy p e xs
lookupBy p e ((l, r) :: xs) =
if p e l then
Just r
else
lookupBy p e xs
||| Find associated information in a list using Boolean equality.
public export
@ -348,7 +343,7 @@ head (x :: xs) = x
public export
tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
tail [] impossible
tail (x :: xs) = xs
tail (_ :: xs) = xs
||| Retrieve the last element of a non-empty list.
||| @ ok proof that the list is non-empty
@ -363,20 +358,20 @@ last (x::y::ys) = last (y::ys)
public export
init : (l : List a) -> {auto ok : NonEmpty l} -> List a
init [] impossible
init [x] = []
init [_] = []
init (x::y::ys) = x :: init (y::ys)
||| Attempt to get the head of a list. If the list is empty, return `Nothing`.
public export
head' : List a -> Maybe a
head' [] = Nothing
head' (x::xs) = Just x
head' (x::_) = Just x
||| Attempt to get the tail of a list. If the list is empty, return `Nothing`.
export
tail' : List a -> Maybe (List a)
tail' [] = Nothing
tail' (x::xs) = Just xs
tail' (_::xs) = Just xs
||| Attempt to retrieve the last element of a non-empty list.
|||
@ -483,11 +478,8 @@ foldr1' f xs@(_::_) = Just (foldr1 f xs)
||| Check whether a list is sorted with respect to the default ordering for the type of its elements.
export
sorted : Ord a => List a -> Bool
sorted [] = True
sorted (x::xs) =
case xs of
Nil => True
(y::ys) => x <= y && sorted (y::ys)
sorted (x :: xs @ (y :: _)) = x <= y && sorted xs
sorted _ = True
||| Merge two sorted lists using an arbitrary comparison
||| predicate. Note that the lists must have been sorted using this
@ -539,13 +531,9 @@ sort = sortBy compare
export
isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
isPrefixOfBy p [] right = True
isPrefixOfBy p left [] = False
isPrefixOfBy p (x::xs) (y::ys) =
if p x y then
isPrefixOfBy p xs ys
else
False
isPrefixOfBy p [] _ = True
isPrefixOfBy p _ [] = False
isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
||| The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second.
export
@ -607,6 +595,12 @@ export
Uninhabited (Prelude.(::) x xs = []) where
uninhabited Refl impossible
||| (::) is injective
export
consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x :: xs = y :: ys -> (x = y, xs = ys)
consInjective Refl = (Refl, Refl)
||| The empty list is a right identity for append.
export
appendNilRightNeutral : (l : List a) ->
@ -641,32 +635,3 @@ revAppend (v :: vs) ns
rewrite sym (revAppend vs ns) in
rewrite appendAssociative (reverse ns) (reverse vs) [v] in
Refl
public export
lemma_val_not_nil : {x : t} -> {xs : List t} -> ((x :: xs) = Prelude.Nil {a = t} -> Void)
lemma_val_not_nil Refl impossible
public export
lemma_x_eq_xs_neq : {x : t} -> {xs : List t} -> {y : t} -> {ys : List t} -> (x = y) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)
lemma_x_eq_xs_neq Refl p Refl = p Refl
public export
lemma_x_neq_xs_eq : {x : t} -> {xs : List t} -> {y : t} -> {ys : List t} -> (x = y -> Void) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> Void)
lemma_x_neq_xs_eq p Refl Refl = p Refl
public export
lemma_x_neq_xs_neq : {x : t} -> {xs : List t} -> {y : t} -> {ys : List t} -> (x = y -> Void) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)
lemma_x_neq_xs_neq p p' Refl = p Refl
public export
implementation DecEq a => DecEq (List a) where
decEq [] [] = Yes Refl
decEq (x :: xs) [] = No lemma_val_not_nil
decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
decEq (x :: xs) (y :: ys) with (decEq x y)
decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq)
decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)
decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)

6
libs/base/Data/List/Views.idr
View File

@ -5,6 +5,8 @@ import Data.List
import Data.Nat
import Data.Nat.Views
%default total
lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
length (xs ++ (y :: ys)) = S (length (xs ++ ys))
lengthSuc [] _ _ = Refl
@ -62,7 +64,7 @@ data SplitRec : List a -> Type where
||| Covering function for the `SplitRec` view
||| Constructs the view in O(n lg n)
public export total
public export
splitRec : (xs : List a) -> SplitRec xs
splitRec xs with (sizeAccessible xs)
splitRec xs | acc with (split xs)
@ -92,5 +94,3 @@ snocListHelp snoc (x :: xs)
export
snocList : (xs : List a) -> SnocList xs
snocList xs = snocListHelp Empty xs

13
libs/base/Data/Maybe.idr
View File

@ -3,12 +3,12 @@ module Data.Maybe
public export
isNothing : Maybe a -> Bool
isNothing Nothing = True
isNothing (Just j) = False
isNothing (Just _) = False
public export
isJust : Maybe a -> Bool
isJust Nothing = False
isJust (Just j) = True
isJust (Just _) = True
||| Proof that some `Maybe` is actually `Just`
public export
@ -22,7 +22,7 @@ Uninhabited (IsJust Nothing) where
||| Decide whether a 'Maybe' is 'Just'
public export
isItJust : (v : Maybe a) -> Dec (IsJust v)
isItJust (Just x) = Yes ItIsJust
isItJust (Just _) = Yes ItIsJust
isItJust Nothing = No absurd
||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
@ -30,7 +30,7 @@ isItJust Nothing = No absurd
public export
fromMaybe : (Lazy a) -> Maybe a -> a
fromMaybe def Nothing = def
fromMaybe def (Just j) = j
fromMaybe _ (Just j) = j
||| Returns the `a` value of a `Maybe a` which is proved `Just`.
public export
@ -43,10 +43,10 @@ fromJust Nothing impossible
public export
toMaybe : Bool -> Lazy a -> Maybe a
toMaybe True j = Just j
toMaybe False j = Nothing
toMaybe False _ = Nothing
export
justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
justInjective : Just x = Just y -> x = y
justInjective Refl = Refl
||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case
@ -60,4 +60,3 @@ lowerMaybe (Just x) = x
export
raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a
raiseToMaybe x = if x == neutral then Nothing else Just x

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

@ -241,7 +241,7 @@ data CmpNat : Nat -> Nat -> Type where
CmpGT : (x : _) -> CmpNat (y + S x) y
export
total cmp : (x, y : Nat) -> CmpNat x y
cmp : (x, y : Nat) -> CmpNat x y
cmp Z Z = CmpEQ
cmp Z (S k) = CmpLT _
cmp (S k) Z = CmpGT _

4
libs/base/Data/Nat/Views.idr
View File

@ -3,6 +3,8 @@ module Data.Nat.Views
import Control.WellFounded
import Data.Nat
%default total
||| View for dividing a Nat in half
public export
data Half : Nat -> Type where
@ -25,7 +27,7 @@ half (S k) with (half k)
HalfEven (S n)
half (S (n + n)) | HalfEven n = HalfOdd n
public export total
public export
halfRec : (n : Nat) -> HalfRec n
halfRec n with (sizeAccessible n)
halfRec Z | acc = HalfRecZ

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

@ -2,6 +2,9 @@ module Decidable.Equality
import Data.Maybe
import Data.Nat
import Data.List
%default total
--------------------------------------------------------------------------------
-- Decidable equality
@ -11,19 +14,19 @@ import Data.Nat
public export
interface DecEq t where
||| Decide whether two elements of `t` are propositionally equal
total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
--------------------------------------------------------------------------------
-- Utility lemmas
--------------------------------------------------------------------------------
||| The negation of equality is symmetric (follows from symmetry of equality)
export total
export
negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
negEqSym p h = p (sym h)
||| Everything is decidably equal to itself
export total
export
decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
decEqSelfIsYes {x} with (decEq x x)
decEqSelfIsYes {x} | Yes Refl = Refl
@ -34,34 +37,29 @@ decEqSelfIsYes {x} with (decEq x x)
--------------------------------------------------------------------------------
export
implementation DecEq () where
DecEq () where
decEq () () = Yes Refl
--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------
total trueNotFalse : True = False -> Void
trueNotFalse Refl impossible
export
implementation DecEq Bool where
DecEq Bool where
decEq True True = Yes Refl
decEq False False = Yes Refl
decEq True False = No trueNotFalse
decEq False True = No (negEqSym trueNotFalse)
decEq False True = No absurd
decEq True False = No absurd
--------------------------------------------------------------------------------
-- Nat
--------------------------------------------------------------------------------
total ZnotS : Z = S n -> Void
ZnotS Refl impossible
export
implementation DecEq Nat where
DecEq Nat where
decEq Z Z = Yes Refl
decEq Z (S _) = No ZnotS
decEq (S _) Z = No (negEqSym ZnotS)
decEq Z (S _) = No absurd
decEq (S _) Z = No absurd
decEq (S n) (S m) with (decEq n m)
decEq (S n) (S m) | Yes p = Yes $ cong S p
decEq (S n) (S m) | No p = No $ \h : (S n = S m) => p $ succInjective n m h
@ -70,18 +68,49 @@ implementation DecEq Nat where
-- Maybe
--------------------------------------------------------------------------------
total nothingNotJust : {x : t} -> (Nothing {ty = t} = Just x) -> Void
nothingNotJust Refl impossible
export
implementation (DecEq t) => DecEq (Maybe t) where
DecEq t => DecEq (Maybe t) where
decEq Nothing Nothing = Yes Refl
decEq Nothing (Just _) = No absurd
decEq (Just _) Nothing = No absurd
decEq (Just x') (Just y') with (decEq x' y')
decEq (Just x') (Just y') | Yes p = Yes $ cong Just p
decEq (Just x') (Just y') | No p
= No $ \h : Just x' = Just y' => p $ justInjective h
decEq Nothing (Just _) = No nothingNotJust
decEq (Just _) Nothing = No (negEqSym nothingNotJust)
--------------------------------------------------------------------------------
-- Tuple
--------------------------------------------------------------------------------
pairInjective : (a, b) = (c, d) -> (a = c, b = d)
pairInjective Refl = (Refl, Refl)
export
(DecEq a, DecEq b) => DecEq (a, b) where
decEq (a, b) (a', b') with (decEq a a')
decEq (a, b) (a', b') | (No contra) =
No $ contra . fst . pairInjective
decEq (a, b) (a, b') | (Yes Refl) with (decEq b b')
decEq (a, b) (a, b) | (Yes Refl) | (Yes Refl) = Yes Refl
decEq (a, b) (a, b') | (Yes Refl) | (No contra) =
No $ contra . snd . pairInjective
--------------------------------------------------------------------------------
-- List
--------------------------------------------------------------------------------
export
DecEq a => DecEq (List a) where
decEq [] [] = Yes Refl
decEq (x :: xs) [] = No absurd
decEq [] (x :: xs) = No absurd
decEq (x :: xs) (y :: ys) with (decEq x y)
decEq (x :: xs) (y :: ys) | No contra =
No $ contra . fst . consInjective
decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
decEq (x :: xs) (x :: ys) | (Yes Refl) | (No contra) =
No $ contra . snd . consInjective
-- TODO: Other prelude data types
@ -91,59 +120,6 @@ implementation (DecEq t) => DecEq (Maybe t) where
-- A postulate would be better, but erasure analysis may think they're needed
-- for computation in a higher order setting.
--------------------------------------------------------------------------------
-- Tuple
--------------------------------------------------------------------------------
lemma_both_neq : (x = x' -> Void) -> (y = y' -> Void) -> ((x, y) = (x', y') -> Void)
lemma_both_neq p_x_not_x' p_y_not_y' Refl = p_x_not_x' Refl
lemma_snd_neq : (x = x) -> (y = y' -> Void) -> ((x, y) = (x, y') -> Void)
lemma_snd_neq Refl p Refl = p Refl
lemma_fst_neq_snd_eq : (x = x' -> Void) ->
(y = y') ->
((x, y) = (x', y) -> Void)
lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl
export
implementation (DecEq a, DecEq b) => DecEq (a, b) where
decEq (a, b) (a', b') with (decEq a a')
decEq (a, b) (a, b') | (Yes Refl) with (decEq b b')
decEq (a, b) (a, b) | (Yes Refl) | (Yes Refl) = Yes Refl
decEq (a, b) (a, b') | (Yes Refl) | (No p) = No (\eq => lemma_snd_neq Refl p eq)
decEq (a, b) (a', b') | (No p) with (decEq b b')
decEq (a, b) (a', b) | (No p) | (Yes Refl) = No (\eq => lemma_fst_neq_snd_eq p Refl eq)
decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
--------------------------------------------------------------------------------
-- List
--------------------------------------------------------------------------------
lemma_val_not_nil : (the (List _) (x :: xs) = Prelude.Nil {a = t} -> Void)
lemma_val_not_nil Refl impossible
lemma_x_eq_xs_neq : (x = y) -> (xs = ys -> Void) -> (the (List _) (x :: xs) = (y :: ys) -> Void)
lemma_x_eq_xs_neq Refl p Refl = p Refl
lemma_x_neq_xs_eq : (x = y -> Void) -> (xs = ys) -> (the (List _) (x :: xs) = (y :: ys) -> Void)
lemma_x_neq_xs_eq p Refl Refl = p Refl
lemma_x_neq_xs_neq : (x = y -> Void) -> (xs = ys -> Void) -> (the (List _) (x :: xs) = (y :: ys) -> Void)
lemma_x_neq_xs_neq p p' Refl = p Refl
implementation DecEq a => DecEq (List a) where
decEq [] [] = Yes Refl
decEq (x :: xs) [] = No lemma_val_not_nil
decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
decEq (x :: xs) (y :: ys) with (decEq x y)
decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq)
decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)
decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)
--------------------------------------------------------------------------------
-- Int
@ -196,4 +172,3 @@ implementation DecEq String where
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()

4
libs/base/System/File.idr
View File

@ -19,7 +19,7 @@ libc fn = "C:" ++ fn ++ ", libc 6"
%foreign support "idris2_openFile"
"node:support:openFile,support_system_file"
prim__open : String -> String -> Int -> PrimIO FilePtr
prim__open : String -> String -> PrimIO FilePtr
%foreign support "idris2_closeFile"
"node:lambdaRequire:fs:(fp) => __require_fs.closeSync(fp.fd)"
@ -151,7 +151,7 @@ stderr = FHandle prim__stderr
export
openFile : HasIO io => String -> Mode -> io (Either FileError File)
openFile f m
= do res <- primIO (prim__open f (modeStr m) 0)
= do res <- primIO (prim__open f (modeStr m))
if prim__nullAnyPtr res /= 0
then returnError
else ok (FHandle res)

6
libs/contrib/Data/List/Equalities.idr
View File

@ -16,12 +16,6 @@ SnocNonEmpty : (xs : List a) -> (x : a) -> NonEmpty (xs `snoc` x)
SnocNonEmpty [] _ = IsNonEmpty
SnocNonEmpty (_::_) _ = IsNonEmpty
||| (::) is injective
export
consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
(x :: xs) = (y :: ys) -> (x = y, xs = ys)
consInjective Refl = (Refl, Refl)
||| Two lists are equal, if their heads are equal and their tails are equal.
export
consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->

28
libs/contrib/Data/Vect/Sort.idr Normal file
View File

@ -0,0 +1,28 @@
module Data.Vect.Sort
import Data.Vect
import Data.Nat.Views
mutual
sortBySplit : (n : Nat) -> (a -> a -> Ordering) -> Vect n a -> Vect n a
sortBySplit Z cmp [] = []
sortBySplit (S Z) cmp [x] = [x]
sortBySplit n cmp xs with (half n)
sortBySplit (k + k) cmp xs | HalfEven k = sortByMerge k k cmp xs
sortBySplit (S (k + k)) cmp xs | HalfOdd k = sortByMerge (S k) k cmp xs
sortByMerge : (n : Nat) -> (m : Nat) -> (a -> a -> Ordering) -> Vect (n + m) a -> Vect (n + m) a
sortByMerge n m cmp xs =
let (left, right) = splitAt n xs in
mergeBy cmp
(sortBySplit n cmp (assert_smaller xs left))
(sortBySplit m cmp (assert_smaller xs right))
||| Merge sort implementation for Vect n a
export total
sortBy : {n : Nat} -> (cmp : a -> a -> Ordering) -> (xs : Vect n a) -> Vect n a
sortBy {n} cmp xs = sortBySplit n cmp xs
export total
sort : Ord a => {n : Nat} -> Vect n a -> Vect n a
sort = sortBy compare

2
libs/contrib/contrib.ipkg
View File

@ -34,6 +34,8 @@ modules = Control.ANSI,
Data.String.Interpolation,
Data.String.Parser,
Data.Vect.Sort,
Debug.Buffer,
Language.JSON,

16
libs/prelude/Prelude.idr
View File

@ -70,6 +70,14 @@ infixl 9 `div`, `mod`
public export
data Bool = True | False
public export
Uninhabited (True = False) where
uninhabited Refl impossible
public export
Uninhabited (False = True) where
uninhabited Refl impossible
||| Boolean NOT.
public export
not : (1 b : Bool) -> Bool
@ -811,6 +819,14 @@ data Maybe : (ty : Type) -> Type where
||| A value of type `ty` is stored
Just : (1 x : ty) -> Maybe ty
public export
Uninhabited (Nothing = Just x) where
uninhabited Refl impossible
public export
Uninhabited (Just x = Nothing) where
uninhabited Refl impossible
public export
maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
maybe n j Nothing = n

6
src/Idris/Error.idr
View File

@ -176,9 +176,9 @@ perror (RecordTypeNeeded fc _)
perror (NotRecordField fc fld Nothing)
= pure $ fld ++ " is not part of a record type at:\n" ++ !(ploc fc)
perror (NotRecordField fc fld (Just ty))
= pure $ "Record type " ++ show ty ++ " has no field " ++ fld ++ " at:\n" ++ !(ploc fc)
= pure $ "Record type " ++ show !(getFullName ty) ++ " has no field " ++ fld ++ " at:\n" ++ !(ploc fc)
perror (NotRecordType fc ty)
= pure $ show ty ++ " is not a record type at:\n" ++ !(ploc fc)
= pure $ show !(getFullName ty) ++ " is not a record type at:\n" ++ !(ploc fc)
perror (IncompatibleFieldUpdate fc flds)
= pure $ "Field update " ++ showSep "->" flds ++
" not compatible with other updates at:\n" ++ !(ploc fc)
@ -263,7 +263,7 @@ perror (BadImplicit fc str)
perror (BadRunElab fc env script)
= pure $ "Bad elaborator script " ++ !(pshow env script) ++ " at:\n" ++ !(ploc fc)
perror (GenericMsg fc str) = pure $ str ++ " at:\n" ++ !(ploc fc)
perror (TTCError msg) = pure $ "Error in TTC file: " ++ show msg
perror (TTCError msg) = pure $ "Error in TTC file: " ++ show msg ++ " (the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files)"
perror (FileErr fname err)
= pure $ "File error in " ++ fname ++ ": " ++ show err
perror (ParseFail _ err)

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

@ -22,20 +22,43 @@ getRecordType env (NTCon _ n _ _ _) = Just n
getRecordType env _ = Nothing
data Rec : Type where
Field : String -> RawImp -> Rec -- field name on left, value on right
Constr : Name -> List (String, Rec) -> Rec
Field : Maybe Name -> -- implicit argument name, if any
String -> RawImp -> Rec -- field name on left, value on right
Constr : Maybe Name -> -- implicit argument name, if any
Name -> List (String, Rec) -> Rec
Show Rec where
show (Field mn n ty)
= "Field " ++ show mn ++ "; " ++ show n ++ " : " ++ show ty
show (Constr mn n args)
= "Constr " ++ show mn ++ " " ++ show n ++ " " ++ show args
applyImp : RawImp -> List (Maybe Name, RawImp) -> RawImp
applyImp f [] = f
applyImp f ((Nothing, arg) :: xs)
= applyImp (IApp (getFC f) f arg) xs
applyImp f ((Just n, arg) :: xs)
= applyImp (IImplicitApp (getFC f) f (Just n) arg) xs
toLHS' : FC -> Rec -> (Maybe Name, RawImp)
toLHS' loc (Field mn@(Just _) n _)
= (mn, IAs loc UseRight (UN n) (Implicit loc True))
toLHS' loc (Field mn n _) = (mn, IBindVar loc n)
toLHS' loc (Constr mn con args)
= let args' = map (\a => toLHS' loc (snd a)) args in
(mn, applyImp (IVar loc con) args')
toLHS : FC -> Rec -> RawImp
toLHS loc (Field n _) = IBindVar loc n
toLHS loc (Constr con args)
= let args' = map (\a => toLHS loc (snd a)) args in
apply (IVar loc con) args'
toLHS fc r = snd (toLHS' fc r)
toRHS' : FC -> Rec -> (Maybe Name, RawImp)
toRHS' loc (Field mn _ val) = (mn, val)
toRHS' loc (Constr mn con args)
= let args' = map (\a => toRHS' loc (snd a)) args in
(mn, applyImp (IVar loc con) args')
toRHS : FC -> Rec -> RawImp
toRHS loc (Field _ val) = val
toRHS loc (Constr con args)
= let args' = map (\a => toRHS loc (snd a)) args in
apply (IVar loc con) args'
toRHS fc r = snd (toRHS' fc r)
findConName : Defs -> Name -> Core (Maybe Name)
findConName defs tyn
@ -43,18 +66,20 @@ findConName defs tyn
Just (TCon _ _ _ _ _ _ [con] _) => pure (Just con)
_ => pure Nothing
findFields : Defs -> Name -> Core (Maybe (List (String, Maybe Name)))
findFields : Defs -> Name ->
Core (Maybe (List (String, Maybe Name, Maybe Name)))
findFields defs con
= case !(lookupTyExact con (gamma defs)) of
Just t => pure (Just !(getExpNames !(nf defs [] t)))
_ => pure Nothing
where
getExpNames : NF [] -> Core (List (String, Maybe Name))
getExpNames : NF [] -> Core (List (String, Maybe Name, Maybe Name))
getExpNames (NBind fc x (Pi _ p ty) sc)
= do rest <- getExpNames !(sc defs (toClosure defaultOpts [] (Erased fc False)))
case p of
Explicit => pure $ (nameRoot x, getRecordType [] ty) :: rest
_ => pure rest
let imp = case p of
Explicit => Nothing
_ => Just x
pure $ (nameRoot x, imp, getRecordType [] ty) :: rest
getExpNames _ = pure []
genFieldName : {auto u : Ref UST UState} ->
@ -79,39 +104,39 @@ findPath : {auto c : Ref Ctxt Defs} ->
FC -> List String -> List String -> Maybe Name ->
(String -> RawImp) ->
Rec -> Core Rec
findPath loc [] full tyn val (Field lhs _) = pure (Field lhs (val lhs))
findPath loc [] full tyn val (Field mn lhs _) = pure (Field mn lhs (val lhs))
findPath loc [] full tyn val rec
= throw (IncompatibleFieldUpdate loc full)
findPath loc (p :: ps) full Nothing val (Field n v)
findPath loc (p :: ps) full Nothing val (Field mn n v)
= throw (NotRecordField loc p Nothing)
findPath loc (p :: ps) full (Just tyn) val (Field n v)
findPath loc (p :: ps) full (Just tyn) val (Field mn n v)
= do defs <- get Ctxt
Just con <- findConName defs tyn
| Nothing => throw (NotRecordType loc tyn)
Just fs <- findFields defs con
| Nothing => throw (NotRecordType loc tyn)
args <- mkArgs fs
let rec' = Constr con args
let rec' = Constr mn con args
findPath loc (p :: ps) full (Just tyn) val rec'
where
mkArgs : List (String, Maybe Name) ->
mkArgs : List (String, Maybe Name, Maybe Name) ->
Core (List (String, Rec))
mkArgs [] = pure []
mkArgs ((p, _) :: ps)
mkArgs ((p, imp, _) :: ps)
= do fldn <- genFieldName p
args' <- mkArgs ps
pure ((p, Field fldn (IVar loc (UN fldn))) :: args')
pure ((p, Field imp fldn (IVar loc (UN fldn))) :: args')
findPath loc (p :: ps) full tyn val (Constr con args)
findPath loc (p :: ps) full tyn val (Constr mn con args)
= do let Just prec = lookup p args
| Nothing => throw (NotRecordField loc p tyn)
defs <- get Ctxt
Just fs <- findFields defs con
| Nothing => pure (Constr con args)
let Just mfty = lookup p fs
| Nothing => pure (Constr mn con args)
let Just (imp, mfty) = lookup p fs
| Nothing => throw (NotRecordField loc p tyn)
prec' <- findPath loc ps full mfty val prec
pure (Constr con (replace p prec' args))
pure (Constr mn con (replace p prec' args))
getSides : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
@ -155,7 +180,8 @@ recUpdate rigc elabinfo loc nest env flds rec grecty
let Just rectyn = getRecordType env rectynf
| Nothing => throw (RecordTypeNeeded loc env)
fldn <- genFieldName "__fld"
sides <- getAllSides loc flds rectyn rec (Field fldn (IVar loc (UN fldn)))
sides <- getAllSides loc flds rectyn rec
(Field Nothing fldn (IVar loc (UN fldn)))
pure $ ICase loc rec (Implicit loc False) [mkClause sides]
where
mkClause : Rec -> ImpClause

2
tests/Main.idr
View File

@ -90,7 +90,7 @@ idrisTests
-- interesting interactions between features
"real001", "real002",
-- Records, access and dependent update
"record001", "record002", "record003", "record004",
"record001", "record002", "record003", "record004", "record005",
-- Quotation and reflection
"reflection001", "reflection002", "reflection003", "reflection004",
"reflection005", "reflection006", "reflection007", "reflection008",

2
tests/ideMode/ideMode001/expected
View File

@ -8,7 +8,7 @@
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:279}_[] ?{_:278}_[])")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:268}_[] ?{_:267}_[])")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:258} : (Main.Vect n[0] a[1])) -> (({arg:259} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:258} : (Main.Vect n[0] a[1])) -> (({arg:259} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:769:1--776:1 n[2] m[4]) a[3])))")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

2
tests/ideMode/ideMode003/expected
View File

@ -8,7 +8,7 @@
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:279}_[] ?{_:278}_[])")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:268}_[] ?{_:267}_[])")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:258} : (Main.Vect n[0] a[1])) -> (({arg:259} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:258} : (Main.Vect n[0] a[1])) -> (({arg:259} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:769:1--776:1 n[2] m[4]) a[3])))")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

9
tests/idris2/record005/Fld.idr Normal file
View File

@ -0,0 +1,9 @@
record Foo where
constructor MkFoo
{Gnu : Char}
AFoo : Foo
AFoo = MkFoo {Gnu = 'c'}
Bar : Foo
Bar = record { Gnu = '?' } AFoo

3
tests/idris2/record005/expected Normal file
View File

@ -0,0 +1,3 @@
1/1: Building Fld (Fld.idr)
Main> Main> MkFoo {Gnu = '?'}
Main> Bye for now!

3
tests/idris2/record005/input Normal file
View File

@ -0,0 +1,3 @@
:set showimplicits
Bar
:q

3
tests/idris2/record005/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-banner Fld.idr < input
rm -rf build

2
tests/idris2/reflection003/expected
View File

@ -1,6 +1,6 @@
1/1: Building refprims (refprims.idr)
LOG 0: Name: Prelude.List.++
LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.List a) (%pi RigW Explicit (Just {arg:6318}) (Prelude.List a) (Prelude.List a))))
LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.List a) (%pi RigW Explicit (Just {arg:6386}) (Prelude.List a) (Prelude.List a))))
LOG 0: Name: Prelude.Strings.++
LOG 0: Type: (%pi Rig1 Explicit (Just x) String (%pi Rig1 Explicit (Just y) String String))
LOG 0: Resolved name: Prelude.Nat