49de647 · Idris-dev · git.iko.soy

CHANGELOG+7

@@ -9,6 +9,13 @@ New in 0.9.12:

99* Lots of performance patches for generated JavaScript

1010* New commands :eval (:e) and :type (:t) in the prover, which either normalise

1111 or show the type of expressions

12+* Allow type providers to return postulates in addition to terms

13+* New syntax for inline documentation. Documentation starts with |||, and

14+ arguments are documented by preceding their name with @. Example:

15+||| Add two natural numbers

16+||| @ n the first number (examined by the function)

17+||| @ m the second number (not examined)

18+plus (n, m : Nat) -> Nat

1219

1320New in 0.9.11:

1421--------------

idris.cabal+3

@@ -299,6 +299,9 @@ Extra-source-files:

299299 test/ffi004/theType

300300 test/ffi004/theOtherType

301301 test/ffi004/expected

302+ test/ffi005/*.idr

303+ test/ffi005/run

304+ test/ffi005/expected

302305

303306 test/interactive001/run

304307 test/interactive001/input

jsrts/Runtime-common.js−3

@@ -1,6 +1,3 @@

1−var __IDRRT__ZERO = __IDRRT__bigInt("0");

2−var __IDRRT__ONE = __IDRRT__bigInt("1");

3−

41/** @constructor */

52var __IDRRT__Type = function(type) {

63 this.type = type;

jsrts/jsbn/jsbn.js+3

@@ -1233,3 +1233,6 @@ return function(val) {

12331233 return new BigInteger(val);

12341234}

12351235})();

1236+

1237+var __IDRRT__ZERO = __IDRRT__bigInt("0");

1238+var __IDRRT__ONE = __IDRRT__bigInt("1");

libs/base/Data/Fun.idr+3

@@ -13,3 +13,6 @@ chain : {ts : Vect n Type} -> Fun [r] r' -> Fun ts r -> Fun ts r'

1313chain {ts = []} g r = g r

1414chain {ts = (_::_)} g f = \ x => chain g (f x)

1515

16+target : {ts : Vect n Type} -> Fun ts r -> Type

17+target {r} _ = r

18+

libs/base/Data/SortedMap.idr+6−4

@@ -183,11 +183,13 @@ treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =

183183 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')

184184 Right t3' => Left (merge3 t1 k1 t2 k2 t3')

185185

186−-- FIXME: this is very inefficient

187186treeToList : Ord k => Tree n k v -> List (k, v)

188−treeToList (Leaf k v) = [(k, v)]

189−treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2

190−treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3

187+treeToList = treeToList' (:: [])

188+ where

189+ treeToList' : Ord k => ((k, v) -> List (k, v)) -> Tree n k v -> List (k, v)

190+ treeToList' cont (Leaf k v) = cont (k, v)

191+ treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1

192+ treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1

191193

192194data SortedMap : Type -> Type -> Type where

193195 Empty : SortedMap k v

libs/base/Data/ZZ.idr+2−2

@@ -7,8 +7,8 @@ import Data.Sign

77%access public

88

99

10−-- | An integer is either a positive nat or the negated successor of a nat.

11−-- Zero is chosen to be positive.

10+||| An integer is either a positive nat or the negated successor of a nat.

11+||| Zero is arbitrarily chosen to be positive.

1212data ZZ = Pos Nat | NegS Nat

1313

1414instance Signed ZZ where

libs/base/Debug/Trace.idr+4−1

@@ -1,6 +1,9 @@

11module Debug.Trace

22

3−trace : String -> a -> a

3+||| Print a message for debugging purposes as a side effect

4+||| @ msg what to print

5+||| @ result the final result

6+trace : (msg : String) -> (result : a) -> a

47trace x val = unsafePerformIO (do putStrLn x; return val)

58

69

libs/base/Decidable/Order.idr+1−1

@@ -21,7 +21,7 @@ class (Preorder t po) => Poset t (po : t -> t -> Type) where

2121 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

2222

2323class (Poset t to) => Ordered t (to : t -> t -> Type) where

24− total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

24+ total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

2525

2626minimum : (Ordered t to) => t -> t -> t

2727minimum x y with (order x y)

libs/base/Language/Reflection.idr+6−6

@@ -22,7 +22,7 @@ data TTUExp = UVar Int

2222 -- ^ explicit universe variable

2323%name TTUExp uexp

2424

25−-- | Primitive constants

25+||| Primitive constants

2626data Const = I Int | BI Integer | Fl Float | Ch Char | Str String

2828 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64

@@ -66,7 +66,7 @@ reflectConstant: (ReflConst a) => a -> Const

6666reflectConstant = toConst

6767

6868

69−-- | Types of named references

69+||| Types of named references

7070data NameType = Bound

7171 -- ^ reference which is just bound, e.g. by intro

7272 | Ref

@@ -77,8 +77,8 @@ data NameType = Bound

7777 -- ^ type constructor with tag and number

7878%name NameType nt, nt'

7979

80−-- | Types annotations for bound variables in different

81−-- binding contexts

80+||| Types annotations for bound variables in different

81+||| binding contexts

8282data Binder a = Lam a

8383 | Pi a

8484 | Let a a

@@ -124,7 +124,7 @@ instance Traversable Binder where

124124 traverse f (PVTy x) = [| PVTy (f x) |]

125125

126126

127−-- | Reflection of the well typed core language

127+||| Reflection of the well typed core language

128128data TT = P NameType TTName TT

129129 -- ^ named binders

130130 | V Int

@@ -146,7 +146,7 @@ data TT = P NameType TTName TT

146146

147147%name TT tm, tm'

148148

149−-- | Raw terms without types

149+||| Raw terms without types

150150data Raw = Var TTName

151151 | RBind TTName (Binder Raw) Raw

152152 | RApp Raw Raw

libs/base/Language/Reflection/Errors.idr+1−1

@@ -42,7 +42,7 @@ data Err = Msg String

4242

4343%name Err err, e

4444

45−-- | Error reports are a list of report parts

45+||| Error reports are a list of report parts

4646data ErrorReportPart = TextPart String

4747 | NamePart TTName

4848 | TermPart TT

libs/base/Providers.idr+19−2

@@ -1,19 +1,36 @@

11module Providers

22

3+||| Type providers must build one of these in an IO computation.

34public

4−data Provider a = Provide a | Error String

5+data Provider : (a : Type) -> Type where

6+ ||| Return a term to be spliced in

7+ ||| @ x the term to be spliced (i.e. the proof)

8+ Provide : (x : a) -> Provider a

9+

10+ ||| Report an error to the user and stop compilation

11+ ||| @ msg the error message

12+ Error : (msg : String) -> Provider a

13+

14+ ||| Postulate the goal type

15+ Postulate : Provider a

516

617-- instances

718instance Functor Provider where

819 map f (Provide a) = Provide (f a)

920 map f (Error err) = Error err

21+ map f Postulate = Postulate

1022

1123instance Applicative Provider where

1224 (Provide f) <$> (Provide x) = Provide (f x)

1325 (Provide f) <$> (Error err) = Error err

14− (Error err) <$> _ = Error err

26+ (Provide f) <$> Postulate = Postulate

27+ (Error err) <$> _ = Error err

28+ Postulate <$> (Error err) = Error err

29+ Postulate <$> _ = Postulate

1530 pure = Provide

1631

32+-- is this correct for Postulate?

1733instance Monad Provider where

1834 (Provide x) >>= f = f x

1935 (Error err) >>= _ = Error err

36+ Postulate >>= f = Postulate

libs/base/System.idr+12−6

@@ -5,6 +5,7 @@ import Prelude

55%default partial

66%access public

77

8+||| Get the command-line arguments that the program was called with.

89getArgs : IO (List String)

910getArgs = do n <- numArgs

1011 ga' [] 0 n

@@ -20,8 +21,8 @@ getArgs = do n <- numArgs

2021 do arg <- getArg i

2122 ga' (arg :: acc) (i+1) n

2223

23−-- Retrieves an value from the environment, if the given key is present,

24−-- otherwise it returns Nothing.

24+||| Retrieves an value from the environment, if the given key is present,

25+||| otherwise it returns Nothing.

2526getEnv : String -> IO (Maybe String)

2627getEnv key = do

2728 str_ptr <- getEnv'

@@ -33,15 +34,15 @@ getEnv key = do

3334 getEnv' : IO String

3435 getEnv' = mkForeign (FFun "getenv" [FString] FString) key

3536

36−-- Sets an environment variable with a given value.

37−-- Returns true if the operation was successful.

37+||| Sets an environment variable with a given value.

38+||| Returns true if the operation was successful.

3839setEnv : String -> String -> IO Bool

3940setEnv key value = do

4041 ok <- mkForeign (FFun "setenv" [FString, FString, FInt] FInt) key value 1

4142 return (ok == 0)

4243

43−-- Unsets an environment variable.

44−-- Returns true if the variable was able to be unset.

44+||| Unsets an environment variable.

45+||| Returns true if the variable was able to be unset.

4546unsetEnv : String -> IO Bool

4647unsetEnv key = do

4748 ok <- mkForeign (FFun "unsetenv" [FString] FInt) key

@@ -68,9 +69,14 @@ getEnvironment = getAllPairs 0 []

6869 then return $ reverse $ map splitEq acc

6970 else getAllPairs (n + 1) (envPair :: acc)

7071

72+||| Quit with a particular exit code

7173exit : Int -> IO ()

7274exit code = mkForeign (FFun "exit" [FInt] FUnit) code

7375

76+||| Get the Unix time

77+time : IO Int

78+time = mkForeign (FFun "idris_time" [] FInt)

79+

7480usleep : Int -> IO ()

7581usleep i = mkForeign (FFun "usleep" [FInt] FUnit) i

7682

libs/neweffects/Effect/Random.idr+8

@@ -20,6 +20,14 @@ rndInt : Integer -> Integer -> { [RND] } Eff m Integer

2020rndInt lower upper = do v <- getRandom

2121 return (v `prim__sremBigInt` (upper - lower) + lower)

2222

23+rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

24+rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)

25+ return (toFin v)

26+ where toFin : Integer -> Fin (S k)

27+ toFin x = case integerToFin x (S k) of

28+ Just v => v

29+ Nothing => toFin (assert_smaller x (x - cast (S k)))

30+

2331srand : Integer -> { [RND] } Eff m ()

2432srand n = setSeed n

2533

libs/neweffects/Effect/System.idrnew file+38

@@ -0,0 +1,38 @@

1+module Effect.System

2+

3+-- Various system interaction features (this is not necessarily the right way

4+-- to split them up, I just need some of them now :))

5+

6+import Effects

7+import System

8+import Control.IOExcept

9+

10+data System : Effect where

11+ Args : { () } System (List String)

12+ Time : { () } System Int

13+ GetEnv : String -> { () } System (Maybe String)

14+

15+instance Handler System IO where

16+ handle () Args k = do x <- getArgs; k x ()

17+ handle () Time k = do x <- time; k x ()

18+ handle () (GetEnv s) k = do x <- getEnv s; k x ()

19+

20+instance Handler System (IOExcept a) where

21+ handle () Args k = do x <- ioe_lift getArgs; k x ()

22+ handle () Time k = do x <- ioe_lift time; k x ()

23+ handle () (GetEnv s) k = do x <- ioe_lift $ getEnv s; k x ()

24+

25+--- The Effect and associated functions

26+

27+SYSTEM : EFFECT

28+SYSTEM = MkEff () System

29+

30+getArgs : Handler System e => { [SYSTEM] } Eff e (List String)

31+getArgs = Args

32+

33+time : Handler System e => { [SYSTEM] } Eff e Int

34+time = Time

35+

36+getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)

37+getEnv s = GetEnv s

38+

libs/neweffects/neweffects.ipkg+1−1

@@ -5,5 +5,5 @@ modules = Effects, Effect.Default,

55

66 Effect.Exception, Effect.File, Effect.State,

77 Effect.Random, Effect.StdIO, Effect.Select,

8− Effect.Memory

8+ Effect.Memory, Effect.System

99

libs/prelude/Builtins.idr+22−8

@@ -3,27 +3,35 @@

33%access public

44%default total

55

6+||| Dependent pairs, in their internal representation

7+||| @ a the type of the witness

8+||| @ P the type of the proof

69data Exists : (a : Type) -> (P : a -> Type) -> Type where

710 Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P

811

12+||| The first projection from a dependent pair

913getWitness : {P : a -> Type} -> Exists a P -> a

1014getWitness (a ** v) = a

1115

16+||| The second projection from a dependent pair

1217getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)

1318getProof (a ** v) = v

1419

1520FalseElim : _|_ -> a

1621

17−-- For 'symbol syntax. 'foo becomes Symbol_ "foo"

22+||| For 'symbol syntax. 'foo becomes Symbol_ "foo"

1823data Symbol_ : String -> Type where

1924

2025-- ------------------------------------------------------ [ For rewrite tactic ]

26+||| Perform substitution in a term. This is used by the `rewrite` tactic and term.

2127replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

2228replace refl prf = prf

2329

30+||| Symmetry of propositional equality

2431sym : {l:a} -> {r:a} -> l = r -> r = l

2532sym refl = refl

2633

34+||| Transitivity of propositional equality

2735trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c

2836trans refl refl = refl

2937

@@ -48,21 +56,27 @@ malloc size x = x -- compiled specially

4856trace_malloc : a -> a

4957trace_malloc x = x -- compiled specially

5058

51−-- Assert to the totality checker than y is always structureally smaller than

52−-- x (which is typically a pattern argument)

53−assert_smaller : a -> a -> a

59+||| Assert to the totality checker than y is always structurally smaller than

60+||| x (which is typically a pattern argument)

61+||| @ x the larger value (typically a pattern argument)

62+||| @ y the smaller value (typically an argument to a recursive call)

63+assert_smaller : (x, y : a) -> a

5464assert_smaller x y = y

5565

56−-- Assert to the totality checker than the given expression will always

57−-- terminate.

66+||| Assert to the totality checker than the given expression will always

67+||| terminate.

5868assert_total : a -> a

5969assert_total x = x

6070

71+||| Subvert the type checker. This function is abstract, so it will not reduce in

72+||| the type checker. Use it with care - it can result in segfaults or worse!

6173abstract %assert_total -- need to pretend

62−believe_me : a -> b -- compiled specially as id, use with care!

74+believe_me : a -> b

6375believe_me x = prim__believe_me _ _ x

6476

65−public %assert_total -- reduces at compile time, use with extreme care!

77+||| Subvert the type checker. This function *will* reduce in the type checker.

78+||| Use it with extreme care - it can result in segfaults or worse!

79+public %assert_total

6680really_believe_me : a -> b

6781really_believe_me x = prim__believe_me _ _ x

6882

libs/prelude/IO.idr+8

@@ -32,6 +32,7 @@ data FTy = FIntT IntTy

3232 | FFloat

3333 | FString

3434 | FPtr

35+ | FManagedPtr

3536 | FAny Type

3637 | FUnit

3738

@@ -85,6 +86,7 @@ interpFTy (FAny t) = t

8586interpFTy FFloat = Float

8687interpFTy FString = String

8788interpFTy FPtr = Ptr

89+interpFTy FManagedPtr = ManagedPtr

8890interpFTy (FIntT IT8x16) = Bits8x16

8991interpFTy (FIntT IT16x8) = Bits16x8

9092interpFTy (FIntT IT32x4) = Bits32x4

@@ -106,6 +108,9 @@ mkForeignPrim : Foreign x -> x

106108mkLazyForeignPrim : Foreign x -> x

107109-- mkForeign and mkLazyForeign compiled as primitives

108110

111+registerPtr : Ptr -> Int -> ManagedPtr

112+registerPtr = prim__registerPtr

113+

109114abstract

110115io_bind : IO a -> (a -> IO b) -> IO b

111116io_bind (MkIO fn) k

@@ -149,3 +154,6 @@ unsafePerformIO (MkIO f) = unsafePerformPrimIO

149154 (prim_io_bind (f TheWorld) (\ b => prim_io_return b))

150155

151156

157+forceGC : IO ()

158+forceGC = mkForeign (FFun "idris_forceGC" [FPtr] FUnit) prim__vm

159+

libs/prelude/Prelude/Applicative.idr+3

@@ -19,12 +19,15 @@ infixl 2 $>

1919($>) : Applicative f => f a -> f b -> f b

2020a $> b = map (const id) a <$> b

2121

22+||| Lift a function to an applicative

2223liftA : Applicative f => (a -> b) -> f a -> f b

2324liftA f a = pure f <$> a

2425

26+||| Lift a two-argument function to an applicative

2527liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c

2628liftA2 f a b = (map f a) <$> b

2729

30+||| Lift a three-argument function to an applicative

2831liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

2932liftA3 f a b c = (map f a) <$> b <$> c

3033

libs/prelude/Prelude/Basics.idr+23−12

@@ -3,44 +3,55 @@ module Prelude.Basics

33Not : Type -> Type

44Not a = a -> _|_

55

6−-- | Identity function.

6+||| Identity function.

77id : a -> a

88id x = x

99

10−-- | Manually assign a type to an expression.

11−the : (a : Type) -> a -> a

10+||| Manually assign a type to an expression.

11+||| @ a the type to assign

12+||| @ x the element to get the type

13+the : (a : Type) -> (x : a) -> a

1214the _ = id

1315

14−-- | Constant function.

16+||| Constant function. Ignores its second argument.

1517const : a -> b -> a

1618const x = \v => x

1719

18−-- | Return the first element of a pair.

20+||| Return the first element of a pair.

1921fst : (s, t) -> s

2022fst (x, y) = x

2123

22−-- | Return the second element of a pair.

24+||| Return the second element of a pair.

2325snd : (a, b) -> b

2426snd (x, y) = y

2527

2628infixl 9 .

2729

28−-- | Function composition

30+||| Function composition

2931(.) : (b -> c) -> (a -> b) -> a -> c

3032(.) f g x = f (g x)

3133

32−-- | Takes in the first two arguments in reverse order.

33−flip : (a -> b -> c) -> b -> a -> c

34+||| Takes in the first two arguments in reverse order.

35+||| @ f the function to flip

36+flip : (f : a -> b -> c) -> b -> a -> c

3437flip f x y = f y x

3538

36−-- | Function application.

39+||| Function application.

3740apply : (a -> b) -> a -> b

3841apply f a = f a

3942

43+||| Equality is a congruence.

4044cong : {f : t -> u} -> (a = b) -> f a = f b

4145cong refl = refl

4246

47+||| Decidability. A decidable property either holds or is a contradiction.

4348data Dec : Type -> Type where

44− Yes : {A : Type} -> A -> Dec A

45− No : {A : Type} -> (A -> _|_) -> Dec A

49+

50+ ||| The case where the property holds

51+ ||| @ prf the proof

52+ Yes : {A : Type} -> (prf : A) -> Dec A

53+

54+ ||| The case where the property holding would be a contradiction

55+ ||| @ contra a demonstration that A would be a contradiction

56+ No : {A : Type} -> (contra : A -> _|_) -> Dec A

4657

libs/prelude/Prelude/Bits.idr+13−21

@@ -8,26 +8,18 @@ import Prelude.Bool

88%default total

99

1010

11−private

12−toHexDigit : Fin 16 -> Char

13−toHexDigit n = index n hexVect where

14− hexVect : Vect 16 Char

15− hexVect = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',

16− 'A', 'B', 'C', 'D', 'E', 'F']

17−

1811b8ToString : Bits8 -> String

19−b8ToString c = pack (with List [c1, c2]) where

20− %assert_total -- We will only supply numbers that can fit in 4 bits

21− toFin16 : Bits8 -> Fin 16

22− toFin16 n = if n == 0

23− then fZ

24− else believe_me (fS (toFin16 (n-1)))

25− c1 = toHexDigit upper where

26− upper : Fin 16

27− upper = toFin16 (prim__lshrB8 c 4)

28− c2 = toHexDigit lower where

29− lower : Fin 16

30− lower = toFin16 (prim__andB8 c 0xf)

12+b8ToString c = pack (with List [c1, c2])

13+ where getDigit : Bits8 -> Char

14+ getDigit b = let n = prim__zextB8_Int b in

15+ if n >= 0 && n <= 9

16+ then '0' `prim__addChar` cast n

17+ else if n >= 10 && n <= 15

18+ then 'A' `prim__addChar` cast (n - 10)

19+ else '?' -- this is for totality - it should not happen

20+ c1 = getDigit (prim__andB8 (prim__lshrB8 c 4) 15)

21+ c2 = getDigit (prim__andB8 c 15)

22+

3123

3224b16ToString : Bits16 -> String

3325b16ToString c = c1 ++ c2 where

@@ -42,7 +34,7 @@ b32ToString : Bits32 -> String

4234b32ToString c = c1 ++ c2 where

4335 c1 = b16ToString upper where

4436 upper : Bits16

45− upper = prim__truncB32_B16 (prim__lshrB32 c 16)

37+ upper = prim__truncB32_B16 (prim__andB32 (prim__lshrB32 c 16) 0x0000ffff)

4638 c2 = b16ToString lower where

4739 lower : Bits16

4840 lower = prim__truncB32_B16 c

@@ -51,7 +43,7 @@ b64ToString : Bits64 -> String

5143b64ToString c = c1 ++ c2 where

5244 c1 = b32ToString upper where

5345 upper : Bits32

54− upper = prim__truncB64_B32 (prim__lshrB64 c 32)

46+ upper = prim__truncB64_B32 (prim__andB64 (prim__lshrB64 c 32) 0x00000000ffffffff)

5547 c2 = b32ToString lower where

5648 lower : Bits32

5749 lower = prim__truncB64_B32 c

libs/prelude/Prelude/Bool.idr+10−7

@@ -1,14 +1,17 @@

11module Prelude.Bool

22

3−-- | Boolean Data Type

3+||| Boolean Data Type

44data Bool = False | True

55

6−-- | Boolean elimination

7−boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a

6+||| The underlying implementation of the if ... then ... else ... syntax

7+||| @ b the condition on the if

8+||| @ t the value if b is true

9+||| @ e the falue if b is false

10+boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

811boolElim True t e = t

912boolElim False t e = e

1013

11−-- | Defines a predicate on Bool which guarantees that the value is true.

14+||| Defines a predicate on Bool which guarantees that the value is true.

1215data so : Bool -> Type where oh : so True

1316

1417-- Syntaxtic sugar for boolean elimination.

@@ -17,17 +20,17 @@ syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

1720-- Boolean Operator Precedence

1821infixl 4 &&, ||

1922

20−-- | Boolean OR

23+||| Boolean OR

2124(||) : Bool -> Bool -> Bool

2225(||) False x = x

2326(||) True _ = True

2427

25−-- | Boolean AND

28+||| Boolean AND

2629(&&) : Bool -> Bool -> Bool

2730(&&) True x = x

2831(&&) False _ = False

2932

30−-- | Boolean NOT

33+||| Boolean NOT

3134not : Bool -> Bool

3235not True = False

3336not False = True

libs/prelude/Prelude/Chars.idr+16−16

@@ -3,67 +3,67 @@ module Prelude.Char

33

44import Builtins

55

6−-- | Return the ASCII representation of the character.

6+||| Return the ASCII representation of the character.

77chr : Int -> Char

88chr x = prim__intToChar x

99

10−-- | Convert the number to its ASCII equivalent.

10+||| Convert the number to its ASCII equivalent.

1111ord : Char -> Int

1212ord x = prim__charToInt x

1313

14−-- | Returns true if the character is in the range [A-Z].

14+||| Returns true if the character is in the range [A-Z].

1515isUpper : Char -> Bool

1616isUpper x = x >= 'A' && x <= 'Z'

1717

18−-- | Returns true if the character is in the range [a-z]

18+||| Returns true if the character is in the range [a-z]

1919isLower : Char -> Bool

2020isLower x = x >= 'a' && x <= 'z'

2121

22−-- | Returns true if the character is in the ranges [A-Z][a-z].

22+||| Returns true if the character is in the ranges [A-Z][a-z].

2323isAlpha : Char -> Bool

2424isAlpha x = isUpper x || isLower x

2525

26−-- | Returns true if the character is in the range [0-9]

26+||| Returns true if the character is in the range [0-9]

2727isDigit : Char -> Bool

2828isDigit x = (x >= '0' && x <= '9')

2929

30−-- | Returns true if the character is in the ranges [A-Z][a-z][0-9]

30+||| Returns true if the character is in the ranges [A-Z][a-z][0-9]

3131isAlphaNum : Char -> Bool

3232isAlphaNum x = isDigit x || isAlpha x

3333

34−-- | Returns true if the character is a whitespace character.

34+||| Returns true if the character is a whitespace character.

3535isSpace : Char -> Bool

3636isSpace x = x == ' ' || x == '\t' || x == '\r' ||

3737 x == '\n' || x == '\f' || x == '\v' ||

3838 x == '\xa0'

3939

40−-- | Returns true if the character represents a new line.

40+||| Returns true if the character represents a new line.

4141isNL : Char -> Bool

4242isNL x = x == '\r' || x == '\n'

4343

44−-- | Convert a letter to the corresponding upper-case letter, if any.

45−-- Non-letters are ignored.

44+||| Convert a letter to the corresponding upper-case letter, if any.

45+||| Non-letters are ignored.

4646toUpper : Char -> Char

4747toUpper x = if (isLower x)

4848 then (prim__intToChar (prim__charToInt x - 32))

4949 else x

5050

51−-- | Convert a letter to the corresponding lower-case letter, if any.

52−-- Non-letters are ignored.

51+||| Convert a letter to the corresponding lower-case letter, if any.

52+||| Non-letters are ignored.

5353toLower : Char -> Char

5454toLower x = if (isUpper x)

5555 then (prim__intToChar (prim__charToInt x + 32))

5656 else x

5757

58−-- | Returns true if the character is a hexadecimal digit i.e. in the range [0-9][a-f][A-F]

58+||| Returns true if the character is a hexadecimal digit i.e. in the range [0-9][a-f][A-F]

5959isHexDigit : Char -> Bool

6060isHexDigit x = elem (toUpper x) hexChars where

6161 hexChars : List Char

6262 hexChars = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',

6363 'A', 'B', 'C', 'D', 'E', 'F']

6464

65−-- | Returns true if the character is an octal digit.

65+||| Returns true if the character is an octal digit.

6666isOctDigit : Char -> Bool

6767isOctDigit x = (x >= '0' && x <= '7')

6868

69−-- --------------------------------------------------------------------- [ EOF ]

69+

libs/prelude/Prelude/Classes.idr+8−8

@@ -20,7 +20,7 @@ boolOp : (a -> a -> Int) -> a -> a -> Bool

2020boolOp op x y = intToBool (op x y)

2121

2222-- ---------------------------------------------------------- [ Equality Class ]

23−-- | The Eq class defines inequality and equality.

23+||| The Eq class defines inequality and equality.

2424class Eq a where

2525 (==) : a -> a -> Bool

2626 (/=) : a -> a -> Bool

@@ -65,7 +65,7 @@ instance Eq Ordering where

6565 GT == GT = True

6666 _ == _ = False

6767

68−-- | The Ord class defines comparison operations on ordered data types.

68+||| The Ord class defines comparison operations on ordered data types.

6969class Eq a => Ord a where

7070 compare : a -> a -> Ordering

7171

@@ -131,14 +131,14 @@ instance (Ord a, Ord b) => Ord (a, b) where

131131 else compare xr yr

132132

133133-- --------------------------------------------------------- [ Numerical Class ]

134−-- | The Num class defines basic numerical arithmetic.

134+||| The Num class defines basic numerical arithmetic.

135135class Num a where

136136 (+) : a -> a -> a

137137 (-) : a -> a -> a

138138 (*) : a -> a -> a

139− -- | Absolute value

139+ ||| Absolute value

140140 abs : a -> a

141− -- | Conversion from Integer.

141+ ||| Conversion from Integer.

142142 fromInteger : Integer -> a

143143

144144instance Num Integer where

@@ -245,11 +245,11 @@ instance Ord Bits64 where

245245-- ------------------------------------------------------------- [ Bounded ]

246246

247247class MinBound b where

248− -- | The lower bound for the type

248+ ||| The lower bound for the type

249249 minBound : b

250250

251251class MaxBound b where

252− -- | The upper bound for the type

252+ ||| The upper bound for the type

253253 maxBound : b

254254

255255instance MinBound Bits16 where

@@ -273,7 +273,7 @@ instance MaxBound Bits64 where

273273

274274-- ------------------------------------------------------------- [ Fractionals ]

275275

276−-- | Fractional division of two Floats.

276+||| Fractional division of two Floats.

277277(/) : Float -> Float -> Float

278278(/) = prim__divFloat

279279

libs/prelude/Prelude/Either.idr+13−5

@@ -1,13 +1,16 @@

1−module Prelude.Either

1+ module Prelude.Either

22

33import Builtins

44

55import Prelude.Maybe

66import Prelude.List

77

8−data Either a b

9− = Left a

10− | Right b

8+||| A sum type

9+data Either a b =

10+ ||| One possibility of the sum, conventionally used to represent errors

11+ Left a |

12+ ||| The other possibility, conventionally used to represent success

13+ Right b

1114

1215--------------------------------------------------------------------------------

1316-- Syntactic tests

@@ -25,11 +28,16 @@ isRight (Right r) = True

2528-- Misc.

2629--------------------------------------------------------------------------------

2730

31+||| Perform a case analysis on a Boolean, providing clients with a `so` proof

2832choose : (b : Bool) -> Either (so b) (so (not b))

2933choose True = Left oh

3034choose False = Right oh

3135

32−either : (a -> c) -> (b -> c) -> Either a b -> c

36+||| Simply-typed eliminator for Either

37+||| @ f the action to take on Left

38+||| @ g the action to take on Right

39+||| @ e the sum to analyze

40+either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c

3341either l r (Left x) = l x

3442either l r (Right x) = r x

3543

libs/prelude/Prelude/Fin.idr+11−1

@@ -5,7 +5,9 @@ import Prelude.Either

55

66%default total

77

8−data Fin : Nat -> Type where

8+||| Numbers strictly less than some bound. The name comes from "finite sets"

9+||| @ n the upper bound

10+data Fin : (n : Nat) -> Type where

911 fZ : Fin (S k)

1012 fS : Fin k -> Fin (S k)

1113

@@ -44,14 +46,18 @@ finToInteger (fS k) = 1 + finToInteger k

4446instance Cast (Fin n) Integer where

4547 cast x = finToInteger x

4648

49+||| Weaken the bound on a Fin by 1

4750weaken : Fin n -> Fin (S n)

4851weaken fZ = fZ

4952weaken (fS k) = fS (weaken k)

5053

54+||| Weaken the bound on a Fin by some amount

5155weakenN : (n : Nat) -> Fin m -> Fin (m + n)

5256weakenN n fZ = fZ

5357weakenN n (fS f) = fS (weakenN n f)

5458

59+||| Attempt to tighten the bound on a Fin.

60+||| Return `Left` if the bound could not be tightened, or `Right` if it could.

5561strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

5662strengthen {n = S k} fZ = Right fZ

5763strengthen {n = S k} (fS i) with (strengthen i)

@@ -59,10 +65,14 @@ strengthen {n = S k} (fS i) with (strengthen i)

5965 strengthen (fS k) | Right x = Right (fS x)

6066strengthen f = Left f

6167

68+||| Add some natural number to a Fin, extending the bound accordingly

69+||| @ n the previous bound

70+||| @ m the number to increase the Fin by

6271shift : (m : Nat) -> Fin n -> Fin (m + n)

6372shift Z f = f

6473shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)

6574

75+||| The largest element of some Fin type

6676last : Fin (S n)

6777last {n=Z} = fZ

6878last {n=S _} = fS last

libs/prelude/Prelude/Functor.idr+6−1

@@ -1,4 +1,9 @@

11module Prelude.Functor

22

3+||| Functors

4+||| @ f the action of the functor on objects

35class Functor (f : Type -> Type) where

4− map : (a -> b) -> f a -> f b

6+ ||| The action of the functor on morphisms

7+ ||| @ f the functor

8+ ||| @ m the morphism

9+ map : (m : a -> b) -> f a -> f b

libs/prelude/Prelude/List.idr+17

@@ -269,6 +269,23 @@ intersperse sep (x::xs) = x :: intersperse' sep xs

269269intercalate : List a -> List (List a) -> List a

270270intercalate sep l = concat $ intersperse sep l

271271

272+||| Transposes rows and columns of a list of lists.

273+|||

274+||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]

275+|||

276+||| This also works for non square scenarios, thus

277+||| involution does not always hold:

278+|||

279+||| > transpose [[], [1, 2]] = [[1], [2]]

280+||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]

281+|||

282+||| TODO: Solution which satisfies the totality checker?

283+%assert_total

284+transpose : List (List a) -> List (List a)

285+transpose [] = []

286+transpose ([] :: xss) = transpose xss

287+transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))

288+

272289--------------------------------------------------------------------------------

273290-- Membership tests

274291--------------------------------------------------------------------------------

libs/prelude/Prelude/Nat.idr+38−5

@@ -10,9 +10,12 @@ import Prelude.Classes

1010%access public

1111%default total

1212

13−%elim data Nat

14− = Z

15− | S Nat

13+||| Unary natural numbers

14+%elim data Nat =

15+ ||| Zero

16+ Z |

17+ ||| Successor

18+ S Nat

1619

1720-- name hints for interactive editing

1821%name Nat k,j,i,n,m

@@ -33,14 +36,19 @@ isSucc (S n) = True

3336-- Basic arithmetic functions

3437--------------------------------------------------------------------------------

3538

36−total plus : Nat -> Nat -> Nat

39+||| Add two natural numbers.

40+||| @ n the number to case-split on

41+||| @ m the other number

42+total plus : (n, m : Nat) -> Nat

3743plus Z right = right

3844plus (S left) right = S (plus left right)

3945

46+||| Multiply natural numbers

4047total mult : Nat -> Nat -> Nat

4148mult Z right = Z

4249mult (S left) right = plus right $ mult left right

4350

51+||| Convert an Integer to a Nat, mapping negative numbers to 0

4452fromIntegerNat : Integer -> Nat

4553fromIntegerNat 0 = Z

4654fromIntegerNat n =

@@ -49,15 +57,18 @@ fromIntegerNat n =

4957 else

5058 Z

5159

60+||| Convert a Nat to an Integer

5261toIntegerNat : Nat -> Integer

5362toIntegerNat Z = 0

5463toIntegerNat (S k) = 1 + toIntegerNat k

5564

65+||| Subtract natural numbers. If the second number is larger than the first, return 0.

5666total minus : Nat -> Nat -> Nat

5767minus Z right = Z

5868minus left Z = left

5969minus (S left) (S right) = minus left right

6070

71+||| Exponentiation of natural numbers

6172total power : Nat -> Nat -> Nat

6273power base Z = S Z

6374power base (S exp) = mult base $ power base exp

@@ -74,33 +85,46 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)

7485-- Comparisons

7586--------------------------------------------------------------------------------

7687

77−data LTE : Nat -> Nat -> Type where

88+||| Proofs that `n` is less than or equal to `m`

89+||| @ n the smaller number

90+||| @ m the larger number

91+data LTE : (n, m : Nat) -> Type where

92+ ||| Zero is the smallest Nat

7893 lteZero : LTE Z right

94+ ||| If n <= m, then n + 1 <= m + 1

7995 lteSucc : LTE left right -> LTE (S left) (S right)

8096

97+||| Greater than or equal to

8198total GTE : Nat -> Nat -> Type

8299GTE left right = LTE right left

83100

101+||| Strict less than

84102total LT : Nat -> Nat -> Type

85103LT left right = LTE (S left) right

86104

105+||| Strict greater than

87106total GT : Nat -> Nat -> Type

88107GT left right = LT right left

89108

109+||| Boolean test than one Nat is less than or equal to another

90110total lte : Nat -> Nat -> Bool

91111lte Z right = True

92112lte left Z = False

93113lte (S left) (S right) = lte left right

94114

115+||| Boolean test than one Nat is greater than or equal to another

95116total gte : Nat -> Nat -> Bool

96117gte left right = lte right left

97118

119+||| Boolean test than one Nat is strictly less than another

98120total lt : Nat -> Nat -> Bool

99121lt left right = lte (S left) right

100122

123+||| Boolean test than one Nat is strictly greater than another

101124total gt : Nat -> Nat -> Bool

102125gt left right = lt right left

103126

127+||| Find the least of two natural numbers

104128total minimum : Nat -> Nat -> Nat

105129minimum left right =

106130 if lte left right then

@@ -108,6 +132,7 @@ minimum left right =

108132 else

109133 right

110134

135+||| Find the greatest of two natural numbers

111136total maximum : Nat -> Nat -> Nat

112137maximum left right =

113138 if lte left right then

@@ -148,9 +173,11 @@ instance MinBound Nat where

148173instance Cast Integer Nat where

149174 cast = fromInteger

150175

176+||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

151177record Multiplicative : Type where

152178 getMultiplicative : Nat -> Multiplicative

153179

180+||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

154181record Additive : Type where

155182 getAdditive : Nat -> Additive

156183

@@ -210,6 +237,7 @@ instance Cast Nat Int where

210237-- Auxilliary notions

211238--------------------------------------------------------------------------------

212239

240+||| The predecessor of a natural number. `pred Z` is `Z`.

213241total pred : Nat -> Nat

214242pred Z = Z

215243pred (S n) = n

@@ -218,11 +246,13 @@ pred (S n) = n

218246-- Fibonacci and factorial

219247--------------------------------------------------------------------------------

220248

249+||| Fibonacci numbers

221250total fib : Nat -> Nat

222251fib Z = Z

223252fib (S Z) = S Z

224253fib (S (S n)) = fib (S n) + fib n

225254

255+||| Factorial function

226256total fact : Nat -> Nat

227257fact Z = S Z

228258fact (S n) = (S n) * fact n

@@ -283,10 +313,13 @@ lcm x y = divNat (x * y) (gcd x y)

283313--------------------------------------------------------------------------------

284314

285315-- Succ

316+

317+||| S preserves equality

286318total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->

287319 S left = S right

288320eqSucc left _ refl = refl

289321

322+||| S is injective

290323total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->

291324 left = right

292325succInjective left _ refl = refl

libs/prelude/Prelude/Stream.idr+19−4

@@ -6,46 +6,61 @@ import Prelude.Vect

66%access public

77%default total

88

9+||| An infinite stream

910codata Stream : Type -> Type where

1011 (::) : a -> Stream a -> Stream a

1112

1213instance Functor Stream where

1314 map f (x::xs) = f x :: map f xs

1415

16+||| The first element of an infinite stream

1517head : Stream a -> a

1618head (x::xs) = x

1719

20+||| All but the first element

1821tail : Stream a -> Stream a

1922tail (x::xs) = xs

2023

21−take : (n : Nat) -> Stream a -> Vect n a

24+||| Take precisely n elements from the stream

25+||| @ n how many elements to take

26+||| @ xs the stream

27+take : (n : Nat) -> (xs : Stream a) -> Vect n a

2228take Z _ = []

2329take (S n) (x :: xs) = x :: (take n xs)

2430

2531%assert_total

2632drop : Nat -> Stream a -> Stream a

27−drop Z xs = xs

33+drop Z xs = xs

2834drop (S k) (x::xs) = drop k xs

2935

36+||| An infinite stream of repetitions of the same thing

3037repeat : a -> Stream a

3138repeat x = x :: repeat x

3239

33−iterate : (a -> a) -> a -> Stream a

40+||| Generate an infinite stream by repeatedly applying a function

41+||| @ f the function to iterate

42+||| @ x the initial value that will be the head of the stream

43+iterate : (f : a -> a) -> (x : a) -> Stream a

3444iterate f x = x :: iterate f (f x)

3545

46+||| Get the nth element of a stream

3647index : Nat -> Stream a -> a

37−index Z (x::xs) = x

48+index Z (x::xs) = x

3849index (S k) (x::xs) = index k xs

3950

51+||| Combine two streams element-wise using a function

4052zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c

4153zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

4254

55+||| Create a stream of pairs from two streams

4356zip : Stream a -> Stream b -> Stream (a, b)

4457zip = zipWith (\x,y => (x,y))

4558

59+||| Create a pair of streams from a stream of pairs

4660unzip : Stream (a, b) -> (Stream a, Stream b)

4761unzip xs = (map fst xs, map snd xs)

4862

63+||| Return the diagonal elements of a stream of streams

4964diag : Stream (Stream a) -> Stream a

5065diag ((x::xs)::xss) = x :: diag (map tail xss)

5166

libs/prelude/Prelude/Strings.idr+6−6

@@ -7,30 +7,30 @@ import Prelude.Cast

77import Prelude.Either

88import Prelude.Foldable

99

10−-- | Appends two strings together.

10+||| Appends two strings together.

1111(++) : String -> String -> String

1212(++) = prim__concat

1313

14−-- | Returns the first character in the specified string.

14+||| Returns the first character in the specified string.

1515partial

1616strHead : String -> Char

1717strHead = prim__strHead

1818

19−-- | Returns the characters specified after the head of the string.

19+||| Returns the characters specified after the head of the string.

2020partial

2121strTail : String -> String

2222strTail = prim__strTail

2323

24−-- | Adds a character to the from of the specified string.

24+||| Adds a character to the from of the specified string.

2525strCons : Char -> String -> String

2626strCons = prim__strCons

2727

28−-- | Returns the nth character (starting from 0) of the specified string.

28+||| Returns the nth character (starting from 0) of the specified string.

2929partial

3030strIndex : String -> Int -> Char

3131strIndex = prim__strIndex

3232

33−-- | Reverses the elements within a String.

33+||| Reverses the elements within a String.

3434reverse : String -> String

3535reverse = prim__strRev

3636

libs/prelude/Prelude/Uninhabited.idr+9−3

@@ -1,6 +1,9 @@

11module Prelude.Uninhabited

22

3+||| A canonical proof that some type is empty

34class Uninhabited t where

5+ ||| If I have a t, I've had a contradiction

6+ ||| @ t the uninhabited type

47 total uninhabited : t -> _|_

58

69instance Uninhabited (Fin Z) where

@@ -10,6 +13,9 @@ instance Uninhabited (Fin Z) where

1013instance Uninhabited (Z = S n) where

1114 uninhabited refl impossible

1215

13−-- | Use an absurd assumption to discharge a proof obligation

14−absurd : Uninhabited t => t -> a

15−absurd t = FalseElim (uninhabited t)

16+||| Use an absurd assumption to discharge a proof obligation

17+||| @ t some empty type

18+||| @ a the goal type

19+||| @ h the contradictory hypothesis

20+absurd : Uninhabited t => (h : t) -> a

21+absurd h = FalseElim (uninhabited h)

rts/Makefile+12−4

@@ -1,12 +1,20 @@

11include ../config.mk

22

3−OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o \

4− idris_bitstring.o idris_net.o idris_opts.o idris_stats.o mini-gmp.o

5−HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h \

6− idris_bitstring.h idris_net.h idris_opts.h idris_stats.h mini-gmp.h

3+OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \

4+ idris_opts.o idris_stats.o mini-gmp.o

5+HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \

6+ idris_opts.h idris_stats.h mini-gmp.h

77CFLAGS:=-fPIC $(CFLAGS)

88CFLAGS += $(GMP_INCLUDE_DIR) $(GMP)

99

10+ifeq ($(OS), windows)

11+ OBJS += windows/idris_stdfgn.o windows/idris_net.o

12+ HDRS += windows/idris_stdfgn.h windows/idris_net.h

13+else

14+ OBJS += idris_stdfgn.o idris_net.o

15+ HDRS += idris_stdfgn.h idris_net.h

16+endif

17+

1018LIBTARGET = libidris_rts.a

1119

1220build: $(LIBTARGET) $(DYLIBTARGET)

rts/idris_gc.c+3

@@ -36,6 +36,9 @@ VAL copy(VM* vm, VAL x) {

3636 case PTR:

3737 cl = MKPTRc(vm, x->info.ptr);

3838 break;

39+ case MANAGEDPTR:

40+ cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size);

41+ break;

3942 case BITS8:

4043 cl = idris_b8CopyForGC(vm, x);

4144 break;

rts/idris_rts.c+25

@@ -178,6 +178,17 @@ VAL MKPTR(VM* vm, void* ptr) {

178178 return cl;

179179}

180180

181+VAL MKMPTR(VM* vm, void* ptr, int size) {

182+ Closure* cl = allocate(vm, sizeof(Closure) +

183+ sizeof(ManagedPtr) + size, 0);

184+ SETTY(cl, MANAGEDPTR);

185+ cl->info.mptr = (ManagedPtr*)((char*)cl + sizeof(Closure));

186+ cl->info.mptr->data = (char*)cl + sizeof(Closure) + sizeof(ManagedPtr);

187+ memcpy(cl->info.mptr->data, ptr, size);

188+ cl->info.mptr->size = size;

189+ return cl;

190+}

191+

181192VAL MKFLOATc(VM* vm, double val) {

182193 Closure* cl = allocate(vm, sizeof(Closure), 1);

183194 SETTY(cl, FLOAT);

@@ -202,6 +213,17 @@ VAL MKPTRc(VM* vm, void* ptr) {

202213 return cl;

203214}

204215

216+VAL MKMPTRc(VM* vm, void* ptr, int size) {

217+ Closure* cl = allocate(vm, sizeof(Closure) +

218+ sizeof(ManagedPtr) + size, 1);

219+ SETTY(cl, MANAGEDPTR);

220+ cl->info.mptr = (ManagedPtr*)((char*)cl + sizeof(Closure));

221+ cl->info.mptr->data = (char*)cl + sizeof(Closure) + sizeof(ManagedPtr);

222+ memcpy(cl->info.mptr->data, ptr, size);

223+ cl->info.mptr->size = size;

224+ return cl;

225+}

226+

205227VAL MKB8(VM* vm, uint8_t bits8) {

206228 Closure* cl = allocate(vm, sizeof(Closure), 1);

207229 SETTY(cl, BITS8);

@@ -795,6 +817,9 @@ VAL copyTo(VM* vm, VAL x) {

795817 case PTR:

796818 cl = MKPTRc(vm, x->info.ptr);

797819 break;

820+ case MANAGEDPTR:

821+ cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size);

822+ break;

798823 case BITS8:

799824 cl = idris_b8CopyForGC(vm, x);

800825 break;

rts/idris_rts.h+10−1

@@ -17,7 +17,7 @@

1717typedef enum {

1818 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,

1919 BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,

20− BUFFER

20+ MANAGEDPTR, BUFFER

2121} ClosureType;

2222

2323typedef struct Closure *VAL;

@@ -40,6 +40,11 @@ typedef struct {

4040 unsigned char store[];

4141} Buffer;

4242

43+// A foreign pointer, managed by the idris GC

44+typedef struct {

45+ size_t size;

46+ void* data;

47+} ManagedPtr;

4348

4449typedef struct Closure {

4550// Use top 16 bits of ty for saying which heap value is in

@@ -57,6 +62,7 @@ typedef struct Closure {

5762 uint32_t bits32;

5863 uint64_t bits64;

5964 Buffer* buf;

65+ ManagedPtr* mptr;

6066 } info;

6167} Closure;

6268

@@ -112,6 +118,7 @@ typedef void(*func)(VM*, VAL*);

112118

113119#define GETSTR(x) (ISSTR(x) ? (((VAL)(x))->info.str) : GETSTROFF(x))

114120#define GETPTR(x) (((VAL)(x))->info.ptr)

121+#define GETMPTR(x) (((VAL)(x))->info.mptr->data)

115122#define GETFLOAT(x) (((VAL)(x))->info.f)

116123

117124#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag_arity >> 8 : (-1)) )

@@ -163,6 +170,7 @@ typedef intptr_t i_int;

163170VAL MKFLOAT(VM* vm, double val);

164171VAL MKSTR(VM* vm, const char* str);

165172VAL MKPTR(VM* vm, void* ptr);

173+VAL MKMPTR(VM* vm, void* ptr, int size);

166174VAL MKB8(VM* vm, uint8_t b);

167175VAL MKB16(VM* vm, uint16_t b);

168176VAL MKB32(VM* vm, uint32_t b);

@@ -173,6 +181,7 @@ VAL MKFLOATc(VM* vm, double val);

173181VAL MKSTROFFc(VM* vm, StrOffset* off);

174182VAL MKSTRc(VM* vm, char* str);

175183VAL MKPTRc(VM* vm, void* ptr);

184+VAL MKMPTRc(VM* vm, void* ptr, int size);

176185VAL MKBUFFERc(VM* vm, Buffer* buf);

177186

178187char* GETSTROFF(VAL stroff);

rts/idris_stdfgn.c+11

@@ -1,8 +1,10 @@

11#include "idris_stdfgn.h"

22#include "idris_rts.h"

3+#include "idris_gc.h"

34#include <sys/select.h>

45#include <fcntl.h>

56#include <stdio.h>

7+#include <time.h>

68

79extern char** environ;

810

@@ -73,3 +75,12 @@ void* idris_stdin() {

7375char* getEnvPair(int i) {

7476 return *(environ + i);

7577}

78+

79+int idris_time() {

80+ time_t t = time(NULL);

81+ return (int)t;

82+}

83+

84+void idris_forceGC(void* vm) {

85+ idris_gc((VM*)vm);

86+}

rts/idris_stdfgn.h+4

@@ -21,4 +21,8 @@ void* idris_stdin();

2121

2222char* getEnvPair(int i);

2323

24+int idris_time();

25+

26+void idris_forceGC();

27+

2428#endif

rts/windows/idris_net.cnew file+185

@@ -0,0 +1,185 @@

1+// C-Side of the Idris network library

2+// (C) Simon Fowler, 2014

3+// MIT Licensed. Have fun!

4+#include "idris_net.h"

5+

6+#include <errno.h>

7+#include <stdbool.h>

8+#include <stdlib.h>

9+#include <stdio.h>

10+#include <string.h>

11+#include <Winsock2.h>

12+#include <Ws2tcpip.h>

13+

14+static int socket_inited = 0;

15+static WSADATA wsa_data;

16+

17+void* idrnet_malloc(int size) {

18+ return malloc(size);

19+}

20+

21+void idrnet_free(void* ptr) {

22+ free(ptr);

23+}

24+

25+static int check_init()

26+{

27+ if (!socket_inited) {

28+ int result = WSAStartup(MAKEWORD(2, 2), &wsa_data);

29+ if (result == NO_ERROR) {

30+ socket_inited = 1;

31+ }

32+ }

33+ return socket_inited;

34+}

35+

36+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {

37+ struct addrinfo hints;

38+ struct addrinfo* address_res;

39+ // Convert port into string

40+ char str_port[8];

41+ sprintf(str_port, "%d", port);

42+

43+ if (!check_init()) {

44+ return -1;

45+ }

46+ // Set up hints structure

47+ memset(&hints, 0, sizeof(hints)); // zero out hints

48+ hints.ai_family = family;

49+ hints.ai_socktype = socket_type;

50+

51+ // If the length of the hostname is 0 (i.e, it was set to Nothing in Idris)

52+ // then we want to instruct the C library to fill in the IP automatically

53+ if (strlen(host) == 0) {

54+ hints.ai_flags = AI_PASSIVE; // fill in IP automatically

55+ }

56+

57+ int addr_res = getaddrinfo(host, str_port, &hints, &address_res);

58+ if (addr_res == -1) {

59+ return -1;

60+ }

61+

62+ int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);

63+ if (bind_res == -1) {

64+ return -1;

65+ }

66+

67+ return 0;

68+}

69+

70+int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port) {

71+ char str_port[8];

72+ sprintf(str_port, "%d", port);

73+ struct addrinfo hints;

74+ struct addrinfo* remote_host;

75+

76+ if (!check_init()) {

77+ return -1;

78+ }

79+ // Set up hints structure for getaddrinfo

80+ memset(&hints, 0, sizeof(hints));

81+ hints.ai_family = family;

82+ hints.ai_socktype = socket_type;

83+

84+ // Get info about the remote host (DNS lookup etc)

85+ int addr_res = getaddrinfo(host, str_port, &hints, &remote_host);

86+ if (addr_res == -1) {

87+ return -1;

88+ }

89+

90+ int connect_res = connect(sockfd, remote_host->ai_addr, remote_host->ai_addrlen);

91+ if (connect_res == -1) {

92+ return -1;

93+ }

94+

95+ return 0;

96+}

97+

98+

99+int idrnet_sockaddr_family(void* sockaddr) {

100+ struct sockaddr* addr = (struct sockaddr*) sockaddr;

101+ return (int) addr->sa_family;

102+}

103+

104+char* idrnet_sockaddr_ipv4(void* sockaddr) {

105+ struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;

106+ char* ip_addr = (char*) malloc(sizeof(char) * INET_ADDRSTRLEN);

107+ inet_ntop(AF_INET, &(addr->sin_addr), ip_addr, INET_ADDRSTRLEN);

108+ return ip_addr;

109+}

110+

111+void* idrnet_create_sockaddr() {

112+ return malloc(sizeof(struct sockaddr_storage));

113+}

114+

115+

116+int idrnet_accept(int sockfd, void* sockaddr) {

117+ struct sockaddr* addr = (struct sockaddr*) sockaddr;

118+ socklen_t addr_size = 0;

119+ if (!check_init()) {

120+ return -1;

121+ }

122+ return accept(sockfd, addr, &addr_size);

123+}

124+

125+int idrnet_send(int sockfd, char* data) {

126+ int len = strlen(data); // For now.

127+ if (!check_init()) {

128+ return -1;

129+ }

130+ return send(sockfd, (void*) data, len, 0);

131+}

132+

133+int idrnet_send_buf(int sockfd, void* data, int len) {

134+ if (!check_init()) {

135+ return -1;

136+ }

137+ return send(sockfd, data, len, 0);

138+}

139+

140+void* idrnet_recv(int sockfd, int len) {

141+ if (!check_init()) {

142+ return -1;

143+ }

144+ idrnet_recv_result* res_struct =

145+ (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));

146+

147+ char* buf = malloc(len + 1);

148+ int recv_res = recv(sockfd, buf, len, 0);

149+ res_struct->result = recv_res;

150+

151+ if (recv_res > 0) { // Data was received

152+ buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it

153+ }

154+ res_struct->payload = (void*) buf;

155+ return (void*) res_struct;

156+}

157+

158+int idrnet_recv_buf(int sockfd, void* buf, int len) {

159+ if (!check_init()) {

160+ return -1;

161+ }

162+ return recv(sockfd, buf, len, 0);

163+}

164+

165+int idrnet_get_recv_res(void* res_struct) {

166+ return (((idrnet_recv_result*) res_struct)->result);

167+}

168+

169+void* idrnet_get_recv_payload(void* res_struct) {

170+ return (((idrnet_recv_result*) res_struct)->payload);

171+}

172+

173+void idrnet_free_recv_struct(void* res_struct) {

174+ idrnet_recv_result* i_res_struct =

175+ (idrnet_recv_result*) res_struct;

176+ if (i_res_struct->payload != NULL) {

177+ free(i_res_struct->payload);

178+ }

179+ free(res_struct);

180+}

181+

182+int idrnet_errno() {

183+ return errno;

184+}

185+

rts/windows/idris_net.hnew file+45

@@ -0,0 +1,45 @@

1+#ifndef IDRISNET_H

2+#define IDRISNET_H

3+

4+

5+typedef struct idrnet_recv_result {

6+ int result;

7+ void* payload;

8+} idrnet_recv_result;

9+

10+// Memory management functions

11+void* idrnet_malloc(int size);

12+void idrnet_free(void* ptr);

13+

14+// Gets value of errno

15+int idrnet_errno();

16+

17+// Bind

18+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port);

19+

20+// Connect

21+int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port);

22+

23+// Accessor functions for struct_sockaddr

24+int idrnet_sockaddr_family(void* sockaddr);

25+char* idrnet_sockaddr_ipv4(void* sockaddr);

26+void* idrnet_create_sockaddr();

27+

28+// Accept

29+int idrnet_accept(int sockfd, void* sockaddr);

30+

31+// Send

32+int idrnet_send(int sockfd, char* data);

33+int idrnet_send_buf(int sockfd, void* data, int len);

34+

35+// Receive

36+// Creates a result structure containing result and payload

37+void* idrnet_recv(int sockfd, int len);

38+// Receives directly into a buffer

39+int idrnet_recv_buf(int sockfd, void* buf, int len);

40+

41+// Receive structure accessors

42+int idrnet_get_recv_res(void* res_struct);

43+void* idrnet_get_recv_payload(void* res_struct);

44+void idrnet_free_recv_struct(void* res_struct);

45+#endif

rts/windows/idris_stdfgn.cnew file+63

@@ -0,0 +1,63 @@

1+#include "idris_stdfgn.h"

2+#include "../idris_rts.h"

3+#include <fcntl.h>

4+#include <stdio.h>

5+

6+extern char** environ;

7+

8+void putStr(char* str) {

9+ printf("%s", str);

10+}

11+

12+void* fileOpen(char* name, char* mode) {

13+ FILE* f = fopen(name, mode);

14+ return (void*)f;

15+}

16+

17+void fileClose(void* h) {

18+ FILE* f = (FILE*)h;

19+ fclose(f);

20+}

21+

22+int fileEOF(void* h) {

23+ FILE* f = (FILE*)h;

24+ return feof(f);

25+}

26+

27+int fileError(void* h) {

28+ FILE* f = (FILE*)h;

29+ return ferror(f);

30+}

31+

32+void fputStr(void* h, char* str) {

33+ FILE* f = (FILE*)h;

34+ fputs(str, f);

35+}

36+

37+int fpoll(void* h)

38+{

39+ return 0;

40+}

41+

42+void* do_popen(const char* cmd, const char* mode) {

43+ FILE* f = _popen(cmd, mode);

44+// int d = fileno(f);

45+// fcntl(d, F_SETFL, O_NONBLOCK);

46+ return f;

47+}

48+

49+int isNull(void* ptr) {

50+ return ptr==NULL;

51+}

52+

53+int idris_eqPtr(void* x, void* y) {

54+ return x==y;

55+}

56+

57+void* idris_stdin() {

58+ return (void*)stdin;

59+}

60+

61+char* getEnvPair(int i) {

62+ return *(environ + i);

63+}

rts/windows/idris_stdfgn.hnew file+24

@@ -0,0 +1,24 @@

1+#ifndef _IDRISSTDFGN_H

2+#define _IDRISSTDFGN_H

3+

4+// A collection of useful standard functions to be used by the prelude.

5+

6+void putStr(char* str);

7+//char* readStr();

8+

9+void* fileOpen(char* f, char* mode);

10+void fileClose(void* h);

11+int fileEOF(void* h);

12+int fileError(void* h);

13+void fputStr(void*h, char* str);

14+

15+void* do_popen(const char* cmd, const char* mode);

16+int fpoll(void* h);

17+

18+int idris_eqPtr(void* x, void* y);

19+int isNull(void* ptr);

20+void* idris_stdin();

21+

22+char* getEnvPair(int i);

23+

24+#endif

samples/reflection.idr+25−25

@@ -2,93 +2,93 @@ module ReflectionExamples

22

33import Language.Reflection

44

5−-- | The reflected term for (\ x => reverse "bba")

5+||| The reflected term for (\ x => reverse "bba")

66reflectVal : TT

77reflectVal = ?valPrf

88

9−-- | intEq for the integers 3 and 3

9+||| intEq for the integers 3 and 3

1010applyTac1 : Int

1111applyTac1 = ?tacPrf1

1212

13−-- | intEq for the integers 3 and 42

13+||| intEq for the integers 3 and 42

1414applyTac0 : Int

1515applyTac0 = ?tacPrf0

1616

17−-- | intEq for the two arguments

17+||| intEq for the two arguments

1818applyTacDyn : Int -> Int -> Int

1919applyTacDyn x y = ?tacPrfDyn

2020

21−-- | Restored version for RConstant (I 42)

21+||| Restored version for RConstant (I 42)

2222fill : Int

2323fill = ?fillPrf

2424

25−-- | The type (TTName, TT) computed from its reflected raw rep.

25+||| The type (TTName, TT) computed from its reflected raw rep.

2626envTuple : Type

2727envTuple = ?envTuplePrf

2828

29−-- | The type List (TTName, TT) computed from its reflected raw rep.

29+||| The type List (TTName, TT) computed from its reflected raw rep.

3030envList : List (TTName, TT)

3131envList = ?envListPrf

3232

33−-- | Reflected raw rep. for the type (TTName, TT)

33+||| Reflected raw rep. for the type (TTName, TT)

3434tupleType : Raw

3535tupleType = RApp (RApp (Var (MN 0 "__Pair"))

3636 (Var (NS (UN "TTName") ["Reflection", "Language"])))

3737 (Var (NS (UN "TT") ["Reflection", "Language"]))

3838

39−-- | Reflected raw rep for the type List (TTName, TT)

39+||| Reflected raw rep for the type List (TTName, TT)

4040mkTuple : Raw

4141mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))

4242 (Var (NS (UN "TTName") ["Reflection", "Language"])))

4343 (Var (NS (UN "TT") ["Reflection", "Language"]))

4444

45−-- | Reflected raw rep for Prelude.List.Nil

45+||| Reflected raw rep for Prelude.List.Nil

4646nil : Raw

4747nil = (Var (NS (UN "Nil") ["List", "Prelude"]))

4848

49−-- | Reflected raw rep for Prelude.List.::

49+||| Reflected raw rep for Prelude.List.::

5050cons : Raw

5151cons = (Var (NS (UN "::") ["List", "Prelude"]))

5252

53−-- | 1 if the two arguments are equal, 0 otherwise

54−-- This function is chosen as simple as possible for

55−-- demo purposes.

53+||| 1 if the two arguments are equal, 0 otherwise

54+||| This function is chosen as simple as possible for

55+||| demo purposes.

5656intEq : Int -> Int -> Int

5757intEq x y = case x == y of

5858 True => 1

5959 False => 0

6060

61−-- | A tactic script to run intEq on two let-bound or introduced

62−-- arguments of the current (otherwise empty) proof context

61+||| A tactic script to run intEq on two let-bound or introduced

62+||| arguments of the current (otherwise empty) proof context

6363firstEq : List (TTName, Binder TT) -> TT -> Tactic

6464firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App f x) y)

6565firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))

6666firstEq xs _ = Exact (TConst (I 0))

6767

68−-- | Skip 1 argument of the proof context and return the second one which

69−-- has to be introduced. Used for the tactical dispatch example, which

70−-- will push dispatch, as first env agrument.

68+||| Skip 1 argument of the proof context and return the second one which

69+||| has to be introduced. Used for the tactical dispatch example, which

70+||| will push dispatch, as first env agrument.

7171innerTac : List (TTName, Binder TT) -> TT -> Tactic

7272innerTac (_::(x, Lam xt)::_) _ = Exact (P Bound x xt)

7373

74−-- | Returns the reflected representation of innerTac

74+||| Returns the reflected representation of innerTac

7575innerTacTT : TT

7676innerTacTT = ?innerTacTTPrf

7777

78−-- | Dispatch to the reflected rep. of innerTac

78+||| Dispatch to the reflected rep. of innerTac

7979dispatch : List (TTName, Binder TT) -> TT -> Tactic

8080dispatch xs _ = ApplyTactic (innerTacTT)

8181

82−-- | Call dispatch which will then dispatch to innerTac.

82+||| Call dispatch which will then dispatch to innerTac.

8383tacticalDispatch : Int -> Int

8484tacticalDispatch = ?tacticalDispatchPrf

8585

86−-- | A tactic to get the representation of its goal

86+||| A tactic to get the representation of its goal

8787studyGoalTac : List (TTName, Binder TT) -> TT -> Tactic

8888studyGoalTac _ goal = Reflect goal

8989

90−-- | Returns the representation of its goal, TT

91−-- (so this is reflect on the type TT)

90+||| Returns the representation of its goal, TT

91+||| (so this is reflect on the type TT)

9292studyGoal : TT

9393studyGoal = ?studyGoalPrf

9494

src/IRTS/CodegenC.hs+4

@@ -262,6 +262,7 @@ c_irts (FArith (ATInt (ITFixed ity))) l x

262262c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")"

263263c_irts FUnit l x = x

264264c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

265+c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")"

265266c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

266267c_irts FAny l x = l ++ x

267268

@@ -272,6 +273,7 @@ irts_c (FArith (ATInt (ITFixed ity))) x

272273irts_c FString x = "GETSTR(" ++ x ++ ")"

273274irts_c FUnit x = x

274275irts_c FPtr x = "GETPTR(" ++ x ++ ")"

276+irts_c FManagedPtr x = "GETMPTR(" ++ x ++ ")"

275277irts_c (FArith ATFloat) x = "GETFLOAT(" ++ x ++ ")"

276278irts_c FAny x = x

277279

@@ -470,6 +472,8 @@ doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ",

470472doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

471473doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

472474doOp v LNullPtr [] = v ++ "MKPTR(vm, NULL)"

475+doOp v LRegisterPtr [p, i] = v ++ "MKMPTR(vm, GETPTR(" ++ creg p ++

476+ "), GETINT(" ++ creg i ++ "))"

473477doOp v (LChInt ITNative) args = v ++ creg (last args)

474478doOp v (LChInt ITChar) args = doOp v (LChInt ITNative) args

475479doOp v (LIntCh ITNative) args = v ++ creg (last args)

src/IRTS/CodegenJava.hs+3−8

@@ -365,17 +365,11 @@ mkGlobalContext initExps = do

365365

366366addMainMethod :: [Decl] -> [Decl]

367367addMainMethod decls

368− | findMain decls = mkMainMethod : decls

368+ | findMainMethod decls = mkMainMethod : decls

369369 | otherwise = decls

370370 where

371− findMain ((MemberDecl (MemberClassDecl (ClassDecl _ name _ _ _ (ClassBody body)))):_)

372− | name == mangle' (sUN "Main") = findMainMethod body

373− findMain (_:decls) = findMain decls

374− findMain [] = False

375−

376− innerMainMethod = (either error id $ mangle (sUN "main"))

377371 findMainMethod ((MemberDecl (MethodDecl _ _ _ name [] _ _)):_)

378− | name == mangle' (sUN "main") = True

372+ | name == mangle' (sMN 0 "runMain") = True

379373 findMainMethod (_:decls) = findMainMethod decls

380374 findMainMethod [] = False

381375

@@ -707,6 +701,7 @@ mkConstant c@(B64V x) = mkConstantArray (constType c) B64 x

707701mkConstant c@(AType x) = ClassLit (Just $ box (constType c))

708702mkConstant c@(StrType ) = ClassLit (Just $ stringType)

709703mkConstant c@(PtrType ) = ClassLit (Just $ objectType)

704+mkConstant c@(ManagedPtrType) = ClassLit (Just $ objectType)

710705mkConstant c@(VoidType ) = ClassLit (Just $ voidType)

711706mkConstant c@(Forgot ) = ClassLit (Just $ objectType)

712707

src/IRTS/CodegenJavaScript.hs+113−66

@@ -20,6 +20,7 @@ import Data.Maybe

2020import System.IO

2121import System.Directory

2222

23+

2324idrNamespace :: String

2425idrNamespace = "__IDR__"

2526idrRTNamespace = "__IDRRT__"

@@ -52,6 +53,13 @@ data JSNum = JSInt Int

5253 deriving Eq

5354

5455

56+data JSAnnotation = JSConstructor deriving Eq

57+

58+

59+instance Show JSAnnotation where

60+ show JSConstructor = "constructor"

61+

62+

5563data JS = JSRaw String

5664 | JSIdent String

5765 | JSFunction [String] JS

@@ -80,13 +88,56 @@ data JS = JSRaw String

8088 | JSTernary JS JS JS

8189 | JSParens JS

8290 | JSWhile JS JS

91+ | JSFFI String [JS]

92+ | JSAnnotation JSAnnotation JS

8393 | JSNoop

8494 deriving Eq

8595

8696

97+data FFI = FFICode Char | FFIArg Int | FFIError String

98+

99+

100+ffi :: String -> [String] -> String

101+ffi code args = let parsed = ffiParse code in

102+ case ffiError parsed of

103+ Just err -> compileJS $ jsError err

104+ Nothing -> renderFFI parsed args

105+ where

106+ ffiParse :: String -> [FFI]

107+ ffiParse "" = []

108+ ffiParse ['%'] = [FFIError "Invalid positional argument"]

109+ ffiParse ('%':'%':ss) = FFICode '%' : ffiParse ss

110+ ffiParse ('%':s:ss)

111+ | isDigit s =

112+ FFIArg (read $ s : takeWhile isDigit ss) : ffiParse (dropWhile isDigit ss)

113+ | otherwise =

114+ [FFIError "Invalid positional argument"]

115+ ffiParse (s:ss) = FFICode s : ffiParse ss

116+

117+

118+ ffiError :: [FFI] -> Maybe String

119+ ffiError [] = Nothing

120+ ffiError ((FFIError s):xs) = Just s

121+ ffiError (x:xs) = ffiError xs

122+

123+

124+ renderFFI :: [FFI] -> [String] -> String

125+ renderFFI [] _ = ""

126+ renderFFI ((FFICode c) : fs) args = c : renderFFI fs args

127+ renderFFI ((FFIArg i) : fs) args

128+ | i < length args && i >= 0 = args !! i ++ renderFFI fs args

129+ | otherwise = "Argument index out of bounds"

130+

131+

87132compileJS :: JS -> String

88133compileJS JSNoop = ""

89134

135+compileJS (JSAnnotation annotation js) =

136+ "/** @" ++ show annotation ++ " */\n" ++ compileJS js

137+

138+compileJS (JSFFI raw args) =

139+ ffi raw (map compileJS args)

140+

90141compileJS (JSRaw code) =

91142 code

92143

@@ -316,6 +367,10 @@ foldJS tr add acc js =

316367 add (tr js) $ foldl' add acc $ map (uncurry add . (fold *** fold)) conds

317368 | JSWhile cond body <- js =

318369 add (tr js) $ add (fold cond) (fold body)

370+ | JSFFI raw args <- js =

371+ add (tr js) $ foldl' add acc $ map fold args

372+ | JSAnnotation a js <- js =

373+ add (tr js) $ fold js

319374 | otherwise =

320375 tr js

321376

@@ -342,7 +397,9 @@ transformJS tr js =

342397 | JSCond conds <- js = JSCond $ map (tr *** tr) conds

343398 | JSTernary c t f <- js = JSTernary (tr c) (tr t) (tr f)

344399 | JSParens val <- js = JSParens $ tr val

345− | JSWhile cond body <- js = JSWhile(tr cond) (tr body)

400+ | JSWhile cond body <- js = JSWhile (tr cond) (tr body)

401+ | JSFFI raw args <- js = JSFFI raw (map tr args)

402+ | JSAnnotation a js <- js = JSAnnotation a (tr js)

346403 | otherwise = js

347404

348405

@@ -350,6 +407,9 @@ moveJSDeclToTop :: String -> [JS] -> [JS]

350407moveJSDeclToTop decl js = move ([], js)

351408 where

352409 move :: ([JS], [JS]) -> [JS]

410+ move (front, js@(JSAnnotation _ (JSAlloc name _)):back)

411+ | name == decl = js : front ++ back

412+

353413 move (front, js@(JSAlloc name _):back)

354414 | name == decl = js : front ++ back

355415

@@ -519,8 +579,6 @@ removeEval js =

519579 match (JSApp (JSIdent "__IDR__mEVAL0") [val]) = val

520580 match js = transformJS match js

521581

522− removeEvalApp js = js

523−

524582 checkEval :: [JS] -> ([JS], Bool)

525583 checkEval js = foldr f ([], False) $ map checkEval' js

526584 where

@@ -664,7 +722,7 @@ inlineFunctions js =

664722 inlineHelper ([], js)

665723 where

666724 inlineHelper :: ([JS], [JS]) -> [JS]

667− inlineHelper (front , (JSAlloc fun (Just (JSFunction args body))):back)

725+ inlineHelper (front , (JSAlloc fun (Just (JSFunction args body))):back)

668726 | countAll fun front + countAll fun back == 0 =

669727 inlineHelper (front, back)

670728 | Just new <- inlineAble (

@@ -1012,7 +1070,7 @@ unfoldLookupTable input =

10121070 adaptCon js =

10131071 adaptCon' [] js

10141072 where

1015− adaptCon' front ((JSAlloc "__IDRRT__Con" (Just _)):back) =

1073+ adaptCon' front ((JSAnnotation _ (JSAlloc "__IDRRT__Con" _)):back) =

10161074 front ++ (new:back)

10171075

10181076 adaptCon' front (next:back) =

@@ -1022,11 +1080,12 @@ unfoldLookupTable input =

10221080

10231081

10241082 new =

1025− JSAlloc "__IDRRT__Con" (Just $

1026− JSFunction newArgs (

1027− JSSeq (map newVar newArgs)

1083+ JSAnnotation JSConstructor $

1084+ JSAlloc "__IDRRT__Con" (Just $

1085+ JSFunction newArgs (

1086+ JSSeq (map newVar newArgs)

1087+ )

10281088 )

1029− )

10301089 where

10311090 newVar var = JSAssign (JSProj JSThis var) (JSIdent var)

10321091 newArgs = ["tag", "eval", "app", "vars"]

@@ -1338,7 +1397,7 @@ codegenJavaScript

13381397 -> OutputType

13391398 -> IO ()

13401399codegenJavaScript target definitions includes filename outputType = do

1341− let (header, runtime) = case target of

1400+ let (header, rt) = case target of

13421401 Node ->

13431402 ("#!/usr/bin/env node\n", "-node")

13441403 JavaScript ->

@@ -1346,13 +1405,10 @@ codegenJavaScript target definitions includes filename outputType = do

13461405 included <- getIncludes includes

13471406 path <- (++) <$> getDataDir <*> (pure "/jsrts/")

13481407 idrRuntime <- readFile $ path ++ "Runtime-common.js"

1349− tgtRuntime <- readFile $ concat [path, "Runtime", runtime, ".js"]

1408+ tgtRuntime <- readFile $ concat [path, "Runtime", rt, ".js"]

13501409 jsbn <- readFile $ path ++ "jsbn/jsbn.js"

13511410 writeFile filename $ header ++ (

1352− intercalate "\n" $ included ++ [ jsbn

1353− , idrRuntime

1354− , tgtRuntime

1355− ] ++ functions

1411+ intercalate "\n" $ included ++ runtime jsbn idrRuntime tgtRuntime ++ functions

13561412 )

13571413

13581414 setPermissions filename (emptyPermissions { readable = True

@@ -1364,15 +1420,32 @@ codegenJavaScript target definitions includes filename outputType = do

13641420 def = map (first translateNamespace) definitions

13651421

13661422

1367− functions :: [String]

1368− functions = translate >>> optimize >>> compile $ def

1423+ checkForBigInt :: [JS] -> Bool

1424+ checkForBigInt js = occur

1425+ where

1426+ occur :: Bool

1427+ occur = or $ map (foldJS match (||) False) js

1428+

1429+ match :: JS -> Bool

1430+ match (JSIdent "__IDRRT__bigInt") = True

1431+ match (JSNum (JSInteger _)) = True

1432+ match js = False

1433+

1434+

1435+ runtime :: String -> String -> String -> [String]

1436+ runtime jsbn idrRuntime tgtRuntime =

1437+ if checkForBigInt optimized

1438+ then [jsbn, idrRuntime, tgtRuntime]

1439+ else [idrRuntime, tgtRuntime]

1440+

1441+

1442+ optimized :: [JS]

1443+ optimized = translate >>> optimize $ def

13691444 where

13701445 translate p =

13711446 prelude ++ concatMap translateDeclaration p ++ [mainLoop, invokeLoop]

13721447 optimize p =

13731448 foldl' (flip ($)) p opt

1374− compile =

1375− map compileJS

13761449

13771450 opt =

13781451 [ removeEval

@@ -1394,16 +1467,21 @@ codegenJavaScript target definitions includes filename outputType = do

13941467 , evalCons

13951468 ]

13961469

1470+ functions :: [String]

1471+ functions = map compileJS optimized

1472+

13971473 prelude :: [JS]

13981474 prelude =

1399− [ JSAlloc (idrRTNamespace ++ "Cont") (Just $ JSFunction ["k"] (

1400− JSAssign (JSProj JSThis "k") (JSIdent "k")

1401− ))

1402− , JSAlloc (idrRTNamespace ++ "Con") (Just $ JSFunction ["tag", "vars"] (

1403− JSSeq [ JSAssign (JSProj JSThis "tag") (JSIdent "tag")

1404− , JSAssign (JSProj JSThis "vars") (JSIdent "vars")

1405− ]

1406− ))

1475+ [ JSAnnotation JSConstructor $

1476+ JSAlloc (idrRTNamespace ++ "Cont") (Just $ JSFunction ["k"] (

1477+ JSAssign (JSProj JSThis "k") (JSIdent "k")

1478+ ))

1479+ , JSAnnotation JSConstructor $

1480+ JSAlloc (idrRTNamespace ++ "Con") (Just $ JSFunction ["tag", "vars"] (

1481+ JSSeq [ JSAssign (JSProj JSThis "tag") (JSIdent "tag")

1482+ , JSAssign (JSProj JSThis "vars") (JSIdent "vars")

1483+ ]

1484+ ))

14071485 ]

14081486

14091487 mainLoop :: JS

@@ -1887,16 +1965,20 @@ translateExpression (SForeign _ _ "idris_eqPtr" [(FPtr, lhs),(FPtr, rhs)]) =

18871965 JSBinOp "==" (JSVar lhs) (JSVar rhs)

18881966

18891967translateExpression (SForeign _ _ fun args) =

1890− ffi fun (map generateWrapper args)

1968+ JSFFI fun (map generateWrapper args)

18911969 where

18921970 generateWrapper (ffunc, name)

18931971 | FFunction <- ffunc =

1894− idrRTNamespace ++ "ffiWrap(" ++ translateVariableName name ++ ")"

1972+ JSApp (

1973+ JSIdent $ idrRTNamespace ++ "ffiWrap"

1974+ ) [JSIdent $ translateVariableName name]

18951975 | FFunctionIO <- ffunc =

1896− idrRTNamespace ++ "ffiWrap(" ++ translateVariableName name ++ ")"

1976+ JSApp (

1977+ JSIdent $ idrRTNamespace ++ "ffiWrap"

1978+ ) [JSIdent $ translateVariableName name]

18971979

18981980 generateWrapper (_, name) =

1899− translateVariableName name

1981+ JSIdent $ translateVariableName name

19001982

19011983translateExpression patterncase

19021984 | (SChkCase var cases) <- patterncase = caseHelper var cases "chk"

@@ -1939,41 +2021,6 @@ translateExpression e =

19392021 jsError $ "Not yet implemented: " ++ filter (/= '\'') (show e)

19402022

19412023

1942−data FFI = FFICode Char | FFIArg Int | FFIError String

1943−

1944−

1945−ffi :: String -> [String] -> JS

1946−ffi code args = let parsed = ffiParse code in

1947− case ffiError parsed of

1948− Just err -> jsError err

1949− Nothing -> JSRaw $ renderFFI parsed args

1950− where

1951− ffiParse :: String -> [FFI]

1952− ffiParse "" = []

1953− ffiParse ['%'] = [FFIError "Invalid positional argument"]

1954− ffiParse ('%':'%':ss) = FFICode '%' : ffiParse ss

1955− ffiParse ('%':s:ss)

1956− | isDigit s =

1957− FFIArg (read $ s : takeWhile isDigit ss) : ffiParse (dropWhile isDigit ss)

1958− | otherwise =

1959− [FFIError "Invalid positional argument"]

1960− ffiParse (s:ss) = FFICode s : ffiParse ss

1961−

1962−

1963− ffiError :: [FFI] -> Maybe String

1964− ffiError [] = Nothing

1965− ffiError ((FFIError s):xs) = Just s

1966− ffiError (x:xs) = ffiError xs

1967−

1968−

1969− renderFFI :: [FFI] -> [String] -> String

1970− renderFFI [] _ = ""

1971− renderFFI ((FFICode c) : fs) args = c : renderFFI fs args

1972− renderFFI ((FFIArg i) : fs) args

1973− | i < length args && i >= 0 = args !! i ++ renderFFI fs args

1974− | otherwise = "Argument index out of bounds"

1975−

1976−

19772024data CaseType = ConCase Int

19782025 | TypeCase JSType

19792026 | DefaultCase

src/IRTS/Compiler.hs+1

@@ -349,6 +349,7 @@ mkIty "FBits32" = mkIntIty "IT32"

349349mkIty "FBits64" = mkIntIty "IT64"

350350mkIty "FString" = FString

351351mkIty "FPtr" = FPtr

352+mkIty "FManagedPtr" = FManagedPtr

352353mkIty "FUnit" = FUnit

353354mkIty "FFunction" = FFunction

354355mkIty "FFunctionIO" = FFunctionIO

src/IRTS/Lang.hs+2

@@ -66,6 +66,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

6666 -- core or another machine. 'id' is a valid implementation

6767 | LVMPtr

6868 | LNullPtr

69+ | LRegisterPtr

6970 | LNoOp

7071 deriving (Show, Eq)

7172

@@ -83,6 +84,7 @@ data FType = FArith ArithTy

8384 | FString

8485 | FUnit

8586 | FPtr

87+ | FManagedPtr

8688 | FAny

8789 deriving (Show, Eq)

8890

src/Idris/AbsSyntax.hs+65−51

@@ -262,10 +262,10 @@ addCoercion :: Name -> Idris ()

262262addCoercion n = do i <- getIState

263263 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

264264

265−addDocStr :: Name -> String -> Idris ()

266−addDocStr n doc

265+addDocStr :: Name -> String -> [(Name, String)] -> Idris ()

266+addDocStr n doc args

267267 = do i <- getIState

268− putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }

268+ putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

269269

270270addNameHint :: Name -> Name -> Idris ()

271271addNameHint ty n

@@ -460,6 +460,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)

460460addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

461461addDeferred' nt ns

462462 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

463+ mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

463464 i <- getIState

464465 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

465466 idris_metavars i }

@@ -475,7 +476,12 @@ solveDeferred :: Name -> Idris ()

475476solveDeferred n = do i <- getIState

476477 putIState $ i { idris_metavars =

477478 filter (\(n', _) -> n/=n')

478− (idris_metavars i) }

479+ (idris_metavars i),

480+ ibc_write =

481+ filter (notMV n) (ibc_write i)

482+ }

483+ where notMV n (IBCMetavar n') = not (n == n')

484+ notMV n _ = True

479485

480486getUndefined :: Idris [Name]

481487getUndefined = do i <- getIState

@@ -993,12 +999,12 @@ expandParams dec ps ns infs tm = en tm

993999expandParamsD :: Bool -> -- True = RHS only

9941000 IState ->

9951001 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

996−expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)

1002+expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)

9971003 = if n `elem` ns && (not rhsonly)

9981004 then -- trace (show (n, expandParams dec ps ns ty)) $

999− PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))

1005+ PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))

10001006 else --trace (show (n, expandParams dec ps ns ty)) $

1001− PTy doc syn fc o n (expandParams dec ps ns [] ty)

1007+ PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)

10021008expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

10031009 = if n `elem` ns && (not rhsonly)

10041010 then -- trace (show (n, expandParams dec ps ns ty)) $

@@ -1044,8 +1050,8 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

10441050 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r

10451051 bnames _ = []

10461052

1047−expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

1048− = PData doc syn fc co (expandPData pd)

1053+expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

1054+ = PData doc argDocs syn fc co (expandPData pd)

10491055 where

10501056 -- just do the type decl, leave constructors alone (parameters will be

10511057 -- added implicitly)

@@ -1054,8 +1060,15 @@ expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

10541060 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))

10551061 (map econ cons)

10561062 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1057− econ (doc, n, t, fc, fs)

1058− = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

1063+ econ (doc, argDocs, n, t, fc, fs)

1064+ = (doc, argDocs, dec n, piBindp impl ps (expandParams dec ps ns [] t), fc, fs)

1065+expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

1066+ = if tn `elem` ns

1067+ then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

1068+ cdoc (dec cn) conty

1069+ else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

1070+ cdoc (dec cn) conty

1071+ where conty = piBindp impl ps (expandParams dec ps ns [] cty)

10591072expandParamsD rhs ist dec ps ns (PParams f params pds)

10601073 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

10611074 (map (expandParamsD True ist dec ps ns) pds)

@@ -1112,6 +1125,7 @@ getPriority i tm = 1 -- pri tm

11121125 pri Placeholder = 1

11131126 pri _ = 3

11141127

1128+

11151129addStatics :: Name -> Term -> PTerm -> Idris ()

11161130addStatics n tm ptm =

11171131 do let (statics, dynamics) = initStatics tm ptm

@@ -1145,8 +1159,8 @@ addStatics n tm ptm =

11451159 -- if a name appears in a type class or tactic implicit index, it doesn't

11461160 -- affect its 'uniquely inferrable' from a static status since these are

11471161 -- resolved by searching.

1148− searchArg (Constraint _ _ _) = True

1149− searchArg (TacImp _ _ _ _) = True

1162+ searchArg (Constraint _ _) = True

1163+ searchArg (TacImp _ _ _) = True

11501164 searchArg _ = False

11511165

11521166 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

@@ -1173,14 +1187,14 @@ addUsingConstraints syn fc t

11731187 -- if all of args in ns, then add it

11741188 doAdd (UConstraint c args : cs) ns t

11751189 | all (\n -> elem n ns) args

1176− = PPi (Constraint [] Dynamic "") (sMN 0 "cu")

1190+ = PPi (Constraint [] Dynamic) (sMN 0 "cu")

11771191 (mkConst c args) (doAdd cs ns t)

11781192 | otherwise = doAdd cs ns t

11791193

11801194 mkConst c args = PApp fc (PRef fc c)

1181− (map (\n -> PExp 0 [] (PRef fc n) "") args)

1195+ (map (\n -> PExp 0 [] (PRef fc n)) args)

11821196

1183− getConstraints (PPi (Constraint _ _ _) _ c sc)

1197+ getConstraints (PPi (Constraint _ _) _ c sc)

11841198 = getcapp c ++ getConstraints sc

11851199 getConstraints (PPi _ _ c sc) = getConstraints sc

11861200 getConstraints _ = []

@@ -1190,7 +1204,7 @@ addUsingConstraints syn fc t

11901204 return (UConstraint c ns)

11911205 getcapp _ = []

11921206

1193− getName (PExp _ _ (PRef _ n) _) = return n

1207+ getName (PExp _ _ (PRef _ n)) = return n

11941208 getName _ = []

11951209

11961210-- Add implicit Pi bindings for any names in the term which appear in an

@@ -1240,34 +1254,34 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

12401254 = do (decls, ns) <- get

12411255 let isn = concatMap (namesIn uvars ist) (map getTm as)

12421256 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1243− imps top env (PPi (Imp l _ doc _) n ty sc)

1257+ imps top env (PPi (Imp l _ _) n ty sc)

12441258 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

12451259 (decls , ns) <- get

1246− put (PImp (getPriority ist ty) True l n Placeholder doc : decls,

1260+ put (PImp (getPriority ist ty) True l n Placeholder : decls,

12471261 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12481262 imps True (n:env) sc

1249− imps top env (PPi (Exp l _ doc _) n ty sc)

1263+ imps top env (PPi (Exp l _ _) n ty sc)

12501264 = do let isn = nub (namesIn uvars ist ty ++ case sc of

12511265 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12521266 _ -> [])

12531267 (decls, ns) <- get -- ignore decls in HO types

1254− put (PExp (getPriority ist ty) l Placeholder doc : decls,

1268+ put (PExp (getPriority ist ty) l Placeholder : decls,

12551269 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12561270 imps True (n:env) sc

1257− imps top env (PPi (Constraint l _ doc) n ty sc)

1271+ imps top env (PPi (Constraint l _) n ty sc)

12581272 = do let isn = nub (namesIn uvars ist ty ++ case sc of

12591273 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12601274 _ -> [])

12611275 (decls, ns) <- get -- ignore decls in HO types

1262− put (PConstraint 10 l Placeholder doc : decls,

1276+ put (PConstraint 10 l Placeholder : decls,

12631277 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12641278 imps True (n:env) sc

1265− imps top env (PPi (TacImp l _ scr doc) n ty sc)

1279+ imps top env (PPi (TacImp l _ scr) n ty sc)

12661280 = do let isn = nub (namesIn uvars ist ty ++ case sc of

12671281 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12681282 _ -> [])

12691283 (decls, ns) <- get -- ignore decls in HO types

1270− put (PTacImplicit 10 l n scr Placeholder doc : decls,

1284+ put (PTacImplicit 10 l n scr Placeholder : decls,

12711285 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12721286 imps True (n:env) sc

12731287 imps top env (PEq _ l r)

@@ -1308,8 +1322,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

13081322 pibind using [] sc = sc

13091323 pibind using (n:ns) sc

13101324 = case lookup n using of

1311− Just ty -> PPi (Imp [] Dynamic "" False) n ty (pibind using ns sc)

1312− Nothing -> PPi (Imp [] Dynamic "" False) n Placeholder

1325+ Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)

1326+ Nothing -> PPi (Imp [] Dynamic False) n Placeholder

13131327 (pibind using ns sc)

13141328

13151329-- Add implicit arguments in function calls

@@ -1425,7 +1439,7 @@ aiFn inpat True ist fc f ds []

14251439-- any constructor alts || any allImp ialts))

14261440 then aiFn inpat False ist fc f ds [] -- use it as a constructor

14271441 else Right $ PPatvar fc f

1428− where imp (PExp _ _ _ _) = False

1442+ where imp (PExp _ _ _) = False

14291443 imp _ = True

14301444-- allImp [] = False

14311445 allImp xs = all imp xs

@@ -1474,30 +1488,30 @@ aiFn inpat expat ist fc f ds as

14741488

14751489

14761490 insertImpl :: [PArg] -> [PArg] -> [PArg]

1477− insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =

1478− PExp p l tm d : insertImpl ps given

1479− insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =

1480− PConstraint p l tm d : insertImpl ps given

1481− insertImpl (PConstraint p l ty d : ps) given =

1482− PConstraint p l (PResolveTC fc) d : insertImpl ps given

1483− insertImpl (PImp p _ l n ty d : ps) given =

1491+ insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

1492+ PExp p l tm : insertImpl ps given

1493+ insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =

1494+ PConstraint p l tm : insertImpl ps given

1495+ insertImpl (PConstraint p l ty : ps) given =

1496+ PConstraint p l (PResolveTC fc) : insertImpl ps given

1497+ insertImpl (PImp p _ l n ty : ps) given =

14841498 case find n given [] of

1485− Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'

1486− Nothing -> PImp p True l n Placeholder "" : insertImpl ps given

1487− insertImpl (PTacImplicit p l n sc' ty d : ps) given =

1499+ Just (tm, given') -> PImp p False l n tm : insertImpl ps given'

1500+ Nothing -> PImp p True l n Placeholder : insertImpl ps given

1501+ insertImpl (PTacImplicit p l n sc' ty : ps) given =

14881502 let sc = addImpl ist sc' in

14891503 case find n given [] of

1490− Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'

1504+ Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'

14911505 Nothing -> if inpat

1492− then PTacImplicit p l n sc Placeholder "" : insertImpl ps given

1493− else PTacImplicit p l n sc sc "" : insertImpl ps given

1506+ then PTacImplicit p l n sc Placeholder : insertImpl ps given

1507+ else PTacImplicit p l n sc sc : insertImpl ps given

14941508 insertImpl expected [] = []

14951509 insertImpl _ given = given

14961510

14971511 find n [] acc = Nothing

1498− find n (PImp _ _ _ n' t _ : gs) acc

1512+ find n (PImp _ _ _ n' t : gs) acc

14991513 | n == n' = Just (t, reverse acc ++ gs)

1500− find n (PTacImplicit _ _ n' _ t _ : gs) acc

1514+ find n (PTacImplicit _ _ n' _ t : gs) acc

15011515 | n == n' = Just (t, reverse acc ++ gs)

15021516 find n (g : gs) acc = find n gs (g : acc)

15031517

@@ -1527,16 +1541,16 @@ stripLinear i tm = evalState (sl tm) [] where

15271541 sl (PApp fc fn args) = do fn' <- sl fn

15281542 args' <- mapM slA args

15291543 return $ PApp fc fn' args'

1530− where slA (PImp p m l n t d) = do t' <- sl t

1531− return $ PImp p m l n t' d

1532− slA (PExp p l t d) = do t' <- sl t

1533− return $ PExp p l t' d

1534− slA (PConstraint p l t d)

1544+ where slA (PImp p m l n t) = do t' <- sl t

1545+ return $ PImp p m l n t'

1546+ slA (PExp p l t) = do t' <- sl t

1547+ return $ PExp p l t'

1548+ slA (PConstraint p l t)

15351549 = do t' <- sl t

1536− return $ PConstraint p l t' d

1537− slA (PTacImplicit p l n sc t d)

1550+ return $ PConstraint p l t'

1551+ slA (PTacImplicit p l n sc t)

15381552 = do t' <- sl t

1539− return $ PTacImplicit p l n sc t' d

1553+ return $ PTacImplicit p l n sc t'

15401554 sl x = return x

15411555

15421556-- Remove functions which aren't applied to anything, which must then

src/Idris/AbsSyntaxTree.hs+75−76

@@ -111,7 +111,7 @@ data IState = IState {

111111 idris_flags :: Ctxt [FnOpt],

112112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113113 idris_calledgraph :: Ctxt [Name],

114− idris_docstrings :: Ctxt String,

114+ idris_docstrings :: Ctxt (String, [(Name, String)]),

115115 idris_tyinfodata :: Ctxt TIData,

116116 idris_totcheck :: [(FC, Name)], -- names to check totality on

117117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

@@ -189,6 +189,7 @@ data IBCWrite = IBCFix FixDecl

189189 | IBCDSL Name

190190 | IBCData Name

191191 | IBCOpt Name

192+ | IBCMetavar Name

192193 | IBCSyntax Syntax

193194 | IBCKeyword String

194195 | IBCImport FilePath

@@ -380,19 +381,15 @@ deriving instance NFData Static

380381-- Mark bindings with their explicitness, and laziness

381382data Plicity = Imp { pargopts :: [ArgOpt],

382383 pstatic :: Static,

383− pdocstr :: String,

384384 pparam :: Bool }

385385 | Exp { pargopts :: [ArgOpt],

386386 pstatic :: Static,

387− pdocstr :: String,

388387 pparam :: Bool }

389388 | Constraint { pargopts :: [ArgOpt],

390− pstatic :: Static,

391− pdocstr :: String }

389+ pstatic :: Static }

392390 | TacImp { pargopts :: [ArgOpt],

393391 pstatic :: Static,

394− pscript :: PTerm,

395− pdocstr :: String }

392+ pscript :: PTerm }

396393 deriving (Show, Eq)

397394

398395plazy :: Plicity -> Bool

@@ -403,11 +400,11 @@ deriving instance Binary Plicity

403400deriving instance NFData Plicity

404401!-}

405402

406−impl = Imp [Lazy] Dynamic "" False

407−expl = Exp [] Dynamic "" False

408−expl_param = Exp [] Dynamic "" True

409−constraint = Constraint [] Dynamic ""

410−tacimpl t = TacImp [] Dynamic t ""

403+impl = Imp [Lazy] Dynamic False

404+expl = Exp [] Dynamic False

405+expl_param = Exp [] Dynamic True

406+constraint = Constraint [] Dynamic

407+tacimpl t = TacImp [] Dynamic t

411408

412409data FnOpt = Inlinable -- always evaluate when simplifying

413410 | TotalFn | PartialFn

@@ -443,15 +440,21 @@ data DataOpt = Codata -- Set if the the data-type is coinductive

443440

444441type DataOpts = [DataOpt]

445442

443+-- | Type provider - what to provide

444+data ProvideWhat = ProvTerm -- ^ only allow providing terms

445+ | ProvPostulate -- ^ only allow postulates

446+ | ProvAny -- ^ either is ok

447+ deriving (Show, Eq)

448+

446449-- | Top-level declarations such as compiler directives, definitions,

447450-- datatypes and typeclasses.

448451data PDecl' t

449452 = PFix FC Fixity [String] -- ^ Fixity declaration

450− | PTy String SyntaxInfo FC FnOpts Name t -- ^ Type declaration

453+ | PTy String [(Name, String)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

451454 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

452455 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

453456 | PCAF FC Name t -- ^ Top level constant

454− | PData String SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

457+ | PData String [(Name, String)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

455458 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

456459 | PNamespace String [PDecl' t] -- ^ New namespace

457460 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

@@ -474,7 +477,7 @@ data PDecl' t

474477 | PSyntax FC Syntax -- ^ Syntax definition

475478 | PMutual FC [PDecl' t] -- ^ Mutual block

476479 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

477− | PProvider SyntaxInfo FC Name t t -- ^ Type provider. The first t is the type, the second is the term

480+ | PProvider SyntaxInfo FC ProvideWhat Name t t -- ^ Type provider. The first t is the type, the second is the term

478481 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

479482 -- bool is True, lhs and rhs must be convertible

480483 deriving Functor

@@ -509,7 +512,7 @@ deriving instance NFData PClause'

509512-- | Data declaration

510513data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

511514 d_tcon :: t, -- ^ Type constructor

512− d_cons :: [(String, Name, t, FC, [Name])] -- ^ Constructors

515+ d_cons :: [(String, [(Name, String)], Name, t, FC, [Name])] -- ^ Constructors

513516 }

514517 -- ^ Data declaration

515518 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -531,13 +534,13 @@ type PClause = PClause' PTerm

531534

532535declared :: PDecl -> [Name]

533536declared (PFix _ _ _) = []

534−declared (PTy _ _ _ _ n t) = [n]

537+declared (PTy _ _ _ _ _ n t) = [n]

535538declared (PPostulate _ _ _ _ n t) = [n]

536539declared (PClauses _ _ n _) = [] -- not a declaration

537540declared (PCAF _ n _) = [n]

538−declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

539− where fstt (_, a, _, _, _) = a

540−declared (PData _ _ _ _ (PLaterdecl n _)) = [n]

541+declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

542+ where fstt (_, _, a, _, _, _) = a

543+declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

541544declared (PParams _ _ ds) = concatMap declared ds

542545declared (PNamespace _ ds) = concatMap declared ds

543546declared (PRecord _ _ _ n _ _ c _) = [n, c]

@@ -551,12 +554,12 @@ declared (PDirective _) = []

551554-- get the names declared, not counting nested parameter blocks

552555tldeclared :: PDecl -> [Name]

553556tldeclared (PFix _ _ _) = []

554−tldeclared (PTy _ _ _ _ n t) = [n]

557+tldeclared (PTy _ _ _ _ _ n t) = [n]

555558tldeclared (PPostulate _ _ _ _ n t) = [n]

556559tldeclared (PClauses _ _ n _) = [] -- not a declaration

557560tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

558−tldeclared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

559− where fstt (_, a, _, _, _) = a

561+tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

562+ where fstt (_, _, a, _, _, _) = a

560563tldeclared (PParams _ _ ds) = []

561564tldeclared (PMutual _ ds) = concatMap tldeclared ds

562565tldeclared (PNamespace _ ds) = concatMap tldeclared ds

@@ -566,13 +569,13 @@ tldeclared _ = []

566569

567570defined :: PDecl -> [Name]

568571defined (PFix _ _ _) = []

569−defined (PTy _ _ _ _ n t) = []

572+defined (PTy _ _ _ _ _ n t) = []

570573defined (PPostulate _ _ _ _ n t) = []

571574defined (PClauses _ _ n _) = [n] -- not a declaration

572575defined (PCAF _ n _) = [n]

573−defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

574− where fstt (_, a, _, _, _) = a

575−defined (PData _ _ _ _ (PLaterdecl n _)) = []

576+defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

577+ where fstt (_, _, a, _, _, _) = a

578+defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

576579defined (PParams _ _ ds) = concatMap defined ds

577580defined (PNamespace _ ds) = concatMap defined ds

578581defined (PRecord _ _ _ n _ _ c _) = [n, c]

@@ -687,7 +690,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

687690 | MatchRefine Name

688691 | LetTac Name t | LetTacTy Name t t

689692 | Exact t | Compute | Trivial | TCInstance

690− | ProofSearch (Maybe Name) Name [Name]

693+ | ProofSearch (Maybe Name) [Name]

691694 | Solve

692695 | Attack

693696 | ProofState | ProofTerm | Undo

@@ -759,22 +762,18 @@ type PDo = PDo' PTerm

759762data PArg' t = PImp { priority :: Int,

760763 machine_inf :: Bool, -- true if the machine inferred it

761764 argopts :: [ArgOpt],

762− pname :: Name, getTm :: t,

763− pargdoc :: String }

765+ pname :: Name, getTm :: t }

764766 | PExp { priority :: Int,

765767 argopts :: [ArgOpt],

766− getTm :: t,

767− pargdoc :: String }

768+ getTm :: t }

768769 | PConstraint { priority :: Int,

769770 argopts :: [ArgOpt],

770− getTm :: t,

771− pargdoc :: String }

771+ getTm :: t }

772772 | PTacImplicit { priority :: Int,

773773 argopts :: [ArgOpt],

774774 pname :: Name,

775775 getScript :: t,

776− getTm :: t,

777− pargdoc :: String }

776+ getTm :: t }

778777 deriving (Show, Eq, Functor)

779778

780779data ArgOpt = Lazy | HideDisplay

@@ -784,20 +783,20 @@ lazyarg :: PArg' t -> Bool

784783lazyarg tm = Lazy `elem` argopts tm

785784

786785instance Sized a => Sized (PArg' a) where

787− size (PImp p _ l nm trm _) = 1 + size nm + size trm

788− size (PExp p l trm _) = 1 + size trm

789− size (PConstraint p l trm _) = 1 + size trm

790− size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm

786+ size (PImp p _ l nm trm) = 1 + size nm + size trm

787+ size (PExp p l trm) = 1 + size trm

788+ size (PConstraint p l trm) = 1 + size trm

789+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

791790

792791{-!

793792deriving instance Binary PArg'

794793deriving instance NFData PArg'

795794!-}

796795

797−pimp n t mach = PImp 1 mach [Lazy] n t ""

798−pexp t = PExp 1 [] t ""

799−pconst t = PConstraint 1 [] t ""

800−ptacimp n s t = PTacImplicit 2 [Lazy] n s t ""

796+pimp n t mach = PImp 1 mach [Lazy] n t

797+pexp t = PExp 1 [] t

798+pconst t = PConstraint 1 [] t

799+ptacimp n s t = PTacImplicit 2 [Lazy] n s t

801800

802801type PArg = PArg' PTerm

803802

@@ -949,9 +948,9 @@ inferTy = sMN 0 "__Infer"

949948inferCon = sMN 0 "__infer"

950949inferDecl = PDatadecl inferTy

951950 PType

952− [("", inferCon, PPi impl (sMN 0 "iType") PType (

953− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

954− (PRef bi inferTy)), bi, [])]

951+ [("", [], inferCon, PPi impl (sMN 0 "iType") PType (

952+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

953+ (PRef bi inferTy)), bi, [])]

955954inferOpts = []

956955

957956infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

@@ -979,7 +978,7 @@ primNames = [unitTy, unitCon,

979978unitTy = sMN 0 "__Unit"

980979unitCon = sMN 0 "__II"

981980unitDecl = PDatadecl unitTy PType

982− [("", unitCon, PRef bi unitTy, bi, [])]

981+ [("", [], unitCon, PRef bi unitTy, bi, [])]

983982unitOpts = [DefaultEliminator]

984983

985984falseTy = sMN 0 "__False"

@@ -989,12 +988,12 @@ falseOpts = []

989988pairTy = sMN 0 "__Pair"

990989pairCon = sMN 0 "__MkPair"

991990pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

992− [("", pairCon, PPi impl (n "A") PType (

993− PPi impl (n "B") PType (

994− PPi expl (n "a") (PRef bi (n "A")) (

995− PPi expl (n "b") (PRef bi (n "B"))

996− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

997− pexp (PRef bi (n "B"))])))), bi, [])]

991+ [("", [], pairCon, PPi impl (n "A") PType (

992+ PPi impl (n "B") PType (

993+ PPi expl (n "a") (PRef bi (n "A")) (

994+ PPi expl (n "b") (PRef bi (n "B"))

995+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

996+ pexp (PRef bi (n "B"))])))), bi, [])]

998997 where n a = sMN 0 a

999998pairOpts = []

1000999

@@ -1003,12 +1002,12 @@ eqCon = sUN "refl"

10031002eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

10041003 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

10051004 PType)

1006− [("", eqCon, PPi impl (n "A") PType (

1007− PPi impl (n "x") (PRef bi (n "A"))

1008− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1009− pimp (n "B") Placeholder False,

1010− pexp (PRef bi (n "x")),

1011− pexp (PRef bi (n "x"))])), bi, [])]

1005+ [("", [], eqCon, PPi impl (n "A") PType (

1006+ PPi impl (n "x") (PRef bi (n "A"))

1007+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1008+ pimp (n "B") Placeholder False,

1009+ pexp (PRef bi (n "x")),

1010+ pexp (PRef bi (n "x"))])), bi, [])]

10121011 where n a = sMN 0 a

10131012eqOpts = []

10141013

@@ -1016,8 +1015,8 @@ elimName = sUN "__Elim"

10161015elimMethElimTy = sUN "__elimTy"

10171016elimMethElim = sUN "elim"

10181017elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1019− [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

1020− PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1018+ [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1019+ PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

10211020

10221021-- Defined in builtins.idr

10231022sigmaTy = sUN "Exists"

@@ -1101,7 +1100,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

11011100 text "let" <+> bindingOf n False <+> text "=" </>

11021101 prettySe 10 bnd v <+> text "in" </>

11031102 prettySe 10 ((n, False):bnd) sc

1104− prettySe p bnd (PPi (Exp l s _ _) n ty sc)

1103+ prettySe p bnd (PPi (Exp l s _) n ty sc)

11051104 | n `elem` allNamesIn sc || impl =

11061105 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

11071106 bracket p 2 . group $

@@ -1115,7 +1114,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

11151114 case s of

11161115 Static -> text "[static]" <> space

11171116 _ -> empty

1118− prettySe p bnd (PPi (Imp l s _ _) n ty sc)

1117+ prettySe p bnd (PPi (Imp l s _) n ty sc)

11191118 | impl =

11201119 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

11211120 bracket p 2 $

@@ -1127,10 +1126,10 @@ pprintPTerm impl bnd = prettySe 10 bnd

11271126 case s of

11281127 Static -> text "[static]" <> space

11291128 _ -> empty

1130− prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1129+ prettySe p bnd (PPi (Constraint _ _) n ty sc) =

11311130 bracket p 2 $

11321131 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1133− prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =

1132+ prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

11341133 bracket p 2 $

11351134 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

11361135 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

@@ -1247,10 +1246,10 @@ pprintPTerm impl bnd = prettySe 10 bnd

12471246

12481247 prettySe p bnd _ = text "test"

12491248

1250− prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)

1251− prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm

1252− prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm

1253− prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)

1249+ prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1250+ prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm

1251+ prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm

1252+ prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

12541253

12551254 prettyArgSe bnd arg = prettySe 0 bnd arg

12561255 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

@@ -1346,16 +1345,16 @@ showCImp impl (PWith _ n l ws r w)

13461345showDImp :: Bool -> PData -> Doc OutputAnnotation

13471346showDImp impl (PDatadecl n ty cons)

13481347 = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1349− (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1348+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

13501349

13511350showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

13521351showDecls i ds = vsep (map (showDeclImp i) ds)

13531352

13541353showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1355−showDeclImp i (PTy _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

1354+showDeclImp i (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

13561355showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

13571356 indent 2 (vsep (map (showCImp i) cs))

1358−showDeclImp _ (PData _ _ _ _ d) = showDImp True d

1357+showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

13591358showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

13601359showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

13611360showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

@@ -1371,17 +1370,17 @@ instance Show (Doc OutputAnnotation) where

13711370

13721371getImps :: [PArg] -> [(Name, PTerm)]

13731372getImps [] = []

1374−getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

1373+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs

13751374getImps (_ : xs) = getImps xs

13761375

13771376getExps :: [PArg] -> [PTerm]

13781377getExps [] = []

1379−getExps (PExp _ _ tm _ : xs) = tm : getExps xs

1378+getExps (PExp _ _ tm : xs) = tm : getExps xs

13801379getExps (_ : xs) = getExps xs

13811380

13821381getConsts :: [PArg] -> [PTerm]

13831382getConsts [] = []

1384−getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

1383+getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

13851384getConsts (_ : xs) = getConsts xs

13861385

13871386getAll :: [PArg] -> [PTerm]

src/Idris/CaseSplit.hs+4−4

@@ -150,7 +150,7 @@ mergePat ist (PApp _ _ args) (PApp fc f args') t

150150 where mergeArg x (y, t)

151151 = do tm' <- mergePat ist (getTm x) (getTm y) t

152152 case x of

153− (PImp _ _ _ _ _ _) ->

153+ (PImp _ _ _ _ _) ->

154154 return (y { machine_inf = machine_inf x,

155155 getTm = tm' })

156156 _ -> return (y { getTm = tm' })

@@ -318,14 +318,14 @@ getClause l fn fp = do ty <- getInternalApp fp l

318318 let ap = mkApp ist ty []

319319 return (show fn ++ " " ++ ap ++

320320 "= ?" ++ show fn ++ "_rhs")

321− where mkApp i (PPi (Exp _ _ _ False) (MN _ _) ty sc) used

321+ where mkApp i (PPi (Exp _ _ False) (MN _ _) ty sc) used

322322 = let n = getNameFrom i used ty in

323323 show n ++ " " ++ mkApp i sc (n : used)

324− mkApp i (PPi (Exp _ _ _ False) (UN n) ty sc) used

324+ mkApp i (PPi (Exp _ _ False) (UN n) ty sc) used

325325 | thead n == '_'

326326 = let n = getNameFrom i used ty in

327327 show n ++ " " ++ mkApp i sc (n : used)

328− mkApp i (PPi (Exp _ _ _ False) n _ sc) used

328+ mkApp i (PPi (Exp _ _ False) n _ sc) used

329329 = show n ++ " " ++ mkApp i sc (n : used)

330330 mkApp i (PPi _ _ _ sc) used = mkApp i sc used

331331 mkApp i _ _ = ""

src/Idris/Completion.hs+1−1

@@ -50,7 +50,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

5050 , (":e", Just ExprTArg)

5151 , (":eval", Just ExprTArg)

5252 ] ++ map (\x -> (x, Nothing)) [

53− "intros", "compute", "trivial", "solve", "attack",

53+ "intros", "compute", "trivial", "search", "solve", "attack",

5454 "state", "term", "undo", "qed", "abandon", ":q"

5555 ]

5656tactics = map fst tacticArgs

src/Idris/Core/DeepSeq.hs+1

@@ -19,6 +19,7 @@ instance NFData SpecialName where

1919 rnf (MethodN x1) = rnf x1 `seq` ()

2020 rnf (CaseN x1) = rnf x1 `seq` ()

2121 rnf (ElimN x1) = rnf x1 `seq` ()

22+ rnf (InstanceCtorN x1) = rnf x1 `seq` ()

2223

2324instance NFData Raw where

2425 rnf (Var x1) = rnf x1 `seq` ()

src/Idris/Core/Evaluate.hs+4−3

@@ -520,12 +520,13 @@ wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b

520520wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)

521521wknV i t = return t

522522

523−convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])

523+convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

524524

525−convEq :: Context -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

526−convEq ctxt = ceq [] where

525+convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

526+convEq ctxt holes = ceq [] where

527527 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

528528 ceq ps (P xt x _) (P yt y _)

529+ | x `elem` holes || y `elem` holes = return True

529530 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

530531 | otherwise = sameDefs ps x y

531532 ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y

src/Idris/Core/Execute.hs+7

@@ -320,6 +320,13 @@ execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

320320 = let res = ioWrap . EConstant . I $ 0

321321 in execApp' env ctxt res (tail rest)

322322

323+-- Right now, there's no way to send command-line arguments to the executor,

324+-- so just return 0.

325+execApp' env ctxt (EP _ fp _) (_:fn:rest)

326+ | fp == mkfprim,

327+ Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

328+ = let res = ioWrap . EConstant . I $ 0

329+ in execApp' env ctxt res (tail rest)

323330-- Throw away the 'World' argument to the foreign function

324331

325332execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

src/Idris/Core/ProofState.hs+10−6

@@ -805,7 +805,7 @@ updateProblems ctxt ns ps inj holes = up ns ps where

805805 (ns', (x',y',env',err', um) : ps')

806806

807807-- attempt to solve remaining problems with match_unify

808−matchProblems all ctxt ps inj holes = up [] ps where

808+matchProblems all ns ctxt ps inj holes = up ns ps where

809809 up ns [] = (ns, [])

810810 up ns ((x, y, env, err, um) : ps)

811811 | all || um == Match =

@@ -860,15 +860,19 @@ processTactic UnifyProblems ps

860860 notunified = updateNotunified ns' (notunified ps),

861861 holes = holes ps \\ (map fst ns') }, plog ps)

862862processTactic (MatchProblems all) ps

863− = let (ns', probs') = matchProblems all (context ps)

863+ = let (ns', probs') = matchProblems all [] (context ps)

864864 (problems ps)

865865 (injective ps)

866866 (holes ps)

867− pterm' = updateSolved ns' (pterm ps) in

868− return (ps { pterm = pterm', solved = Nothing, problems = probs',

867+ (ns'', probs'') = matchProblems all ns' (context ps)

868+ probs'

869+ (injective ps)

870+ (holes ps)

871+ pterm' = updateSolved ns'' (pterm ps) in

872+ return (ps { pterm = pterm', solved = Nothing, problems = probs'',

869873 previous = Just ps, plog = "",

870− notunified = updateNotunified ns' (notunified ps),

871− holes = holes ps \\ (map fst ns') }, plog ps)

874+ notunified = updateNotunified ns'' (notunified ps),

875+ holes = holes ps \\ (map fst ns'') }, plog ps)

872876processTactic t ps

873877 = case holes ps of

874878 [] -> fail "Nothing to fill in."

src/Idris/Core/TT.hs+5−1

@@ -279,6 +279,7 @@ data SpecialName = WhereN Int Name Name

279279 | MethodN Name

280280 | CaseN Name

281281 | ElimN Name

282+ | InstanceCtorN Name

282283 deriving (Eq, Ord)

283284{-!

284285deriving instance Binary SpecialName

@@ -322,6 +323,7 @@ instance Show SpecialName where

322323 show (ParentN p c) = show p ++ "#" ++ T.unpack c

323324 show (CaseN n) = "case block in " ++ show n

324325 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

326+ show (InstanceCtorN n) = "constructor of " ++ show n

325327

326328-- Show a name in a way decorated for code generation, not human reading

327329showCG :: Name -> String

@@ -475,7 +477,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

475477 | B8V (Vector Word8) | B16V (Vector Word16)

476478 | B32V (Vector Word32) | B64V (Vector Word64)

477479 | AType ArithTy | StrType

478− | PtrType | BufferType | VoidType | Forgot

479481 deriving (Eq, Ord)

480482{-!

481483deriving instance Binary Const

@@ -495,6 +497,7 @@ instance Pretty Const OutputAnnotation where

495497 pretty StrType = text "String"

496498 pretty BufferType = text "prim__UnsafeBuffer"

497499 pretty PtrType = text "Ptr"

500+ pretty ManagedPtrType = text "Ptr"

498501 pretty VoidType = text "Void"

499502 pretty Forgot = text "Forgot"

500503 pretty (B8 w) = text . show $ w

@@ -1041,6 +1044,7 @@ instance Show Const where

10411044 show StrType = "String"

10421045 show BufferType = "prim__UnsafeBuffer"

10431046 show PtrType = "Ptr"

1047+ show ManagedPtrType = "ManagedPtr"

10441048 show VoidType = "Void"

10451049

10461050showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String

src/Idris/Core/Typecheck.hs+11−6

@@ -16,11 +16,12 @@ import Idris.Core.Evaluate

1616-- indexed with 'finalise'

1717

1818convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()

19−convertsC ctxt env x y

20− = do c1 <- convEq ctxt x y

19+convertsC ctxt env x y =

20+ do let hs = map fst (filter isHole env)

21+ c1 <- convEq ctxt hs x y

2122 if c1 then return ()

2223 else

23− do c2 <- convEq ctxt (finalise (normalise ctxt env x))

24+ do c2 <- convEq ctxt hs (finalise (normalise ctxt env x))

2425 (finalise (normalise ctxt env y))

2526 if c2 then return ()

2627 else lift $ tfail (CantConvert

@@ -29,15 +30,19 @@ convertsC ctxt env x y

2930

3031converts :: Context -> Env -> Term -> Term -> TC ()

3132converts ctxt env x y

32− = case convEq' ctxt x y of

33+ = let hs = map fst (filter isHole env) in

34+ case convEq' ctxt hs x y of

3335 OK True -> return ()

34− _ -> case convEq' ctxt (finalise (normalise ctxt env x))

35− (finalise (normalise ctxt env y)) of

36+ _ -> case convEq' ctxt hs (finalise (normalise ctxt env x))

37+ (finalise (normalise ctxt env y)) of

3638 OK True -> return ()

3739 _ -> tfail (CantConvert

3840 (finalise (normalise ctxt env x))

3941 (finalise (normalise ctxt env y)) (errEnv env))

4042

43+isHole (n, Hole _) = True

44+isHole _ = False

45+

4146errEnv = map (\(x, b) -> (x, binderTy b))

4247

4348isType :: Context -> Env -> Term -> TC ()

src/Idris/Core/Unify.hs+2−2

@@ -79,7 +79,7 @@ match_unify ctxt env topx topy inj holes =

7979 ha <- un names ax ay

8080 combine names hf ha

8181 un names x y

82− | OK True <- convEq' ctxt x y = do sc 1; return []

82+ | OK True <- convEq' ctxt holes x y = do sc 1; return []

8383 | otherwise = do UI s f <- get

8484 let r = recoverable x y

8585 let err = CantUnify r

@@ -356,7 +356,7 @@ unify ctxt env topx topy inj holes =

356356 sameBinder (Pi _) (Pi _) = True

357357 sameBinder _ _ = False

358358 un' fn bnames x y

359− | OK True <- convEq' ctxt x y = do sc 1; return []

359+ | OK True <- convEq' ctxt holes x y = do sc 1; return []

360360 | otherwise = do UI s f <- get

361361 let r = recoverable x y

362362 let err = CantUnify r

src/Idris/Coverage.hs+2−2

@@ -56,7 +56,7 @@ genClauses fc n xs given

5656 -- there may be more case splitting that the idris_implicits record

5757 -- suggests)

5858 let parg = case lookupCtxt n (idris_implicits i) of

59− (p : _) -> p ++ repeat (PExp 0 [] Placeholder "")

59+ (p : _) -> p ++ repeat (PExp 0 [] Placeholder)

6060 _ -> repeat (pexp Placeholder)

6161 let tryclauses = mkClauses parg all_args

6262 logLvl 2 $ show (length tryclauses) ++ " initially to check"

@@ -187,7 +187,7 @@ genAll i args

187187 _ -> [p]

188188 ops fc n arg o = return Placeholder

189189

190− getExpTm (PImp _ True _ _ _ _) = Placeholder -- machine inferred, no point!

190+ getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!

191191 getExpTm t = getTm t

192192

193193 -- put it back to its original form

src/Idris/DeepSeq.hs+30−24

@@ -57,14 +57,14 @@ instance NFData ArgOpt where

5757 rnf _ = ()

5858

5959instance NFData Plicity where

60− rnf (Imp x1 x2 x3 x4)

61− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

62− rnf (Exp x1 x2 x3 x4)

63− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

64− rnf (Constraint x1 x2 x3)

60+ rnf (Imp x1 x2 x3)

61+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

62+ rnf (Exp x1 x2 x3)

63+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

64+ rnf (Constraint x1 x2)

65+ = rnf x1 `seq` rnf x2 `seq` ()

66+ rnf (TacImp x1 x2 x3)

6567 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

66− rnf (TacImp x1 x2 x3 x4)

67− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

6868

6969instance NFData FnOpt where

7070 rnf Inlinable = ()

@@ -84,18 +84,20 @@ instance NFData DataOpt where

8484

8585instance (NFData t) => NFData (PDecl' t) where

8686 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

87− rnf (PTy x1 x2 x3 x4 x5 x6)

87+ rnf (PTy x1 x2 x3 x4 x5 x6 x7)

8888 = rnf x1 `seq`

89− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

89+ rnf x2 `seq`

90+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

9091 rnf (PPostulate x1 x2 x3 x4 x5 x6)

9192 = rnf x1 `seq`

9293 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

9394 rnf (PClauses x1 x2 x3 x4)

9495 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

9596 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

96− rnf (PData x1 x2 x3 x4 x5)

97+ rnf (PData x1 x2 x3 x4 x5 x6)

9798 = rnf x1 `seq`

98− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

99+ rnf x2 `seq`

100+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

99101 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

100102 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

101103 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

@@ -116,12 +118,17 @@ instance (NFData t) => NFData (PDecl' t) where

116118 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

117119 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

118120 rnf (PDirective x1) = ()

119− rnf (PProvider x1 x2 x3 x4 x5)

121+ rnf (PProvider x1 x2 x3 x4 x5 x6)

120122 = rnf x1 `seq`

121− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

123+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

122124 rnf (PTransform x1 x2 x3 x4)

123125 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

124126

127+instance NFData ProvideWhat where

128+ rnf ProvAny = ()

129+ rnf ProvTerm = ()

130+ rnf ProvPostulate = ()

131+

125132instance NFData PunInfo where

126133 rnf x = x `seq` ()

127134

@@ -200,8 +207,8 @@ instance (NFData t) => NFData (PTactic' t) where

200207 rnf (Exact x1) = rnf x1 `seq` ()

201208 rnf Compute = ()

202209 rnf Trivial = ()

203− rnf (ProofSearch x1 x2 x3)

204− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

210+ rnf (ProofSearch x1 x2)

211+ = rnf x1 `seq` rnf x2 `seq` ()

205212 rnf Solve = ()

206213 rnf Attack = ()

207214 rnf ProofState = ()

@@ -225,16 +232,15 @@ instance (NFData t) => NFData (PDo' t) where

225232 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

226233

227234instance (NFData t) => NFData (PArg' t) where

228− rnf (PImp x1 x2 x3 x4 x5 x6)

229− = rnf x1 `seq`

230− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

231− rnf (PExp x1 x2 x3 x4)

232− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

233− rnf (PConstraint x1 x2 x3 x4)

234− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

235− rnf (PTacImplicit x1 x2 x3 x4 x5 x6)

235+ rnf (PImp x1 x2 x3 x4 x5)

236+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

237+ rnf (PExp x1 x2 x3)

238+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

239+ rnf (PConstraint x1 x2 x3)

240+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

241+ rnf (PTacImplicit x1 x2 x3 x4 x5)

236242 = rnf x1 `seq`

237− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

243+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

238244

239245instance NFData ClassInfo where

240246 rnf (CI x1 x2 x3 x4 x5 x6)

src/Idris/Delaborate.hs+15−10

@@ -56,19 +56,24 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

5656 _ -> PRef un n

5757 de env _ (Bind n (Lam ty) sc)

5858 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

59− de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

60− = PPi impl n (de env [] ty) (de ((n,n):env) is sc)

61− de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)

59+ de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) sc)

60+ = PPi (Imp opts Dynamic False) n (de env [] ty) (de ((n,n):env) is sc)

61+ de env (PConstraint _ _ _:is) (Bind n (Pi ty) sc)

6262 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

63− de env (PTacImplicit _ _ _ tac _ _:is) (Bind n (Pi ty) sc)

63+ de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi ty) sc)

6464 = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

65− de env _ (Bind n (Pi ty) sc)

65+ de env (plic:is) (Bind n (Pi ty) sc)

66+ = PPi (Exp (argopts plic) Dynamic False)

67+ n

68+ (de env [] ty)

69+ (de ((n,n):env) is sc)

70+ de env [] (Bind n (Pi ty) sc)

6671 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

6772 de env _ (Bind n (Let ty val) sc)

6873 = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

6974 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

7075 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

71− de env _ (Bind n _ sc) = de ((n,n):env) [] sc

76+ de env plic (Bind n bb sc) = de ((n,n):env) [] sc

7277 de env _ (Constant i) = PConstant i

7378 de env _ Erased = Placeholder

7479 de env _ Impossible = Placeholder

@@ -112,10 +117,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

112117 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

113118 | otherwise = PApp un (PRef un n) (map pexp args)

114119

115− imp (PImp p m l n _ d) arg = PImp p m l n arg d

116− imp (PExp p l _ d) arg = PExp p l arg d

117− imp (PConstraint p l _ d) arg = PConstraint p l arg d

118− imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

120+ imp (PImp p m l n _) arg = PImp p m l n arg

121+ imp (PExp p l _) arg = PExp p l arg

122+ imp (PConstraint p l _) arg = PConstraint p l arg

123+ imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

119124

120125-- | How far to indent sub-errors

121126errorIndent :: Int

src/Idris/Docs.hs+33−21

@@ -14,15 +14,17 @@ import Data.List

1414-- TODO: Only include names with public/abstract accessibility

1515

1616data FunDoc = FD Name String

17− [(Name, PTerm, Plicity)] -- args: name, ty, plicity

17+ [(Name, PTerm, Plicity, Maybe String)] -- args: name, ty, implicit, docs

1818 PTerm -- function type

1919 (Maybe Fixity)

20+ deriving Show

2021

2122data Docs = FunDoc FunDoc

2223 | DataDoc FunDoc -- type constructor docs

2324 [FunDoc] -- data constructor docs

2425 | ClassDoc Name String -- class docs

2526 [FunDoc] -- method docs

27+ deriving Show

2628

2729showDoc "" = empty

2830showDoc x = text " -- " <> text x

@@ -31,23 +33,32 @@ pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

3133pprintFD imp (FD n doc args ty f)

3234 = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>

3335 maybe empty (\f -> text (show f) <> line) f <>

34− let argshow = mapMaybe showArg args in

36+ let argshow = showArgs args [] in

3537 if not (null argshow)

3638 then nest 4 $ text "Arguments:" <$> vsep argshow

3739 else empty)

3840

39− where showArg (n, ty, arg@(Exp {}))

40− = Just $ bindingOf n False <+> colon <+> prettyImp imp ty <>

41− showDoc (pdocstr arg) <> line

42− showArg (n, ty, arg@(Constraint {}))

43− = Just $ text "Class constraint" <+>

44− prettyImp imp ty <> showDoc (pdocstr arg) <> line

45− showArg (n, ty, arg@(Imp {}))

41+ where showArgs ((n, ty, Exp {}, d):args) bnd

42+ = bindingOf n False <+> colon <+>

43+ pprintPTerm imp bnd ty <>

44+ showDoc (maybe "" id d) <> line

45+ :

46+ showArgs args ((n, False):bnd)

47+ showArgs ((n, ty, Constraint {}, d):args) bnd

48+ = text "Class constraint" <+>

49+ pprintPTerm imp bnd ty <> showDoc (maybe "" id d) <> line

50+ :

51+ showArgs args ((n, True):bnd)

52+ showArgs ((n, ty, Imp {}, d):args) bnd

4653 | not (null doc)

47− = Just $ text "(implicit)" <+>

48− bindingOf n True <+> colon <+> prettyImp imp ty

49− <> showDoc (pdocstr arg) <> line

50− showArg (n, _, _) = Nothing

54+ = text "(implicit)" <+>

55+ bindingOf n True <+> colon <+>

56+ pprintPTerm imp bnd ty <>

57+ showDoc (maybe "" id d) <> line

58+ :

59+ showArgs args ((n, True):bnd)

60+ showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

61+ showArgs [] _ = []

5162

5263

5364

@@ -81,7 +92,7 @@ docClass :: Name -> ClassInfo -> Idris Docs

8192docClass n ci

8293 = do i <- getIState

8394 let docstr = case lookupCtxt n (idris_docstrings i) of

84− [str] -> str

95+ [str] -> fst str

8596 _ -> ""

8697 mdocs <- mapM docFun (map fst (class_methods ci))

8798 return (ClassDoc n docstr mdocs)

@@ -89,11 +100,11 @@ docClass n ci

89100docFun :: Name -> Idris FunDoc

90101docFun n

91102 = do i <- getIState

92− let docstr = case lookupCtxt n (idris_docstrings i) of

93− [str] -> str

94− _ -> ""

103+ let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of

104+ [d] -> d

105+ _ -> ("", [])

95106 let ty = delabTy i n

96− let args = getPArgNames ty

107+ let args = getPArgNames ty argDocs

97108 let infixes = idris_infixes i

98109 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes

99110 let f = case fixdecls of

@@ -105,6 +116,7 @@ docFun n

105116 funName (UN n) = str n

106117 funName (NS n _) = funName n

107118

108−getPArgNames :: PTerm -> [(Name, PTerm, Plicity)]

109−getPArgNames (PPi plicity name ty body) = ((name, ty, plicity) : getPArgNames body)

110−getPArgNames _ = []

119+getPArgNames :: PTerm -> [(Name, String)] -> [(Name, PTerm, Plicity, Maybe String)]

120+getPArgNames (PPi plicity name ty body) ds =

121+ (name, ty, plicity, lookup name ds) : getPArgNames body ds

122+getPArgNames _ _ = []

src/Idris/ElabDecls.hs+109−84

@@ -63,15 +63,15 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

6363-- return (n, (i, top, t'))) ns

6464

6565-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

66−elabType :: ElabInfo -> SyntaxInfo -> String ->

66+elabType :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

6767 FC -> FnOpts -> Name -> PTerm -> Idris Type

6868elabType = elabType' False

6969

7070elabType' :: Bool -> -- normalise it

71− ElabInfo -> SyntaxInfo -> String ->

71+ ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

7272 FC -> FnOpts -> Name -> PTerm -> Idris Type

73−elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

74− n = liftname info n_in in -}

73+elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

74+ n = liftname info n_in in -}

7575 do checkUndefined fc n

7676 ctxt <- getContext

7777 i <- getIState

@@ -122,7 +122,8 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

122122 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

123123 addDeferred ds'

124124 setFlags n opts'

125− addDocStr n doc

125+ checkDocs fc argDocs ty

126+ addDocStr n doc argDocs

126127 addIBC (IBCDoc n)

127128 addIBC (IBCFlags n opts')

128129 when (Implicit `elem` opts) $ do addCoercion n

@@ -167,13 +168,13 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

167168 , ns2 == map txt ["Maybe", "Prelude"]

168169 , ns3 == map txt ["List", "Prelude"]

169170 , ns4 == map txt ["Errors","Reflection","Language"] = True

170− tyIsHandler _ = False

171+ tyIsHandler _ = False

171172

172173

173174elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

174175 FC -> FnOpts -> Name -> PTerm -> Idris ()

175176elabPostulate info syn doc fc opts n ty

176− = do elabType info syn doc fc opts n ty

177+ = do elabType info syn doc [] fc opts n ty

177178 -- make sure it's collapsible, so it is never needed at run time

178179 -- start by getting the elaborated type

179180 ctxt <- getContext

@@ -194,8 +195,8 @@ elabPostulate info syn doc fc opts n ty

194195 -- remove it from the deferred definitions list

195196 solveDeferred n

196197

197−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()

198−elabData info syn doc fc opts (PLaterdecl n t_in)

198+elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()

199+elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

199200 = do let codata = Codata `elem` opts

200201 iLOG (show (fc, doc))

201202 checkUndefined fc n

@@ -213,7 +214,7 @@ elabData info syn doc fc opts (PLaterdecl n t_in)

213214 logLvl 2 $ "---> " ++ show cty

214215 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

215216

216−elabData info syn doc fc opts (PDatadecl n t_in dcons)

217+elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

217218 = do let codata = Codata `elem` opts

218219 iLOG (show fc)

219220 undef <- isUndefined fc n

@@ -241,12 +242,13 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

241242 let as = map (const Nothing) (getArgTys cty)

242243 let params = findParams (map snd cons)

243244 logLvl 2 $ "Parameters : " ++ show params

244− putIState (i { idris_datatypes =

245+ putIState (i { idris_datatypes =

245246 addDef n (TI (map fst cons) codata opts params)

246247 (idris_datatypes i) })

247248 addIBC (IBCDef n)

248249 addIBC (IBCData n)

249− addDocStr n doc

250+ checkDocs fc argDocs t_in

251+ addDocStr n doc argDocs

250252 addIBC (IBCDoc n)

251253 let metainf = DataMI params

252254 addIBC (IBCMetaInformation n metainf)

@@ -258,10 +260,10 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

258260 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

259261 else return ()

260262 where

261− checkDefinedAs fc n t ctxt

263+ checkDefinedAs fc n t ctxt

262264 = case lookupDef n ctxt of

263265 [] -> return ()

264− [TyDecl _ ty] ->

266+ [TyDecl _ ty] ->

265267 case converts ctxt [] t ty of

266268 OK () -> return ()

267269 _ -> tclift $ tfail (At fc (AlreadyDefined n))

@@ -319,7 +321,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

319321type EliminatorState = StateT (Map.Map String Int) Idris

320322

321323-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

322−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->

324+elabEliminator :: [Int] -> Name -> PTerm ->

325+ [(String, [(Name, String)], Name, PTerm, FC, [Name])] ->

323326 ElabInfo -> EliminatorState ()

324327elabEliminator paramPos n ty cons info = do

325328 elimLog $ "Elaborating eliminator"

@@ -328,15 +331,15 @@ elabEliminator paramPos n ty cons info = do

328331 generalParams <- namePis False pms

329332 motiveIdxs <- namePis False idxs

330333 let motive = mkMotive n paramPos generalParams motiveIdxs

331− consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do

332− name <- freshName $ "elim_" ++ simpleName cnm

333− consTerm <- extractConsTerm c generalParams

334− return (name, expl, consTerm)) cons

334+ consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do

335+ name <- freshName $ "elim_" ++ simpleName cnm

336+ consTerm <- extractConsTerm c generalParams

337+ return (name, expl, consTerm)) cons

335338 scrutineeIdxs <- namePis False idxs

336339 let motiveConstr = [(motiveName, expl, motive)]

337340 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

338341 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

339− let eliminatorTyDecl = PTy (show n) defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

342+ let eliminatorTyDecl = PTy (show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

340343 let clauseConsElimArgs = map getPiName consTerms

341344 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

342345 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

@@ -500,8 +503,8 @@ elabEliminator paramPos n ty cons info = do

500503 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

501504 _ -> return implargs

502505

503− extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

504− extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do

506+ extractConsTerm :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

507+ extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

505508 let cons' = replaceParams paramPos generalParameters ty

506509 let (args, resTy) = splitPi cons'

507510 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

@@ -536,8 +539,8 @@ elabEliminator paramPos n ty cons info = do

536539 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

537540 convertImplPi _ = Nothing

538541

539− generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

540− generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

542+ generateEliminatorClauses :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

543+ generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

541544 let cons' = replaceParams paramPos generalParameters ty

542545 let (args, resTy) = splitPi cons'

543546 i <- State.lift getIState

@@ -558,7 +561,7 @@ elabEliminator paramPos n ty cons info = do

558561

559562elabPrims :: Idris ()

560563elabPrims = do mapM_ (elabDecl EAll toplevel)

561− (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)

564+ (map (\(opt, decl) -> PData "" [] defaultSyntax (fileFC "builtin") opt decl)

562565 (zip

563566 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

564567 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

@@ -626,8 +629,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

626629

627630

628631-- | Elaborate a type provider

629−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

630−elabProvider info syn fc n ty tm

632+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()

633+elabProvider info syn fc what n ty tm

631634 = do i <- getIState

632635 -- Ensure that the experimental extension is enabled

633636 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -647,9 +650,6 @@ elabProvider info syn fc n ty tm

647650 ifail $ "Expected provider type IO (Provider (" ++

648651 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

649652

650− -- Create the top-level type declaration

651− elabType info syn "" fc [] n ty

652−

653653 -- Execute the type provider and normalise the result

654654 -- use 'run__provider' to convert to a primitive IO action

655655

@@ -658,12 +658,25 @@ elabProvider info syn fc n ty tm

658658 let rhs' = normalise ctxt [] rhs

659659 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

660660

661− -- Extract the provided term from the type provider

662− tm <- getProvided fc rhs'

663−

664− -- Finally add a top-level definition of the provided term

665− elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

666− logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

661+ -- Extract the provided term or postulate from the type provider

662+ provided <- getProvided fc rhs'

663+

664+ case provided of

665+ Provide tm

666+ | what `elem` [ProvTerm, ProvAny] ->

667+ do -- Finally add a top-level definition of the provided term

668+ elabType info syn "" [] fc [] n ty

669+ elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

670+ logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

671+ | otherwise ->

672+ ierror . Msg $ "Attempted to provide a term where a postulate was expected."

673+ Postulate

674+ | what `elem` [ProvPostulate, ProvAny] ->

675+ do -- Add the postulate

676+ elabPostulate info syn "Provided postulate" fc [] n ty

677+ logLvl 1 $ "Elaborated provided postulate " ++ show n

678+ | otherwise ->

679+ ierror . Msg $ "Attempted to provide a postulate where a term was expected."

667680

668681 where isTType :: TT Name -> Bool

669682 isTType (TType _) = True

@@ -714,7 +727,7 @@ elabTransform info fc safe lhs_in rhs_in

714727elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

715728 PTerm -> String -> Name -> PTerm -> Idris ()

716729elabRecord info syn doc fc tyn ty cdoc cn cty

717− = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc, [])])

730+ = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

718731 cty' <- implicit syn cn cty

719732 i <- getIState

720733 cty <- case lookupTy cn (tt_ctxt i) of

@@ -737,7 +750,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

737750 where

738751-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

739752

740− isNonImp (PExp _ _ _ _, a) = Just a

753+ isNonImp (PExp _ _ _, a) = Just a

741754 isNonImp _ = Nothing

742755

743756 tryElabDecl info (fn, ty, val)

@@ -749,15 +762,15 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

749762 show fn ++ " (" ++ show ty ++ ")"

750763 putIState i)

751764

752− getImplB k (PPi (Imp l s _ _) n Placeholder sc)

765+ getImplB k (PPi (Imp l s _) n Placeholder sc)

753766 = getImplB k sc

754− getImplB k (PPi (Imp l s d p) n ty sc)

755− = getImplB (\x -> k (PPi (Imp l s d p) n ty x)) sc

767+ getImplB k (PPi (Imp l s p) n ty sc)

768+ = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc

756769 getImplB k (PPi _ n ty sc)

757770 = getImplB k sc

758771 getImplB k _ = k

759772

760− renameBs (PImp _ _ _ _ _ _ : ps) (PPi p n ty s)

773+ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)

761774 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

762775 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

763776 renameBs _ t = t

@@ -784,7 +797,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

784797

785798 mkProj recty substs cimp ((pn_in, pty), pos)

786799 = do let pn = expandNS syn pn_in

787− let pfnTy = PTy "" defaultSyntax fc [] pn

800+ let pfnTy = PTy "" [] defaultSyntax fc [] pn

788801 (PPi expl rec recty

789802 (substMatches substs pty))

790803 let pls = repeat Placeholder

@@ -805,7 +818,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

805818 let valname = sMN 0 "updateval"

806819 let pt = k (PPi expl pn pty

807820 (PPi expl rec recty recty))

808− let pfnTy = PTy "" defaultSyntax fc [] setname pt

821+ let pfnTy = PTy "" [] defaultSyntax fc [] setname pt

809822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

810823 let lhsArgs = pls

811824 let rhsArgs = take pos pls ++ (PRef fc valname) :

@@ -821,8 +834,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

821834 return (pn, pfnTy, PClauses fc [] setname [pclause])

822835

823836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

824− (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)

825−elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

837+ (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

838+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

826839 = do checkUndefined fc n

827840 ctxt <- getContext

828841 i <- getIState

@@ -843,7 +856,8 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

843856 tyIs cty'

844857 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

845858 addIBC (IBCDef n)

846− addDocStr n doc

859+ checkDocs fc argDocs t_in

860+ addDocStr n doc argDocs

847861 addIBC (IBCDoc n)

848862 let fs = map (getNamePos 0 t) forcenames

849863 -- FIXME: 'forcenames' is an almighty hack! Need a better way of

@@ -1148,7 +1162,7 @@ elabPE info fc caller r =

11481162 (map (\ (lhs, rhs) ->

11491163 (showTmImpls lhs ++ " = " ++

11501164 showTmImpls rhs)) pats)

1151− elabType info defaultSyntax "" fc opts newnm specTy

1165+ elabType info defaultSyntax "" [] fc opts newnm specTy

11521166 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

11531167 elabClauses info fc opts newnm def

11541168 logLvl 1 $ "Specialised " ++ show newnm)

@@ -1266,7 +1280,7 @@ checkPossible info fc tcgen fname lhs_in

12661280 ((P _ x _, _), (P _ y _, _)) -> x == y

12671281 _ -> False

12681282

1269−getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1283+getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)

12701284 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

12711285getFixedInType i env (_ : is) (Bind n (Pi t) sc)

12721286 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

@@ -1490,7 +1504,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

14901504-- = NS (UN ('#':show x)) [show cnum, show fname]

14911505

14921506 sepBlocks bs = sepBlocks' [] bs where

1493− sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)

1507+ sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)

14941508 = let (bf, af) = sepBlocks' (n : ns) bs in

14951509 (d : bf, af)

14961510 sepBlocks' ns (d@(PClauses _ _ n _) : bs)

@@ -1711,7 +1725,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->

17111725 FC -> [PTerm] ->

17121726 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

17131727elabClass info syn doc fc constraints tn ps ds

1714− = do let cn = sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

1728+ = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

17151729 let tty = pibind ps PType

17161730 let constraint = PApp fc (PRef fc tn)

17171731 (map (pexp . PRef fc) (map fst ps))

@@ -1734,10 +1748,10 @@ elabClass info syn doc fc constraints tn ps ds

17341748 let cty = impbind ps $ conbind constraints

17351749 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

17361750 constraint

1737− let cons = [("", cn, cty, fc, [])]

1751+ let cons = [("", [], cn, cty, fc, [])]

17381752 let ddecl = PDatadecl tn tty cons

17391753 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1740− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl

1754+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl

17411755 -- for each constraint, build a top level function to chase it

17421756 logLvl 5 $ "Building functions"

17431757 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -1775,8 +1789,8 @@ elabClass info syn doc fc constraints tn ps ds

17751789 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

17761790 conbind [] x = x

17771791

1778− getMName (PTy _ _ _ _ n _) = nsroot n

1779− tdecl allmeths (PTy doc syn _ o n t)

1792+ getMName (PTy _ _ _ _ _ n _) = nsroot n

1793+ tdecl allmeths (PTy doc _ syn _ o n t)

17801794 = do t' <- implicit' syn allmeths n t

17811795 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

17821796 return ( (n, (toExp (map fst ps) Exp t')),

@@ -1789,7 +1803,7 @@ elabClass info syn doc fc constraints tn ps ds

17891803 case lookup n mtys of

17901804 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

17911805 let ds = map (decorateid defaultdec)

1792− [PTy "" syn fc [] n ty',

1806+ [PTy "" [] syn fc [] n ty',

17931807 PClauses fc (o ++ opts) n cs]

17941808 iLOG (show ds)

17951809 return (n, ((defaultdec n, ds!!1), ds))

@@ -1799,7 +1813,7 @@ elabClass info syn doc fc constraints tn ps ds

17991813 defaultdec (UN n) = sUN ("default#" ++ str n)

18001814 defaultdec (NS n ns) = NS (defaultdec n) ns

18011815

1802− tydecl (PTy _ _ _ _ _ _) = True

1816+ tydecl (PTy _ _ _ _ _ _ _) = True

18031817 tydecl _ = False

18041818 instdecl (PInstance _ _ _ _ _ _ _ _) = True

18051819 instdecl _ = False

@@ -1827,7 +1841,7 @@ elabClass info syn doc fc constraints tn ps ds

18271841 addInstance False conn' cfn

18281842 addIBC (IBCInstance False conn' cfn)

18291843-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1830− return [PTy "" syn fc [] cfn ty,

1844+ return [PTy "" [] syn fc [] cfn ty,

18311845 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

18321846

18331847 -- Generate a top level function which looks up a method in a given

@@ -1843,12 +1857,12 @@ elabClass info syn doc fc constraints tn ps ds

18431857 iLOG (showTmImpls ty)

18441858 iLOG (show (m, ty', capp, margs))

18451859 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1846− return [PTy doc syn fc o m ty',

1860+ return [PTy doc [] syn fc o m ty',

18471861 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

18481862

1849− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

1850− getMArgs (PPi (Exp _ _ _ _) n ty sc) = EA : getMArgs sc

1851− getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc

1863+ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

1864+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

1865+ getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

18521866 getMArgs _ = []

18531867

18541868 getMeth (m:ms) (a:as) x | x == a = PRef fc m

@@ -1864,14 +1878,14 @@ elabClass info syn doc fc constraints tn ps ds

18641878 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

18651879 rhsArgs [] _ = []

18661880

1867− insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

1881+ insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

18681882 = PPi p n ty (insertConstraint c sc)

18691883 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc

18701884

18711885 -- make arguments explicit and don't bind class parameters

1872− toExp ns e (PPi (Imp l s _ p) n ty sc)

1886+ toExp ns e (PPi (Imp l s p) n ty sc)

18731887 | n `elem` ns = toExp ns e sc

1874− | otherwise = PPi (e l s "" p) n ty (toExp ns e sc)

1888+ | otherwise = PPi (e l s p) n ty (toExp ns e sc)

18751889 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

18761890 toExp ns e sc = sc

18771891

@@ -1891,7 +1905,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

18911905 let constraint = PApp fc (PRef fc n) (map pexp ps)

18921906 let iname = mkiname n ps expn

18931907 when (what /= EDefns) $ do

1894− nty <- elabType' True info syn "" fc [] iname t

1908+ nty <- elabType' True info syn "" [] fc [] iname t

18951909 -- if the instance type matches any of the instances we have already,

18961910 -- and it's not a named instance, then it's overlapping, so report an error

18971911 case expn of

@@ -1999,17 +2013,17 @@ elabInstance info syn what fc cs n ps t expn ds = do

19992013

20002014 mkMethApp (n, _, _, ty)

20012015 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

2002− lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'

2016+ lamBind i (PPi (Constraint _ _) _ _ sc) sc'

20032017 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

20042018 lamBind i (PPi _ n ty sc) sc'

20052019 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

20062020 lamBind i _ sc = sc

2007− methArgs i (PPi (Imp _ _ _ _) n ty sc)

2008− = PImp 0 True [] n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

2009− methArgs i (PPi (Exp _ _ _ _) n ty sc)

2010− = PExp 0 [] (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

2011− methArgs i (PPi (Constraint _ _ _) n ty sc)

2012− = PConstraint 0 [] (PResolveTC fc) "" : methArgs (i+1) sc

2021+ methArgs i (PPi (Imp _ _ _) n ty sc)

2022+ = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2023+ methArgs i (PPi (Exp _ _ _) n ty sc)

2024+ = PExp 0 [] (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2025+ methArgs i (PPi (Constraint _ _) n ty sc)

2026+ = PConstraint 0 [] (PResolveTC fc) : methArgs (i+1) sc

20132027 methArgs i _ = []

20142028

20152029 papp fc f [] = f

@@ -2028,12 +2042,12 @@ elabInstance info syn what fc cs n ps t expn ds = do

20282042 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

20292043 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

20302044

2031− mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

2045+ mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t

20322046

20332047 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

20342048 conbind [] x = x

20352049

2036− coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

2050+ coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

20372051 coninsert cs sc = conbind cs sc

20382052

20392053 insertDefaults :: IState -> Name ->

@@ -2091,7 +2105,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

20912105 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

20922106-}

20932107

2094−decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t

2108+decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorate n) t

20952109decorateid decorate (PClauses f o n cs)

20962110 = PClauses f o (decorate n) (map dc cs)

20972111 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

@@ -2145,22 +2159,22 @@ elabDecl' _ info (PFix _ _ _)

21452159 = return () -- nothing to elaborate

21462160elabDecl' _ info (PSyntax _ p)

21472161 = return () -- nothing to elaborate

2148−elabDecl' what info (PTy doc s f o n ty)

2162+elabDecl' what info (PTy doc argdocs s f o n ty)

21492163 | what /= EDefns

21502164 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

2151− elabType info s doc f o n ty

2165+ elabType info s doc argdocs f o n ty

21522166 return ()

21532167elabDecl' what info (PPostulate doc s f o n ty)

21542168 | what /= EDefns

21552169 = do iLOG $ "Elaborating postulate " ++ show n ++ show o

21562170 elabPostulate info s doc f o n ty

2157−elabDecl' what info (PData doc s f co d)

2171+elabDecl' what info (PData doc argDocs s f co d)

21582172 | what /= ETypes

21592173 = do iLOG $ "Elaborating " ++ show (d_name d)

2160− elabData info s doc f co d

2174+ elabData info s doc argDocs f co d

21612175 | otherwise

21622176 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

2163− elabData info s doc f co (PLaterdecl (d_name d) (d_tcon d))

2177+ elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_tcon d))

21642178elabDecl' what info d@(PClauses f o n ps)

21652179 | what /= ETypes

21662180 = do iLOG $ "Elaborating clause " ++ show n

@@ -2217,17 +2231,17 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

22172231 elabRecord info s doc f tyn ty cdoc cn cty

22182232 | otherwise

22192233 = do iLOG $ "Elaborating [type of] " ++ show tyn

2220− elabData info s doc f [] (PLaterdecl tyn ty)

2234+ elabData info s doc [] f [] (PLaterdecl tyn ty)

22212235elabDecl' _ info (PDSL n dsl)

22222236 = do i <- getIState

22232237 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

22242238 addIBC (IBCDSL n)

22252239elabDecl' what info (PDirective i)

22262240 | what /= EDefns = i

2227−elabDecl' what info (PProvider syn fc n tp tm)

2241+elabDecl' what info (PProvider syn fc provWhat n tp tm)

22282242 | what /= EDefns

22292243 = do iLOG $ "Elaborating type provider " ++ show n

2230− elabProvider info syn fc n tp tm

2244+ elabProvider info syn fc provWhat n tp tm

22312245elabDecl' what info (PTransform fc safety old new)

22322246 = elabTransform info fc safety old new

22332247elabDecl' _ _ _ = return () -- skipped this time

@@ -2272,3 +2286,14 @@ inferredDiff fc inf user =

22722286 Right vs -> return False

22732287 Left (x, y) -> return True

22742288

2289+-- | Check a PTerm against documentation and ensure that every documented

2290+-- argument actually exists. This must be run _after_ implicits have been

2291+-- found, or it will give spurious errors.

2292+checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()

2293+checkDocs fc args tm = cd (Map.fromList args) tm

2294+ where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc

2295+ cd as _ | Map.null as = return ()

2296+ | otherwise = ierror . At fc . Msg $

2297+ "There is documentation for argument(s) "

2298+ ++ (concat . intersperse ", " . map show . Map.keys) as

2299+ ++ " but they were not found."

src/Idris/ElabTerm.hs+23−20

@@ -153,10 +153,9 @@ elab ist info pattern opts fn tm

153153 [] -> return ()

154154

155155 elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()

156− elabE ina t = {- do g <- goal

157− tm <- get_term

158− trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

159− $ -}

156+ elabE ina t =

157+-- do g <- goal

158+-- trace ("Elaborating " ++ show t ++ " : " ++ show g) $

160159 do ct <- insertCoerce ina t

161160 t' <- insertLazy ct

162161 g <- goal

@@ -539,9 +538,9 @@ elab ist info pattern opts fn tm

539538 mkN n = case namespace info of

540539 Just xs@(_:_) -> sNS n xs

541540 _ -> n

542− elab' ina (PProof ts) = do compute; mapM_ (runTac True ist) ts

541+ elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts

543542 elab' ina (PTactics ts)

544− | not pattern = do mapM_ (runTac False ist) ts

543+ | not pattern = do mapM_ (runTac False ist fn) ts

545544 | otherwise = elab' ina Placeholder

546545 elab' ina (PElabError e) = fail (pshow ist e)

547546 elab' ina (PRewrite fc r sc newg)

@@ -841,9 +840,11 @@ proofSearch' ist top n hints

841840

842841

843842resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

844−resolveTC 0 topg fn ist = fail $ "Can't resolve type class"

845−resolveTC 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True

846−resolveTC depth topg fn ist

843+resolveTC = resTC' []

844+

845+resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class"

846+resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True

847+resTC' tcs depth topg fn ist

847848 = do hnf_compute

848849 g <- goal

849850 ptm <- get_term

@@ -915,15 +916,17 @@ resolveTC depth topg fn ist

915916 mapM_ (\ (_,n) -> do focus n

916917 t' <- goal

917918 let (tc', ttype) = unApply t'

918− let depth' = if t == t' then depth - 1 else depth

919− resolveTC depth' topg fn ist)

919+ let got = fst (unApply t)

920+ let depth' = if tc' `elem` tcs

921+ then depth - 1 else depth

922+ resTC' (got : tcs) depth' topg fn ist)

920923 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

921924 -- if there's any arguments left, we've failed to resolve

922925 hs <- get_holes

923926 ulog <- getUnifyLog

924927 solve

925928 traceWhen ulog ("Got " ++ show n) $ return ()

926− where isImp (PImp p _ _ _ _ _) = (True, p)

929+ where isImp (PImp p _ _ _ _) = (True, p)

927930 isImp arg = (False, priority arg)

928931

929932collectDeferred :: Maybe Name ->

@@ -947,8 +950,8 @@ collectDeferred top t = return t

947950-- Running tactics directly

948951-- if a tactic adds unification problems, return an error

949952

950−runTac :: Bool -> IState -> PTactic -> ElabD ()

951−runTac autoSolve ist tac

953+runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()

954+runTac autoSolve ist fn tac

952955 = do env <- get_env

953956 g <- goal

954957 if autoSolve

@@ -998,7 +1001,7 @@ runTac autoSolve ist tac

9981001 show fn')) fnimps

9991002 tryAll tacs

10001003 when autoSolve solveAll

1001− where isImp (PImp _ _ _ _ _ _) = True

1004+ where isImp (PImp _ _ _ _ _) = True

10021005 isImp _ = False

10031006 envArgs n = do e <- get_env

10041007 case lookup n e of

@@ -1062,8 +1065,8 @@ runTac autoSolve ist tac

10621065 runT Compute = compute

10631066 runT Trivial = do trivial' ist; when autoSolve solveAll

10641067 runT TCInstance = runT (Exact (PResolveTC emptyFC))

1065− runT (ProofSearch top n hints)

1066− = do proofSearch' ist top n hints; when autoSolve solveAll

1068+ runT (ProofSearch top hints)

1069+ = do proofSearch' ist top fn hints; when autoSolve solveAll

10671070 runT (Focus n) = focus n

10681071 runT Solve = solve

10691072 runT (Try l r) = do try' (runT l) (runT r) True

@@ -1142,7 +1145,7 @@ runTac autoSolve ist tac

11421145 ctxt <- get_context

11431146 env <- get_env

11441147 let value' = hnf ctxt env value

1145− runTac autoSolve ist (Exact $ PQuote (reflect value'))

1148+ runTac autoSolve ist fn (Exact $ PQuote (reflect value'))

11461149 runT (Fill v) = do attack -- let x = fill x in ...

11471150 tyn <- getNameFrom (sMN 0 "letty")

11481151 claim tyn RType

@@ -1157,7 +1160,7 @@ runTac autoSolve ist tac

11571160 env <- get_env

11581161 let value' = normalise ctxt env value

11591162 rawValue <- reifyRaw value'

1160− runTac autoSolve ist (Exact $ PQuote rawValue)

1163+ runTac autoSolve ist fn (Exact $ PQuote rawValue)

11611164 runT (GoalType n tac) = do g <- goal

11621165 case unApply g of

11631166 (P _ n' _, _) ->

@@ -1170,7 +1173,7 @@ runTac autoSolve ist tac

11701173 runT x = fail $ "Not implemented " ++ show x

11711174

11721175 runReflected t = do t' <- reify ist t

1173− runTac autoSolve ist t'

1176+ runTac autoSolve ist fn t'

11741177

11751178-- | Prefix a name with the "Language.Reflection" namespace

11761179reflm :: String -> Name

src/Idris/ErrReverse.hs+2−2

@@ -13,7 +13,7 @@ import Debug.Trace

1313-- errors will be more readable

1414

1515errReverse :: IState -> Term -> Term

16−errReverse ist t = rewrite 5 (elideLambdas t)

16+errReverse ist t = rewrite 5 t -- (elideLambdas t)

1717 where

1818

1919 rewrite 0 t = t

@@ -65,7 +65,7 @@ errReverse ist t = rewrite 5 (elideLambdas t)

6565

6666 elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)

6767 elideLambdas (Bind n (Lam t) sc)

68− | size sc > 100 = P Ref (sUN "...") Erased

68+ | size sc > 200 = P Ref (sUN "...") Erased

6969 elideLambdas (Bind n b sc)

7070 = Bind n (fmap elideLambdas b) (elideLambdas sc)

7171 elideLambdas t = t

src/Idris/IBC.hs+55−50

@@ -24,9 +24,8 @@ import System.Directory

2424import Codec.Compression.Zlib (compress)

2525import Util.Zlib (decompressEither)

2626

27−

2827ibcVersion :: Word8

29−ibcVersion = 60

28+ibcVersion = 62

3029

3130

3231data IBCFile = IBCFile { ver :: Word8,

@@ -53,7 +52,7 @@ data IBCFile = IBCFile { ver :: Word8,

5352 ibc_flags :: [(Name, [FnOpt])],

5453 ibc_cg :: [(Name, CGInfo)],

5554 ibc_defs :: [(Name, Def)],

56− ibc_docstrings :: [(Name, String)],

55+ ibc_docstrings :: [(Name, (String, [(Name, String)]))],

5756 ibc_transforms :: [(Term, Term)],

5857 ibc_errRev :: [(Term, Term)],

5958 ibc_coercions :: [Name],

@@ -61,7 +60,8 @@ data IBCFile = IBCFile { ver :: Word8,

6160 ibc_namehints :: [(Name, Name)],

6261 ibc_metainformation :: [(Name, MetaInformation)],

6362 ibc_errorhandlers :: [Name],

64− ibc_function_errorhandlers :: [(Name, Name, Name)] -- fn, arg, handler

63+ ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler

64+ ibc_metavars :: [(Name, (Maybe Name, Int, Bool))]

6565 }

6666 deriving Show

6767{-!

@@ -69,8 +69,7 @@ deriving instance Binary IBCFile

6969!-}

7070

7171initIBC :: IBCFile

72−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

73−

72+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

7473

7574loadIBC :: FilePath -> Idris ()

7675loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -91,9 +90,9 @@ writeIBC :: FilePath -> FilePath -> Idris ()

9190writeIBC src f

9291 = do iLOG $ "Writing ibc " ++ show f

9392 i <- getIState

94− case (Data.List.map fst (idris_metavars i)) \\ primDefs of

95− (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

96− [] -> return ()

93+-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

94+-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

95+-- [] -> return ()

9796 resetNameIdx

9897 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

9998 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

@@ -222,6 +221,10 @@ ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_

222221ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }

223222ibc i (IBCFunctionErrorHandler fn a n) f =

224223 return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }

224+ibc i (IBCMetavar n) f =

225+ case lookup n (idris_metavars i) of

226+ Nothing -> return f

227+ Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

225228

226229process :: IBCFile -> FilePath -> Idris ()

227230process i fn

@@ -262,6 +265,7 @@ process i fn

262265 pMetaInformation (ibc_metainformation i)

263266 pErrorHandlers (ibc_errorhandlers i)

264267 pFunctionErrorHandlers (ibc_function_errorhandlers i)

268+ pMetavars (ibc_metavars i)

265269

266270timestampOlder :: FilePath -> FilePath -> IO ()

267271timestampOlder src ibc = do srct <- getModificationTime src

@@ -389,7 +393,7 @@ pDefs syms ds

389393 updateOrig (Left t) = Left (update t)

390394 updateOrig (Right (l, r)) = Right (update l, update r)

391395

392− updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

396+ updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

393397 = CaseDefs (ts, fmap update t)

394398 (cs, fmap update c)

395399 (is, fmap update i)

@@ -401,8 +405,8 @@ pDefs syms ds

401405 update (Proj t i) = Proj (update t) i

402406 update t = t

403407

404−pDocs :: [(Name, String)] -> Idris ()

405−pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds

408+pDocs :: [(Name, (String, [(Name, String)]))] -> Idris ()

409+pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

406410

407411pAccess :: [(Name, Accessibility)] -> Idris ()

408412pAccess ds = mapM_ (\ (n, a) ->

@@ -451,6 +455,12 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

451455pFunctionErrorHandlers [] = return ()

452456pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]

453457 pFunctionErrorHandlers ns

458+

459+pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

460+pMetavars ns = do i <- getIState

461+ putIState $ i { idris_metavars = Data.List.reverse ns

462+ ++ idris_metavars i }

463+

454464----- Generated by 'derive'

455465

456466instance Binary SizeChange where

@@ -549,6 +559,7 @@ instance Binary SpecialName where

549559 put x1

550560 CaseN x1 -> do putWord8 4; put x1

551561 ElimN x1 -> do putWord8 5; put x1

562+ InstanceCtorN x1 -> do putWord8 6; put x1

552563 get

553564 = do i <- getWord8

554565 case i of

@@ -568,6 +579,8 @@ instance Binary SpecialName where

568579 return (CaseN x1)

569580 5 -> do x1 <- get

570581 return (ElimN x1)

582+ 6 -> do x1 <- get

583+ return (InstanceCtorN x1)

571584 _ -> error "Corrupted binary data for SpecialName"

572585

573586

@@ -607,6 +620,7 @@ instance Binary Const where

607620 B32V x1 -> putWord8 23 >> put x1

608621 B64V x1 -> putWord8 24 >> put x1

609622 BufferType -> putWord8 25

623+ ManagedPtrType -> putWord8 26

610624 get

611625 = do i <- getWord8

612626 case i of

@@ -648,6 +662,7 @@ instance Binary Const where

648662 23 -> fmap B32V get

649663 24 -> fmap B64V get

650664 25 -> return BufferType

665+ 26 -> return ManagedPtrType

651666

652667 _ -> error "Corrupted binary data for Const"

653668

@@ -1037,7 +1052,7 @@ instance Binary MetaInformation where

10371052 return (DataMI x1)

10381053

10391054instance Binary IBCFile where

1040− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33)

1055+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34)

10411056 = {-# SCC "putIBCFile" #-}

10421057 do put x1

10431058 put x2

@@ -1072,6 +1087,7 @@ instance Binary IBCFile where

10721087 put x31

10731088 put x32

10741089 put x33

1090+ put x34

10751091

10761092 get

10771093 = do x1 <- get

@@ -1108,7 +1124,8 @@ instance Binary IBCFile where

11081124 x31 <- get

11091125 x32 <- get

11101126 x33 <- get

1111− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33)

1127+ x34 <- get

1128+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34)

11121129 else return (initIBC { ver = x1 })

11131130

11141131instance Binary DataOpt where

@@ -1217,51 +1234,43 @@ instance Binary Static where

12171234instance Binary Plicity where

12181235 put x

12191236 = case x of

1220− Imp x1 x2 x3 x4 ->

1237+ Imp x1 x2 x3 ->

12211238 do putWord8 0

12221239 put x1

12231240 put x2

12241241 put x3

1225− put x4

1226− Exp x1 x2 x3 x4 ->

1242+ Exp x1 x2 x3 ->

12271243 do putWord8 1

12281244 put x1

12291245 put x2

12301246 put x3

1231− put x4

1232− Constraint x1 x2 x3 ->

1247+ Constraint x1 x2 ->

12331248 do putWord8 2

12341249 put x1

12351250 put x2

1236− put x3

1237− TacImp x1 x2 x3 x4 ->

1251+ TacImp x1 x2 x3 ->

12381252 do putWord8 3

12391253 put x1

12401254 put x2

12411255 put x3

1242− put x4

12431256 get

12441257 = do i <- getWord8

12451258 case i of

12461259 0 -> do x1 <- get

12471260 x2 <- get

12481261 x3 <- get

1249− x4 <- get

1250− return (Imp x1 x2 x3 x4)

1262+ return (Imp x1 x2 x3)

12511263 1 -> do x1 <- get

12521264 x2 <- get

12531265 x3 <- get

1254− x4 <- get

1255− return (Exp x1 x2 x3 x4)

1266+ return (Exp x1 x2 x3)

12561267 2 -> do x1 <- get

12571268 x2 <- get

1258− x3 <- get

1259− return (Constraint x1 x2 x3)

1269+ return (Constraint x1 x2)

12601270 3 -> do x1 <- get

12611271 x2 <- get

12621272 x3 <- get

1263− x4 <- get

1264− return (TacImp x1 x2 x3 x4)

1273+ return (TacImp x1 x2 x3)

12651274 _ -> error "Corrupted binary data for Plicity"

12661275

12671276

@@ -1272,7 +1281,7 @@ instance (Binary t) => Binary (PDecl' t) where

12721281 put x1

12731282 put x2

12741283 put x3

1275− PTy x1 x2 x3 x4 x5 x6

1284+ PTy x1 x2 x3 x4 x5 x6 x7

12761285 -> do putWord8 1

12771286 put x1

12781287 put x2

@@ -1280,18 +1289,20 @@ instance (Binary t) => Binary (PDecl' t) where

12801289 put x4

12811290 put x5

12821291 put x6

1292+ put x7

12831293 PClauses x1 x2 x3 x4 -> do putWord8 2

12841294 put x1

12851295 put x2

12861296 put x3

12871297 put x4

1288− PData x1 x2 x3 x4 x5 ->

1298+ PData x1 x2 x3 x4 x5 x6 ->

12891299 do putWord8 3

12901300 put x1

12911301 put x2

12921302 put x3

12931303 put x4

12941304 put x5

1305+ put x6

12951306 PParams x1 x2 x3 -> do putWord8 4

12961307 put x1

12971308 put x2

@@ -1358,7 +1369,8 @@ instance (Binary t) => Binary (PDecl' t) where

13581369 x4 <- get

13591370 x5 <- get

13601371 x6 <- get

1361− return (PTy x1 x2 x3 x4 x5 x6)

1372+ x7 <- get

1373+ return (PTy x1 x2 x3 x4 x5 x6 x7)

13621374 2 -> do x1 <- get

13631375 x2 <- get

13641376 x3 <- get

@@ -1369,7 +1381,8 @@ instance (Binary t) => Binary (PDecl' t) where

13691381 x3 <- get

13701382 x4 <- get

13711383 x5 <- get

1372− return (PData x1 x2 x3 x4 x5)

1384+ x6 <- get

1385+ return (PData x1 x2 x3 x4 x5 x6)

13731386 4 -> do x1 <- get

13741387 x2 <- get

13751388 x3 <- get

@@ -1907,34 +1920,30 @@ instance (Binary t) => Binary (PDo' t) where

19071920instance (Binary t) => Binary (PArg' t) where

19081921 put x

19091922 = case x of

1910− PImp x1 x2 x3 x4 x5 x6 ->

1923+ PImp x1 x2 x3 x4 x5 ->

19111924 do putWord8 0

19121925 put x1

19131926 put x2

19141927 put x3

19151928 put x4

19161929 put x5

1917− put x6

1918− PExp x1 x2 x3 x4 ->

1930+ PExp x1 x2 x3 ->

19191931 do putWord8 1

19201932 put x1

19211933 put x2

19221934 put x3

1923− put x4

1924− PConstraint x1 x2 x3 x4 ->

1935+ PConstraint x1 x2 x3 ->

19251936 do putWord8 2

19261937 put x1

19271938 put x2

19281939 put x3

1929− put x4

1930− PTacImplicit x1 x2 x3 x4 x5 x6 ->

1940+ PTacImplicit x1 x2 x3 x4 x5 ->

19311941 do putWord8 3

19321942 put x1

19331943 put x2

19341944 put x3

19351945 put x4

19361946 put x5

1937− put x6

19381947 get

19391948 = do i <- getWord8

19401949 case i of

@@ -1943,25 +1952,21 @@ instance (Binary t) => Binary (PArg' t) where

19431952 x3 <- get

19441953 x4 <- get

19451954 x5 <- get

1946− x6 <- get

1947− return (PImp x1 x2 x3 x4 x5 x6)

1955+ return (PImp x1 x2 x3 x4 x5)

19481956 1 -> do x1 <- get

19491957 x2 <- get

19501958 x3 <- get

1951− x4 <- get

1952− return (PExp x1 x2 x3 x4)

1959+ return (PExp x1 x2 x3)

19531960 2 -> do x1 <- get

19541961 x2 <- get

19551962 x3 <- get

1956− x4 <- get

1957− return (PConstraint x1 x2 x3 x4)

1963+ return (PConstraint x1 x2 x3)

19581964 3 -> do x1 <- get

19591965 x2 <- get

19601966 x3 <- get

19611967 x4 <- get

19621968 x5 <- get

1963− x6 <- get

1964− return (PTacImplicit x1 x2 x3 x4 x5 x6)

1969+ return (PTacImplicit x1 x2 x3 x4 x5)

19651970 _ -> error "Corrupted binary data for PArg'"

19661971

19671972

src/Idris/ParseData.hs+26−24

@@ -33,13 +33,15 @@ import qualified Data.HashSet as HS

3333import qualified Data.Text as T

3434import qualified Data.ByteString.UTF8 as UTF8

3535

36+import Debug.Trace

37+

3638{- |Parses a record type declaration

3739Record ::=

3840 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

3941-}

4042record :: SyntaxInfo -> IdrisParser PDecl

4143record syn = do (doc, acc) <- try (do

42− doc <- option "" (docComment '|')

44+ doc <- option ("", []) docComment

4345 acc <- optional accessibility

4446 reserved "record"

4547 return (doc, acc))

@@ -49,13 +51,13 @@ record syn = do (doc, acc) <- try (do

4951 ty <- typeExpr (allowImp syn)

5052 let tyn = expandNS syn tyn_in

5153 reserved "where"

52− (cdoc, cn, cty, _, _) <- indentedBlockS (constructor syn)

54+ (cdoc, argDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)

5355 accData acc tyn [cn]

5456 let rsyn = syn { syn_namespace = show (nsroot tyn) :

5557 syn_namespace syn }

5658 let fns = getRecNames rsyn cty

5759 mapM_ (\n -> addAcc n acc) fns

58− return $ PRecord doc rsyn fc tyn ty cdoc cn cty

60+ return $ PRecord (fst doc) rsyn fc tyn ty cdoc cn cty

5961 <?> "record type declaration"

6062 where

6163 getRecNames :: SyntaxInfo -> PTerm -> [Name]

@@ -100,29 +102,29 @@ SimpleConstructorList ::=

100102 ;

101103-}

102104data_ :: SyntaxInfo -> IdrisParser PDecl

103−data_ syn = do (doc, acc, dataOpts) <- try (do

104− doc <- option "" (docComment '|')

105+data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

106+ (doc, argDocs) <- option ("", []) docComment

105107 pushIndent

106108 acc <- optional accessibility

107109 elim <- dataOpts []

108110 co <- dataI

109111 let dataOpts = combineDataOpts(elim ++ co)

110− return (doc, acc, dataOpts))

112+ return (doc, argDocs, acc, dataOpts))

111113 fc <- getFC

112114 tyn_in <- fnName

113115 (do try (lchar ':')

114116 popIndent

115117 ty <- typeExpr (allowImp syn)

116118 let tyn = expandNS syn tyn_in

117− option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

119+ option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

118120 reserved "where"

119121 cons <- indentedBlock (constructor syn)

120− accData acc tyn (map (\ (_, n, _, _, _) -> n) cons)

121− return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

122+ accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons)

123+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

122124 args <- many name

123125 let ty = bindArgs (map (const PType) args) PType

124126 let tyn = expandNS syn tyn_in

125− option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

127+ option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

126128 try (lchar '=') <|> do reserved "where"

127129 let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

128130 let n = show tyn_in ++ " "

@@ -134,14 +136,14 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

134136 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

135137 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

136138 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

137− cons <- sepBy1 (simpleConstructor syn) (lchar '|')

139+ cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

138140 terminator

139141 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

140− cons' <- mapM (\ (doc, x, cargs, cfc, fs) ->

142+ cons' <- mapM (\ (doc, argDocs, x, cargs, cfc, fs) ->

141143 do let cty = bindArgs cargs conty

142− return (doc, x, cty, cfc, fs)) cons

143− accData acc tyn (map (\ (_, n, _, _, _) -> n) cons')

144− return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))

144+ return (doc, argDocs, x, cty, cfc, fs)) cons

145+ accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons')

146+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons')))

145147 <?> "data type declaration"

146148 where

147149 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

@@ -150,17 +152,17 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

150152 bindArgs :: [PTerm] -> PTerm -> PTerm

151153 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

152154 combineDataOpts :: DataOpts -> DataOpts

153− combineDataOpts opts = if Codata `elem` opts

154− then delete DefaultEliminator opts

155+ combineDataOpts opts = if Codata `elem` opts

156+ then delete DefaultEliminator opts

155157 else opts

156158

157159

158160{- | Parses a type constructor declaration

159161 Constructor ::= DocComment? FnName TypeSig;

160162-}

161−constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC, [Name])

163+constructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, PTerm, FC, [Name])

162164constructor syn

163− = do doc <- option "" (docComment '|')

165+ = do (doc, argDocs) <- option ("", []) docComment

164166 cn_in <- fnName; fc <- getFC

165167 let cn = expandNS syn cn_in

166168 lchar ':'

@@ -169,21 +171,21 @@ constructor syn

169171 fs <- option [] (do lchar '%'; reserved "erase"

170172 sepBy1 name (lchar ','))

171173 ty <- typeExpr (allowImp syn)

172− return (doc, cn, ty, fc, fs)

174+ return (doc, argDocs, cn, ty, fc, fs)

173175 <?> "constructor"

174176

175177{- | Parses a constructor for simple discriminative union data types

176178 SimpleConstructor ::= FnName SimpleExpr* DocComment?

177179-}

178−simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC, [Name])

180+simpleConstructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, [PTerm], FC, [Name])

179181simpleConstructor syn

180− = do cn_in <- fnName

182+ = do doc <- option ("", []) (try docComment)

183+ cn_in <- fnName

181184 let cn = expandNS syn cn_in

182185 fc <- getFC

183186 args <- many (do notEndApp

184187 simpleExpr syn)

185− doc <- option "" (try $ docComment '^')

186− return (doc, cn, args, fc, [])

188+ return (fst doc, [], cn, args, fc, [])

187189 <?> "constructor"

188190

189191{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+7−5

@@ -786,10 +786,9 @@ pi syn =

786786 return []

787787 st <- static

788788 (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

789− doc <- option "" (docComment '^')

790789 symbol "->"

791790 sc <- expr syn

792− return (bindList (PPi (Exp opts st doc False)) xt sc)) <|> (do

791+ return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

793792 lchar '{'

794793 (do reserved "auto"

795794 when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

@@ -798,7 +797,7 @@ pi syn =

798797 symbol "->"

799798 sc <- expr syn

800799 return (bindList (PPi

801− (TacImp [] Dynamic (PTactics [Trivial]) "")) xt sc))

800+ (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

802801 <|> (do

803802 reserved "default"

804803 when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

@@ -807,13 +806,13 @@ pi syn =

807806 lchar '}'

808807 symbol "->"

809808 sc <- expr syn

810− return (bindList (PPi (TacImp [] Dynamic script "")) xt sc))

809+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

811810 <|> (if implicitAllowed syn then do

812811 xt <- typeDeclList syn

813812 lchar '}'

814813 symbol "->"

815814 sc <- expr syn

816− return (bindList (PPi (Imp opts st "" False)) xt sc)

815+ return (bindList (PPi (Imp opts st False)) xt sc)

817816 else do fail "no implicit arguments allowed here"))

818817 <?> "dependent type signature"

819818

@@ -1003,6 +1002,7 @@ Constant ::=

10031002 | 'Float'

10041003 | 'String'

10051004 | 'Ptr'

1005+ | 'ManagedPtr'

10061006 | 'prim__UnsafeBuffer'

10071007 | 'Bits8'

10081008 | 'Bits16'

@@ -1027,6 +1027,7 @@ constant = do reserved "Integer"; return (AType (ATInt ITBig))

10271027 <|> do reserved "Float"; return (AType ATFloat)

10281028 <|> do reserved "String"; return StrType

10291029 <|> do reserved "Ptr"; return PtrType

1030+ <|> do reserved "ManagedPtr"; return ManagedPtrType

10301031 <|> do reserved "prim__UnsafeBuffer"; return BufferType

10311032 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))

10321033 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))

@@ -1165,6 +1166,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

11651166 return $ TSeq t (mergeSeq ts)

11661167 <|> do reserved "compute"; return Compute

11671168 <|> do reserved "trivial"; return Trivial

1169+ <|> do reserved "search"; return (ProofSearch Nothing [])

11681170 <|> do reserved "instance"; return TCInstance

11691171 <|> do reserved "solve"; return Solve

11701172 <|> do reserved "attack"; return Attack

src/Idris/ParseHelpers.hs+33−32

@@ -17,6 +17,8 @@ import Idris.Core.TT

1717import Idris.Core.Evaluate

1818import Idris.Delaborate (pprintErr)

1919

20+import qualified Util.Pretty as Pretty (text)

21+

2022import Control.Applicative

2123import Control.Monad

2224import Control.Monad.State.Strict

@@ -33,6 +35,8 @@ import qualified Data.ByteString.UTF8 as UTF8

3335

3436import System.FilePath

3537

38+import Debug.Trace

39+

3640-- | Idris parser with state used during parsing

3741type IdrisParser = StateT IState IdrisInnerParser

3842

@@ -51,10 +55,10 @@ runparser p i inputname =

5155 parseString (runInnerParser (evalStateT p i))

5256 (Directed (UTF8.fromString inputname) 0 0 0 0)

5357

54−noDocCommentHere :: Char -> String -> IdrisParser ()

55−noDocCommentHere c msg =

58+noDocCommentHere :: String -> IdrisParser ()

59+noDocCommentHere msg =

5660 optional (do fc <- getFC

57− docComment c

61+ docComment

5862 ist <- get

5963 put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>

6064 pure ()

@@ -86,12 +90,6 @@ isEol _ = False

8690eol :: MonadicParsing m => m ()

8791eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

8892

89−-- | Checks if a character is a documentation comment marker

90−isDocCommentMarker :: Char -> Bool

91−isDocCommentMarker '|' = True

92−isDocCommentMarker '^' = True

93−isDocCommentMarker _ = False

94−

9593{- | Consumes a single-line comment

9694

9795@

@@ -103,7 +101,6 @@ isDocCommentMarker _ = False

103101singleLineComment :: MonadicParsing m => m ()

104102singleLineComment = try (string "--" *> eol *> pure ())

105103 <|> try (string "--" *> many simpleWhiteSpace *>

106− satisfy (not . isDocCommentMarker) *>

107104 many (satisfy (not . isEol)) *>

108105 eol *> pure ())

109106 <?> ""

@@ -127,13 +124,12 @@ singleLineComment = try (string "--" *> eol *> pure ())

127124-}

128125multiLineComment :: MonadicParsing m => m ()

129126multiLineComment = try (string "{-" *> (string "-}") *> pure ())

130− <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars

127+ <|> string "{-" *> inCommentChars

131128 <?> ""

132129 where inCommentChars :: MonadicParsing m => m ()

133130 inCommentChars = string "-}" *> pure ()

134131 <|> try (multiLineComment) *> inCommentChars

135− <|> try (docComment '|') *> inCommentChars

136− <|> try (docComment '^') *> inCommentChars

132+ <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

137133 <|> skipSome (noneOf startEnd) *> inCommentChars

138134 <|> oneOf startEnd *> inCommentChars

139135 <?> "end of comment"

@@ -148,27 +144,32 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

148144 ;

149145@

150146 -}

151−docComment :: MonadicParsing m => Char -> m String

152−docComment marker | isDocCommentMarker marker = do dc <- docComment' marker

153− return (T.unpack $ T.strip $ T.pack dc)

154− | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"

155− where docComment' :: MonadicParsing m => Char -> m String

156− docComment' marker = (do string "--"

147+docComment :: IdrisParser (String, [(Name, String)])

148+docComment = do dc <- pushIndent *> docCommentLine

149+ rest <- many (indented docCommentLine)

150+ args <- many (indented argDocCommentLine)

151+ popIndent

152+ return (T.unpack $ T.strip $ T.pack (dc ++ concat rest), args)

153+

154+ where docCommentLine :: MonadicParsing m => m String

155+ docCommentLine = try (do string "|||"

157156 many (satisfy isSpace)

158− char marker

157+ first <- satisfy (\c -> not (isEol c || c == '@'))

159158 res <- many (satisfy (not . isEol))

160− eol

161− rest <- many (do string "--"

162− stuff <- many (satisfy (not . isEol))

163− eol

164− return stuff)

165− someSpace

166− return (res ++ concat rest))-- ++ concat rest))

167− <|> (do string "{-"

168− many (satisfy isSpace)

169− char marker

170− (manyTill anyChar (try (string "-}")) <?> "end of comment"))

171− <?> ""

159+ eol ; someSpace

160+ return (first:res))-- ++ concat rest))

161+ <?> ""

162+ argDocCommentLine = do string "|||"

163+ many (satisfy isSpace)

164+ char '@'

165+ many (satisfy isSpace)

166+ n <- name

167+ many (satisfy isSpace)

168+ docs <- many (satisfy (not . isEol))

169+ eol ; someSpace

170+ return (n, docs)

171+

172+

172173

173174-- | Parses some white space

174175whiteSpace :: MonadicParsing m => m ()

src/Idris/ParseOps.hs+1−1

@@ -59,7 +59,7 @@ binary name f = Infix (do fc <- getFC

5959 indentPropHolds gtProp

6060 reservedOp name

6161 indentPropHolds gtProp

62− doc <- option "" (docComment '^')

62+ doc <- option ("", []) docComment

6363 return (f fc))

6464

6565-- | Prefix operator

src/Idris/Parser.hs+72−61

@@ -87,7 +87,7 @@ import System.IO

8787@

8888-}

8989moduleHeader :: IdrisParser [String]

90−moduleHeader = try (do noDocCommentHere '|' "Modules cannot have documentation comments"

90+moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"

9191 reserved "module"

9292 i <- identifier

9393 option ';' (lchar ';')

@@ -315,7 +315,7 @@ fnDecl' syn = checkFixity $

315315 do (doc, fc, opts', n, acc) <- try (do

316316 pushIndent

317317 ist <- get

318− doc <- option "" (docComment '|')

318+ doc <- option ("", []) docComment

319319 ist <- get

320320 let initOpts = if default_total ist

321321 then [TotalFn]

@@ -331,7 +331,7 @@ fnDecl' syn = checkFixity $

331331 ty <- typeExpr (allowImp syn)

332332 terminator

333333 addAcc n acc

334− return (PTy doc syn fc opts' n ty)

334+ return (PTy (fst doc) (snd doc) syn fc opts' n ty)

335335 <|> postulate syn

336336 <|> caf syn

337337 <|> pattern syn

@@ -344,7 +344,7 @@ fnDecl' syn = checkFixity $

344344 unless fOk . fail $

345345 "Missing fixity declaration for " ++ show n

346346 return decl

347− getName (PTy _ _ _ _ n _) = Just n

347+ getName (PTy _ _ _ _ _ n _) = Just n

348348 getName _ = Nothing

349349 fixityOK (NS n _) = fixityOK n

350350 fixityOK (UN n) | all (flip elem opChars) (str n) =

@@ -413,7 +413,7 @@ Postulate ::=

413413@

414414-}

415415postulate :: SyntaxInfo -> IdrisParser PDecl

416−postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

416+postulate syn = do doc <- try $ do doc <- option ("", []) docComment

417417 pushIndent

418418 reserved "postulate"

419419 return doc

@@ -431,7 +431,7 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

431431 fc <- getFC

432432 terminator

433433 addAcc n acc

434− return (PPostulate doc syn fc opts' n ty)

434+ return (PPostulate (fst doc) syn fc opts' n ty)

435435 <?> "postulate"

436436

437437{- | Parses a using declaration

@@ -561,7 +561,7 @@ Class ::=

561561-}

562562class_ :: SyntaxInfo -> IdrisParser [PDecl]

563563class_ syn = do (doc, acc) <- try (do

564− doc <- option "" (docComment '|')

564+ doc <- option ("", []) docComment

565565 acc <- optional accessibility

566566 return (doc, acc))

567567 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

@@ -569,7 +569,7 @@ class_ syn = do (doc, acc) <- try (do

569569 cs <- many carg

570570 ds <- option [] (classBlock syn)

571571 accData acc n (concatMap declared ds)

572− return [PClass doc syn fc cons n cs ds]

572+ return [PClass (fst doc) syn fc cons n cs ds]

573573 <?> "type-class declaration"

574574 where

575575 carg :: IdrisParser (Name, PTerm)

@@ -1039,18 +1039,25 @@ totality

10391039{- | Parses a type provider

10401040

10411041@

1042−Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;

1042+Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1043+ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

10431044@

10441045 -}

10451046provider :: SyntaxInfo -> IdrisParser [PDecl]

10461047provider syn = do try (lchar '%' *> reserved "provide");

1048+ what <- provideWhat

10471049 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

10481050 fc <- getFC

10491051 reserved "with"

10501052 e <- expr syn

1051− return [PProvider syn fc n t e]

1053+ return [PProvider syn fc what n t e]

10521054 <?> "type provider"

1053−

1055+ where provideWhat :: IdrisParser ProvideWhat

1056+ provideWhat = option ProvAny

1057+ ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>

1058+ pure ProvTerm)

1059+ <|> (reserved "postulate" *> pure ProvPostulate)

1060+ <?> "provider variety")

10541061{- | Parses a transform

10551062

10561063@

@@ -1219,56 +1226,60 @@ loadSource h lidr f

12191226 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

12201227 let syntax = defaultSyntax{ syn_namespace = reverse mname }

12211228 ds' <- parseProg syntax f file pos

1222− unless (null ds') $ do

1223− let ds = namespaces mname ds'

1224− logLvl 3 (show $ showDecls True ds)

1225− i <- getIState

1226− logLvl 10 (show (toAlist (idris_implicits i)))

1227− logLvl 3 (show (idris_infixes i))

1228− -- Now add all the declarations to the context

1229− v <- verbose

1230− when v $ ihputStrLn h $ "Type checking " ++ f

1231− -- we totality check after every Mutual block, so if

1232− -- anything is a single definition, wrap it in a

1233− -- mutual block on its own

1234− elabDecls toplevel (map toMutual ds)

1235− i <- getIState

1236− -- simplify every definition do give the totality checker

1237− -- a better chance

1238− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1239− updateContext (simplifyCasedef n))

1240− (map snd (idris_totcheck i))

1241− -- build size change graph from simplified definitions

1242− iLOG "Totality checking"

1243− i <- getIState

1244− mapM_ buildSCG (idris_totcheck i)

1245− mapM_ checkDeclTotality (idris_totcheck i)

1246−

1247− -- Redo totality check for deferred names

1248− let deftots = idris_defertotcheck i

1249− iLOG $ "Totality checking " ++ show deftots

1250− mapM_ (\x -> do tot <- getTotality x

1251− case tot of

1252− Total _ -> setTotality x Unchecked

1253− _ -> return ()) (map snd deftots)

1254− mapM_ buildSCG deftots

1255− mapM_ checkDeclTotality deftots

1256−

1257− iLOG ("Finished " ++ f)

1258− ibcsd <- valIBCSubDir i

1259− iLOG "Universe checking"

1260− iucheck

1261− let ibc = ibcPathNoFallback ibcsd f

1262− i <- getIState

1263− addHides (hide_list i)

1264− ok <- noErrors

1265− when ok $

1266− idrisCatch (do writeIBC f ibc; clearIBC)

1267− (\c -> return ()) -- failure is harmless

1268− i <- getIState

1269− putIState (i { default_total = def_total,

1270− hide_list = [] })

1271− return ()

1229+

1230+ -- Parsing done, now process declarations

1231+

1232+ let ds = namespaces mname ds'

1233+ logLvl 3 (show $ showDecls True ds)

1234+ i <- getIState

1235+ logLvl 10 (show (toAlist (idris_implicits i)))

1236+ logLvl 3 (show (idris_infixes i))

1237+ -- Now add all the declarations to the context

1238+ v <- verbose

1239+ when v $ ihputStrLn h $ "Type checking " ++ f

1240+ -- we totality check after every Mutual block, so if

1241+ -- anything is a single definition, wrap it in a

1242+ -- mutual block on its own

1243+ elabDecls toplevel (map toMutual ds)

1244+ i <- getIState

1245+ -- simplify every definition do give the totality checker

1246+ -- a better chance

1247+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1248+ updateContext (simplifyCasedef n))

1249+ (map snd (idris_totcheck i))

1250+ -- build size change graph from simplified definitions

1251+ iLOG "Totality checking"

1252+ i <- getIState

1253+ mapM_ buildSCG (idris_totcheck i)

1254+ mapM_ checkDeclTotality (idris_totcheck i)

1255+

1256+ -- Redo totality check for deferred names

1257+ let deftots = idris_defertotcheck i

1258+ iLOG $ "Totality checking " ++ show deftots

1259+ mapM_ (\x -> do tot <- getTotality x

1260+ case tot of

1261+ Total _ -> setTotality x Unchecked

1262+ _ -> return ()) (map snd deftots)

1263+ mapM_ buildSCG deftots

1264+ mapM_ checkDeclTotality deftots

1265+

1266+ iLOG ("Finished " ++ f)

1267+ ibcsd <- valIBCSubDir i

1268+ iLOG "Universe checking"

1269+ iucheck

1270+ let ibc = ibcPathNoFallback ibcsd f

1271+ i <- getIState

1272+ addHides (hide_list i)

1273+

1274+ -- Finally, write an ibc if checking was successful

1275+

1276+ ok <- noErrors

1277+ when ok $

1278+ idrisCatch (do writeIBC f ibc; clearIBC)

1279+ (\c -> return ()) -- failure is harmless

1280+ i <- getIState

1281+ putIState (i { default_total = def_total,

1282+ hide_list = [] })

12721283 return ()

12731284 where

12741285 namespaces :: [String] -> [PDecl] -> [PDecl]

src/Idris/PartialEval.hs+2−2

@@ -103,7 +103,7 @@ mkPE_TermDecl ist newname sname ns

103103 deImp (PApp fc t as) = PApp fc t (map deImpArg as)

104104 deImp t = t

105105

106− deImpArg a@(PImp _ _ _ _ _ _) = a { getTm = Placeholder }

106+ deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }

107107 deImpArg a = a

108108

109109data PEArgType = ImplicitS | ImplicitD

@@ -124,7 +124,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

124124 | imparg imp = (ImplicitD, tm)

125125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

126126

127− imparg (PExp _ _ _ _) = False

127+ imparg (PExp _ _ _) = False

128128 imparg _ = True

129129

130130 buildApp env [] [] _ _ = []

src/Idris/Primitives.hs+3−1

@@ -172,7 +172,9 @@ primitives =

172172 (0, LStdIn) partial,

173173 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

174174 (0, LNullPtr) total,

175−

175+ -- Managed pointer registration

176+ Prim (sUN "prim__registerPtr") (ty [PtrType, AType (ATInt ITNative)] ManagedPtrType) 2 (p_cantreduce)

177+ (2, LRegisterPtr) total,

176178 -- Buffers

177179 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)

178180 (1, LAllocate) total,

src/Idris/ProofSearch.hs+1−1

@@ -109,6 +109,6 @@ proofSearch elab fn nroot hints ist

109109 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

110110 solve

111111

112− isImp (PImp p _ _ _ _ _) = (True, p)

112+ isImp (PImp p _ _ _ _) = (True, p)

113113 isImp arg = (False, priority arg)

114114

src/Idris/Prover.hs+5−5

@@ -59,7 +59,7 @@ prove :: Context -> Bool -> Name -> Type -> Idris ()

5959prove ctxt lit n ty

6060 = do let ps = initElaborator n ctxt ty

6161 ideslavePutSExp "start-proof-mode" n

62− (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

62+ (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

6363 iLOG $ "Adding " ++ show tm

6464 iputStrLn $ showProof lit n prf

6565 i <- getIState

@@ -161,8 +161,8 @@ receiveInput e =

161161 Just (Interpret cmd) -> return (Just cmd)

162162 Nothing -> return Nothing

163163

164−ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

165−ploop d prompt prf e h

164+ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

165+ploop fn d prompt prf e h

166166 = do i <- getIState

167167 when d $ dumpState i (proof e)

168168 (x, h') <-

@@ -260,7 +260,7 @@ ploop d prompt prf e h

260260 return (False, e, False, prf))

261261 (\err -> do putIState ist ; ierror err)

262262 Success tac -> do (_, e) <- elabStep e saveState

263− (_, st) <- elabStep e (runTac True i tac)

263+ (_, st) <- elabStep e (runTac True i fn tac)

264264-- trace (show (problems (proof st))) $

265265 iPrintResult ""

266266 return (True, st, False, prf ++ [step]))

@@ -269,5 +269,5 @@ ploop d prompt prf e h

269269 ideslavePutSExp "write-proof-state" (prf', length prf')

270270 if done then do (tm, _) <- elabStep st get_term

271271 return (tm, prf')

272− else ploop d prompt prf' st h'

272+ else ploop fn d prompt prf' st h'

273273 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

src/Idris/Providers.hs+14−5

@@ -1,5 +1,5 @@

1−{-# LANGUAGE PatternGuards #-}

2−module Idris.Providers (providerTy, getProvided) where

1+{-# LANGUAGE PatternGuards, DeriveFunctor #-}

2+module Idris.Providers (providerTy, getProvided, Provided(..)) where

33

44import Idris.Core.TT

55import Idris.Core.Evaluate

@@ -11,14 +11,19 @@ import Debug.Trace

1111

1212-- | Wrap a type provider in the type of type providers

1313providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm ""]

14+providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm]

1515

1616ioret = sUN "prim_io_return"

1717ermod = sNS (sUN "Error") ["Providers"]

1818prmod = sNS (sUN "Provide") ["Providers"]

19+posmod = sNS (sUN "Postulate") ["Providers"]

20+

21+data Provided a = Provide a

22+ | Postulate

23+ deriving (Show, Eq, Functor)

1924

2025-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

21−getProvided :: FC -> TT Name -> Idris (TT Name)

26+getProvided :: FC -> TT Name -> Idris (Provided (TT Name))

2227getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

2328 , (P _ nm _, [_, err]) <- unApply result

2429 , pioret == ioret && nm == ermod

@@ -28,7 +33,11 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

2833 | (P _ pioret _, [tp, result]) <- unApply tm

2934 , (P _ nm _, [_, res]) <- unApply result

3035 , pioret == ioret && nm == prmod

31− = return res

36+ = return . Provide $ res

37+ | (P _ pioret _, [tp, result]) <- unApply tm

38+ , (P _ nm _, [_]) <- unApply result

39+ , pioret == ioret && nm == posmod

40+ = return Postulate

3241 | otherwise = ifail $ "Internal type provider error: result was not " ++

3342 "IO (Provider a), or perhaps missing normalisation."

3443

src/Idris/REPL.hs+2−2

@@ -724,8 +724,8 @@ process h fn (DoProofSearch updatefile l n hints)

724724 Just (t, e, False) -> (t, e, False)

725725 _ -> (Nothing, 0, True)

726726 let fc = fileFC fn

727− let body t = PProof [Try (TSeq Intros (ProofSearch t n hints))

728− (ProofSearch t n hints)]

727+ let body t = PProof [Try (TSeq Intros (ProofSearch t hints))

728+ (ProofSearch t hints)]

729729 let def = PClause fc mn (PRef fc mn) [] (body top) []

730730 newmv <- idrisCatch

731731 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

src/Pkg/Package.hs+6−6

@@ -57,12 +57,12 @@ buildPkg warnonly (install, fp)

5757 _ -> return ()

5858 -- Also give up if there are metavariables to solve

5959 case (map fst (idris_metavars ist) \\ primDefs) of

60− [] -> when install $ installPkg pkgdesc

61− ms -> do if install

62− then putStrLn "Can't install: there are undefined metavariables:"

63− else putStrLn "There are undefined metavariables:"

64− putStrLn $ "\t" ++ show ms

65− exitWith (ExitFailure 1)

60+ _ -> when install $ installPkg pkgdesc

61+-- ms -> do if install

62+-- then putStrLn "Can't install: there are undefined metavariables:"

63+-- else putStrLn "There are undefined metavariables:"

64+-- putStrLn $ "\t" ++ show ms

65+-- exitWith (ExitFailure 1)

6666

6767-- | Type check packages only

6868--

test/Makefile+1−1

@@ -11,7 +11,7 @@ test_java:

1111 perl ./runtest.pl without buffer001 --codegen Java

1212

1313test_js:

14− @perl ./runtest.pl without reg029 io001 dsl002 io003 effects001 effects002 buffer001 --codegen node

14+ @perl ./runtest.pl without reg029 io001 dsl002 io003 effects001 effects002 buffer001 bounded001 --codegen node

1515

1616test_llvm:

1717 @perl ./runtest.pl without io003 buffer001 --codegen llvm

test/ffi005/Postulate.idrnew file+14

@@ -0,0 +1,14 @@

1+module Main

2+

3+import Providers

4+

5+%language TypeProviders

6+

7+bad : IO (Provider _|_)

8+bad = pure Postulate

9+

10+%provide (oops : _|_) with bad

11+

12+main : IO ()

13+main = putStrLn "oops"

14+

test/ffi005/Postulate2.idrnew file+13

@@ -0,0 +1,13 @@

1+module Main

2+

3+import Providers

4+

5+%language TypeProviders

6+

7+bad : IO (Provider _|_)

8+bad = pure Postulate

9+

10+%provide postulate (oops : _|_) with bad

11+

12+main : IO ()

13+main = putStrLn "oops"

test/ffi005/Postulate3.idrnew file+13

@@ -0,0 +1,13 @@

1+module Main

2+

3+import Providers

4+

5+%language TypeProviders

6+

7+bad : IO (Provider _|_)

8+bad = pure Postulate

9+

10+%provide term (oops : _|_) with bad

11+

12+main : IO ()

13+main = putStrLn "oops"

test/ffi005/expectednew file+3

@@ -0,0 +1,3 @@

1+oops

2+oops

3+Attempted to provide a postulate where a term was expected.

test/ffi005/runnew file+12

@@ -0,0 +1,12 @@

1+#!/usr/bin/env bash

2+

3+idris $@ Postulate.idr -o postulate

4+./postulate

5+rm -f postulate *.ibc

6+

7+idris $@ Postulate2.idr -o postulate

8+./postulate

9+rm -f postulate *.ibc

10+

11+idris $@ Postulate3.idr -o postulate

12+rm -f postulate *.ibc