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' into add-docs-about-dirs

Browse Source
This commit is contained in:
Christian Rasmussen 2020-07-01 23:51:40 +02:00 committed by GitHub
commit b4ba476c8a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
121 changed files with 1736 additions and 205 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
CHANGELOG.md
View File

@ -34,6 +34,8 @@ Library changes:
* Added `Control.Monad.ST`, for update in-place via `STRef` (which is like
`IORef`, but can escape from `IO`). Also added `Data.Ref` which provides an
interface to both `IORef` and `STRef`.
* Added `Control.ANSI` in `contrib`, for usage of ANSI escape codes for text
styling and cursor/screen control in terminals.
Command-line options changes:

2
INSTALL.md
View File

@ -13,7 +13,7 @@ The requirements are:
On a Mac, you can install this with `brew install coreutils`.
On FreeBSD, OpenBSD and NetBSD, you can install `realpath` and `GNU make`
using a package manager. For instance, on OpenBSD you can install all of them
with `pkg_add coreutuls gmake` command.
with `pkg_add coreutils gmake` command.
On Windows, it has been reported that installing via `MSYS2` works
(https://www.msys2.org/). On Windows older than Windows 8, you may need to

4
Makefile
View File

@ -115,7 +115,7 @@ endif
mkdir -p ${PREFIX}/bin/${NAME}_app
install ${TARGETDIR}/${NAME}_app/* ${PREFIX}/bin/${NAME}_app
install-support: support
install-support:
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/racket
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/gambit
@ -124,7 +124,7 @@ install-support: support
install support/gambit/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/gambit
@${MAKE} -C support/c install
install-libs: libs
install-libs:
${MAKE} -C libs/prelude install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

2
docs/source/listing/idris-prompt-helloworld.txt
View File

@ -9,6 +9,6 @@ Welcome to Idris 2. Enjoy yourself!
Main> :t main
Main.main : IO ()
Main> :c hello main
File hello.so written
File build/exec/hello written
Main> :q
Bye for now!

2
docs/source/tutorial/starting.rst
View File

@ -87,7 +87,7 @@ which you can run:
::
$ idris2 hello.idr -o hello
$ ./build/exec/hello.so
$ ./build/exec/hello
Hello world
Please note that the dollar sign ``$`` indicates the shell prompt!

8
docs/source/tutorial/typesfuns.rst
View File

@ -143,9 +143,9 @@ We can test these functions at the Idris prompt:
::
Main> plus (S (S Z)) (S (S Z))
S (S (S (S Z)))
4
Main> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))
12
Like arithmetic operations, integer literals are also overloaded using
interfaces, meaning that we can also test the functions as follows:
@ -153,9 +153,9 @@ interfaces, meaning that we can also test the functions as follows:
::
Idris> plus 2 2
S (S (S (S Z)))
4
Idris> mult 3 (plus 2 2)
S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))
12
You may wonder, by the way, why we have unary natural numbers when our
computers have perfectly good integer arithmetic built in. The reason

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

@ -12,7 +12,7 @@ data Vect : (len : Nat) -> (elem : Type) -> Type where
Nil : Vect Z elem
||| A non-empty vector of length `S len`, consisting of a head element and
||| the rest of the list, of length `len`.
(::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
(::) : (1 x : elem) -> (1 xs : Vect len elem) -> Vect (S len) elem
-- Hints for interactive editing
%name Vect xs,ys,zs,ws
@ -23,8 +23,8 @@ length [] = 0
length (x::xs) = 1 + length xs
||| Show that the length function on vectors in fact calculates the length
private
lengthCorrect : (len : Nat) -> (xs : Vect len elem) -> length xs = len
export
lengthCorrect : (0 len : Nat) -> (xs : Vect len elem) -> length xs = len
lengthCorrect Z [] = Refl
lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
@ -86,10 +86,9 @@ index (FS k) (x::xs) = index k xs
||| insertAt 1 8 [1,2,3,4]
||| ```
public export
insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
insertAt : (1 idx : Fin (S len)) -> (1 x : elem) -> (1 xs : Vect len elem) -> Vect (S len) elem
insertAt FZ y xs = y :: xs
insertAt (FS k) y (x::xs) = x :: insertAt k y xs
insertAt (FS k) y [] = absurd k
||| Construct a new vector consisting of all but the indicated element
|||
@ -133,7 +132,7 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
||| [1,2,3,4] ++ [5,6]
||| ```
public export
(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
(++) : (1 xs : Vect m elem) -> (1 ys : Vect n elem) -> Vect (m + n) elem
(++) [] ys = ys
(++) (x::xs) ys = x :: xs ++ ys
@ -181,9 +180,9 @@ merge = mergeBy compare
||| reverse [1,2,3,4]
||| ```
public export
reverse : Vect len elem -> Vect len elem
reverse : (1 xs : Vect len elem) -> Vect len elem
reverse xs = go [] xs
where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
where go : (1 _ : Vect n elem) -> (1 _ : Vect m elem) -> Vect (n+m) elem
go {n} acc [] = rewrite plusZeroRightNeutral n in acc
go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
in go (x::acc) xs
@ -210,7 +209,7 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
--------------------------------------------------------------------------------
public export
fromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elem
fromList' : (1 xs : Vect len elem) -> (1 l : List elem) -> Vect (length l + len) elem
fromList' ys [] = ys
fromList' {len} ys (x::xs) =
rewrite (plusSuccRightSucc (length xs) len) in
@ -224,7 +223,7 @@ fromList' {len} ys (x::xs) =
||| fromList [1,2,3,4]
||| ```
public export
fromList : (l : List elem) -> Vect (length l) elem
fromList : (1 l : List elem) -> Vect (length l) elem
fromList l =
rewrite (sym $ plusZeroRightNeutral (length l)) in
reverse $ fromList' [] l
@ -263,8 +262,9 @@ zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])
||| ```
public export
zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
zip = zipWith (\x,y => (x,y))
zip : (1 xs : Vect n a) -> (1 ys : Vect n b) -> Vect n (a, b)
zip [] [] = []
zip (x::xs) (y::ys) = (x, y) :: zip xs ys
||| Combine three equal-length vectors elementwise into a vector of tuples
|||
@ -272,8 +272,9 @@ zip = zipWith (\x,y => (x,y))
||| zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])
||| ```
public export
zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
zip3 = zipWith3 (\x,y,z => (x,y,z))
zip3 : (1 xs : Vect n a) -> (1 ys : Vect n b) -> (1 zs : Vect n c) -> Vect n (a, b, c)
zip3 [] [] [] = []
zip3 (x::xs) (y::ys) (z::zs) = (x, y, z) :: zip3 xs ys zs
||| Convert a vector of pairs to a pair of vectors
|||
@ -281,10 +282,10 @@ zip3 = zipWith3 (\x,y,z => (x,y,z))
||| unzip (fromList [(1,2), (1,2)])
||| ```
public export
unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
unzip : (1 xs : Vect n (a, b)) -> (Vect n a, Vect n b)
unzip [] = ([], [])
unzip ((l, r)::xs) with (unzip xs)
unzip ((l, r)::xs) | (lefts, rights) = (l::lefts, r::rights)
unzip ((l, r)::xs) = let (lefts, rights) = unzip xs
in (l::lefts, r::rights)
||| Convert a vector of three-tuples to a triplet of vectors
|||
@ -292,11 +293,10 @@ unzip ((l, r)::xs) with (unzip xs)
||| unzip3 (fromList [(1,2,3), (1,2,3)])
||| ```
public export
unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
unzip3 : (1 xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
unzip3 [] = ([], [], [])
unzip3 ((l,c,r)::xs) with (unzip3 xs)
unzip3 ((l,c,r)::xs) | (lefts, centers, rights)
= (l::lefts, c::centers, r::rights)
unzip3 ((l,c,r)::xs) = let (lefts, centers, rights) = unzip3 xs
in (l::lefts, c::centers, r::rights)
--------------------------------------------------------------------------------
-- Equality
@ -374,7 +374,7 @@ implementation Foldable (Vect n) where
||| concat [[1,2,3], [4,5,6]]
||| ```
public export
concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
concat : (1 xss : Vect m (Vect n elem)) -> Vect (m * n) elem
concat [] = []
concat (v::vs) = v ++ Vect.concat vs
@ -748,7 +748,7 @@ vectToMaybe (x::xs) = Just x
||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
||| ```
public export
catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
catMaybes : (1 xs : Vect n (Maybe elem)) -> (p ** Vect p elem)
catMaybes [] = (_ ** [])
catMaybes (Nothing::xs) = catMaybes xs
catMaybes ((Just j)::xs) =
@ -780,15 +780,22 @@ range {len=S _} = FZ :: map FS range
||| transpose [[1,2], [3,4], [5,6], [7,8]]
||| ```
public export
transpose : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose [] = replicate _ [] -- = [| [] |]
transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
transpose : {n : _} -> (1 array : Vect m (Vect n elem)) -> Vect n (Vect m elem)
transpose [] = replicate _ [] -- = [| [] |]
transpose (x :: xs) = helper x (transpose xs) -- = [| x :: xs |]
where -- Can't use zipWith since it doesn't preserve linearity
helper : (1 _ : Vect a elem)
-> (1 _ : Vect a (Vect b elem))
-> Vect a (Vect (S b) elem)
helper [] [] = []
helper (x::xs) (tl::tls) = (x::tl) :: helper xs tls
--------------------------------------------------------------------------------
-- Applicative/Monad/Traversable
--------------------------------------------------------------------------------
-- These only work if the length is known at run time!
public export
implementation {k : Nat} -> Applicative (Vect k) where
pure = replicate _
fs <*> vs = zipWith apply fs vs

36
libs/contrib/Control/ANSI.idr Normal file
View File

@ -0,0 +1,36 @@
module Control.ANSI
import public Control.ANSI.CSI
import public Control.ANSI.SGR
%default total
public export
record DecoratedString where
constructor MkDString
sgr : List SGR
str : String
export
Show DecoratedString where
show dstr = escapeSGR dstr.sgr ++ dstr.str ++ escapeSGR [Reset]
export
colored : Color -> String -> DecoratedString
colored c = MkDString [SetForeground c]
export
background : Color -> String -> DecoratedString
background c = MkDString [SetBackground c]
export
bolden : String -> DecoratedString
bolden = MkDString [SetStyle Bold]
export
italicize : String -> DecoratedString
italicize = MkDString [SetStyle Italic]
export
underline : String -> DecoratedString
underline = MkDString [SetStyle SingleUnderline]

105
libs/contrib/Control/ANSI/CSI.idr Normal file
View File

@ -0,0 +1,105 @@
module Control.ANSI.CSI
%default total
||| Moves the cursor n columns up.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorUp : Nat -> String
cursorUp n = "\x1B[" ++ show n ++ "A"
export
cursorUp1 : String
cursorUp1 = cursorUp 1
||| Moves the cursor n columns down.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorDown : Nat -> String
cursorDown n = "\x1B[" ++ show n ++ "B"
export
cursorDown1 : String
cursorDown1 = cursorDown 1
||| Moves the cursor n columns forward.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorForward : Nat -> String
cursorForward n = "\x1B[" ++ show n ++ "C"
export
cursorForward1 : String
cursorForward1 = cursorForward 1
||| Moves the cursor n columns back.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorBack : Nat -> String
cursorBack n = "\x1B[" ++ show n ++ "D"
export
cursorBack1 : String
cursorBack1 = cursorBack 1
||| Moves the cursor at the beginning of n lines down.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorNextLine : Nat -> String
cursorNextLine n = "\x1B[" ++ show n ++ "E"
export
cursorNextLine1 : String
cursorNextLine1 = cursorNextLine 1
||| Moves the cursor at the beginning of n lines up.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorPrevLine : Nat -> String
cursorPrevLine n = "\x1B[" ++ show n ++ "F"
export
cursorPrevLine1 : String
cursorPrevLine1 = cursorPrevLine 1
||| Moves the cursor at an arbitrary line and column.
||| Both lines and columns start at 1.
export
cursorMove : (row : Nat) -> (col : Nat) -> String
cursorMove row col = "\x1B[" ++ show row ++ ";" ++ show col ++ "H"
public export
data EraseDirection = Start | End | All
Cast EraseDirection String where
cast Start = "1"
cast End = "0"
cast All = "2"
||| Clears part of the screen.
export
eraseScreen : EraseDirection -> String
eraseScreen to = "\x1B[" ++ cast to ++ "J"
||| Clears part of the line.
export
eraseLine : EraseDirection -> String
eraseLine to = "\x1B[" ++ cast to ++ "K"
||| Scrolls the whole screen up by n lines.
export
scrollUp : Nat -> String
scrollUp n = "\x1B[" ++ show n ++ "S"
export
scrollUp1 : String
scrollUp1 = scrollUp 1
||| Scrolls the whole screen down by n lines.
export
scrollDown : Nat -> String
scrollDown n = "\x1B[" ++ show n ++ "T"
export
scrollDown1 : String
scrollDown1 = scrollDown 1

73
libs/contrib/Control/ANSI/SGR.idr Normal file
View File

@ -0,0 +1,73 @@
module Control.ANSI.SGR
import Data.List
%default total
public export
data Color
= Black | Red | Green | Yellow | Blue | Magenta | Cyan | White
| BrightBlack | BrightRed | BrightGreen | BrightYellow | BrightBlue | BrightMagenta | BrightCyan | BrightWhite
Cast Color String where
cast Black = "0"
cast Red = "1"
cast Green = "2"
cast Yellow = "3"
cast Blue = "4"
cast Magenta = "5"
cast Cyan = "6"
cast White = "7"
cast BrightBlack = "8"
cast BrightRed = "9"
cast BrightGreen = "10"
cast BrightYellow = "11"
cast BrightBlue = "12"
cast BrightMagenta = "13"
cast BrightCyan = "14"
cast BrightWhite = "15"
public export
data Style
= Bold | Faint | NotBoldOrFaint | Italic
| SingleUnderline | DoubleUnderline | NoUnderline
| Striked | NotStriked
Cast Style String where
cast Bold = "1"
cast Faint = "2"
cast NotBoldOrFaint = "22"
cast Italic = "3"
cast SingleUnderline = "4"
cast DoubleUnderline = "21"
cast NoUnderline = "24"
cast Striked = "9"
cast NotStriked = "29"
public export
data Blink = Slow | Rapid | NoBlink
Cast Blink String where
cast Slow = "5"
cast Rapid = "6"
cast NoBlink = "25"
public export
data SGR
= Reset
| SetForeground Color
| SetBackground Color
| SetStyle Style
| SetBlink Blink
||| Returns the ANSI escape code equivalent to the list of operations provided.
export
escapeSGR : List SGR -> String
escapeSGR xs = "\x1B[" ++ concat (intersperse ";" (toCode <$> xs)) ++ "m"
where
toCode : SGR -> String
toCode Reset = "0"
toCode (SetForeground c) = "38;5;" ++ cast c
toCode (SetBackground c) = "48;5;" ++ cast c
toCode (SetStyle s) = cast s
toCode (SetBlink b) = cast b

21
libs/contrib/Control/Monad/Syntax.idr Normal file
View File

@ -0,0 +1,21 @@
module Control.Monad.Syntax
%default total
infixr 1 =<<, <=<, >=>
||| Left-to-right Kleisli composition of monads.
public export
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>=>) f g = \x => f x >>= g
public export
||| Right-to-left Kleisli composition of monads, flipped version of `>=>`.
(<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
(<=<) = flip (>=>)
public export
||| Right-to-left monadic bind, flipped version of `>>=`.
(=<<) : Monad m => (a -> m b) -> m a -> m b
(=<<) = flip (>>=)

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

@ -24,18 +24,18 @@ consCong2 Refl Refl = Refl
||| Equal non-empty lists should result in equal components after destructuring 'snoc'.
export
snocCong2 : {x : a} -> {xs : List a} -> {y : a} -> {ys : List a} ->
snocInjective : {x : a} -> {xs : List a} -> {y : a} -> {ys : List a} ->
(xs `snoc` x) = (ys `snoc` y) -> (xs = ys, x = y)
snocCong2 {xs = []} {ys = []} Refl = (Refl, Refl)
snocCong2 {xs = []} {ys = z :: zs} prf =
snocInjective {xs = []} {ys = []} Refl = (Refl, Refl)
snocInjective {xs = []} {ys = z :: zs} prf =
let nilIsSnoc = snd $ consInjective {xs = []} {ys = zs ++ [y]} prf
in void $ snocNonEmpty (sym nilIsSnoc)
snocCong2 {xs = z :: xs} {ys = []} prf =
snocInjective {xs = z :: xs} {ys = []} prf =
let snocIsNil = snd $ consInjective {x = z} {xs = xs ++ [x]} {ys = []} prf
in void $ snocNonEmpty snocIsNil
snocCong2 {xs = w :: xs} {ys = z :: ys} prf =
snocInjective {xs = w :: xs} {ys = z :: ys} prf =
let (wEqualsZ, xsSnocXEqualsYsSnocY) = consInjective prf
(xsEqualsYS, xEqualsY) = snocCong2 xsSnocXEqualsYsSnocY
(xsEqualsYS, xEqualsY) = snocInjective xsSnocXEqualsYsSnocY
in (consCong2 wEqualsZ xsEqualsYS, xEqualsY)
||| Appending pairwise equal lists gives equal lists

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

@ -45,7 +45,7 @@ reversePalindromeEqualsLemma x x' xs prf = equateInnerAndOuter flipHeadX
: reverse (xs ++ [x']) ++ [x] = (x :: xs) ++ [x']
-> (reverse xs = xs, x = x')
equateInnerAndOuter prf =
let (prf', xEqualsX') = snocCong2 prf
let (prf', xEqualsX') = snocInjective prf
in (cancelOuter prf', xEqualsX')
||| Only Palindromes are equal to their own reverse.

33
libs/contrib/Data/String/Interpolation.idr Normal file
View File

@ -0,0 +1,33 @@
||| A DYI version of 'string interpolation', mimicking Python 3's 'f-string' syntax
||| Not as fancy
module Data.String.Interpolation
import Data.Strings
namespace Data.String.Interpolation.Basic
%inline
public export
F : List String -> String
F strs = concat (strs)
namespace Data.String.Interpolation.Nested
%inline
public export
F : List (List String) -> String
F strss = F (concat strss)
{- Examples:
fstring : String
fstring = let apples = "apples" in
F["I have some ", apples," here."] --- cf. f"I have some {apples} here."
multiline : String
multiline = let name = "Edwin"
profession = "Hacker"
affiliation = "the University of St. Andrews" in --- cf.
F [["Hi ",name,". " ] --- f"Hi {name}. " \
,["You are a ",profession,". "] --- f"You are a {profession}. " \
,["You were in ",affiliation,"."] --- f"You were in {affiliation}."
]
-}

7
libs/contrib/contrib.ipkg
View File

@ -1,7 +1,11 @@
package contrib
modules = Control.Delayed,
modules = Control.ANSI,
Control.ANSI.SGR,
Control.ANSI.CSI,
Control.Delayed,
Control.Linear.LIO,
Control.Monad.Syntax,
Data.Linear.Array,
@ -24,6 +28,7 @@ modules = Control.Delayed,
Data.SortedMap,
Data.SortedSet,
Data.String.Extra,
Data.String.Interpolation,
Debug.Buffer,

8
libs/prelude/Builtin.idr
View File

@ -174,3 +174,11 @@ believe_me = prim__believe_me _ _
export partial
idris_crash : String -> a
idris_crash = prim__crash _
public export
delay : a -> Lazy a
delay x = Delay x
public export
force : Lazy a -> a
force x = Force x

21
samples/BTree.idr Normal file
View File

@ -0,0 +1,21 @@
module BTree
public export
data BTree a = Leaf
| Node (BTree a) a (BTree a)
export
insert : Ord a => a -> BTree a -> BTree a
insert x Leaf = Node Leaf x Leaf
insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
else (Node l v (insert x r))
export
toList : BTree a -> List a
toList Leaf = []
toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r)
export
toTree : Ord a => List a -> BTree a
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)

14
samples/FFI-readline/Test/ReadHistory.idr Normal file
View File

@ -0,0 +1,14 @@
import Text.Readline
echoLoop : IO ()
echoLoop
= do Just x <- readline "> "
| Nothing => putStrLn "EOF"
putStrLn ("Read: " ++ x)
when (x /= "") $ addHistory x
if x /= "quit"
then echoLoop
else putStrLn "Done"
main : IO ()
main = echoLoop

19
samples/FFI-readline/Test/ReadTab.idr Normal file
View File

@ -0,0 +1,19 @@
import Text.Readline
testComplete : String -> Int -> IO (Maybe String)
testComplete text 0 = pure $ Just "hamster"
testComplete text 1 = pure $ Just "bar"
testComplete text st = pure Nothing
loop : IO ()
loop = do Just x <- readline "> "
| Nothing => putStrLn "EOF"
putStrLn x
when (x /= "") $ addHistory x
if x /= "quit"
then loop
else putStrLn "Done"
main : IO ()
main = do setCompletionFn testComplete
loop

3
samples/FFI-readline/Test/test.ipkg Normal file
View File

@ -0,0 +1,3 @@
package test
opts = "-p readline"

10
samples/FFI-readline/readline.ipkg Normal file
View File

@ -0,0 +1,10 @@
package readline
sourcedir = "src"
modules = Text.Readline
prebuild = "make -C readline_glue"
postinstall = "make -C readline_glue install"
postclean = "make -C readline_glue clean"

7
samples/FFI-readline/readline_glue/.gitignore vendored Normal file
View File

@ -0,0 +1,7 @@
*.d
*.o
*.obj
*.so
*.dylib
*.dll

40
samples/FFI-readline/readline_glue/Makefile Normal file
View File

@ -0,0 +1,40 @@
include ../../../config.mk
IDRIS := idris2
INSTALLDIR = `${IDRIS} --libdir`/readline/lib
TARGET = libidrisreadline
LDFLAGS += -lreadline
SRCS = $(wildcard *.c)
OBJS = $(SRCS:.c=.o)
DEPS = $(OBJS:.o=.d)
all: $(TARGET)$(SHLIB_SUFFIX)
$(TARGET)$(SHLIB_SUFFIX): $(OBJS)
$(CC) -shared $(LDFLAGS) -o $@ $^
-include $(DEPS)
%.d: %.c
@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@
.PHONY: clean
clean :
rm -f $(OBJS) $(TARGET)$(SHLIB_SUFFIX)
cleandep: clean
rm -f $(DEPS)
.PHONY: install
install:
@if ! [ -d $(INSTALLDIR) ]; then mkdir -p $(INSTALLDIR); fi
install $(TARGET)$(SHLIB_SUFFIX) $(wildcard *.h) $(INSTALLDIR)

38
samples/FFI-readline/readline_glue/idris_readline.c Normal file
View File

@ -0,0 +1,38 @@
#include <readline/readline.h>
#include <string.h>
#include <stdlib.h>
rl_compentry_func_t* my_compentry;
char* compentry_wrapper(const char* text, int i) {
char* res = my_compentry(text, i); // Idris frees this
if (res != NULL) {
char* comp = malloc(strlen(res)+1); // Readline frees this
strcpy(comp, res);
return comp;
}
else {
return NULL;
}
}
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
rl_completion_entry_function = compentry_wrapper;
my_compentry = fn;
}
char* getString(void* str) {
return (char*)str;
}
void* mkString(char* str) {
return (void*)str;
}
void* nullString() {
return NULL;
}
int isNullString(void* str) {
return str == NULL;
}

11
samples/FFI-readline/readline_glue/idris_readline.h Normal file
View File

@ -0,0 +1,11 @@
#ifndef _IDRIS_READLINE_H
#define _IDRIS_READLINE_H
void idrisrl_setCompletion(rl_completion_func_t* fn);
char* getString(void* str);
void* mkString(char* str);
void* nullString();
int isNullString(void* str);
#endif

53
samples/FFI-readline/src/Text/Readline.idr Normal file
View File

@ -0,0 +1,53 @@
module Text.Readline
rlib : String -> String
rlib fn = "C:" ++ fn ++ ",libidrisreadline"
%foreign (rlib "getString")
export
getString : Ptr String -> String
%foreign (rlib "mkString")
export
mkString : String -> Ptr String
%foreign (rlib "nullString")
export
nullString : Ptr String
%foreign (rlib "isNullString")
prim_isNullString : Ptr String -> Int
export
isNullString : Ptr String -> Bool
isNullString str = if prim_isNullString str == 0 then False else True
%foreign (rlib "readline")
prim_readline : String -> PrimIO (Ptr String)
export
readline : HasIO io => String -> io (Maybe String)
readline s
= do mstr <- primIO $ prim_readline s
if isNullString mstr
then pure $ Nothing
else pure $ Just (getString mstr)
%foreign (rlib "add_history")
prim_add_history : String -> PrimIO ()
export
addHistory : HasIO io => String -> io ()
addHistory s = primIO $ prim_add_history s
%foreign (rlib "idrisrl_setCompletion")
prim_setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()
export
setCompletionFn : HasIO io => (String -> Int -> IO (Maybe String)) -> io ()
setCompletionFn fn
= primIO $ prim_setCompletion $ \s, i => toPrim $
do mstr <- fn s i
case mstr of
Nothing => pure nullString
Just str => pure (mkString str)

57
samples/Interp.idr Normal file
View File

@ -0,0 +1,57 @@
import Data.Vect
data Ty = TyInt | TyBool | TyFun Ty Ty
interpTy : Ty -> Type
interpTy TyInt = Integer
interpTy TyBool = Bool
interpTy (TyFun a t) = interpTy a -> interpTy t
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
Stop : HasType FZ (t :: ctxt) t
Pop : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
data Expr : Vect n Ty -> Ty -> Type where
Var : HasType i ctxt t -> Expr ctxt t
Val : (x : Integer) -> Expr ctxt TyInt
Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
Op : (interpTy a -> interpTy b -> interpTy c) ->
Expr ctxt a -> Expr ctxt b -> Expr ctxt c
If : Expr ctxt TyBool ->
Lazy (Expr ctxt a) ->
Lazy (Expr ctxt a) -> Expr ctxt a
data Env : Vect n Ty -> Type where
Nil : Env Nil
(::) : interpTy a -> Env ctxt -> Env (a :: ctxt)
lookup : HasType i ctxt t -> Env ctxt -> interpTy t
lookup Stop (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs
interp : Env ctxt -> Expr ctxt t -> interpTy t
interp env (Var i) = lookup i env
interp env (Val x) = x
interp env (Lam sc) = \x => interp (x :: env) sc
interp env (App f s) = interp env f (interp env s)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e) = if interp env x then interp env t
else interp env e
add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
fact : Expr ctxt (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var Stop) (Val 0))
(Val 1)
(Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
(Var Stop)))
main : IO ()
main = do putStr "Enter a number: "
x <- getLine
printLn (interp [] fact (cast x))

36
samples/InterpE.idr Normal file
View File

@ -0,0 +1,36 @@
module InterpE
data Expr = Var String -- variables
| Val Int -- values
| Add Expr Expr -- addition
data Eval : Type -> Type where
MkEval : (List (String, Int) -> Maybe a) -> Eval a
fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
fetchVal : List (String, Int) -> Maybe Int
fetchVal [] = Nothing
fetchVal ((v, val) :: xs) = if (x == v)
then (Just val)
else (fetchVal xs)
Functor Eval where
map f (MkEval g) = MkEval (\e => map f (g e))
Applicative Eval where
pure x = MkEval (\e => Just x)
(<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
app : Maybe (a -> b) -> Maybe a -> Maybe b
app (Just fx) (Just gx) = Just (fx gx)
app _ _ = Nothing
eval : Expr -> Eval Int
eval (Var x) = fetch x
eval (Val x) = [| x |]
eval (Add x y) = [| eval x + eval y |]
runEval : List (String, Int) -> Expr -> Maybe Int
runEval env e = case eval e of
MkEval envFn => envFn env

10
samples/MyOrd.idr Normal file
View File

@ -0,0 +1,10 @@
import Data.List
[myord] Ord Nat where
compare Z (S n) = GT
compare (S n) Z = LT
compare Z Z = EQ
compare (S x) (S y) = compare @{myord} x y
testList : List Nat
testList = [3,4,1]

11
samples/NamedSemi.idr Normal file
View File

@ -0,0 +1,11 @@
[PlusNatSemi] Semigroup Nat where
(<+>) x y = x + y
[MultNatSemi] Semigroup Nat where
(<+>) x y = x * y
[PlusNatMonoid] Monoid Nat using PlusNatSemi where
neutral = 0
[MultNatMonoid] Monoid Nat using MultNatSemi where
neutral = 1

13
samples/Prims.idr Normal file
View File

@ -0,0 +1,13 @@
module Prims
x : Int
x = 94
foo : String
foo = "Sausage machine"
bar : Char
bar = 'Z'
quux : Bool
quux = False

29
samples/Proofs.idr Normal file
View File

@ -0,0 +1,29 @@
fiveIsFive : 5 = 5
fiveIsFive = Refl
twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl
-- twoPlusTwoBad : 2 + 2 = 5
-- twoPlusTwoBad = Refl
disjoint : (n : Nat) -> Z = S n -> Void
disjoint n prf = replace {p = disjointTy} prf ()
where
disjointTy : Nat -> Type
disjointTy Z = ()
disjointTy (S k) = Void
plusReduces : (n:Nat) -> plus Z n = n
plusReduces n = Refl
plusReducesR : (n:Nat) -> plus n Z = n
plusReducesR n = Refl
plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong S (plusReducesZ k)
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = Refl
plusReducesS (S k) m = cong S (plusReducesS k m)

40
samples/Vect.idr Normal file
View File

@ -0,0 +1,40 @@
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ ys
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
index : Fin n -> Vect n a -> a
index FZ (x :: xs) = x
index (FS k) (x :: xs) = index k xs
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter p Nil = (_ ** [])
filter p (x :: xs)
= case filter p xs of
(_ ** xs') => if p x then (_ ** x :: xs')
else (_ ** xs')
cons : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
cons val xs
= record { fst = S (fst xs),
snd = (val :: snd xs) } xs
cons' : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
cons' val
= record { fst $= S,
snd $= (val ::) }
Show a => Show (Vect n a) where
show xs = "[" ++ show' xs ++ "]" where
show' : forall n . Vect n a -> String
show' Nil = ""
show' (x :: Nil) = show x
show' (x :: xs) = show x ++ ", " ++ show' xs

11
samples/Void.idr Normal file
View File

@ -0,0 +1,11 @@
module Void
-- making use of 'hd' being partially defined
empty1 : Void
empty1 = hd [] where
hd : List a -> a
hd (x :: xs) = x
-- not terminating
empty2 : Void
empty2 = empty2

47
samples/With.idr Normal file
View File

@ -0,0 +1,47 @@
import Data.Vect
import Data.Nat
my_filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
my_filter p [] = ( _ ** [] )
my_filter p (x :: xs) with (filter p xs)
my_filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
foo : Int -> Int -> Bool
foo n m with (n + 1)
foo _ m | 2 with (m + 1)
foo _ _ | 2 | 3 = True
foo _ _ | 2 | _ = False
foo _ _ | _ = False
data Parity : Nat -> Type where
Even : {n : _} -> Parity (n + n)
Odd : {n : _} ->Parity (S (n + n))
-- parity : (n : Nat) -> Parity n
-- parity Z = Even {n = Z}
-- parity (S Z) = Odd {n = Z}
-- parity (S (S k)) with (parity k)
-- parity (S (S (j + j))) | Even
-- = rewrite plusSuccRightSucc j j in Even {n = S j}
-- parity (S (S (S (j + j)))) | Odd
-- = rewrite plusSuccRightSucc j j in Odd {n = S j}
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p
parity : (n:Nat) -> Parity n
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})
parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})
natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
natToBin (j + j) | Even = False :: natToBin j
natToBin (S (j + j)) | Odd = True :: natToBin j

7
samples/bmain.idr Normal file
View File

@ -0,0 +1,7 @@
module Main
import BTree
main : IO ()
main = do let t = toTree [1,8,2,7,9,3]
print (BTree.toList t)

25
samples/deprec.idr Normal file
View File

@ -0,0 +1,25 @@
import Data.Vect
record Person where
constructor MkPerson
firstName, middleName, lastName : String
age : Int
record SizedClass (size : Nat) where
constructor SizedClassInfo
students : Vect size Person
className : String
record Class where
constructor ClassInfo
students : Vect n Person
className : String
addStudent : Person -> Class -> Class
addStudent p c = record { students = p :: students c } c
addStudent' : Person -> SizedClass n -> SizedClass (S n)
addStudent' p c = SizedClassInfo (p :: students c) (className c)
addStudent'' : Person -> SizedClass n -> SizedClass (S n)
addStudent'' p c = record { students = p :: students c } c

5
samples/dummy.ipkg Normal file
View File

@ -0,0 +1,5 @@
-- This is just so the above Idris 1 ipkg doesn't interfere with the
-- interactive editing modes for the Idris 2 code here!
package dummy

13
samples/fctypes.idr Normal file
View File

@ -0,0 +1,13 @@
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs

40
samples/ffi/Small.idr Normal file
View File

@ -0,0 +1,40 @@
libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmall"
%foreign (libsmall "add")
add : Int -> Int -> Int
%foreign (libsmall "addWithMessage")
prim_addWithMessage : String -> Int -> Int -> PrimIO Int
addWithMessage : String -> Int -> Int -> IO Int
addWithMessage s x y = primIO $ prim_addWithMessage s x y
%foreign (libsmall "applyFn")
prim_applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String
applyFn : String -> Int -> (String -> Int -> String) -> IO String
applyFn c i f = primIO $ prim_applyFn c i f
%foreign (libsmall "applyFn")
prim_applyFnIO : String -> Int -> (String -> Int -> PrimIO String) -> PrimIO String
applyFnIO : String -> Int -> (String -> Int -> IO String) -> IO String
applyFnIO c i f = primIO $ prim_applyFnIO c i (\s, i => toPrim $ f s i)
pluralise : String -> Int -> IO String
pluralise str x
= do putStrLn "Pluralising"
pure $ show x ++ " " ++
if x == 1
then str
else str ++ "s"
main : IO ()
main
= do -- printLn (add 70 24)
-- primIO $ prim_addWithMessage "Sum" 70 24
str1 <- applyFnIO "Biscuit" 10 pluralise
putStrLn str1
str2 <- applyFnIO "Tree" 1 pluralise
putStrLn str2

29
samples/ffi/Struct.idr Normal file
View File

@ -0,0 +1,29 @@
import System.FFI
libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmall"
Point : Type
Point = Struct "point" [("x", Int), ("y", Int)]
%foreign (libsmall "mkPoint")
mkPoint : Int -> Int -> Point
%foreign (libsmall "freePoint")
prim_freePoint : Point -> PrimIO ()
freePoint : Point -> IO ()
freePoint p = primIO $ prim_freePoint p
showPoint : Point -> String
showPoint pt
= let x : Int = getField pt "x"
y : Int = getField pt "y" in
show (x, y)
main : IO ()
main
= do let pt = mkPoint 20 30
setField pt "x" (the Int 40)
putStrLn $ showPoint pt
freePoint pt

4
samples/ffi/args.idr Normal file
View File

@ -0,0 +1,4 @@
import System
main : IO ()
main = printLn !getArgs

5
samples/ffi/dummy.ipkg Normal file
View File

@ -0,0 +1,5 @@
-- This is just so the above Idris 1 ipkg doesn't interfere with the
-- interactive editing modes for the Idris 2 code here!
package dummy

39
samples/ffi/smallc.c Normal file
View File

@ -0,0 +1,39 @@
#include <stdlib.h>
#include <stdio.h>
int add(int x, int y) {
return x+y;
}
int addWithMessage(char* msg, int x, int y) {
printf("%s: %d + %d = %d\n", msg, x, y, x+y);
return x+y;
}
typedef char*(*StringFn)(char*, int);
char* applyFn(char* x, int y, StringFn f) {
printf("Applying callback to %s %d\n", x, y);
return f(x, y);
}
char* applyFnPure(char* x, int y, StringFn f) {
return f(x, y);
}
typedef struct {
int x;
int y;
} point;
point* mkPoint(int x, int y) {
point* pt = malloc(sizeof(point));
pt->x = x;
pt->y = y;
return pt;
}
void freePoint(point* pt) {
free(pt);
}

6
samples/holes.idr Normal file
View File

@ -0,0 +1,6 @@
main : IO ()
main = putStrLn ?greeting
even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs

4
samples/io.idr Normal file
View File

@ -0,0 +1,4 @@
greet : IO ()
greet = do putStr "What is your name? "
name <- getLine
putStrLn ("Hello " ++ name)

3
samples/listcomp.idr Normal file
View File

@ -0,0 +1,3 @@
pythag : Int -> List (Int, Int, Int)
pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
x*x + y*y == z*z ]

22
samples/multiplicity.idr Normal file
View File

@ -0,0 +1,22 @@
import Data.Vect
append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs
data DoorState = Open | Closed
data Door : DoorState -> Type where
MkDoor : (doorId : Int) -> Door st
openDoor : (1 d : Door Closed) -> Door Open
closeDoor : (1 d : Door Open) -> Door Closed
newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()
deleteDoor : (1 d : Door Closed) -> IO ()
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d' = openDoor d
d'' = closeDoor d' in
deleteDoor d''

12
samples/params.idr Normal file
View File

@ -0,0 +1,12 @@
import Data.Vect
parameters (x : Nat, y : Nat)
addAll : Nat -> Nat
addAll z = x + y + z
parameters (y : Nat, xs : Vect x a)
data Vects : Type -> Type where
MkVects : Vect y a -> Vects a
append : Vects a -> Vect (x + y) a
append (MkVects ys) = xs ++ ys

17
samples/proofs/induction.idr Normal file
View File

@ -0,0 +1,17 @@
nat_induction :
(prop : Nat -> Type) -> -- Property to show
(prop Z) -> -- Base case
((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step
(x : Nat) -> -- Show for all x
prop x
nat_induction prop p_Z p_S Z = p_Z
nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)
plus_ind : Nat -> Nat -> Nat
plus_ind n m
= nat_induction (\x => Nat)
m -- Base case, plus_ind Z m
(\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
-- where k_rec = plus_ind k m
n

17
samples/proofs/pluscomm.idr Normal file
View File

@ -0,0 +1,17 @@
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k)
= let rec = plus_commutes_Z k in
rewrite sym rec in Refl
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
plus_commutes_S k Z = Refl
plus_commutes_S k (S j)
= rewrite plus_commutes_S k j in Refl
total
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = plus_commutes_Z m
plus_commutes (S k) m
= rewrite plus_commutes k m in
plus_commutes_S k m

4
samples/proofs/plusprops.idr Normal file
View File

@ -0,0 +1,4 @@
plus_commutes : (n, m : Nat) -> plus n m = plus m n
plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p

21
samples/proofs/prfintro.idr Normal file
View File

@ -0,0 +1,21 @@
import Data.Vect
four_eq : 4 = 4
four_eq = Refl
-- four_eq_five : 4 = 5
-- four_eq_five = Refl
twoplustwo_eq_four : 2 + 2 = 4
twoplustwo_eq_four = Refl
plus_reduces_Z : (m : Nat) -> plus Z m = m
plus_reduces_Z m = Refl
plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
plus_reduces_Sk k m = Refl
idris_not_php : Z = "Z"
vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> n = m
vect_eq_length xs xs Refl = Refl

5
samples/proofs/proof.ipkg Normal file
View File

@ -0,0 +1,5 @@
-- This is just so the above ipkg doesn't interfere with the
-- interactive editing modes for the Idris 2 code here!
package proof

26
samples/wheres.idr Normal file
View File

@ -0,0 +1,26 @@
foo : Int -> Int
foo x = case isLT of
Yes => x*2
No => x*4
where
data MyLT = Yes | No
isLT : MyLT
isLT = if x < 20 then Yes else No
even : Nat -> Bool
even Z = True
even (S k) = odd k where
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
test : List Nat
test = [c (S 1), c Z, d (S Z)]
where c : Nat -> Nat
c x = 42 + x
d : Nat -> Nat
d y = c (y + 1 + z y)
where z : Nat -> Nat
z w = y + w

10
src/Core/AutoSearch.idr
View File

@ -51,7 +51,7 @@ mkArgs fc rigc env (NBind nfc x (Pi c p ty) sc)
argTy <- quote empty env ty
let argRig = rigMult rigc c
(idx, arg) <- newMeta fc argRig env nm argTy
(Hole (length env) False) False
(Hole (length env) (holeInit False)) False
setInvertible fc (Resolved idx)
(rest, restTy) <- mkArgs fc rigc env
!(sc defs (toClosure defaultOpts env arg))
@ -456,12 +456,16 @@ concreteDets {vars} fc defaults env top pos dets (arg :: args)
concrete defs argnf False) args
pure ()
concrete defs (NApp _ (NMeta n i _) _) True
= do Just (Hole _ True) <- lookupDefExact n (gamma defs)
= do Just (Hole _ b) <- lookupDefExact n (gamma defs)
| _ => throw (DeterminingArg fc n i [] top)
when (not (implbind b)) $
throw (DeterminingArg fc n i [] top)
pure ()
concrete defs (NApp _ (NMeta n i _) _) False
= do Just (Hole _ True) <- lookupDefExact n (gamma defs)
= do Just (Hole _ b) <- lookupDefExact n (gamma defs)
| def => throw (CantSolveGoal fc [] top)
when (not (implbind b)) $
throw (CantSolveGoal fc [] top)
pure ()
concrete defs tm atTop = pure ()

2
src/Core/Binary.idr
View File

@ -30,7 +30,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 34
ttcVersion = 35
export
checkTTCVersion : String -> Int -> Int -> Core ()

14
src/Core/Context.idr
View File

@ -49,6 +49,16 @@ export
defaultFlags : TypeFlags
defaultFlags = MkTypeFlags False False
public export
record HoleFlags where
constructor MkHoleFlags
implbind : Bool -- stands for an implicitly bound name
precisetype : Bool -- don't generalise multiplicities when instantiating
export
holeInit : Bool -> HoleFlags
holeInit b = MkHoleFlags b False
public export
data Def : Type where
None : Def -- Not yet defined
@ -92,7 +102,7 @@ data Def : Type where
Def
Hole : (numlocs : Nat) -> -- Number of locals in scope at binding point
-- (mostly to help display)
(implbind : Bool) -> -- Does this stand for an implicitly bound name
HoleFlags ->
Def
BySearch : RigCount -> (maxdepth : Nat) -> (defining : Name) -> Def
-- Constraints are integer references into the current map of
@ -124,7 +134,7 @@ Show Def where
show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++
" " ++ show cs ++">"
show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
show (Hole _ p) = "Hole" ++ if p then " [impl]" else ""
show (Hole _ p) = "Hole" ++ if implbind p then " [impl]" else ""
show (BySearch c depth def) = "Search in " ++ show def
show (Guess tm _ cs) = "Guess " ++ show tm ++ " when " ++ show cs
show ImpBind = "Bound name"

4
src/Core/TTC.idr
View File

@ -826,7 +826,7 @@ TTC Def where
toBuf b detpos; toBuf b u; toBuf b ms; toBuf b datacons
toBuf b dets
toBuf b (Hole locs p)
= do tag 6; toBuf b locs; toBuf b p
= do tag 6; toBuf b locs; toBuf b (implbind p)
toBuf b (BySearch c depth def)
= do tag 7; toBuf b c; toBuf b depth; toBuf b def
toBuf b (Guess guess envb constraints)
@ -857,7 +857,7 @@ TTC Def where
pure (TCon t a ps dets u ms cs detags)
6 => do l <- fromBuf b
p <- fromBuf b
pure (Hole l p)
pure (Hole l (holeInit p))
7 => do c <- fromBuf b; depth <- fromBuf b
def <- fromBuf b
pure (BySearch c depth def)

45
src/Core/Unify.idr
View File

@ -505,6 +505,12 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
addDef (Resolved mref) newdef
removeHole mref
where
precise : Bool
precise
= case definition mdef of
Hole _ p => precisetype p
_ => False
isSimple : Term vs -> Bool
isSimple (Local _ _ _ _) = True
isSimple (Ref _ _ _) = True
@ -561,7 +567,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
= do p' <- updateIVarsPi ivs p
if isLinear rig
then do t' <- updateIVars ivs t
pure $ if inLam mode
pure $ if inLam mode || precise
then (Pi linear p' t')
else (Pi top p' t')
else Just (Pi rig p' !(updateIVars ivs t))
@ -662,18 +668,22 @@ mutual
headsConvert : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
Env Term vars ->
{auto u : Ref UST UState} ->
UnifyInfo ->
FC -> Env Term vars ->
Maybe (List (NF vars)) -> Maybe (List (NF vars)) ->
Core Bool
headsConvert env (Just vs) (Just ns)
headsConvert mode fc env (Just vs) (Just ns)
= case (reverse vs, reverse ns) of
(v :: _, n :: _) =>
do logNF 10 "Converting" env v
logNF 10 "......with" env n
defs <- get Ctxt
convert defs env v n
do logNF 10 "Unifying head" env v
logNF 10 ".........with" env n
res <- unify mode fc env v n
-- If there's constraints, we postpone the whole equation
-- so no need to record them
pure (isNil (constraints res ))
_ => pure False
headsConvert env _ _
headsConvert mode fc env _ _
= do log 10 "Nothing to convert"
pure True
@ -701,7 +711,7 @@ mutual
nty
-- If the rightmost arguments have the same type, or we don't
-- know the types of the arguments, we'll get on with it.
if !(headsConvert env vargTys nargTys)
if !(headsConvert mode fc env vargTys nargTys)
then
-- Unify the rightmost arguments, with the goal of turning the
-- hole application into a pattern form
@ -1271,9 +1281,14 @@ mutual
unifyWithLazyD _ _ mode loc env (NDelayed _ _ tmx) (NDelayed _ _ tmy)
= unify (lower mode) loc env tmx tmy
unifyWithLazyD _ _ mode loc env (NDelayed _ r tmx) tmy
= do vs <- unify (lower mode) loc env tmx tmy
pure (record { addLazy = AddForce r } vs)
unifyWithLazyD _ _ mode loc env x@(NDelayed _ r tmx) tmy
= if isHoleApp tmy && not (umode mode == InMatch)
-- given type delayed, expected unknown, so let's wait and see
-- what the expected type turns out to be
then postpone True
loc mode "Postponing in lazy" env x tmy
else do vs <- unify (lower mode) loc env tmx tmy
pure (record { addLazy = AddForce r } vs)
unifyWithLazyD _ _ mode loc env tmx (NDelayed _ r tmy)
= do vs <- unify (lower mode) loc env tmx tmy
pure (record { addLazy = AddDelay r } vs)
@ -1430,7 +1445,7 @@ retryGuess mode smode (hid, (loc, hname))
do logTerm 5 ("Failed (det " ++ show hname ++ " " ++ show n ++ ")")
(type def)
setInvertible loc (Resolved i)
pure False -- progress made!
pure False -- progress not made yet!
_ => do logTermNF 5 ("Search failed at " ++ show rig ++ " for " ++ show hname)
[] (type def)
case smode of
@ -1526,9 +1541,9 @@ giveUpConstraints
= do defs <- get Ctxt
case !(lookupDefExact (Resolved hid) (gamma defs)) of
Just (BySearch _ _ _) =>
updateDef (Resolved hid) (const (Just (Hole 0 False)))
updateDef (Resolved hid) (const (Just (Hole 0 (holeInit False))))
Just (Guess _ _ _) =>
updateDef (Resolved hid) (const (Just (Hole 0 False)))
updateDef (Resolved hid) (const (Just (Hole 0 (holeInit False))))
_ => pure ()
-- Check whether any of the given hole references have the same solution

2
src/Core/UnifyState.idr
View File

@ -674,7 +674,7 @@ dumpHole lvl hole
(Hole _ p, ty) =>
log lvl $ "?" ++ show (fullname gdef) ++ " : " ++
show !(normaliseHoles defs [] ty)
++ if p then " (ImplBind)" else ""
++ if implbind p then " (ImplBind)" else ""
++ if invertible gdef then " (Invertible)" else ""
(BySearch _ _ _, ty) =>
log lvl $ "Search " ++ show hole ++ " : " ++

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

@ -182,7 +182,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- 2. Elaborate top level function types for this interface
defs <- get Ctxt
fns <- topMethTypes [] impName methImps impsp (params cdata)
fns <- topMethTypes [] impName methImps impsp
(implParams cdata) (params cdata)
(map fst (methods cdata))
(methods cdata)
traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)
@ -316,11 +317,11 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- in later method types (specifically, putting implicits in)
topMethType : List (Name, RawImp) ->
Name -> List (Name, RigCount, RawImp) ->
List String -> List Name -> List Name ->
List String -> List Name -> List Name -> List Name ->
(Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp),
List (Name, RawImp))
topMethType methupds impName methImps impsp pnames allmeths (mn, c, treq, (d, mty_in))
topMethType methupds impName methImps impsp imppnames pnames allmeths (mn, c, treq, (d, mty_in))
= do -- Get the specialised type by applying the method to the
-- parameters
n <- inCurrentNS (methName mn)
@ -335,9 +336,23 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- parameters are passed through to any earlier methods which
-- appear in the type
let mty_in = substNames vars methupds mty_in
-- Substitute _ in for the implicit parameters, then
-- substitute in the explicit parameters.
let mty_iparams
= substBindVars vars
(map (\n => (n, Implicit fc False)) imppnames)
mty_in
let mty_params
= substNames vars (zip pnames ps) mty_iparams
log 5 $ "Substitute implicits " ++ show imppnames ++
" parameters " ++ show (zip pnames ps) ++
" " ++ show mty_in ++ " is " ++
show mty_params
let mbase = bindImps methImps $
bindConstraints fc AutoImplicit cons $
substNames vars (zip pnames ps) mty_in
mty_params
let ibound = findImplicits mbase
mty <- bindTypeNamesUsed ibound vars mbase
@ -358,13 +373,14 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
topMethTypes : List (Name, RawImp) ->
Name -> List (Name, RigCount, RawImp) ->
List String -> List Name -> List Name ->
List String ->
List Name -> List Name -> List Name ->
List (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
Core (List (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp))
topMethTypes upds impName methImps impsp pnames allmeths [] = pure []
topMethTypes upds impName methImps impsp pnames allmeths (m :: ms)
= do (m', newupds) <- topMethType upds impName methImps impsp pnames allmeths m
ms' <- topMethTypes (newupds ++ upds) impName methImps impsp pnames allmeths ms
topMethTypes upds impName methImps impsp imppnames pnames allmeths [] = pure []
topMethTypes upds impName methImps impsp imppnames pnames allmeths (m :: ms)
= do (m', newupds) <- topMethType upds impName methImps impsp imppnames pnames allmeths m
ms' <- topMethTypes (newupds ++ upds) impName methImps impsp imppnames pnames allmeths ms
pure (m' :: ms')
mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl

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

@ -7,6 +7,7 @@ import Core.Env
import Core.Metadata
import Core.TT
import Core.Unify
import Core.Value
import Idris.Resugar
import Idris.Syntax
@ -230,13 +231,13 @@ mkCon loc n
updateIfaceSyn : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Name -> Name -> List Name -> List RawImp ->
Name -> Name -> List Name -> List Name -> List RawImp ->
List (Name, RigCount, List FnOpt, (Bool, RawImp)) -> List (Name, List ImpClause) ->
Core ()
updateIfaceSyn iname cn ps cs ms ds
updateIfaceSyn iname cn impps ps cs ms ds
= do syn <- get Syn
ms' <- traverse totMeth ms
let info = MkIFaceInfo cn ps cs ms' ds
let info = MkIFaceInfo cn impps ps cs ms' ds
put Syn (record { ifaces $= addName iname info } syn)
where
findSetTotal : List FnOpt -> Maybe TotalReq
@ -250,6 +251,13 @@ updateIfaceSyn iname cn ps cs ms ds
= do let treq = findSetTotal opts
pure (n, c, treq, t)
-- Read the implicitly added parameters from an interface type, so that we
-- know to substitute an implicit in when defining the implementation
getImplParams : Term vars -> List Name
getImplParams (Bind _ n (Pi _ Implicit _) sc)
= n :: getImplParams sc
getImplParams _ = []
export
elabInterface : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -267,6 +275,7 @@ elabInterface : {vars : _} ->
Core ()
elabInterface {vars} fc vis env nest constraints iname params dets mcon body
= do fullIName <- getFullName iname
ns_iname <- inCurrentNS fullIName
let conName_in = maybe (mkCon fc fullIName) id mcon
-- Machine generated names need to be qualified when looking them up
conName <- inCurrentNS conName_in
@ -282,9 +291,13 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
ns_meths <- traverse (\mt => do n <- inCurrentNS (fst mt)
pure (n, snd mt)) meth_decls
ns_iname <- inCurrentNS fullIName
defs <- get Ctxt
Just ty <- lookupTyExact ns_iname (gamma defs)
| Nothing => throw (UndefinedName fc iname)
let implParams = getImplParams ty
updateIfaceSyn ns_iname conName
(map fst params) (map snd constraints)
implParams (map fst params) (map snd constraints)
ns_meths ds
where
nameCons : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp)

27
src/Idris/IDEMode/MakeClause.idr
View File

@ -52,3 +52,30 @@ makeWith n srcline
mkWithPat mark indent lhs
= pref mark (indent + 2) ++ lhs ++ "| with_pat = ?" ++
showRHSName n ++ "_rhs"
export
makeCase : Bool -> Name -> String -> String
makeCase brack n srcline
= let capp = ("case _ of", "case_val => ?" ++ show n) in
newLines capp
where
addBrackets : Bool -> String -> String
addBrackets False str = str
addBrackets True str = "(" ++ str ++ ")"
addCase : Nat -> (String, String) -> String
addCase n (c, pat)
= addBrackets brack $ c ++ "\n" ++
pack (replicate (n + (if brack then 6 else 5)) ' ') ++ pat
replaceStr : Nat -> String -> (String, String) -> String -> String
replaceStr indent rep new "" = ""
replaceStr indent rep new str
= if isPrefixOf rep str
then addCase indent new ++ pack (drop (length rep) (unpack str))
else assert_total $ strCons (prim__strHead str)
(replaceStr (1 + indent) rep new
(prim__strTail str))
newLines : (String, String) -> String
newLines capp = replaceStr 0 ("?" ++ show n) capp srcline

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

@ -354,6 +354,12 @@ displayIDEResult outf i (REPL $ Edited (EditError x))
displayIDEResult outf i (REPL $ Edited (MadeLemma lit name pty pappstr))
= printIDEResult outf i
$ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr
displayIDEResult outf i (REPL $ Edited (MadeWith lit wapp))
= printIDEResult outf i
$ StringAtom $ showSep "\n" (map (relit lit) wapp)
displayIDEResult outf i (REPL $ (Edited (MadeCase lit cstr)))
= printIDEResult outf i
$ StringAtom $ showSep "\n" (map (relit lit) cstr)
displayIDEResult outf i (NameList ns)
= printIDEResult outf i $ SExpList $ map toSExp ns
displayIDEResult outf i (Term t)

48
src/Idris/REPL.idr
View File

@ -215,6 +215,8 @@ data EditResult : Type where
DisplayEdit : List String -> EditResult
EditError : String -> EditResult
MadeLemma : Maybe String -> Name -> PTerm -> String -> EditResult
MadeWith : Maybe String -> List String -> EditResult
MadeCase : Maybe String -> List String -> EditResult
updateFile : {auto r : Ref ROpts REPLOpts} ->
(List String -> List String) -> Core EditResult
@ -232,7 +234,11 @@ rtrim : String -> String
rtrim str = reverse (ltrim (reverse str))
addClause : String -> Nat -> List String -> List String
addClause c Z xs = rtrim c :: xs
addClause c Z [] = rtrim c :: []
addClause c Z (x :: xs)
= if all isSpace (unpack x)
then rtrim c :: x :: xs
else x :: addClause c Z xs
addClause c (S k) (x :: xs) = x :: addClause c k xs
addClause c (S k) [] = [c]
@ -271,6 +277,17 @@ addMadeLemma lit n ty app line content
addApp lit (S k) acc (x :: xs) = addApp lit k (x :: acc) xs
addApp _ (S k) acc [] = reverse acc
-- Replace a line; works for 'case' and 'with'
addMadeCase : Maybe String -> List String -> Nat -> List String -> List String
addMadeCase lit wapp line content
= addW line [] content
where
addW : Nat -> List String -> List String -> List String
addW Z acc (_ :: rest) = reverse acc ++ map (relit lit) wapp ++ rest
addW Z acc [] = [] -- shouldn't happen!
addW (S k) acc (x :: xs) = addW k (x :: acc) xs
addW (S k) acc [] = reverse acc
processEdit : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -389,18 +406,35 @@ processEdit (MakeLemma upd line name)
Just srcLine <- getSourceLine line
| Nothing => pure (EditError "Source line not found")
let (markM,_) = isLitLine srcLine
let markML : Nat = length (fromMaybe "" markM)
if upd
then updateFile (addMadeLemma markM name (show pty) pappstr
(max 0 (integerToNat (cast (line - 1)))))
else pure $ MadeLemma markM name pty pappstr
_ => pure $ EditError "Can't make lifted definition"
processEdit (MakeCase upd line name)
= pure $ EditError "Not implemented yet"
processEdit (MakeWith upd line name)
= do Just l <- getSourceLine line
= do litStyle <- getLitStyle
syn <- get Syn
let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
Just src <- getSourceLine line
| Nothing => pure (EditError "Source line not available")
pure $ DisplayEdit [makeWith name l]
let Right l = unlit litStyle src
| Left err => pure (EditError "Invalid literate Idris")
let (markM, _) = isLitLine src
let c = lines $ makeCase brack name l
if upd
then updateFile (addMadeCase markM c (max 0 (integerToNat (cast (line - 1)))))
else pure $ MadeCase markM c
processEdit (MakeWith upd line name)
= do litStyle <- getLitStyle
Just src <- getSourceLine line
| Nothing => pure (EditError "Source line not available")
let Right l = unlit litStyle src
| Left err => pure (EditError "Invalid literate Idris")
let (markM, _) = isLitLine src
let w = lines $ makeWith name l
if upd
then updateFile (addMadeCase markM w (max 0 (integerToNat (cast (line - 1)))))
else pure $ MadeWith markM w
public export
data MissedResult : Type where
@ -843,6 +877,8 @@ mutual
displayResult (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs
displayResult (Edited (EditError x)) = printError x
displayResult (Edited (MadeLemma lit name pty pappstr)) = printResult (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr)
displayResult (Edited (MadeWith lit wapp)) = printResult $ showSep "\n" (map (relit lit) wapp)
displayResult (Edited (MadeCase lit cstr)) = printResult $ showSep "\n" (map (relit lit) cstr)
displayResult (OptionsSet opts) = printResult $ showSep "\n" $ map show opts
displayResult _ = pure ()

22
src/Idris/REPLOpts.idr
View File

@ -2,6 +2,7 @@ module Idris.REPLOpts
import Compiler.Common
import Idris.Syntax
import Parser.Unlit
import Data.List
import Data.Strings
@ -20,6 +21,7 @@ record REPLOpts where
showTypes : Bool
evalMode : REPLEval
mainfile : Maybe String
literateStyle : Maybe LiterateStyle
source : String
editor : String
errorLine : Maybe Int
@ -33,7 +35,11 @@ record REPLOpts where
export
defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
defaultOpts fname outmode cgs
= MkREPLOpts False NormaliseAll fname "" "vim" Nothing outmode "" cgs
= MkREPLOpts False NormaliseAll fname (litStyle fname) "" "vim" Nothing outmode "" cgs
where
litStyle : Maybe String -> Maybe LiterateStyle
litStyle Nothing = Nothing
litStyle (Just fn) = isLitFile fn
export
data ROpts : Type where
@ -59,7 +65,12 @@ setMainFile : {auto o : Ref ROpts REPLOpts} ->
Maybe String -> Core ()
setMainFile src
= do opts <- get ROpts
put ROpts (record { mainfile = src } opts)
put ROpts (record { mainfile = src,
literateStyle = litStyle src } opts)
where
litStyle : Maybe String -> Maybe LiterateStyle
litStyle Nothing = Nothing
litStyle (Just fn) = isLitFile fn
export
setSource : {auto o : Ref ROpts REPLOpts} ->
@ -87,6 +98,13 @@ getSourceLine l
findLine (S k) (l :: ls) = findLine k ls
findLine _ [] = Nothing
export
getLitStyle : {auto o : Ref ROpts REPLOpts} ->
Core (Maybe LiterateStyle)
getLitStyle
= do opts <- get ROpts
pure (literateStyle opts)
export
setCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
String -> Core ()

16
src/Idris/Resugar.idr
View File

@ -8,6 +8,7 @@ import Idris.Syntax
import TTImp.TTImp
import TTImp.Unelab
import TTImp.Utils
import Data.List
import Data.Maybe
@ -161,10 +162,21 @@ mutual
toPTerm p (IPi fc rig Implicit n arg ret)
= do imp <- showImplicits
if imp
then do arg' <- toPTerm appPrec arg
then do arg' <- toPTerm tyPrec arg
ret' <- toPTerm tyPrec ret
bracket p tyPrec (PPi fc rig Implicit n arg' ret')
else toPTerm p ret
else if needsBind n
then do arg' <- toPTerm tyPrec arg
ret' <- toPTerm tyPrec ret
bracket p tyPrec (PPi fc rig Implicit n arg' ret')
else toPTerm p ret
where
needsBind : Maybe Name -> Bool
needsBind (Just (UN t))
= let ns = findBindableNames False [] [] ret
allNs = findAllNames [] ret in
((UN t) `elem` allNs) && not (t `elem` (map Builtin.fst ns))
needsBind _ = False
toPTerm p (IPi fc rig pt n arg ret)
= do arg' <- toPTerm appPrec arg
ret' <- toPTerm tyPrec ret

7
src/Idris/Syntax.idr
View File

@ -593,6 +593,7 @@ public export
record IFaceInfo where
constructor MkIFaceInfo
iconstructor : Name
implParams : List Name
params : List Name
parents : List RawImp
methods : List (Name, RigCount, Maybe TotalReq, Bool, RawImp)
@ -601,8 +602,9 @@ record IFaceInfo where
export
TTC IFaceInfo where
toBuf b (MkIFaceInfo ic ps cs ms ds)
toBuf b (MkIFaceInfo ic impps ps cs ms ds)
= do toBuf b ic
toBuf b impps
toBuf b ps
toBuf b cs
toBuf b ms
@ -610,11 +612,12 @@ TTC IFaceInfo where
fromBuf b
= do ic <- fromBuf b
impps <- fromBuf b
ps <- fromBuf b
cs <- fromBuf b
ms <- fromBuf b
ds <- fromBuf b
pure (MkIFaceInfo ic ps cs ms ds)
pure (MkIFaceInfo ic impps ps cs ms ds)
-- If you update this, update 'extendAs' in Desugar to keep it up to date
-- when reading imports

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

@ -410,7 +410,7 @@ mutual
else pure tm
case elabMode elabinfo of
InLHS _ => -- reset hole and redo it with the unexpanded definition
do updateDef (Resolved idx) (const (Just (Hole 0 False)))
do updateDef (Resolved idx) (const (Just (Hole 0 (holeInit False))))
solveIfUndefined env metaval argv
pure ()
_ => pure ()

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

@ -364,7 +364,7 @@ metaVar : {vars : _} ->
FC -> RigCount ->
Env Term vars -> Name -> Term vars -> Core (Term vars)
metaVar fc rig env n ty
= do (_, tm) <- newMeta fc rig env n ty (Hole (length env) False) True
= do (_, tm) <- newMeta fc rig env n ty (Hole (length env) (holeInit False)) True
pure tm
export
@ -374,7 +374,7 @@ implBindVar : {vars : _} ->
FC -> RigCount ->
Env Term vars -> Name -> Term vars -> Core (Term vars)
implBindVar fc rig env n ty
= do (_, tm) <- newMeta fc rig env n ty (Hole (length env) True) True
= do (_, tm) <- newMeta fc rig env n ty (Hole (length env) (holeInit True)) True
pure tm
export
@ -384,7 +384,13 @@ metaVarI : {vars : _} ->
FC -> RigCount ->
Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
metaVarI fc rig env n ty
= newMeta fc rig env n ty (Hole (length env) False) True
= do defs <- get Ctxt
tynf <- nf defs env ty
let hinf = case tynf of
NApp _ (NMeta _ _ _) _ =>
record { precisetype = True } (holeInit False)
_ => holeInit False
newMeta fc rig env n ty (Hole (length env) hinf) True
export
argVar : {vars : _} ->
@ -393,7 +399,7 @@ argVar : {vars : _} ->
FC -> RigCount ->
Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
argVar fc rig env n ty
= newMetaLets fc rig env n ty (Hole (length env) False) False True
= newMetaLets fc rig env n ty (Hole (length env) (holeInit False)) False True
export
searchVar : {vars : _} ->

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

@ -14,6 +14,18 @@ import TTImp.TTImp
%default covering
-- If the hole type is itself a hole, mark it as to be solved without
-- generalising multiplicities so that we get as precise as possible a type
-- for the hole
mkPrecise : {auto c : Ref Ctxt Defs} ->
NF vars -> Core ()
mkPrecise (NApp _ (NMeta n i _) _)
= updateDef (Resolved i)
(\case
Hole i p => Just (Hole i (record { precisetype = True} p))
d => Nothing)
mkPrecise _ = pure ()
export
checkHole : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -37,6 +49,7 @@ checkHole rig elabinfo nest env fc n_in (Just gexpty)
-- applying the metavariable isn't a pattern form)
let env' = letToLam env
(idx, metaval) <- metaVarI fc rig env' nm expty
mkPrecise !(getNF gexpty)
-- Record the LHS for this hole in the metadata
withCurrentLHS (Resolved idx)
addUserHole nm
@ -48,6 +61,8 @@ checkHole rig elabinfo nest env fc n_in exp
ty <- metaVar fc erased env' nmty (TType fc)
nm <- inCurrentNS (UN n_in)
defs <- get Ctxt
mkPrecise !(nf defs env' ty)
Nothing <- lookupCtxtExact nm (gamma defs)
| _ => do log 1 $ show nm ++ " already defined"
throw (AlreadyDefined fc nm)

16
src/TTImp/Impossible.idr
View File

@ -158,8 +158,8 @@ mutual
export
getImpossibleTerm : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
Env Term vars -> RawImp -> Core ClosedTerm
getImpossibleTerm env tm
Env Term vars -> NestedNames vars -> RawImp -> Core ClosedTerm
getImpossibleTerm env nest tm
= do q <- newRef QVar (the Int 0)
mkTerm (applyEnv tm) Nothing [] []
where
@ -175,9 +175,17 @@ getImpossibleTerm env tm
then addEnv fc env
else Implicit fc False :: addEnv fc env
-- Need to apply the function to the surrounding environment
expandNest : RawImp -> RawImp
expandNest (IVar fc n)
= case lookup n (names nest) of
Just (Just n', _, _) => IVar fc n'
_ => IVar fc n
expandNest tm = tm
-- Need to apply the function to the surrounding environment, and update
-- the name to the proper one from the nested names map
applyEnv : RawImp -> RawImp
applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg
applyEnv (IImplicitApp fc fn n arg)
= IImplicitApp fc (applyEnv fn) n arg
applyEnv tm = apply tm (addEnv (getFC tm) env)
applyEnv tm = apply (expandNest tm) (addEnv (getFC tm) env)

5
src/TTImp/Interactive/CaseSplit.idr
View File

@ -84,6 +84,8 @@ getDefining tm
Ref _ _ fn => Just fn
_ => Nothing
-- For the name on the lhs, return the function name being defined, the
-- type name, and the possible constructors.
findCons : {auto c : Ref Ctxt Defs} ->
Name -> Term [] -> Core (SplitResult (Name, Name, List Name))
findCons n lhs
@ -102,7 +104,8 @@ findCons n lhs
(CantSplitThis n
("Not a type constructor " ++
show res)))
pure (OK (fn, tyn, cons))
pure (OK (fn, !(toFullNames tyn),
!(traverse toFullNames cons)))
findAllVars : Term vars -> List Name
findAllVars (Bind _ x (PVar c p ty) sc)

2
src/TTImp/Interactive/ExprSearch.idr
View File

@ -183,7 +183,7 @@ getSuccessful {vars} fc rig opts mkHole env ty topty defining all
defining
hn <- uniqueName defs (map nameRoot vars) base
(idx, tm) <- newMeta fc rig env (UN hn) ty
(Hole (length env) False)
(Hole (length env) (holeInit False))
False
pure [tm]
else if holesOK opts

2
src/TTImp/ProcessData.idr
View File

@ -317,7 +317,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
Nothing => pure []
Just ndef =>
case definition ndef of
TCon _ _ _ _ _ mw _ _ =>
TCon _ _ _ _ _ mw [] _ =>
do ok <- convert defs [] fullty (type ndef)
if ok then pure mw
else do logTermNF 1 "Previous" [] (type ndef)

5
src/TTImp/ProcessDef.idr
View File

@ -795,10 +795,11 @@ processDef opts nest env fc n_in cs_in
getClause : Either RawImp Clause -> Core (Maybe Clause)
getClause (Left rawlhs)
= catch (do lhsp <- getImpossibleTerm env rawlhs
= catch (do lhsp <- getImpossibleTerm env nest rawlhs
log 3 $ "Generated impossible LHS: " ++ show lhsp
pure $ Just $ MkClause [] lhsp (Erased (getFC rawlhs) True))
(\e => pure Nothing)
(\e => do log 5 $ "Error in getClause " ++ show e
pure Nothing)
getClause (Right c) = pure (Just c)
checkCoverage : Int -> ClosedTerm -> RigCount ->

208
src/TTImp/Utils.idr
View File

@ -30,13 +30,13 @@ findBindableNames arg env used (IPi fc rig p mn aty retty)
= let env' = case mn of
Nothing => env
Just n => n :: env in
findBindableNames True env' used aty ++
findBindableNames True env used aty ++
findBindableNames True env' used retty
findBindableNames arg env used (ILam fc rig p mn aty sc)
= let env' = case mn of
Nothing => env
Just n => n :: env in
findBindableNames True env' used aty ++
findBindableNames True env used aty ++
findBindableNames True env' used sc
findBindableNames arg env used (IApp fc fn av)
= findBindableNames False env used fn ++ findBindableNames True env used av
@ -66,6 +66,46 @@ findBindableNames arg env used (IAlternative fc u alts)
-- name should be bound, leave it to the programmer
findBindableNames arg env used tm = []
export
findAllNames : (env : List Name) -> RawImp -> List Name
findAllNames env (IVar fc n)
= if not (n `elem` env) then [n] else []
findAllNames env (IPi fc rig p mn aty retty)
= let env' = case mn of
Nothing => env
Just n => n :: env in
findAllNames env aty ++ findAllNames env' retty
findAllNames env (ILam fc rig p mn aty sc)
= let env' = case mn of
Nothing => env
Just n => n :: env in
findAllNames env' aty ++ findAllNames env' sc
findAllNames env (IApp fc fn av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IImplicitApp fc fn n av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IWithApp fc fn av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IAs fc _ n pat)
= n :: findAllNames env pat
findAllNames env (IMustUnify fc r pat)
= findAllNames env pat
findAllNames env (IDelayed fc r t)
= findAllNames env t
findAllNames env (IDelay fc t)
= findAllNames env t
findAllNames env (IForce fc t)
= findAllNames env t
findAllNames env (IQuote fc t)
= findAllNames env t
findAllNames env (IUnquote fc t)
= findAllNames env t
findAllNames env (IAlternative fc u alts)
= concatMap (findAllNames env) alts
-- We've skipped case, let and local - rather than guess where the
-- name should be bound, leave it to the programmer
findAllNames env tm = []
-- Find the names in a type that affect the 'using' declarations (i.e.
-- the ones that mean the declaration will be added).
export
@ -95,97 +135,117 @@ findIBindVars (IAlternative fc u alts)
findIBindVars tm = []
mutual
export
substNames : List Name -> List (Name, RawImp) ->
RawImp -> RawImp
substNames bound ps (IVar fc n)
-- Substitute for either an explicit variable name, or a bound variable name
substNames' : Bool -> List Name -> List (Name, RawImp) ->
RawImp -> RawImp
substNames' False bound ps (IVar fc n)
= if not (n `elem` bound)
then case lookup n ps of
Just t => t
_ => IVar fc n
else IVar fc n
substNames bound ps (IPi fc r p mn argTy retTy)
substNames' True bound ps (IBindVar fc n)
= if not (UN n `elem` bound)
then case lookup (UN n) ps of
Just t => t
_ => IBindVar fc n
else IBindVar fc n
substNames' bvar bound ps (IPi fc r p mn argTy retTy)
= let bound' = maybe bound (\n => n :: bound) mn in
IPi fc r p mn (substNames bound ps argTy)
(substNames bound' ps retTy)
substNames bound ps (ILam fc r p mn argTy scope)
IPi fc r p mn (substNames' bvar bound ps argTy)
(substNames' bvar bound' ps retTy)
substNames' bvar bound ps (ILam fc r p mn argTy scope)
= let bound' = maybe bound (\n => n :: bound) mn in
ILam fc r p mn (substNames bound ps argTy)
(substNames bound' ps scope)
substNames bound ps (ILet fc r n nTy nVal scope)
ILam fc r p mn (substNames' bvar bound ps argTy)
(substNames' bvar bound' ps scope)
substNames' bvar bound ps (ILet fc r n nTy nVal scope)
= let bound' = n :: bound in
ILet fc r n (substNames bound ps nTy)
(substNames bound ps nVal)
(substNames bound' ps scope)
substNames bound ps (ICase fc y ty xs)
= ICase fc (substNames bound ps y) (substNames bound ps ty)
(map (substNamesClause bound ps) xs)
substNames bound ps (ILocal fc xs y)
ILet fc r n (substNames' bvar bound ps nTy)
(substNames' bvar bound ps nVal)
(substNames' bvar bound' ps scope)
substNames' bvar bound ps (ICase fc y ty xs)
= ICase fc (substNames' bvar bound ps y) (substNames' bvar bound ps ty)
(map (substNamesClause' bvar bound ps) xs)
substNames' bvar bound ps (ILocal fc xs y)
= let bound' = definedInBlock [] xs ++ bound in
ILocal fc (map (substNamesDecl bound ps) xs)
(substNames bound' ps y)
substNames bound ps (IApp fc fn arg)
= IApp fc (substNames bound ps fn) (substNames bound ps arg)
substNames bound ps (IImplicitApp fc fn y arg)
= IImplicitApp fc (substNames bound ps fn) y (substNames bound ps arg)
substNames bound ps (IWithApp fc fn arg)
= IWithApp fc (substNames bound ps fn) (substNames bound ps arg)
substNames bound ps (IAlternative fc y xs)
= IAlternative fc y (map (substNames bound ps) xs)
substNames bound ps (ICoerced fc y)
= ICoerced fc (substNames bound ps y)
substNames bound ps (IAs fc s y pattern)
= IAs fc s y (substNames bound ps pattern)
substNames bound ps (IMustUnify fc r pattern)
= IMustUnify fc r (substNames bound ps pattern)
substNames bound ps (IDelayed fc r t)
= IDelayed fc r (substNames bound ps t)
substNames bound ps (IDelay fc t)
= IDelay fc (substNames bound ps t)
substNames bound ps (IForce fc t)
= IForce fc (substNames bound ps t)
substNames bound ps tm = tm
ILocal fc (map (substNamesDecl' bvar bound ps) xs)
(substNames' bvar bound' ps y)
substNames' bvar bound ps (IApp fc fn arg)
= IApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
substNames' bvar bound ps (IImplicitApp fc fn y arg)
= IImplicitApp fc (substNames' bvar bound ps fn) y (substNames' bvar bound ps arg)
substNames' bvar bound ps (IWithApp fc fn arg)
= IWithApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
substNames' bvar bound ps (IAlternative fc y xs)
= IAlternative fc y (map (substNames' bvar bound ps) xs)
substNames' bvar bound ps (ICoerced fc y)
= ICoerced fc (substNames' bvar bound ps y)
substNames' bvar bound ps (IAs fc s y pattern)
= IAs fc s y (substNames' bvar bound ps pattern)
substNames' bvar bound ps (IMustUnify fc r pattern)
= IMustUnify fc r (substNames' bvar bound ps pattern)
substNames' bvar bound ps (IDelayed fc r t)
= IDelayed fc r (substNames' bvar bound ps t)
substNames' bvar bound ps (IDelay fc t)
= IDelay fc (substNames' bvar bound ps t)
substNames' bvar bound ps (IForce fc t)
= IForce fc (substNames' bvar bound ps t)
substNames' bvar bound ps tm = tm
export
substNamesClause : List Name -> List (Name, RawImp) ->
ImpClause -> ImpClause
substNamesClause bound ps (PatClause fc lhs rhs)
substNamesClause' : Bool -> List Name -> List (Name, RawImp) ->
ImpClause -> ImpClause
substNamesClause' bvar bound ps (PatClause fc lhs rhs)
= let bound' = map UN (map snd (findBindableNames True bound [] lhs))
++ bound in
PatClause fc (substNames [] [] lhs)
(substNames bound' ps rhs)
substNamesClause bound ps (WithClause fc lhs wval flags cs)
PatClause fc (substNames' bvar [] [] lhs)
(substNames' bvar bound' ps rhs)
substNamesClause' bvar bound ps (WithClause fc lhs wval flags cs)
= let bound' = map UN (map snd (findBindableNames True bound [] lhs))
++ bound in
WithClause fc (substNames [] [] lhs)
(substNames bound' ps wval) flags cs
substNamesClause bound ps (ImpossibleClause fc lhs)
= ImpossibleClause fc (substNames bound [] lhs)
WithClause fc (substNames' bvar [] [] lhs)
(substNames' bvar bound' ps wval) flags cs
substNamesClause' bvar bound ps (ImpossibleClause fc lhs)
= ImpossibleClause fc (substNames' bvar bound [] lhs)
substNamesTy : List Name -> List (Name, RawImp) ->
substNamesTy' : Bool -> List Name -> List (Name, RawImp) ->
ImpTy -> ImpTy
substNamesTy bound ps (MkImpTy fc n ty)
= MkImpTy fc n (substNames bound ps ty)
substNamesTy' bvar bound ps (MkImpTy fc n ty)
= MkImpTy fc n (substNames' bvar bound ps ty)
substNamesData : List Name -> List (Name, RawImp) ->
ImpData -> ImpData
substNamesData bound ps (MkImpData fc n con opts dcons)
= MkImpData fc n (substNames bound ps con) opts
(map (substNamesTy bound ps) dcons)
substNamesData bound ps (MkImpLater fc n con)
= MkImpLater fc n (substNames bound ps con)
substNamesData' : Bool -> List Name -> List (Name, RawImp) ->
ImpData -> ImpData
substNamesData' bvar bound ps (MkImpData fc n con opts dcons)
= MkImpData fc n (substNames' bvar bound ps con) opts
(map (substNamesTy' bvar bound ps) dcons)
substNamesData' bvar bound ps (MkImpLater fc n con)
= MkImpLater fc n (substNames' bvar bound ps con)
substNamesDecl : List Name -> List (Name, RawImp ) ->
substNamesDecl' : Bool -> List Name -> List (Name, RawImp ) ->
ImpDecl -> ImpDecl
substNamesDecl bound ps (IClaim fc r vis opts td)
= IClaim fc r vis opts (substNamesTy bound ps td)
substNamesDecl bound ps (IDef fc n cs)
= IDef fc n (map (substNamesClause bound ps) cs)
substNamesDecl bound ps (IData fc vis d)
= IData fc vis (substNamesData bound ps d)
substNamesDecl bound ps (INamespace fc ns ds)
= INamespace fc ns (map (substNamesDecl bound ps) ds)
substNamesDecl bound ps d = d
substNamesDecl' bvar bound ps (IClaim fc r vis opts td)
= IClaim fc r vis opts (substNamesTy' bvar bound ps td)
substNamesDecl' bvar bound ps (IDef fc n cs)
= IDef fc n (map (substNamesClause' bvar bound ps) cs)
substNamesDecl' bvar bound ps (IData fc vis d)
= IData fc vis (substNamesData' bvar bound ps d)
substNamesDecl' bvar bound ps (INamespace fc ns ds)
= INamespace fc ns (map (substNamesDecl' bvar bound ps) ds)
substNamesDecl' bvar bound ps d = d
export
substNames : List Name -> List (Name, RawImp) ->
RawImp -> RawImp
substNames = substNames' False
export
substBindVars : List Name -> List (Name, RawImp) ->
RawImp -> RawImp
substBindVars = substNames' True
export
substNamesClause : List Name -> List (Name, RawImp) ->
ImpClause -> ImpClause
substNamesClause = substNamesClause' False
mutual
export

17
tests/Main.idr
View File

@ -54,12 +54,7 @@ idrisTests
"interactive001", "interactive002", "interactive003", "interactive004",
"interactive005", "interactive006", "interactive007", "interactive008",
"interactive009", "interactive010", "interactive011", "interactive012",
"interactive013",
-- Literate
"literate001", "literate002", "literate003", "literate004",
"literate005", "literate006", "literate007", "literate008",
"literate009", "literate010", "literate011", "literate012",
"literate013",
"interactive013", "interactive014",
-- Interfaces
"interface001", "interface002", "interface003", "interface004",
"interface005", "interface006", "interface007", "interface008",
@ -72,7 +67,12 @@ idrisTests
-- QTT and linearity related
"linear001", "linear002", "linear003", "linear004", "linear005",
"linear006", "linear007", "linear008", "linear009", "linear010",
"linear011",
"linear011", "linear012",
-- Literate
"literate001", "literate002", "literate003", "literate004",
"literate005", "literate006", "literate007", "literate008",
"literate009", "literate010", "literate011", "literate012",
"literate013", "literate014",
-- Namespace blocks
"namespace001",
-- Parameters blocks
@ -97,7 +97,8 @@ idrisTests
"reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
"reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
"reg022", "reg023",
"reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
"reg029",
-- Totality checking
"total001", "total002", "total003", "total004", "total005",
"total006", "total007", "total008",

12
tests/ideMode/ideMode001/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:269}_[] ?{_:270}_[])")))))) 1)
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 ?{_:271}_[] ?{_:270}_[])")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:277} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:278}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:277}_[] ?{_:278}_[])")))))) 1)
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 ?{_:260}_[] ?{_:259}_[])")))))) 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:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (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)
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)
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)

12
tests/ideMode/ideMode003/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:269}_[] ?{_:270}_[])")))))) 1)
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 ?{_:271}_[] ?{_:270}_[])")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:277} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:278}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:277}_[] ?{_:278}_[])")))))) 1)
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 ?{_:260}_[] ?{_:259}_[])")))))) 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:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (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)
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)
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/idris2/coverage008/expected
View File

@ -1,6 +1,6 @@
1/1: Building wcov (wcov.idr)
Main> Main.tfoo is total
Main> Main.wfoo is total
Main> Main.wbar is not covering due to call to function Main.with block in 1393
Main> Main.wbar is not covering due to call to function Main.with block in 1395
Main> Main.wbar1 is total
Main> Bye for now!

2
tests/idris2/coverage010/expected
View File

@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
12 main : IO ()
13 main = do
Calls non covering function Main.case block in 2145(622)
Calls non covering function Main.case block in 2148(630)

7
tests/idris2/interactive014/case.idr Normal file
View File

@ -0,0 +1,7 @@
foo : Nat -> Nat
foo x = ?foo_rhs
bar : Nat -> Nat
bar x = plus x ?bar_rhs
-- Rest of file

6
tests/idris2/interactive014/expected Normal file
View File

@ -0,0 +1,6 @@
1/1: Building case (case.idr)
Main> foo x = case _ of
case_val => ?foo_rhs
Main> bar x = plus x (case _ of
case_val => ?bar_rhs)
Main> Bye for now!

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

@ -0,0 +1,3 @@
:mc 2 foo_rhs
:mc 5 bar_rhs
:q

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

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

20
tests/idris2/linear012/expected Normal file
View File

@ -0,0 +1,20 @@
1/1: Building linholes (linholes.idr)
Main> 0 c : Type
0 b : Type
0 a : Type
f : ((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()
-------------------------------------
foo1h : (1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()
Main> 0 c : Type
0 b : Type
0 a : Type
f : ((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()
-------------------------------------
foo2h : (1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()
Main> 0 c : Type
0 b : Type
0 a : Type
f : ((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()
-------------------------------------
foo3h : (1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()
Main> Bye for now!

4
tests/idris2/linear012/input Normal file
View File

@ -0,0 +1,4 @@
:t foo1h
:t foo2h
:t foo3h
:q

15
tests/idris2/linear012/linholes.idr Normal file
View File

@ -0,0 +1,15 @@
infixr 6 -*
(-*) : Type -> Type -> Type
(-*) a b = (1 _ : a) -> b
-- Test that the types of holes are not overly generalised wrt the
-- multiplicities in the function type
foo1 : (((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()) -> ()
foo1 f = f ?foo1h
foo2 : (((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()) -> ()
foo2 f = f (id ?foo2h)
foo3 : ((a -* b -* c -* ()) -> ()) -> ()
foo3 f = f (id ?foo3h)

3
tests/idris2/linear012/run Normal file
View File

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

4
tests/idris2/literate014/expected Normal file
View File

@ -0,0 +1,4 @@
1/1: Building with (with.lidr)
Main> > dnat x y with (_)
> dnat x y | with_pat = ?dnat_rhs
Main> Bye for now!

2
tests/idris2/literate014/input Normal file
View File

@ -0,0 +1,2 @@
:mw 4 dnat
:q

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

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

4
tests/idris2/literate014/with.lidr Normal file
View File

@ -0,0 +1,4 @@
> import Decidable.Equality
>
> dnat : (x : Nat) -> (y : Nat) -> Maybe (x = y)
> dnat x y = ?dec

7
tests/idris2/literate015/case.lidr Normal file
View File

@ -0,0 +1,7 @@
> foo : Nat -> Nat
> foo x = ?foo_rhs
>
> bar : Nat -> Nat
> bar x = plus x ?bar_rhs
>
> -- Rest of file

6
tests/idris2/literate015/expected Normal file
View File

@ -0,0 +1,6 @@
1/1: Building case (case.lidr)
Main> > foo x = case _ of
> case_val => ?foo_rhs
Main> > bar x = plus x (case _ of
> case_val => ?bar_rhs)
Main> Bye for now!

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

@ -0,0 +1,3 @@
:mc 2 foo_rhs
:mc 5 bar_rhs
:q

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

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

2
tests/idris2/namespace001/expected
View File

@ -1,5 +1,5 @@
1/1: Building Dup (Dup.idr)
Dup.idr:14:13--14:15:Main.A is already defined
Dup.idr:13:1--15:1:Main.Test is already defined
Main> Bye for now!
1/1: Building Scope (Scope.idr)
Main> Main.Test : Type

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