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

Merge branch 'master' into exportiface_js

Browse Source
This commit is contained in:
Niklas Larsson 2017-09-18 12:14:17 +02:00 committed by GitHub
commit 26cb165e59
118 changed files with 619 additions and 1496 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
CHANGELOG.md
View File

@ -1,7 +1,20 @@
# New in 1.1.*
+ Addition of `Text.Literate`, a module for working with literate
source files.
## Language updates
+ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side
of any definitions in `where` clauses, provided the left-hand side of the
definition does not shadow it.
## Library Updates
+ Added `Text.Literate`, a module for working with literate source files.
+ Added `Data.IORef`, for working with mutable references in `IO`.
## Tool Updates
+ Private functions are no longer visible in the REPL except for modules
that are explicitly loaded.
# New in 1.1.1

3
codegen/idris-codegen-c/Main.hs
View File

@ -1,7 +1,6 @@
module Main where
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.ElabDecls
import Idris.Main
import Idris.Options
@ -10,8 +9,6 @@ import IRTS.Compiler
import Util.System
import Paths_idris
import Control.Monad
import System.Environment
import System.Exit

3
codegen/idris-codegen-javascript/Main.hs
View File

@ -1,15 +1,12 @@
module Main where
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.ElabDecls
import Idris.Main
import Idris.Options
import IRTS.CodegenJavaScript
import IRTS.Compiler
import Paths_idris
import System.Environment
import System.Exit

2
codegen/idris-codegen-node/Main.hs
View File

@ -1,7 +1,6 @@
module Main where
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.ElabDecls
import Idris.Main
import Idris.Options
@ -11,6 +10,7 @@ import IRTS.Compiler
import Paths_idris
import Control.Monad
import System.Environment
import System.Exit

1
idris.cabal
View File

@ -226,7 +226,6 @@ Library
, Idris.WhoCalls
, Idris.CmdOptions
, IRTS.BCImp
, IRTS.Bytecode
, IRTS.CodegenC
, IRTS.CodegenCommon

28
libs/base/Data/IORef.idr Normal file
View File

@ -0,0 +1,28 @@
module Data.IORef
export
data IORef a = MkIORef a
export
newIORef : a -> IO (IORef a)
newIORef val
= do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
pure (MkIORef ref)
export
readIORef : IORef a -> IO a
readIORef (MkIORef ref)
= do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)
pure val
export
writeIORef : IORef a -> a -> IO ()
writeIORef (MkIORef old) val
= foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
(MkRaw old) (MkRaw val)
export
modifyIORef : IORef a -> (a -> a) -> IO ()
modifyIORef ref fn
= do val <- readIORef ref
writeIORef ref (fn val)

1
libs/base/base.ipkg
View File

@ -21,6 +21,7 @@ modules = System,
Data.HVect,
Data.Complex,
Data.Erased,
Data.IORef,
Data.List,
Data.List.Views,
Data.List.Quantifiers,

108
libs/contrib/Text/Lexer.idr
View File

@ -9,7 +9,7 @@ export
data Recognise : (consumes : Bool) -> Type where
Empty : Recognise False
Fail : Recognise c
Expect : Recognise c -> Recognise False
Lookahead : (positive : Bool) -> Recognise c -> Recognise False
Pred : (Char -> Bool) -> Recognise True
SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
@ -47,18 +47,12 @@ fail = Fail
||| Positive lookahead. Never consumes input.
export
expect : Recognise c -> Recognise False
expect = Expect
expect = Lookahead True
||| Negative lookahead. Never consumes input.
export
reject : Recognise c -> Recognise False
reject Empty = Fail
reject Fail = Empty
reject (Expect x) = reject x
reject (Pred f) = Expect (Pred (not . f))
reject (SeqEat r1 r2) = reject r1 <|> Expect (SeqEat r1 (reject r2))
reject (SeqEmpty r1 r2) = reject r1 <|> Expect (SeqEmpty r1 (reject r2))
reject (Alt r1 r2) = reject r1 <+> reject r2
reject = Lookahead False
||| Recognise a specific character
export
@ -113,11 +107,25 @@ export
many : Lexer -> Recognise False
many l = opt (some l)
||| Recognise the first matching lexer from a non-empty list.
||| Recognise the first matching lexer from a Foldable. Always consumes input
||| if one of the options succeeds. Fails if the foldable is empty.
export
choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
choice (x :: []) = x
choice (x :: xs@(_ :: _)) = x <|> choice xs
choice : Foldable t => t Lexer -> Lexer
choice xs = foldr Alt Fail xs
||| Repeat the sub-lexer `l` zero or more times until the lexer
||| `stopBefore` is encountered. `stopBefore` will not be consumed.
||| Not guaranteed to consume input.
export
manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
manyUntil stopBefore l = many (reject stopBefore <+> l)
||| Repeat the sub-lexer `l` zero or more times until the lexer
||| `stopAfter` is encountered, and consume it. Guaranteed to
||| consume if `stopAfter` consumes.
export
manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
||| Recognise many instances of `l` until an instance of `end` is
||| encountered.
@ -126,6 +134,36 @@ choice (x :: xs@(_ :: _)) = x <|> choice xs
export
manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
manyTill l end = end <|> opt (l <+> manyTill l end)
%deprecate manyTill
"Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."
||| Recognise a sub-lexer at least `min` times. Consumes input unless
||| min is zero.
export
atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
atLeast Z l = many l
atLeast (S min) l = l <+> atLeast min l
||| Recognise a sub-lexer at most `max` times. Not guaranteed to
||| consume input.
export
atMost : (max : Nat) -> (l : Lexer) -> Recognise False
atMost Z _ = Empty
atMost (S k) l = atMost k l <+> opt l
||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
||| if the inputs are out of order. Consumes input unless min is zero.
export
between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
between Z max l = atMost max l
between (S min) Z _ = Fail
between (S min) (S max) l = l <+> between min max l
||| Recognise exactly `count` repeated occurrences of a sub-lexer.
||| Consumes input unless count is zero.
export
exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
exactly n l = between n n l
||| Recognise any character
export
@ -175,10 +213,10 @@ strTail start (MkStrLen str len)
scan : Recognise c -> Nat -> StrLen -> Maybe Nat
scan Empty idx str = pure idx
scan Fail idx str = Nothing
scan (Expect r) idx str
= case scan r idx str of
Just _ => pure idx
Nothing => Nothing
scan (Lookahead positive r) idx str
= if isJust (scan r idx str) == positive
then Just idx
else Nothing
scan (Pred f) idx str
= do c <- strIndex str idx
if f c
@ -220,7 +258,7 @@ digits = some digit
||| Recognise a single hexidecimal digit
export
hexDigit : Lexer
hexDigit = digit <|> oneOf "abcdefABCDEF"
hexDigit = pred isHexDigit
||| Recognise one or more hexidecimal digits
export
@ -277,6 +315,17 @@ export
spaces : Lexer
spaces = some space
||| Recognise a single newline sequence. Understands CRLF, CR, and LF
export
newline : Lexer
newline = let crlf = "\r\n" in
exact crlf <|> oneOf crlf
||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
export
newlines : Lexer
newlines = some newline
||| Recognise a single non-whitespace, non-alphanumeric character
export
symbol : Lexer
@ -291,7 +340,7 @@ symbols = some symbol
||| delimiting lexers
export
surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
surround start end l = start <+> manyTill l end
surround start end l = start <+> manyThen end l
||| Recognise zero or more occurrences of a sub-lexer surrounded
||| by the same quote lexer on both sides (useful for strings)
@ -325,7 +374,26 @@ intLit = opt (is '-') <+> digits
||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
export
hexLit : Lexer
hexLit = is '0' <+> oneOf "xX" <+> hexDigits
hexLit = approx "0x" <+> hexDigits
||| Recognise `start`, then recognise all input until a newline is encountered,
||| and consume the newline. Will succeed if end-of-input is encountered before
||| a newline.
export
lineComment : (start : Lexer) -> Lexer
lineComment start = start <+> manyUntil newline any <+> opt newline
||| Recognise all input between `start` and `end` lexers.
||| Supports balanced nesting.
|||
||| For block comments that don't support nesting (such as C-style comments),
||| use `surround`.
export
blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
blockComment start end = start <+> middle <+> end
where
middle : Recognise False
middle = manyUntil end (blockComment start end <|> any)
||| A mapping from lexers to the tokens they produce.
||| This is a list of pairs `(Lexer, String -> tokenType)`

4
libs/contrib/Text/Literate.idr
View File

@ -30,13 +30,13 @@ import Data.List.Views
%default total
untilEOL : Recognise False
untilEOL = manyTill any (is '\n')
untilEOL = manyUntil (is '\n') any
line : String -> Lexer
line s = exact s <+> space <+> untilEOL
block : String -> String -> Lexer
block s e = exact s <+> manyTill any (exact e)
block s e = exact s <+> manyUntil (exact e) any
data Token = CodeBlock String String String
| Any String

77
libs/contrib/Text/Parser.idr
View File

@ -40,18 +40,72 @@ inf False t = t
||| consumed and therefore the input is smaller)
export %inline
(>>=) : {c1 : Bool} ->
Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->
Grammar tok c1 a ->
inf c1 (a -> Grammar tok c2 b) ->
Grammar tok (c1 || c2) b
(>>=) {c1 = False} = SeqEmpty
(>>=) {c1 = True} = SeqEat
||| Sequence a grammar followed by the grammar it returns.
export
join : {c1 : Bool} ->
Grammar tok c1 (Grammar tok c2 a) ->
Grammar tok (c1 || c2) a
join {c1 = False} p = SeqEmpty p id
join {c1 = True} p = SeqEat p id
||| Give two alternative grammars. If both consume, the combination is
||| guaranteed to consume.
export
(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
(<|>) : Grammar tok c1 ty ->
Grammar tok c2 ty ->
Grammar tok (c1 && c2) ty
(<|>) = Alt
||| Allows the result of a grammar to be mapped to a different value.
export
Functor (Grammar tok c) where
map f (Empty val) = Empty (f val)
map f (Fail msg) = Fail msg
map f (Terminal g) = Terminal (\t => map f (g t))
map f (Alt x y) = Alt (map f x) (map f y)
map f (SeqEat act next)
= SeqEat act (\val => map f (next val))
map f (SeqEmpty act next)
= SeqEmpty act (\val => map f (next val))
-- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
-- so a sequence must be used.
map {c = False} f p = SeqEmpty p (Empty . f)
||| Sequence a grammar with value type `a -> b` and a grammar
||| with value type `a`. If both succeed, apply the function
||| from the first grammar to the value from the second grammar.
||| Guaranteed to consume if either grammar consumes.
export
(<*>) : {c1 : Bool} ->
Grammar tok c1 (a -> b) ->
inf c1 (Grammar tok c2 a) ->
Grammar tok (c1 || c2) b
(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
(<*>) {c1 = True} x y = SeqEat x (\f => map f y)
||| Sequence two grammars. If both succeed, use the value of the first one.
||| Guaranteed to consume if either grammar consumes.
export
(<*) : Grammar tok c1 a ->
inf c1 (Grammar tok c2 b) ->
Grammar tok (c1 || c2) a
(<*) x y = map const x <*> y
||| Sequence two grammars. If both succeed, use the value of the second one.
||| Guaranteed to consume if either grammar consumes.
export
(*>) : Grammar tok c1 a ->
inf c1 (Grammar tok c2 b) ->
Grammar tok (c1 || c2) b
(*>) x y = map (const id) x <*> y
||| Always succeed with the given value.
export
pure : (val : ty) -> Grammar tok False ty
pure = Empty
@ -98,12 +152,16 @@ data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
(val : ty) -> (more : List tok) ->
ParseResult (x :: xs ++ more) c ty
-- Take the result of an alternative branch, reset the commit flag to
-- the commit flag from the outer alternative, and weaken the 'consumes'
-- flag to take both alternatives into account
weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
ParseResult xs c ty -> ParseResult xs (whatever && c) ty
weakenRes (Failure com msg ts) = Failure com msg ts
weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
(com' : Bool) ->
ParseResult xs c ty -> ParseResult xs (whatever && c) ty
weakenRes com' (Failure com msg ts) = Failure com' msg ts
weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
shorter : (more : List tok) -> .(ys : List tok) ->
LTE (S (length more)) (S (length (ys ++ more)))
@ -138,7 +196,7 @@ doParse com xs act with (sizeAccessible xs)
= if com' -- If the alternative had committed, don't try the
-- other branch (and reset commit flag)
then Failure com msg ts
else weakenRes (doParse False xs y | sml)
else weakenRes com (doParse False xs y | sml)
-- Successfully parsed the first option, so use the outer commit flag
doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
= EmptyRes com val xs
@ -226,6 +284,9 @@ optional : Grammar tok True a -> (ifNothing : a) ->
Grammar tok False a
optional p def = p <|> pure def
||| Fold over a list of grammars until the first one succeeds.
choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a
choice xs = foldr Alt (Fail "No more options") xs
||| Parse an instance of `p` that is between `left` and `right`.
export

7
main/Main.hs
View File

@ -2,9 +2,7 @@ module Main where
import System.Exit (ExitCode(..), exitSuccess, exitWith)
import Control.Monad (unless, when, (>=>))
import Data.Foldable (foldrM)
import Data.Maybe (fromMaybe)
import Control.Monad (unless, when)
import Idris.AbsSyntax
import Idris.CmdOptions
@ -16,9 +14,6 @@ import Idris.Package
import Util.System (setupBundledCC)
import System.Exit (ExitCode(..), exitWith)
import Util.System (setupBundledCC)
processShowOptions :: [Opt] -> Idris ()
processShowOptions opts = runIO $ do
when (ShowAll `elem` opts) $ showExitIdrisInfo

8
rts/idris_gc.c
View File

@ -50,6 +50,9 @@ VAL copy(VM* vm, VAL x) {
case CT_BITS64:
cl = idris_b64CopyForGC(vm, x);
break;
case CT_REF:
cl = idris_newRefLock((VAL)(x->info.ptr), 1);
break;
case CT_FWD:
return x->info.ptr;
case CT_RAWDATA:
@ -79,7 +82,7 @@ void cheney(VM *vm) {
while(scan < vm->heap.next) {
size_t inc = *((size_t*)scan);
VAL heap_item = (VAL)(scan+sizeof(size_t));
// If it's a CT_CON or CT_STROFFSET, copy its arguments
// If it's a CT_CON, CT_REF or CT_STROFFSET, copy its arguments
switch(GETTY(heap_item)) {
case CT_CON:
ar = ARITY(heap_item);
@ -88,6 +91,9 @@ void cheney(VM *vm) {
heap_item->info.c.args[i] = newptr;
}
break;
case CT_REF:
heap_item->info.ptr = copy(vm, (VAL)(heap_item->info.ptr));
break;
case CT_STROFFSET:
heap_item->info.str_offset->str
= copy(vm, heap_item->info.str_offset->str);

20
rts/idris_rts.c
View File

@ -776,6 +776,26 @@ VAL idris_strRev(VM* vm, VAL str) {
return cl;
}
VAL idris_newRefLock(VAL x, int outerlock) {
Closure* cl = allocate(sizeof(Closure), outerlock);
SETTY(cl, CT_REF);
cl->info.ptr = (void*)x;
return cl;
}
VAL idris_newRef(VAL x) {
return idris_newRefLock(x, 0);
}
void idris_writeRef(VAL ref, VAL x) {
ref->info.ptr = (void*)x;
SETTY(ref, CT_REF);
}
VAL idris_readRef(VAL ref) {
return (VAL)(ref->info.ptr);
}
VAL idris_systemInfo(VM* vm, VAL index) {
int i = GETINT(index);
switch(i) {

10
rts/idris_rts.h
View File

@ -26,8 +26,8 @@
// Closures
typedef enum {
CT_CON, CT_INT, CT_BIGINT, CT_FLOAT, CT_STRING, CT_STROFFSET,
CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_FWD,
CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA
CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_REF,
CT_FWD, CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA
} ClosureType;
typedef struct Closure *VAL;
@ -401,6 +401,12 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i);
VAL idris_strRev(VM* vm, VAL str);
VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str);
// Support for IORefs
VAL idris_newRefLock(VAL x, int outerlock);
VAL idris_newRef(VAL x);
void idris_writeRef(VAL ref, VAL x);
VAL idris_readRef(VAL ref);
// system infox
// used indices:
// 0 returns backend

23
src/IRTS/BCImp.hs
View File

@ -1,23 +0,0 @@
{-|
Module : IRTS.BCImp
Description : Bytecode for a register/variable based VM (e.g. for generating code in an imperative language where we let the language deal with GC)
Copyright :
License : BSD3
Maintainer : The Idris Community.
-}
module IRTS.BCImp where
import Idris.Core.TT
import IRTS.Lang
import IRTS.Simplified
data Reg = RVal | L Int
data BC = NOP
toBC :: (Name, SDecl) -> (Name, [BC])
toBC (n, SFun n' args locs exp)
= (n, bc RVal exp)
bc :: Reg -> SExp -> [BC]
bc = undefined

1
src/IRTS/Bytecode.hs
View File

@ -23,7 +23,6 @@ module IRTS.Bytecode where
import Idris.Core.TT
import IRTS.Defunctionalise
import IRTS.Lang
import IRTS.Simplified
import Data.Maybe

17
src/IRTS/CodegenC.hs
View File

@ -9,12 +9,10 @@ Maintainer : The Idris Community.
module IRTS.CodegenC (codegenC) where
import Idris.AbsSyntax
import Idris.Core.TT
import IRTS.Bytecode
import IRTS.CodegenCommon
import IRTS.Defunctionalise
import IRTS.Lang
import IRTS.Simplified
import IRTS.System
@ -24,9 +22,7 @@ import Control.Monad
import Data.Bits
import Data.Char
import Data.List (intercalate, nubBy)
import Debug.Trace
import Numeric
import System.Directory
import System.Exit
import System.FilePath ((<.>), (</>))
import System.IO
@ -205,11 +201,7 @@ bcc i (MKCON l loc tag args)
= indent i ++ alloc loc tag ++
indent i ++ setArgs 0 args ++ "\n" ++
indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++
-- show (length args) ++ concatMap showArg args ++ ");\n"
where showArg r = ", " ++ creg r
setArgs i [] = ""
where setArgs i [] = ""
setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++
"); " ++ setArgs (i + 1) xs
alloc Nothing tag
@ -305,13 +297,6 @@ bcc i (CONSTCASE r code def)
iCase v (B64 w, bc) =
indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
++ concatMap (bcc (i+1)) bc ++
indent (i + 1) ++ "break;\n"
showDef i Nothing = ""
showDef i (Just c) = indent i ++ "default:\n"
++ concatMap (bcc (i+1)) c ++
indent (i + 1) ++ "break;\n"
showDefS i Nothing = ""
showDefS i (Just c) = concatMap (bcc (i+1)) c

14
src/IRTS/Compiler.hs
View File

@ -10,7 +10,6 @@ Maintainer : The Idris Community.
module IRTS.Compiler(compile, generate) where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Evaluate
@ -21,33 +20,24 @@ import Idris.Options
import Idris.Output
import IRTS.CodegenC
import IRTS.CodegenCommon
import IRTS.CodegenJavaScript
import IRTS.Defunctionalise
import IRTS.DumpBC
import IRTS.Exports
import IRTS.Inliner
import IRTS.Lang
import IRTS.LangOpts
import IRTS.Portable
import IRTS.Simplified
import Prelude hiding (id, (.))
import Control.Applicative
import Control.Category
import Control.Monad.State
import Data.IntSet (IntSet)
import qualified Data.IntSet as IS
import Data.List
import qualified Data.Map as M
import Data.Maybe
import Data.Ord
import qualified Data.Set as S
import Debug.Trace
import System.Directory
import System.Environment
import System.Exit
import System.FilePath (addTrailingPathSeparator, (</>))
import System.IO
import System.Process
@ -516,7 +506,9 @@ doForeign vs env (ret : fname : world : args)
= do let l' = toFDesc l
r' <- irTerm (sMN 0 "__foreignCall") vs env r
return (l', r')
splitArg _ = ifail "Badly formed foreign function call"
splitArg _ = ifail $ "Badly formed foreign function call: " ++
show (ret : fname : world : args)
toFDesc (Constant (Str str)) = FStr str
toFDesc tm

53
src/IRTS/Defunctionalise.hs
View File

@ -32,7 +32,6 @@ import Control.Monad
import Control.Monad.State
import Data.List
import Data.Maybe
import Debug.Trace
data DExp = DV Name
| DApp Bool Name [DExp] -- True = tail call
@ -165,32 +164,6 @@ addApps defs (n, LFun _ _ args e)
-- = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as
chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as
-- if anything in the DExp is projected from, we'll need to evaluate it,
-- but we only want to do it once, rather than every time we project.
preEval [] t = t
preEval (x : xs) t
| needsEval x t = DLet x (DV x) (preEval xs t)
| otherwise = preEval xs t
needsEval x (DApp _ _ args) = any (needsEval x) args
needsEval x (DC _ _ _ args) = any (needsEval x) args
needsEval x (DCase up e alts) = needsEval x e || any nec alts
where nec (DConCase _ _ _ e) = needsEval x e
nec (DConstCase _ e) = needsEval x e
nec (DDefaultCase e) = needsEval x e
needsEval x (DChkCase e alts) = needsEval x e || any nec alts
where nec (DConCase _ _ _ e) = needsEval x e
nec (DConstCase _ e) = needsEval x e
nec (DDefaultCase e) = needsEval x e
needsEval x (DLet n v e)
| x == n = needsEval x v
| otherwise = needsEval x v || needsEval x e
needsEval x (DForeign _ _ args) = any (needsEval x) (map snd args)
needsEval x (DOp op args) = any (needsEval x) args
needsEval x (DProj (DV x') _) = x == x'
needsEval x _ = False
eEVAL x = DApp False (sMN 0 "EVAL") [x]
data EvalApply a = EvalCase (Name -> a)
@ -222,7 +195,6 @@ toConsA ns (n, i)
-- (DApp False n (map DV (take i (genArgs 0))))))))
= mkApplyCase n ar i
| otherwise = []
where dupdate tlarg x = x
mkApplyCase fname n ar | n == ar = []
mkApplyCase fname n ar
@ -331,30 +303,7 @@ instance Show DExp where
-- 'max' branches
mkBigCase cn max arg branches
| length branches <= max = DChkCase arg branches
| otherwise = -- DChkCase arg branches -- until I think of something...
-- divide the branches into groups of at most max (by tag),
-- generate a new case and shrink, recursively
let bs = sortBy tagOrd branches
(all, def) = case (last bs) of
DDefaultCase t -> (init all, Just (DDefaultCase t))
_ -> (all, Nothing)
bss = groupsOf max all
cs = map mkCase bss in
DChkCase arg branches
where mkCase bs = DChkCase arg bs
tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t'
tagOrd (DConstCase c _) (DConstCase c' _) = compare c c'
tagOrd (DDefaultCase _) (DDefaultCase _) = EQ
tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT
tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT
tagOrd (DConstCase _ _) (DDefaultCase _) = LT
tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT
tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT
tagOrd (DDefaultCase _) (DConstCase _ _) = GT
| otherwise = DChkCase arg branches
groupsOf :: Int -> [DAlt] -> [[DAlt]]
groupsOf x [] = []

1
src/IRTS/DumpBC.hs
View File

@ -9,7 +9,6 @@ module IRTS.DumpBC where
import Idris.Core.TT
import IRTS.Bytecode
import IRTS.Lang
import IRTS.Simplified
import Data.List

10
src/IRTS/JavaScript/LangTransforms.hs
View File

@ -12,23 +12,18 @@ module IRTS.JavaScript.LangTransforms( removeDeadCode
) where
import Control.DeepSeq
import Control.Monad.Trans.State
import Data.List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as T
import Idris.Core.CaseTree
import Idris.Core.TT
import IRTS.Lang
import Data.Data
import Data.Generics.Uniplate.Data
import GHC.Generics (Generic)
deriving instance Typeable FDesc
deriving instance Data FDesc
@ -49,11 +44,6 @@ deriving instance Data LOpt
restrictKeys :: Ord k => Map k a -> Set k -> Map k a
restrictKeys m s = Map.filterWithKey (\k _ -> k `Set.member` s) m
mapMapListKeys :: Ord k => (a->a) -> [k] -> Map k a -> Map k a
mapMapListKeys _ [] x = x
mapMapListKeys f (t:r) x = mapMapListKeys f r $ Map.adjust f t x
extractGlobs :: Map Name LDecl -> LDecl -> [Name]
extractGlobs defs (LConstructor _ _ _) = []
extractGlobs defs (LFun _ _ _ e) =

3
src/IRTS/JavaScript/Name.hs
View File

@ -20,12 +20,9 @@ module IRTS.JavaScript.Name
) where
import Data.Char
import Data.List
import qualified Data.Map.Strict as Map
import Data.Text (Text)
import qualified Data.Text as T
import Idris.Core.TT
import IRTS.JavaScript.AST
jsEscape :: String -> String
jsEscape = concatMap jschar

4
src/IRTS/JavaScript/PrimOp.hs
View File

@ -16,11 +16,7 @@ module IRTS.JavaScript.PrimOp
, jsPrimCoerce
) where
import Data.Char
import Data.List
import qualified Data.Map.Strict as Map
import Data.Text (Text)
import qualified Data.Text as T
import Idris.Core.TT
import IRTS.JavaScript.AST
import IRTS.Lang

14
src/IRTS/JavaScript/Specialize.hs
View File

@ -17,10 +17,7 @@ module IRTS.JavaScript.Specialize
, qualifyN
) where
import Data.Char
import Data.List
import qualified Data.Map.Strict as Map
import Data.Text (Text)
import qualified Data.Text as T
import Idris.Core.TT
import IRTS.JavaScript.AST
@ -62,23 +59,12 @@ constructorOptimizeDB =
]
-- constructors
where
nil = const $ JsArray []
cons [h, t] = JsMethod (JsArray [h]) "concat" [t]
-- tests
--trueTest e = JsUniOp (T.pack "!") $ JsUniOp (T.pack "!") e
trueTest = id
falseTest e = JsUniOp (T.pack "!") e
emptyList e = JsBinOp "===" (JsProp e "length") (JsInt 0)
fillList e = JsBinOp ">" (JsProp e "length") (JsInt 0)
ltTest e = JsBinOp "<" e (JsInt 0)
eqTest e = JsBinOp "===" e (JsInt 0)
gtTest e = JsBinOp ">" e (JsInt 0)
noneTest e = JsBinOp "===" e JsUndefined
notNoneTest e = JsBinOp "!==" e JsUndefined
-- projections
justProj x n = x
uncons x 1 = JsArrayProj (JsInt 0) x
uncons x 2 = JsMethod x "slice" [JsInt 1]
cantProj x j = error $ "This type should be projected"
item :: String
-> String

2
src/IRTS/Lang.hs
View File

@ -13,12 +13,10 @@ module IRTS.Lang where
import Idris.Core.CaseTree
import Idris.Core.TT
import Control.Applicative hiding (Const)
import Control.Monad.State hiding (lift)
import Data.Data (Data)
import Data.List
import Data.Typeable (Typeable)
import Debug.Trace
import GHC.Generics (Generic)
data Endianness = Native | BE | LE deriving (Show, Eq)

4
src/IRTS/LangOpts.hs
View File

@ -9,14 +9,10 @@ Maintainer : The Idris Community.
module IRTS.LangOpts where
import Idris.Core.CaseTree
import Idris.Core.TT
import IRTS.Lang
import Control.Applicative hiding (Const)
import Control.Monad.State hiding (lift)
import Data.List
import Debug.Trace
inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]
inlineAll lds = let defs = addAlist lds emptyContext in

2
src/IRTS/Portable.hs
View File

@ -14,12 +14,10 @@ import Idris.Core.TT
import IRTS.Bytecode
import IRTS.CodegenCommon
import IRTS.Defunctionalise
import IRTS.Lang
import IRTS.Simplified
import Data.Aeson
import qualified Data.ByteString.Lazy as B
import qualified Data.Text as T
import System.IO
data CodegenFile = CGFile {

3
src/IRTS/Simplified.hs
View File

@ -10,12 +10,9 @@ module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
import Idris.Core.CaseTree
import Idris.Core.TT
import Idris.Core.Typecheck
import IRTS.Defunctionalise
import Control.Monad.State
import Data.Maybe
import Debug.Trace
data SExp = SV LVar
| SApp Bool Name [LVar]

1
src/Idris/ASTUtils.hs
View File

@ -52,7 +52,6 @@ import Idris.Options
import Prelude hiding (id, (.))
import Control.Applicative
import Control.Category
import Control.Monad.State.Class
import Data.Maybe

38
src/Idris/AbsSyntax.hs
View File

@ -7,6 +7,7 @@ Maintainer : The Idris Community.
-}
{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.AbsSyntax(
module Idris.AbsSyntax
@ -39,7 +40,6 @@ import System.IO.Error (tryIOError)
import Data.Generics.Uniplate.Data (descend, descendM)
import Debug.Trace
import Util.DynamicLinker
import Util.Pretty
import Util.System
@ -597,7 +597,7 @@ getHdrs :: Codegen -> Idris [String]
getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
getImported :: Idris [(FilePath, Bool)]
getImported = do i <- getIState; return (idris_imported i)
getImported = idris_imported `fmap` getIState
setErrSpan :: FC -> Idris ()
setErrSpan x = do i <- getIState;
@ -1465,28 +1465,7 @@ expandImplementationScope ist dec ps ns d = d
-- * if there's a function type, next (2)
-- * finally, everything else (3)
getPriority :: IState -> PTerm -> Int
getPriority i tm = 1 -- pri tm
where
pri (PRef _ _ n) =
case lookupP n (tt_ctxt i) of
((P (DCon _ _ _) _ _):_) -> 1
((P (TCon _ _) _ _):_) -> 1
((P Ref _ _):_) -> 1
[] -> 0 -- must be locally bound, if it's not an error...
pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
pri (PTrue _ _) = 0
pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
pri (PTyped l r) = pri l
pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
pri (PAlternative _ a as) = maximum (map pri as)
pri (PConstant _ _) = 0
pri Placeholder = 1
pri _ = 3
getPriority i tm = 1
addStatics :: Name -> Term -> PTerm -> Idris ()
addStatics n tm ptm =
@ -2013,9 +1992,6 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds []
unqualified (NS _ _) = False
unqualified _ = True
constructor (TyDecl (DCon _ _ _) _) = True
constructor _ = False
conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
vname (UN n) = True -- non qualified
@ -2202,12 +2178,8 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
-- check will not necessarily fully resolve constructor names,
-- and these bare names will otherwise get in the way of
-- impossbility checking.
| -- Just fn <- getFn f,
canBeDConName fn ctxt
| canBeDConName fn ctxt
= PApp fc f (fmap (fmap su) args)
where getFn (PRef _ _ fn) = Just fn
getFn (PApp _ f args) = getFn f
getFn _ = Nothing
su (PApp fc f args)
= PHidden (PApp fc f args)
su (PAlternative ms b alts)
@ -2264,8 +2236,6 @@ findStatics ist tm = let (ns, ss) = fs tm
(ns, ss)
fs _ = ([], [])
inOne n ns = length (filter id (map (elem n) ns)) == 1
pos ns ss (PPi p n fc t sc)
| elem n ss = do sc' <- pos ns ss sc
spos <- get

16
src/Idris/AbsSyntaxTree.hs
View File

@ -46,7 +46,6 @@ import qualified Data.Text as T
import Data.Traversable (Traversable)
import Data.Typeable
import GHC.Generics (Generic)
import Network.Socket (PortNumber)
data ElabWhat = ETypes | EDefns | EAll
@ -2201,7 +2200,6 @@ showName ist bnd ppo colour n = case ist of
showbasic (MN i s) = str s
showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
showbasic (SN s) = show s
fst3 (x, _, _) = x
colourise n t = let ctxt' = fmap tt_ctxt ist in
case ctxt' of
Nothing -> name
@ -2349,20 +2347,6 @@ implicitNamesIn uvars ist tm
addFn n = do (imps, fns) <- get
put (imps, n: fns)
notCAF [] = False
notCAF (PExp _ _ _ _ : _) = True
notCAF (_ : xs) = notCAF xs
notHidden (n, _) = case getAccessibility n of
Hidden -> False
Private -> False
_ -> True
getAccessibility n
= case lookupDefAccExact n False (tt_ctxt ist) of
Just (n,t) -> t
_ -> Public
ni 0 env (PRef _ _ n@(NS _ _))
| not (n `elem` env)
-- Never implicitly bind if there's a namespace

8
src/Idris/Apropos.hs
View File

@ -11,7 +11,7 @@ module Idris.Apropos (apropos, aproposModules) where
import Idris.AbsSyntax
import Idris.Core.Evaluate (Def(..), ctxtAlist)
import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),
Type, lookupCtxtExact, toAlist)
toAlist)
import Idris.Docstrings (DocTerm, Docstring, containsText)
import Data.List (intersperse, nub, nubBy)
@ -104,9 +104,3 @@ instance (Apropos a) => Apropos (Maybe a) where
instance (Apropos a) => Apropos [a] where
isApropos str xs = any (isApropos str) xs
defType :: Def -> Type
defType (Function t _) = t
defType (TyDecl _ t) = t
defType (Operator t _ _) = t
defType (CaseOp _ t _ _ _ _) = t

9
src/Idris/Chaser.hs
View File

@ -16,19 +16,15 @@ module Idris.Chaser(
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Error
import Idris.IBC
import Idris.Imports
import Idris.Parser
import Idris.Unlit
import Control.Monad.State
import Control.Monad.Trans
import Data.List
import Data.Time.Clock
import Debug.Trace
import System.Directory
import System.FilePath
import Util.System (readSource, writeSource)
import Util.System (readSource)
data ModuleTree = MTree { mod_path :: IFileType,
mod_needsRecheck :: Bool,
@ -62,9 +58,6 @@ getModuleFiles ts = nub $ execState (modList ts) [] where
-- when (not (ibc p) || rechk) $
mapM_ (modTree (getSrc p : path)) deps
ibc (IBC _ _) = True
ibc _ = False
chkReload False p = p
chkReload True (IBC fn src) = chkReload True src
chkReload True p = p

21
src/Idris/Completion.hs
View File

@ -5,12 +5,16 @@ Copyright :
License : BSD3
Maintainer : The Idris Community.
-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.Completion (replCompletion, proverCompletion) where
import Idris.AbsSyntax (runIO)
import Idris.AbsSyntax (getIState, runIO)
import Idris.AbsSyntaxTree
import Idris.Colours
import Idris.Core.Evaluate (ctxtAlist, definitions)
import Idris.Core.Evaluate (ctxtAlist, visibleDefinitions)
import Idris.Core.TT
import Idris.Help
import Idris.Imports (installedPackages)
@ -28,19 +32,21 @@ import qualified Data.Text as T
import System.Console.ANSI (Color)
import System.Console.Haskeline
commands :: [String]
commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]
tacticArgs :: [(String, Maybe TacticArg)]
tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics
, name <- names ]
tactics :: [String]
tactics = map fst tacticArgs
-- | Get the user-visible names from the current interpreter state.
names :: Idris [String]
names = do i <- get
let ctxt = tt_ctxt i
names = do ctxt <- tt_ctxt <$> getIState
return $
mapMaybe nameString (allNames $ definitions ctxt) ++
mapMaybe nameString (allNames $ visibleDefinitions ctxt) ++
"Type" : map fst Idris.Parser.Expr.constants
where
-- We need both fully qualified names and identifiers that map to them
@ -61,11 +67,6 @@ metavars :: Idris [String]
metavars = do i <- get
return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t,_)) -> not t) (idris_metavars i)) \\ primDefs
modules :: Idris [String]
modules = do i <- get
return $ map show $ imported i
namespaces :: Idris [String]
namespaces = do
ctxt <- fmap tt_ctxt get

4
src/Idris/Core/Binary.hs
View File

@ -13,14 +13,10 @@ module Idris.Core.Binary where
import Idris.Core.TT
import Control.Applicative ((<$>), (<*>))
import Control.DeepSeq (($!!))
import Control.Monad (liftM2)
import Data.Binary
import Data.Binary.Get
import Data.Binary.Put
import qualified Data.Text as T
import qualified Data.Text.Encoding as E
import Data.Vector.Binary
instance Binary ErrorReportPart where
put (TextPart msg) = do putWord8 0 ; put msg

62
src/Idris/Core/CaseTree.hs
View File

@ -31,14 +31,11 @@ module Idris.Core.CaseTree (
import Idris.Core.TT
import Control.Applicative hiding (Const)
import Control.Monad.Reader
import Control.Monad.State
import Data.List hiding (partition)
import qualified Data.List (partition)
import Data.Maybe
import qualified Data.Set as S
import Debug.Trace
import GHC.Generics (Generic)
data CaseDef = CaseDef [Name] !SC [Term]
@ -125,7 +122,7 @@ instance TermSize CaseAlt where
small :: Name -> [Name] -> SC -> Bool
small n args t = let as = findAllUsedArgs t args in
length as == length (nub as) &&
termsize n t < 10
termsize n t < 20
namesUsed :: SC -> [Name]
namesUsed sc = nub $ nu' [] sc where
@ -271,7 +268,6 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
= return $ CaseDef [] (UnmatchedCase (show fc ++ ":No pattern clauses")) []
sc' tc defcase phase fc cs
= let proj = phase == RunTime
vnames = fstT (head cs)
pats = map (\ (avs, l, r) ->
(avs, toPats reflect tc l, (l, r))) cs
chkPats = mapM chkAccessible pats in
@ -288,10 +284,7 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
else return t
Error err -> Error (At fc err)
where args = map (\i -> sMN i "e") [0..]
defaultCase True = STerm Erased
defaultCase False = UnmatchedCase "Error"
fstT (x, _, _) = x
lstT (_, _, x) = x
-- Check that all pattern variables are reachable by a case split
-- Otherwise, they won't make sense on the RHS.
@ -306,48 +299,6 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
acc (PSuc p : xs) n = acc (p : xs) n
acc (_ : xs) n = acc xs n
-- For each 'Case', make sure every choice is in the same type family,
-- as directed by the variable type (i.e. there is no implicit type casing
-- going on).
checkSameTypes :: [(Name, Type)] -> SC -> Bool
checkSameTypes tys (Case _ n alts)
= case lookup n tys of
Just t -> and (map (checkAlts t) alts)
_ -> and (map ((checkSameTypes tys).getSC) alts)
where
checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc
checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc
checkAlts _ (ConstCase c sc) = False
checkAlts _ _ = True
getSC (ConCase _ _ _ sc) = sc
getSC (FnCase _ _ sc) = sc
getSC (ConstCase _ sc) = sc
getSC (SucCase _ sc) = sc
getSC (DefaultCase sc) = sc
checkSameTypes _ _ = True
-- FIXME: All we're actually doing here is checking that we haven't arrived
-- at a specific constructor for a polymorphic argument. I *think* this
-- is sufficient, but if it turns out not to be, fix it!
--
-- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718
isType n t | (P (TCon _ _) _ _, _) <- unApply t = True
isType n t | (P Ref _ _, _) <- unApply t = True
isType n t = False
isConstType (I _) (AType (ATInt ITNative)) = True
isConstType (BI _) (AType (ATInt ITBig)) = True
isConstType (Fl _) (AType ATFloat) = True
isConstType (Ch _) (AType (ATInt ITChar)) = True
isConstType (Str _) StrType = True
isConstType (B8 _) (AType (ATInt _)) = True
isConstType (B16 _) (AType (ATInt _)) = True
isConstType (B32 _) (AType (ATInt _)) = True
isConstType (B64 _) (AType (ATInt _)) = True
isConstType _ _ = False
data Pat = PCon Bool Name Int [Pat]
| PConst Const
| PInferred Pat
@ -403,12 +354,6 @@ toPat reflect tc = map $ toPat' []
toPat' _ t = PAny
fixedN IT8 = "Bits8"
fixedN IT16 = "Bits16"
fixedN IT32 = "Bits32"
fixedN IT64 = "Bits64"
data Partition = Cons [Clause]
| Vars [Clause]
deriving Show
@ -666,9 +611,6 @@ argsToAlt inacc rs@((r, m) : rest) = do
where
(acc, inacc) = partitionAcc r
uniq i (UN n) = MN i n
uniq i n = n
getVar :: String -> CaseBuilder Name
getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)
@ -872,5 +814,3 @@ mkForce = mkForceSC
= SucCase sn (mkForceSC n arg rhs)
mkForceAlt n arg (DefaultCase rhs)
= DefaultCase (mkForceSC n arg rhs)
forceTm n arg t = subst n arg t

6
src/Idris/Core/Constraints.hs
View File

@ -8,15 +8,13 @@ Maintainer : The Idris Community.
-}
module Idris.Core.Constraints ( ucheck ) where
import Idris.Core.TT (ConstraintFC(..), Err'(..), FC(..), TC(..),
UConstraint(..), UExp(..))
import Idris.Core.TT (ConstraintFC(..), Err'(..), TC(..), UConstraint(..),
UExp(..))
import Control.Applicative
import Control.Monad.State.Strict
import Data.List (partition)
import qualified Data.Map.Strict as M
import qualified Data.Set as S
import Debug.Trace
-- | Check that a list of universe constraints can be satisfied.
ucheck :: S.Set ConstraintFC -> TC ()

19
src/Idris/Core/Elaborate.hs
View File

@ -16,7 +16,6 @@ module Idris.Core.Elaborate (
, module Idris.Core.ProofState
) where
import Idris.Core.DeepSeq
import Idris.Core.Evaluate
import Idris.Core.ProofState
import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,
@ -24,15 +23,9 @@ import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.Unify
import Idris.Core.WHNF
import Util.Pretty hiding (fill)
import Control.DeepSeq
import Control.Monad.State.Strict
import Data.Char
import Data.List
import Debug.Trace
data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
deriving Show
@ -614,9 +607,6 @@ prepare_apply fn imps =
lift $ tfail $ TooManyArguments n
| otherwise = fail $ "Too many arguments for " ++ show fn
doClaim ((i, _), n, t) = do claim n t
when i (movelast n)
mkMN n@(MN i _) = n
mkMN n@(UN x) = MN 99999 x
mkMN n@(SN s) = sMN 99999 (show s)
@ -673,8 +663,6 @@ apply' fillt fn imps =
| i = getNonUnify acc is as
| otherwise = getNonUnify (t : acc) is as
-- getNonUnify imps args = map fst (filter (not . snd) (zip (map snd args) (map fst imps)))
apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
apply2 fn elabs =
@ -682,7 +670,6 @@ apply2 fn elabs =
fill (raw_apply fn (map (Var . snd) args))
elabArgs (map snd args) elabs
ES (p, a) s prev <- get
let (n, hs) = unified p
end_unify
solve
where elabArgs [] [] = return $! ()
@ -700,16 +687,10 @@ apply_elab n args =
env <- get_env
claims <- doClaims (normalise ctxt env ty) args []
prep_fill n (map fst claims)
let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
elabClaims [] False claims
complete_fill
end_unify
where
priOrder Nothing Nothing = EQ
priOrder Nothing _ = LT
priOrder _ Nothing = GT
priOrder (Just (x, _)) (Just (y, _)) = compare x y
doClaims (Bind n' (Pi _ _ t _) sc) (i : is) claims =
do n <- unique_hole (mkMN n')
when (null claims) (start_unify n)

60
src/Idris/Core/Evaluate.hs
View File

@ -5,9 +5,11 @@ Copyright :
License : BSD3
Maintainer : The Idris Community.
-}
{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,
MultiParamTypeClasses, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
normaliseAll, normaliseBlocking, toValue, quoteTerm,
@ -28,20 +30,19 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
conGuarded,
Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
visibleDefinitions,
isUniverse, linearCheck, linearCheckArg) where
import Idris.Core.CaseTree
import Idris.Core.TT
import Control.Applicative hiding (Const)
import Control.Monad.State
import Data.Binary hiding (get, put)
import qualified Data.Binary as B
import Data.List
import Data.Maybe (listToMaybe)
import Debug.Trace
import GHC.Generics (Generic)
import qualified Data.Map.Strict as Map
data EvalState = ES { limited :: [(Name, Int)],
nexthole :: Int,
blocking :: Bool }
@ -205,16 +206,6 @@ unfold ctxt env ns t
finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))
finalEntry (n, r, b) = (n, r, fmap finalise b)
bindEnv :: EnvTT n -> TT n -> TT n
bindEnv [] tm = tm
bindEnv ((n, r, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
bindEnv ((n, r, b):bs) tm = Bind n b (bindEnv bs tm)
unbindEnv :: EnvTT n -> TT n -> TT n
unbindEnv [] tm = tm
unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."
usable :: Bool -- specialising
-> Bool -- unfolding only
-> Int -- Reduction depth limit (when simplifying/at REPL)
@ -392,22 +383,6 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
evApply ntimes stk top env args f
= apply ntimes stk top env f args
reapply ntimes stk top env f@(VP Ref n ty) args
= let val = lookupDefAccExact n (spec || (atRepl && noFree env) || runtime) ctxt in
case val of
Just (CaseOp ci _ _ _ _ cd, acc) ->
let (ns, tree) = getCases cd in
do c <- evCase ntimes n (n:stk) top env ns args tree
case c of
(Nothing, _) -> return $ unload env (VP Ref n ty) args
(Just v, rest) -> evApply ntimes stk top env rest v
_ -> case args of
(a : as) -> return $ unload env f (a : as)
[] -> return f
reapply ntimes stk top env (VApp f a) args
= reapply ntimes stk top env f (a : args)
reapply ntimes stk top env v args = return v
apply ntimes stk top env (VBind True n (Lam _ t) sc) (a:as)
= do a' <- sc a
app <- apply ntimes stk top env a' as
@ -740,13 +715,6 @@ convEq ctxt holes topx topy = ceq [] topx topy where
(caseeq ((x,y):ps) xdef ydef)
_ -> return False
-- SPECIALISATION -----------------------------------------------------------
-- We need too much control to be able to do this by tweaking the main
-- evaluator
spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
spec ctxt statics genv tm = error "spec undefined"
-- CONTEXTS -----------------------------------------------------------------
{-| A definition is either a simple function (just an expression with a type),
@ -983,8 +951,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
( CaseDef args_ct sc_ct _,
CaseDef args_rt sc_rt _) ->
let inl = alwaysInline -- tcdict
inlc = (inl || small n args_ct sc_ct) && (not asserted)
inlr = inl || small n args_rt sc_rt
inlc = (inl || small n args_rt sc_rt) && (not asserted)
cdef = CaseDefs (args_ct, sc_ct)
(args_rt, sc_rt)
op = (CaseOp (ci { case_inlinable = inlc })
@ -1152,6 +1119,14 @@ conGuarded ctxt n tm = guarded n tm
isConName f ctxt = any (guarded n) as
guarded _ _ = False
visibleDefinitions :: Context -> Ctxt TTDecl
visibleDefinitions ctxt =
Map.filter (\m -> length m > 0) . Map.map onlyVisible . definitions $ ctxt
where
onlyVisible = Map.filter visible
visible (_def, _rigCount, _injectivity, accessibility, _totality, _metaInformation) =
accessibility `notElem` [Hidden, Private]
lookupP :: Name -> Context -> [Term]
lookupP = lookupP_all False False
@ -1240,13 +1215,6 @@ linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)
tfail $ Msg $ show f ++ " can only appear in a linear binding"
_ -> return ()
checkArgs (Bind n (Pi RigW _ ty _) sc)
= do mapM_ checkNameOK (allTTNames ty)
checkArgs (substV (P Bound n Erased) sc)
checkArgs (Bind n (Pi _ _ _ _) sc)
= checkArgs (substV (P Bound n Erased) sc)
checkArgs _ = return ()
-- Check if a name is reducible in the type checker. Partial definitions
-- are not reducible (so treated as a constant)
tcReducible :: Name -> Context -> Bool

41
src/Idris/Core/Execute.hs
View File

@ -11,7 +11,6 @@ Maintainer : The Idris Community.
module Idris.Core.Execute (execute) where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
@ -22,15 +21,11 @@ import IRTS.Lang (FDesc(..), FType(..))
import Util.DynamicLinker
import Util.System
import Control.Applicative hiding (Const)
import Control.Exception
import Control.Monad hiding (forM)
import Control.Monad.Trans
import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
import Control.Monad.Trans.State.Strict
import Data.Bits
import Data.IORef
import qualified Data.Map as M
import Data.Maybe
import Data.Time.Clock.POSIX (getPOSIXTime)
import Data.Traversable (forM)
@ -42,7 +37,6 @@ import System.IO.Unsafe
#ifdef IDRIS_FFI
import Foreign.C.String
import Foreign.LibFFI
import Foreign.Marshal.Alloc (free)
import Foreign.Ptr
#endif
@ -51,10 +45,6 @@ execute :: Term -> Idris Term
execute tm = fail "libffi not supported, rebuild Idris with -f FFI"
#else
-- else is rest of file
readMay :: (Read a) => String -> Maybe a
readMay s = case reads s of
[(x, "")] -> Just x
_ -> Nothing
data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
@ -170,9 +160,6 @@ runExec ex st = fst <$> runStateT (runExceptT ex) st
getExecState :: Exec ExecState
getExecState = lift get
putExecState :: ExecState -> Exec ()
putExecState = lift . put
execFail :: Err -> Exec a
execFail = throwE
@ -481,8 +468,8 @@ execForeign env ctxt arity ty fn xs onfail
execForeign env ctxt arity ty fn xs onfail
= case foreignFromTT arity ty fn xs of
Just ffun@(FFun f argTs retT) | length xs >= arity ->
do let (args', xs') = (take arity xs, -- foreign args
drop arity xs) -- rest
do let (_, xs') = (take arity xs, -- foreign args
drop arity xs) -- rest
res <- call ffun (map snd argTs)
case res of
Nothing -> fail $ "Could not call foreign function \"" ++ f ++
@ -710,26 +697,6 @@ foreignFromTT arity ty (EConstant (Str name)) args
return $ FFun name argFTyVals (toFDesc ty)
foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing
getFTy :: ExecVal -> Maybe FType
getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
| fi == txt "FIntT" =
case str intTy of
"ITNative" -> Just (FArith (ATInt ITNative))
"ITChar" -> Just (FArith (ATInt ITChar))
"IT8" -> Just (FArith (ATInt (ITFixed IT8)))
"IT16" -> Just (FArith (ATInt (ITFixed IT16)))
"IT32" -> Just (FArith (ATInt (ITFixed IT32)))
"IT64" -> Just (FArith (ATInt (ITFixed IT64)))
_ -> Nothing
getFTy (EP _ (UN t) _) =
case str t of
"FFloat" -> Just (FArith ATFloat)
"FString" -> Just FString
"FPtr" -> Just FPtr
"FUnit" -> Just FUnit
_ -> Nothing
getFTy _ = Nothing
unEList :: ExecVal -> Maybe [ExecVal]
unEList tm = case unApplyV tm of
(nil, [_]) -> Just []
@ -739,10 +706,6 @@ unEList tm = case unApplyV tm of
(f, args) -> Nothing
toConst :: Term -> Maybe Const
toConst (Constant c) = Just c
toConst _ = Nothing
mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM f [] = return []
mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

68
src/Idris/Core/ProofState.hs
View File

@ -28,11 +28,9 @@ import Idris.Core.WHNF
import Util.Pretty hiding (fill)
import Control.Applicative hiding (empty)
import Control.Arrow ((***))
import Control.Monad.State.Strict
import Data.List
import Debug.Trace
data ProofState = PS { thname :: Name,
holes :: [Name], -- ^ holes still to be solved
@ -181,7 +179,6 @@ match_unify' :: Context -> Env ->
match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
do ps <- get
let while = while_elaborating ps
let dont = dontunify ps
let inj = injective ps
traceWhen (unifylog ps)
("Matching " ++ show (topx, topy) ++
@ -494,15 +491,6 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
Nothing -> error ("deferType can't find " ++ show n)
deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."
regret :: RunTactic
regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
do action (\ps -> let hs = holes ps in
ps { holes = hs \\ [x] })
return sc
regret ctxt env (Bind x (Hole t) _)
= fail $ show x ++ " : " ++ show t ++ " is not solved..."
regret _ _ _ = fail "The current focus is not a hole."
unifyGoal :: Raw -> RunTactic
unifyGoal tm ctxt env h@(Bind x b sc) =
do (tmv, _) <- lift $ check ctxt env tm
@ -529,14 +517,8 @@ exact _ _ _ _ = fail "Can't fill here."
fill :: Raw -> RunTactic
fill guess ctxt env (Bind x (Hole ty) sc) =
do (val, valty) <- lift $ check ctxt env guess
-- let valtyn = normalise ctxt env valty
-- let tyn = normalise ctxt env ty
ns <- unify' ctxt env (valty, Just $ SourceTerm val)
(ty, Just (chkPurpose val ty))
ps <- get
let (uh, uns) = unified ps
-- put (ps { unified = (uh, uns ++ ns) })
-- addLog (show (uh, uns ++ ns))
unify' ctxt env (valty, Just $ SourceTerm val)
(ty, Just (chkPurpose val ty))
return $ Bind x (Guess ty val) sc
where
-- some expected types show up commonly in errors and indicate a
@ -552,14 +534,8 @@ fill _ _ _ _ = fail "Can't fill here."
match_fill :: Raw -> RunTactic
match_fill guess ctxt env (Bind x (Hole ty) sc) =
do (val, valty) <- lift $ check ctxt env guess
-- let valtyn = normalise ctxt env valty
-- let tyn = normalise ctxt env ty
ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)
(ty, Just ExpectedType)
ps <- get
let (uh, uns) = unified ps
-- put (ps { unified = (uh, uns ++ ns) })
-- addLog (show (uh, uns ++ ns))
match_unify' ctxt env (valty, Just $ SourceTerm val)
(ty, Just ExpectedType)
return $ Bind x (Guess ty val) sc
match_fill _ _ _ _ = fail "Can't fill here."
@ -573,11 +549,8 @@ complete_fill :: RunTactic
complete_fill ctxt env (Bind x (Guess ty val) sc) =
do let guess = forget val
(val', valty) <- lift $ check ctxt env guess
ns <- unify' ctxt env (valty, Just $ SourceTerm val')
(ty, Just ExpectedType)
ps <- get
let (uh, uns) = unified ps
-- put (ps { unified = (uh, uns ++ ns) })
unify' ctxt env (valty, Just $ SourceTerm val')
(ty, Just ExpectedType)
return $ Bind x (Guess ty val) sc
complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
@ -588,7 +561,6 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
solve :: RunTactic
solve ctxt env (Bind x (Guess ty val) sc)
= do ps <- get
let (uh, uns) = unified ps
dropdots <-
case lookup x (notunified ps) of
Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
@ -605,7 +577,7 @@ solve ctxt env (Bind x (Guess ty val) sc)
recents = x : recents ps,
implementations = implementations ps \\ [x],
dotted = dropUnified dropdots (dotted ps) })
let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in
let (locked, _) = tryLock (holes ps \\ [x]) (updsubst x val sc) in
return locked
where dropUnified ddots [] = []
dropUnified ddots ((x, es) : ds)
@ -630,7 +602,6 @@ solve ctxt env (Bind x (Guess ty val) sc)
(Bind n (Let ty' val') sc', tyl && vall && scl)
tryLock hs t@(Bind n b sc)
= let (bt', btl) = tryLock hs (binderTy b)
(val', vall) = tryLock hs val
(sc', scl) = tryLock hs sc in
(Bind n (b { binderTy = bt' }) sc', btl && scl)
tryLock hs t = (t, True)
@ -656,13 +627,9 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
x@(Bind y (Pi _ _ s _) _) -> x
_ -> normalise ctxt env t
(tyv, tyt) <- lift $ check ctxt env ty
-- ns <- lift $ unify ctxt env tyv t'
case t' of
Bind y (Pi rig _ s _) t -> let t' = updsubst y (P Bound n s) t in
do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
ps <- get
let (uh, uns) = unified ps
-- put (ps { unified = (uh, uns ++ ns) })
do unify' ctxt env (s, Nothing) (tyv, Nothing)
return $ Bind n (Lam rig tyv) (Bind x (Hole t') (P Bound x t'))
_ -> lift $ tfail $ CantIntroduce t'
introTy ty n ctxt env _ = fail "Can't introduce here."
@ -760,7 +727,7 @@ casetac :: Raw -> Bool -> RunTactic
casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
(tmv, tmt) <- lift $ check ctxt env tm
let tmt' = normalise ctxt env tmt
let (tacn, tacstr, tactt) = if induction
let (tacn, tacstr, _) = if induction
then (ElimN, "eliminator", "Induction")
else (CaseN (FC' emptyFC), "case analysis", "Case analysis")
case unApply tmt' of
@ -773,13 +740,9 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
_ -> return []
let (params, indicies) = splitTyArgs param_pos tyargs
let args = getArgTys elimTy
let pmargs = take (length params) args
let args' = drop (length params) args
let propTy = head args'
let restargs = init $ tail args'
let consargs = take (length restargs - length indicies) restargs
let indxargs = drop (length restargs - length indicies) restargs
let scr = last $ tail args'
let indxnames = makeIndexNames indicies
currentNames <- query $ allTTNames . getProofTerm . pterm
let tmnm = case tm of
@ -801,8 +764,7 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
_ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")
tmt'
where scname = sMN 0 "scarg"
makeConsArg (nm, ty) = P Bound nm ty
where makeConsArg (nm, ty) = P Bound nm ty
bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
bindConsArgs [] v = v
addConsHole (nm, ty) =
@ -881,8 +843,6 @@ start_unify :: Name -> RunTactic
start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
return tm
tmap f (a, b, c) = (f a, b, c)
solve_unified :: RunTactic
solve_unified ctxt env tm =
do ps <- get
@ -931,14 +891,6 @@ updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)
(updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc
updateError ns e = e
updateRes ns [] = []
updateRes ns ((x, t) : ts) = (x, updateSolvedTerm ns t) : updateRes ns ts
solveInProblems x val [] = []
solveInProblems x val ((l, r, env, err) : ps)
= ((psubst x val l, psubst x val r,
updateEnv [(x, val)] env, err) : solveInProblems x val ps)
mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
mergeNotunified env holes ns = mnu ns [] [] where
mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

13
src/Idris/Core/ProofTerm.hs
View File

@ -18,11 +18,8 @@ module Idris.Core.ProofTerm(
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Control.Monad.State.Strict
import Data.List
import Debug.Trace
-- | A zipper over terms, in order to efficiently update proof terms.
data TermPath = Top
@ -198,16 +195,6 @@ updateSolvedTerm' xs x = updateSolved' xs x where
updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in
if u then (b { binderTy = ty' }, u) else (b, False)
noneOf ns (P _ n _) | n `elem` ns = False
noneOf ns (App s f a) = noneOf ns a && noneOf ns f
noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t
noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b
where
noneOfB ns (Let t v) = noneOf ns t && noneOf ns v
noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v
noneOfB ns b = noneOf ns (binderTy b)
noneOf ns _ = True
-- | As 'subst', in TT, but takes advantage of knowing not to substitute
-- under Complete applications.
updsubst :: Eq n => n {-^ The id to replace -} ->

27
src/Idris/Core/TT.hs
View File

@ -60,31 +60,25 @@ import Util.Pretty hiding (Str)
-- Work around AMP without CPP
import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,
Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),
Read(..), Show(..), String, div, error, flip, fst, mod, not,
otherwise, read, snd, ($), (&&), (.), (||))
Show(..), String, div, error, fst, mod, not, otherwise, read,
snd, ($), (&&), (.), (||))
import Control.Applicative (Alternative, Applicative(..))
import qualified Control.Applicative as A (Alternative(..))
import Control.DeepSeq (($!!))
import Control.Monad.State.Strict
import Control.Monad.Trans.Except (Except(..))
import Data.Binary hiding (get, put)
import qualified Data.Binary as B
import Data.Char
import Data.Data (Data)
import Data.Foldable (Foldable)
import Data.List hiding (group, insert)
import qualified Data.Map.Strict as Map
import Data.Maybe (listToMaybe)
import Data.Monoid (mconcat)
import Data.Set (Set, fromList, insert, member)
import qualified Data.Text as T
import Data.Traversable (Traversable)
import Data.Typeable (Typeable)
import Data.Vector.Unboxed (Vector)
import qualified Data.Vector.Unboxed as V
import Debug.Trace
import Foreign.Storable (sizeOf)
import GHC.Generics (Generic)
import Numeric (showIntAtBase)
import Numeric.IEEE (IEEE(identicalIEEE))
@ -436,13 +430,6 @@ instance Show a => Show (TC a) where
tfail :: Err -> TC a
tfail e = Error e
failMsg :: String -> TC a
failMsg str = Error (Msg str)
trun :: FC -> TC a -> TC a
trun fc (OK a) = OK a
trun fc (Error e) = Error (At fc e)
discard :: Monad m => m a -> m ()
discard f = f >> return ()
@ -515,9 +502,6 @@ deriving instance Binary SpecialName
sImplementationN :: Name -> [String] -> SpecialName
sImplementationN n ss = ImplementationN n (map T.pack ss)
sParentN :: Name -> String -> SpecialName
sParentN n s = ParentN n (T.pack s)
instance Sized Name where
size (UN n) = 1
size (NS n els) = 1 + length els
@ -704,13 +688,6 @@ nativeTyWidth IT16 = 16
nativeTyWidth IT32 = 32
nativeTyWidth IT64 = 64
{-# DEPRECATED intTyWidth "Non-total function, use nativeTyWidth and appropriate casing" #-}
intTyWidth :: IntTy -> Int
intTyWidth (ITFixed n) = nativeTyWidth n
intTyWidth ITNative = 8 * sizeOf (0 :: Int)
intTyWidth ITChar = error "IRTS.Lang.intTyWidth: Characters have platform and backend dependent width"
intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"
data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
| B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64
| AType ArithTy | StrType

34
src/Idris/Core/Typecheck.hs
View File

@ -13,11 +13,8 @@ module Idris.Core.Typecheck where
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.WHNF
import Control.Monad.State
import qualified Data.Vector.Unboxed as V (length)
import Debug.Trace
-- To check conversion, normalise each term wrt the current environment.
-- Since we haven't converted everything to de Bruijn indices yet, we'll have to
@ -208,12 +205,6 @@ check' holes tcns ctxt env top
Just v' -> v'
(tv, tt, tns) <- chk Rig0 st (Just maxu) ((n, Rig0, Pi Rig0 i sv kv) : envZero env) t
-- convertsC ctxt env st (TType maxu)
-- convertsC ctxt env tt (TType maxu)
-- when holes $ put (v, cs)
-- return (Bind n (Pi i (uniqueBinders (map fst env) sv) (TType maxu))
-- (pToV n tv), TType maxu)
case (normalise ctxt env st, normalise ctxt env tt) of
(TType su, TType tu) -> do
when (not holes) $ do (v, cs) <- get
@ -227,21 +218,6 @@ check' holes tcns ctxt env top
return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')
(pToV n tv), k', sns ++ tns)
where mkUniquePi kv (Bind n (Pi rig i s k) sc)
= let k' = smaller kv k in
Bind n (Pi rig i s k') (mkUniquePi k' sc)
mkUniquePi kv (Bind n (Lam rig t) sc)
= Bind n (Lam rig (mkUniquePi kv t)) (mkUniquePi kv sc)
mkUniquePi kv (Bind n (Let t v) sc)
= Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)
mkUniquePi kv t = t
-- Kind of the whole thing is the kind of the most unique thing
-- in the environment (because uniqueness taints everything...)
mostUnique [] k = k
mostUnique (Pi _ _ _ pk : es) k = mostUnique es (smaller pk k)
mostUnique (_ : es) k = mostUnique es k
chk rigc u lvl env (RBind n b sc)
= do (b', bt', bns) <- checkBinder b
(scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc
@ -264,7 +240,6 @@ check' holes tcns ctxt env top
checkBinder (Lam rig t)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
let tv' = normalise ctxt env tv
convType tcns ctxt env tt
return (Lam rig tv, tt, [])
checkBinder (Let t v)
@ -273,14 +248,12 @@ check' holes tcns ctxt env top
-- (or rather, like an application of a lambda, multiply)
-- (Consider: adding a single use let?)
(vv, vt, vns) <- chk (rigMult rigc RigW) u Nothing env v
let tv' = normalise ctxt env tv
convertsC ctxt env vt tv
convType tcns ctxt env tt
return (Let tv vv, tt, vns)
checkBinder (NLet t v)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
(vv, vt, vns) <- chk rigc u Nothing env v
let tv' = normalise ctxt env tv
convertsC ctxt env vt tv
convType tcns ctxt env tt
return (NLet tv vv, tt, vns)
@ -288,12 +261,10 @@ check' holes tcns ctxt env top
| not holes = lift $ tfail (IncompleteTerm undefined)
| otherwise
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
let tv' = normalise ctxt env tv
convType tcns ctxt env tt
return (Hole tv, tt, [])
checkBinder (GHole i ns t)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
let tv' = normalise ctxt env tv
convType tcns ctxt env tt
return (GHole i ns tv, tt, [])
checkBinder (Guess t v)
@ -301,20 +272,15 @@ check' holes tcns ctxt env top
| otherwise
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
(vv, vt, vns) <- chk rigc u Nothing env v
let tv' = normalise ctxt env tv
convertsC ctxt env vt tv
convType tcns ctxt env tt
return (Guess tv vv, tt, vns)
checkBinder (PVar rig t)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
let tv' = normalise ctxt env tv
convType tcns ctxt env tt
-- Normalised version, for erasure purposes (it's easier
-- to tell if it's a collapsible variable)
return (PVar rig tv, tt, [])
checkBinder (PVTy t)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
let tv' = normalise ctxt env tv
convType tcns ctxt env tt
return (PVTy tv, tt, [])

90
src/Idris/Core/Unify.hs
View File

@ -22,11 +22,9 @@ module Idris.Core.Unify(
import Idris.Core.Evaluate
import Idris.Core.TT
import Control.Monad
import Control.Monad.State.Strict
import Data.List
import Data.Maybe
import Debug.Trace
-- terms which need to be injective, with the things we're trying to unify
-- at the time
@ -39,7 +37,6 @@ data FailContext = FailContext { fail_sourceloc :: FC,
}
deriving (Eq, Show)
type Injs = [(TT Name, TT Name, TT Name)]
type Fails = [(TT Name, TT Name, -- unification error
Bool, -- ready to retry yet
Env, Err, [FailContext], FailAt)]
@ -57,10 +54,6 @@ unrecoverable = any bad
data UInfo = UI Int Fails
deriving Show
data UResult a = UOK a
| UPartOK a
| UFail Err
-- | Smart constructor for unification errors that takes into account the FailContext
cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
@ -191,16 +184,10 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
| otherwise = checkScope ns (x, tm)
checkScope ns (x, tm) =
-- case boundVs (envPos x 0 env) tm of
-- [] -> return [(x, tm)]
-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
-- (impl ns tm) (errEnv env))
let v = highV (-1) tm in
if v >= length ns
then lift $ tfail (Msg "SCOPE ERROR")
else return [(x, bind v ns tm)]
where impl [] tm = tm
impl ((n, _) : ns) tm = impl ns (substV (P Bound n Erased) tm)
bind i ns tm
| i < 0 = tm
@ -257,20 +244,6 @@ trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPa
followSols vs (n : ns) = do ns' <- followSols vs ns
return $ n : ns'
expandLets env (x, tm) = (x, doSubst (reverse env) tm)
where
doSubst [] tm = tm
doSubst ((n, Let v t) : env) tm
= doSubst env (subst n v tm)
doSubst (_ : env) tm
= doSubst env tm
hasv :: TT Name -> Bool
hasv (V x) = True
hasv (App _ f a) = hasv f || hasv a
hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
hasv _ = False
unify :: Context -> Env ->
(TT Name, Maybe Provenance) ->
(TT Name, Maybe Provenance) ->
@ -297,10 +270,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
Error e -> tfail e
where
headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
headDiff _ _ = False
injective (P (DCon _ _ _) _ _) = True
injective (P (TCon _ _) _ _) = True
-- injective (P Ref n _)
@ -327,10 +296,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
sc i = do UI s f <- get
put (UI (s+i) f)
errors :: StateT UInfo TC Bool
errors = do UI s f <- get
return (not (null f))
uplus u1 u2 = do UI s f <- get
r <- u1
UI s f' <- get
@ -342,12 +307,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
StateT UInfo
TC [(Name, TT Name)]
un = un' env
-- un fn names x y
-- = let (xf, _) = unApply x
-- (yf, _) = unApply y in
-- if headDiff xf yf then unifyFail x y else
-- uplus (un' fn names x y)
-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
StateT UInfo
@ -577,26 +536,11 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
= unifyFail appx appy
checkHeads _ _ = return []
numArgs tm = let (f, args) = unApply tm in length args
metavarApp tm = let (f, args) = unApply tm in
(metavar f &&
all (\x -> metavarApp x) args
&& nub args == args) ||
globmetavar tm
metavarArgs tm = let (f, args) = unApply tm in
all (\x -> metavar x || inenv x) args
&& nub args == args
metavarApp' tm = let (f, args) = unApply tm in
all (\x -> pat x || metavar x) (f : args)
&& nub args == args
rigid (P (DCon _ _ _) _ _) = True
rigid (P (TCon _ _) _ _) = True
rigid t@(P Ref _ _) = inenv t || globmetavar t
rigid (Constant _) = True
rigid (App _ f a) = rigid f && rigid a
rigid t = not (metavar t) || globmetavar t
globmetavar t = case unApply t of
(P _ x _, _) ->
@ -610,14 +554,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
(x `elem` holes || holeIn env x))
|| globmetavar t
_ -> False
pat t = case t of
P _ x _ -> x `elem` holes || patIn env x
_ -> False
inenv t = case t of
P _ x _ -> x `elem` (map fstEnv env)
_ -> False
notFn t = injective t || metavar t || inenv t
injectiveTC t@(P Ref n _) t'@(P Ref n' _)
| Just ni <- lookupInjectiveExact n ctxt,
@ -682,16 +618,10 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
| otherwise = checkScope ns (x, tm)
checkScope ns (x, tm) | pureTerm tm =
-- case boundVs (envPos x 0 env) tm of
-- [] -> return [(x, tm)]
-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
-- (impl ns tm) (errEnv env))
let v = highV (-1) tm in
if v >= length ns
then lift $ tfail (Msg "SCOPE ERROR")
else return [(x, bind v ns tm)]
where impl [] tm = tm
impl (((n, _), _) : ns) tm = impl ns (substV (P Bound n Erased) tm)
checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
bind i ns tm
@ -710,15 +640,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
sc 1
combine env bnames as (ns' ++ bs)
boundVs :: Int -> Term -> [Int]
boundVs i (V j) | j < i = []
| otherwise = [j]
boundVs i (Bind n b sc) = boundVs (i + 1) sc
boundVs i (App _ f x) = let fs = boundVs i f
xs = boundVs i x in
nub (fs ++ xs)
boundVs i _ = []
highV :: Int -> Term -> Int
highV i (V j) | j > i = j
| otherwise = i
@ -726,11 +647,6 @@ highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
highV i (App _ f x) = max (highV i f) (highV i x)
highV i _ = i
envPos x i [] = 0
envPos x i ((y, _) : ys) | x == y = i
| otherwise = envPos x (i + 1) ys
-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
-- more work may help.
-- FIXME: Depending on how overloading gets used, this may cause problems. Better
@ -796,9 +712,3 @@ holeIn env n = case lookupBinder n env of
Just (Hole _) -> True
Just (Guess _ _) -> True
_ -> False
patIn :: Env -> Name -> Bool
patIn env n = case lookupBinder n env of
Just (PVar _ _) -> True
Just (PVTy _) -> True
_ -> False

3
src/Idris/Core/WHNF.hs
View File

@ -12,11 +12,8 @@ module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
import Idris.Core.CaseTree
import Idris.Core.Evaluate hiding (quote)
import qualified Idris.Core.Evaluate as Evaluate
import Idris.Core.TT
import Debug.Trace
-- | A stack entry consists of a term and the environment it is to be
-- evaluated in (i.e. it's a thunk)
type StackEntry = (Term, WEnv)

10
src/Idris/Coverage.hs
View File

@ -16,14 +16,11 @@ import Idris.Core.TT
import Idris.Delaborate
import Idris.Elab.Utils
import Idris.Error
import Idris.Output (iWarn, iputStrLn)
import Control.Monad.State.Strict
import Data.Char
import Data.Either
import Data.List
import Data.Maybe
import Debug.Trace
-- | Generate a pattern from an 'impossible' LHS.
--
@ -284,10 +281,6 @@ addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)
collectConsts (ConstCase c sc) = Just c
collectConsts _ = Nothing
hasDefault (DefaultCase (UnmatchedCase _)) = False
hasDefault (DefaultCase _) = True
hasDefault _ = False
getConType n = do ty <- lookupTyExact n (tt_ctxt ist)
case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of
(P _ tyn _, _) -> Just tyn
@ -336,9 +329,6 @@ trimOverlapping sc = trim [] [] sc
trimAlts cs nots vn (DefaultCase sc : rest)
= DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest
isConMatch c (ConCase cn t args sc) = c == cn
isConMatch _ _ = False
substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]
substMatch ca [] = []
substMatch (c,args) (ConCase cn t args' sc : _)

5
src/Idris/DSL.hs
View File

@ -11,12 +11,10 @@ Maintainer : The Idris Community.
module Idris.DSL where
import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Control.Monad.State.Strict
import Data.Generics.Uniplate.Data (transform)
import Debug.Trace
debindApp :: SyntaxInfo -> PTerm -> PTerm
debindApp syn t = debind (dsl_bind (dsl_info syn)) t
@ -169,8 +167,7 @@ var dsl n t i = v' i t where
setFC fc t = t
unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
mkap (getFn e)
unIdiom ap pure fc e@(PApp _ _ _) = mkap (getFn e)
where
getFn (PApp fc f args) = (PApp fc pure [pexp f], args)
getFn f = (f, [])

6
src/Idris/DataOpts.hs
View File

@ -10,14 +10,8 @@ Maintainer : The Idris Community.
module Idris.DataOpts(applyOpts) where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.Core.TT
import Control.Applicative
import Data.List
import Data.Maybe
import Debug.Trace
class Optimisable term where
applyOpts :: term -> Idris term

1
src/Idris/DeepSeq.hs
View File

@ -24,7 +24,6 @@ import IRTS.Lang (PrimFn(..))
import Util.DynamicLinker
import qualified Cheapskate.Types as CT
import Control.DeepSeq
import Network.Socket (PortNumber)

12
src/Idris/Delaborate.hs
View File

@ -26,10 +26,9 @@ import Prelude hiding ((<$>))
import Control.Applicative (Alternative((<|>)))
import Control.Monad.State
import Data.Generics.Uniplate.Data (transform)
import Data.List (intersperse, nub)
import Data.List (nub)
import Data.Maybe (mapMaybe)
import qualified Data.Text as T
import Debug.Trace
bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
@ -192,13 +191,6 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
de tys env _ (TType i) = PType un
de tys env _ (UType u) = PUniverse un u
dens x | fullname = x
dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of
[_] -> n -- just one thing
[] -> n -- metavariables have no implicits
_ -> ns
dens n = n
deFn tys env (App _ f a) args = deFn tys env f (a:args)
deFn tys env (P _ n _) [l,r]
| n == pairTy = PPair un [] IsType (de tys env [] l) (de tys env [] r)
@ -354,7 +346,7 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
then text "Unification failure" <$> showSc i sc
else empty
pprintErr' i (CantConvert x_in y_in env) =
let (x_ns, y_ns, nms) = renameMNs x_in y_in
let (x_ns, y_ns, _) = renameMNs x_in y_in
(x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))
(delabSugared i (flagUnique y_ns)) in
text "Type mismatch between" <>

1
src/Idris/Directives.hs
View File

@ -8,7 +8,6 @@ Maintainer : The Idris Community.
module Idris.Directives(directiveAction) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Imports

4
src/Idris/Docs.hs
View File

@ -240,10 +240,6 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_
updateRef nm (PRef fc _ _) = PRef fc [] nm
updateRef _ pt = pt
isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'
isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt
isSubInterface _ = False
prettyConstraints =
cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

31
src/Idris/Elab/AsPat.hs
View File

@ -10,20 +10,31 @@ module Idris.Elab.AsPat(desugarAs) where
import Idris.AbsSyntax
import Idris.Core.TT
import Control.Applicative
import Control.Monad.State.Strict
import Data.Generics.Uniplate.Data (transformM)
import Data.Generics.Uniplate.Data (transformM, universe)
-- | Desugar by changing x@y on lhs to let x = y in ... or rhs
desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)
desugarAs lhs rhs
= let (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) [] in
(lhs', bindPats pats rhs)
desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])
desugarAs lhs rhs whereblock
= (lhs', bindOnRight rhs pats, map (bindInWhereDecl pats) whereblock)
where
bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm
bindPats [] rhs = rhs
bindPats ((n, fc, tm) : ps) rhs
= PLet fc n NoFC Placeholder tm (bindPats ps rhs)
(lhs', pats) = runState (collectAs (replaceUnderscore lhs)) []
bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm
bindOnRight = foldr (\(n, fc, tm) -> PLet fc n NoFC Placeholder tm)
bindInWhereDecl :: [(Name, FC, PTerm)] -> PDecl -> PDecl
bindInWhereDecl pats (PClauses fc opts n clauses)
= PClauses fc opts n $ map (bindInWhereClause pats) clauses
bindInWhereDecl _ d = d
bindInWhereClause :: [(Name, FC, PTerm)] -> PClause -> PClause
bindInWhereClause pats (PClause fc n lhs ws rhs wb)
= let bound = [ n | (PRef _ _ n) <- universe lhs ]
pats' = filter (not . (`elem` bound) . \(n,_,_) -> n) pats
rhs' = bindOnRight rhs pats' in
PClause fc n lhs ws rhs' $ map (bindInWhereDecl pats') wb
bindInWhereClause _ c = c
collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs (PAs fc n tm) = do tm' <- collectAs tm

60
src/Idris/Elab/Clause.hs
View File

@ -13,51 +13,37 @@ import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.WHNF
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.DeepSeq ()
import Idris.Delaborate
import Idris.Docstrings hiding (Unchecked)
import Idris.DSL
import Idris.Elab.AsPat
import Idris.Elab.Term
import Idris.Elab.Transform
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Options
import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.Output (iputStrLn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import Idris.Termination
import Idris.Transforms
import IRTS.Lang
import Util.Pretty hiding ((<$>))
import Util.Pretty (pretty, text)
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import qualified Control.Monad.State.Lazy as LState
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Data.Word
import Debug.Trace
import Numeric
@ -153,12 +139,6 @@ elabClauses info' fc opts n_in cs =
-- optimisation applied to LHS
let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $
map debind pats_forced
-- pdef_cov is the pattern definition without forcing, which
-- we feed to the coverage checker (we need to know what the
-- programmer wrote before forcing erasure)
let pdef_cov
= map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $
map debind pats_raw
-- pdef_pe is the one which will get further optimised
-- for run-time, with no forcing optimisation of the LHS because
-- the affects erasure. Also, it's partially evaluated
@ -173,8 +153,6 @@ elabClauses info' fc opts n_in cs =
-- help with later inlinings.
ist <- getIState
let pdef_inl = inlineDef ist pdef
numArgs <- tclift $ sameLength pdef
case specNames opts of
@ -197,7 +175,6 @@ elabClauses info' fc opts n_in cs =
missing' <- checkPossibles info fc True n missing
-- Filter out the ones which match one of the
-- given cases (including impossible ones)
let clhs = map getLHS pdef
logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++
showSep "\n" (map showTmImpls missing') ++
"\nAgainst: " ++
@ -245,7 +222,6 @@ elabClauses info' fc opts n_in cs =
logElab 3 $ "Optimised: " ++ show tree'
ctxt <- getContext
ist <- getIState
let opt = idris_optimisation ist
putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)
(idris_patdefs ist) })
let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)
@ -315,15 +291,6 @@ elabClauses info' fc opts n_in cs =
return ()
where
noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of
Right _ -> False
Left miss -> True) cs
where
trim_matchClause i (PApp fcl fl ls) (PApp fcr fr rs)
= let args = min (length ls) (length rs) in
matchClause i (PApp fcl fl (take args ls))
(PApp fcr fr (take args rs))
checkUndefined n ctxt = case lookupDef n ctxt of
[] -> return ()
[TyDecl _ _] -> return ()
@ -371,7 +338,7 @@ elabClauses info' fc opts n_in cs =
sameLength ((_, x, _) : xs)
= do l <- sameLength xs
let (f, as) = unApply x
let (_, as) = unApply x
if (null xs || l == length as) then return (length as)
else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
sameLength [] = return 0
@ -683,11 +650,10 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++
"\n" ++ show ptm
return (Left ptm, lhs)
elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)
= do let tcgen = Dictionary `elem` opts
push_estack fname False
elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)
= do push_estack fname False
ctxt <- getContext
let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as
let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as
-- Build the LHS as an "Infer", and pull out its type and
-- pattern bindings
@ -916,8 +882,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
pinfo info ns ds i
= let newps = params info ++ ns
dsParams = map (\n -> (n, map fst newps)) ds
newb = addAlist dsParams (inblock info)
l = liftname info in
newb = addAlist dsParams (inblock info) in
info { params = newps,
inblock = newb,
liftname = id -- (\n -> case lookupCtxt n newb of
@ -966,8 +931,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
isOutsideWith _ = True
elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
= do let tcgen = Dictionary `elem` opts
ctxt <- getContext
= do ctxt <- getContext
-- Build the LHS as an "Infer", and pull out its type and
-- pattern bindings
i <- getIState
@ -1189,9 +1153,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
mkAux pn wname toplhs ns ns' c
= ifail $ show fc ++ ":badly formed with clause"
addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])
addArg (PRef fc hls f) w = PApp fc (PRef fc hls f) [pexp w]
-- ns, arguments which don't depend on the with argument
-- ns', arguments which do
updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w
@ -1215,11 +1176,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
updateWithTerm ist pn wname toplhs ns_in ns_in' tm
= mapPT updateApp tm
where
arity (PApp _ _ as) = length as
arity _ = 0
lhs_arity = arity toplhs
currentFn fname (PAlternative _ _ as)
| Just tm <- getApp as = tm
where getApp (tm@(PApp _ (PRef _ _ f) _) : as)

44
src/Idris/Elab/Data.hs
View File

@ -10,49 +10,30 @@ module Idris.Elab.Data(elabData) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings
import Idris.DSL
import Idris.Elab.Rewrite
import Idris.Elab.Term
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import IRTS.Lang
import Idris.Output (iWarn, sendHighlighting)
import Util.Pretty
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
warnLC :: FC -> Name -> Idris ()
warnLC fc n
@ -61,8 +42,7 @@ warnLC fc n
elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()
elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)
= do let codata = Codata `elem` opts
logElab 1 (show (fc, doc))
= do logElab 1 (show (fc, doc))
checkUndefined fc n
when (implicitable (nsroot n)) $ warnLC fc n
(cty, _, t, inacc) <- buildType info syn fc [] n t_in
@ -92,7 +72,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))
cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
ttag <- getName
let as = map (const (Left (Msg ""))) (getArgTys cty)
ctxt <- getContext
let params = findParams n (normalise ctxt [] cty) (map snd cons)
@ -170,8 +149,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
cinfo info ds
= let newps = params info
dsParams = map (\n -> (n, [])) ds
newb = addAlist dsParams (inblock info)
l = liftname info in
newb = addAlist dsParams (inblock info) in
info { params = newps,
inblock = newb,
liftname = id -- Is this appropriate?
@ -245,12 +223,6 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
getTyName (PRef _ _ n) = n == nsroot tn
getTyName _ = False
getNamePos :: Int -> PTerm -> Name -> Maybe Int
getNamePos i (PPi _ n _ _ sc) x | n == x = Just i
| otherwise = getNamePos (i + 1) sc x
getNamePos _ _ _ = Nothing
-- if the constructor is a UniqueType, the datatype must be too
-- (AnyType is fine, since that is checked for uniqueness too)
-- if hte contructor is AnyType, the datatype must be at least AnyType
@ -358,7 +330,7 @@ elabCaseFun ind paramPos n ty cons info = do
elimLog "Elaborating case function"
put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
let (cnstrs, _) = splitPi ty
let (splittedTy@(pms, idxs)) = splitPms cnstrs
let (pms, idxs) = splitPms cnstrs
generalParams <- namePis False pms
motiveIdxs <- namePis False idxs
let motive = mkMotive n paramPos generalParams motiveIdxs
@ -396,10 +368,6 @@ elabCaseFun ind paramPos n ty cons info = do
elimDeclName :: Name
elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n
applyNS :: Name -> [String] -> Name
applyNS n [] = n
applyNS n ns = sNS n ns
splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
splitPi = splitPi' []
where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
@ -440,10 +408,6 @@ elabCaseFun ind paramPos n ty cons info = do
simpleName (MN i n) = str n ++ show i
simpleName n = show n
nameSpaces :: Name -> [String]
nameSpaces (NS _ ns) = map str ns
nameSpaces _ = []
freshName :: String -> EliminatorState Name
freshName key = do
nameMap <- get

31
src/Idris/Elab/Implementation.hs
View File

@ -9,50 +9,27 @@ Maintainer : The Idris Community.
module Idris.Elab.Implementation(elabImplementation) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings
import Idris.DSL
import Idris.Elab.Data
import Idris.Elab.Term
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import IRTS.Lang
import Idris.Output (iWarn, sendHighlighting)
import Util.Pretty (pretty, text)
import Util.Pretty (text)
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
elabImplementation :: ElabInfo
-> SyntaxInfo
@ -79,7 +56,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
[] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"
cs -> tclift $ tfail $ At fc
(CantResolveAlts (map fst cs))
let constraint = PApp fc (PRef fc [] n) (map pexp ps)
let iname = mkiname n (namespace info) ps expn
putIState (ist { hide_list = addDef iname acc (hide_list ist) })
ist <- getIState
@ -167,7 +143,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
let wbVals_orig = map (decorateid (decorate ns iname)) ds'
ist <- getIState
let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig
let wb = wbTys ++ wbVals
logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))
@ -300,8 +275,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
mkMethApp ps (n, _, _, ty)
= lamBind 0 ty (papp fc (PRef fc [] n)
(ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))
where
needed is p = pname p `elem` map pname is
lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'
= PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

47
src/Idris/Elab/Interface.hs
View File

@ -10,51 +10,22 @@ Maintainer : The Idris Community.
module Idris.Elab.Interface(elabInterface) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings
import Idris.DSL
import Idris.Elab.Data
import Idris.Elab.Term
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import IRTS.Lang
import Util.Pretty (pretty, text)
import Idris.Output (sendHighlighting)
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.Generics.Uniplate.Data (transform)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
data MArgTy = IA Name | EA Name | CA deriving Show
@ -123,8 +94,7 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn
ims <- mapM (tdecl impps mnames) mdecls
defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
(filter clause ds)
let (methods, imethods)
= unzip (map (\ (x, y, z) -> (x, y)) ims)
let imethods = map (\ (x, y, z) -> y) ims
let defaults = map (\ (x, (y, z)) -> (x,y)) defs
addInterface tn (CI cn (map nodoc imethods) defaults idecls
@ -396,13 +366,6 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn
return (PTy doc [] syn fc o m mfc ty',
PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])
updateIMethod :: [(Name, PTerm)] ->
(Name, (a, b, c, d, PTerm)) ->
(Name, (a, b, c, d, PTerm))
updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))
| Just ty' <- lookup (nsroot n) ns = (n, (isf, mfc, doc, o, ty'))
| otherwise = tm
getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc
getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc
getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc
@ -452,12 +415,6 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn
toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
toExp ns e sc = sc
-- | Get the method declaration name corresponding to a user-provided name
mdec :: Name -> Name
mdec (UN n) = SN (MethodN (UN n))
mdec (NS x n) = NS (mdec x) n
mdec x = x
-- | Get the docstring corresponding to a member, if one exists
memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

27
src/Idris/Elab/Provider.hs
View File

@ -9,51 +9,24 @@ Maintainer : The Idris Community.
module Idris.Elab.Provider(elabProvider) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings
import Idris.DSL
import Idris.Elab.Clause
import Idris.Elab.Term
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Options
import Idris.Output (iWarn, iputStrLn, pshow)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import IRTS.Lang
import Util.Pretty (pretty, text)
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
-- | Elaborate a type provider
elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()

41
src/Idris/Elab/Record.hs
View File

@ -11,25 +11,11 @@ module Idris.Elab.Record(elabRecord) where
import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings
import Idris.Elab.Data
import Idris.Elab.Data
import Idris.Elab.Term
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.Parser.Expr (tryFullExpr)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import IRTS.Lang
import Idris.Output (sendHighlighting)
import Control.Monad
import Data.List
@ -225,15 +211,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
isFieldOrParam' :: (Name, a) -> Bool
isFieldOrParam' = isFieldOrParam . fst
isField :: Name -> Bool
isField = flip elem fieldNames
isField' :: (Name, a, b, c, d, f) -> Bool
isField' (n, _, _, _, _, _) = isField n
fieldTerms :: [PTerm]
fieldTerms = [t | (_, _, _, t, _) <- fields]
-- Delabs the TT to PTerm
-- This is not good.
-- However, for machine generated implicits, there seems to be no PTerm available.
@ -252,13 +229,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
freeName (NS n s) = NS (freeName n) s
freeName n = n
-- | Zips together parameters with their documentation. If no documentation for a given field exists, an empty docstring is used.
zipParams :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]
zipParams i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zipParams i rest rest')
zipParams i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zipParams i rest [])
where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring
zipParams _ [] [] = []
paramName :: Name -> Name
paramName (UN n) = sUN ("param_" ++ str n)
paramName (MN i n) = sMN i ("param_" ++ str n)
@ -295,15 +265,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
fieldDep :: Name -> PTerm -> (Name, [Name])
fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
-- | A list of fields depending on another field.
dependentFields :: [Name]
dependentFields = filter depends fieldNames
where
depends :: Name -> Bool
depends n = case lookup n fieldDependencies of
Just xs -> not $ null xs
Nothing -> False
-- | A list of fields depended on by other fields.
dependedOn :: [Name]
dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))

3
src/Idris/Elab/Rewrite.hs
View File

@ -10,7 +10,6 @@ Maintainer : The Idris Community.
module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.Core.Elaborate
import Idris.Core.Evaluate
import Idris.Core.TT
@ -20,8 +19,6 @@ import Idris.Error
import Control.Monad
import Control.Monad.State.Strict
import Data.List
import Debug.Trace
elabRewrite :: (PTerm -> ElabD ()) -> IState ->
FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()

4
src/Idris/Elab/RunElab.hs
View File

@ -9,14 +9,12 @@ module Idris.Elab.RunElab (elabRunElab) where
import Idris.AbsSyntax
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Elab.Term
import Idris.Elab.Value (elabVal)
import Idris.Error
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.Output (sendHighlighting)
elabScriptTy :: Type
elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)

66
src/Idris/Elab/Term.hs
View File

@ -10,40 +10,34 @@ Maintainer : The Idris Community.
module Idris.Elab.Term where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)
import Idris.Core.CaseTree (SC'(STerm), findCalls)
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.ProofTerm (getProofTerm)
import Idris.Core.TT
import Idris.Core.Typecheck (check, converts, isType, recheck)
import Idris.Core.Unify
import Idris.Core.WHNF (whnf, whnfArgs)
import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)
import Idris.Core.WHNF (whnf)
import Idris.Coverage (genClauses, recoverableCoverage)
import Idris.Delaborate
import Idris.DSL
import Idris.Elab.Quasiquote (extractUnquotes)
import Idris.Elab.Rewrite
import Idris.Elab.Utils
import Idris.Error
import Idris.ErrReverse (errReverse)
import Idris.Options
import Idris.Output (pshow)
import Idris.ProofSearch
import Idris.Reflection
import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)
import qualified Util.Pretty as U
import Control.Applicative ((<$>))
import Control.Monad
import Control.Monad.State.Strict
import Data.Foldable (for_)
import Data.List
import qualified Data.Map as M
import Data.Maybe (catMaybes, fromMaybe, mapMaybe, maybeToList)
import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS
@ -85,7 +79,6 @@ build :: IState
-> ElabD ElabResult
build ist info emode opts fn tm
= do elab ist info emode opts fn tm
let tmIn = tm
let inf = case lookupCtxt fn (idris_tyinfodata ist) of
[TIPartial] -> True
_ -> False
@ -163,8 +156,7 @@ buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->
PTerm ->
ElabD ElabResult
buildTC ist info emode opts fn ns tm
= do let tmIn = tm
let inf = case lookupCtxt fn (idris_tyinfodata ist) of
= do let inf = case lookupCtxt fn (idris_tyinfodata ist) of
[TIPartial] -> True
_ -> False
-- set name supply to begin after highest index in tm
@ -190,7 +182,6 @@ buildTC ist info emode opts fn ns tm
if (log /= "")
then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
where pattern = emode == ELHS || emode == EImpossible
-- | return whether arguments of the given constructor name can be
-- matched on. If they're polymorphic, no, unless the type has beed
@ -247,7 +238,6 @@ elab ist info emode opts fn tm
= do let loglvl = opt_logLevel (idris_options ist)
when (loglvl > 5) $ unifyLog True
compute -- expand type synonyms, etc
let fc = maybe "(unknown)"
elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
est <- getAux
sequence_ (get_delayed_elab est)
@ -283,14 +273,6 @@ elab ist info emode opts fn tm
Placeholder -> (True, priority arg)
tm -> (False, priority arg)
toElab ina arg = case getTm arg of
Placeholder -> Nothing
v -> Just (priority arg, elabE ina (elabFC info) v)
toElab' ina arg = case getTm arg of
Placeholder -> Nothing
v -> Just (elabE ina (elabFC info) v)
mkPat = do hs <- get_holes
tm <- get_term
case hs of
@ -356,18 +338,6 @@ elab ist info emode opts fn tm
notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False
notDelay _ = True
local f = do e <- get_env
return (f `elem` map fstEnv e)
-- | Is a constant a type?
constType :: Const -> Bool
constType (AType _) = True
constType StrType = True
constType VoidType = True
constType _ = False
-- "guarded" means immediately under a constructor, to help find patvars
elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)
-> Maybe FC -- ^ The closest FC in the syntax tree, if applicable
-> PTerm -- ^ The term to elaborate
@ -603,13 +573,6 @@ elab ist info emode opts fn tm
(P _ n' _, _) -> n == n'
_ -> False
showQuick (CantUnify _ (l, _) (r, _) _ _ _)
= show (l, r)
showQuick (ElaboratingArg _ _ _ e) = showQuick e
showQuick (At _ e) = showQuick e
showQuick (ProofSearchFail (Msg _)) = "search fail"
showQuick _ = "No chance"
elab' ina _ (PPatvar fc n) | bindfree
= do patvar n
update_term liftPats
@ -627,8 +590,6 @@ elab ist info emode opts fn tm
= do ty <- goal
testImplicitWarning fc n ty
let ina = e_inarg ec
guarded = e_guarded ec
inty = e_intype ec
ctxt <- get_context
env <- get_env
@ -890,7 +851,6 @@ elab ist info emode opts fn tm
_ -> do mapM_ setInjective (map getTm args)
-- maybe more things are solvable now
unifyProblems
let guarded = isConName f ctxt
-- trace ("args is " ++ show args) $ return ()
ns <- apply (Var f) (map isph args)
-- trace ("ns is " ++ show ns) $ return ()
@ -1000,10 +960,6 @@ elab ist info emode opts fn tm
getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as
| otherwise = getDets (i + 1) ds as
tacTm (PTactics _) = True
tacTm (PProof _) = True
tacTm _ = False
setInjective (PRef _ _ n) = setinj n
setInjective (PApp _ (PRef _ _ n) _) = setinj n
setInjective _ = return ()
@ -1078,7 +1034,6 @@ elab ist info emode opts fn tm
matchProblems True
args <- get_env
envU <- mapM (getKind args) args
let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
-- Drop the unique arguments used in the term already
-- and in the scrutinee (since it's
@ -1156,12 +1111,6 @@ elab ist info emode opts fn tm
UType AllTypes -> return (n, True)
_ -> return (n, False)
tcName tm | (P _ n _, _) <- unApply tm
= case lookupCtxt n (idris_interfaces ist) of
[_] -> True
_ -> False
tcName _ = False
isNotLift env n
= case lookupBinder n env of
Just ty ->
@ -1170,10 +1119,6 @@ elab ist info emode opts fn tm
_ -> False
_ -> False
usedIn ns (n, b)
= n `elem` ns
|| any (\x -> x `elem` ns) (allTTNames (binderTy b))
elab' ina fc (PUnifyLog t) = do unifyLog True
elab' ina fc t
unifyLog False
@ -2716,7 +2661,6 @@ processTacticDecls info steps =
RDatatypeDefnInstrs tyn tyconTy ctors ->
do let cn (n, _, _) = n
cimpls (_, impls, _) = impls
cty (_, _, t) = t
addIBC (IBCDef tyn)
mapM_ (addIBC . IBCDef . cn) ctors

31
src/Idris/Elab/Transform.hs
View File

@ -9,47 +9,19 @@ Maintainer : The Idris Community.
module Idris.Elab.Transform where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings
import Idris.DSL
import Idris.Elab.Term
import Idris.Elab.Utils
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import IRTS.Lang
import Util.Pretty (pretty, text)
import Idris.Output (sendHighlighting)
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
@ -66,7 +38,6 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
sendHighlighting highlights
updateIState $ \i -> i { idris_name = newGName }
let lhs_tm = orderPats (getInferTerm lhs')
let lhs_ty = getInferType lhs'
let newargs = pvars i lhs_tm
(clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm

42
src/Idris/Elab/Type.hs
View File

@ -13,50 +13,23 @@ module Idris.Elab.Type (
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.WHNF
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings (Docstring)
import Idris.DSL
import Idris.Elab.Term
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Options
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import IRTS.Lang
import Util.Pretty (pretty, text)
import Idris.Output (sendHighlighting)
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import qualified Data.Traversable as Traversable
import Debug.Trace
buildType :: ElabInfo
-> SyntaxInfo
@ -196,11 +169,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))
let (fam, _) = unApply (getRetTy nty')
let corec = case fam of
P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
[TI _ True _ _ _ _] -> True
_ -> False
_ -> False
-- Productivity checking now via checking for guarded 'Delay'
let opts' = opts -- if corec then (Coinductive : opts) else opts
let usety = if norm then nty' else nty
@ -251,14 +219,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
_ -> return ()
return usety
where
-- for making an internalapp, we only want the explicit ones, and don't
-- want the parameters, so just take the arguments which correspond to the
-- user declared explicit ones
mergeTy (PPi e n fc ty sc) (PPi e' n' _ _ sc')
| e == e' = PPi e n fc ty (mergeTy sc sc')
| otherwise = mergeTy sc sc'
mergeTy _ sc = sc
ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]
err = txt "Err"

7
src/Idris/Elab/Utils.hs
View File

@ -14,7 +14,6 @@ import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.WHNF
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings
import Idris.Error
@ -22,14 +21,11 @@ import Idris.Output
import Util.Pretty
import Control.Applicative hiding (Const)
import Control.Monad
import Control.Monad.State
import Data.List
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Traversable as Traversable
import Debug.Trace
recheckC = recheckC_borrowing False True []
@ -122,7 +118,6 @@ elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()
elabCaseBlock info opts d@(PClauses f o n ps)
= do addIBC (IBCDef n)
logElab 5 $ "CASE BLOCK: " ++ show (n, d)
let opts' = nub (o ++ opts)
-- propagate totality assertion to the new definitions
let opts' = filter propagatable opts
setFlags n opts'
@ -750,7 +745,7 @@ pruneByType _ _ t _ _ as = as
-- to it later - just returns 'var' for now. EB)
isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
isPlausible ist var env n ty
= let (hvar, interfaces) = collectConstraints [] [] ty in
= let (hvar, _) = collectConstraints [] [] ty in
case hvar of
Nothing -> True
Just rth -> var -- trace (show (rth, interfaces)) var

32
src/Idris/Elab/Value.hs
View File

@ -13,48 +13,20 @@ module Idris.Elab.Value(
) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate hiding (Unchecked)
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Docstrings
import Idris.DSL
import Idris.Elab.Term
import Idris.Elab.Utils
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Primitives
import Idris.Providers
import IRTS.Lang
import Util.Pretty (pretty, text)
import Idris.Output (sendHighlighting)
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Data.Char (toLower)
import qualified Data.Traversable as Traversable
import Debug.Trace
-- | Elaborate a value, returning any new bindings created (this will only
-- happen if elaborating as a pattern clause)

35
src/Idris/ElabDecls.hs
View File

@ -12,20 +12,10 @@ Maintainer : The Idris Community.
module Idris.ElabDecls where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq
import Idris.Delaborate
import Idris.Directives
import Idris.Docstrings hiding (Unchecked)
import Idris.DSL
import Idris.Elab.Clause
import Idris.Elab.Data
import Idris.Elab.Implementation
@ -36,36 +26,21 @@ import Idris.Elab.RunElab
import Idris.Elab.Term
import Idris.Elab.Transform
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.Error
import Idris.Imports
import Idris.Inliner
import Idris.Options
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Output (sendHighlighting)
import Idris.Primitives
import Idris.Providers
import Idris.Termination
import IRTS.Lang
import Util.Pretty (pretty, text)
import Prelude hiding (id, (.))
import Control.Applicative hiding (Const)
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import Data.List.Split (splitOn)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
-- | Top level elaborator info, supporting recursive elaboration
recinfo :: FC -> ElabInfo
@ -269,12 +244,6 @@ elabDecl' what info (PParams f ns ps)
let nblock = pblock i
mapM_ (elabDecl' what info) nblock
where
pinfo = let ds = concatMap tldeclared ps
newps = params info ++ ns
dsParams = map (\n -> (n, map fst newps)) ds
newb = addAlist dsParams (inblock info) in
info { params = newps,
inblock = newb }
pblock i = map (expandParamsD False i id ns
(concatMap tldeclared ps)) ps
@ -311,6 +280,8 @@ elabDecl' _ info (PDSL n dsl)
ifail "You must turn on the DSLNotation extension to use a dsl block"
putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
addIBC (IBCDSL n)
elabDecl' what info (PDirective i@(DLogging _))
= directiveAction i
elabDecl' what info (PDirective i)
| what /= EDefns = directiveAction i
elabDecl' what info (PProvider doc syn fc nfc provWhat n)

7
src/Idris/Erasure.hs
View File

@ -20,7 +20,6 @@ import Idris.Primitives
import Prelude hiding (id, (.))
import Control.Applicative
import Control.Arrow
import Control.Category
import Control.Monad.State
@ -36,8 +35,6 @@ import Data.Set (Set)
import qualified Data.Set as S
import Data.Text (pack)
import qualified Data.Text as T
import Debug.Trace
import System.IO.Unsafe
-- | UseMap maps names to the set of used (reachable) argument
-- positions.
@ -290,7 +287,6 @@ buildDepMap ci used externs ctx startNames
-- mini-DSL for postulates
(==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])
it n is = [(sUN n, Arg i) | i <- is]
mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
-- believe_me is special because it does not use all its arguments
specialPrims = S.fromList [sUN "prim__believe_me"]
@ -627,9 +623,6 @@ buildDepMap ci used externs ctx startNames
union :: Deps -> Deps -> Deps
union = M.unionWith (M.unionWith S.union)
unions :: [Deps] -> Deps
unions = M.unionsWith (M.unionWith S.union)
unionMap :: (a -> Deps) -> [a] -> Deps
unionMap f = M.unionsWith (M.unionWith S.union) . map f

12
src/Idris/ErrReverse.hs
View File

@ -12,10 +12,8 @@ module Idris.ErrReverse(errReverse) where
import Idris.AbsSyntax
import Idris.Core.Evaluate (unfold)
import Idris.Core.TT
import Util.Pretty
import Data.List
import Debug.Trace
-- | For display purposes, apply any 'error reversal' transformations
-- so that errors will be more readable,
@ -73,13 +71,3 @@ errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)
Just (fs ++ as)
-- no matching Binds, for now...
match' ns x y = if x == y then Just [] else Nothing
-- if the term under a lambda is huge, there's no much point in showing
-- it as it won't be very enlightening.
elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)
elideLambdas (Bind n (Lam _ t) sc)
| size sc > 200 = P Ref (sUN "...") Erased
elideLambdas (Bind n b sc)
= Bind n (fmap elideLambdas b) (elideLambdas sc)
elideLambdas t = t

7
src/Idris/Error.hs
View File

@ -14,23 +14,16 @@ import Idris.AbsSyntax
import Idris.Core.Constraints
import Idris.Core.Evaluate (ctxtAlist)
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Delaborate
import Idris.Output
import Prelude hiding (catch)
import Control.Monad (when)
import Control.Monad.State.Strict
import Data.Char
import qualified Data.Foldable as Foldable
import Data.List (intercalate, isPrefixOf)
import qualified Data.Set as S
import qualified Data.Text as T
import qualified Data.Traversable as Traversable
import Data.Typeable
import System.Console.Haskeline
import System.Console.Haskeline.MonadException
import System.IO.Error (ioeGetErrorString, isUserError)
iucheck :: Idris ()

57
src/Idris/IBC.hs
View File

@ -5,20 +5,20 @@ Copyright :
License : BSD3
Maintainer : The Idris Community.
-}
{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.IBC (loadIBC, loadPkgIndex,
writeIBC, writePkgIndex,
hasValidIBCVersion, IBCPhase(..)) where
import Idris.AbsSyntax
import Idris.Core.Binary
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.DeepSeq
import Idris.Delaborate
import Idris.DeepSeq ()
import Idris.Docstrings (Docstring)
import qualified Idris.Docstrings as D
import Idris.Error
@ -27,23 +27,15 @@ import Idris.Options
import Idris.Output
import IRTS.System (getIdrisLibDir)
import Paths_idris
import qualified Cheapskate.Types as CT
import Codec.Archive.Zip
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict hiding (get, put)
import qualified Control.Monad.State.Strict as ST
import Data.Binary
import Data.ByteString.Lazy as B hiding (elem, length, map)
import Data.Functor
import Data.List as L
import Data.Maybe (catMaybes)
import qualified Data.Set as S
import qualified Data.Text as T
import Data.Vector.Binary
import Debug.Trace
import System.Directory
import System.FilePath
@ -59,7 +51,6 @@ data IBCPhase = IBC_Building -- ^ when building the module tree
data IBCFile = IBCFile {
ver :: Word16
, sourcefile :: FilePath
, ibc_reachablenames :: ![Name]
, ibc_imports :: ![(Bool, FilePath)]
, ibc_importdirs :: ![FilePath]
, ibc_sourcedirs :: ![FilePath]
@ -116,7 +107,7 @@ deriving instance Binary IBCFile
!-}
initIBC :: IBCFile
initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []
initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []
hasValidIBCVersion :: FilePath -> Idris Bool
hasValidIBCVersion fp = do
@ -131,7 +122,9 @@ loadIBC :: Bool -- ^ True = reexport, False = make everything private
-> IBCPhase
-> FilePath -> Idris ()
loadIBC reexport phase fp
= do imps <- getImported
= do logIBC 1 $ "loadIBC (reexport, phase, fp)" ++ show (reexport, phase, fp)
imps <- getImported
logIBC 3 $ "loadIBC imps" ++ show imps
case lookup fp imps of
Nothing -> load True
Just p -> if (not p && reexport) then load False else return ()
@ -517,13 +510,16 @@ processImports reexp phase fname ar = do
ibcsd <- valIBCSubDir i
ids <- rankedImportDirs fname
putIState (i { imported = f : imported i })
let phase' = case phase of
IBC_REPL _ -> IBC_REPL False
p -> p
let (phase', reexp') =
case phase of
IBC_REPL True -> (IBC_REPL False, reexp)
IBC_REPL False -> (IBC_Building, reexp && re)
p -> (p, reexp && re)
fp <- findIBC ids ibcsd f
logIBC 4 $ "processImports (fp, phase')" ++ show (fp, phase')
case fp of
Nothing -> do logIBC 2 $ "Failed to load ibc " ++ f
Just fn -> do loadIBC (reexp && re) phase' fn) fs
Just fn -> do loadIBC reexp' phase' fn) fs
processImplicits :: Archive -> Idris ()
processImplicits ar = do
@ -639,6 +635,7 @@ processPatternDefs ar = do
processDefs :: Archive -> Idris ()
processDefs ar = do
ds <- getEntry [] "ibc_defs" ar
logIBC 4 $ "processDefs ds" ++ show ds
mapM_ (\ (n, d) -> do
d' <- updateDef d
case d' of
@ -735,8 +732,11 @@ processAccess :: Bool -- ^ Reexporting?
-> IBCPhase
-> Archive -> Idris ()
processAccess reexp phase ar = do
logIBC 3 $ "processAccess (reexp, phase)" ++ show (reexp, phase)
ds <- getEntry [] "ibc_access" ar
logIBC 3 $ "processAccess ds" ++ show ds
mapM_ (\ (n, a_in) -> do
let a = if reexp then a_in else Hidden
logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })
@ -745,10 +745,15 @@ processAccess reexp phase ar = do
then do
logIBC 2 $ "Not exporting " ++ show n
setAccessibility n Hidden
else logIBC 2 $ "Exporting " ++ show n
else
logIBC 2 $ "Exporting " ++ show n
-- Everything should be available at the REPL from
-- things imported publicly
when (phase == IBC_REPL True) $ setAccessibility n Public) ds
-- things imported publicly.
when (phase == IBC_REPL True) $ do
logIBC 2 $ "Top level, exporting " ++ show n
setAccessibility n Public
) ds
processFlags :: Archive -> Idris ()
processFlags ar = do
@ -1117,16 +1122,6 @@ instance Binary Accessibility where
3 -> return Hidden
_ -> error "Corrupted binary data for Accessibility"
safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a
safeToEnum label x' = result
where
x = fromIntegral x'
result
| x < fromEnum (minBound `asTypeOf` result)
|| x > fromEnum (maxBound `asTypeOf` result)
= error $ label ++ ": corrupted binary representation in IBC"
| otherwise = toEnum x
instance Binary PReason where
put x
= case x of

5
src/Idris/IdeMode.hs
View File

@ -11,7 +11,7 @@ Maintainer : The Idris Community.
module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where
import Idris.Core.Binary
import Idris.Core.Binary ()
import Idris.Core.TT
import Control.Applicative hiding (Const)
@ -176,9 +176,6 @@ instance SExpable OutputAnnotation where
encodeName :: Name -> String
encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n
decodeName :: String -> Name
decodeName = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
encodeTerm :: [(Name, Bool)] -> Term -> String
encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
(bnd, tm)

20
src/Idris/IdrisDoc.hs
View File

@ -10,11 +10,10 @@ Maintainer : The Idris Community.
module Idris.IdrisDoc (generateDocs) where
import Idris.AbsSyntax
import Idris.Core.Evaluate (Accessibility(..), Def(..), ctxtAlist, isDConName,
isFnName, isTConName, lookupDefAcc)
import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),
TextFormatting(..), constIsType, nsroot, sUN, str,
toAlist, txt)
import Idris.Core.Evaluate (Accessibility(..), ctxtAlist, isDConName, isFnName,
isTConName, lookupDefAcc)
import Idris.Core.TT (Name(..), OutputAnnotation(..), TextFormatting(..),
constIsType, nsroot, sUN, str, toAlist, txt)
import Idris.Docs
import Idris.Docstrings (nullDocstring)
import qualified Idris.Docstrings as Docstrings
@ -26,17 +25,13 @@ import Control.Applicative ((<|>))
import Control.Monad (forM_)
import Control.Monad.Trans.Except
import Control.Monad.Trans.State.Strict
import qualified Data.ByteString as BS
import qualified Data.ByteString.Lazy as BS2
import qualified Data.List as L
import qualified Data.List.Split as LS
import qualified Data.Map as M hiding ((!))
import Data.Maybe
import Data.Monoid (mempty)
import qualified Data.Ord (compare)
import qualified Data.Set as S
import qualified Data.Text as T
import qualified Data.Text.Encoding as E
import System.Directory
import System.FilePath
import System.IO
@ -253,13 +248,6 @@ getAccess ist n =
[(_, acc)] -> acc
_ -> Private
-- | Simple predicate for whether an NsItem has Docs
hasDoc :: NsItem -- ^ The NsItem to test
-> Bool -- ^ The result
hasDoc (_, Just _, _) = True
hasDoc _ = False
-- | Predicate saying whether a Name possibly may have docs defined
-- Without this, getDocs from Idris.Docs may fail a pattern match.
mayHaveDocs :: Name -- ^ The Name to test

5
src/Idris/Imports.hs
View File

@ -13,7 +13,6 @@ module Idris.Imports(
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Error
import Idris.Output
import IRTS.System (getIdrisLibDir)
import Control.Applicative ((<$>))
@ -30,13 +29,13 @@ pkgIndex :: String -> FilePath
pkgIndex s = "00" ++ s ++ "-idx.ibc"
srcPath :: FilePath -> FilePath
srcPath fp = let (n, ext) = splitExtension fp in
srcPath fp = let (_, ext) = splitExtension fp in
case ext of
".idr" -> fp
_ -> fp ++ ".idr"
lsrcPath :: FilePath -> FilePath
lsrcPath fp = let (n, ext) = splitExtension fp in
lsrcPath fp = let (_, ext) = splitExtension fp in
case ext of
".lidr" -> fp
_ -> fp ++ ".lidr"

1
src/Idris/Info.hs
View File

@ -29,7 +29,6 @@ import Idris.Imports (installedPackages)
import Idris.Options (loggingCatsStr)
import qualified IRTS.System as S
import Paths_idris
import Version_idris (gitHash)
import Data.Version

4
src/Idris/Interactive.hs
View File

@ -382,9 +382,7 @@ makeLemma fn updatefile l n
StringAtom lem_app]]]
in runIO . hPutStrLn h $ convSExp "return" good n
where getIndent s = length (takeWhile isSpace s)
appArgs skip 0 _ = ""
where appArgs skip 0 _ = ""
appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)
| (thead c /= '_' && n `notElem` skip)
= " " ++ show n ++ appArgs skip (i - 1) sc

45
src/Idris/ModeCommon.hs
View File

@ -4,6 +4,11 @@ Description : Common utilities used by all modes.
License : BSD3
Maintainer : The Idris Community.
-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-binds #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.ModeCommon where
import Idris.AbsSyntax
@ -25,16 +30,11 @@ import Prelude hiding (id, (.), (<$>))
import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.Trans.State.Strict (get)
import Data.List hiding (group)
import Data.Maybe
import Network.Socket (PortNumber)
import System.Directory
defaultPort :: PortNumber
defaultPort = fromIntegral 4294
loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs inputs toline -- furthest line to read in input source files
= idrisCatch
@ -49,6 +49,8 @@ loadInputs inputs toline -- furthest line to read in input source files
[] -> not (NoREPL `elem` opts)
_ -> True
logParser 3 $ show "loadInputs loadCode" ++ show loadCode
-- For each ifile list, check it and build ibcs in the same clean IState
-- so that they don't interfere with each other when checking
@ -59,6 +61,7 @@ loadInputs inputs toline -- furthest line to read in input source files
let ninputs = zip [1..] inputs
ifiles <- mapWhileOK (\(num, input) ->
do putIState ist
logParser 3 $ show "loadInputs (num, input)" ++ show (num, input)
modTree <- buildTree
(map snd (take (num-1) ninputs))
importlists
@ -77,9 +80,18 @@ loadInputs inputs toline -- furthest line to read in input source files
case errSpan inew of
Nothing ->
do putIState $!! ist { idris_tyinfodata = tidata }
ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))
-- logLvl 0 $ "Loading from " ++ show ibcfiles
tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)
logParser 3 $ "loadInputs ifiles" ++ show ifiles
let fileToIFileType :: FilePath -> Idris IFileType
fileToIFileType file = do
ibcsd <- valIBCSubDir ist
ids <- rankedImportDirs file
findImport ids ibcsd file
ibcfiles <- mapM fileToIFileType inputs
logParser 3 $ show "loadInputs ibcfiles" ++ show ibcfiles
tryLoad True (IBC_REPL True) ibcfiles
_ -> return ()
exports <- findExports
@ -103,6 +115,8 @@ loadInputs inputs toline -- furthest line to read in input source files
tryLoad keepstate phase [] = warnTotality >> return ()
tryLoad keepstate phase (f : fs)
= do ist <- getIState
logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++
show (keepstate, phase, f : fs)
let maxline
= case toline of
Nothing -> Nothing
@ -142,21 +156,6 @@ loadInputs inputs toline -- furthest line to read in input source files
fmatch xs ('.':'/':ys) = fmatch xs ys
fmatch xs ys = xs == ys
findNewIBC :: IFileType -> Idris (Maybe IFileType)
findNewIBC i@(IBC _ _) = return (Just i)
findNewIBC s@(IDR f) = do ist <- get
ibcsd <- valIBCSubDir ist
let ibc = ibcPathNoFallback ibcsd f
ok <- runIO $ doesFileExist ibc
if ok then return (Just (IBC ibc s))
else return Nothing
findNewIBC s@(LIDR f) = do ist <- get
ibcsd <- valIBCSubDir ist
let ibc = ibcPathNoFallback ibcsd f
ok <- runIO $ doesFileExist ibc
if ok then return (Just (IBC ibc s))
else return Nothing
-- Like mapM, but give up when there's an error
mapWhileOK f [] = return []
mapWhileOK f (x : xs) = do x' <- f x

5
src/Idris/Output.hs
View File

@ -13,7 +13,7 @@ module Idris.Output where
import Idris.AbsSyntax
import Idris.Colours (hEndColourise, hStartColourise)
import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)
import Idris.Core.Evaluate (normaliseAll)
import Idris.Core.TT
import Idris.Delaborate
import Idris.Docstrings
@ -27,13 +27,12 @@ import Util.System (isATTY)
import Prelude hiding ((<$>))
import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
import Data.Char (isAlpha)
import Data.List (intersperse, nub)
import Data.Maybe (fromMaybe)
import System.Console.Haskeline.MonadException (MonadException(controlIO),
RunIO(RunIO))
import System.FilePath (replaceExtension)
import System.IO (Handle, hPutStr, hPutStrLn, stdout)
import System.IO (Handle, hPutStr, hPutStrLn)
instance MonadException m => MonadException (ExceptT Err m) where
controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

7
src/Idris/Package.hs
View File

@ -12,7 +12,7 @@ import System.Directory
import System.Directory (copyFile, createDirectoryIfMissing)
import System.Exit
import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,
hasExtension, normalise, takeDirectory, takeExtension,
hasExtension, takeDirectory, takeExtension,
takeFileName, (</>))
import System.IO
import System.Process
@ -23,10 +23,8 @@ import Control.Monad
import Control.Monad.Trans.Except (runExceptT)
import Control.Monad.Trans.State.Strict (execStateT)
import Data.Either (partitionEithers)
import Data.Either (partitionEithers)
import Data.List
import Data.List.Split (splitOn)
import Data.Maybe (fromMaybe)
import Idris.AbsSyntax
import Idris.Core.TT
@ -38,7 +36,6 @@ import Idris.Main (idris, idrisMain)
import Idris.Options
import Idris.Output
import Idris.Parser (loadModule)
import Idris.REPL
import Idris.Package.Common
import Idris.Package.Parser
@ -336,11 +333,9 @@ auditPackage True ipkg = do
getIdrisFiles :: FilePath -> IO [FilePath]
getIdrisFiles dir = do
contents <- getDirectoryContents dir
let contents' = filter (\fname -> fname /= "." && fname /= "..") contents
-- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.
files <- forM contents (findRest dir)
return $ filter (isIdrisFile) (concat files)

6
src/Idris/Package/Parser.hs
View File

@ -8,19 +8,13 @@ Maintainer : The Idris Community.
{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}
module Idris.Package.Parser where
import Idris.AbsSyntaxTree
import Idris.CmdOptions
import Idris.Core.TT
import Idris.Package.Common
import Idris.Parser.Helpers hiding (stringLiteral)
import Idris.REPL
import Util.System
import Control.Applicative
import Control.Monad.State.Strict
import Data.List (union)
import Data.Maybe (fromJust, isNothing)
import System.Directory (doesFileExist)
import System.Exit
import System.FilePath (isValid, takeExtension, takeFileName)

38
src/Idris/Parser.hs
View File

@ -5,9 +5,13 @@ Copyright :
License : BSD3
Maintainer : The Idris Community.
-}
{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
PatternGuards #-}
{-# OPTIONS_GHC -O0 #-}
-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.Parser(module Idris.Parser,
module Idris.Parser.Expr,
module Idris.Parser.Data,
@ -17,11 +21,9 @@ module Idris.Parser(module Idris.Parser,
import Idris.AbsSyntax hiding (namespace, params)
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Coverage
import Idris.Delaborate
import Idris.Docstrings hiding (Unchecked)
import Idris.DSL
import Idris.Elab.Term
import Idris.Elab.Value
import Idris.ElabDecls
import Idris.Error
@ -33,15 +35,11 @@ import Idris.Parser.Data
import Idris.Parser.Expr
import Idris.Parser.Helpers
import Idris.Parser.Ops
import Idris.Providers
import Idris.Termination
import Idris.Unlit
import Util.DynamicLinker
import qualified Util.Pretty as P
import Util.System (readSource, writeSource)
import Paths_idris
import Util.System (readSource)
import Prelude hiding (pi)
@ -53,24 +51,14 @@ import Data.Char
import Data.Foldable (asum)
import Data.Function
import Data.Generics.Uniplate.Data (descendM)
import qualified Data.HashSet as HS
import Data.List
import qualified Data.List.Split as Spl
import qualified Data.Map as M
import Data.Maybe
import Data.Monoid
import Data.Ord
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
import qualified System.Directory as Dir (makeAbsolute)
import System.FilePath
import System.IO
import qualified Text.Parser.Char as Chr
import Text.Parser.Expression
import Text.Parser.LookAhead
import qualified Text.Parser.Token as Tok
import qualified Text.Parser.Token.Highlight as Hi
import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
@ -806,7 +794,6 @@ mutual :: SyntaxInfo -> IdrisParser [PDecl]
mutual syn =
do reservedHL "mutual"
openBlock
let pvars = syn_params syn
ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
closeBlock
fc <- getFC
@ -1157,7 +1144,6 @@ clause syn
Just t -> return t
Nothing -> fail "Invalid clause"
(do r <- rhs syn n
let ctxt = tt_ctxt ist
let wsyn = syn { syn_namespace = [], syn_toplevel = False }
(wheres, nmap) <- choice [do x <- whereBlock n wsyn
popIndent
@ -1181,8 +1167,6 @@ clause syn
fc <- getFC
n_in <- fst <$> fnName; let n = expandNS syn n_in
r <- rhs syn n
ist <- get
let ctxt = tt_ctxt ist
let wsyn = syn { syn_namespace = [] }
(wheres, nmap) <- choice [do x <- whereBlock n wsyn
popIndent
@ -1239,8 +1223,6 @@ clause syn
wargs <- many (wExpr syn)
let capp = PApp fc (PRef nfc [nfc] n) args
(do r <- rhs syn n
ist <- get
let ctxt = tt_ctxt ist
let wsyn = syn { syn_namespace = [] }
(wheres, nmap) <- choice [do x <- whereBlock n wsyn
popIndent
@ -1585,11 +1567,6 @@ parseImports fname input
let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
return ((mdoc, mname, ps, mrk'), annots, i)
imp m = ImportInfo False (toPath m)
Nothing [] NoFC NoFC
ns = Spl.splitOn "."
toPath = foldl1' (</>) . ns
addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
addPath [] _ = []
addPath ((fc, AnnNamespace ns Nothing) : annots) path =
@ -1685,6 +1662,7 @@ loadModule' f phase
loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
loadFromIFile reexp phase i@(IBC fn src) maxline
= do logParser 1 $ "Skipping " ++ getSrcFile i
logParser 3 $ "loadFromIFile i" ++ show i
idrisCatch (loadIBC reexp phase fn)
(\err -> ierror $ LoadingFailed fn err)
where
@ -1893,8 +1871,6 @@ loadSource lidr f toline
{-| Adds names to hide list -}
addHides :: Ctxt Accessibility -> Idris ()
addHides xs = do i <- getIState
let defh = default_access i
mapM_ doHide (toAlist xs)
addHides xs = mapM_ doHide (toAlist xs)
where doHide (n, a) = do setAccessibility n a
addIBC (IBCAccess n a)

25
src/Idris/Parser/Data.hs
View File

@ -9,10 +9,8 @@ Maintainer : The Idris Community.
module Idris.Parser.Data where
import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Docstrings
import Idris.DSL
import Idris.Options
import Idris.Parser.Expr
import Idris.Parser.Helpers
@ -21,25 +19,11 @@ import Idris.Parser.Ops
import Prelude hiding (pi)
import Control.Applicative
import Control.Monad
import Control.Monad.State.Strict
import qualified Data.ByteString.UTF8 as UTF8
import Data.Char
import qualified Data.HashSet as HS
import Data.List
import qualified Data.List.Split as Spl
import Data.Maybe
import Data.Monoid
import qualified Data.Text as T
import Debug.Trace
import qualified Text.Parser.Char as Chr
import Text.Parser.Expression
import Text.Parser.LookAhead
import qualified Text.Parser.Token as Tok
import qualified Text.Parser.Token.Highlight as Hi
import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
stringLiteral, symbol, whiteSpace)
import Text.Trifecta.Delta
{- | Parses a record type declaration
Record ::=
@ -70,18 +54,9 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do
return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn
<?> "record type declaration"
where
getRecNames :: SyntaxInfo -> PTerm -> [Name]
getRecNames syn (PPi _ n _ _ sc) = [expandNS syn n, expandNS syn (mkType n)]
++ getRecNames syn sc
getRecNames _ _ = []
getName (Just (n, _), _, _, _) = Just n
getName _ = Nothing
toFreeze :: Maybe Accessibility -> Maybe Accessibility
toFreeze (Just Frozen) = Just Private
toFreeze x = x
recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))
recordBody syn tyn = do
ist <- get

12
src/Idris/Parser/Expr.hs
View File

@ -21,24 +21,12 @@ import Prelude hiding (pi)
import Control.Applicative
import Control.Monad
import Control.Monad.State.Strict
import qualified Data.ByteString.UTF8 as UTF8
import Data.Char
import Data.Function (on)
import qualified Data.HashSet as HS
import Data.List
import qualified Data.List.Split as Spl
import Data.Maybe
import Data.Monoid
import qualified Data.Text as T
import Debug.Trace
import qualified Text.Parser.Char as Chr
import Text.Parser.Expression
import Text.Parser.LookAhead
import qualified Text.Parser.Token as Tok
import qualified Text.Parser.Token.Highlight as Hi
import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
stringLiteral, symbol, whiteSpace)
import Text.Trifecta.Delta
-- | Allow implicit type declarations
allowImp :: SyntaxInfo -> SyntaxInfo

6
src/Idris/Parser/Helpers.hs
View File

@ -18,8 +18,6 @@ import Idris.Docstrings
import Idris.Options
import Idris.Output (iWarn)
import qualified Util.Pretty as Pretty (text)
import Prelude hiding (pi)
import Control.Applicative
@ -29,15 +27,11 @@ import qualified Data.ByteString.UTF8 as UTF8
import Data.Char
import qualified Data.HashSet as HS
import Data.List
import qualified Data.List.Split as Spl
import qualified Data.Map as M
import Data.Maybe
import Data.Monoid
import qualified Data.Text as T
import Debug.Trace
import System.FilePath
import qualified Text.Parser.Char as Chr
import Text.Parser.Expression
import Text.Parser.LookAhead
import qualified Text.Parser.Token as Tok
import qualified Text.Parser.Token.Highlight as Hi

13
src/Idris/Parser/Ops.hs
View File

@ -18,23 +18,10 @@ import Prelude hiding (pi)
import Control.Applicative
import Control.Monad
import Control.Monad.State.Strict
import qualified Data.ByteString.UTF8 as UTF8
import Data.Char
import qualified Data.HashSet as HS
import Data.List
import qualified Data.List.Split as Spl
import Data.Maybe
import Data.Monoid
import qualified Data.Text as T
import Debug.Trace
import qualified Text.Parser.Char as Chr
import Text.Parser.Expression
import Text.Parser.LookAhead
import qualified Text.Parser.Token as Tok
import qualified Text.Parser.Token.Highlight as Hi
import Text.Trifecta hiding (char, charLiteral, natural, span, string,
stringLiteral, symbol, whiteSpace)
import Text.Trifecta.Delta
-- | Creates table for fixity declarations to build expression parser
-- using pre-build and user-defined operator/fixity declarations

7
src/Idris/PartialEval.hs
View File

@ -19,10 +19,7 @@ import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Control.Applicative
import Control.Monad.State
import Data.Maybe
import Debug.Trace
-- | Data type representing binding-time annotations for partial evaluation of arguments
data PEArgType = ImplicitS Name -- ^ Implicit static argument
@ -261,10 +258,6 @@ mkNewPats ist d ns newname sname lhs rhs =
mkRHSargs (_ : ns) as = mkRHSargs ns as
mkRHSargs _ _ = []
mkSubst :: (Term, Term) -> Maybe (Name, Term)
mkSubst (P _ n _, t) = Just (n, t)
mkSubst _ = Nothing
-- | Creates a new declaration for a specialised function application.
-- Simple version at the moment: just create a version which is a direct
-- application of the function to be specialised.

42
src/Idris/Primitives.hs
View File

@ -9,7 +9,6 @@ Maintainer : The Idris Community.
module Idris.Primitives(primitives, Prim(..)) where
import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import IRTS.Lang
@ -18,9 +17,6 @@ import Data.Bits
import Data.Char
import Data.Function (on)
import Data.Int
import qualified Data.Vector.Unboxed as V
import Data.Word
import Debug.Trace
data Prim = Prim { p_name :: Name,
p_type :: Type,
@ -34,10 +30,9 @@ ty :: [Const] -> Const -> Type
ty [] x = Constant x
ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)
total, partial, iopartial :: Totality
total, partial :: Totality
total = Total []
partial = Partial NotCovering
iopartial = Partial ExternalIO
primitives :: [Prim]
primitives =
@ -235,36 +230,6 @@ intConv ity =
(1, LFloatInt ity) total
]
bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim
bitcastPrim from to impl prim =
Prim (sUN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)
(1, prim) total
concatWord8 :: (Word8, Word8) -> Word16
concatWord8 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 8)
concatWord16 :: (Word16, Word16) -> Word32
concatWord16 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 16)
concatWord32 :: (Word32, Word32) -> Word64
concatWord32 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 32)
truncWord16 :: Bool -> Word16 -> Word8
truncWord16 True x = fromIntegral (x `shiftR` 8)
truncWord16 False x = fromIntegral x
truncWord32 :: Bool -> Word32 -> Word16
truncWord32 True x = fromIntegral (x `shiftR` 16)
truncWord32 False x = fromIntegral x
truncWord64 :: Bool -> Word64 -> Word32
truncWord64 True x = fromIntegral (x `shiftR` 32)
truncWord64 False x = fromIntegral x
aTyName :: ArithTy -> String
aTyName (ATInt t) = intTyName t
aTyName ATFloat = "Float"
iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
iCmp ity op self impl irop totality
= Prim (sUN $ "prim__" ++ op ++ intTyName ity)
@ -295,11 +260,6 @@ bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in
Just $ I i
bfBin _ _ = Nothing
bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const
bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in
Just $ I i
bcBin _ _ = Nothing
bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const
bsBin op [Str x, Str y]
= let i = (if op x y then 1 else 0) in

18
src/Idris/ProofSearch.hs
View File

@ -16,21 +16,17 @@ module Idris.ProofSearch(
) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.Unify
import Idris.Delaborate
import Idris.Error
import Control.Applicative ((<$>))
import Control.Monad
import Control.Monad.State.Strict
import Data.List
import qualified Data.Set as S
import Debug.Trace
-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
@ -52,7 +48,6 @@ trivialHoles psnames ok elab ist
tryAll ((x, _, b):xs)
= do -- if type of x has any holes in it, move on
hs <- get_holes
let badhs = hs -- filter (flip notElem holesOK) hs
g <- goal
-- anywhere but the top is okay for a hole, if holesOK set
if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
@ -88,7 +83,6 @@ trivialTCs ok elab ist
tryAll ((x, _, b):xs)
= do -- if type of x has any holes in it, move on
hs <- get_holes
let badhs = hs -- filter (flip notElem holesOK) hs
g <- goal
env <- get_env
-- anywhere but the top is okay for a hole, if holesOK set
@ -233,9 +227,6 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
| (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs
notHole _ _ = True
inHS hs (P _ n _) = n `elem` hs
isHS _ _ = False
toUN t@(P nt (MN i n) ty)
| ('_':xs) <- str n = t
| otherwise = P nt (UN n) ty
@ -444,12 +435,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist
isMeta ns (P _ n _) = n `elem` ns
isMeta _ _ = False
notHole hs (P _ n _, c)
| (P _ cn _, _) <- unApply (getRetTy c),
n `elem` hs && isConName cn (tt_ctxt ist) = False
| Constant _ <- c = not (n `elem` hs)
notHole _ _ = True
numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]
addDefault t num@(P _ nc _) [P Bound a _] | nc == numinterface && defaultOn
@ -487,7 +472,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist
| otherwise
= do lams <- introImps
t <- goal
let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)
-- if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist
-- else do
-- if there's a hole in the goal, don't even try
@ -505,7 +489,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist
-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
mapM_ (\ (_,n) -> do focus n
t' <- goal
let (tc', ttype) = unApply (getRetTy t')
let (tc', _) = unApply (getRetTy t')
let got = fst (unApply (getRetTy t))
let depth' = if tc' `elem` tcs
then depth - 1 else depth

11
src/Idris/Prover.hs
View File

@ -11,12 +11,11 @@ module Idris.Prover (prover, showProof, showRunElab) where
-- Hack for GHC 7.10 and earlier compat without CPP or warnings
-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,
concatMap, elem, error, flip, foldl, foldr, fst, id, init,
length, lines, map, not, null, repeat, reverse, tail, zip, ($),
(&&), (++), (.), (||))
concatMap, elem, error, foldl, foldr, fst, id, init, length,
lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),
(++), (.), (||))
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.Completion
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
@ -41,7 +40,6 @@ import Util.Pretty
import Control.DeepSeq
import Control.Monad.State.Strict
import Debug.Trace
import System.Console.Haskeline
import System.Console.Haskeline.History
import System.IO (Handle, hPutStrLn, stdin, stdout)
@ -166,7 +164,7 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do
iputGoal rendered
where
(h : hs) = holes ps -- apparently the pattern guards don't give us this
(h : _) = holes ps -- apparently the pattern guards don't give us this
ppo = ppOptionIst ist
@ -502,7 +500,6 @@ checkType e prf t = do
putIState ist { tt_ctxt = ctxt' }
(tm, ty) <- elabVal (recinfo proverfc) ERHS t
let ppo = ppOptionIst ist
ty' = normaliseC ctxt [] ty
infixes = idris_infixes ist
action = case tm of
TType _ ->

2
src/Idris/Providers.hs
View File

@ -13,8 +13,6 @@ module Idris.Providers (
) where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Error

29
src/Idris/REPL.hs
View File

@ -6,6 +6,8 @@ Maintainer : The Idris Community.
-}
{-# LANGUAGE FlexibleContexts, PatternGuards #-}
-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.REPL
( idemodeStart
@ -49,7 +51,6 @@ import Idris.Core.Execute (execute)
import Idris.Core.TT
import Idris.Core.Unify
import Idris.Core.WHNF
import Idris.Coverage
import Idris.DataOpts
import Idris.Delaborate
import Idris.Docs
@ -99,8 +100,6 @@ import Util.Pretty hiding ((</>))
import Util.System
import Version_idris (gitHash)
import Debug.Trace
-- | Run the REPL
repl :: IState -- ^ The initial state
-> [FilePath] -- ^ The loaded modules
@ -404,7 +403,6 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
| (n, (_, i, _, _, _)) <- idris_metavars ist
, not (n `elem` primDefs)
]
let ppo = ppOptionIst ist
-- splitMvs is a list of pairs of names and their split types
let splitMvs = [ (n, (premises, concl, tm))
| (n, i, ty) <- mvTys ist mvs
@ -422,14 +420,11 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
runIO . hPutStrLn h $
IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id
where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
firstOfThree (x, y, z) = x
mapThird f xs = map (\(x, y, z) -> (x, y, f z)) xs
-- | Split a function type into a pair of premises, conclusion.
-- Each maintains both the original and delaborated versions.
splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =
let (hs, c, pc) = splitPi ist (i - 1) rest in
let (hs, c, _) = splitPi ist (i - 1) rest in
((n, t, delabTy' ist [] [] t False False True):hs,
c, delabTy' ist [] [] c False False True)
splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)
@ -982,7 +977,7 @@ process fn (Check (PRef _ _ n))
= do ctxt <- getContext
ist <- getIState
let ppo = ppOptionIst ist
case lookupNames n ctxt of
case lookupVisibleNames n ctxt of
ts@(t:_) ->
case lookup t (idris_metavars ist) of
Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $
@ -990,6 +985,9 @@ process fn (Check (PRef _ _ n))
Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)
[] -> iPrintError $ "No such variable " ++ show n
where
lookupVisibleNames :: Name -> Context -> [Name]
lookupVisibleNames n ctxt = map fst $ lookupCtxtName n (visibleDefinitions ctxt)
showMetavarInfo ppo ist n i
= case lookupTy n (tt_ctxt ist) of
(ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in
@ -1020,8 +1018,7 @@ process fn (Check t)
= do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t
ctxt <- getContext
ist <- getIState
let ppo = ppOptionIst ist
ty' = if opt_evaltypes (idris_options ist)
let ty' = if opt_evaltypes (idris_options ist)
then normaliseC ctxt [] ty
else ty
case tm of
@ -1126,7 +1123,6 @@ process fn (DebugInfo n)
when (not (null imps)) $ iputStrLn (show imps)
let d = lookupDefAcc n False (tt_ctxt i)
when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
let cg = lookupCtxtName n (idris_callgraph i)
i <- getIState
let cg' = lookupCtxtName n (idris_callgraph i)
sc <- checkSizeChange n
@ -1457,12 +1453,6 @@ process fn (TransformInfo n)
ts' = showTrans i ts in
ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'
-- iRenderOutput (pretty lhs)
-- iputStrLn " ==> "
-- iPrintTermWithType (pprintDelab i rhs)
-- iputStrLn "---------------"
-- showTrans i ts
process fn (PPrint fmt width (PRef _ _ n))
= do outs <- pprintDef False n
iPrintResult =<< renderExternal fmt width (vsep outs)
@ -1470,10 +1460,7 @@ process fn (PPrint fmt width (PRef _ _ n))
process fn (PPrint fmt width t)
= do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
ctxt <- getContext
ist <- getIState
let ppo = ppOptionIst ist
ty' = normaliseC ctxt [] ty
iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

7
src/Idris/REPL/Parser.hs
View File

@ -21,17 +21,14 @@ import Idris.REPL.Commands
import Control.Applicative
import Control.Monad.State.Strict
import qualified Data.ByteString.UTF8 as UTF8
import Data.Char (isSpace, toLower)
import Data.List
import Data.List.Split (splitOn)
import Debug.Trace
import System.Console.ANSI (Color(..))
import System.FilePath ((</>))
import Text.Parser.Char (anyChar, oneOf)
import Text.Parser.Combinators
import Text.Trifecta (Result, parseString)
import Text.Trifecta.Delta
import Text.Trifecta (Result)
parseCmd :: IState -> String -> String -> Result (Either String Command)
parseCmd i inputname = P.runparser pCmd i inputname . trim
@ -181,8 +178,6 @@ namespaceArgCmd names command doc =
(names, NamespaceArg, doc, namespaceArg command)
exprArgCmd names command doc =
(names, ExprArg, doc, exprArg command)
metavarArgCmd names command doc =
(names, MetaVarArg, doc, fnNameArg command)
optArgCmd names command doc =
(names, OptionArg, doc, optArg command)
proofArgCmd names command doc =

14
src/Idris/Termination.hs
View File

@ -15,10 +15,9 @@ import Idris.Core.TT
import Idris.Delaborate
import Idris.Error
import Idris.Options
import Idris.Output (iWarn, iputStrLn)
import Idris.Output (iWarn)
import Control.Monad.State.Strict
import Data.Char
import Data.Either
import Data.List
import Data.Maybe
@ -143,9 +142,6 @@ checkPositive mut_ns (cn, ty')
calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
calcTotality fc n pats
= do i <- getIState
let opts = case lookupCtxt n (idris_flags i) of
[fs] -> fs
_ -> []
case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
(failure : _) -> return failure
_ -> checkSizeChange n
@ -302,7 +298,7 @@ buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
scgPat (lhs, rhs) = let lhs' = delazy lhs
rhs' = delazy rhs
(f, pargs) = unApply (dePat lhs') in
(_, pargs) = unApply (dePat lhs') in
findCalls [] Toplevel (dePat rhs') (patvars lhs')
(zip pargs [0..])
@ -393,7 +389,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
fccPat cases pvs pargs args g (lhs, rhs)
= let lhs' = delazy lhs
rhs' = delazy rhs
(f, pargs_case) = unApply (dePat lhs')
(_, pargs_case) = unApply (dePat lhs')
-- pargs is a pair of a term, and the argument position that
-- term appears in. If any of the arguments to the case block
-- are also on the lhs, we also want those patterns to appear
@ -545,10 +541,6 @@ checkMP ist topfn i mp = if i > 0
collapse paths
else tryPath 0 [] mp 0
where
tryPath' d path mp arg
= let res = tryPath d path mp arg in
trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
mkBig (e, d) = (e, 10000)
tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

3
src/Idris/Transforms.hs
View File

@ -16,11 +16,8 @@ module Idris.Transforms(
) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.TT
import Debug.Trace
transformPats :: IState -> [Either Term (Term, Term)] ->
[Either Term (Term, Term)]
transformPats ist ps = map tClause ps where

8
src/Idris/TypeSearch.hs
View File

@ -13,8 +13,7 @@ module Idris.TypeSearch (
, defaultScoreFunction
) where
import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,
logLvl, putIState)
import Idris.AbsSyntax (addUsingConstraints, getIState, implicit, putIState)
import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),
Idris, InterfaceInfo, OutputMode(..), PTerm,
defaultSyntax, eqTy, implicitAllowed,
@ -58,7 +57,6 @@ searchByType pkgs pterm = do
mapM_ loadPkgIndex pkgs
pterm' <- addUsingConstraints syn emptyFC pterm
pterm'' <- implicit toplevel syn name pterm'
let pterm''' = addImpl [] i pterm''
ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'
let names = searchUsing searchPred i ty
let names' = take numLimit names
@ -304,7 +302,7 @@ interfaceUnify interfaceInfo ctxt ty tyTry = do
isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool
isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where
(clss, args) = unApply ty
(clss, _) = unApply ty
getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]
getInterfaceName _ = []
@ -358,8 +356,6 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
usedns = map fst startingHoles
startingHoles = argNames1 ++ argNames2
startingTypes = [(retTy1, retTy2)]
startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types

29
src/Util/DynamicLinker.hs
View File

@ -13,22 +13,29 @@ module Util.DynamicLinker ( ForeignFun(..)
) where
#ifdef IDRIS_FFI
import Foreign.LibFFI
import Foreign.Ptr (FunPtr, Ptr, castPtrToFunPtr, nullFunPtr, nullPtr)
import System.Directory
#ifndef mingw32_HOST_OS
import Control.Exception (IOException, throwIO, try)
import Data.Array (Array, bounds, inRange, (!))
import Data.Functor ((<$>))
import Data.Maybe (catMaybes)
import System.FilePath.Posix ((</>))
import System.Posix.DynamicLinker
import Text.Regex.TDFA
#else
#ifdef mingw32_HOST_OS
import qualified Control.Exception as Exception (IOException, catch)
import Foreign.Ptr (FunPtr, castPtrToFunPtr, nullFunPtr, nullPtr)
import System.FilePath.Windows ((</>))
import System.Win32.DLL
import System.Win32.Types
#else
import Control.Exception (IOException, throwIO, try)
import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr)
#ifdef linux_HOST_OS
import Data.Array (bounds, inRange, (!))
import Data.Functor ((<$>))
import Data.Maybe (catMaybes)
#else
import Data.Array (bounds, (!))
#endif
import System.FilePath.Posix ((</>))
import System.Posix.DynamicLinker
import Text.Regex.TDFA
#endif
#ifdef mingw32_HOST_OS
type DL = HMODULE
#endif

3
stack.yaml
View File

@ -9,6 +9,9 @@ flags:
FFI: true
GMP: true
ghc-options:
idris: -fwarn-unused-imports -fwarn-unused-binds
extra-deps:
- binary-0.8.5.1
- cheapskate-0.1.1

10
test/TestData.hs
View File

@ -71,7 +71,9 @@ testFamiliesData = [
( 16, ANY ),
( 17, ANY ),
( 18, ANY ),
( 19, ANY )]),
( 19, ANY ),
( 20, ANY ),
( 21, ANY )]),
("bignum", "Bignum",
[ ( 1, ANY ),
( 2, ANY )]),
@ -157,7 +159,11 @@ testFamiliesData = [
( 13, ANY ),
( 14, C_CG ),
( 15, ANY ),
( 16, ANY )]),
( 16, ANY ),
-- FIXME: Re-enable interactive017 once it works with and without node.
-- FIXME: See https://github.com/idris-lang/Idris-dev/pull/4046#issuecomment-326910042
-- ( 17, ANY ),
( 18, ANY )]),
("interfaces", "Interfaces",
[ ( 1, ANY ),
( 2, ANY ),

42
test/basic020/basic020.idr Normal file
View File

@ -0,0 +1,42 @@
%default total
data Ty = Ctor Int
fn : Ty -> Ty
fn m@(Ctor _) = y
where
y = m -- from @ pattern
asPatternVisibleInWhere : fn (Ctor 42) = Ctor 42
asPatternVisibleInWhere = Refl
fn2 : Ty -> Ty
fn2 m@(Ctor _) = y (Ctor 99)
where
y m = m -- should be the arg `m`, not the @ pattern
lhsVariablesShadowAsPattern : fn2 (Ctor 42) = Ctor 99
lhsVariablesShadowAsPattern = Refl
fn3 : Ty -> Ty
fn3 m@(Ctor _) = y (Ctor 99)
where
y m = z
where
z = m -- should be y's arg `m`, not @ pattern
nestedWhereShadowsAsPattern : fn3 (Ctor 42) = Ctor 99
nestedWhereShadowsAsPattern = Refl
fn4 : Ty -> Ty
fn4 m@(Ctor _) = y (Ctor 99)
where
y _ = z
where
z = m -- should be @ pattern
nestedWhereExposesAsPattern : fn4 (Ctor 42) = Ctor 42
nestedWhereExposesAsPattern = Refl
main : IO ()
main = putStrLn "OK"

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