idris 0.9.20.1 → 0.9.20.2

raw patch · 64 files changed

+730/−289 lines, 64 filesdep ~zlib

Dependency ranges changed: zlib

Files

• README.md +8/−42
• idris.cabal +12/−2
• libs/base/Data/Complex.idr +8/−8
• libs/base/Data/List/Quantifiers.idr +75/−0
• libs/base/Data/String.idr +75/−19
• libs/base/Data/Vect/Quantifiers.idr +1/−0
• libs/base/Language/Reflection/Utils.idr +8/−2
• libs/base/System.idr +1/−1
• libs/base/base.ipkg +1/−0
• libs/contrib/Control/Algebra/NumericInstances.idr +7/−7
• libs/effects/Effect/Default.idr +1/−1
• libs/effects/Effect/File.idr +6/−6
• libs/prelude/Builtins.idr +17/−2
• libs/prelude/Decidable/Equality.idr +1/−1
• libs/prelude/IO.idr +2/−2
• libs/prelude/Language/Reflection.idr +9/−9
• libs/prelude/Language/Reflection/Elab.idr +21/−8
• libs/prelude/Prelude.idr +10/−0
• libs/prelude/Prelude/Classes.idr +6/−6
• libs/prelude/Prelude/Either.idr +7/−3
• libs/prelude/Prelude/File.idr +35/−7
• libs/prelude/Prelude/Interactive.idr +2/−2
• libs/prelude/Prelude/List.idr +7/−3
• libs/prelude/Prelude/Maybe.idr +8/−5
• libs/prelude/Prelude/Nat.idr +3/−0
• libs/prelude/Prelude/Stream.idr +4/−1
• libs/pruviloj/Pruviloj/Core.idr +2/−2
• libs/pruviloj/Pruviloj/Derive/DecEq.idr +2/−4
• libs/pruviloj/Pruviloj/Derive/Eliminators.idr +2/−5
• libs/pruviloj/Pruviloj/Internals.idr +1/−1
• rts/idris_gmp.c +106/−0
• rts/idris_gmp.h +5/−0
• src/IRTS/CodegenC.hs +5/−0
• src/IRTS/CodegenJavaScript.hs +1/−2
• src/IRTS/JavaScript/AST.hs +4/−1
• src/Idris/AbsSyntaxTree.hs +2/−2
• src/Idris/Coverage.hs +0/−50
• src/Idris/DSL.hs +3/−3
• src/Idris/Delaborate.hs +2/−2
• src/Idris/Elab/Clause.hs +3/−3
• src/Idris/Elab/Term.hs +37/−11
• src/Idris/Erasure.hs +3/−6
• src/Idris/IBC.hs +3/−3
• src/Idris/REPL.hs +2/−2
• src/Idris/Reflection.hs +44/−16
• src/Util/System.hs +11/−7
• stack.yaml +9/−2
• test/dsl002/test014.idr +2/−2
• test/ffi001/test022.idr +2/−2
• test/interactive010/expected +3/−3
• test/interactive012/run +1/−1
• test/io001/test004.idr +3/−3
• test/meta001/Finite.idr +13/−13
• test/meta002/Deriving.idr +2/−0
• test/meta002/run +2/−1
• test/meta004/expected +3/−0
• test/meta004/meta004.idr +48/−0
• test/meta004/run +3/−0
• test/proofsearch002/proofsearch002.idr +0/−3
• test/quasiquote001/expected +2/−2
• test/reg067/expected +1/−0
• test/reg067/reg067.idr +23/−0
• test/reg067/run +5/−0
• test/runtest.pl +35/−0

@@ -7,50 +7,16 @@ Idris (http://idris-lang.org/) is a general-purpose functional programming language with dependent types. -## Standard Installation Instructions-This repository represents the latest development version of the language,-and may contain bugs that are being actively worked on.-For those who wish to use a more stable version of Idris please consider-installing the latest version that has been released on Hackage.-Installation instructions for various platforms can be [found on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions).--## Installing Development Versions--If you like to work against the latest development version, please consider-using Cabal Sandboxes to minimise disruption to your local Haskell setup.-Instructions for installing Idris HEAD within a cabal sandbox are-[available on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installing-an-Idris-Development-version-in-a-sandbox).--To configure, edit config.mk. The default values should work for most people.--Idris is built using a Makefile common targets include:--* `make` This will install everything using cabal and-typecheck the libraries.-* `make test` This target execute the test suite.-* `make relib` This target will typecheck and recompile the standard library.--Idris has an optional buildtime dependency on the C library `libffi`. If you-would like to use the features that it enables, make sure that it is compiled-for the same architecture as your Haskell compiler (e.g. 64 bit libraries-for 64 bit ghc). By default, Idris builds without it. To build with it, pass-the flag `-f FFI`.--To build with `libffi` by default, create a `custom.mk` file and add the-following line to it:--`CABALFLAGS += -f FFI`--The file custom.mk-alldeps is a suitable example.--The continuous integration builds on travis-ci.org are built using the-ghc-flag -Werror. To enable this behaviour locally also, please compile-using `make CI=true` or adding the following line into `custom.mk`:+## Installation Guides. -`CI = true`+This repository represents the latest development version of the+language, and may contain bugs that are being actively worked on.  For+those who wish to use a more stable version of Idris please consider+installing the latest version that has been released on Hackage.+Installation instructions for various platforms can be+[found on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions). -If you are only compiling for installing the most current version, you can-omit the CI flag, but please make sure you use it if you want to contribute.+More information about building Idris from source has been detailed in the [Installation Guide](INSTALL.md)  ## Code Generation 

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.20.1+Version:        0.9.20.2 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -115,6 +115,7 @@                        libs/base/Control/*.idr                        libs/base/Control/Monad/*.idr                        libs/base/Data/*.idr+                       libs/base/Data/List/*.idr                        libs/base/Data/Vect/*.idr                        libs/base/Debug/*.idr                        libs/base/Language/Reflection/*.idr@@ -309,6 +310,9 @@                        test/reg066/run                        test/reg066/*.idr                        test/reg066/expected+                       test/reg067/run+                       test/reg067/*.idr+                       test/reg067/expected                         test/basic001/run                        test/basic001/*.idr@@ -570,6 +574,9 @@                        test/meta002/run                        test/meta002/*.idr                        test/meta002/expected+                       test/meta004/run+                       test/meta004/*.idr+                       test/meta004/expected                         test/primitives001/run                        test/primitives001/*.idr@@ -971,8 +978,11 @@                 , vector < 0.12                 , vector-binary-instances < 0.3                 , zip-archive > 0.2.3.5 && < 0.2.4-                , zlib < 0.6                 , safe+  -- zlib >= 0.6.1 is broken with GHC < 7.10.3+  if impl(ghc < 7.10.3)+     build-depends: zlib < 0.6.1+   Extensions:     MultiParamTypeClasses                 , DeriveFoldable                 , DeriveTraversable

@@ -25,7 +25,7 @@             plus_i = User 6  --- when we have a type class 'Fractional' (which contains Float and Double),+-- when we have a type class 'Fractional' (which contains Double), -- we can do: {- instance Fractional a => Fractional (Complex a) where@@ -40,16 +40,16 @@  ------------------------------ Polarform -mkPolar : Float -> Float -> Complex Float+mkPolar : Double -> Double -> Complex Double mkPolar radius angle = radius * cos angle :+ radius * sin angle -cis : Float -> Complex Float+cis : Double -> Complex Double cis angle = cos angle :+ sin angle -magnitude : Complex Float -> Float+magnitude : Complex Double -> Double magnitude (r:+i) = sqrt (r*r+i*i) -phase : Complex Float -> Float+phase : Complex Double -> Double phase (x:+y) = atan2 y x  @@ -62,13 +62,13 @@     map f (r :+ i) = f r :+ f i  -- We can't do "instance Num a => Num (Complex a)" because--- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float-instance Num (Complex Float) where+-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double+instance Num (Complex Double) where     (+) (a:+b) (c:+d) = ((a+c):+(b+d))     (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))     fromInteger x = (fromInteger x:+0) -instance Neg (Complex Float) where+instance Neg (Complex Double) where     negate = map negate     (-) (a:+b) (c:+d) = ((a-c):+(b-d))     abs (a:+b) = (magnitude (a:+b):+0)

@@ -0,0 +1,75 @@+module Data.List.Quantifiers++import Data.List++||| A proof that some element of a list satisfies some property+|||+||| @ P the property to be satsified+data Any : (P : a -> Type) -> List a -> Type where+  ||| A proof that the satisfying element is the first one in the `List`+  Here  : {P : a -> Type} -> {xs : List a} -> P x -> Any P (x :: xs)+  ||| A proof that the satsifying element is in the tail of the `List`+  There : {P : a -> Type} -> {xs : List a} -> Any P xs -> Any P (x :: xs)++||| No element of an empty list satisfies any property+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void+anyNilAbsurd (Here _) impossible+anyNilAbsurd (There _) impossible++instance Uninhabited (Any p Nil) where+  uninhabited = anyNilAbsurd++||| Eliminator for `Any`+anyElim : {xs : List a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b+anyElim _ f (Here p) = f p+anyElim f _ (There p) = f p++||| Given a decision procedure for a property, determine if an element of a+||| list satisfies it.+|||+||| @ P the property to be satisfied+||| @ dec the decision procedure+||| @ xs the list to examine+any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : List a) -> Dec (Any P xs)+any _ Nil = No anyNilAbsurd+any p (x::xs) with (p x)+  | Yes prf = Yes (Here prf)+  | No prf =+    case any p xs of+      Yes prf' => Yes (There prf')+      No prf' => No (anyElim prf' prf)++||| A proof that all elements of a list satisfy a property. It is a list of+||| proofs, corresponding element-wise to the `List`.+data All : (P : a -> Type) -> List a -> Type where+  Nil : {P : a -> Type} -> All P Nil+  (::) : {P : a -> Type} -> {xs : List a} -> P x -> All P xs -> All P (x :: xs)++||| If there does not exist an element that satifies the property, then it is+||| the case that all elements do not satisfy.+negAnyAll : {P : a -> Type} -> {xs : List a} -> Not (Any P xs) -> All (\x => Not (P x)) xs+negAnyAll {xs=Nil} _ = Nil+negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))++notAllHere : {P : a -> Type} -> {xs : List a} -> Not (P x) -> All P (x :: xs) -> Void+notAllHere _ Nil impossible+notAllHere np (p :: _) = np p++notAllThere : {P : a -> Type} -> {xs : List a} -> Not (All P xs) -> All P (x :: xs) -> Void+notAllThere _ Nil impossible+notAllThere np (_ :: ps) = np ps++||| Given a decision procedure for a property, decide whether all elements of+||| a list satisfy it.+|||+||| @ P the property+||| @ dec the decision procedure+||| @ xs the list to examine+all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : List a) -> Dec (All P xs)+all _ Nil = Yes Nil+all d (x::xs) with (d x)+  | No prf = No (notAllHere prf)+  | Yes prf =+    case all d xs of+      Yes prf' => Yes (prf :: prf')+      No prf' => No (notAllThere prf')

@@ -1,5 +1,14 @@ module Data.String +private+parseNumWithoutSign : List Char -> Integer -> Maybe Integer+parseNumWithoutSign []        acc = Just acc+parseNumWithoutSign (c :: cs) acc = +  if (c >= '0' && c <= '9') +  then parseNumWithoutSign cs ((acc * 10) + (cast ((ord c) - (ord '0'))))+  else Nothing+         + ||| Convert a positive number string to a Num. ||| ||| ```idris example@@ -15,15 +24,8 @@       parsePosTrimmed ""             | StrNil         = Nothing       parsePosTrimmed (strCons x xs) | (StrCons x xs) =          if (x == '+') -          then map fromInteger (parsePosAux (unpack xs) 0)-          else map fromInteger (parsePosAux (unpack xs)  (cast (ord x - ord '0')))-            where-              parsePosAux : List Char -> Integer -> Maybe Integer-              parsePosAux []        acc = Just acc-              parsePosAux (c :: cs) acc = -                if (c >= '0' && c <= '9') -                  then parsePosAux cs ((acc * 10) + (cast ((ord c) - (ord '0'))))-                  else Nothing+          then map fromInteger (parseNumWithoutSign (unpack xs) 0)+          else map fromInteger (parseNumWithoutSign (unpack xs)  (cast (ord x - ord '0')))   ||| Convert a number string to a Num.@@ -41,14 +43,68 @@       parseIntTrimmed ""             | StrNil         = Nothing       parseIntTrimmed (strCons x xs) | (StrCons x xs) =          if (x == '-') -          then map (\y => negate (fromInteger y)) (parseIntegerAux (unpack xs) 0)+          then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0)           else if (x == '+') -            then map fromInteger (parseIntegerAux (unpack xs) (cast {from=Int} 0))-            else map fromInteger (parseIntegerAux (unpack xs) (cast (ord x - ord '0')))-              where-                parseIntegerAux : List Char -> Integer -> Maybe Integer-                parseIntegerAux []        acc = Just acc-                parseIntegerAux (c :: cs) acc = -                  if (c >= '0' && c <= '9') -                    then parseIntegerAux cs ((acc * 10) + (cast ((ord c) - (ord '0'))))-                    else Nothing+            then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0))+            else map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))+++||| Convert a number string to a Double.+|||+||| ```idris example+||| parseDouble "+123.123e-2"+||| ```+||| ```idris example+||| parseDouble {a=Int} " -123.123E+2"+||| ```+||| ```idris example+||| parseDouble {a=Int} " +123.123"+||| ```+parseDouble : String -> Maybe Double+parseDouble = mkDouble . wfe . trim+  where+    mkDouble (Just (w, f, e)) = let ex = intPow 10 e in+                                Just $ (w * ex + f * ex)+    mkDouble Nothing = Nothing+    +    %assert_total+    intPow : Integer -> Integer -> Double+    intPow base exp = if exp > 0 then (num base exp) else 1 / (num base exp)+      where+        num base 0 = 1+        num base e = if e < 0 +                     then cast base * num base (e + 1)+                     else cast base * num base (e - 1)++    wfe : String -> Maybe (Double, Double, Integer)+    wfe cs = case split (== '.') cs of+               (wholeAndExp :: []) => +                 case split (\c => c == 'e' || c == 'E') wholeAndExp of+                   (whole::exp::[]) =>  +                     do+                       w <- cast <$> parseInteger whole+                       e <- parseInteger exp+                       return (w, 0, e)+                   (whole::[]) =>      +                     do+                       w <- cast <$> parseInteger whole+                       return (w, 0, 0)+                   _ => Nothing+               (whole::fracAndExp::[]) =>+                 case split (\c => c == 'e' || c == 'E') fracAndExp of+                   (""::exp::[]) => Nothing+                   (frac::exp::[]) =>  +                     do+                       w <- cast <$> parseInteger whole+                       f <- (/ (pow 10 (length frac))) <$> +                            (cast <$> parseNumWithoutSign (unpack frac) 0)+                       e <- parseInteger exp+                       return (w, if w < 0 then (-f) else f, e)+                   (frac::[]) =>      +                     do+                       w <- cast <$> parseInteger whole+                       f <- (/ (pow 10 (length frac))) <$> +                            (cast <$> parseNumWithoutSign (unpack frac) 0)+                       return (w, if w < 0 then (-f) else f, 0)+                   _ => Nothing+               _ => Nothing

@@ -19,6 +19,7 @@ instance Uninhabited (Any p Nil) where   uninhabited = anyNilAbsurd +||| Eliminator for `Any` anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b anyElim _ f (Here p) = f p anyElim f _ (There p) = f p

@@ -129,7 +129,7 @@  instance Show ArithTy where   showPrec d (ATInt t) = showCon d "ATInt" $ showArg t-  showPrec d ATFloat   = "ATFloat"+  showPrec d ATDouble   = "ATDouble"  instance Show Const where   showPrec d (I i)      = showCon d "I" $ showArg i@@ -162,7 +162,7 @@  instance Eq ArithTy where   (ATInt x) == (ATInt y) = x == y-  ATFloat   == ATFloat   = True+  ATDouble  == ATDouble   = True   _         == _         = False  instance Eq Const where@@ -349,3 +349,9 @@ instance Show TyDecl where   showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++                                      showArg args ++ showArg ret++instance Show tm => Show (FunClause tm) where+  showPrec d (MkFunClause lhs rhs) =+      showCon d "MkFunClause" $ showArg lhs ++ showArg rhs+  showPrec d (MkImpossibleClause lhs) =+      showCon d "MkImpossibleClause" $ showArg lhs

@@ -56,7 +56,7 @@ exit : Int -> IO () exit code = foreign FFI_C "exit" (Int -> IO ()) code -||| Get the Unix time+||| Get the numbers of sections since 1st January 1970, 00:00 UTC  time : IO Integer time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))           return t

@@ -17,6 +17,7 @@           Data.HVect, Data.Vect.Quantifiers,           Data.Complex,           Data.Erased, Data.List,+          Data.List.Quantifiers,           Data.So, Data.String,            Control.Isomorphism,

@@ -44,24 +44,24 @@   unity = 1  -instance Semigroup Float where+instance Semigroup Double where   (<+>) = (+) -instance Monoid Float where+instance Monoid Double where   neutral = 0 -instance Group Float where+instance Group Double where   inverse = (* -1) -instance AbelianGroup Float+instance AbelianGroup Double -instance Ring Float where+instance Ring Double where   (<.>) = (*) -instance RingWithUnity Float where+instance RingWithUnity Double where   unity = 1 -instance Field Float where+instance Field Double where   inverseM f _ = 1 / f  

@@ -11,7 +11,7 @@ instance Default Integer where     default = 0 -instance Default Float where+instance Default Double where     default = 0  instance Default Nat where

@@ -79,14 +79,14 @@                                     k True (FH h)     handle (FH h) Close      k = do closeFile h                                     k () ()-    handle (FH h) ReadLine        k = do Right str <- fread h+    handle (FH h) ReadLine        k = do Right str <- fGetLine h                                          -- Need proper error handling!                                              | Left err => k "" (FH h)                                          k str (FH h)-    handle (FH h) (WriteString str) k = do Right () <- fwrite h str+    handle (FH h) (WriteString str) k = do Right () <- fPutStr h str                                              | Left err => k () (FH h)                                            k () (FH h)-    handle (FH h) EOF             k = do e <- feof h+    handle (FH h) EOF             k = do e <- fEOF h                                          k e (FH h)  instance Handler FileIO (IOExcept a) where@@ -95,14 +95,14 @@                                     k True (FH h)     handle (FH h) Close      k = do ioe_lift $ closeFile h                                     k () ()-    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fread h+    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fGetLine h                                          -- Need proper error handling!                                              | Left err => k "" (FH h)                                          k str (FH h)-    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fwrite h str+    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fPutStr h str                                              | Left err => k () (FH h)                                            k () (FH h)-    handle (FH h) EOF             k = do e <- ioe_lift $ feof h+    handle (FH h) EOF             k = do e <- ioe_lift $ fEOF h                                          k e (FH h)  -- -------------------------------------------------------------- [ The Effect ]

@@ -19,6 +19,10 @@      ||| @b the right element of the pair      MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B +  -- Usage hints for erasure analysis+  %used MkPair a+  %used MkPair b+   ||| The non-dependent pair type, also known as conjunction, usable with   ||| UniqueTypes.   ||| @A the type of the left elements in the pair@@ -29,6 +33,10 @@      ||| @b the right element of the pair      MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B +  -- Usage hints for erasure analysis+  %used MkUPair a+  %used MkUPair b+   ||| Dependent pairs   |||   ||| Dependent pairs represent existential quantification - they consist of a@@ -48,7 +56,12 @@      ||| The eliminator for the `Void` type. void : Void -> a-void {a} v = elim_for Void (\_ => a) v+-- We can't define void yet. We can't define a function with no clauses without+-- elaborator reflection, and we can't do elaborator reflection without+-- Language.Reflection.Elab, and Language.Reflection.Elab depends on Builtins.+-- We can't delay the declaration of void, because Prelude.Uninhabited depends on+-- it, Prelude.Nat depends on Prelude.Uninhabited, and Language.Reflection.Elab+-- depends on Prelude.Nat. Instead, void is defined in Prelude.idr  ||| For 'symbol syntax. 'foo becomes Symbol_ "foo" data Symbol_ : String -> Type where@@ -152,9 +165,11 @@ really_believe_me : a -> b really_believe_me x = prim__believe_me _ _ x --- Deprecated - for backward compatibility+||| Deprecated alias for `Double`, for the purpose of backwards+||| compatibility. Idris does not support 32 bit floats at present. Float : Type Float = Double+%deprecate Float  -- Pointers as external primitive; there's no literals for these, so no -- need for them to be part of the compiler.

@@ -178,7 +178,7 @@ instance DecEq Integer where     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq        where primitiveEq : x = y-             primitiveEq = believe_me (Refl {x})+             primitiveEq = really_believe_me (Refl {x})              postulate primitiveNotEq : x = y -> Void  

@@ -162,7 +162,7 @@   ||| Supported C foreign types   data C_Types : Type -> Type where        C_Str   : C_Types String-       C_Float : C_Types Float+       C_Float : C_Types Double        C_Ptr   : C_Types Ptr        C_MPtr  : C_Types ManagedPtr        C_Unit  : C_Types ()@@ -221,7 +221,7 @@    data JS_Types : Type -> Type where        JS_Str   : JS_Types String-       JS_Float : JS_Types Float+       JS_Float : JS_Types Double        JS_Ptr   : JS_Types Ptr        JS_Unit  : JS_Types ()        JS_FnT   : JS_FnTypes a -> JS_Types (JsFn a)

@@ -70,10 +70,10 @@  data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar -data ArithTy = ATInt Language.Reflection.IntTy | ATFloat+data ArithTy = ATInt Language.Reflection.IntTy | ATDouble  ||| Primitive constants-data Const = I Int | BI Integer | Fl Float | Ch Char | Str String+data Const = I Int | BI Integer | Fl Double | Ch Char | Str String            | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64            | AType ArithTy | StrType            | VoidType | Forgot@@ -89,7 +89,7 @@ instance ReflConst Integer where    toConst = BI -instance ReflConst Float where+instance ReflConst Double where    toConst = Fl  instance ReflConst Char where@@ -366,12 +366,12 @@   quotedTy = `(Int)   quote x = RConstant (I x) -instance Quotable Float TT where-  quotedTy = `(Float)+instance Quotable Double TT where+  quotedTy = `(Double)   quote x = TConst (Fl x) -instance Quotable Float Raw where-  quotedTy = `(Float)+instance Quotable Double Raw where+  quotedTy = `(Double)   quote x = RConstant (Fl x)  instance Quotable Char TT where@@ -541,12 +541,12 @@ instance Quotable ArithTy TT where   quotedTy = `(ArithTy)   quote (ATInt x) = `(ATInt ~(quote x))-  quote ATFloat = `(ATFloat)+  quote ATDouble = `(ATDouble)  instance Quotable ArithTy Raw where   quotedTy = `(ArithTy)   quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))-  quote ATFloat = `(ATFloat)+  quote ATDouble = `(ATDouble)  instance Quotable Const TT where   quotedTy = `(Const)

@@ -69,17 +69,16 @@   returnType : Raw  --- Note: FunClause is not a record because impossible clauses may be--- added at some point. ||| A single pattern-matching clause-data FunClause : Type where-  MkFunClause : (lhs, rhs : Raw) -> FunClause+data FunClause : Type -> Type where+  MkFunClause : (lhs, rhs : a) -> FunClause a+  MkImpossibleClause : (lhs : a) -> FunClause a  ||| A reflected function definition.-record FunDefn where+record FunDefn a where   constructor DefineFun   name : TTName-  clauses : List FunClause+  clauses : List (FunClause a)   data CtorArg = CtorParameter FunArg | CtorField FunArg@@ -116,6 +115,7 @@   Prim__Guess : Elab TT   Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))   Prim__LookupDatatype : TTName -> Elab (List Datatype)+  Prim__LookupFunDefn : TTName -> Elab (List (FunDefn TT))   Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))    Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)@@ -148,7 +148,7 @@   Prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()    Prim__DeclareType : TyDecl -> Elab ()-  Prim__DefineFunction : FunDefn -> Elab ()+  Prim__DefineFunction : FunDefn Raw -> Elab ()   Prim__AddInstance : TTName -> TTName -> Elab ()   Prim__IsTCName : TTName -> Elab Bool @@ -231,7 +231,20 @@                             []    => fail [TextPart "No datatype named", NamePart n]                             xs    => fail [TextPart "More than one datatype named", NamePart n] +  ||| Find the reflected function definition of all functions whose names+  ||| are overloadings of some name.+  lookupFunDefn : TTName -> Elab (List (FunDefn TT))+  lookupFunDefn n = Prim__LookupFunDefn n +  ||| Find the reflected function definition of a function, given its+  ||| fully-qualified name. Fail if the name does not uniquely resolve+  ||| to a function.+  lookupFunDefnExact : TTName -> Elab (FunDefn TT)+  lookupFunDefnExact n = case !(lookupFunDefn n) of+                           [res] => return res+                           []    => fail [TextPart "No function named", NamePart n]+                           xs    => fail [TextPart "More than one function named", NamePart n]+   ||| Get the argument specification for each overloading of a name.   lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))   lookupArgs n = Prim__LookupArgs n@@ -452,7 +465,7 @@   ||| Define a function in the global context. The function must have   ||| already been declared, either in ordinary Idris code or using   ||| `declareType`.-  defineFunction : FunDefn -> Elab ()+  defineFunction : FunDefn Raw -> Elab ()   defineFunction defun = Prim__DefineFunction defun    ||| Register a new instance for type class resolution.

@@ -37,6 +37,10 @@ %default total  -- Things that can't be elsewhere for import cycle reasons+-- See comment after declaration of void in Builtins.idr+-- for explanation of this definition's location+%runElab (defineFunction $ DefineFun `{void} [])+ decAsBool : Dec p -> Bool decAsBool (Yes _) = True decAsBool (No _)  = False@@ -202,6 +206,12 @@     where go : List Nat -> List Int           go [] = []           go (x :: xs) = n + (cast x * inc) :: go xs++instance Enum Char where+  toNat c   = toNat (ord c)+  fromNat n = chr (fromNat n)+  +  pred c = fromNat (pred (toNat c))  syntax "[" [start] ".." [end] "]"      = enumFromTo start end

@@ -37,7 +37,7 @@ instance Eq Integer where     (==) = boolOp prim__eqBigInt -instance Eq Float where+instance Eq Double where     (==) = boolOp prim__eqFloat  instance Eq Char where@@ -118,7 +118,7 @@                   GT  -instance Ord Float where+instance Ord Double where     compare x y = if (x == y) then EQ else                   if (boolOp prim__sltFloat x y) then LT else                   GT@@ -170,7 +170,7 @@     fromInteger = prim__truncBigInt_Int  -instance Num Float where+instance Num Double where     (+) = prim__addFloat     (*) = prim__mulFloat @@ -215,7 +215,7 @@     (-) = prim__subInt     abs x = if x < (prim__truncBigInt_Int 0) then -x else x -instance Neg Float where+instance Neg Double where     negate x = prim__negFloat x     (-) = prim__subFloat     abs x = if x < (prim__toFloatBigInt 0) then -x else x@@ -306,8 +306,8 @@  -- ------------------------------------------------------------- [ Fractionals ] -||| Fractional division of two Floats.-(/) : Float -> Float -> Float+||| Fractional division of two Doubles.+(/) : Double -> Double -> Double (/) = prim__divFloat  

@@ -9,11 +9,15 @@ import Prelude.List  ||| A sum type-%elim data Either a b =+%elim data Either : (a, b : Type) -> Type where   ||| One possibility of the sum, conventionally used to represent errors-  Left a |+  Left : (l : a) -> Either a b   ||| The other possibility, conventionally used to represent success-  Right b+  Right : (r : b) -> Either a b++-- Usage hints for erasure analysis+%used Left l+%used Right r  -------------------------------------------------------------------------------- -- Syntactic tests

@@ -18,8 +18,12 @@  ||| A file handle abstract-data File = FHandle Ptr+data File : Type where+  FHandle : (p : Ptr) -> File +-- Usage hints for erasure analysis+%used FHandle p+ ||| An error from a file operation -- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure -- the values correspond!@@ -88,7 +92,7 @@  ||| Open a file ||| @ f the filename-||| @ m the mode+||| @ m the mode; either Read, Write, or ReadWrite openFile : (f : String) -> (m : Mode) -> IO (Either FileError File) openFile f m = fopen f (modeStr m) where   modeStr Read  = "r"@@ -139,6 +143,13 @@                           then return (Left FileReadError)                           else return (Right str) +||| Read a line from a file+||| @h a file handle which must be open for reading+fGetLine : (h : File) -> IO (Either FileError String)+fGetLine = fread++%deprecate fread "Use fGetLine instead"+ do_fwrite : Ptr -> String -> IO (Either FileError ()) do_fwrite h s = do res <- prim_fwrite h s                    if (res /= 0)@@ -152,14 +163,31 @@ fwrite : File -> String -> IO (Either FileError ()) fwrite (FHandle h) s = do_fwrite h s +||| Write a line to a file+||| @h a file handle which must be open for writing+||| @str the line to write to the file+fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())+fPutStr (FHandle h) s = do_fwrite h s++fPutStrLn : File -> String -> IO (Either FileError ())+fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")++%deprecate fwrite "Use fPutStr instead"+ do_feof : Ptr -> IO Int do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h  ||| Check if a file handle has reached the end-feof : File -> IO Bool-feof (FHandle h) = do eof <- do_feof h+fEOF : File -> IO Bool+fEOF (FHandle h) = do eof <- do_feof h                       return (not (eof == 0)) +||| Check if a file handle has reached the end+feof : File -> IO Bool+feof = fEOF++%deprecate feof "Use fEOF instead"+ fpoll : File -> IO Bool fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h                        return (p > 0)@@ -177,8 +205,8 @@     partial     readFile' : File -> String -> IO (Either FileError String)     readFile' h contents =-       do x <- feof h-          if not x then do Right l <- fread h+       do x <- fEOF h+          if not x then do Right l <- fGetLine h                                | Left err => return (Left err)                            readFile' h (contents ++ l)                    else return (Right contents)@@ -188,6 +216,6 @@             IO (Either FileError ()) writeFile fn contents = do      Right h <- openFile fn Write | Left err => return (Left err)-     Right () <- fwrite h contents | Left err => return (Left err)+     Right () <- fPutStr h contents | Left err => return (Left err)      closeFile h      return (Right ())

@@ -121,9 +121,9 @@                 (onEOF : a -> String) ->                  IO () processHandle h acc onRead onEOF -   = if !(feof h)+   = if !(fEOF h)         then putStr (onEOF acc)-        else do Right x <- fread h+        else do Right x <- fGetLine h                     | Left err => putStr (onEOF acc)                 let (out, acc') = onRead acc x                 putStr out

@@ -19,15 +19,19 @@ infixr 7 ::,++  ||| Generic lists-%elim data List elem =+%elim data List : (elem : Type) -> Type where   ||| Empty list-  Nil |+  Nil : List elem   ||| A non-empty list, consisting of a head element and the rest of   ||| the list.-  (::) elem (List elem)+  (::) : (x : elem) -> (xs : List elem) -> List elem  -- Name hints for interactive editing %name List xs, ys, zs, ws++-- Usage hints for erasure analysis+%used List.(::) x+%used List.(::) xs  -------------------------------------------------------------------------------- -- Syntactic tests

@@ -13,11 +13,14 @@  ||| An optional value. This can be used to represent the possibility of ||| failure, where a function may return a value, or not.-data Maybe a-    = ||| No value stored-      Nothing-    | ||| A value of type `a` is stored-      Just a+data Maybe : (a : Type) -> Type where+    ||| No value stored+    Nothing : Maybe a+    ||| A value of type `a` is stored+    Just : (x : a) -> Maybe a++-- Used hints for erasure analysis+%used Just x  -------------------------------------------------------------------------------- -- Syntactic tests

@@ -214,6 +214,9 @@ instance Cast Integer Nat where   cast = fromInteger +instance Cast String Nat where+    cast str = cast (the Integer (cast str))+ ||| A wrapper for Nat that specifies the semigroup and monad instances that use (*) record Multiplicative where   constructor GetMultiplicative

@@ -14,10 +14,13 @@  ||| An infinite stream codata Stream : Type -> Type where-  (::) : a -> Stream a -> Stream a+  (::) : (e : a) -> Stream a -> Stream a  -- Hints for interactive editing %name Stream xs,ys,zs,ws++-- Usage hints for erasure analysis+%used Stream.(::) e  instance Functor Stream where     map f (x::xs) = f x :: map f xs

@@ -91,7 +91,7 @@ ||| ||| @ tm the term that has the right type for the hole exact : (tm : Raw) -> Elab ()-exact tm = do apply tm []+exact tm = do fill tm               solve  ||| Introduce as many names as possible, returning them.@@ -178,7 +178,7 @@ total inferType : (tac : Elab ()) -> Elab (TT, TT) inferType tac =-    case fst !(runElab `(Infer) (startInfer *> tac)) of+    case fst !(runElab `(Infer) (do startInfer; tac)) of         `(MkInfer ~ty ~tm) => return (tm, ty)         _ => fail [TextPart "Not infer"]   where

@@ -44,9 +44,7 @@ matchCase : List Raw -> Elab () matchCase []          = search matchCase (tm :: tms) =-    do hs <- induction tm-       y <- unsafeNth 0 hs-       n <- unsafeNth 1 hs+    do (y :: n :: _)  <- induction tm         focus n; compute        contra <- gensym "contra"@@ -183,7 +181,7 @@                     Nothing => return False      partial -- mkRhs-    mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe FunClause)+    mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe (FunClause Raw))     mkCase k fam (cn1, args1, _) (cn2, args2, _) =         perhaps $ elabPatternClause           (do (h2 :: h1 :: _) <- reverse <$>

@@ -134,7 +134,7 @@   show (NormalArgument x) = "NormalArgument " ++ show x  getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->-                (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause+                (TTName, List CtorArg, Raw) -> Nat -> Elab (FunClause Raw) getElimClause info elimn methCount (cn, args, resTy) whichCon =   elabPatternClause     (do -- Establish a hole for each parameter@@ -242,14 +242,11 @@         bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x  getElimClauses : TyConInfo -> (elimn : TTName) ->-                 List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+                 List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw)) getElimClauses info elimn ctors =   let methodCount = length ctors   in traverse (\(i, con) => getElimClause info elimn methodCount con i)               (enumerate ctors)--instance Show FunClause where-  show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"  abstract deriveElim : (tyn, elimn : TTName) -> Elab ()

@@ -101,7 +101,7 @@ |||       It will be run in a context where the pattern variables are |||       already bound, and should leave behind no holes. partial-elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause+elabPatternClause : (lhs, rhs : Elab ()) -> Elab (FunClause Raw) elabPatternClause lhs rhs =   do -- Elaborate the LHS in a context where its type will be solved via unification      (pat, _) <- runElab `(Infer) $

@@ -196,6 +196,88 @@     return cl; } +VAL bigAnd(VM* vm, VAL x, VAL y) {+    idris_requireAlloc(IDRIS_MAXGMP);++    mpz_t* bigint;+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);+    idris_doneAlloc();+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));+    mpz_and(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));+    SETTY(cl, BIGINT);+    cl -> info.ptr = (void*)bigint;+    return cl;+}++VAL bigOr(VM* vm, VAL x, VAL y) {+    idris_requireAlloc(IDRIS_MAXGMP);++    mpz_t* bigint;+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);+    idris_doneAlloc();+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));+    mpz_ior(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));+    SETTY(cl, BIGINT);+    cl -> info.ptr = (void*)bigint;+    return cl;+}++VAL bigShiftLeft(VM* vm, VAL x, VAL y) {+    idris_requireAlloc(IDRIS_MAXGMP);++    mpz_t* bigint;+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);+    idris_doneAlloc();+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));+    mpz_mul_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));+    SETTY(cl, BIGINT);+    cl -> info.ptr = (void*)bigint;+    return cl;+}+++VAL bigLShiftRight(VM* vm, VAL x, VAL y) {+    idris_requireAlloc(IDRIS_MAXGMP);++    mpz_t* bigint;+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);+    idris_doneAlloc();+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));+    mpz_fdiv_q_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));+    SETTY(cl, BIGINT);+    cl -> info.ptr = (void*)bigint;+    return cl;+}++VAL bigAShiftRight(VM* vm, VAL x, VAL y) {+    idris_requireAlloc(IDRIS_MAXGMP);++    mpz_t* bigint;+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);+    idris_doneAlloc();+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));+    mpz_fdiv_q_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));+    SETTY(cl, BIGINT);+    cl -> info.ptr = (void*)bigint;+    return cl;+}++VAL idris_bigAnd(VM* vm, VAL x, VAL y) {+    if (ISINT(x) && ISINT(y)) {+        return INTOP(&, x, y);+    } else {+        return bigAnd(vm, GETBIG(vm, x), GETBIG(vm, y));+    }+}++VAL idris_bigOr(VM* vm, VAL x, VAL y) {+    if (ISINT(x) && ISINT(y)) {+        return INTOP(|, x, y);+    } else {+        return bigOr(vm, GETBIG(vm, x), GETBIG(vm, y));+    }+}+ VAL idris_bigPlus(VM* vm, VAL x, VAL y) {     if (ISINT(x) && ISINT(y)) {         i_int vx = GETINT(x);@@ -250,6 +332,30 @@         }     } else {         return bigMul(vm, GETBIG(vm, x), GETBIG(vm, y));+    }+}++VAL idris_bigShiftLeft(VM* vm, VAL x, VAL y) {+    if (ISINT(x) && ISINT(y)) {+        return INTOP(<<, x, y);+    } else {+        return bigShiftLeft(vm, GETBIG(vm, x), GETBIG(vm, y));+    }+}++VAL idris_bigAShiftRight(VM* vm, VAL x, VAL y) {+    if (ISINT(x) && ISINT(y)) {+        return INTOP(>>, x, y);+    } else {+        return bigAShiftRight(vm, GETBIG(vm, x), GETBIG(vm, y));+    }+}++VAL idris_bigLShiftRight(VM* vm, VAL x, VAL y) {+    if (ISINT(x) && ISINT(y)) {+        return INTOP(>>, x, y);+    } else {+        return bigLShiftRight(vm, GETBIG(vm, x), GETBIG(vm, y));     } } 

@@ -38,6 +38,11 @@ VAL idris_castStrBig(VM* vm, VAL i); VAL idris_castBigStr(VM* vm, VAL i); +VAL idris_bigAnd(VM* vm, VAL x, VAL y);+VAL idris_bigOr(VM* vm, VAL x, VAL y);+VAL idris_bigShiftLeft(VM* vm, VAL x, VAL y);+VAL idris_bigShiftRight(VM* vm, VAL x, VAL y);+ #define GETMPZ(x) *((mpz_t*)((x)->info.ptr))  #endif

@@ -444,6 +444,11 @@ doOp v (LTimes (ATInt ITBig)) [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")" doOp v (LSDiv (ATInt ITBig)) [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")" doOp v (LSRem (ATInt ITBig)) [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LAnd ITBig) [l, r] = v ++ "idris_bigAnd(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LOr ITBig) [l, r] = v ++ "idris_bigOr(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LSHL ITBig) [l, r] = v ++ "idris_bigShiftLeft(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LLSHR ITBig) [l, r] = v ++ "idris_bigLShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LASHR ITBig) [l, r] = v ++ "idris_bigAShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")" doOp v (LEq (ATInt ITBig)) [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")" doOp v (LSLt (ATInt ITBig)) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")" doOp v (LSLe (ATInt ITBig)) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

@@ -604,7 +604,7 @@ jsBASETOP _ n = JSAssign jsSTACKBASE (JSBinOp "+" jsSTACKTOP (JSNum (JSInt n)))  jsNULL :: CompileInfo -> Reg -> JS-jsNULL _ r = JSDelete (translateReg r)+jsNULL _ r = JSClear (translateReg r)  jsERROR :: CompileInfo -> String -> JS jsERROR _ = JSError@@ -1277,4 +1277,3 @@ toFType (FApp c [_,fty])     | c == sUN "JS_FnT" = toFnType fty toFType t = error (show t ++ " not yet defined in toFType")-

@@ -77,6 +77,7 @@         | JSFFI String [JS]         | JSAnnotation JSAnnotation JS         | JSDelete JS+        | JSClear JS         | JSNoop         deriving Eq @@ -133,6 +134,9 @@ compileJS' indent (JSDelete js) =   "delete " `T.append` compileJS' 0 js +compileJS' indent (JSClear js) =+   compileJS' 0 js `T.append` " = undefined"+ compileJS' indent (JSFFI raw args) =   ffi raw (map (T.unpack . compileJS' indent) args) @@ -398,4 +402,3 @@  jsPackSBits32 :: JS -> JS jsPackSBits32 js = JSNew "Int32Array" [JSArray [js]]-

@@ -188,7 +188,7 @@     idris_optimisation :: Ctxt OptInfo,     idris_datatypes :: Ctxt TypeInfo,     idris_namehints :: Ctxt [Name],-    idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported+    idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm]), -- not exported       -- ^ list of lhs/rhs, and a list of missing clauses     idris_flags :: Ctxt [FnOpt],     idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos@@ -717,7 +717,7 @@ -- | A set of instructions for things that need to happen in IState -- after a term elaboration when there's been reflected elaboration. data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type-                       | RClausesInstrs Name [([Name], Term, Term)]+                       | RClausesInstrs Name [([(Name, Term)], Term, Term)]                        | RAddInstance Name Name  -- | For elaborator state

@@ -351,56 +351,6 @@     noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)  -calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality-calcProd i fc topn pats-    = cp topn pats []-   where-     -- every application of n must be in an argument of a coinductive-     -- constructor, in every function reachable from here in the-     -- call graph.-     cp n pats done = do patsprod <- mapM (prodRec n done) pats-                         if (and patsprod)-                            then return Productive-                            else return (Partial NotProductive)--     prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool-     prodRec n done _ | n `elem` done = return True-     prodRec n done (_, _, tm) = prod n done False (delazy' True tm)--     prod :: Name -> [Name] -> Bool -> Term -> Idris Bool-     prod n done ok ap@(App _ _ _)-        | (P nt f _, args) <- unApply ap-            = do recOK <- checkProdRec (n:done) f-                 let ctxt = tt_ctxt i-                 let [ty] = lookupTy f ctxt -- must exist!-                 let co = cotype nt f ty in-                     if (not recOK) then return False else-                       if f == topn-                         then do argsprod <- mapM (prod n done co) args-                                 return (and (ok : argsprod) )-                         else do argsprod <- mapM (prod n done co) args-                                 return (and argsprod)-     prod n done ok (App _ f a) = liftM2 (&&) (prod n done False f)-                                              (prod n done False a)-     prod n done ok (Bind _ (Let t v) sc)-         = liftM2 (&&) (prod n done False v) (prod n done False v)-     prod n done ok (Bind _ b sc) = prod n done ok sc-     prod n done ok t = return True--     checkProdRec :: [Name] -> Name -> Idris Bool-     checkProdRec done f-        = case lookupCtxt f (idris_patdefs i) of-               [(def, _)] -> do ok <- mapM (prodRec f done) def-                                return (and ok)-               _ -> return True -- defined elsewhere, can't call topn--     cotype (DCon _ _ _) n ty-        | (P _ t _, _) <- unApply (getRetTy ty)-            = case lookupCtxt t (idris_datatypes i) of-                   [TI _ True _ _ _] -> True-                   _ -> False-     cotype nt n ty = False- -- | Calculate the totality of a function from its patterns. -- Either follow the size change graph (if inductive) or check for -- productivity (if coinductive)

@@ -98,8 +98,8 @@     block b (DoBind fc n nfc tm : rest)         = PApp fc b [pexp tm, pexp (PLam fc n nfc Placeholder (block b rest))]     block b (DoBindP fc p tm alts : rest)-        = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "bpat") NoFC Placeholder-                                   (PCase fc (PRef fc [] (sMN 0 "bpat"))+        = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "__bpat") NoFC Placeholder+                                   (PCase fc (PRef fc [] (sMN 0 "__bpat"))                                              ((p, block b rest) : alts)))]     block b (DoLet fc n nfc ty tm : rest)         = PLet fc n nfc ty tm (block b rest)@@ -108,7 +108,7 @@     block b (DoExp fc tm : rest)         = PApp fc b             [pexp tm,-             pexp (PLam fc (sMN 0 "bindx") NoFC (mkTy tm) (block b rest))]+             pexp (PLam fc (sMN 0 "__bindx") NoFC (mkTy tm) (block b rest))]         where mkTy (PCase _ _ _) = PRef fc [] unitTy               mkTy (PMetavar _ _) = PRef fc [] unitTy               mkTy _ = Placeholder

@@ -204,8 +204,8 @@                     [(cases, _)] -> return cases                     _ -> Nothing          return $ PCase un (de env imps scrutinee)-                    [ (de (env ++ map (\n -> (n, n)) vars) imps (splitArg lhs),-                       de (env ++ map (\n -> (n, n)) vars) imps rhs)+                    [ (de (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),+                       de (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)                     | (vars, lhs, rhs) <- cases                     ]       where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args)

@@ -133,7 +133,7 @@             -- pdef is the compile-time pattern definition.            -- This will get further inlined to help with totality checking.-           let pdef = map debind pats_raw+           let pdef = 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, and, partially evaluated            let pdef_pe = map debind pats_transformed@@ -182,7 +182,7 @@             -- pdef' is the version that gets compiled for run-time,            -- so we start from the partially evaluated version-           pdef_in' <- applyOpts pdef_pe+           pdef_in' <- applyOpts $ map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) pdef_pe            let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'             logLvl 5 $ "After data structure transformations:\n" ++ show pdef'@@ -289,7 +289,7 @@     debind (Left x)       = let (vs, x') = depat [] x in                                 (vs, x', Impossible) -    depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)+    depat acc (Bind n (PVar t) sc) = depat ((n, t) : acc) (instantiate (P Bound n t) sc)     depat acc x = (acc, x)  

@@ -1775,14 +1775,33 @@      returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased) -    patvars :: [Name] -> Term -> ([Name], Term)-    patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)+    patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)+    patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)     patvars ns tm                   = (ns, tm) -    pullVars :: (Term, Term) -> ([Name], Term, Term)+    pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)     pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs -    defineFunction :: RFunDefn -> ElabD ()+    requireError :: Err -> ElabD a -> ElabD ()+    requireError orErr elab =+      do state <- get+         case runStateT elab state of+           OK (_, state') -> lift (tfail orErr)+           Error e -> return ()++    -- create a fake TT term for the LHS of an impossible case+    fakeTT :: Raw -> Term+    fakeTT (Var n) =+      case lookupNameDef n (tt_ctxt ist) of+        [(n', TyDecl nt _)] -> P nt n' Erased+        _ -> P Ref n Erased+    fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)+    fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)+    fakeTT RType = TType (UVar (-1))+    fakeTT (RUType u) = UType u+    fakeTT (RConstant c) = Constant c++    defineFunction :: RFunDefn Raw -> ElabD ()     defineFunction (RDefineFun n clauses) =       do ctxt <- get_context          ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt@@ -1794,22 +1813,24 @@                                            lift $ converts ctxt [] lty rty                                            return $ Right (lhs', rhs')                                       RMkImpossibleClause lhs ->-                                        do lhs' <- fmap fst . lift $ check ctxt [] lhs-                                           return $ Left lhs')+                                        do requireError (Msg "Not an impossible case") . lift $+                                             check ctxt [] lhs+                                           return $ Left (fakeTT lhs))          let clauses'' = map (\case Right c -> pullVars c-                                    Left lhs -> let (ns, lhs') = patvars [] lhs'+                                    Left lhs -> let (ns, lhs') = patvars [] lhs                                                 in (ns, lhs', Impossible))                             clauses'+         let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''          ctxt'<- lift $                   addCasedef n (const [])                              info False (STerm Erased)                              True False -- TODO what are these?                              (map snd $ getArgTys ty) [] -- TODO inaccessible types                              clauses'-                             clauses''-                             clauses''-                             clauses''-                             clauses''+                             clauses'''+                             clauses'''+                             clauses'''+                             clauses'''                              ty                              ctxt          set_context ctxt'@@ -1874,6 +1895,11 @@            fmap fst . checkClosed $              rawList (Var (tacN "Datatype"))                      (map reflectDatatype (buildDatatypes ist n'))+      | n == tacN "Prim__LookupFunDefn", [name] <- args+      = do n' <- reifyTTName name+           fmap fst . checkClosed $+             rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))+               (map reflectFunDefn (buildFunDefns ist n'))       | n == tacN "Prim__LookupArgs", [name] <- args       = do n' <- reifyTTName name            let listTy = Var (sNS (sUN "List") ["List", "Prelude"])

@@ -414,7 +414,7 @@             V i -> snd (bs !! i) cd `union` unconditionalDeps args              -- we interpret applied lambdas as lets in order to reuse code here-            Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)+            Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet app)              -- and we interpret applied lets as lambdas             Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')@@ -491,11 +491,8 @@      -- convert applications of lambdas to lets     -- Note that this transformation preserves de bruijn numbering-    lamToLet :: [Term] -> Term -> Term-    lamToLet    xs  (App _ f x)         = lamToLet (x:xs) f-    lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)-    lamToLet (x:xs)  t                  = App Complete (lamToLet xs t) x-    lamToLet    []   t                  = t+    lamToLet :: Term -> Term+    lamToLet (App _ (Bind n (Lam ty) tm) val) = Bind n (Let ty val) tm      -- split "\x_i -> T(x_i)" into [x_i] and T     unfoldLams :: Term -> ([Name], Term)

@@ -40,7 +40,7 @@ import Codec.Archive.Zip  ibcVersion :: Word16-ibcVersion = 127+ibcVersion = 128  data IBCFile = IBCFile { ver :: Word16,                          sourcefile :: FilePath,@@ -80,7 +80,7 @@                          ibc_errorhandlers :: ![Name],                          ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler                          ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))],-                         ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],+                         ibc_patdefs :: ![(Name, ([([(Name, Term)], Term, Term)], [PTerm]))],                          ibc_postulates :: ![Name],                          ibc_externs :: ![(Name, Int)],                          ibc_parsedSpan :: !(Maybe FC),@@ -505,7 +505,7 @@ pHdrs :: [(Codegen, String)] -> Idris () pHdrs hs = mapM_ (uncurry addHdr) hs -pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()+pPatdefs :: [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))] -> Idris () pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->             i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds 

@@ -1450,11 +1450,11 @@      return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++               map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++               map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))-  where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation+  where ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation         ppDef amb ist (n, (clauses, missing)) =           prettyName True amb [] n <+> colon <+>           align (pprintDelabTy ist n) <$>-          ppClauses ist clauses <> ppMissing missing+          ppClauses ist (map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses) <> ppMissing missing         ppClauses ist [] = text "No clauses."         ppClauses ist cs = vsep (map pp cs)           where pp (vars, lhs, rhs) =

@@ -7,6 +7,8 @@  #if __GLASGOW_HASKELL__ < 710 import Control.Applicative ((<$>), (<*>), pure)+import Prelude hiding (mapM)+import Data.Traversable (mapM) #endif import Control.Monad (liftM, liftM2, liftM4) import Control.Monad.State.Strict (lift)@@ -19,7 +21,7 @@ import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact) import Idris.Core.TT -import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),+import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes, idris_patdefs),                             PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),                             initEState, pairCon, pairTy) import Idris.Delaborate (delab)@@ -55,11 +57,11 @@ rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder -data RFunClause = RMkFunClause Raw Raw-                | RMkImpossibleClause Raw-                deriving Show+data RFunClause a = RMkFunClause a a+                  | RMkImpossibleClause a+                  deriving Show -data RFunDefn = RDefineFun Name [RFunClause] deriving Show+data RFunDefn a = RDefineFun Name [RFunClause a] deriving Show  -- | Prefix a name with the "Language.Reflection" namespace reflm :: String -> Name@@ -357,8 +359,8 @@ reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))  reifyArithTy :: Term -> ElabD ArithTy-reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt"   = fmap ATInt (reifyIntTy intTy)-reifyArithTy (P _ n _)             | n == reflm "ATFloat" = return ATFloat+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt"    = fmap ATInt (reifyIntTy intTy)+reifyArithTy (P _ n _)               | n == reflm "ATDouble" = return ATFloat reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)  reifyNativeTy :: Term -> ElabD NativeTy@@ -768,7 +770,7 @@ reflectConstant c@(B64 _) = reflCall "B64" [RConstant c] reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]] reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]-reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATDouble")] reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]] reflectConstant StrType = Var (reflm "StrType") reflectConstant (AType (ATInt (ITFixed IT8)))  = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]@@ -1023,21 +1025,21 @@      return $ RDeclare tyN' args' ret' reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration." -reifyFunDefn :: Term -> ElabD RFunDefn-reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)-  | n == tacN "DefineFun" =+reifyFunDefn :: Term -> ElabD (RFunDefn Raw)+reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)+  | n == tacN "DefineFun" && t == reflm "Raw" =   do fnN' <- reifyTTName fnN      clauses' <- case unList clauses of                    Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"                    Just cs -> mapM reifyC cs      return $ RDefineFun fnN' clauses'-  where reifyC :: Term -> ElabD RFunClause-        reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)-          | n == tacN "MkFunClause" = liftM2 RMkFunClause+  where reifyC :: Term -> ElabD (RFunClause Raw)+        reifyC (App _ (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs) rhs)+          | n == tacN "MkFunClause" && t == reflm "Raw" = liftM2 RMkFunClause                                              (reifyRaw lhs)                                              (reifyRaw rhs)-        reifyC (App _ (P (DCon _ _ _) n _) lhs)-          | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs+        reifyC (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs)+          | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs         reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause." reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration." @@ -1074,6 +1076,22 @@     ua args (RApp f a) = ua (a:args) f     ua args t         = (t, args) +-- | Build the reflected function definition(s) that correspond(s) to+-- a provided unqualifed name+buildFunDefns :: IState -> Name -> [RFunDefn Term]+buildFunDefns ist n =+  [ mkFunDefn name clauses+  | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist+  ]++  where mkFunDefn name clauses = RDefineFun name (map mkFunClause clauses)++        mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs+        mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs+        mkFunClause (((n, ty) : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where+          bind Impossible = Impossible+          bind tm = Bind n (PVar ty) tm+ -- | Build the reflected datatype definition(s) that correspond(s) to -- a provided unqualified name buildDatatypes :: IState -> Name -> [RDatatype]@@ -1163,3 +1181,13 @@           RApp (Var $ tacN "TyConParameter") (reflectArg a)         reflectConArg (RIndex a) =           RApp (Var $ tacN "TyConIndex") (reflectArg a)++reflectFunClause :: RFunClause Term -> Raw+reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]+reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause") $ [ Var $ reflm "TT", reflect lhs ]++reflectFunDefn :: RFunDefn Term -> Raw+reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [ Var $ reflm "TT"+                                                                              , reflectName name+                                                                              , rawList (RApp (Var $ tacN "FunClause") (Var $ reflm "TT")) (map reflectFunClause clauses)+                                                                              ]

@@ -16,9 +16,8 @@                         , removeFile                         , removeDirectoryRecursive                         , createDirectoryIfMissing-                        , doesDirectoryExist                         )-import System.FilePath ((</>), normalise, isAbsolute, dropFileName)+import System.FilePath ((</>), normalise) import System.IO import System.Info import System.IO.Error@@ -66,7 +65,7 @@ withTempdir :: String -> (FilePath -> IO a) -> IO a withTempdir subdir callback   = do dir <- getTemporaryDirectory-       let tmpDir = (normalise dir) </> subdir+       let tmpDir = normalise dir </> subdir        removeLater <- catchIO (createDirectoryIfMissing True tmpDir >> return True)                               (\ ioError -> if isAlreadyExistsError ioError then return False                                             else throw ioError@@ -76,10 +75,15 @@        return result  rmFile :: FilePath -> IO ()-rmFile f = do putStrLn $ "Removing " ++ f-              catchIO (removeFile f)-                      (\ioerr -> putStrLn $ "WARNING: Cannot remove file "-                                 ++ f ++ ", Error msg:" ++ show ioerr)+rmFile f = do+  result <- try (removeFile f)+  case result of+    Right _ -> putStrLn $ "Removed: " ++ f+    Left err -> handleExists err+     where handleExists e+            | isDoesNotExistError e = return ()+            | otherwise = putStrLn $ "WARNING: Cannot remove file "+                          ++ f ++ ", Error msg:" ++ show e  setupBundledCC :: IO() #ifdef FREESTANDING

@@ -1,6 +1,13 @@-flags: {}+resolver: lts-3.16 packages: - '.'+flags:+  # idris:+  #   FFI: true+  #   GMP: True+  #   curses: True extra-deps: +- annotated-wl-pprint-0.7.0 - cheapskate-0.1.0.4-resolver: nightly-2015-07-24+# - hscurses-1.4.2.0+# - libffi-0.1

@@ -23,12 +23,12 @@ close (OpenH h) = iou (closeFile h)  readLine : FILE Reading -> Reader String-readLine (OpenH h) = ior (do Right str <- fread h+readLine (OpenH h) = ior (do Right str <- fGetLine h                                    | return ""                              return str)  eof : FILE Reading -> Reader Bool-eof (OpenH h) = ior (feof h)+eof (OpenH h) = ior (fEOF h)  syntax rclose [h]    = Update close h syntax rreadLine [h] = Use readLine h

@@ -2,8 +2,8 @@  %dynamic "dummy", "libm", "msvcrt" -x : Float-x = unsafePerformIO (foreign FFI_C "sin" (Float -> IO Float) 1.6)+x : Double+x = unsafePerformIO (foreign FFI_C "sin" (Double -> IO Double) 1.6)  main : IO () main = putStrLn (show x)

@@ -1,14 +1,14 @@ Prelude.List.(++) : List a -> List a -> List a Prelude.Strings.(++) : String -> String -> String-Prelude.Classes./ : (__pi_arg : Float) →-                    (__pi_arg1 : Float) → Float+Prelude.Classes./ : (__pi_arg : Double) →+                    (__pi_arg1 : Double) → Double Usage is :doc <functionname> Usage is :wc <functionname> Usage is :printdef <functionname> prim__divFloat Prelude.Classes./ - : Float -> Float -> Float+ : Double -> Double -> Double (input):1:1: error: expected: ":",     dependent type signature,     end of input

@@ -1,3 +1,3 @@ #!/usr/bin/env bash-idris --quiet interactive012.idr < input+idris --nocolour --consolewidth 70 --quiet interactive012.idr < input rm -f *.ibc

@@ -10,15 +10,15 @@ dumpFile : String -> IO () dumpFile fn = do { Right h <- openFile fn Read                    mwhile (do { -- putStrLn "TEST"-                                x <- feof h+                                x <- fEOF h                                 return (not x) })-                          (do { Right l <- fread h+                          (do { Right l <- fGetLine h                                 putStr l })                    closeFile h }  main : IO () main = do { Right h <- openFile "testfile" Write-            fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"+            fPutStr h "Hello!\nWorld!\n...\n3\n4\nLast line\n"             closeFile h             putStrLn "Reading testfile"             Right f <- readFile "testfile"

@@ -29,7 +29,7 @@  mkToClause : TTName -> (size, i : Nat) ->              (constr : (TTName, List CtorArg, Raw)) ->-             Elab FunClause+             Elab (FunClause Raw) mkToClause fn size i (n, [], Var ty) =   MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i mkToClause fn size i (n, _, ty) =@@ -38,14 +38,14 @@  mkFromClause : TTName -> (size, i : Nat) ->                (constr : (TTName, List CtorArg, Raw)) ->-               Elab FunClause+               Elab (FunClause Raw) mkFromClause fn size i (n, [], Var ty) =   return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n) mkFromClause fn size i (n, _, ty) =   fail [TextPart "unsupported constructor", NamePart n]  -mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw) mkOk1Clause fn size i (n, [], Var ty) =   return $ MkFunClause (RApp (Var fn) (Var n))                        [| (Var (UN "Refl")) (Var ty) (Var n) |]@@ -53,7 +53,7 @@   fail [TextPart "unsupported constructor", NamePart n]  -mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw) mkOk2Clause fn size i (n, [], Var ty) =   return $ MkFunClause (RApp (Var fn) !(mkFin size i))                        [| (Var "Refl") `(Fin ~(quote size))@@ -62,9 +62,9 @@   fail [TextPart "unsupported constructor", NamePart n]  -mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw)) mkToClauses fn size xs = mkToClauses' Z xs-  where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+  where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))         mkToClauses' k []        = return []         mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs                                       clause <- mkToClause fn size k x@@ -76,7 +76,7 @@ ||| This is to satisfy the totality checker, because `impossible` ||| clauses are still mkAbsurdFinClause : (fn : TTName) -> (goal : Raw -> Raw) -> (size : Nat) ->-                    Elab FunClause+                    Elab (FunClause Raw) mkAbsurdFinClause fn goal size =   do pv <- gensym "badfin"      lhsArg <- lhsBody pv size@@ -92,26 +92,26 @@   mkFromClauses : TTName -> TTName -> Nat ->-                List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+                List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw)) mkFromClauses fn ty size xs = mkFromClauses' Z xs-  where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+  where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))         mkFromClauses' k []        =              return [!(mkAbsurdFinClause fn (const (Var ty)) size)]         mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs                                         clause <- mkFromClause fn size k x                                         return $ clause :: rest -mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw)) mkOk1Clauses fn size xs = mkOk1Clauses' Z xs-  where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+  where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))         mkOk1Clauses' k []        = return []         mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs                                        clause <- mkOk1Clause fn size k x                                        return $ clause :: rest -mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)+mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List (FunClause Raw)) mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs-  where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+  where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))         mkOk2Clauses' k []        = return [!(mkAbsurdFinClause fn resTy size)]         mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs                                        clause <- mkOk2Clause fn size k x

@@ -1,6 +1,8 @@ ||| Test some deriving features module Deriving +-- NB: test disabled due to excess memory consumption+ import Pruviloj import Pruviloj.Derive.DecEq 

@@ -1,5 +1,6 @@ #!/usr/bin/env bash idris $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr idris $@ -p pruviloj --nocolour --check --consolewidth 70 AgdaStyleReflection.idr-idris $@ -p pruviloj --nocolour --check --consolewidth 70 Deriving.idr+# Disabled due to excess memory consumption+# idris $@ -p pruviloj --nocolour --check --consolewidth 70 Deriving.idr rm -f *.ibc

@@ -0,0 +1,3 @@+meta004.idr:48:1-9:+While running an elaboration script, the following error occurred:+Not an impossible case

@@ -0,0 +1,48 @@+import Data.Fin+import Language.Reflection.Utils+import Pruviloj.Core++rename : TTName -> TTName -> Raw -> Raw+rename old new (RBind name b body) = RBind name (map (rename old new) b) (rename old new body)+rename old new (RApp f arg) = RApp (rename old new f) (rename old new arg)+rename old new (Var n) = if n == old then Var new else Var n+rename old new tm = tm++roundtrip : TTName -> TTName -> Elab ()+roundtrip old new = do+  DefineFun _ clauses <- lookupFunDefnExact old+  clauses' <- for clauses (\(MkFunClause lhs rhs) => do+    lhs' <- rename old new <$> forget lhs+    rhs' <- rename old new <$> forget rhs+    pure $ MkFunClause lhs' rhs')+  defineFunction (DefineFun new clauses')++plus' : Nat -> Nat -> Nat+%runElab (roundtrip `{plus} `{plus'})++total+p : (a : Nat) -> (b : Nat) -> plus a b = plus' a b+p Z right = Refl+p (S left) right = Refl+++-- Test handling of impossible clauses in function definitions+foo : Fin Z -> Nat+bar : Nat -> Fin Z++doit : Elab ()+doit = defineFunction $+          DefineFun `{foo} [MkImpossibleClause+                             (RBind `{{n}}+                               (PVar (Var `{Nat}))+                               (RApp (Var `{foo})+                                 (RApp (Var `{FZ}) (Var `{{n}}))))]++domore : Elab ()+domore = defineFunction $+            DefineFun `{foo} [MkImpossibleClause $+                                RBind `{{k}} (PVar `(Nat)) $+                                  RApp (Var `{bar}) (Var `{{k}})]++%runElab doit+%runElab domore

@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris $@ -p pruviloj --nocolour --check --consolewidth 70 meta004.idr+rm -f *.ibc

@@ -24,9 +24,6 @@                                                         Pure (fact k, ()))                  Loop mathsServer -instance Cast String Nat where-    cast orig = cast (the Integer (cast orig))- -- Start up a couple of servers, send them requests testProg1 : Program () (const Void) testProg1 = do -- with Process do 

@@ -1,5 +1,5 @@-App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1)))))) ---------------App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27)))) -------------- App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))

@@ -0,0 +1,1 @@+tst2["as"]

@@ -0,0 +1,23 @@+module Main++-- https://github.com/idris-lang/Idris-dev/issues/2844+main_2844 : IO ()+main_2844 =+  let+    f =+      the+        ((String,String) -> String -> (String, Maybe String ))+        (\(_,s),y => (s, Just s))+  in+    case snd $ f ("tst","tst2") "cenas" of+      Just z => putStr z++-- https://github.com/idris-lang/Idris-dev/issues/2493+main_2493 : IO ()+main_2493 = printLn $ doThing [1,2,3] [("as",1),("asasasas",4)]+  where+    doThing : List Nat -> List (v,Nat) -> List v+    doThing is g = foldr (\(v,i),res => if elem i is then v::res else res) List.Nil g++main : IO ()+main = main_2844 *> main_2493

@@ -0,0 +1,5 @@+#!/usr/bin/env bash+rm -f *.ibc reg067+idris $@ reg067.idr -o reg067 --warnreach+./reg067+rm -f *.ibc reg067

@@ -8,18 +8,46 @@ my $exitstatus = 0; my @idrOpts    = (); ++# Determines how idris was built locally, returning a PATH modifier.+#+# Order of checking is:+#+#  1. Cabal Sandboxing+#  2. Stack+#  3. Pure cabal.+# sub sandbox_path {     my ($test_dir,) = @_;     my $sandbox = "$test_dir/../../.cabal-sandbox/bin"; +    my $stack_bin_path = `stack path --dist-dir`;+    $stack_bin_path =~ s/\n//g;+    my $stack_work_dir = "$test_dir/../../$stack_bin_path/build/idris";+     if ( -d $sandbox ) {+         my $sandbox_abs = abs_path($sandbox);+        print "Using Cabal Sandbox\n";+        printf("Sandbox located at: %s\n", $sandbox_abs);         return "PATH=\"$sandbox_abs:$PATH\"";++    } elsif ( -d $stack_work_dir ) {++        my $stack_work_abs = abs_path($stack_work_dir);+        print "Using Stack Work\n";+        printf("Stack work located at: %s\n", $stack_work_abs);+        return "PATH=\"$stack_work_abs:$PATH\"";+     } else {+        print "Using Default Cabal.\n";         return "";     } } +# Run an individual test, and compare expected output with given+# output and report results.+# sub runtest {     my ($test, $update) = @_; @@ -73,8 +101,13 @@     chdir ".."; } +# Main test running program to sort test input, and execute individual+# tests.+#+ my ( @without, @args, @tests, @opts ); +# Deal with the Args. if ($#ARGV>=0) {     my $test = shift @ARGV;     if ($test eq "all") {@@ -119,6 +152,8 @@     print "Give a test name, or 'all' to run all.\n";     exit; }++# Run the tests.  my $update  = 0; my $diff    = 0;