git.iko.soy/Idris-dev
on master help sign in
Renamed Prelude.Classes to Prelude.Interfaces
74926ffJan de Muijnck-Hughes
libs/prelude/Decidable/Equality.idr+2−5
compare with master
unifiedsplit
@@ -3,7 +3,7 @@ module Decidable.Equality
3import Builtins
3import Builtins
4import Prelude.Basics
4import Prelude.Basics
5import Prelude.Bool
5import Prelude.Bool
6−import Prelude.Classes
6+import Prelude.Interfaces
7import Prelude.Either
7import Prelude.Either
8import Prelude.List
8import Prelude.List
9import Prelude.Nat
9import Prelude.Nat
@@ -141,7 +141,7 @@ implementation DecEq a => DecEq (List a) where
141 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
141 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
142 decEq (x :: xs) (y :: ys) with (decEq x y)
142 decEq (x :: xs) (y :: ys) with (decEq x y)
143 decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
143 decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
144− decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
144+ decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
145 decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq)
145 decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq)
146 decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
146 decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
147 decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)
147 decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)
@@ -211,6 +211,3 @@ implementation DecEq ManagedPtr where
211 where primitiveEq : x = y
211 where primitiveEq : x = y
212 primitiveEq = believe_me (Refl {x})
212 primitiveEq = believe_me (Refl {x})
213 postulate primitiveNotEq : x = y -> Void
213 postulate primitiveNotEq : x = y -> Void
214−
215−
216−
libs/prelude/Prelude.idr+4−5
@@ -6,7 +6,7 @@ import public IO
6import public Prelude.Algebra
6import public Prelude.Algebra
7import public Prelude.Basics
7import public Prelude.Basics
8import public Prelude.Bool
8import public Prelude.Bool
9−import public Prelude.Classes
9+import public Prelude.Interfaces
10import public Prelude.Cast
10import public Prelude.Cast
11import public Prelude.Nat
11import public Prelude.Nat
12import public Prelude.List
12import public Prelude.List
@@ -210,7 +210,7 @@ Enum Int where
210Enum Char where
210Enum Char where
211 toNat c = toNat (ord c)
211 toNat c = toNat (ord c)
212 fromNat n = chr (fromNat n)
212 fromNat n = chr (fromNat n)
213−
213+
214 pred c = fromNat (pred (toNat c))
214 pred c = fromNat (pred (toNat c))
215
215
216syntax "[" [start] ".." [end] "]"
216syntax "[" [start] ".." [end] "]"
@@ -264,12 +264,12 @@ while t b = do v <- t
264------- Some error rewriting
264------- Some error rewriting
265
265
266%language ErrorReflection
266%language ErrorReflection
267−
267+
268private
268private
269cast_part : TT -> ErrorReportPart
269cast_part : TT -> ErrorReportPart
270cast_part (P Bound n t) = TextPart "unknown type"
270cast_part (P Bound n t) = TextPart "unknown type"
271cast_part x = TermPart x
271cast_part x = TermPart x
272−
272+
273%error_handler
273%error_handler
274cast_error : Err -> Maybe (List ErrorReportPart)
274cast_error : Err -> Maybe (List ErrorReportPart)
275cast_error (CantResolve `(Cast ~x ~y))
275cast_error (CantResolve `(Cast ~x ~y))
@@ -284,4 +284,3 @@ num_error : Err -> Maybe (List ErrorReportPart)
284num_error (CantResolve `(Num ~x))
284num_error (CantResolve `(Num ~x))
285 = Just [TermPart x, TextPart "is not a numeric type"]
285 = Just [TermPart x, TextPart "is not a numeric type"]
286num_error _ = Nothing
286num_error _ = Nothing
287−
libs/prelude/Prelude/Applicative.idr+1−1
@@ -4,7 +4,7 @@ import Builtins
4
4
5import Prelude.Basics
5import Prelude.Basics
6import Prelude.Bool
6import Prelude.Bool
7−import Prelude.Classes
7+import Prelude.Interfaces
8import Prelude.Foldable
8import Prelude.Foldable
9import Prelude.Functor
9import Prelude.Functor
10
10
libs/prelude/Prelude/Bits.idr+1−1
@@ -6,7 +6,7 @@ import Prelude.Basics
6import Prelude.Bool
6import Prelude.Bool
7import Prelude.Cast
7import Prelude.Cast
8import Prelude.Chars
8import Prelude.Chars
9−import Prelude.Classes
9+import Prelude.Interfaces
10import Prelude.Foldable
10import Prelude.Foldable
11import Prelude.Nat
11import Prelude.Nat
12import Prelude.List
12import Prelude.List
libs/prelude/Prelude/Chars.idr+1−3
@@ -2,7 +2,7 @@ module Prelude.Chars
2-- Functions operating over Chars
2-- Functions operating over Chars
3
3
4import Prelude.Bool
4import Prelude.Bool
5−import Prelude.Classes
5+import Prelude.Interfaces
6import Prelude.List
6import Prelude.List
7import Prelude.Cast
7import Prelude.Cast
8import Builtins
8import Builtins
@@ -74,5 +74,3 @@ isHexDigit x = elem (toUpper x) hexChars where
74||| Returns true if the character is an octal digit.
74||| Returns true if the character is an octal digit.
75isOctDigit : Char -> Bool
75isOctDigit : Char -> Bool
76isOctDigit x = (x >= '0' && x <= '7')
76isOctDigit x = (x >= '0' && x <= '7')
77−
78−
libs/prelude/Prelude/Doubles.idr+3−5
@@ -1,7 +1,7 @@
1−module Prelude.Doubles
1+module Prelude.Doubles
2
2
3import Builtins
3import Builtins
4−import Prelude.Classes
4+import Prelude.Interfaces
5
5
6%access public
6%access public
7%default total
7%default total
@@ -10,7 +10,7 @@ import Prelude.Classes
10%lib C "m"
10%lib C "m"
11
11
12pi : Double
12pi : Double
13−pi = 3.14159265358979323846
13+pi = 3.14159265358979323846
14
14
15euler : Double
15euler : Double
16euler = 2.7182818284590452354
16euler = 2.7182818284590452354
@@ -59,5 +59,3 @@ floor x = prim__floatFloor x
59
59
60ceiling : Double -> Double
60ceiling : Double -> Double
61ceiling x = prim__floatCeil x
61ceiling x = prim__floatCeil x
62−
63−
libs/prelude/Prelude/Either.idr+1−1
@@ -4,7 +4,7 @@ import Builtins
4
4
5import Prelude.Basics
5import Prelude.Basics
6import Prelude.Bool
6import Prelude.Bool
7−import Prelude.Classes
7+import Prelude.Interfaces
8import Prelude.Maybe
8import Prelude.Maybe
9import Prelude.List
9import Prelude.List
10
10
libs/prelude/Prelude/File.idr+5−5
@@ -9,7 +9,7 @@ import Prelude.Strings
9import Prelude.Cast
9import Prelude.Cast
10import Prelude.Bool
10import Prelude.Bool
11import Prelude.Basics
11import Prelude.Basics
12−import Prelude.Classes
12+import Prelude.Interfaces
13import Prelude.Either
13import Prelude.Either
14import Prelude.Show
14import Prelude.Show
15import IO
15import IO
@@ -39,7 +39,7 @@ strError err = unsafePerformIO -- yeah, yeah...
39 (foreign FFI_C "idris_showerror" (Int -> IO String) err)
39 (foreign FFI_C "idris_showerror" (Int -> IO String) err)
40
40
41getFileError : IO FileError
41getFileError : IO FileError
42−getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"
42+getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"
43 (Ptr -> IO (Raw FileError)) prim__vm
43 (Ptr -> IO (Raw FileError)) prim__vm
44 return err
44 return err
45
45
@@ -154,7 +154,7 @@ do_fwrite : Ptr -> String -> IO (Either FileError ())
154do_fwrite h s = do res <- prim_fwrite h s
154do_fwrite h s = do res <- prim_fwrite h s
155 if (res /= 0)
155 if (res /= 0)
156 then do errno <- getErrno
156 then do errno <- getErrno
157− if errno == 0
157+ if errno == 0
158 then return (Left FileWriteError)
158 then return (Left FileWriteError)
159 else do err <- getFileError
159 else do err <- getFileError
160 return (Left err)
160 return (Left err)
@@ -193,7 +193,7 @@ fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
193 return (p > 0)
193 return (p > 0)
194
194
195||| Read the contents of a file into a string
195||| Read the contents of a file into a string
196−partial -- might be reading something infinitely long like /dev/null ...
196+partial -- might be reading something infinitely long like /dev/null ...
197covering
197covering
198readFile : String -> IO (Either FileError String)
198readFile : String -> IO (Either FileError String)
199readFile fn = do Right h <- openFile fn Read
199readFile fn = do Right h <- openFile fn Read
@@ -212,7 +212,7 @@ readFile fn = do Right h <- openFile fn Read
212 else return (Right contents)
212 else return (Right contents)
213
213
214||| Write a string to a file
214||| Write a string to a file
215−writeFile : (filepath : String) -> (contents : String) ->
215+writeFile : (filepath : String) -> (contents : String) ->
216 IO (Either FileError ())
216 IO (Either FileError ())
217writeFile fn contents = do
217writeFile fn contents = do
218 Right h <- openFile fn Write | Left err => return (Left err)
218 Right h <- openFile fn Write | Left err => return (Left err)
libs/prelude/Prelude/Foldable.idr+1−2
@@ -3,7 +3,7 @@ module Prelude.Foldable
3import Builtins
3import Builtins
4import Prelude.Bool
4import Prelude.Bool
5import Prelude.Basics
5import Prelude.Basics
6−import Prelude.Classes
6+import Prelude.Interfaces
7import Prelude.Algebra
7import Prelude.Algebra
8
8
9%access public
9%access public
@@ -54,4 +54,3 @@ sum = foldr (+) 0
54||| Multiply together all elements of a structure
54||| Multiply together all elements of a structure
55product : (Foldable t, Num a) => t a -> a
55product : (Foldable t, Num a) => t a -> a
56product = foldr (*) 1
56product = foldr (*) 1
57−
libs/prelude/Prelude/Interactive.idr+17−18
@@ -1,5 +1,5 @@
1||| Various helper functions for creating simple interactive systems.
1||| Various helper functions for creating simple interactive systems.
2−|||
2+|||
3||| These are mostly intended for helping with teaching, in that they will allow
3||| These are mostly intended for helping with teaching, in that they will allow
4||| the easy creation of interactive programs without needing to teach IO
4||| the easy creation of interactive programs without needing to teach IO
5||| or Effects first, but they also capture some common patterns of interactive
5||| or Effects first, but they also capture some common patterns of interactive
@@ -10,7 +10,7 @@ import Builtins
10import Prelude.List
10import Prelude.List
11import Prelude.File
11import Prelude.File
12import Prelude.Bool
12import Prelude.Bool
13−import Prelude.Classes
13+import Prelude.Interfaces
14import Prelude.Strings
14import Prelude.Strings
15import Prelude.Chars
15import Prelude.Chars
16import Prelude.Show
16import Prelude.Show
@@ -115,19 +115,19 @@ getArgs = do n <- numArgs
115||| @ onEOF the function to run on reaching end of file, returning a String
115||| @ onEOF the function to run on reaching end of file, returning a String
116||| to output
116||| to output
117partial
117partial
118−processHandle : File ->
118+processHandle : File ->
119 (state : a) ->
119 (state : a) ->
120− (onRead : a -> String -> (String, a)) ->
120+ (onRead : a -> String -> (String, a)) ->
121− (onEOF : a -> String) ->
121+ (onEOF : a -> String) ->
122 IO ()
122 IO ()
123−processHandle h acc onRead onEOF
123+processHandle h acc onRead onEOF
124 = if !(fEOF h)
124 = if !(fEOF h)
125 then putStr (onEOF acc)
125 then putStr (onEOF acc)
126 else do Right x <- fGetLine h
126 else do Right x <- fGetLine h
127 | Left err => putStr (onEOF acc)
127 | Left err => putStr (onEOF acc)
128 let (out, acc') = onRead acc x
128 let (out, acc') = onRead acc x
129 putStr out
129 putStr out
130− processHandle h acc' onRead onEOF
130+ processHandle h acc' onRead onEOF
131
131
132||| Process input from the standard input stream, while maintaining a state.
132||| Process input from the standard input stream, while maintaining a state.
133||| @ state the input state
133||| @ state the input state
@@ -136,34 +136,33 @@ processHandle h acc onRead onEOF
136||| @ onEOI the function to run on reaching end of input, returning a String
136||| @ onEOI the function to run on reaching end of input, returning a String
137||| to output
137||| to output
138partial
138partial
139−processStdin : (state : a) ->
139+processStdin : (state : a) ->
140− (onRead : a -> String -> (String, a)) ->
140+ (onRead : a -> String -> (String, a)) ->
141 (onEOI : a -> String) -> IO ()
141 (onEOI : a -> String) -> IO ()
142processStdin = processHandle stdin
142processStdin = processHandle stdin
143
143
144||| A basic read-eval-print loop, maintaining a state
144||| A basic read-eval-print loop, maintaining a state
145||| @ state the input state
145||| @ state the input state
146−||| @ prompt the prompt to show
146+||| @ prompt the prompt to show
147||| @ onInput the function to run on reading input, returning a String to
147||| @ onInput the function to run on reading input, returning a String to
148||| output and a new state. Returns Nothing if the repl should exit
148||| output and a new state. Returns Nothing if the repl should exit
149partial
149partial
150−replWith : (state : a) -> (prompt : String) ->
150+replWith : (state : a) -> (prompt : String) ->
151 (onInput : a -> String -> Maybe (String, a)) -> IO ()
151 (onInput : a -> String -> Maybe (String, a)) -> IO ()
152−replWith acc prompt fn
152+replWith acc prompt fn
153 = do putStr prompt
153 = do putStr prompt
154 x <- getLine
154 x <- getLine
155 case fn acc x of
155 case fn acc x of
156− Just (out, acc') => do putStr out
156+ Just (out, acc') => do putStr out
157 replWith acc' prompt fn
157 replWith acc' prompt fn
158 Nothing => return ()
158 Nothing => return ()
159
159
160||| A basic read-eval-print loop
160||| A basic read-eval-print loop
161−||| @ prompt the prompt to show
161+||| @ prompt the prompt to show
162||| @ onInput the function to run on reading input, returning a String to
162||| @ onInput the function to run on reading input, returning a String to
163−||| output
163+||| output
164partial
164partial
165−repl : (prompt : String) ->
165+repl : (prompt : String) ->
166 (onInput : String -> String) -> IO ()
166 (onInput : String -> String) -> IO ()
167−repl prompt fn
167+repl prompt fn
168 = replWith () prompt (\x, s => Just (fn s, ()))
168 = replWith () prompt (\x, s => Just (fn s, ()))
169−
libs/prelude/Prelude/Classes.idr → libs/prelude/Prelude/Interfaces.idrrenamed+9−11
@@ -1,4 +1,4 @@
1−module Prelude.Classes
1+module Prelude.Interfaces
2
2
3import Builtins
3import Builtins
4import Prelude.Basics
4import Prelude.Basics
@@ -57,7 +57,7 @@ Eq Bool where
57 True == False = False
57 True == False = False
58 False == True = False
58 False == True = False
59 False == False = True
59 False == False = True
60−
60+
61(Eq a, Eq b) => Eq (a, b) where
61(Eq a, Eq b) => Eq (a, b) where
62 (==) (a, c) (b, d) = (a == b) && (c == d)
62 (==) (a, c) (b, d) = (a == b) && (c == d)
63
63
@@ -357,7 +357,7 @@ divB8 x y = case y == 0 of
357modB8 : Bits8 -> Bits8 -> Bits8
357modB8 : Bits8 -> Bits8 -> Bits8
358modB8 x y = case y == 0 of
358modB8 x y = case y == 0 of
359 False => prim__sremB8 x y
359 False => prim__sremB8 x y
360−
360+
361Integral Bits8 where
361Integral Bits8 where
362 div = divB8
362 div = divB8
363 mod = modB8
363 mod = modB8
@@ -372,8 +372,8 @@ modB16 x y = case y == 0 of
372 False => prim__sremB16 x y
372 False => prim__sremB16 x y
373
373
374Integral Bits16 where
374Integral Bits16 where
375− div = divB16
375+ div = divB16
376− mod = modB16
376+ mod = modB16
377
377
378-- ------------------------------------------------------------------ [ Bits32 ]
378-- ------------------------------------------------------------------ [ Bits32 ]
379divB32 : Bits32 -> Bits32 -> Bits32
379divB32 : Bits32 -> Bits32 -> Bits32
@@ -385,8 +385,8 @@ modB32 x y = case y == 0 of
385 False => prim__sremB32 x y
385 False => prim__sremB32 x y
386
386
387Integral Bits32 where
387Integral Bits32 where
388− div = divB32
388+ div = divB32
389− mod = modB32
389+ mod = modB32
390
390
391-- ------------------------------------------------------------------ [ Bits64 ]
391-- ------------------------------------------------------------------ [ Bits64 ]
392divB64 : Bits64 -> Bits64 -> Bits64
392divB64 : Bits64 -> Bits64 -> Bits64
@@ -398,7 +398,5 @@ modB64 x y = case y == 0 of
398 False => prim__sremB64 x y
398 False => prim__sremB64 x y
399
399
400Integral Bits64 where
400Integral Bits64 where
401− div = divB64
401+ div = divB64
402− mod = modB64
402+ mod = modB64
403−
404−
libs/prelude/Prelude/List.idr+4−5
@@ -5,7 +5,7 @@ import Builtins
5import Prelude.Algebra
5import Prelude.Algebra
6import Prelude.Basics
6import Prelude.Basics
7import Prelude.Bool
7import Prelude.Bool
8−import Prelude.Classes
8+import Prelude.Interfaces
9import Prelude.Foldable
9import Prelude.Foldable
10import Prelude.Functor
10import Prelude.Functor
11import Prelude.Maybe
11import Prelude.Maybe
@@ -174,7 +174,7 @@ init' [] = Nothing
174init' (x::xs) =
174init' (x::xs) =
175 case xs of
175 case xs of
176 [] => Just []
176 [] => Just []
177− y::ys =>
177+ y::ys =>
178 case init' $ y::ys of
178 case init' $ y::ys of
179 Nothing => Nothing
179 Nothing => Nothing
180 Just j => Just $ x :: j
180 Just j => Just $ x :: j
@@ -305,7 +305,7 @@ zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
305||| @ z the third list
305||| @ z the third list
306zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
306zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
307 (z : List c) -> List d
307 (z : List c) -> List d
308−zipWith3 f _ [] (z::zs) = []
308+zipWith3 f _ [] (z::zs) = []
309zipWith3 f _ (y::ys) [] = []
309zipWith3 f _ (y::ys) [] = []
310zipWith3 f [] (y::ys) _ = []
310zipWith3 f [] (y::ys) _ = []
311zipWith3 f (x::xs) [] _ = []
311zipWith3 f (x::xs) [] _ = []
@@ -761,7 +761,7 @@ mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
761mergeBy order [] right = right
761mergeBy order [] right = right
762mergeBy order left [] = left
762mergeBy order left [] = left
763mergeBy order (x::xs) (y::ys) =
763mergeBy order (x::xs) (y::ys) =
764− if order x y == LT
764+ if order x y == LT
765 then x :: mergeBy order xs (y::ys)
765 then x :: mergeBy order xs (y::ys)
766 else y :: mergeBy order (x::xs) ys
766 else y :: mergeBy order (x::xs) ys
767
767
@@ -888,4 +888,3 @@ foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
888foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs
888foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs
889foldlMatchesFoldr f q [] = Refl
889foldlMatchesFoldr f q [] = Refl
890foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
890foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
891−
libs/prelude/Prelude/Maybe.idr+1−1
@@ -5,7 +5,7 @@ import Prelude.Algebra
5import Prelude.Basics
5import Prelude.Basics
6import Prelude.Bool
6import Prelude.Bool
7import Prelude.Cast
7import Prelude.Cast
8−import Prelude.Classes
8+import Prelude.Interfaces
9import Prelude.Foldable
9import Prelude.Foldable
10
10
11%access public
11%access public
libs/prelude/Prelude/Nat.idr+17−18
@@ -6,7 +6,7 @@ import Prelude.Algebra
6import Prelude.Basics
6import Prelude.Basics
7import Prelude.Bool
7import Prelude.Bool
8import Prelude.Cast
8import Prelude.Cast
9−import Prelude.Classes
9+import Prelude.Interfaces
10import Prelude.Uninhabited
10import Prelude.Uninhabited
11
11
12%access public
12%access public
@@ -224,9 +224,9 @@ record Multiplicative where
224
224
225||| A wrapper for Nat that specifies the semigroup and monad implementations that use (+)
225||| A wrapper for Nat that specifies the semigroup and monad implementations that use (+)
226record Additive where
226record Additive where
227− constructor GetAdditive
227+ constructor GetAdditive
228 _ : Nat
228 _ : Nat
229−
229+
230Semigroup Multiplicative where
230Semigroup Multiplicative where
231 (<+>) left right = GetMultiplicative $ left' * right'
231 (<+>) left right = GetMultiplicative $ left' * right'
232 where
232 where
@@ -424,7 +424,7 @@ total plusCommutative : (left : Nat) -> (right : Nat) ->
424plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
424plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
425plusCommutative (S left) right =
425plusCommutative (S left) right =
426 let inductiveHypothesis = plusCommutative left right in
426 let inductiveHypothesis = plusCommutative left right in
427− rewrite inductiveHypothesis in
427+ rewrite inductiveHypothesis in
428 rewrite plusSuccRightSucc right left in Refl
428 rewrite plusSuccRightSucc right left in Refl
429
429
430total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
430total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
@@ -450,21 +450,21 @@ total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
450plusLeftCancel Z right right' p = p
450plusLeftCancel Z right right' p = p
451plusLeftCancel (S left) right right' p =
451plusLeftCancel (S left) right right' p =
452 let inductiveHypothesis = plusLeftCancel left right right' in
452 let inductiveHypothesis = plusLeftCancel left right right' in
453− inductiveHypothesis (succInjective _ _ p)
453+ inductiveHypothesis (succInjective _ _ p)
454
454
455total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
455total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
456 (p : left + right = left' + right) -> left = left'
456 (p : left + right = left' + right) -> left = left'
457plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in
457plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in
458 rewrite sym (plusZeroRightNeutral left') in
458 rewrite sym (plusZeroRightNeutral left') in
459− p
459+ p
460plusRightCancel left left' (S right) p =
460plusRightCancel left left' (S right) p =
461− plusRightCancel left left' right
461+ plusRightCancel left left' right
462− (succInjective _ _ (rewrite plusSuccRightSucc left right in
462+ (succInjective _ _ (rewrite plusSuccRightSucc left right in
463 rewrite plusSuccRightSucc left' right in p))
463 rewrite plusSuccRightSucc left' right in p))
464
464
465total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
465total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
466 (p : left + right = left) -> right = Z
466 (p : left + right = left) -> right = Z
467−plusLeftLeftRightZero Z right p = p
467+plusLeftLeftRightZero Z right p = p
468plusLeftLeftRightZero (S left) right p =
468plusLeftLeftRightZero (S left) right p =
469 plusLeftLeftRightZero left right (succInjective _ _ p)
469 plusLeftLeftRightZero left right (succInjective _ _ p)
470
470
@@ -481,7 +481,7 @@ total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
481multRightSuccPlus Z right = Refl
481multRightSuccPlus Z right = Refl
482multRightSuccPlus (S left) right =
482multRightSuccPlus (S left) right =
483 let inductiveHypothesis = multRightSuccPlus left right in
483 let inductiveHypothesis = multRightSuccPlus left right in
484− rewrite inductiveHypothesis in
484+ rewrite inductiveHypothesis in
485 rewrite plusAssociative left right (mult left right) in
485 rewrite plusAssociative left right (mult left right) in
486 rewrite plusAssociative right left (mult left right) in
486 rewrite plusAssociative right left (mult left right) in
487 rewrite plusCommutative right left in
487 rewrite plusCommutative right left in
@@ -493,11 +493,11 @@ multLeftSuccPlus left right = Refl
493
493
494total multCommutative : (left : Nat) -> (right : Nat) ->
494total multCommutative : (left : Nat) -> (right : Nat) ->
495 left * right = right * left
495 left * right = right * left
496−multCommutative Z right = rewrite multZeroRightZero right in Refl
496+multCommutative Z right = rewrite multZeroRightZero right in Refl
497multCommutative (S left) right =
497multCommutative (S left) right =
498 let inductiveHypothesis = multCommutative left right in
498 let inductiveHypothesis = multCommutative left right in
499 rewrite inductiveHypothesis in
499 rewrite inductiveHypothesis in
500− rewrite multRightSuccPlus right left in
500+ rewrite multRightSuccPlus right left in
501 Refl
501 Refl
502
502
503total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
503total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
@@ -505,7 +505,7 @@ total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right :
505multDistributesOverPlusRight Z centre right = Refl
505multDistributesOverPlusRight Z centre right = Refl
506multDistributesOverPlusRight (S left) centre right =
506multDistributesOverPlusRight (S left) centre right =
507 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
507 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
508− rewrite inductiveHypothesis in
508+ rewrite inductiveHypothesis in
509 rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in
509 rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in
510 rewrite sym (plusAssociative centre (mult left centre) right) in
510 rewrite sym (plusAssociative centre (mult left centre) right) in
511 rewrite plusCommutative (mult left centre) right in
511 rewrite plusCommutative (mult left centre) right in
@@ -527,7 +527,7 @@ total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
527multAssociative Z centre right = Refl
527multAssociative Z centre right = Refl
528multAssociative (S left) centre right =
528multAssociative (S left) centre right =
529 let inductiveHypothesis = multAssociative left centre right in
529 let inductiveHypothesis = multAssociative left centre right in
530− rewrite inductiveHypothesis in
530+ rewrite inductiveHypothesis in
531 rewrite multDistributesOverPlusLeft centre (mult left centre) right in
531 rewrite multDistributesOverPlusLeft centre (mult left centre) right in
532 Refl
532 Refl
533
533
@@ -619,7 +619,7 @@ powerSuccPowerLeft base exp = Refl
619
619
620total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
620total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
621 (power base exp) * (power base exp') = power base (exp + exp')
621 (power base exp) * (power base exp') = power base (exp + exp')
622−multPowerPowerPlus base Z exp' =
622+multPowerPowerPlus base Z exp' =
623 rewrite sym (plusZeroRightNeutral (power base exp')) in Refl
623 rewrite sym (plusZeroRightNeutral (power base exp')) in Refl
624multPowerPowerPlus base (S exp) exp' =
624multPowerPowerPlus base (S exp) exp' =
625 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
625 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
@@ -651,7 +651,7 @@ total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
651powerPowerMultPower base exp Z = rewrite multZeroRightZero exp in Refl
651powerPowerMultPower base exp Z = rewrite multZeroRightZero exp in Refl
652powerPowerMultPower base exp (S exp') =
652powerPowerMultPower base exp (S exp') =
653 let inductiveHypothesis = powerPowerMultPower base exp exp' in
653 let inductiveHypothesis = powerPowerMultPower base exp exp' in
654− rewrite inductiveHypothesis in
654+ rewrite inductiveHypothesis in
655 rewrite multRightSuccPlus exp exp' in
655 rewrite multRightSuccPlus exp exp' in
656 rewrite sym (multPowerPowerPlus base exp (mult exp exp')) in
656 rewrite sym (multPowerPowerPlus base exp (mult exp exp')) in
657 Refl
657 Refl
@@ -664,7 +664,7 @@ total minusSuccPred : (left : Nat) -> (right : Nat) ->
664 minus left (S right) = pred (minus left right)
664 minus left (S right) = pred (minus left right)
665minusSuccPred Z right = Refl
665minusSuccPred Z right = Refl
666minusSuccPred (S left) Z =
666minusSuccPred (S left) Z =
667− rewrite minusZeroRight left in Refl
667+ rewrite minusZeroRight left in Refl
668minusSuccPred (S left) (S right) =
668minusSuccPred (S left) (S right) =
669 let inductiveHypothesis = minusSuccPred left right in
669 let inductiveHypothesis = minusSuccPred left right in
670 rewrite inductiveHypothesis in Refl
670 rewrite inductiveHypothesis in Refl
@@ -782,4 +782,3 @@ sucMinL (S l) = cong (sucMinL l)
782total sucMinR : (l : Nat) -> minimum l (S l) = l
782total sucMinR : (l : Nat) -> minimum l (S l) = l
783sucMinR Z = Refl
783sucMinR Z = Refl
784sucMinR (S l) = cong (sucMinR l)
784sucMinR (S l) = cong (sucMinR l)
785−
libs/prelude/Prelude/Show.idr+1−2
@@ -7,7 +7,7 @@ import Prelude.Bits
7import Prelude.Bool
7import Prelude.Bool
8import Prelude.Cast
8import Prelude.Cast
9import Prelude.Chars
9import Prelude.Chars
10−import Prelude.Classes
10+import Prelude.Interfaces
11import Prelude.List
11import Prelude.List
12import Prelude.Maybe
12import Prelude.Maybe
13import Prelude.Either
13import Prelude.Either
@@ -192,4 +192,3 @@ Show a => Show (Maybe a) where
192
192
193(Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
193(Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
194 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
194 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
195−
libs/prelude/Prelude/Strings.idr+2−3
@@ -8,7 +8,7 @@ import Prelude.Basics
8import Prelude.Bool
8import Prelude.Bool
9import Prelude.Chars
9import Prelude.Chars
10import Prelude.Cast
10import Prelude.Cast
11−import Prelude.Classes
11+import Prelude.Interfaces
12import Prelude.Either
12import Prelude.Either
13import Prelude.Foldable
13import Prelude.Foldable
14import Prelude.Functor
14import Prelude.Functor
@@ -112,7 +112,7 @@ strTail' x p = assert_total $ prim__strTail x
112-- we need the 'believe_me' because the operations are primitives
112-- we need the 'believe_me' because the operations are primitives
113strM : (x : String) -> StrM x
113strM : (x : String) -> StrM x
114strM x with (decEq (not (x == "")) True)
114strM x with (decEq (not (x == "")) True)
115− strM x | (Yes p) = really_believe_me $
115+ strM x | (Yes p) = really_believe_me $
116 StrCons (assert_total (strHead' x p))
116 StrCons (assert_total (strHead' x p))
117 (assert_total (strTail' x p))
117 (assert_total (strTail' x p))
118 strM x | (No p) = really_believe_me StrNil
118 strM x | (No p) = really_believe_me StrNil
@@ -364,4 +364,3 @@ partial
364nullStr : String -> IO Bool
364nullStr : String -> IO Bool
365nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p
365nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p
366 return (ok /= 0)
366 return (ok /= 0)
367−
libs/prelude/prelude.ipkg+1−2
@@ -4,7 +4,7 @@ opts = "--nobuiltins --total --no-elim-deprecation-warnings"
4modules = Builtins, Prelude, IO,
4modules = Builtins, Prelude, IO,
5
5
6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
7− Prelude.Classes, Prelude.Nat, Prelude.List,
7+ Prelude.Interfaces, Prelude.Nat, Prelude.List,
8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
9 Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,
9 Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
@@ -14,4 +14,3 @@ modules = Builtins, Prelude, IO,
14 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
14 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
15
15
16 Decidable.Equality
16 Decidable.Equality
17−
src/Idris/ProofSearch.hs+31−33
@@ -48,13 +48,13 @@ trivialHoles psnames ok elab ist
48 then try' (elab (PRef (fileFC "prf") [] x))
48 then try' (elab (PRef (fileFC "prf") [] x))
49 (tryAll xs) True
49 (tryAll xs) True
50 else tryAll xs
50 else tryAll xs
51−
51+
52 holesOK hs ap@(App _ _ _)
52 holesOK hs ap@(App _ _ _)
53 | (P _ n _, args) <- unApply ap
53 | (P _ n _, args) <- unApply ap
54 = holeArgsOK hs n 0 args
54 = holeArgsOK hs n 0 args
55 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
55 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
56 holesOK hs (P _ n _) = not (n `elem` hs)
56 holesOK hs (P _ n _) = not (n `elem` hs)
57− holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
57+ holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
58 holesOK hs sc
58 holesOK hs sc
59 holesOK hs _ = True
59 holesOK hs _ = True
60
60
@@ -85,8 +85,8 @@ trivialTCs ok elab ist
85 then try' (elab (PRef (fileFC "prf") [] x))
85 then try' (elab (PRef (fileFC "prf") [] x))
86 (tryAll xs) True
86 (tryAll xs) True
87 else tryAll xs
87 else tryAll xs
88−
88+
89− tcArg env ty
89+ tcArg env ty
90 | (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty))
90 | (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty))
91 = case lookupCtxtExact n (idris_classes ist) of
91 = case lookupCtxtExact n (idris_classes ist) of
92 Just _ -> True
92 Just _ -> True
@@ -98,7 +98,7 @@ trivialTCs ok elab ist
98 = holeArgsOK hs n 0 args
98 = holeArgsOK hs n 0 args
99 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
99 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
100 holesOK hs (P _ n _) = not (n `elem` hs)
100 holesOK hs (P _ n _) = not (n `elem` hs)
101− holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
101+ holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
102 holesOK hs sc
102 holesOK hs sc
103 holesOK hs _ = True
103 holesOK hs _ = True
104
104
@@ -111,16 +111,16 @@ cantSolveGoal :: ElabD a
111cantSolveGoal = do g <- goal
111cantSolveGoal = do g <- goal
112 env <- get_env
112 env <- get_env
113 lift $ tfail $
113 lift $ tfail $
114− CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
114+ CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
115
115
116−proofSearch :: Bool -> -- recursive search (False for 'refine')
116+proofSearch :: Bool -> -- recursive search (False for 'refine')
117 Bool -> -- invoked from a tactic proof. If so, making
117 Bool -> -- invoked from a tactic proof. If so, making
118 -- new metavariables is meaningless, and there shoudl
118 -- new metavariables is meaningless, and there shoudl
119 -- be an error reported instead.
119 -- be an error reported instead.
120 Bool -> -- ambiguity ok
120 Bool -> -- ambiguity ok
121 Bool -> -- defer on failure
121 Bool -> -- defer on failure
122 Int -> -- maximum depth
122 Int -> -- maximum depth
123− (PTerm -> ElabD ()) -> Maybe Name -> Name ->
123+ (PTerm -> ElabD ()) -> Maybe Name -> Name ->
124 [Name] ->
124 [Name] ->
125 [Name] ->
125 [Name] ->
126 IState -> ElabD ()
126 IState -> ElabD ()
@@ -131,7 +131,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]
131 tryAllFns all_imps
131 tryAllFns all_imps
132 where
132 where
133 -- if nothing worked, make a new metavariable
133 -- if nothing worked, make a new metavariable
134− tryAllFns [] | fromProver = cantSolveGoal
134+ tryAllFns [] | fromProver = cantSolveGoal
135 tryAllFns [] = do attack; defer [] nroot; solve
135 tryAllFns [] = do attack; defer [] nroot; solve
136 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
136 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
137
137
@@ -142,20 +142,20 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]
142 (match_apply (Var f) imps) True
142 (match_apply (Var f) imps) True
143 ps' <- get_probs
143 ps' <- get_probs
144-- when (length ps < length ps') $ fail "Can't apply constructor"
144-- when (length ps < length ps') $ fail "Can't apply constructor"
145− -- Make metavariables for new holes
145+ -- Make metavariables for new holes
146 hs' <- get_holes
146 hs' <- get_holes
147 ptm <- get_term
147 ptm <- get_term
148 if fromProver then cantSolveGoal
148 if fromProver then cantSolveGoal
149 else do
149 else do
150 mapM_ (\ h -> do focus h
150 mapM_ (\ h -> do focus h
151− attack; defer [] nroot; solve)
151+ attack; defer [] nroot; solve)
152 (hs' \\ hs)
152 (hs' \\ hs)
153-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
153-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
154 solve
154 solve
155
155
156 isImp (PImp p _ _ _ _) = (True, p)
156 isImp (PImp p _ _ _ _) = (True, p)
157 isImp arg = (True, priority arg) -- try to get all of them by unification
157 isImp arg = (True, priority arg) -- try to get all of them by unification
158−proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist
158+proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist
159 = do compute
159 = do compute
160 ty <- goal
160 ty <- goal
161 hs <- get_holes
161 hs <- get_holes
@@ -172,7 +172,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
172 (autoArg (sUN "auto"))
172 (autoArg (sUN "auto"))
173 else autoArg (sUN "auto") -- not enough info in the type yet
173 else autoArg (sUN "auto") -- not enough info in the type yet
174 where
174 where
175− findInferredTy (t : _) = elab (delab ist (toUN t))
175+ findInferredTy (t : _) = elab (delab ist (toUN t))
176
176
177 cantsolve (InternalMsg _) = True
177 cantsolve (InternalMsg _) = True
178 cantsolve (CantSolveGoal _ _) = True
178 cantsolve (CantSolveGoal _ _) = True
@@ -185,12 +185,12 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
185 conArgsOK ty
185 conArgsOK ty
186 = let (f, as) = unApply ty in
186 = let (f, as) = unApply ty in
187 case f of
187 case f of
188− P _ n _ ->
188+ P _ n _ ->
189 let autohints = case lookupCtxtExact n (idris_autohints ist) of
189 let autohints = case lookupCtxtExact n (idris_autohints ist) of
190 Nothing -> []
190 Nothing -> []
191 Just hs -> hs in
191 Just hs -> hs in
192 case lookupCtxtExact n (idris_datatypes ist) of
192 case lookupCtxtExact n (idris_datatypes ist) of
193− Just t -> do rs <- mapM (conReady as)
193+ Just t -> do rs <- mapM (conReady as)
194 (autohints ++ con_names t)
194 (autohints ++ con_names t)
195 return (and rs)
195 return (and rs)
196 Nothing -> -- local variable, go for it
196 Nothing -> -- local variable, go for it
@@ -199,7 +199,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
199 _ -> typeNotSearchable ty
199 _ -> typeNotSearchable ty
200
200
201 conReady :: [Term] -> Name -> ElabD Bool
201 conReady :: [Term] -> Name -> ElabD Bool
202− conReady as n
202+ conReady as n
203 = case lookupTyExact n (tt_ctxt ist) of
203 = case lookupTyExact n (tt_ctxt ist) of
204 Just ty -> do let (_, cs) = unApply (getRetTy ty)
204 Just ty -> do let (_, cs) = unApply (getRetTy ty)
205 -- if any metavariables in 'as' correspond to
205 -- if any metavariables in 'as' correspond to
@@ -223,7 +223,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
223 inHS hs (P _ n _) = n `elem` hs
223 inHS hs (P _ n _) = n `elem` hs
224 isHS _ _ = False
224 isHS _ _ = False
225
225
226− toUN t@(P nt (MN i n) ty)
226+ toUN t@(P nt (MN i n) ty)
227 | ('_':xs) <- str n = t
227 | ('_':xs) <- str n = t
228 | otherwise = P nt (UN n) ty
228 | otherwise = P nt (UN n) ty
229 toUN (App s f a) = App s (toUN f) (toUN a)
229 toUN (App s f a) = App s (toUN f) (toUN a)
@@ -239,7 +239,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
239 psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
239 psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
240 psRec _ 0 locs tys | fromProver = cantSolveGoal
240 psRec _ 0 locs tys | fromProver = cantSolveGoal
241 psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"
241 psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"
242− psRec False d locs tys = tryCons d locs tys hints
242+ psRec False d locs tys = tryCons d locs tys hints
243 psRec True d locs tys
243 psRec True d locs tys
244 = do compute
244 = do compute
245 ty <- goal
245 ty <- goal
@@ -248,11 +248,11 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
248 try' (try' (trivialHoles psnames [] elab ist)
248 try' (try' (trivialHoles psnames [] elab ist)
249 (resolveTC False False 20 ty nroot elab ist)
249 (resolveTC False False 20 ty nroot elab ist)
250 True)
250 True)
251− (try' (try' (resolveByCon (d - 1) locs tys')
251+ (try' (try' (resolveByCon (d - 1) locs tys')
252 (resolveByLocals (d - 1) locs tys')
252 (resolveByLocals (d - 1) locs tys')
253 True)
253 True)
254 -- if all else fails, make a new metavariable
254 -- if all else fails, make a new metavariable
255− (if fromProver
255+ (if fromProver
256 then fail "cantSolveGoal"
256 then fail "cantSolveGoal"
257 else do attack; defer [] nroot; solve) True) True
257 else do attack; defer [] nroot; solve) True) True
258
258
@@ -269,7 +269,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
269 = do t <- goal
269 = do t <- goal
270 let (f, _) = unApply t
270 let (f, _) = unApply t
271 case f of
271 case f of
272− P _ n _ ->
272+ P _ n _ ->
273 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
273 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
274 Nothing -> []
274 Nothing -> []
275 Just hs -> hs
275 Just hs -> hs
@@ -292,26 +292,26 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
292 tryLocals d locs tys env
292 tryLocals d locs tys env
293
293
294 tryLocals d locs tys [] = fail "Locals failed"
294 tryLocals d locs tys [] = fail "Locals failed"
295− tryLocals d locs tys ((x, t) : xs)
295+ tryLocals d locs tys ((x, t) : xs)
296 | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs
296 | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs
297− | otherwise = try' (tryLocal d (x : locs) tys x t)
297+ | otherwise = try' (tryLocal d (x : locs) tys x t)
298 (tryLocals d locs tys xs) True
298 (tryLocals d locs tys xs) True
299
299
300 tryCons d locs tys [] = fail "Constructors failed"
300 tryCons d locs tys [] = fail "Constructors failed"
301− tryCons d locs tys (c : cs)
301+ tryCons d locs tys (c : cs)
302 = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
302 = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
303
303
304− tryLocal d locs tys n t
304+ tryLocal d locs tys n t
305 = do let a = getPArity (delab ist (binderTy t))
305 = do let a = getPArity (delab ist (binderTy t))
306 tryLocalArg d locs tys n a
306 tryLocalArg d locs tys n a
307
307
308 tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)
308 tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)
309− tryLocalArg d locs tys n i
309+ tryLocalArg d locs tys n i
310 = simple_app False (tryLocalArg d locs tys n (i - 1))
310 = simple_app False (tryLocalArg d locs tys n (i - 1))
311 (psRec True d locs tys) "proof search local apply"
311 (psRec True d locs tys) "proof search local apply"
312
312
313 -- Like type class resolution, but searching with constructors
313 -- Like type class resolution, but searching with constructors
314− tryCon d locs tys n =
314+ tryCon d locs tys n =
315 do ty <- goal
315 do ty <- goal
316 let imps = case lookupCtxtExact n (idris_implicits ist) of
316 let imps = case lookupCtxtExact n (idris_implicits ist) of
317 Nothing -> []
317 Nothing -> []
@@ -341,7 +341,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
341 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
341 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
342 _ -> []
342 _ -> []
343
343
344−-- In interactive mode, only search for things if there is some
344+-- In interactive mode, only search for things if there is some
345-- index to help pick a relevant constructor
345-- index to help pick a relevant constructor
346checkConstructor :: IState -> [Name] -> ElabD ()
346checkConstructor :: IState -> [Name] -> ElabD ()
347checkConstructor ist [] = return ()
347checkConstructor ist [] = return ()
@@ -397,7 +397,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
397 _ -> []
397 _ -> []
398
398
399 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
399 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
400− try' (trivialTCs okholes elab ist)
400+ try' (trivialTCs okholes elab ist)
401 (do addDefault t tc ttypes
401 (do addDefault t tc ttypes
402 let stk = map fst (filter snd $ elab_stack ist)
402 let stk = map fst (filter snd $ elab_stack ist)
403 let insts = findInstances ist t
403 let insts = findInstances ist t
@@ -432,7 +432,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
432 tcDetArgsOK _ _ _ [] = Just []
432 tcDetArgsOK _ _ _ [] = Just []
433
433
434 isMeta :: [Name] -> Term -> Bool
434 isMeta :: [Name] -> Term -> Bool
435− isMeta ns (P _ n _) = n `elem` ns
435+ isMeta ns (P _ n _) = n `elem` ns
436 isMeta _ _ = False
436 isMeta _ _ = False
437
437
438 notHole hs (P _ n _, c)
438 notHole hs (P _ n _, c)
@@ -449,7 +449,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
449 chaser (NS n _) = chaser n
449 chaser (NS n _) = chaser n
450 chaser _ = False
450 chaser _ = False
451
451
452− numclass = sNS (sUN "Num") ["Classes","Prelude"]
452+ numclass = sNS (sUN "Num") ["Interfaces","Prelude"]
453
453
454 addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
454 addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
455 = do focus a
455 = do focus a
@@ -530,5 +530,3 @@ findInstances ist t
530 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
530 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
531 Just (_, Hidden) -> False
531 Just (_, Hidden) -> False
532 _ -> True
532 _ -> True
533−
534−
test/interactive010/expected+3−3
@@ -1,12 +1,12 @@
1Prelude.List.(++) : List a -> List a -> List a
1Prelude.List.(++) : List a -> List a -> List a
2Prelude.Strings.(++) : String -> String -> String
2Prelude.Strings.(++) : String -> String -> String
3−a is not an implicit argument of Prelude.Classes./
3+a is not an implicit argument of Prelude.Interfaces./
4Usage is :doc <functionname>
4Usage is :doc <functionname>
5Usage is :wc <functionname>
5Usage is :wc <functionname>
6Usage is :printdef <functionname>
6Usage is :printdef <functionname>
7−pat {ty504} : Type u. pat {__class505} : Prelude.Classes.Fractional {ty504}. Prelude.Classes./ {ty504} {__class505}
7+pat {ty504} : Type u. pat {__class505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__class505}
8
8
9− : pty {ty504} : Type u. pty {__class505} : Prelude.Classes.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}
9+ : pty {ty504} : Type u. pty {__class505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}
10(input):1:1: error: expected: ":",
10(input):1:1: error: expected: ":",
11 dependent type signature,
11 dependent type signature,
12 end of input
12 end of input
test/syntax001/expected+2−2
@@ -2,7 +2,7 @@ Syntax.idr:6:7-9:1:
2When checking right hand side of foo with expected type
2When checking right hand side of foo with expected type
3 Nat
3 Nat
4
4
5−When checking an application of function Prelude.Classes.+:
5+When checking an application of function Prelude.Interfaces.+:
6 Type mismatch between
6 Type mismatch between
7 String (Type of "argh")
7 String (Type of "argh")
8 and
8 and
@@ -11,7 +11,7 @@ SyntaxTest.idr:5:7-6:1:
11When checking right hand side of foo with expected type
11When checking right hand side of foo with expected type
12 Nat
12 Nat
13
13
14−When checking an application of function Prelude.Classes.+:
14+When checking an application of function Prelude.Interfaces.+:
15 Type mismatch between
15 Type mismatch between
16 String (Type of "argh")
16 String (Type of "argh")
17 and
17 and