ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-10 15:16:54 +03:00
Code Issues Projects Releases Wiki Activity

Renamed Prelude.Classes to Prelude.Interfaces

Browse Source
This commit is contained in:
Jan de Muijnck-Hughes 2016-01-26 21:56:07 +00:00
parent f7a9c280bc
commit 74926fffab
20 changed files with 107 additions and 126 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libs/prelude/Decidable/Equality.idr
View File

@ -3,7 +3,7 @@ module Decidable.Equality
import Builtins
import Prelude.Basics
import Prelude.Bool
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Either
import Prelude.List
import Prelude.Nat
@ -141,7 +141,7 @@ implementation DecEq a => DecEq (List a) where
decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
decEq (x :: xs) (y :: ys) with (decEq x y)
decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq)
decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)
@ -211,6 +211,3 @@ implementation DecEq ManagedPtr where
where primitiveEq : x = y
primitiveEq = believe_me (Refl {x})
postulate primitiveNotEq : x = y -> Void

9
libs/prelude/Prelude.idr
View File

@ -6,7 +6,7 @@ import public IO
import public Prelude.Algebra
import public Prelude.Basics
import public Prelude.Bool
import public Prelude.Classes
import public Prelude.Interfaces
import public Prelude.Cast
import public Prelude.Nat
import public Prelude.List
@ -210,7 +210,7 @@ Enum Int where
Enum Char where
toNat c = toNat (ord c)
fromNat n = chr (fromNat n)
pred c = fromNat (pred (toNat c))
syntax "[" [start] ".." [end] "]"
@ -264,12 +264,12 @@ while t b = do v <- t
------- Some error rewriting
%language ErrorReflection
private
cast_part : TT -> ErrorReportPart
cast_part (P Bound n t) = TextPart "unknown type"
cast_part x = TermPart x
%error_handler
cast_error : Err -> Maybe (List ErrorReportPart)
cast_error (CantResolve `(Cast ~x ~y))
@ -284,4 +284,3 @@ num_error : Err -> Maybe (List ErrorReportPart)
num_error (CantResolve `(Num ~x))
= Just [TermPart x, TextPart "is not a numeric type"]
num_error _ = Nothing

2
libs/prelude/Prelude/Applicative.idr
View File

@ -4,7 +4,7 @@ import Builtins
import Prelude.Basics
import Prelude.Bool
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Foldable
import Prelude.Functor

2
libs/prelude/Prelude/Bits.idr
View File

@ -6,7 +6,7 @@ import Prelude.Basics
import Prelude.Bool
import Prelude.Cast
import Prelude.Chars
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Foldable
import Prelude.Nat
import Prelude.List

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

@ -2,7 +2,7 @@ module Prelude.Chars
-- Functions operating over Chars
import Prelude.Bool
import Prelude.Classes
import Prelude.Interfaces
import Prelude.List
import Prelude.Cast
import Builtins
@ -74,5 +74,3 @@ isHexDigit x = elem (toUpper x) hexChars where
||| Returns true if the character is an octal digit.
isOctDigit : Char -> Bool
isOctDigit x = (x >= '0' && x <= '7')

8
libs/prelude/Prelude/Doubles.idr
View File

@ -1,7 +1,7 @@
module Prelude.Doubles
module Prelude.Doubles
import Builtins
import Prelude.Classes
import Prelude.Interfaces
%access public
%default total
@ -10,7 +10,7 @@ import Prelude.Classes
%lib C "m"
pi : Double
pi = 3.14159265358979323846
pi = 3.14159265358979323846
euler : Double
euler = 2.7182818284590452354
@ -59,5 +59,3 @@ floor x = prim__floatFloor x
ceiling : Double -> Double
ceiling x = prim__floatCeil x

2
libs/prelude/Prelude/Either.idr
View File

@ -4,7 +4,7 @@ import Builtins
import Prelude.Basics
import Prelude.Bool
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Maybe
import Prelude.List

10
libs/prelude/Prelude/File.idr
View File

@ -9,7 +9,7 @@ import Prelude.Strings
import Prelude.Cast
import Prelude.Bool
import Prelude.Basics
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Either
import Prelude.Show
import IO
@ -39,7 +39,7 @@ strError err = unsafePerformIO -- yeah, yeah...
(foreign FFI_C "idris_showerror" (Int -> IO String) err)
getFileError : IO FileError
getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"
getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"
(Ptr -> IO (Raw FileError)) prim__vm
return err
@ -154,7 +154,7 @@ do_fwrite : Ptr -> String -> IO (Either FileError ())
do_fwrite h s = do res <- prim_fwrite h s
if (res /= 0)
then do errno <- getErrno
if errno == 0
if errno == 0
then return (Left FileWriteError)
else do err <- getFileError
return (Left err)
@ -193,7 +193,7 @@ fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
return (p > 0)
||| Read the contents of a file into a string
partial -- might be reading something infinitely long like /dev/null ...
partial -- might be reading something infinitely long like /dev/null ...
covering
readFile : String -> IO (Either FileError String)
readFile fn = do Right h <- openFile fn Read
@ -212,7 +212,7 @@ readFile fn = do Right h <- openFile fn Read
else return (Right contents)
||| Write a string to a file
writeFile : (filepath : String) -> (contents : String) ->
writeFile : (filepath : String) -> (contents : String) ->
IO (Either FileError ())
writeFile fn contents = do
Right h <- openFile fn Write | Left err => return (Left err)

3
libs/prelude/Prelude/Foldable.idr
View File

@ -3,7 +3,7 @@ module Prelude.Foldable
import Builtins
import Prelude.Bool
import Prelude.Basics
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Algebra
%access public
@ -54,4 +54,3 @@ sum = foldr (+) 0
||| Multiply together all elements of a structure
product : (Foldable t, Num a) => t a -> a
product = foldr (*) 1

35
libs/prelude/Prelude/Interactive.idr
View File

@ -1,5 +1,5 @@
||| Various helper functions for creating simple interactive systems.
|||
|||
||| These are mostly intended for helping with teaching, in that they will allow
||| the easy creation of interactive programs without needing to teach IO
||| or Effects first, but they also capture some common patterns of interactive
@ -10,7 +10,7 @@ import Builtins
import Prelude.List
import Prelude.File
import Prelude.Bool
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Strings
import Prelude.Chars
import Prelude.Show
@ -115,19 +115,19 @@ getArgs = do n <- numArgs
||| @ onEOF the function to run on reaching end of file, returning a String
||| to output
partial
processHandle : File ->
processHandle : File ->
(state : a) ->
(onRead : a -> String -> (String, a)) ->
(onEOF : a -> String) ->
(onRead : a -> String -> (String, a)) ->
(onEOF : a -> String) ->
IO ()
processHandle h acc onRead onEOF
processHandle h acc onRead onEOF
= if !(fEOF h)
then putStr (onEOF acc)
else do Right x <- fGetLine h
| Left err => putStr (onEOF acc)
let (out, acc') = onRead acc x
putStr out
processHandle h acc' onRead onEOF
processHandle h acc' onRead onEOF
||| Process input from the standard input stream, while maintaining a state.
||| @ state the input state
@ -136,34 +136,33 @@ processHandle h acc onRead onEOF
||| @ onEOI the function to run on reaching end of input, returning a String
||| to output
partial
processStdin : (state : a) ->
(onRead : a -> String -> (String, a)) ->
processStdin : (state : a) ->
(onRead : a -> String -> (String, a)) ->
(onEOI : a -> String) -> IO ()
processStdin = processHandle stdin
||| A basic read-eval-print loop, maintaining a state
||| @ state the input state
||| @ prompt the prompt to show
||| @ prompt the prompt to show
||| @ onInput the function to run on reading input, returning a String to
||| output and a new state. Returns Nothing if the repl should exit
partial
replWith : (state : a) -> (prompt : String) ->
replWith : (state : a) -> (prompt : String) ->
(onInput : a -> String -> Maybe (String, a)) -> IO ()
replWith acc prompt fn
replWith acc prompt fn
= do putStr prompt
x <- getLine
case fn acc x of
Just (out, acc') => do putStr out
Just (out, acc') => do putStr out
replWith acc' prompt fn
Nothing => return ()
||| A basic read-eval-print loop
||| @ prompt the prompt to show
||| @ prompt the prompt to show
||| @ onInput the function to run on reading input, returning a String to
||| output
||| output
partial
repl : (prompt : String) ->
repl : (prompt : String) ->
(onInput : String -> String) -> IO ()
repl prompt fn
repl prompt fn
= replWith () prompt (\x, s => Just (fn s, ()))

20
libs/prelude/Prelude/Classes.idr → libs/prelude/Prelude/Interfaces.idr
View File

@ -1,4 +1,4 @@
module Prelude.Classes
module Prelude.Interfaces
import Builtins
import Prelude.Basics
@ -57,7 +57,7 @@ Eq Bool where
True == False = False
False == True = False
False == False = True
(Eq a, Eq b) => Eq (a, b) where
(==) (a, c) (b, d) = (a == b) && (c == d)
@ -357,7 +357,7 @@ divB8 x y = case y == 0 of
modB8 : Bits8 -> Bits8 -> Bits8
modB8 x y = case y == 0 of
False => prim__sremB8 x y
Integral Bits8 where
div = divB8
mod = modB8
@ -372,8 +372,8 @@ modB16 x y = case y == 0 of
False => prim__sremB16 x y
Integral Bits16 where
div = divB16
mod = modB16
div = divB16
mod = modB16
-- ------------------------------------------------------------------ [ Bits32 ]
divB32 : Bits32 -> Bits32 -> Bits32
@ -385,8 +385,8 @@ modB32 x y = case y == 0 of
False => prim__sremB32 x y
Integral Bits32 where
div = divB32
mod = modB32
div = divB32
mod = modB32
-- ------------------------------------------------------------------ [ Bits64 ]
divB64 : Bits64 -> Bits64 -> Bits64
@ -398,7 +398,5 @@ modB64 x y = case y == 0 of
False => prim__sremB64 x y
Integral Bits64 where
div = divB64
mod = modB64
div = divB64
mod = modB64

9
libs/prelude/Prelude/List.idr
View File

@ -5,7 +5,7 @@ import Builtins
import Prelude.Algebra
import Prelude.Basics
import Prelude.Bool
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Foldable
import Prelude.Functor
import Prelude.Maybe
@ -174,7 +174,7 @@ init' [] = Nothing
init' (x::xs) =
case xs of
[] => Just []
y::ys =>
y::ys =>
case init' $ y::ys of
Nothing => Nothing
Just j => Just $ x :: j
@ -305,7 +305,7 @@ zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
||| @ z the third list
zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
(z : List c) -> List d
zipWith3 f _ [] (z::zs) = []
zipWith3 f _ [] (z::zs) = []
zipWith3 f _ (y::ys) [] = []
zipWith3 f [] (y::ys) _ = []
zipWith3 f (x::xs) [] _ = []
@ -761,7 +761,7 @@ mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
mergeBy order [] right = right
mergeBy order left [] = left
mergeBy order (x::xs) (y::ys) =
if order x y == LT
if order x y == LT
then x :: mergeBy order xs (y::ys)
else y :: mergeBy order (x::xs) ys
@ -888,4 +888,3 @@ foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs
foldlMatchesFoldr f q [] = Refl
foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs

2
libs/prelude/Prelude/Maybe.idr
View File

@ -5,7 +5,7 @@ import Prelude.Algebra
import Prelude.Basics
import Prelude.Bool
import Prelude.Cast
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Foldable
%access public

35
libs/prelude/Prelude/Nat.idr
View File

@ -6,7 +6,7 @@ import Prelude.Algebra
import Prelude.Basics
import Prelude.Bool
import Prelude.Cast
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Uninhabited
%access public
@ -224,9 +224,9 @@ record Multiplicative where
||| A wrapper for Nat that specifies the semigroup and monad implementations that use (+)
record Additive where
constructor GetAdditive
constructor GetAdditive
_ : Nat
Semigroup Multiplicative where
(<+>) left right = GetMultiplicative $ left' * right'
where
@ -424,7 +424,7 @@ total plusCommutative : (left : Nat) -> (right : Nat) ->
plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
plusCommutative (S left) right =
let inductiveHypothesis = plusCommutative left right in
rewrite inductiveHypothesis in
rewrite inductiveHypothesis in
rewrite plusSuccRightSucc right left in Refl
total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
@ -450,21 +450,21 @@ total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
plusLeftCancel Z right right' p = p
plusLeftCancel (S left) right right' p =
let inductiveHypothesis = plusLeftCancel left right right' in
inductiveHypothesis (succInjective _ _ p)
inductiveHypothesis (succInjective _ _ p)
total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
(p : left + right = left' + right) -> left = left'
plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in
rewrite sym (plusZeroRightNeutral left') in
p
p
plusRightCancel left left' (S right) p =
plusRightCancel left left' right
(succInjective _ _ (rewrite plusSuccRightSucc left right in
plusRightCancel left left' right
(succInjective _ _ (rewrite plusSuccRightSucc left right in
rewrite plusSuccRightSucc left' right in p))
total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
(p : left + right = left) -> right = Z
plusLeftLeftRightZero Z right p = p
plusLeftLeftRightZero Z right p = p
plusLeftLeftRightZero (S left) right p =
plusLeftLeftRightZero left right (succInjective _ _ p)
@ -481,7 +481,7 @@ total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
multRightSuccPlus Z right = Refl
multRightSuccPlus (S left) right =
let inductiveHypothesis = multRightSuccPlus left right in
rewrite inductiveHypothesis in
rewrite inductiveHypothesis in
rewrite plusAssociative left right (mult left right) in
rewrite plusAssociative right left (mult left right) in
rewrite plusCommutative right left in
@ -493,11 +493,11 @@ multLeftSuccPlus left right = Refl
total multCommutative : (left : Nat) -> (right : Nat) ->
left * right = right * left
multCommutative Z right = rewrite multZeroRightZero right in Refl
multCommutative Z right = rewrite multZeroRightZero right in Refl
multCommutative (S left) right =
let inductiveHypothesis = multCommutative left right in
rewrite inductiveHypothesis in
rewrite multRightSuccPlus right left in
rewrite multRightSuccPlus right left in
Refl
total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
@ -505,7 +505,7 @@ total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right :
multDistributesOverPlusRight Z centre right = Refl
multDistributesOverPlusRight (S left) centre right =
let inductiveHypothesis = multDistributesOverPlusRight left centre right in
rewrite inductiveHypothesis in
rewrite inductiveHypothesis in
rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in
rewrite sym (plusAssociative centre (mult left centre) right) in
rewrite plusCommutative (mult left centre) right in
@ -527,7 +527,7 @@ total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
multAssociative Z centre right = Refl
multAssociative (S left) centre right =
let inductiveHypothesis = multAssociative left centre right in
rewrite inductiveHypothesis in
rewrite inductiveHypothesis in
rewrite multDistributesOverPlusLeft centre (mult left centre) right in
Refl
@ -619,7 +619,7 @@ powerSuccPowerLeft base exp = Refl
total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
(power base exp) * (power base exp') = power base (exp + exp')
multPowerPowerPlus base Z exp' =
multPowerPowerPlus base Z exp' =
rewrite sym (plusZeroRightNeutral (power base exp')) in Refl
multPowerPowerPlus base (S exp) exp' =
let inductiveHypothesis = multPowerPowerPlus base exp exp' in
@ -651,7 +651,7 @@ total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
powerPowerMultPower base exp Z = rewrite multZeroRightZero exp in Refl
powerPowerMultPower base exp (S exp') =
let inductiveHypothesis = powerPowerMultPower base exp exp' in
rewrite inductiveHypothesis in
rewrite inductiveHypothesis in
rewrite multRightSuccPlus exp exp' in
rewrite sym (multPowerPowerPlus base exp (mult exp exp')) in
Refl
@ -664,7 +664,7 @@ total minusSuccPred : (left : Nat) -> (right : Nat) ->
minus left (S right) = pred (minus left right)
minusSuccPred Z right = Refl
minusSuccPred (S left) Z =
rewrite minusZeroRight left in Refl
rewrite minusZeroRight left in Refl
minusSuccPred (S left) (S right) =
let inductiveHypothesis = minusSuccPred left right in
rewrite inductiveHypothesis in Refl
@ -782,4 +782,3 @@ sucMinL (S l) = cong (sucMinL l)
total sucMinR : (l : Nat) -> minimum l (S l) = l
sucMinR Z = Refl
sucMinR (S l) = cong (sucMinR l)

3
libs/prelude/Prelude/Show.idr
View File

@ -7,7 +7,7 @@ import Prelude.Bits
import Prelude.Bool
import Prelude.Cast
import Prelude.Chars
import Prelude.Classes
import Prelude.Interfaces
import Prelude.List
import Prelude.Maybe
import Prelude.Either
@ -192,4 +192,3 @@ Show a => Show (Maybe a) where
(Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

5
libs/prelude/Prelude/Strings.idr
View File

@ -8,7 +8,7 @@ import Prelude.Basics
import Prelude.Bool
import Prelude.Chars
import Prelude.Cast
import Prelude.Classes
import Prelude.Interfaces
import Prelude.Either
import Prelude.Foldable
import Prelude.Functor
@ -112,7 +112,7 @@ strTail' x p = assert_total $ prim__strTail x
-- we need the 'believe_me' because the operations are primitives
strM : (x : String) -> StrM x
strM x with (decEq (not (x == "")) True)
strM x | (Yes p) = really_believe_me $
strM x | (Yes p) = really_believe_me $
StrCons (assert_total (strHead' x p))
(assert_total (strTail' x p))
strM x | (No p) = really_believe_me StrNil
@ -364,4 +364,3 @@ partial
nullStr : String -> IO Bool
nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p
return (ok /= 0)

3
libs/prelude/prelude.ipkg
View File

@ -4,7 +4,7 @@ opts = "--nobuiltins --total --no-elim-deprecation-warnings"
modules = Builtins, Prelude, IO,
Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
Prelude.Classes, Prelude.Nat, Prelude.List,
Prelude.Interfaces, Prelude.Nat, Prelude.List,
Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,
Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
@ -14,4 +14,3 @@ modules = Builtins, Prelude, IO,
Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
Decidable.Equality

64
src/Idris/ProofSearch.hs
View File

@ -48,13 +48,13 @@ trivialHoles psnames ok elab ist
then try' (elab (PRef (fileFC "prf") [] x))
(tryAll xs) True
else tryAll xs
holesOK hs ap@(App _ _ _)
| (P _ n _, args) <- unApply ap
= holeArgsOK hs n 0 args
holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
holesOK hs (P _ n _) = not (n `elem` hs)
holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
holesOK hs sc
holesOK hs _ = True
@ -85,8 +85,8 @@ trivialTCs ok elab ist
then try' (elab (PRef (fileFC "prf") [] x))
(tryAll xs) True
else tryAll xs
tcArg env ty
tcArg env ty
| (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty))
= case lookupCtxtExact n (idris_classes ist) of
Just _ -> True
@ -98,7 +98,7 @@ trivialTCs ok elab ist
= holeArgsOK hs n 0 args
holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
holesOK hs (P _ n _) = not (n `elem` hs)
holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
holesOK hs sc
holesOK hs _ = True
@ -111,16 +111,16 @@ cantSolveGoal :: ElabD a
cantSolveGoal = do g <- goal
env <- get_env
lift $ tfail $
CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
proofSearch :: Bool -> -- recursive search (False for 'refine')
proofSearch :: Bool -> -- recursive search (False for 'refine')
Bool -> -- invoked from a tactic proof. If so, making
-- new metavariables is meaningless, and there shoudl
-- be an error reported instead.
Bool -> -- ambiguity ok
Bool -> -- defer on failure
Int -> -- maximum depth
(PTerm -> ElabD ()) -> Maybe Name -> Name ->
(PTerm -> ElabD ()) -> Maybe Name -> Name ->
[Name] ->
[Name] ->
IState -> ElabD ()
@ -131,7 +131,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]
tryAllFns all_imps
where
-- if nothing worked, make a new metavariable
tryAllFns [] | fromProver = cantSolveGoal
tryAllFns [] | fromProver = cantSolveGoal
tryAllFns [] = do attack; defer [] nroot; solve
tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
@ -142,20 +142,20 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]
(match_apply (Var f) imps) True
ps' <- get_probs
-- when (length ps < length ps') $ fail "Can't apply constructor"
-- Make metavariables for new holes
-- Make metavariables for new holes
hs' <- get_holes
ptm <- get_term
if fromProver then cantSolveGoal
else do
mapM_ (\ h -> do focus h
attack; defer [] nroot; solve)
attack; defer [] nroot; solve)
(hs' \\ hs)
-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
solve
isImp (PImp p _ _ _ _) = (True, p)
isImp arg = (True, priority arg) -- try to get all of them by unification
proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist
proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist
= do compute
ty <- goal
hs <- get_holes
@ -172,7 +172,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
(autoArg (sUN "auto"))
else autoArg (sUN "auto") -- not enough info in the type yet
where
findInferredTy (t : _) = elab (delab ist (toUN t))
findInferredTy (t : _) = elab (delab ist (toUN t))
cantsolve (InternalMsg _) = True
cantsolve (CantSolveGoal _ _) = True
@ -185,12 +185,12 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
conArgsOK ty
= let (f, as) = unApply ty in
case f of
P _ n _ ->
P _ n _ ->
let autohints = case lookupCtxtExact n (idris_autohints ist) of
Nothing -> []
Just hs -> hs in
case lookupCtxtExact n (idris_datatypes ist) of
Just t -> do rs <- mapM (conReady as)
Just t -> do rs <- mapM (conReady as)
(autohints ++ con_names t)
return (and rs)
Nothing -> -- local variable, go for it
@ -199,7 +199,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
_ -> typeNotSearchable ty
conReady :: [Term] -> Name -> ElabD Bool
conReady as n
conReady as n
= case lookupTyExact n (tt_ctxt ist) of
Just ty -> do let (_, cs) = unApply (getRetTy ty)
-- if any metavariables in 'as' correspond to
@ -223,7 +223,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
inHS hs (P _ n _) = n `elem` hs
isHS _ _ = False
toUN t@(P nt (MN i n) ty)
toUN t@(P nt (MN i n) ty)
| ('_':xs) <- str n = t
| otherwise = P nt (UN n) ty
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
psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
psRec _ 0 locs tys | fromProver = cantSolveGoal
psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"
psRec False d locs tys = tryCons d locs tys hints
psRec False d locs tys = tryCons d locs tys hints
psRec True d locs tys
= do compute
ty <- goal
@ -248,11 +248,11 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
try' (try' (trivialHoles psnames [] elab ist)
(resolveTC False False 20 ty nroot elab ist)
True)
(try' (try' (resolveByCon (d - 1) locs tys')
(try' (try' (resolveByCon (d - 1) locs tys')
(resolveByLocals (d - 1) locs tys')
True)
-- if all else fails, make a new metavariable
(if fromProver
(if fromProver
then fail "cantSolveGoal"
else do attack; defer [] nroot; solve) True) True
@ -269,7 +269,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
= do t <- goal
let (f, _) = unApply t
case f of
P _ n _ ->
P _ n _ ->
do let autohints = case lookupCtxtExact n (idris_autohints ist) of
Nothing -> []
Just hs -> hs
@ -292,26 +292,26 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
tryLocals d locs tys env
tryLocals d locs tys [] = fail "Locals failed"
tryLocals d locs tys ((x, t) : xs)
tryLocals d locs tys ((x, t) : xs)
| x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs
| otherwise = try' (tryLocal d (x : locs) tys x t)
| otherwise = try' (tryLocal d (x : locs) tys x t)
(tryLocals d locs tys xs) True
tryCons d locs tys [] = fail "Constructors failed"
tryCons d locs tys (c : cs)
tryCons d locs tys (c : cs)
= try' (tryCon d locs tys c) (tryCons d locs tys cs) True
tryLocal d locs tys n t
tryLocal d locs tys n t
= do let a = getPArity (delab ist (binderTy t))
tryLocalArg d locs tys n a
tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)
tryLocalArg d locs tys n i
tryLocalArg d locs tys n i
= simple_app False (tryLocalArg d locs tys n (i - 1))
(psRec True d locs tys) "proof search local apply"
-- Like type class resolution, but searching with constructors
tryCon d locs tys n =
tryCon d locs tys n =
do ty <- goal
let imps = case lookupCtxtExact n (idris_implicits ist) of
Nothing -> []
@ -341,7 +341,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
(Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
_ -> []
-- In interactive mode, only search for things if there is some
-- In interactive mode, only search for things if there is some
-- index to help pick a relevant constructor
checkConstructor :: IState -> [Name] -> ElabD ()
checkConstructor ist [] = return ()
@ -397,7 +397,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
_ -> []
traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
try' (trivialTCs okholes elab ist)
try' (trivialTCs okholes elab ist)
(do addDefault t tc ttypes
let stk = map fst (filter snd $ elab_stack ist)
let insts = findInstances ist t
@ -432,7 +432,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
tcDetArgsOK _ _ _ [] = Just []
isMeta :: [Name] -> Term -> Bool
isMeta ns (P _ n _) = n `elem` ns
isMeta ns (P _ n _) = n `elem` ns
isMeta _ _ = False
notHole hs (P _ n _, c)
@ -449,7 +449,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
chaser (NS n _) = chaser n
chaser _ = False
numclass = sNS (sUN "Num") ["Classes","Prelude"]
numclass = sNS (sUN "Num") ["Interfaces","Prelude"]
addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
= do focus a
@ -530,5 +530,3 @@ findInstances ist t
where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
Just (_, Hidden) -> False
_ -> True

6
test/interactive010/expected
View File

@ -1,12 +1,12 @@
Prelude.List.(++) : List a -> List a -> List a
Prelude.Strings.(++) : String -> String -> String
a is not an implicit argument of Prelude.Classes./
a is not an implicit argument of Prelude.Interfaces./
Usage is :doc <functionname>
Usage is :wc <functionname>
Usage is :printdef <functionname>
pat {ty504} : Type u. pat {__class505} : Prelude.Classes.Fractional {ty504}. Prelude.Classes./ {ty504} {__class505}
pat {ty504} : Type u. pat {__class505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__class505}
: pty {ty504} : Type u. pty {__class505} : Prelude.Classes.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}
: pty {ty504} : Type u. pty {__class505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}
(input):1:1: error: expected: ":",
dependent type signature,
end of input

4
test/syntax001/expected
View File

@ -2,7 +2,7 @@ Syntax.idr:6:7-9:1:
When checking right hand side of foo with expected type
Nat
When checking an application of function Prelude.Classes.+:
When checking an application of function Prelude.Interfaces.+:
Type mismatch between
String (Type of "argh")
and
@ -11,7 +11,7 @@ SyntaxTest.idr:5:7-6:1:
When checking right hand side of foo with expected type
Nat
When checking an application of function Prelude.Classes.+:
When checking an application of function Prelude.Interfaces.+:
Type mismatch between
String (Type of "argh")
and