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

CHANGELOG+7

compare with master

unifiedsplit

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

9* Lots of performance patches for generated JavaScript

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

11 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

12

19

13New in 0.9.11:

20New in 0.9.11:

14--------------

21--------------

idris.cabal+3

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

299 test/ffi004/theType

300 test/ffi004/theOtherType

301 test/ffi004/expected

302+ test/ffi005/*.idr

303+ test/ffi005/run

304+ test/ffi005/expected

302

305

303 test/interactive001/run

306 test/interactive001/run

304 test/interactive001/input

307 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−

4/** @constructor */

1/** @constructor */

5var __IDRRT__Type = function(type) {

2var __IDRRT__Type = function(type) {

6 this.type = type;

3 this.type = type;

jsrts/jsbn/jsbn.js+3

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

1233 return new BigInteger(val);

1234}

1235})();

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'

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

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

15

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) =

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

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

185

186−-- FIXME: this is very inefficient

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

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

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

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)

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

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

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

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

191

193

192data SortedMap : Type -> Type -> Type where

194data SortedMap : Type -> Type -> Type where

193 Empty : SortedMap k v

195 Empty : SortedMap k v

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

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

7%access public

8

9

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

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

11−-- Zero is chosen to be positive.

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

12data ZZ = Pos Nat | NegS Nat

13

14instance Signed ZZ where

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

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

1module Debug.Trace

2

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

4+||| @ msg what to print

5+||| @ result the final result

3−trace : String -> a -> a

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

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

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

5

8

6

9

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

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

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

22

23class (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)

25

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

27minimum x y with (order x y)

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

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

22 -- ^ explicit universe variable

23%name TTUExp uexp

24

25−-- | Primitive constants

25+||| Primitive constants

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

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

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

66reflectConstant = toConst

67

68

69−-- | Types of named references

69+||| Types of named references

70data NameType = Bound

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

72 | Ref

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

77 -- ^ type constructor with tag and number

78%name NameType nt, nt'

79

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

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

81−-- binding contexts

81+||| binding contexts

82data Binder a = Lam a

83 | Pi a

84 | Let a a

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

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

125

126

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

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

128data TT = P NameType TTName TT

129 -- ^ named binders

130 | V Int

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

146

147%name TT tm, tm'

148

149−-- | Raw terms without types

149+||| Raw terms without types

150data Raw = Var TTName

151 | RBind TTName (Binder Raw) Raw

152 | RApp Raw Raw

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

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

42

43%name Err err, e

44

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

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

46data ErrorReportPart = TextPart String

47 | NamePart TTName

48 | TermPart TT

libs/base/Providers.idr+19−2

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

1module Providers

2

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

3public

4public

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

5

16

6-- instances

17-- instances

7instance Functor Provider where

18instance Functor Provider where

8 map f (Provide a) = Provide (f a)

19 map f (Provide a) = Provide (f a)

9 map f (Error err) = Error err

20 map f (Error err) = Error err

21+ map f Postulate = Postulate

10

22

11instance Applicative Provider where

23instance Applicative Provider where

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

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

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

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

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

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

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

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

29+ Postulate <$> _ = Postulate

15 pure = Provide

30 pure = Provide

16

31

32+-- is this correct for Postulate?

17instance Monad Provider where

33instance Monad Provider where

18 (Provide x) >>= f = f x

34 (Provide x) >>= f = f x

19 (Error err) >>= _ = Error err

35 (Error err) >>= _ = Error err

36+ Postulate >>= f = Postulate

libs/base/System.idr+12−6

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

5%default partial

6%access public

7

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

8getArgs : IO (List String)

9getArgs : IO (List String)

9getArgs = do n <- numArgs

10getArgs = do n <- numArgs

10 ga' [] 0 n

11 ga' [] 0 n

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

20 do arg <- getArg i

21 do arg <- getArg i

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

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

22

23

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

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

24−-- otherwise it returns Nothing.

25+||| otherwise it returns Nothing.

25getEnv : String -> IO (Maybe String)

26getEnv : String -> IO (Maybe String)

26getEnv key = do

27getEnv key = do

27 str_ptr <- getEnv'

28 str_ptr <- getEnv'

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

33 getEnv' : IO String

34 getEnv' : IO String

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

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

35

36

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

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

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

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

38setEnv : String -> String -> IO Bool

39setEnv : String -> String -> IO Bool

39setEnv key value = do

40setEnv key value = do

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

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

41 return (ok == 0)

42 return (ok == 0)

42

43

43−-- Unsets an environment variable.

44+||| Unsets an environment variable.

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

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

45unsetEnv : String -> IO Bool

46unsetEnv : String -> IO Bool

46unsetEnv key = do

47unsetEnv key = do

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

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

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

68 then return $ reverse $ map splitEq acc

69 then return $ reverse $ map splitEq acc

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

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

70

71

72+||| Quit with a particular exit code

71exit : Int -> IO ()

73exit : Int -> IO ()

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

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

73

75

76+||| Get the Unix time

77+time : IO Int

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

79+

74usleep : Int -> IO ()

80usleep : Int -> IO ()

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

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

76

82

libs/neweffects/Effect/Random.idr+8

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

20rndInt lower upper = do v <- getRandom

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

22

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+

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

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

24srand n = setSeed n

32srand n = setSeed n

25

33

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,

5

6 Effect.Exception, Effect.File, Effect.State,

7 Effect.Random, Effect.StdIO, Effect.Select,

8− Effect.Memory

8+ Effect.Memory, Effect.System

9

libs/prelude/Builtins.idr+22−8

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

3%access public

4%default total

5

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

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

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

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

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

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

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

8

11

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

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

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

10getWitness (a ** v) = a

14getWitness (a ** v) = a

11

15

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

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

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

13getProof (a ** v) = v

18getProof (a ** v) = v

14

19

15FalseElim : _|_ -> a

20FalseElim : _|_ -> a

16

21

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

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

18data Symbol_ : String -> Type where

23data Symbol_ : String -> Type where

19

24

20-- ------------------------------------------------------ [ For rewrite tactic ]

25-- ------------------------------------------------------ [ For rewrite tactic ]

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

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

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

22replace refl prf = prf

28replace refl prf = prf

23

29

30+||| Symmetry of propositional equality

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

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

25sym refl = refl

32sym refl = refl

26

33

34+||| Transitivity of propositional equality

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

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

28trans refl refl = refl

36trans refl refl = refl

29

37

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

48trace_malloc : a -> a

56trace_malloc : a -> a

49trace_malloc x = x -- compiled specially

57trace_malloc x = x -- compiled specially

50

58

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

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

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

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)

53−assert_smaller : a -> a -> a

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

54assert_smaller x y = y

64assert_smaller x y = y

55

65

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

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

57−-- terminate.

67+||| terminate.

58assert_total : a -> a

68assert_total : a -> a

59assert_total x = x

69assert_total x = x

60

70

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!

61abstract %assert_total -- need to pretend

73abstract %assert_total -- need to pretend

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

74+believe_me : a -> b

63believe_me x = prim__believe_me _ _ x

75believe_me x = prim__believe_me _ _ x

64

76

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

66really_believe_me : a -> b

80really_believe_me : a -> b

67really_believe_me x = prim__believe_me _ _ x

81really_believe_me x = prim__believe_me _ _ x

68

82

libs/prelude/IO.idr+8

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

32 | FFloat

33 | FString

34 | FPtr

35+ | FManagedPtr

35 | FAny Type

36 | FAny Type

36 | FUnit

37 | FUnit

37

38

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

85interpFTy FFloat = Float

86interpFTy FFloat = Float

86interpFTy FString = String

87interpFTy FString = String

87interpFTy FPtr = Ptr

88interpFTy FPtr = Ptr

89+interpFTy FManagedPtr = ManagedPtr

88interpFTy (FIntT IT8x16) = Bits8x16

90interpFTy (FIntT IT8x16) = Bits8x16

89interpFTy (FIntT IT16x8) = Bits16x8

91interpFTy (FIntT IT16x8) = Bits16x8

90interpFTy (FIntT IT32x4) = Bits32x4

92interpFTy (FIntT IT32x4) = Bits32x4

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

106mkLazyForeignPrim : Foreign x -> x

108mkLazyForeignPrim : Foreign x -> x

107-- mkForeign and mkLazyForeign compiled as primitives

109-- mkForeign and mkLazyForeign compiled as primitives

108

110

111+registerPtr : Ptr -> Int -> ManagedPtr

112+registerPtr = prim__registerPtr

113+

109abstract

114abstract

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

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

111io_bind (MkIO fn) k

116io_bind (MkIO fn) k

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

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

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

150

155

151

156

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 $>

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

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

21

22+||| Lift a function to an applicative

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

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

23liftA f a = pure f <$> a

24liftA f a = pure f <$> a

24

25

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

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

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

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

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

27

29

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

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

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

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

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

30

33

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

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

3Not : Type -> Type

4Not a = a -> _|_

5

6−-- | Identity function.

6+||| Identity function.

7id : a -> a

8id x = x

9

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

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

11+||| @ a the type to assign

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

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

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

12the _ = id

14the _ = id

13

15

14−-- | Constant function.

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

15const : a -> b -> a

17const : a -> b -> a

16const x = \v => x

18const x = \v => x

17

19

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

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

19fst : (s, t) -> s

21fst : (s, t) -> s

20fst (x, y) = x

22fst (x, y) = x

21

23

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

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

23snd : (a, b) -> b

25snd : (a, b) -> b

24snd (x, y) = y

26snd (x, y) = y

25

27

26infixl 9 .

28infixl 9 .

27

29

28−-- | Function composition

30+||| Function composition

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

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

30(.) f g x = f (g x)

32(.) f g x = f (g x)

31

33

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

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

35+||| @ f the function to flip

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

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

34flip f x y = f y x

37flip f x y = f y x

35

38

36−-- | Function application.

39+||| Function application.

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

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

38apply f a = f a

41apply f a = f a

39

42

43+||| Equality is a congruence.

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

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

41cong refl = refl

45cong refl = refl

42

46

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

43data Dec : Type -> Type where

48data Dec : Type -> Type where

49+

50+ ||| The case where the property holds

51+ ||| @ prf the proof

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

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

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

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

46

57

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

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

8%default total

9

10

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−

18b8ToString : Bits8 -> String

11b8ToString : Bits8 -> String

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

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

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

13+ where getDigit : Bits8 -> Char

21− toFin16 : Bits8 -> Fin 16

14+ getDigit b = let n = prim__zextB8_Int b in

22− toFin16 n = if n == 0

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

23− then fZ

16+ then '0' `prim__addChar` cast n

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

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

25− c1 = toHexDigit upper where

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

26− upper : Fin 16

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

27− upper = toFin16 (prim__lshrB8 c 4)

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

28− c2 = toHexDigit lower where

29− lower : Fin 16

30− lower = toFin16 (prim__andB8 c 0xf)

21+ c2 = getDigit (prim__andB8 c 15)

22+

31

23

32b16ToString : Bits16 -> String

24b16ToString : Bits16 -> String

33b16ToString c = c1 ++ c2 where

25b16ToString c = c1 ++ c2 where

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

42b32ToString c = c1 ++ c2 where

34b32ToString c = c1 ++ c2 where

43 c1 = b16ToString upper where

35 c1 = b16ToString upper where

44 upper : Bits16

36 upper : Bits16

45− upper = prim__truncB32_B16 (prim__lshrB32 c 16)

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

46 c2 = b16ToString lower where

38 c2 = b16ToString lower where

47 lower : Bits16

39 lower : Bits16

48 lower = prim__truncB32_B16 c

40 lower = prim__truncB32_B16 c

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

51b64ToString c = c1 ++ c2 where

43b64ToString c = c1 ++ c2 where

52 c1 = b32ToString upper where

44 c1 = b32ToString upper where

53 upper : Bits32

45 upper : Bits32

54− upper = prim__truncB64_B32 (prim__lshrB64 c 32)

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

55 c2 = b32ToString lower where

47 c2 = b32ToString lower where

56 lower : Bits32

48 lower : Bits32

57 lower = prim__truncB64_B32 c

49 lower = prim__truncB64_B32 c

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

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

1module Prelude.Bool

2

3−-- | Boolean Data Type

3+||| Boolean Data Type

4data Bool = False | True

5

6−-- | Boolean elimination

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

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

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

8boolElim True t e = t

11boolElim True t e = t

9boolElim False t e = e

12boolElim False t e = e

10

13

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.

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

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

13

16

14-- Syntaxtic sugar for boolean elimination.

17-- Syntaxtic sugar for boolean elimination.

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

17-- Boolean Operator Precedence

20-- Boolean Operator Precedence

18infixl 4 &&, ||

21infixl 4 &&, ||

19

22

20−-- | Boolean OR

23+||| Boolean OR

21(||) : Bool -> Bool -> Bool

24(||) : Bool -> Bool -> Bool

22(||) False x = x

25(||) False x = x

23(||) True _ = True

26(||) True _ = True

24

27

25−-- | Boolean AND

28+||| Boolean AND

26(&&) : Bool -> Bool -> Bool

29(&&) : Bool -> Bool -> Bool

27(&&) True x = x

30(&&) True x = x

28(&&) False _ = False

31(&&) False _ = False

29

32

30−-- | Boolean NOT

33+||| Boolean NOT

31not : Bool -> Bool

34not : Bool -> Bool

32not True = False

35not True = False

33not False = True

36not False = True

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

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

3

4import Builtins

5

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

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

7chr : Int -> Char

8chr x = prim__intToChar x

9

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

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

11ord : Char -> Int

12ord x = prim__charToInt x

13

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

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

15isUpper : Char -> Bool

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

17

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

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

19isLower : Char -> Bool

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

21

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].

23isAlpha : Char -> Bool

24isAlpha x = isUpper x || isLower x

25

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

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

27isDigit : Char -> Bool

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

29

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]

31isAlphaNum : Char -> Bool

32isAlphaNum x = isDigit x || isAlpha x

33

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

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

35isSpace : Char -> Bool

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

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

38 x == '\xa0'

39

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

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

41isNL : Char -> Bool

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

43

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

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

45−-- Non-letters are ignored.

45+||| Non-letters are ignored.

46toUpper : Char -> Char

47toUpper x = if (isLower x)

48 then (prim__intToChar (prim__charToInt x - 32))

49 else x

50

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

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

52−-- Non-letters are ignored.

52+||| Non-letters are ignored.

53toLower : Char -> Char

54toLower x = if (isUpper x)

55 then (prim__intToChar (prim__charToInt x + 32))

56 else x

57

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]

59isHexDigit : Char -> Bool

60isHexDigit x = elem (toUpper x) hexChars where

61 hexChars : List Char

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

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

64

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

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

66isOctDigit : Char -> Bool

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

68

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

69+

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

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

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

21

22-- ---------------------------------------------------------- [ Equality Class ]

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

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

24class Eq a where

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

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

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

65 GT == GT = True

66 _ == _ = False

67

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

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

69class Eq a => Ord a where

70 compare : a -> a -> Ordering

71

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

131 else compare xr yr

132

133-- --------------------------------------------------------- [ Numerical Class ]

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

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

135class Num a where

136 (+) : a -> a -> a

137 (-) : a -> a -> a

138 (*) : a -> a -> a

139− -- | Absolute value

139+ ||| Absolute value

140 abs : a -> a

141− -- | Conversion from Integer.

141+ ||| Conversion from Integer.

142 fromInteger : Integer -> a

143

144instance Num Integer where

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

245-- ------------------------------------------------------------- [ Bounded ]

246

247class MinBound b where

248− -- | The lower bound for the type

248+ ||| The lower bound for the type

249 minBound : b

250

251class MaxBound b where

252− -- | The upper bound for the type

252+ ||| The upper bound for the type

253 maxBound : b

254

255instance MinBound Bits16 where

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

273

274-- ------------------------------------------------------------- [ Fractionals ]

275

276−-- | Fractional division of two Floats.

276+||| Fractional division of two Floats.

277(/) : Float -> Float -> Float

278(/) = prim__divFloat

279

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

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

1−module Prelude.Either

1+ module Prelude.Either

2

3import Builtins

4

5import Prelude.Maybe

6import Prelude.List

7

8+||| A sum type

8−data Either a b

9+data Either a b =

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

9− = Left a

11+ Left a |

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

10− | Right b

13+ Right b

11

14

12--------------------------------------------------------------------------------

15--------------------------------------------------------------------------------

13-- Syntactic tests

16-- Syntactic tests

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

25-- Misc.

28-- Misc.

26--------------------------------------------------------------------------------

29--------------------------------------------------------------------------------

27

30

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

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

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

29choose True = Left oh

33choose True = Left oh

30choose False = Right oh

34choose False = Right oh

31

35

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

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

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

33either l r (Left x) = l x

41either l r (Left x) = l x

34either l r (Right x) = r x

42either l r (Right x) = r x

35

43

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

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

5

6%default total

7

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

9+||| @ n the upper bound

8−data Fin : Nat -> Type where

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

9 fZ : Fin (S k)

11 fZ : Fin (S k)

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

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

11

13

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

44instance Cast (Fin n) Integer where

46instance Cast (Fin n) Integer where

45 cast x = finToInteger x

47 cast x = finToInteger x

46

48

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

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

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

48weaken fZ = fZ

51weaken fZ = fZ

49weaken (fS k) = fS (weaken k)

52weaken (fS k) = fS (weaken k)

50

53

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

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

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

52weakenN n fZ = fZ

56weakenN n fZ = fZ

53weakenN n (fS f) = fS (weakenN n f)

57weakenN n (fS f) = fS (weakenN n f)

54

58

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

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

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

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

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

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

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

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

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

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

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

60strengthen f = Left f

66strengthen f = Left f

61

67

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

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

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

63shift Z f = f

72shift Z f = f

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

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

65

74

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

66last : Fin (S n)

76last : Fin (S n)

67last {n=Z} = fZ

77last {n=Z} = fZ

68last {n=S _} = fS last

78last {n=S _} = fS last

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

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

1module Prelude.Functor

2

3+||| Functors

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

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

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

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

7+ ||| @ f the functor

8+ ||| @ m the morphism

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

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

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

270intercalate sep l = concat $ intersperse sep l

271

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+

272--------------------------------------------------------------------------------

289--------------------------------------------------------------------------------

273-- Membership tests

290-- Membership tests

274--------------------------------------------------------------------------------

291--------------------------------------------------------------------------------

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

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

10%access public

11%default total

12

13+||| Unary natural numbers

13−%elim data Nat

14+%elim data Nat =

15+ ||| Zero

14− = Z

16+ Z |

17+ ||| Successor

15− | S Nat

18+ S Nat

16

19

17-- name hints for interactive editing

20-- name hints for interactive editing

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

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

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

33-- Basic arithmetic functions

36-- Basic arithmetic functions

34--------------------------------------------------------------------------------

37--------------------------------------------------------------------------------

35

38

39+||| Add two natural numbers.

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

41+||| @ m the other number

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

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

37plus Z right = right

43plus Z right = right

38plus (S left) right = S (plus left right)

44plus (S left) right = S (plus left right)

39

45

46+||| Multiply natural numbers

40total mult : Nat -> Nat -> Nat

47total mult : Nat -> Nat -> Nat

41mult Z right = Z

48mult Z right = Z

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

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

43

50

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

44fromIntegerNat : Integer -> Nat

52fromIntegerNat : Integer -> Nat

45fromIntegerNat 0 = Z

53fromIntegerNat 0 = Z

46fromIntegerNat n =

54fromIntegerNat n =

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

49 else

57 else

50 Z

58 Z

51

59

60+||| Convert a Nat to an Integer

52toIntegerNat : Nat -> Integer

61toIntegerNat : Nat -> Integer

53toIntegerNat Z = 0

62toIntegerNat Z = 0

54toIntegerNat (S k) = 1 + toIntegerNat k

63toIntegerNat (S k) = 1 + toIntegerNat k

55

64

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

56total minus : Nat -> Nat -> Nat

66total minus : Nat -> Nat -> Nat

57minus Z right = Z

67minus Z right = Z

58minus left Z = left

68minus left Z = left

59minus (S left) (S right) = minus left right

69minus (S left) (S right) = minus left right

60

70

71+||| Exponentiation of natural numbers

61total power : Nat -> Nat -> Nat

72total power : Nat -> Nat -> Nat

62power base Z = S Z

73power base Z = S Z

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

74power 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)

74-- Comparisons

85-- Comparisons

75--------------------------------------------------------------------------------

86--------------------------------------------------------------------------------

76

87

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

89+||| @ n the smaller number

90+||| @ m the larger number

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

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

92+ ||| Zero is the smallest Nat

78 lteZero : LTE Z right

93 lteZero : LTE Z right

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

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

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

80

96

97+||| Greater than or equal to

81total GTE : Nat -> Nat -> Type

98total GTE : Nat -> Nat -> Type

82GTE left right = LTE right left

99GTE left right = LTE right left

83

100

101+||| Strict less than

84total LT : Nat -> Nat -> Type

102total LT : Nat -> Nat -> Type

85LT left right = LTE (S left) right

103LT left right = LTE (S left) right

86

104

105+||| Strict greater than

87total GT : Nat -> Nat -> Type

106total GT : Nat -> Nat -> Type

88GT left right = LT right left

107GT left right = LT right left

89

108

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

90total lte : Nat -> Nat -> Bool

110total lte : Nat -> Nat -> Bool

91lte Z right = True

111lte Z right = True

92lte left Z = False

112lte left Z = False

93lte (S left) (S right) = lte left right

113lte (S left) (S right) = lte left right

94

114

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

95total gte : Nat -> Nat -> Bool

116total gte : Nat -> Nat -> Bool

96gte left right = lte right left

117gte left right = lte right left

97

118

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

98total lt : Nat -> Nat -> Bool

120total lt : Nat -> Nat -> Bool

99lt left right = lte (S left) right

121lt left right = lte (S left) right

100

122

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

101total gt : Nat -> Nat -> Bool

124total gt : Nat -> Nat -> Bool

102gt left right = lt right left

125gt left right = lt right left

103

126

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

104total minimum : Nat -> Nat -> Nat

128total minimum : Nat -> Nat -> Nat

105minimum left right =

129minimum left right =

106 if lte left right then

130 if lte left right then

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

108 else

132 else

109 right

133 right

110

134

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

111total maximum : Nat -> Nat -> Nat

136total maximum : Nat -> Nat -> Nat

112maximum left right =

137maximum left right =

113 if lte left right then

138 if lte left right then

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

148instance Cast Integer Nat where

173instance Cast Integer Nat where

149 cast = fromInteger

174 cast = fromInteger

150

175

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

151record Multiplicative : Type where

177record Multiplicative : Type where

152 getMultiplicative : Nat -> Multiplicative

178 getMultiplicative : Nat -> Multiplicative

153

179

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

154record Additive : Type where

181record Additive : Type where

155 getAdditive : Nat -> Additive

182 getAdditive : Nat -> Additive

156

183

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

210-- Auxilliary notions

237-- Auxilliary notions

211--------------------------------------------------------------------------------

238--------------------------------------------------------------------------------

212

239

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

213total pred : Nat -> Nat

241total pred : Nat -> Nat

214pred Z = Z

242pred Z = Z

215pred (S n) = n

243pred (S n) = n

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

218-- Fibonacci and factorial

246-- Fibonacci and factorial

219--------------------------------------------------------------------------------

247--------------------------------------------------------------------------------

220

248

249+||| Fibonacci numbers

221total fib : Nat -> Nat

250total fib : Nat -> Nat

222fib Z = Z

251fib Z = Z

223fib (S Z) = S Z

252fib (S Z) = S Z

224fib (S (S n)) = fib (S n) + fib n

253fib (S (S n)) = fib (S n) + fib n

225

254

255+||| Factorial function

226total fact : Nat -> Nat

256total fact : Nat -> Nat

227fact Z = S Z

257fact Z = S Z

228fact (S n) = (S n) * fact n

258fact (S n) = (S n) * fact n

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

283--------------------------------------------------------------------------------

313--------------------------------------------------------------------------------

284

314

285-- Succ

315-- Succ

316+

317+||| S preserves equality

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

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

287 S left = S right

319 S left = S right

288eqSucc left _ refl = refl

320eqSucc left _ refl = refl

289

321

322+||| S is injective

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

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

291 left = right

324 left = right

292succInjective left _ refl = refl

325succInjective left _ refl = refl

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

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

6%access public

7%default total

8

9+||| An infinite stream

9codata Stream : Type -> Type where

10codata Stream : Type -> Type where

10 (::) : a -> Stream a -> Stream a

11 (::) : a -> Stream a -> Stream a

11

12

12instance Functor Stream where

13instance Functor Stream where

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

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

14

15

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

15head : Stream a -> a

17head : Stream a -> a

16head (x::xs) = x

18head (x::xs) = x

17

19

20+||| All but the first element

18tail : Stream a -> Stream a

21tail : Stream a -> Stream a

19tail (x::xs) = xs

22tail (x::xs) = xs

20

23

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

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

26+||| @ xs the stream

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

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

22take Z _ = []

28take Z _ = []

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

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

24

30

25%assert_total

31%assert_total

26drop : Nat -> Stream a -> Stream a

32drop : Nat -> Stream a -> Stream a

27−drop Z xs = xs

33+drop Z xs = xs

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

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

29

35

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

30repeat : a -> Stream a

37repeat : a -> Stream a

31repeat x = x :: repeat x

38repeat x = x :: repeat x

32

39

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

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

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

34iterate f x = x :: iterate f (f x)

44iterate f x = x :: iterate f (f x)

35

45

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

36index : Nat -> Stream a -> a

47index : Nat -> Stream a -> a

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

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

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

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

39

50

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

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

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

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

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

42

54

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

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

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

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

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

45

58

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

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

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

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

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

48

62

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

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

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

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

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

51

66

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

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

7import Prelude.Either

8import Prelude.Foldable

9

10−-- | Appends two strings together.

10+||| Appends two strings together.

11(++) : String -> String -> String

12(++) = prim__concat

13

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

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

15partial

16strHead : String -> Char

17strHead = prim__strHead

18

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

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

20partial

21strTail : String -> String

22strTail = prim__strTail

23

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

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

25strCons : Char -> String -> String

26strCons = prim__strCons

27

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

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

29partial

30strIndex : String -> Int -> Char

31strIndex = prim__strIndex

32

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

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

34reverse : String -> String

35reverse = prim__strRev

36

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

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

1module Prelude.Uninhabited

2

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

3class Uninhabited t where

4class Uninhabited t where

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

6+ ||| @ t the uninhabited type

4 total uninhabited : t -> _|_

7 total uninhabited : t -> _|_

5

8

6instance Uninhabited (Fin Z) where

9instance Uninhabited (Fin Z) where

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

10instance Uninhabited (Z = S n) where

13instance Uninhabited (Z = S n) where

11 uninhabited refl impossible

14 uninhabited refl impossible

12

15

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

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

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

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

15−absurd t = FalseElim (uninhabited t)

21+absurd h = FalseElim (uninhabited h)

rts/Makefile+12−4

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

1include ../config.mk

2

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

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

4− idris_bitstring.o idris_net.o idris_opts.o idris_stats.o mini-gmp.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_stdfgn.h \

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

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

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

7CFLAGS:=-fPIC $(CFLAGS)

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

9

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+

10LIBTARGET = libidris_rts.a

18LIBTARGET = libidris_rts.a

11

19

12build: $(LIBTARGET) $(DYLIBTARGET)

20build: $(LIBTARGET) $(DYLIBTARGET)

rts/idris_gc.c+3

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

36 case PTR:

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

38 break;

39+ case MANAGEDPTR:

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

41+ break;

39 case BITS8:

42 case BITS8:

40 cl = idris_b8CopyForGC(vm, x);

43 cl = idris_b8CopyForGC(vm, x);

41 break;

44 break;

rts/idris_rts.c+25

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

178 return cl;

179}

180

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+

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

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

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

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

183 SETTY(cl, FLOAT);

194 SETTY(cl, FLOAT);

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

202 return cl;

213 return cl;

203}

214}

204

215

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+

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

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

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

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

207 SETTY(cl, BITS8);

229 SETTY(cl, BITS8);

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

795 case PTR:

817 case PTR:

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

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

797 break;

819 break;

820+ case MANAGEDPTR:

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

822+ break;

798 case BITS8:

823 case BITS8:

799 cl = idris_b8CopyForGC(vm, x);

824 cl = idris_b8CopyForGC(vm, x);

800 break;

825 break;

rts/idris_rts.h+10−1

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

17typedef enum {

18 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,

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

20− BUFFER

20+ MANAGEDPTR, BUFFER

21} ClosureType;

22

23typedef struct Closure *VAL;

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

40 unsigned char store[];

41} Buffer;

42

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

44+typedef struct {

45+ size_t size;

46+ void* data;

47+} ManagedPtr;

43

48

44typedef struct Closure {

49typedef struct Closure {

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

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

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

57 uint32_t bits32;

62 uint32_t bits32;

58 uint64_t bits64;

63 uint64_t bits64;

59 Buffer* buf;

64 Buffer* buf;

65+ ManagedPtr* mptr;

60 } info;

66 } info;

61} Closure;

67} Closure;

62

68

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

112

118

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

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

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

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

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

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

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

116

123

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

124#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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

177

186

178char* GETSTROFF(VAL stroff);

187char* GETSTROFF(VAL stroff);

rts/idris_stdfgn.c+11

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

1#include "idris_stdfgn.h"

2#include "idris_rts.h"

3+#include "idris_gc.h"

3#include <sys/select.h>

4#include <sys/select.h>

4#include <fcntl.h>

5#include <fcntl.h>

5#include <stdio.h>

6#include <stdio.h>

7+#include <time.h>

6

8

7extern char** environ;

9extern char** environ;

8

10

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

73char* getEnvPair(int i) {

75char* getEnvPair(int i) {

74 return *(environ + i);

76 return *(environ + i);

75}

77}

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();

21

22char* getEnvPair(int i);

23

24+int idris_time();

25+

26+void idris_forceGC();

27+

24#endif

28#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

2

3import Language.Reflection

4

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

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

6reflectVal : TT

7reflectVal = ?valPrf

8

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

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

10applyTac1 : Int

11applyTac1 = ?tacPrf1

12

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

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

14applyTac0 : Int

15applyTac0 = ?tacPrf0

16

17−-- | intEq for the two arguments

17+||| intEq for the two arguments

18applyTacDyn : Int -> Int -> Int

19applyTacDyn x y = ?tacPrfDyn

20

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

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

22fill : Int

23fill = ?fillPrf

24

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

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

26envTuple : Type

27envTuple = ?envTuplePrf

28

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

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

30envList : List (TTName, TT)

31envList = ?envListPrf

32

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

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

34tupleType : Raw

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

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

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

38

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

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

40mkTuple : Raw

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

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

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

44

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

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

46nil : Raw

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

48

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

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

50cons : Raw

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

52

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

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

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

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

55−-- demo purposes.

55+||| demo purposes.

56intEq : Int -> Int -> Int

57intEq x y = case x == y of

58 True => 1

59 False => 0

60

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

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

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

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

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

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

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

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

67

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

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

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

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

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

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

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

73

74−-- | Returns the reflected representation of innerTac

74+||| Returns the reflected representation of innerTac

75innerTacTT : TT

76innerTacTT = ?innerTacTTPrf

77

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

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

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

80dispatch xs _ = ApplyTactic (innerTacTT)

81

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

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

83tacticalDispatch : Int -> Int

84tacticalDispatch = ?tacticalDispatchPrf

85

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

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

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

88studyGoalTac _ goal = Reflect goal

89

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

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

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

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

92studyGoal : TT

93studyGoal = ?studyGoalPrf

94

src/IRTS/CodegenC.hs+4

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

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

263c_irts FUnit l x = x

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

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

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

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

266c_irts FAny l x = l ++ x

267c_irts FAny l x = l ++ x

267

268

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

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

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

273irts_c FUnit x = x

274irts_c FUnit x = x

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

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

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

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

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

276irts_c FAny x = x

278irts_c FAny x = x

277

279

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/IRTS/CodegenJava.hs+3−8

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

365

366addMainMethod :: [Decl] -> [Decl]

367addMainMethod decls

368− | findMain decls = mkMainMethod : decls

368+ | findMainMethod decls = mkMainMethod : decls

369 | otherwise = decls

370 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"))

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

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

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

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

379 findMainMethod (_:decls) = findMainMethod decls

373 findMainMethod (_:decls) = findMainMethod decls

380 findMainMethod [] = False

374 findMainMethod [] = False

381

375

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

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

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

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

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

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

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

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

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

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

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

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

712

707

src/IRTS/CodegenJavaScript.hs+113−66

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

20import System.IO

21import System.Directory

22

23+

23idrNamespace :: String

24idrNamespace :: String

24idrNamespace = "__IDR__"

25idrNamespace = "__IDR__"

25idrRTNamespace = "__IDRRT__"

26idrRTNamespace = "__IDRRT__"

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

52 deriving Eq

53 deriving Eq

53

54

55

56+data JSAnnotation = JSConstructor deriving Eq

57+

58+

59+instance Show JSAnnotation where

60+ show JSConstructor = "constructor"

61+

62+

55data JS = JSRaw String

63data JS = JSRaw String

56 | JSIdent String

64 | JSIdent String

57 | JSFunction [String] JS

65 | JSFunction [String] JS

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

80 | JSTernary JS JS JS

88 | JSTernary JS JS JS

81 | JSParens JS

89 | JSParens JS

82 | JSWhile JS JS

90 | JSWhile JS JS

91+ | JSFFI String [JS]

92+ | JSAnnotation JSAnnotation JS

83 | JSNoop

93 | JSNoop

84 deriving Eq

94 deriving Eq

85

95

86

96

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+

87compileJS :: JS -> String

132compileJS :: JS -> String

88compileJS JSNoop = ""

133compileJS JSNoop = ""

89

134

135+compileJS (JSAnnotation annotation js) =

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

137+

138+compileJS (JSFFI raw args) =

139+ ffi raw (map compileJS args)

140+

90compileJS (JSRaw code) =

141compileJS (JSRaw code) =

91 code

142 code

92

143

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

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

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

317 | JSWhile cond body <- js =

368 | JSWhile cond body <- js =

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

369 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

319 | otherwise =

374 | otherwise =

320 tr js

375 tr js

321

376

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

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

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

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

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

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

399 | 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)

346 | otherwise = js

403 | otherwise = js

347

404

348

405

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

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

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

351 where

408 where

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

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

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

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

412+

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

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

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

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

355

415

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

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

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

520 match js = transformJS match js

580 match js = transformJS match js

521

581

522− removeEvalApp js = js

523−

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

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

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

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

526 where

584 where

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

664 inlineHelper ([], js)

722 inlineHelper ([], js)

665 where

723 where

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

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

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

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

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

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

669 inlineHelper (front, back)

727 inlineHelper (front, back)

670 | Just new <- inlineAble (

728 | Just new <- inlineAble (

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

1012 adaptCon js =

1070 adaptCon js =

1013 adaptCon' [] js

1071 adaptCon' [] js

1014 where

1072 where

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

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

1016 front ++ (new:back)

1074 front ++ (new:back)

1017

1075

1018 adaptCon' front (next:back) =

1076 adaptCon' front (next:back) =

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

1022

1080

1023

1081

1024 new =

1082 new =

1083+ JSAnnotation JSConstructor $

1025− JSAlloc "__IDRRT__Con" (Just $

1084+ JSAlloc "__IDRRT__Con" (Just $

1026− JSFunction newArgs (

1085+ JSFunction newArgs (

1027− JSSeq (map newVar newArgs)

1086+ JSSeq (map newVar newArgs)

1087+ )

1028 )

1088 )

1029− )

1030 where

1089 where

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

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

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

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

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

1338 -> OutputType

1397 -> OutputType

1339 -> IO ()

1398 -> IO ()

1340codegenJavaScript target definitions includes filename outputType = do

1399codegenJavaScript target definitions includes filename outputType = do

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

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

1342 Node ->

1401 Node ->

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

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

1344 JavaScript ->

1403 JavaScript ->

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

1346 included <- getIncludes includes

1405 included <- getIncludes includes

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

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

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

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

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

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

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

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

1351 writeFile filename $ header ++ (

1410 writeFile filename $ header ++ (

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

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

1353− , idrRuntime

1354− , tgtRuntime

1355− ] ++ functions

1356 )

1412 )

1357

1413

1358 setPermissions filename (emptyPermissions { readable = True

1414 setPermissions filename (emptyPermissions { readable = True

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

1364 def = map (first translateNamespace) definitions

1420 def = map (first translateNamespace) definitions

1365

1421

1366

1422

1367− functions :: [String]

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]

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

1443+ optimized = translate >>> optimize $ def

1369 where

1444 where

1370 translate p =

1445 translate p =

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

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

1372 optimize p =

1447 optimize p =

1373 foldl' (flip ($)) p opt

1448 foldl' (flip ($)) p opt

1374− compile =

1375− map compileJS

1376

1449

1377 opt =

1450 opt =

1378 [ removeEval

1451 [ removeEval

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

1394 , evalCons

1467 , evalCons

1395 ]

1468 ]

1396

1469

1470+ functions :: [String]

1471+ functions = map compileJS optimized

1472+

1397 prelude :: [JS]

1473 prelude :: [JS]

1398 prelude =

1474 prelude =

1475+ [ JSAnnotation JSConstructor $

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

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

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

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

1401− ))

1478+ ))

1479+ , JSAnnotation JSConstructor $

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

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

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

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

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

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

1405− ]

1483+ ]

1406− ))

1484+ ))

1407 ]

1485 ]

1408

1486

1409 mainLoop :: JS

1487 mainLoop :: JS

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

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

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

1888

1966

1889translateExpression (SForeign _ _ fun args) =

1967translateExpression (SForeign _ _ fun args) =

1890− ffi fun (map generateWrapper args)

1968+ JSFFI fun (map generateWrapper args)

1891 where

1969 where

1892 generateWrapper (ffunc, name)

1970 generateWrapper (ffunc, name)

1893 | FFunction <- ffunc =

1971 | FFunction <- ffunc =

1972+ JSApp (

1973+ JSIdent $ idrRTNamespace ++ "ffiWrap"

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

1974+ ) [JSIdent $ translateVariableName name]

1895 | FFunctionIO <- ffunc =

1975 | FFunctionIO <- ffunc =

1976+ JSApp (

1977+ JSIdent $ idrRTNamespace ++ "ffiWrap"

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

1978+ ) [JSIdent $ translateVariableName name]

1897

1979

1898 generateWrapper (_, name) =

1980 generateWrapper (_, name) =

1899− translateVariableName name

1981+ JSIdent $ translateVariableName name

1900

1982

1901translateExpression patterncase

1983translateExpression patterncase

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

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

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

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

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

1940

2022

1941

2023

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−

1977data CaseType = ConCase Int

2024data CaseType = ConCase Int

1978 | TypeCase JSType

2025 | TypeCase JSType

1979 | DefaultCase

2026 | DefaultCase

src/IRTS/Compiler.hs+1

@@ -349,6 +349,7 @@ mkIty "FBits32" = mkIntIty "IT32"

349mkIty "FBits64" = mkIntIty "IT64"

350mkIty "FString" = FString

351mkIty "FPtr" = FPtr

352+mkIty "FManagedPtr" = FManagedPtr

352mkIty "FUnit" = FUnit

353mkIty "FUnit" = FUnit

353mkIty "FFunction" = FFunction

354mkIty "FFunction" = FFunction

354mkIty "FFunctionIO" = FFunctionIO

355mkIty "FFunctionIO" = FFunctionIO

src/IRTS/Lang.hs+2

@@ -66,6 +66,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

66 -- core or another machine. 'id' is a valid implementation

67 | LVMPtr

68 | LNullPtr

69+ | LRegisterPtr

69 | LNoOp

70 | LNoOp

70 deriving (Show, Eq)

71 deriving (Show, Eq)

71

72

@@ -83,6 +84,7 @@ data FType = FArith ArithTy

83 | FString

84 | FString

84 | FUnit

85 | FUnit

85 | FPtr

86 | FPtr

87+ | FManagedPtr

86 | FAny

88 | FAny

87 deriving (Show, Eq)

89 deriving (Show, Eq)

88

90

src/Idris/AbsSyntax.hs+65−51

@@ -262,10 +262,10 @@ addCoercion :: Name -> Idris ()

262addCoercion n = do i <- getIState

263 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

264

265−addDocStr :: Name -> String -> Idris ()

265+addDocStr :: Name -> String -> [(Name, String)] -> Idris ()

266−addDocStr n doc

266+addDocStr n doc args

267 = 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) }

269

270addNameHint :: Name -> Name -> Idris ()

271addNameHint ty n

@@ -460,6 +460,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)

460addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

461addDeferred' nt ns

462 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

463+ mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

463 i <- getIState

464 i <- getIState

464 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

465 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

465 idris_metavars i }

466 idris_metavars i }

@@ -475,7 +476,12 @@ solveDeferred :: Name -> Idris ()

475solveDeferred n = do i <- getIState

476solveDeferred n = do i <- getIState

476 putIState $ i { idris_metavars =

477 putIState $ i { idris_metavars =

477 filter (\(n', _) -> n/=n')

478 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

479

485

480getUndefined :: Idris [Name]

486getUndefined :: Idris [Name]

481getUndefined = do i <- getIState

487getUndefined = do i <- getIState

@@ -993,12 +999,12 @@ expandParams dec ps ns infs tm = en tm

993expandParamsD :: Bool -> -- True = RHS only

999expandParamsD :: Bool -> -- True = RHS only

994 IState ->

1000 IState ->

995 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

1001 (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)

997 = if n `elem` ns && (not rhsonly)

1003 = if n `elem` ns && (not rhsonly)

998 then -- trace (show (n, expandParams dec ps ns ty)) $

1004 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))

1000 else --trace (show (n, expandParams dec ps ns ty)) $

1006 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)

1002expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

1008expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

1003 = if n `elem` ns && (not rhsonly)

1009 = if n `elem` ns && (not rhsonly)

1004 then -- trace (show (n, expandParams dec ps ns ty)) $

1010 then -- trace (show (n, expandParams dec ps ns ty)) $

@@ -1044,8 +1050,8 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

1044 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r

1050 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r

1045 bnames _ = []

1051 bnames _ = []

1046

1052

1047−expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

1053+expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

1048− = PData doc syn fc co (expandPData pd)

1054+ = PData doc argDocs syn fc co (expandPData pd)

1049 where

1055 where

1050 -- just do the type decl, leave constructors alone (parameters will be

1056 -- just do the type decl, leave constructors alone (parameters will be

1051 -- added implicitly)

1057 -- added implicitly)

@@ -1054,8 +1060,15 @@ expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

1054 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))

1060 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))

1055 (map econ cons)

1061 (map econ cons)

1056 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1062 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1057− econ (doc, n, t, fc, fs)

1063+ econ (doc, argDocs, n, t, fc, fs)

1058− = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] 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)

1059expandParamsD rhs ist dec ps ns (PParams f params pds)

1072expandParamsD rhs ist dec ps ns (PParams f params pds)

1060 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

1073 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

1061 (map (expandParamsD True ist dec ps ns) pds)

1074 (map (expandParamsD True ist dec ps ns) pds)

@@ -1112,6 +1125,7 @@ getPriority i tm = 1 -- pri tm

1112 pri Placeholder = 1

1125 pri Placeholder = 1

1113 pri _ = 3

1126 pri _ = 3

1114

1127

1128+

1115addStatics :: Name -> Term -> PTerm -> Idris ()

1129addStatics :: Name -> Term -> PTerm -> Idris ()

1116addStatics n tm ptm =

1130addStatics n tm ptm =

1117 do let (statics, dynamics) = initStatics tm ptm

1131 do let (statics, dynamics) = initStatics tm ptm

@@ -1145,8 +1159,8 @@ addStatics n tm ptm =

1145 -- if a name appears in a type class or tactic implicit index, it doesn't

1159 -- if a name appears in a type class or tactic implicit index, it doesn't

1146 -- affect its 'uniquely inferrable' from a static status since these are

1160 -- affect its 'uniquely inferrable' from a static status since these are

1147 -- resolved by searching.

1161 -- resolved by searching.

1148− searchArg (Constraint _ _ _) = True

1162+ searchArg (Constraint _ _) = True

1149− searchArg (TacImp _ _ _ _) = True

1163+ searchArg (TacImp _ _ _) = True

1150 searchArg _ = False

1164 searchArg _ = False

1151

1165

1152 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

1166 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

@@ -1173,14 +1187,14 @@ addUsingConstraints syn fc t

1173 -- if all of args in ns, then add it

1187 -- if all of args in ns, then add it

1174 doAdd (UConstraint c args : cs) ns t

1188 doAdd (UConstraint c args : cs) ns t

1175 | all (\n -> elem n ns) args

1189 | all (\n -> elem n ns) args

1176− = PPi (Constraint [] Dynamic "") (sMN 0 "cu")

1190+ = PPi (Constraint [] Dynamic) (sMN 0 "cu")

1177 (mkConst c args) (doAdd cs ns t)

1191 (mkConst c args) (doAdd cs ns t)

1178 | otherwise = doAdd cs ns t

1192 | otherwise = doAdd cs ns t

1179

1193

1180 mkConst c args = PApp fc (PRef fc c)

1194 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)

1182

1196

1183− getConstraints (PPi (Constraint _ _ _) _ c sc)

1197+ getConstraints (PPi (Constraint _ _) _ c sc)

1184 = getcapp c ++ getConstraints sc

1198 = getcapp c ++ getConstraints sc

1185 getConstraints (PPi _ _ c sc) = getConstraints sc

1199 getConstraints (PPi _ _ c sc) = getConstraints sc

1186 getConstraints _ = []

1200 getConstraints _ = []

@@ -1190,7 +1204,7 @@ addUsingConstraints syn fc t

1190 return (UConstraint c ns)

1204 return (UConstraint c ns)

1191 getcapp _ = []

1205 getcapp _ = []

1192

1206

1193− getName (PExp _ _ (PRef _ n) _) = return n

1207+ getName (PExp _ _ (PRef _ n)) = return n

1194 getName _ = []

1208 getName _ = []

1195

1209

1196-- Add implicit Pi bindings for any names in the term which appear in an

1210-- 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) $

1240 = do (decls, ns) <- get

1254 = do (decls, ns) <- get

1241 let isn = concatMap (namesIn uvars ist) (map getTm as)

1255 let isn = concatMap (namesIn uvars ist) (map getTm as)

1242 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1256 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)

1244 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

1258 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

1245 (decls , ns) <- get

1259 (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,

1247 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1261 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1248 imps True (n:env) sc

1262 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)

1250 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1264 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1251 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1265 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1252 _ -> [])

1266 _ -> [])

1253 (decls, ns) <- get -- ignore decls in HO types

1267 (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,

1255 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1269 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1256 imps True (n:env) sc

1270 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)

1258 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1272 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1259 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1273 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1260 _ -> [])

1274 _ -> [])

1261 (decls, ns) <- get -- ignore decls in HO types

1275 (decls, ns) <- get -- ignore decls in HO types

1262− put (PConstraint 10 l Placeholder doc : decls,

1276+ put (PConstraint 10 l Placeholder : decls,

1263 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1277 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1264 imps True (n:env) sc

1278 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)

1266 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1280 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1267 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1281 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1268 _ -> [])

1282 _ -> [])

1269 (decls, ns) <- get -- ignore decls in HO types

1283 (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,

1271 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1285 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1272 imps True (n:env) sc

1286 imps True (n:env) sc

1273 imps top env (PEq _ l r)

1287 imps top env (PEq _ l r)

@@ -1308,8 +1322,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1308 pibind using [] sc = sc

1322 pibind using [] sc = sc

1309 pibind using (n:ns) sc

1323 pibind using (n:ns) sc

1310 = case lookup n using of

1324 = case lookup n using of

1311− Just ty -> PPi (Imp [] Dynamic "" False) n ty (pibind using ns sc)

1325+ Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)

1312− Nothing -> PPi (Imp [] Dynamic "" False) n Placeholder

1326+ Nothing -> PPi (Imp [] Dynamic False) n Placeholder

1313 (pibind using ns sc)

1327 (pibind using ns sc)

1314

1328

1315-- Add implicit arguments in function calls

1329-- Add implicit arguments in function calls

@@ -1425,7 +1439,7 @@ aiFn inpat True ist fc f ds []

1425-- any constructor alts || any allImp ialts))

1439-- any constructor alts || any allImp ialts))

1426 then aiFn inpat False ist fc f ds [] -- use it as a constructor

1440 then aiFn inpat False ist fc f ds [] -- use it as a constructor

1427 else Right $ PPatvar fc f

1441 else Right $ PPatvar fc f

1428− where imp (PExp _ _ _ _) = False

1442+ where imp (PExp _ _ _) = False

1429 imp _ = True

1443 imp _ = True

1430-- allImp [] = False

1444-- allImp [] = False

1431 allImp xs = all imp xs

1445 allImp xs = all imp xs

@@ -1474,30 +1488,30 @@ aiFn inpat expat ist fc f ds as

1474

1488

1475

1489

1476 insertImpl :: [PArg] -> [PArg] -> [PArg]

1490 insertImpl :: [PArg] -> [PArg] -> [PArg]

1477− insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =

1491+ insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

1478− PExp p l tm d : insertImpl ps given

1492+ PExp p l tm : insertImpl ps given

1479− insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =

1493+ insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =

1480− PConstraint p l tm d : insertImpl ps given

1494+ PConstraint p l tm : insertImpl ps given

1481− insertImpl (PConstraint p l ty d : ps) given =

1495+ insertImpl (PConstraint p l ty : ps) given =

1482− PConstraint p l (PResolveTC fc) d : insertImpl ps given

1496+ PConstraint p l (PResolveTC fc) : insertImpl ps given

1483− insertImpl (PImp p _ l n ty d : ps) given =

1497+ insertImpl (PImp p _ l n ty : ps) given =

1484 case find n given [] of

1498 case find n given [] of

1485− Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'

1499+ Just (tm, given') -> PImp p False l n tm : insertImpl ps given'

1486− Nothing -> PImp p True l n Placeholder "" : insertImpl ps given

1500+ Nothing -> PImp p True l n Placeholder : insertImpl ps given

1487− insertImpl (PTacImplicit p l n sc' ty d : ps) given =

1501+ insertImpl (PTacImplicit p l n sc' ty : ps) given =

1488 let sc = addImpl ist sc' in

1502 let sc = addImpl ist sc' in

1489 case find n given [] of

1503 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'

1491 Nothing -> if inpat

1505 Nothing -> if inpat

1492− then PTacImplicit p l n sc Placeholder "" : insertImpl ps given

1506+ then PTacImplicit p l n sc Placeholder : insertImpl ps given

1493− else PTacImplicit p l n sc sc "" : insertImpl ps given

1507+ else PTacImplicit p l n sc sc : insertImpl ps given

1494 insertImpl expected [] = []

1508 insertImpl expected [] = []

1495 insertImpl _ given = given

1509 insertImpl _ given = given

1496

1510

1497 find n [] acc = Nothing

1511 find n [] acc = Nothing

1498− find n (PImp _ _ _ n' t _ : gs) acc

1512+ find n (PImp _ _ _ n' t : gs) acc

1499 | n == n' = Just (t, reverse acc ++ gs)

1513 | n == n' = Just (t, reverse acc ++ gs)

1500− find n (PTacImplicit _ _ n' _ t _ : gs) acc

1514+ find n (PTacImplicit _ _ n' _ t : gs) acc

1501 | n == n' = Just (t, reverse acc ++ gs)

1515 | n == n' = Just (t, reverse acc ++ gs)

1502 find n (g : gs) acc = find n gs (g : acc)

1516 find n (g : gs) acc = find n gs (g : acc)

1503

1517

@@ -1527,16 +1541,16 @@ stripLinear i tm = evalState (sl tm) [] where

1527 sl (PApp fc fn args) = do fn' <- sl fn

1541 sl (PApp fc fn args) = do fn' <- sl fn

1528 args' <- mapM slA args

1542 args' <- mapM slA args

1529 return $ PApp fc fn' args'

1543 return $ PApp fc fn' args'

1530− where slA (PImp p m l n t d) = do t' <- sl t

1544+ where slA (PImp p m l n t) = do t' <- sl t

1531− return $ PImp p m l n t' d

1545+ return $ PImp p m l n t'

1532− slA (PExp p l t d) = do t' <- sl t

1546+ slA (PExp p l t) = do t' <- sl t

1533− return $ PExp p l t' d

1547+ return $ PExp p l t'

1534− slA (PConstraint p l t d)

1548+ slA (PConstraint p l t)

1535 = do t' <- sl t

1549 = do t' <- sl t

1536− return $ PConstraint p l t' d

1550+ return $ PConstraint p l t'

1537− slA (PTacImplicit p l n sc t d)

1551+ slA (PTacImplicit p l n sc t)

1538 = do t' <- sl t

1552 = do t' <- sl t

1539− return $ PTacImplicit p l n sc t' d

1553+ return $ PTacImplicit p l n sc t'

1540 sl x = return x

1554 sl x = return x

1541

1555

1542-- Remove functions which aren't applied to anything, which must then

1556-- Remove functions which aren't applied to anything, which must then

src/Idris/AbsSyntaxTree.hs+75−76

@@ -111,7 +111,7 @@ data IState = IState {

111 idris_flags :: Ctxt [FnOpt],

112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113 idris_calledgraph :: Ctxt [Name],

114− idris_docstrings :: Ctxt String,

114+ idris_docstrings :: Ctxt (String, [(Name, String)]),

115 idris_tyinfodata :: Ctxt TIData,

116 idris_totcheck :: [(FC, Name)], -- names to check totality on

117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

@@ -189,6 +189,7 @@ data IBCWrite = IBCFix FixDecl

189 | IBCDSL Name

190 | IBCData Name

191 | IBCOpt Name

192+ | IBCMetavar Name

192 | IBCSyntax Syntax

193 | IBCSyntax Syntax

193 | IBCKeyword String

194 | IBCKeyword String

194 | IBCImport FilePath

195 | IBCImport FilePath

@@ -380,19 +381,15 @@ deriving instance NFData Static

380-- Mark bindings with their explicitness, and laziness

381-- Mark bindings with their explicitness, and laziness

381data Plicity = Imp { pargopts :: [ArgOpt],

382data Plicity = Imp { pargopts :: [ArgOpt],

382 pstatic :: Static,

383 pstatic :: Static,

383− pdocstr :: String,

384 pparam :: Bool }

385 | Exp { pargopts :: [ArgOpt],

386 pstatic :: Static,

387− pdocstr :: String,

388 pparam :: Bool }

387 pparam :: Bool }

389 | Constraint { pargopts :: [ArgOpt],

388 | Constraint { pargopts :: [ArgOpt],

390− pstatic :: Static,

389+ pstatic :: Static }

391− pdocstr :: String }

392 | TacImp { pargopts :: [ArgOpt],

390 | TacImp { pargopts :: [ArgOpt],

393 pstatic :: Static,

391 pstatic :: Static,

394− pscript :: PTerm,

392+ pscript :: PTerm }

395− pdocstr :: String }

396 deriving (Show, Eq)

393 deriving (Show, Eq)

397

394

398plazy :: Plicity -> Bool

395plazy :: Plicity -> Bool

@@ -403,11 +400,11 @@ deriving instance Binary Plicity

403deriving instance NFData Plicity

400deriving instance NFData Plicity

404!-}

401!-}

405

402

406−impl = Imp [Lazy] Dynamic "" False

403+impl = Imp [Lazy] Dynamic False

407−expl = Exp [] Dynamic "" False

404+expl = Exp [] Dynamic False

408−expl_param = Exp [] Dynamic "" True

405+expl_param = Exp [] Dynamic True

409−constraint = Constraint [] Dynamic ""

406+constraint = Constraint [] Dynamic

410−tacimpl t = TacImp [] Dynamic t ""

407+tacimpl t = TacImp [] Dynamic t

411

408

412data FnOpt = Inlinable -- always evaluate when simplifying

409data FnOpt = Inlinable -- always evaluate when simplifying

413 | TotalFn | PartialFn

410 | TotalFn | PartialFn

@@ -443,15 +440,21 @@ data DataOpt = Codata -- Set if the the data-type is coinductive

443

440

444type DataOpts = [DataOpt]

441type DataOpts = [DataOpt]

445

442

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+

446-- | Top-level declarations such as compiler directives, definitions,

449-- | Top-level declarations such as compiler directives, definitions,

447-- datatypes and typeclasses.

450-- datatypes and typeclasses.

448data PDecl' t

451data PDecl' t

449 = PFix FC Fixity [String] -- ^ Fixity declaration

452 = 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

451 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

454 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

452 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

455 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

453 | PCAF FC Name t -- ^ Top level constant

456 | 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.

455 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

458 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

456 | PNamespace String [PDecl' t] -- ^ New namespace

459 | PNamespace String [PDecl' t] -- ^ New namespace

457 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

460 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

@@ -474,7 +477,7 @@ data PDecl' t

474 | PSyntax FC Syntax -- ^ Syntax definition

477 | PSyntax FC Syntax -- ^ Syntax definition

475 | PMutual FC [PDecl' t] -- ^ Mutual block

478 | PMutual FC [PDecl' t] -- ^ Mutual block

476 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

479 | 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

478 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

481 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

479 -- bool is True, lhs and rhs must be convertible

482 -- bool is True, lhs and rhs must be convertible

480 deriving Functor

483 deriving Functor

@@ -509,7 +512,7 @@ deriving instance NFData PClause'

509-- | Data declaration

512-- | Data declaration

510data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

513data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

511 d_tcon :: t, -- ^ Type constructor

514 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

513 }

516 }

514 -- ^ Data declaration

517 -- ^ Data declaration

515 | PLaterdecl { d_name :: Name, d_tcon :: t }

518 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -531,13 +534,13 @@ type PClause = PClause' PTerm

531

534

532declared :: PDecl -> [Name]

535declared :: PDecl -> [Name]

533declared (PFix _ _ _) = []

536declared (PFix _ _ _) = []

534−declared (PTy _ _ _ _ n t) = [n]

537+declared (PTy _ _ _ _ _ n t) = [n]

535declared (PPostulate _ _ _ _ n t) = [n]

538declared (PPostulate _ _ _ _ n t) = [n]

536declared (PClauses _ _ n _) = [] -- not a declaration

539declared (PClauses _ _ n _) = [] -- not a declaration

537declared (PCAF _ n _) = [n]

540declared (PCAF _ n _) = [n]

538−declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

541+declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

539− where fstt (_, a, _, _, _) = a

542+ where fstt (_, _, a, _, _, _) = a

540−declared (PData _ _ _ _ (PLaterdecl n _)) = [n]

543+declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

541declared (PParams _ _ ds) = concatMap declared ds

544declared (PParams _ _ ds) = concatMap declared ds

542declared (PNamespace _ ds) = concatMap declared ds

545declared (PNamespace _ ds) = concatMap declared ds

543declared (PRecord _ _ _ n _ _ c _) = [n, c]

546declared (PRecord _ _ _ n _ _ c _) = [n, c]

@@ -551,12 +554,12 @@ declared (PDirective _) = []

551-- get the names declared, not counting nested parameter blocks

554-- get the names declared, not counting nested parameter blocks

552tldeclared :: PDecl -> [Name]

555tldeclared :: PDecl -> [Name]

553tldeclared (PFix _ _ _) = []

556tldeclared (PFix _ _ _) = []

554−tldeclared (PTy _ _ _ _ n t) = [n]

557+tldeclared (PTy _ _ _ _ _ n t) = [n]

555tldeclared (PPostulate _ _ _ _ n t) = [n]

558tldeclared (PPostulate _ _ _ _ n t) = [n]

556tldeclared (PClauses _ _ n _) = [] -- not a declaration

559tldeclared (PClauses _ _ n _) = [] -- not a declaration

557tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

560tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

558−tldeclared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

561+tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

559− where fstt (_, a, _, _, _) = a

562+ where fstt (_, _, a, _, _, _) = a

560tldeclared (PParams _ _ ds) = []

563tldeclared (PParams _ _ ds) = []

561tldeclared (PMutual _ ds) = concatMap tldeclared ds

564tldeclared (PMutual _ ds) = concatMap tldeclared ds

562tldeclared (PNamespace _ ds) = concatMap tldeclared ds

565tldeclared (PNamespace _ ds) = concatMap tldeclared ds

@@ -566,13 +569,13 @@ tldeclared _ = []

566

569

567defined :: PDecl -> [Name]

570defined :: PDecl -> [Name]

568defined (PFix _ _ _) = []

571defined (PFix _ _ _) = []

569−defined (PTy _ _ _ _ n t) = []

572+defined (PTy _ _ _ _ _ n t) = []

570defined (PPostulate _ _ _ _ n t) = []

573defined (PPostulate _ _ _ _ n t) = []

571defined (PClauses _ _ n _) = [n] -- not a declaration

574defined (PClauses _ _ n _) = [n] -- not a declaration

572defined (PCAF _ n _) = [n]

575defined (PCAF _ n _) = [n]

573−defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

576+defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

574− where fstt (_, a, _, _, _) = a

577+ where fstt (_, _, a, _, _, _) = a

575−defined (PData _ _ _ _ (PLaterdecl n _)) = []

578+defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

576defined (PParams _ _ ds) = concatMap defined ds

579defined (PParams _ _ ds) = concatMap defined ds

577defined (PNamespace _ ds) = concatMap defined ds

580defined (PNamespace _ ds) = concatMap defined ds

578defined (PRecord _ _ _ n _ _ c _) = [n, c]

581defined (PRecord _ _ _ n _ _ c _) = [n, c]

@@ -687,7 +690,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

687 | MatchRefine Name

690 | MatchRefine Name

688 | LetTac Name t | LetTacTy Name t t

691 | LetTac Name t | LetTacTy Name t t

689 | Exact t | Compute | Trivial | TCInstance

692 | Exact t | Compute | Trivial | TCInstance

690− | ProofSearch (Maybe Name) Name [Name]

693+ | ProofSearch (Maybe Name) [Name]

691 | Solve

694 | Solve

692 | Attack

695 | Attack

693 | ProofState | ProofTerm | Undo

696 | ProofState | ProofTerm | Undo

@@ -759,22 +762,18 @@ type PDo = PDo' PTerm

759data PArg' t = PImp { priority :: Int,

762data PArg' t = PImp { priority :: Int,

760 machine_inf :: Bool, -- true if the machine inferred it

763 machine_inf :: Bool, -- true if the machine inferred it

761 argopts :: [ArgOpt],

764 argopts :: [ArgOpt],

762− pname :: Name, getTm :: t,

765+ pname :: Name, getTm :: t }

763− pargdoc :: String }

764 | PExp { priority :: Int,

766 | PExp { priority :: Int,

765 argopts :: [ArgOpt],

767 argopts :: [ArgOpt],

766− getTm :: t,

768+ getTm :: t }

767− pargdoc :: String }

768 | PConstraint { priority :: Int,

769 | PConstraint { priority :: Int,

769 argopts :: [ArgOpt],

770 argopts :: [ArgOpt],

770− getTm :: t,

771+ getTm :: t }

771− pargdoc :: String }

772 | PTacImplicit { priority :: Int,

773 argopts :: [ArgOpt],

774 pname :: Name,

775 getScript :: t,

776− getTm :: t,

776+ getTm :: t }

777− pargdoc :: String }

778 deriving (Show, Eq, Functor)

777 deriving (Show, Eq, Functor)

779

778

780data ArgOpt = Lazy | HideDisplay

779data ArgOpt = Lazy | HideDisplay

@@ -784,20 +783,20 @@ lazyarg :: PArg' t -> Bool

784lazyarg tm = Lazy `elem` argopts tm

783lazyarg tm = Lazy `elem` argopts tm

785

784

786instance Sized a => Sized (PArg' a) where

785instance Sized a => Sized (PArg' a) where

787− size (PImp p _ l nm trm _) = 1 + size nm + size trm

786+ size (PImp p _ l nm trm) = 1 + size nm + size trm

788− size (PExp p l trm _) = 1 + size trm

787+ size (PExp p l trm) = 1 + size trm

789− size (PConstraint p l trm _) = 1 + size trm

788+ size (PConstraint p l trm) = 1 + size trm

790− size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm

789+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

791

790

792{-!

791{-!

793deriving instance Binary PArg'

792deriving instance Binary PArg'

794deriving instance NFData PArg'

793deriving instance NFData PArg'

795!-}

794!-}

796

795

797−pimp n t mach = PImp 1 mach [Lazy] n t ""

796+pimp n t mach = PImp 1 mach [Lazy] n t

798−pexp t = PExp 1 [] t ""

797+pexp t = PExp 1 [] t

799−pconst t = PConstraint 1 [] t ""

798+pconst t = PConstraint 1 [] t

800−ptacimp n s t = PTacImplicit 2 [Lazy] n s t ""

799+ptacimp n s t = PTacImplicit 2 [Lazy] n s t

801

800

802type PArg = PArg' PTerm

801type PArg = PArg' PTerm

803

802

@@ -949,9 +948,9 @@ inferTy = sMN 0 "__Infer"

949inferCon = sMN 0 "__infer"

948inferCon = sMN 0 "__infer"

950inferDecl = PDatadecl inferTy

949inferDecl = PDatadecl inferTy

951 PType

950 PType

952− [("", inferCon, PPi impl (sMN 0 "iType") PType (

951+ [("", [], inferCon, PPi impl (sMN 0 "iType") PType (

953− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

952+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

954− (PRef bi inferTy)), bi, [])]

953+ (PRef bi inferTy)), bi, [])]

955inferOpts = []

954inferOpts = []

956

955

957infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

956infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

@@ -979,7 +978,7 @@ primNames = [unitTy, unitCon,

979unitTy = sMN 0 "__Unit"

978unitTy = sMN 0 "__Unit"

980unitCon = sMN 0 "__II"

979unitCon = sMN 0 "__II"

981unitDecl = PDatadecl unitTy PType

980unitDecl = PDatadecl unitTy PType

982− [("", unitCon, PRef bi unitTy, bi, [])]

981+ [("", [], unitCon, PRef bi unitTy, bi, [])]

983unitOpts = [DefaultEliminator]

982unitOpts = [DefaultEliminator]

984

983

985falseTy = sMN 0 "__False"

984falseTy = sMN 0 "__False"

@@ -989,12 +988,12 @@ falseOpts = []

989pairTy = sMN 0 "__Pair"

988pairTy = sMN 0 "__Pair"

990pairCon = sMN 0 "__MkPair"

989pairCon = sMN 0 "__MkPair"

991pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

990pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

992− [("", pairCon, PPi impl (n "A") PType (

991+ [("", [], pairCon, PPi impl (n "A") PType (

993− PPi impl (n "B") PType (

992+ PPi impl (n "B") PType (

994− PPi expl (n "a") (PRef bi (n "A")) (

993+ PPi expl (n "a") (PRef bi (n "A")) (

995− PPi expl (n "b") (PRef bi (n "B"))

994+ PPi expl (n "b") (PRef bi (n "B"))

996− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

995+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

997− pexp (PRef bi (n "B"))])))), bi, [])]

996+ pexp (PRef bi (n "B"))])))), bi, [])]

998 where n a = sMN 0 a

997 where n a = sMN 0 a

999pairOpts = []

998pairOpts = []

1000

999

@@ -1003,12 +1002,12 @@ eqCon = sUN "refl"

1003eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

1002eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

1004 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1003 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1005 PType)

1004 PType)

1006− [("", eqCon, PPi impl (n "A") PType (

1005+ [("", [], eqCon, PPi impl (n "A") PType (

1007− PPi impl (n "x") (PRef bi (n "A"))

1006+ PPi impl (n "x") (PRef bi (n "A"))

1008− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1007+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1009− pimp (n "B") Placeholder False,

1008+ pimp (n "B") Placeholder False,

1010− pexp (PRef bi (n "x")),

1009+ pexp (PRef bi (n "x")),

1011− pexp (PRef bi (n "x"))])), bi, [])]

1010+ pexp (PRef bi (n "x"))])), bi, [])]

1012 where n a = sMN 0 a

1011 where n a = sMN 0 a

1013eqOpts = []

1012eqOpts = []

1014

1013

@@ -1016,8 +1015,8 @@ elimName = sUN "__Elim"

1016elimMethElimTy = sUN "__elimTy"

1015elimMethElimTy = sUN "__elimTy"

1017elimMethElim = sUN "elim"

1016elimMethElim = sUN "elim"

1018elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1017elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1019− [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

1018+ [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1020− PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1019+ PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1021

1020

1022-- Defined in builtins.idr

1021-- Defined in builtins.idr

1023sigmaTy = sUN "Exists"

1022sigmaTy = sUN "Exists"

@@ -1101,7 +1100,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

1101 text "let" <+> bindingOf n False <+> text "=" </>

1100 text "let" <+> bindingOf n False <+> text "=" </>

1102 prettySe 10 bnd v <+> text "in" </>

1101 prettySe 10 bnd v <+> text "in" </>

1103 prettySe 10 ((n, False):bnd) sc

1102 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)

1105 | n `elem` allNamesIn sc || impl =

1104 | n `elem` allNamesIn sc || impl =

1106 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1105 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1107 bracket p 2 . group $

1106 bracket p 2 . group $

@@ -1115,7 +1114,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

1115 case s of

1114 case s of

1116 Static -> text "[static]" <> space

1115 Static -> text "[static]" <> space

1117 _ -> empty

1116 _ -> empty

1118− prettySe p bnd (PPi (Imp l s _ _) n ty sc)

1117+ prettySe p bnd (PPi (Imp l s _) n ty sc)

1119 | impl =

1118 | impl =

1120 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1119 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1121 bracket p 2 $

1120 bracket p 2 $

@@ -1127,10 +1126,10 @@ pprintPTerm impl bnd = prettySe 10 bnd

1127 case s of

1126 case s of

1128 Static -> text "[static]" <> space

1127 Static -> text "[static]" <> space

1129 _ -> empty

1128 _ -> empty

1130− prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1129+ prettySe p bnd (PPi (Constraint _ _) n ty sc) =

1131 bracket p 2 $

1130 bracket p 2 $

1132 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1131 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) =

1134 bracket p 2 $

1133 bracket p 2 $

1135 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1134 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1136 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1135 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

@@ -1247,10 +1246,10 @@ pprintPTerm impl bnd = prettySe 10 bnd

1247

1246

1248 prettySe p bnd _ = text "test"

1247 prettySe p bnd _ = text "test"

1249

1248

1250− prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)

1249+ prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1251− prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm

1250+ prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm

1252− prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm

1251+ prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm

1253− prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)

1252+ prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1254

1253

1255 prettyArgSe bnd arg = prettySe 0 bnd arg

1254 prettyArgSe bnd arg = prettySe 0 bnd arg

1256 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1255 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)

1346showDImp :: Bool -> PData -> Doc OutputAnnotation

1345showDImp :: Bool -> PData -> Doc OutputAnnotation

1347showDImp impl (PDatadecl n ty cons)

1346showDImp impl (PDatadecl n ty cons)

1348 = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1347 = 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))

1350

1349

1351showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1350showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1352showDecls i ds = vsep (map (showDeclImp i) ds)

1351showDecls i ds = vsep (map (showDeclImp i) ds)

1353

1352

1354showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1353showDeclImp _ (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

1356showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1355showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1357 indent 2 (vsep (map (showCImp i) cs))

1356 indent 2 (vsep (map (showCImp i) cs))

1358−showDeclImp _ (PData _ _ _ _ d) = showDImp True d

1357+showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

1359showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1358showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1360showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1359showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1361showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1360showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

@@ -1371,17 +1370,17 @@ instance Show (Doc OutputAnnotation) where

1371

1370

1372getImps :: [PArg] -> [(Name, PTerm)]

1371getImps :: [PArg] -> [(Name, PTerm)]

1373getImps [] = []

1372getImps [] = []

1374−getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

1373+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs

1375getImps (_ : xs) = getImps xs

1374getImps (_ : xs) = getImps xs

1376

1375

1377getExps :: [PArg] -> [PTerm]

1376getExps :: [PArg] -> [PTerm]

1378getExps [] = []

1377getExps [] = []

1379−getExps (PExp _ _ tm _ : xs) = tm : getExps xs

1378+getExps (PExp _ _ tm : xs) = tm : getExps xs

1380getExps (_ : xs) = getExps xs

1379getExps (_ : xs) = getExps xs

1381

1380

1382getConsts :: [PArg] -> [PTerm]

1381getConsts :: [PArg] -> [PTerm]

1383getConsts [] = []

1382getConsts [] = []

1384−getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

1383+getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

1385getConsts (_ : xs) = getConsts xs

1384getConsts (_ : xs) = getConsts xs

1386

1385

1387getAll :: [PArg] -> [PTerm]

1386getAll :: [PArg] -> [PTerm]

src/Idris/CaseSplit.hs+4−4

@@ -150,7 +150,7 @@ mergePat ist (PApp _ _ args) (PApp fc f args') t

150 where mergeArg x (y, t)

151 = do tm' <- mergePat ist (getTm x) (getTm y) t

152 case x of

153− (PImp _ _ _ _ _ _) ->

153+ (PImp _ _ _ _ _) ->

154 return (y { machine_inf = machine_inf x,

155 getTm = tm' })

156 _ -> return (y { getTm = tm' })

@@ -318,14 +318,14 @@ getClause l fn fp = do ty <- getInternalApp fp l

318 let ap = mkApp ist ty []

319 return (show fn ++ " " ++ ap ++

320 "= ?" ++ 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

322 = let n = getNameFrom i used ty in

323 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

325 | thead n == '_'

326 = let n = getNameFrom i used ty in

327 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

329 = show n ++ " " ++ mkApp i sc (n : used)

330 mkApp i (PPi _ _ _ sc) used = mkApp i sc used

331 mkApp i _ _ = ""

src/Idris/Completion.hs+1−1

@@ -50,7 +50,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

50 , (":e", Just ExprTArg)

51 , (":eval", Just ExprTArg)

52 ] ++ map (\x -> (x, Nothing)) [

53− "intros", "compute", "trivial", "solve", "attack",

53+ "intros", "compute", "trivial", "search", "solve", "attack",

54 "state", "term", "undo", "qed", "abandon", ":q"

55 ]

56tactics = map fst tacticArgs

src/Idris/Core/DeepSeq.hs+1

@@ -19,6 +19,7 @@ instance NFData SpecialName where

19 rnf (MethodN x1) = rnf x1 `seq` ()

20 rnf (CaseN x1) = rnf x1 `seq` ()

21 rnf (ElimN x1) = rnf x1 `seq` ()

22+ rnf (InstanceCtorN x1) = rnf x1 `seq` ()

22

23

23instance NFData Raw where

24instance NFData Raw where

24 rnf (Var x1) = rnf x1 `seq` ()

25 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

520wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)

521wknV i t = return t

522

523−convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])

523+convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

524

525−convEq :: Context -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

525+convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

526−convEq ctxt = ceq [] where

526+convEq ctxt holes = ceq [] where

527 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

528 ceq ps (P xt x _) (P yt y _)

529+ | x `elem` holes || y `elem` holes = return True

529 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

530 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

530 | otherwise = sameDefs ps x y

531 | otherwise = sameDefs ps x y

531 ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y

532 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)

320 = let res = ioWrap . EConstant . I $ 0

321 in execApp' env ctxt res (tail rest)

322

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)

323-- Throw away the 'World' argument to the foreign function

330-- Throw away the 'World' argument to the foreign function

324

331

325execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

332execApp' 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

805 (ns', (x',y',env',err', um) : ps')

806

807-- 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

809 up ns [] = (ns, [])

810 up ns ((x, y, env, err, um) : ps)

811 | all || um == Match =

@@ -860,15 +860,19 @@ processTactic UnifyProblems ps

860 notunified = updateNotunified ns' (notunified ps),

861 holes = holes ps \\ (map fst ns') }, plog ps)

862processTactic (MatchProblems all) ps

863− = let (ns', probs') = matchProblems all (context ps)

863+ = let (ns', probs') = matchProblems all [] (context ps)

864 (problems ps)

865 (injective ps)

866 (holes ps)

867+ (ns'', probs'') = matchProblems all ns' (context ps)

868+ probs'

869+ (injective ps)

870+ (holes ps)

867− pterm' = updateSolved ns' (pterm ps) in

871+ pterm' = updateSolved ns'' (pterm ps) in

868− return (ps { pterm = pterm', solved = Nothing, problems = probs',

872+ return (ps { pterm = pterm', solved = Nothing, problems = probs'',

869 previous = Just ps, plog = "",

873 previous = Just ps, plog = "",

870− notunified = updateNotunified ns' (notunified ps),

874+ notunified = updateNotunified ns'' (notunified ps),

871− holes = holes ps \\ (map fst ns') }, plog ps)

875+ holes = holes ps \\ (map fst ns'') }, plog ps)

872processTactic t ps

876processTactic t ps

873 = case holes ps of

877 = case holes ps of

874 [] -> fail "Nothing to fill in."

878 [] -> fail "Nothing to fill in."

src/Idris/Core/TT.hs+5−1

@@ -279,6 +279,7 @@ data SpecialName = WhereN Int Name Name

279 | MethodN Name

280 | CaseN Name

281 | ElimN Name

282+ | InstanceCtorN Name

282 deriving (Eq, Ord)

283 deriving (Eq, Ord)

283{-!

284{-!

284deriving instance Binary SpecialName

285deriving instance Binary SpecialName

@@ -322,6 +323,7 @@ instance Show SpecialName where

322 show (ParentN p c) = show p ++ "#" ++ T.unpack c

323 show (ParentN p c) = show p ++ "#" ++ T.unpack c

323 show (CaseN n) = "case block in " ++ show n

324 show (CaseN n) = "case block in " ++ show n

324 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

325 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

326+ show (InstanceCtorN n) = "constructor of " ++ show n

325

327

326-- Show a name in a way decorated for code generation, not human reading

328-- Show a name in a way decorated for code generation, not human reading

327showCG :: Name -> String

329showCG :: Name -> String

@@ -475,7 +477,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

475 | B8V (Vector Word8) | B16V (Vector Word16)

477 | B8V (Vector Word8) | B16V (Vector Word16)

476 | B32V (Vector Word32) | B64V (Vector Word64)

478 | B32V (Vector Word32) | B64V (Vector Word64)

477 | AType ArithTy | StrType

479 | AType ArithTy | StrType

478− | PtrType | BufferType | VoidType | Forgot

479 deriving (Eq, Ord)

481 deriving (Eq, Ord)

480{-!

482{-!

481deriving instance Binary Const

483deriving instance Binary Const

@@ -495,6 +497,7 @@ instance Pretty Const OutputAnnotation where

495 pretty StrType = text "String"

497 pretty StrType = text "String"

496 pretty BufferType = text "prim__UnsafeBuffer"

498 pretty BufferType = text "prim__UnsafeBuffer"

497 pretty PtrType = text "Ptr"

499 pretty PtrType = text "Ptr"

500+ pretty ManagedPtrType = text "Ptr"

498 pretty VoidType = text "Void"

501 pretty VoidType = text "Void"

499 pretty Forgot = text "Forgot"

502 pretty Forgot = text "Forgot"

500 pretty (B8 w) = text . show $ w

503 pretty (B8 w) = text . show $ w

@@ -1041,6 +1044,7 @@ instance Show Const where

1041 show StrType = "String"

1044 show StrType = "String"

1042 show BufferType = "prim__UnsafeBuffer"

1045 show BufferType = "prim__UnsafeBuffer"

1043 show PtrType = "Ptr"

1046 show PtrType = "Ptr"

1047+ show ManagedPtrType = "ManagedPtr"

1044 show VoidType = "Void"

1048 show VoidType = "Void"

1045

1049

1046showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String

1050showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String

src/Idris/Core/Typecheck.hs+11−6

@@ -16,11 +16,12 @@ import Idris.Core.Evaluate

16-- indexed with 'finalise'

17

18convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()

19−convertsC ctxt env x y

19+convertsC ctxt env x y =

20+ do let hs = map fst (filter isHole env)

20− = do c1 <- convEq ctxt x y

21+ c1 <- convEq ctxt hs x y

21 if c1 then return ()

22 if c1 then return ()

22 else

23 else

23− do c2 <- convEq ctxt (finalise (normalise ctxt env x))

24+ do c2 <- convEq ctxt hs (finalise (normalise ctxt env x))

24 (finalise (normalise ctxt env y))

25 (finalise (normalise ctxt env y))

25 if c2 then return ()

26 if c2 then return ()

26 else lift $ tfail (CantConvert

27 else lift $ tfail (CantConvert

@@ -29,15 +30,19 @@ convertsC ctxt env x y

29

30

30converts :: Context -> Env -> Term -> Term -> TC ()

31converts :: Context -> Env -> Term -> Term -> TC ()

31converts ctxt env x y

32converts ctxt env x y

33+ = let hs = map fst (filter isHole env) in

32− = case convEq' ctxt x y of

34+ case convEq' ctxt hs x y of

33 OK True -> return ()

35 OK True -> return ()

34− _ -> case convEq' ctxt (finalise (normalise ctxt env x))

36+ _ -> case convEq' ctxt hs (finalise (normalise ctxt env x))

35− (finalise (normalise ctxt env y)) of

37+ (finalise (normalise ctxt env y)) of

36 OK True -> return ()

38 OK True -> return ()

37 _ -> tfail (CantConvert

39 _ -> tfail (CantConvert

38 (finalise (normalise ctxt env x))

40 (finalise (normalise ctxt env x))

39 (finalise (normalise ctxt env y)) (errEnv env))

41 (finalise (normalise ctxt env y)) (errEnv env))

40

42

43+isHole (n, Hole _) = True

44+isHole _ = False

45+

41errEnv = map (\(x, b) -> (x, binderTy b))

46errEnv = map (\(x, b) -> (x, binderTy b))

42

47

43isType :: Context -> Env -> Term -> TC ()

48isType :: Context -> Env -> Term -> TC ()

src/Idris/Core/Unify.hs+2−2

@@ -79,7 +79,7 @@ match_unify ctxt env topx topy inj holes =

79 ha <- un names ax ay

80 combine names hf ha

81 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 []

83 | otherwise = do UI s f <- get

84 let r = recoverable x y

85 let err = CantUnify r

@@ -356,7 +356,7 @@ unify ctxt env topx topy inj holes =

356 sameBinder (Pi _) (Pi _) = True

357 sameBinder _ _ = False

358 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 []

360 | otherwise = do UI s f <- get

361 let r = recoverable x y

362 let err = CantUnify r

src/Idris/Coverage.hs+2−2

@@ -56,7 +56,7 @@ genClauses fc n xs given

56 -- there may be more case splitting that the idris_implicits record

57 -- suggests)

58 let parg = case lookupCtxt n (idris_implicits i) of

59− (p : _) -> p ++ repeat (PExp 0 [] Placeholder "")

59+ (p : _) -> p ++ repeat (PExp 0 [] Placeholder)

60 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

@@ -187,7 +187,7 @@ genAll i args

187 _ -> [p]

188 ops fc n arg o = return Placeholder

189

190− getExpTm (PImp _ True _ _ _ _) = Placeholder -- machine inferred, no point!

190+ getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!

191 getExpTm t = getTm t

192

193 -- put it back to its original form

src/Idris/DeepSeq.hs+30−24

@@ -57,14 +57,14 @@ instance NFData ArgOpt where

57 rnf _ = ()

58

59instance NFData Plicity where

60− rnf (Imp x1 x2 x3 x4)

60+ rnf (Imp x1 x2 x3)

61− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

61+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

62− rnf (Exp x1 x2 x3 x4)

62+ rnf (Exp x1 x2 x3)

63− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

63+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

64− rnf (Constraint x1 x2 x3)

64+ rnf (Constraint x1 x2)

65+ = rnf x1 `seq` rnf x2 `seq` ()

66+ rnf (TacImp x1 x2 x3)

65 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

67 = 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` ()

68

69instance NFData FnOpt where

70 rnf Inlinable = ()

@@ -84,18 +84,20 @@ instance NFData DataOpt where

84

85instance (NFData t) => NFData (PDecl' t) where

86 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)

88 = rnf x1 `seq`

89+ rnf x2 `seq`

89− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

90+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

90 rnf (PPostulate x1 x2 x3 x4 x5 x6)

91 rnf (PPostulate x1 x2 x3 x4 x5 x6)

91 = rnf x1 `seq`

92 = rnf x1 `seq`

92 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

93 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

93 rnf (PClauses x1 x2 x3 x4)

94 rnf (PClauses x1 x2 x3 x4)

94 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

95 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

95 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

96 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)

97 = rnf x1 `seq`

98 = rnf x1 `seq`

99+ rnf x2 `seq`

98− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

100+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

99 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

101 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

100 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

102 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

101 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

103 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

@@ -116,12 +118,17 @@ instance (NFData t) => NFData (PDecl' t) where

116 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

118 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

117 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

119 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

118 rnf (PDirective x1) = ()

120 rnf (PDirective x1) = ()

119− rnf (PProvider x1 x2 x3 x4 x5)

121+ rnf (PProvider x1 x2 x3 x4 x5 x6)

120 = rnf x1 `seq`

122 = 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` ()

122 rnf (PTransform x1 x2 x3 x4)

124 rnf (PTransform x1 x2 x3 x4)

123 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

125 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

124

126

127+instance NFData ProvideWhat where

128+ rnf ProvAny = ()

129+ rnf ProvTerm = ()

130+ rnf ProvPostulate = ()

131+

125instance NFData PunInfo where

132instance NFData PunInfo where

126 rnf x = x `seq` ()

133 rnf x = x `seq` ()

127

134

@@ -200,8 +207,8 @@ instance (NFData t) => NFData (PTactic' t) where

200 rnf (Exact x1) = rnf x1 `seq` ()

207 rnf (Exact x1) = rnf x1 `seq` ()

201 rnf Compute = ()

208 rnf Compute = ()

202 rnf Trivial = ()

209 rnf Trivial = ()

203− rnf (ProofSearch x1 x2 x3)

210+ rnf (ProofSearch x1 x2)

204− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

211+ = rnf x1 `seq` rnf x2 `seq` ()

205 rnf Solve = ()

212 rnf Solve = ()

206 rnf Attack = ()

213 rnf Attack = ()

207 rnf ProofState = ()

214 rnf ProofState = ()

@@ -225,16 +232,15 @@ instance (NFData t) => NFData (PDo' t) where

225 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

232 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

226

233

227instance (NFData t) => NFData (PArg' t) where

234instance (NFData t) => NFData (PArg' t) where

228− rnf (PImp x1 x2 x3 x4 x5 x6)

235+ rnf (PImp x1 x2 x3 x4 x5)

229− = rnf x1 `seq`

230− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

236+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

231− rnf (PExp x1 x2 x3 x4)

237+ rnf (PExp x1 x2 x3)

232− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

238+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

233− rnf (PConstraint x1 x2 x3 x4)

239+ rnf (PConstraint x1 x2 x3)

234− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

240+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

235− rnf (PTacImplicit x1 x2 x3 x4 x5 x6)

241+ rnf (PTacImplicit x1 x2 x3 x4 x5)

236 = rnf x1 `seq`

242 = 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` ()

238

244

239instance NFData ClassInfo where

245instance NFData ClassInfo where

240 rnf (CI x1 x2 x3 x4 x5 x6)

246 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

56 _ -> PRef un n

57 de env _ (Bind n (Lam ty) sc)

58 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

59− de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

59+ de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) sc)

60− = PPi impl n (de env [] ty) (de ((n,n):env) is 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)

61+ de env (PConstraint _ _ _:is) (Bind n (Pi ty) sc)

62 = 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)

64 = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is 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)

65− de env _ (Bind n (Pi ty) sc)

70+ de env [] (Bind n (Pi ty) sc)

66 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

71 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

67 de env _ (Bind n (Let ty val) sc)

72 de env _ (Bind n (Let ty val) sc)

68 = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

73 = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

69 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

74 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

70 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

75 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

72 de env _ (Constant i) = PConstant i

77 de env _ (Constant i) = PConstant i

73 de env _ Erased = Placeholder

78 de env _ Erased = Placeholder

74 de env _ Impossible = Placeholder

79 de env _ Impossible = Placeholder

@@ -112,10 +117,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

112 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

117 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

113 | otherwise = PApp un (PRef un n) (map pexp args)

118 | otherwise = PApp un (PRef un n) (map pexp args)

114

119

115− imp (PImp p m l n _ d) arg = PImp p m l n arg d

120+ imp (PImp p m l n _) arg = PImp p m l n arg

116− imp (PExp p l _ d) arg = PExp p l arg d

121+ imp (PExp p l _) arg = PExp p l arg

117− imp (PConstraint p l _ d) arg = PConstraint p l arg d

122+ imp (PConstraint p l _) arg = PConstraint p l arg

118− imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

123+ imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

119

124

120-- | How far to indent sub-errors

125-- | How far to indent sub-errors

121errorIndent :: Int

126errorIndent :: Int

src/Idris/Docs.hs+33−21

@@ -14,15 +14,17 @@ import Data.List

14-- TODO: Only include names with public/abstract accessibility

15

16data FunDoc = FD Name String

17− [(Name, PTerm, Plicity)] -- args: name, ty, plicity

17+ [(Name, PTerm, Plicity, Maybe String)] -- args: name, ty, implicit, docs

18 PTerm -- function type

19 (Maybe Fixity)

20+ deriving Show

20

21

21data Docs = FunDoc FunDoc

22data Docs = FunDoc FunDoc

22 | DataDoc FunDoc -- type constructor docs

23 | DataDoc FunDoc -- type constructor docs

23 [FunDoc] -- data constructor docs

24 [FunDoc] -- data constructor docs

24 | ClassDoc Name String -- class docs

25 | ClassDoc Name String -- class docs

25 [FunDoc] -- method docs

26 [FunDoc] -- method docs

27+ deriving Show

26

28

27showDoc "" = empty

29showDoc "" = empty

28showDoc x = text " -- " <> text x

30showDoc x = text " -- " <> text x

@@ -31,23 +33,32 @@ pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

31pprintFD imp (FD n doc args ty f)

33pprintFD imp (FD n doc args ty f)

32 = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>

34 = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>

33 maybe empty (\f -> text (show f) <> line) f <>

35 maybe empty (\f -> text (show f) <> line) f <>

34− let argshow = mapMaybe showArg args in

36+ let argshow = showArgs args [] in

35 if not (null argshow)

37 if not (null argshow)

36 then nest 4 $ text "Arguments:" <$> vsep argshow

38 then nest 4 $ text "Arguments:" <$> vsep argshow

37 else empty)

39 else empty)

38

40

39− where showArg (n, ty, arg@(Exp {}))

41+ where showArgs ((n, ty, Exp {}, d):args) bnd

40− = Just $ bindingOf n False <+> colon <+> prettyImp imp ty <>

42+ = bindingOf n False <+> colon <+>

43+ pprintPTerm imp bnd ty <>

41− showDoc (pdocstr arg) <> line

44+ showDoc (maybe "" id d) <> line

45+ :

46+ showArgs args ((n, False):bnd)

42− showArg (n, ty, arg@(Constraint {}))

47+ showArgs ((n, ty, Constraint {}, d):args) bnd

43− = Just $ text "Class constraint" <+>

48+ = text "Class constraint" <+>

44− prettyImp imp ty <> showDoc (pdocstr arg) <> line

49+ pprintPTerm imp bnd ty <> showDoc (maybe "" id d) <> line

45− showArg (n, ty, arg@(Imp {}))

50+ :

51+ showArgs args ((n, True):bnd)

52+ showArgs ((n, ty, Imp {}, d):args) bnd

46 | not (null doc)

53 | not (null doc)

47− = Just $ text "(implicit)" <+>

54+ = text "(implicit)" <+>

48− bindingOf n True <+> colon <+> prettyImp imp ty

55+ bindingOf n True <+> colon <+>

56+ pprintPTerm imp bnd ty <>

49− <> showDoc (pdocstr arg) <> line

57+ showDoc (maybe "" id d) <> line

50− showArg (n, _, _) = Nothing

58+ :

59+ showArgs args ((n, True):bnd)

60+ showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

61+ showArgs [] _ = []

51

62

52

63

53

64

@@ -81,7 +92,7 @@ docClass :: Name -> ClassInfo -> Idris Docs

81docClass n ci

92docClass n ci

82 = do i <- getIState

93 = do i <- getIState

83 let docstr = case lookupCtxt n (idris_docstrings i) of

94 let docstr = case lookupCtxt n (idris_docstrings i) of

84− [str] -> str

95+ [str] -> fst str

85 _ -> ""

96 _ -> ""

86 mdocs <- mapM docFun (map fst (class_methods ci))

97 mdocs <- mapM docFun (map fst (class_methods ci))

87 return (ClassDoc n docstr mdocs)

98 return (ClassDoc n docstr mdocs)

@@ -89,11 +100,11 @@ docClass n ci

89docFun :: Name -> Idris FunDoc

100docFun :: Name -> Idris FunDoc

90docFun n

101docFun n

91 = do i <- getIState

102 = do i <- getIState

92− let docstr = case lookupCtxt n (idris_docstrings i) of

103+ let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of

93− [str] -> str

104+ [d] -> d

94− _ -> ""

105+ _ -> ("", [])

95 let ty = delabTy i n

106 let ty = delabTy i n

96− let args = getPArgNames ty

107+ let args = getPArgNames ty argDocs

97 let infixes = idris_infixes i

108 let infixes = idris_infixes i

98 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes

109 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes

99 let f = case fixdecls of

110 let f = case fixdecls of

@@ -105,6 +116,7 @@ docFun n

105 funName (UN n) = str n

116 funName (UN n) = str n

106 funName (NS n _) = funName n

117 funName (NS n _) = funName n

107

118

108−getPArgNames :: PTerm -> [(Name, PTerm, Plicity)]

119+getPArgNames :: PTerm -> [(Name, String)] -> [(Name, PTerm, Plicity, Maybe String)]

109−getPArgNames (PPi plicity name ty body) = ((name, ty, plicity) : getPArgNames body)

120+getPArgNames (PPi plicity name ty body) ds =

121+ (name, ty, plicity, lookup name ds) : getPArgNames body ds

110−getPArgNames _ = []

122+getPArgNames _ _ = []

src/Idris/ElabDecls.hs+109−84

@@ -63,15 +63,15 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

63-- return (n, (i, top, t'))) ns

64

65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

66−elabType :: ElabInfo -> SyntaxInfo -> String ->

66+elabType :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

67 FC -> FnOpts -> Name -> PTerm -> Idris Type

68elabType = elabType' False

69

70elabType' :: Bool -> -- normalise it

71− ElabInfo -> SyntaxInfo -> String ->

71+ ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

72 FC -> FnOpts -> Name -> PTerm -> Idris Type

73−elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_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 -}

74+ n = liftname info n_in in -}

75 do checkUndefined fc n

76 ctxt <- getContext

77 i <- getIState

@@ -122,7 +122,8 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

122 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

123 addDeferred ds'

124 setFlags n opts'

125+ checkDocs fc argDocs ty

125− addDocStr n doc

126+ addDocStr n doc argDocs

126 addIBC (IBCDoc n)

127 addIBC (IBCDoc n)

127 addIBC (IBCFlags n opts')

128 addIBC (IBCFlags n opts')

128 when (Implicit `elem` opts) $ do addCoercion n

129 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

167 , ns2 == map txt ["Maybe", "Prelude"]

168 , ns2 == map txt ["Maybe", "Prelude"]

168 , ns3 == map txt ["List", "Prelude"]

169 , ns3 == map txt ["List", "Prelude"]

169 , ns4 == map txt ["Errors","Reflection","Language"] = True

170 , ns4 == map txt ["Errors","Reflection","Language"] = True

170− tyIsHandler _ = False

171+ tyIsHandler _ = False

171

172

173

173elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

174elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

174 FC -> FnOpts -> Name -> PTerm -> Idris ()

175 FC -> FnOpts -> Name -> PTerm -> Idris ()

175elabPostulate info syn doc fc opts n ty

176elabPostulate 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

177 -- make sure it's collapsible, so it is never needed at run time

178 -- make sure it's collapsible, so it is never needed at run time

178 -- start by getting the elaborated type

179 -- start by getting the elaborated type

179 ctxt <- getContext

180 ctxt <- getContext

@@ -194,8 +195,8 @@ elabPostulate info syn doc fc opts n ty

194 -- remove it from the deferred definitions list

195 -- remove it from the deferred definitions list

195 solveDeferred n

196 solveDeferred n

196

197

197−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()

198+elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()

198−elabData info syn doc fc opts (PLaterdecl n t_in)

199+elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

199 = do let codata = Codata `elem` opts

200 = do let codata = Codata `elem` opts

200 iLOG (show (fc, doc))

201 iLOG (show (fc, doc))

201 checkUndefined fc n

202 checkUndefined fc n

@@ -213,7 +214,7 @@ elabData info syn doc fc opts (PLaterdecl n t_in)

213 logLvl 2 $ "---> " ++ show cty

214 logLvl 2 $ "---> " ++ show cty

214 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

215 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

215

216

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)

217 = do let codata = Codata `elem` opts

218 = do let codata = Codata `elem` opts

218 iLOG (show fc)

219 iLOG (show fc)

219 undef <- isUndefined fc n

220 undef <- isUndefined fc n

@@ -241,12 +242,13 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

241 let as = map (const Nothing) (getArgTys cty)

242 let as = map (const Nothing) (getArgTys cty)

242 let params = findParams (map snd cons)

243 let params = findParams (map snd cons)

243 logLvl 2 $ "Parameters : " ++ show params

244 logLvl 2 $ "Parameters : " ++ show params

244− putIState (i { idris_datatypes =

245+ putIState (i { idris_datatypes =

245 addDef n (TI (map fst cons) codata opts params)

246 addDef n (TI (map fst cons) codata opts params)

246 (idris_datatypes i) })

247 (idris_datatypes i) })

247 addIBC (IBCDef n)

248 addIBC (IBCDef n)

248 addIBC (IBCData n)

249 addIBC (IBCData n)

250+ checkDocs fc argDocs t_in

249− addDocStr n doc

251+ addDocStr n doc argDocs

250 addIBC (IBCDoc n)

252 addIBC (IBCDoc n)

251 let metainf = DataMI params

253 let metainf = DataMI params

252 addIBC (IBCMetaInformation n metainf)

254 addIBC (IBCMetaInformation n metainf)

@@ -258,10 +260,10 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

258 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

260 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

259 else return ()

261 else return ()

260 where

262 where

261− checkDefinedAs fc n t ctxt

263+ checkDefinedAs fc n t ctxt

262 = case lookupDef n ctxt of

264 = case lookupDef n ctxt of

263 [] -> return ()

265 [] -> return ()

264− [TyDecl _ ty] ->

266+ [TyDecl _ ty] ->

265 case converts ctxt [] t ty of

267 case converts ctxt [] t ty of

266 OK () -> return ()

268 OK () -> return ()

267 _ -> tclift $ tfail (At fc (AlreadyDefined n))

269 _ -> tclift $ tfail (At fc (AlreadyDefined n))

@@ -319,7 +321,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

319type EliminatorState = StateT (Map.Map String Int) Idris

321type EliminatorState = StateT (Map.Map String Int) Idris

320

322

321-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

323-- 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])] ->

323 ElabInfo -> EliminatorState ()

326 ElabInfo -> EliminatorState ()

324elabEliminator paramPos n ty cons info = do

327elabEliminator paramPos n ty cons info = do

325 elimLog $ "Elaborating eliminator"

328 elimLog $ "Elaborating eliminator"

@@ -328,15 +331,15 @@ elabEliminator paramPos n ty cons info = do

328 generalParams <- namePis False pms

331 generalParams <- namePis False pms

329 motiveIdxs <- namePis False idxs

332 motiveIdxs <- namePis False idxs

330 let motive = mkMotive n paramPos generalParams motiveIdxs

333 let motive = mkMotive n paramPos generalParams motiveIdxs

331− consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do

334+ consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do

332− name <- freshName $ "elim_" ++ simpleName cnm

335+ name <- freshName $ "elim_" ++ simpleName cnm

333− consTerm <- extractConsTerm c generalParams

336+ consTerm <- extractConsTerm c generalParams

334− return (name, expl, consTerm)) cons

337+ return (name, expl, consTerm)) cons

335 scrutineeIdxs <- namePis False idxs

338 scrutineeIdxs <- namePis False idxs

336 let motiveConstr = [(motiveName, expl, motive)]

339 let motiveConstr = [(motiveName, expl, motive)]

337 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

340 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

338 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

341 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

340 let clauseConsElimArgs = map getPiName consTerms

343 let clauseConsElimArgs = map getPiName consTerms

341 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

344 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

342 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

345 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

@@ -500,8 +503,8 @@ elabEliminator paramPos n ty cons info = do

500 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

503 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

501 _ -> return implargs

504 _ -> return implargs

502

505

503− extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

506+ extractConsTerm :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

504− extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do

507+ extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

505 let cons' = replaceParams paramPos generalParameters ty

508 let cons' = replaceParams paramPos generalParameters ty

506 let (args, resTy) = splitPi cons'

509 let (args, resTy) = splitPi cons'

507 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

510 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

@@ -536,8 +539,8 @@ elabEliminator paramPos n ty cons info = do

536 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

539 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

537 convertImplPi _ = Nothing

540 convertImplPi _ = Nothing

538

541

539− generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

542+ generateEliminatorClauses :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

540− generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

543+ generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

541 let cons' = replaceParams paramPos generalParameters ty

544 let cons' = replaceParams paramPos generalParameters ty

542 let (args, resTy) = splitPi cons'

545 let (args, resTy) = splitPi cons'

543 i <- State.lift getIState

546 i <- State.lift getIState

@@ -558,7 +561,7 @@ elabEliminator paramPos n ty cons info = do

558

561

559elabPrims :: Idris ()

562elabPrims :: Idris ()

560elabPrims = do mapM_ (elabDecl EAll toplevel)

563elabPrims = 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)

562 (zip

565 (zip

563 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

566 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

564 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

567 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

@@ -626,8 +629,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

626

629

627

630

628-- | Elaborate a type provider

631-- | Elaborate a type provider

629−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

632+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()

630−elabProvider info syn fc n ty tm

633+elabProvider info syn fc what n ty tm

631 = do i <- getIState

634 = do i <- getIState

632 -- Ensure that the experimental extension is enabled

635 -- Ensure that the experimental extension is enabled

633 unless (TypeProviders `elem` idris_language_extensions i) $

636 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -647,9 +650,6 @@ elabProvider info syn fc n ty tm

647 ifail $ "Expected provider type IO (Provider (" ++

650 ifail $ "Expected provider type IO (Provider (" ++

648 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

651 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

649

652

650− -- Create the top-level type declaration

651− elabType info syn "" fc [] n ty

652−

653 -- Execute the type provider and normalise the result

654 -- use 'run__provider' to convert to a primitive IO action

655

@@ -658,12 +658,25 @@ elabProvider info syn fc n ty tm

658 let rhs' = normalise ctxt [] rhs

659 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

660

661− -- Extract the provided term from the type provider

661+ -- Extract the provided term or postulate from the type provider

662− tm <- getProvided fc rhs'

662+ provided <- getProvided fc rhs'

663−

663+

664+ case provided of

665+ Provide tm

666+ | what `elem` [ProvTerm, ProvAny] ->

664− -- Finally add a top-level definition of the provided term

667+ do -- Finally add a top-level definition of the provided term

668+ elabType info syn "" [] fc [] n ty

665− elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

669+ 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

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."

667

680

668 where isTType :: TT Name -> Bool

681 where isTType :: TT Name -> Bool

669 isTType (TType _) = True

682 isTType (TType _) = True

@@ -714,7 +727,7 @@ elabTransform info fc safe lhs_in rhs_in

714elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

727elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

715 PTerm -> String -> Name -> PTerm -> Idris ()

728 PTerm -> String -> Name -> PTerm -> Idris ()

716elabRecord info syn doc fc tyn ty cdoc cn cty

729elabRecord 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, [])])

718 cty' <- implicit syn cn cty

731 cty' <- implicit syn cn cty

719 i <- getIState

732 i <- getIState

720 cty <- case lookupTy cn (tt_ctxt i) of

733 cty <- case lookupTy cn (tt_ctxt i) of

@@ -737,7 +750,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

737 where

750 where

738-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

751-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

739

752

740− isNonImp (PExp _ _ _ _, a) = Just a

753+ isNonImp (PExp _ _ _, a) = Just a

741 isNonImp _ = Nothing

754 isNonImp _ = Nothing

742

755

743 tryElabDecl info (fn, ty, val)

756 tryElabDecl info (fn, ty, val)

@@ -749,15 +762,15 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

749 show fn ++ " (" ++ show ty ++ ")"

762 show fn ++ " (" ++ show ty ++ ")"

750 putIState i)

763 putIState i)

751

764

752− getImplB k (PPi (Imp l s _ _) n Placeholder sc)

765+ getImplB k (PPi (Imp l s _) n Placeholder sc)

753 = getImplB k sc

766 = getImplB k sc

754− getImplB k (PPi (Imp l s d p) n ty sc)

767+ getImplB k (PPi (Imp l s p) n ty sc)

755− = getImplB (\x -> k (PPi (Imp l s d p) n ty x)) sc

768+ = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc

756 getImplB k (PPi _ n ty sc)

769 getImplB k (PPi _ n ty sc)

757 = getImplB k sc

770 = getImplB k sc

758 getImplB k _ = k

771 getImplB k _ = k

759

772

760− renameBs (PImp _ _ _ _ _ _ : ps) (PPi p n ty s)

773+ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)

761 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

774 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

762 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

775 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

763 renameBs _ t = t

776 renameBs _ t = t

@@ -784,7 +797,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

784

797

785 mkProj recty substs cimp ((pn_in, pty), pos)

798 mkProj recty substs cimp ((pn_in, pty), pos)

786 = do let pn = expandNS syn pn_in

799 = do let pn = expandNS syn pn_in

787− let pfnTy = PTy "" defaultSyntax fc [] pn

800+ let pfnTy = PTy "" [] defaultSyntax fc [] pn

788 (PPi expl rec recty

801 (PPi expl rec recty

789 (substMatches substs pty))

802 (substMatches substs pty))

790 let pls = repeat Placeholder

803 let pls = repeat Placeholder

@@ -805,7 +818,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

805 let valname = sMN 0 "updateval"

818 let valname = sMN 0 "updateval"

806 let pt = k (PPi expl pn pty

819 let pt = k (PPi expl pn pty

807 (PPi expl rec recty recty))

820 (PPi expl rec recty recty))

808− let pfnTy = PTy "" defaultSyntax fc [] setname pt

821+ let pfnTy = PTy "" [] defaultSyntax fc [] setname pt

809 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

810 let lhsArgs = pls

823 let lhsArgs = pls

811 let rhsArgs = take pos pls ++ (PRef fc valname) :

824 let rhsArgs = take pos pls ++ (PRef fc valname) :

@@ -821,8 +834,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

821 return (pn, pfnTy, PClauses fc [] setname [pclause])

834 return (pn, pfnTy, PClauses fc [] setname [pclause])

822

835

823elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

824− (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)

837+ (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

825−elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

838+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

826 = do checkUndefined fc n

839 = do checkUndefined fc n

827 ctxt <- getContext

840 ctxt <- getContext

828 i <- getIState

841 i <- getIState

@@ -843,7 +856,8 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

843 tyIs cty'

856 tyIs cty'

844 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

857 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

845 addIBC (IBCDef n)

858 addIBC (IBCDef n)

859+ checkDocs fc argDocs t_in

846− addDocStr n doc

860+ addDocStr n doc argDocs

847 addIBC (IBCDoc n)

861 addIBC (IBCDoc n)

848 let fs = map (getNamePos 0 t) forcenames

862 let fs = map (getNamePos 0 t) forcenames

849 -- FIXME: 'forcenames' is an almighty hack! Need a better way of

863 -- FIXME: 'forcenames' is an almighty hack! Need a better way of

@@ -1148,7 +1162,7 @@ elabPE info fc caller r =

1148 (map (\ (lhs, rhs) ->

1162 (map (\ (lhs, rhs) ->

1149 (showTmImpls lhs ++ " = " ++

1163 (showTmImpls lhs ++ " = " ++

1150 showTmImpls rhs)) pats)

1164 showTmImpls rhs)) pats)

1151− elabType info defaultSyntax "" fc opts newnm specTy

1165+ elabType info defaultSyntax "" [] fc opts newnm specTy

1152 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1166 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1153 elabClauses info fc opts newnm def

1167 elabClauses info fc opts newnm def

1154 logLvl 1 $ "Specialised " ++ show newnm)

1168 logLvl 1 $ "Specialised " ++ show newnm)

@@ -1266,7 +1280,7 @@ checkPossible info fc tcgen fname lhs_in

1266 ((P _ x _, _), (P _ y _, _)) -> x == y

1280 ((P _ x _, _), (P _ y _, _)) -> x == y

1267 _ -> False

1281 _ -> False

1268

1282

1269−getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1283+getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)

1270 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1284 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1271getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1285getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1272 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1286 = 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)

1490-- = NS (UN ('#':show x)) [show cnum, show fname]

1504-- = NS (UN ('#':show x)) [show cnum, show fname]

1491

1505

1492 sepBlocks bs = sepBlocks' [] bs where

1506 sepBlocks bs = sepBlocks' [] bs where

1493− sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)

1507+ sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)

1494 = let (bf, af) = sepBlocks' (n : ns) bs in

1508 = let (bf, af) = sepBlocks' (n : ns) bs in

1495 (d : bf, af)

1509 (d : bf, af)

1496 sepBlocks' ns (d@(PClauses _ _ n _) : bs)

1510 sepBlocks' ns (d@(PClauses _ _ n _) : bs)

@@ -1711,7 +1725,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->

1711 FC -> [PTerm] ->

1725 FC -> [PTerm] ->

1712 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1726 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1713elabClass info syn doc fc constraints tn ps ds

1727elabClass 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)

1715 let tty = pibind ps PType

1729 let tty = pibind ps PType

1716 let constraint = PApp fc (PRef fc tn)

1730 let constraint = PApp fc (PRef fc tn)

1717 (map (pexp . PRef fc) (map fst ps))

1731 (map (pexp . PRef fc) (map fst ps))

@@ -1734,10 +1748,10 @@ elabClass info syn doc fc constraints tn ps ds

1734 let cty = impbind ps $ conbind constraints

1748 let cty = impbind ps $ conbind constraints

1735 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1749 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1736 constraint

1750 constraint

1737− let cons = [("", cn, cty, fc, [])]

1751+ let cons = [("", [], cn, cty, fc, [])]

1738 let ddecl = PDatadecl tn tty cons

1752 let ddecl = PDatadecl tn tty cons

1739 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1753 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

1741 -- for each constraint, build a top level function to chase it

1755 -- for each constraint, build a top level function to chase it

1742 logLvl 5 $ "Building functions"

1756 logLvl 5 $ "Building functions"

1743 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

1757 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -1775,8 +1789,8 @@ elabClass info syn doc fc constraints tn ps ds

1775 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

1789 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

1776 conbind [] x = x

1790 conbind [] x = x

1777

1791

1778− getMName (PTy _ _ _ _ n _) = nsroot n

1792+ getMName (PTy _ _ _ _ _ n _) = nsroot n

1779− tdecl allmeths (PTy doc syn _ o n t)

1793+ tdecl allmeths (PTy doc _ syn _ o n t)

1780 = do t' <- implicit' syn allmeths n t

1794 = do t' <- implicit' syn allmeths n t

1781 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1795 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1782 return ( (n, (toExp (map fst ps) Exp t')),

1796 return ( (n, (toExp (map fst ps) Exp t')),

@@ -1789,7 +1803,7 @@ elabClass info syn doc fc constraints tn ps ds

1789 case lookup n mtys of

1803 case lookup n mtys of

1790 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

1804 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

1791 let ds = map (decorateid defaultdec)

1805 let ds = map (decorateid defaultdec)

1792− [PTy "" syn fc [] n ty',

1806+ [PTy "" [] syn fc [] n ty',

1793 PClauses fc (o ++ opts) n cs]

1807 PClauses fc (o ++ opts) n cs]

1794 iLOG (show ds)

1808 iLOG (show ds)

1795 return (n, ((defaultdec n, ds!!1), ds))

1809 return (n, ((defaultdec n, ds!!1), ds))

@@ -1799,7 +1813,7 @@ elabClass info syn doc fc constraints tn ps ds

1799 defaultdec (UN n) = sUN ("default#" ++ str n)

1813 defaultdec (UN n) = sUN ("default#" ++ str n)

1800 defaultdec (NS n ns) = NS (defaultdec n) ns

1814 defaultdec (NS n ns) = NS (defaultdec n) ns

1801

1815

1802− tydecl (PTy _ _ _ _ _ _) = True

1816+ tydecl (PTy _ _ _ _ _ _ _) = True

1803 tydecl _ = False

1817 tydecl _ = False

1804 instdecl (PInstance _ _ _ _ _ _ _ _) = True

1818 instdecl (PInstance _ _ _ _ _ _ _ _) = True

1805 instdecl _ = False

1819 instdecl _ = False

@@ -1827,7 +1841,7 @@ elabClass info syn doc fc constraints tn ps ds

1827 addInstance False conn' cfn

1841 addInstance False conn' cfn

1828 addIBC (IBCInstance False conn' cfn)

1842 addIBC (IBCInstance False conn' cfn)

1829-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1843-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1830− return [PTy "" syn fc [] cfn ty,

1844+ return [PTy "" [] syn fc [] cfn ty,

1831 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

1845 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

1832

1846

1833 -- Generate a top level function which looks up a method in a given

1847 -- 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

1843 iLOG (showTmImpls ty)

1857 iLOG (showTmImpls ty)

1844 iLOG (show (m, ty', capp, margs))

1858 iLOG (show (m, ty', capp, margs))

1845 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1859 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1846− return [PTy doc syn fc o m ty',

1860+ return [PTy doc [] syn fc o m ty',

1847 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1861 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1848

1862

1849− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

1863+ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

1850− getMArgs (PPi (Exp _ _ _ _) n ty sc) = EA : getMArgs sc

1864+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

1851− getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc

1865+ getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

1852 getMArgs _ = []

1866 getMArgs _ = []

1853

1867

1854 getMeth (m:ms) (a:as) x | x == a = PRef fc m

1868 getMeth (m:ms) (a:as) x | x == a = PRef fc m

@@ -1864,14 +1878,14 @@ elabClass info syn doc fc constraints tn ps ds

1864 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

1878 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

1865 rhsArgs [] _ = []

1879 rhsArgs [] _ = []

1866

1880

1867− insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

1881+ insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

1868 = PPi p n ty (insertConstraint c sc)

1882 = PPi p n ty (insertConstraint c sc)

1869 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc

1883 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc

1870

1884

1871 -- make arguments explicit and don't bind class parameters

1885 -- 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)

1873 | n `elem` ns = toExp ns e sc

1887 | 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)

1875 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

1889 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

1876 toExp ns e sc = sc

1890 toExp ns e sc = sc

1877

1891

@@ -1891,7 +1905,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

1891 let constraint = PApp fc (PRef fc n) (map pexp ps)

1905 let constraint = PApp fc (PRef fc n) (map pexp ps)

1892 let iname = mkiname n ps expn

1906 let iname = mkiname n ps expn

1893 when (what /= EDefns) $ do

1907 when (what /= EDefns) $ do

1894− nty <- elabType' True info syn "" fc [] iname t

1908+ nty <- elabType' True info syn "" [] fc [] iname t

1895 -- if the instance type matches any of the instances we have already,

1909 -- if the instance type matches any of the instances we have already,

1896 -- and it's not a named instance, then it's overlapping, so report an error

1910 -- and it's not a named instance, then it's overlapping, so report an error

1897 case expn of

1911 case expn of

@@ -1999,17 +2013,17 @@ elabInstance info syn what fc cs n ps t expn ds = do

1999

2013

2000 mkMethApp (n, _, _, ty)

2014 mkMethApp (n, _, _, ty)

2001 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

2015 = 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'

2003 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

2017 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

2004 lamBind i (PPi _ n ty sc) sc'

2018 lamBind i (PPi _ n ty sc) sc'

2005 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

2019 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

2006 lamBind i _ sc = sc

2020 lamBind i _ sc = sc

2007− methArgs i (PPi (Imp _ _ _ _) n ty sc)

2021+ methArgs i (PPi (Imp _ _ _) n ty sc)

2008− = PImp 0 True [] n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

2022+ = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2009− methArgs i (PPi (Exp _ _ _ _) n ty sc)

2023+ methArgs i (PPi (Exp _ _ _) n ty sc)

2010− = PExp 0 [] (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

2024+ = PExp 0 [] (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2011− methArgs i (PPi (Constraint _ _ _) n ty sc)

2025+ methArgs i (PPi (Constraint _ _) n ty sc)

2012− = PConstraint 0 [] (PResolveTC fc) "" : methArgs (i+1) sc

2026+ = PConstraint 0 [] (PResolveTC fc) : methArgs (i+1) sc

2013 methArgs i _ = []

2027 methArgs i _ = []

2014

2028

2015 papp fc f [] = f

2029 papp fc f [] = f

@@ -2028,12 +2042,12 @@ elabInstance info syn what fc cs n ps t expn ds = do

2028 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2042 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2029 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2043 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2030

2044

2031− mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

2045+ mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t

2032

2046

2033 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

2047 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

2034 conbind [] x = x

2048 conbind [] x = x

2035

2049

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)

2037 coninsert cs sc = conbind cs sc

2051 coninsert cs sc = conbind cs sc

2038

2052

2039 insertDefaults :: IState -> Name ->

2053 insertDefaults :: IState -> Name ->

@@ -2091,7 +2105,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2091 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

2105 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

2092-}

2106-}

2093

2107

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

2095decorateid decorate (PClauses f o n cs)

2109decorateid decorate (PClauses f o n cs)

2096 = PClauses f o (decorate n) (map dc cs)

2110 = PClauses f o (decorate n) (map dc cs)

2097 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

2111 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 _ _ _)

2145 = return () -- nothing to elaborate

2159 = return () -- nothing to elaborate

2146elabDecl' _ info (PSyntax _ p)

2160elabDecl' _ info (PSyntax _ p)

2147 = return () -- nothing to elaborate

2161 = 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)

2149 | what /= EDefns

2163 | what /= EDefns

2150 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

2164 = 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

2152 return ()

2166 return ()

2153elabDecl' what info (PPostulate doc s f o n ty)

2167elabDecl' what info (PPostulate doc s f o n ty)

2154 | what /= EDefns

2168 | what /= EDefns

2155 = do iLOG $ "Elaborating postulate " ++ show n ++ show o

2169 = do iLOG $ "Elaborating postulate " ++ show n ++ show o

2156 elabPostulate info s doc f o n ty

2170 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)

2158 | what /= ETypes

2172 | what /= ETypes

2159 = do iLOG $ "Elaborating " ++ show (d_name d)

2173 = do iLOG $ "Elaborating " ++ show (d_name d)

2160− elabData info s doc f co d

2174+ elabData info s doc argDocs f co d

2161 | otherwise

2175 | otherwise

2162 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

2176 = 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))

2164elabDecl' what info d@(PClauses f o n ps)

2178elabDecl' what info d@(PClauses f o n ps)

2165 | what /= ETypes

2179 | what /= ETypes

2166 = do iLOG $ "Elaborating clause " ++ show n

2180 = do iLOG $ "Elaborating clause " ++ show n

@@ -2217,17 +2231,17 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

2217 elabRecord info s doc f tyn ty cdoc cn cty

2231 elabRecord info s doc f tyn ty cdoc cn cty

2218 | otherwise

2232 | otherwise

2219 = do iLOG $ "Elaborating [type of] " ++ show tyn

2233 = 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)

2221elabDecl' _ info (PDSL n dsl)

2235elabDecl' _ info (PDSL n dsl)

2222 = do i <- getIState

2236 = do i <- getIState

2223 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

2237 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

2224 addIBC (IBCDSL n)

2238 addIBC (IBCDSL n)

2225elabDecl' what info (PDirective i)

2239elabDecl' what info (PDirective i)

2226 | what /= EDefns = i

2240 | what /= EDefns = i

2227−elabDecl' what info (PProvider syn fc n tp tm)

2241+elabDecl' what info (PProvider syn fc provWhat n tp tm)

2228 | what /= EDefns

2242 | what /= EDefns

2229 = do iLOG $ "Elaborating type provider " ++ show n

2243 = do iLOG $ "Elaborating type provider " ++ show n

2230− elabProvider info syn fc n tp tm

2244+ elabProvider info syn fc provWhat n tp tm

2231elabDecl' what info (PTransform fc safety old new)

2245elabDecl' what info (PTransform fc safety old new)

2232 = elabTransform info fc safety old new

2246 = elabTransform info fc safety old new

2233elabDecl' _ _ _ = return () -- skipped this time

2247elabDecl' _ _ _ = return () -- skipped this time

@@ -2272,3 +2286,14 @@ inferredDiff fc inf user =

2272 Right vs -> return False

2286 Right vs -> return False

2273 Left (x, y) -> return True

2287 Left (x, y) -> return True

2274

2288

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

153 [] -> return ()

154

155 elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()

156− elabE ina t = {- do g <- goal

156+ elabE ina t =

157− tm <- get_term

157+-- do g <- goal

158− trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

158+-- trace ("Elaborating " ++ show t ++ " : " ++ show g) $

159− $ -}

160 do ct <- insertCoerce ina t

159 do ct <- insertCoerce ina t

161 t' <- insertLazy ct

160 t' <- insertLazy ct

162 g <- goal

161 g <- goal

@@ -539,9 +538,9 @@ elab ist info pattern opts fn tm

539 mkN n = case namespace info of

538 mkN n = case namespace info of

540 Just xs@(_:_) -> sNS n xs

539 Just xs@(_:_) -> sNS n xs

541 _ -> n

540 _ -> 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

543 elab' ina (PTactics ts)

542 elab' ina (PTactics ts)

544− | not pattern = do mapM_ (runTac False ist) ts

543+ | not pattern = do mapM_ (runTac False ist fn) ts

545 | otherwise = elab' ina Placeholder

544 | otherwise = elab' ina Placeholder

546 elab' ina (PElabError e) = fail (pshow ist e)

545 elab' ina (PElabError e) = fail (pshow ist e)

547 elab' ina (PRewrite fc r sc newg)

546 elab' ina (PRewrite fc r sc newg)

@@ -841,9 +840,11 @@ proofSearch' ist top n hints

841

840

842

841

843resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

842resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

843+resolveTC = resTC' []

844+

844−resolveTC 0 topg fn ist = fail $ "Can't resolve type class"

845+resTC' tcs 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+resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True

846−resolveTC depth topg fn ist

847+resTC' tcs depth topg fn ist

847 = do hnf_compute

848 = do hnf_compute

848 g <- goal

849 g <- goal

849 ptm <- get_term

850 ptm <- get_term

@@ -915,15 +916,17 @@ resolveTC depth topg fn ist

915 mapM_ (\ (_,n) -> do focus n

916 mapM_ (\ (_,n) -> do focus n

916 t' <- goal

917 t' <- goal

917 let (tc', ttype) = unApply t'

918 let (tc', ttype) = unApply t'

919+ let got = fst (unApply t)

920+ let depth' = if tc' `elem` tcs

918− let depth' = if t == t' then depth - 1 else depth

921+ then depth - 1 else depth

919− resolveTC depth' topg fn ist)

922+ resTC' (got : tcs) depth' topg fn ist)

920 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

923 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

921 -- if there's any arguments left, we've failed to resolve

924 -- if there's any arguments left, we've failed to resolve

922 hs <- get_holes

925 hs <- get_holes

923 ulog <- getUnifyLog

926 ulog <- getUnifyLog

924 solve

927 solve

925 traceWhen ulog ("Got " ++ show n) $ return ()

928 traceWhen ulog ("Got " ++ show n) $ return ()

926− where isImp (PImp p _ _ _ _ _) = (True, p)

929+ where isImp (PImp p _ _ _ _) = (True, p)

927 isImp arg = (False, priority arg)

930 isImp arg = (False, priority arg)

928

931

929collectDeferred :: Maybe Name ->

932collectDeferred :: Maybe Name ->

@@ -947,8 +950,8 @@ collectDeferred top t = return t

947-- Running tactics directly

950-- Running tactics directly

948-- if a tactic adds unification problems, return an error

951-- if a tactic adds unification problems, return an error

949

952

950−runTac :: Bool -> IState -> PTactic -> ElabD ()

953+runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()

951−runTac autoSolve ist tac

954+runTac autoSolve ist fn tac

952 = do env <- get_env

955 = do env <- get_env

953 g <- goal

956 g <- goal

954 if autoSolve

957 if autoSolve

@@ -998,7 +1001,7 @@ runTac autoSolve ist tac

998 show fn')) fnimps

1001 show fn')) fnimps

999 tryAll tacs

1002 tryAll tacs

1000 when autoSolve solveAll

1003 when autoSolve solveAll

1001− where isImp (PImp _ _ _ _ _ _) = True

1004+ where isImp (PImp _ _ _ _ _) = True

1002 isImp _ = False

1005 isImp _ = False

1003 envArgs n = do e <- get_env

1006 envArgs n = do e <- get_env

1004 case lookup n e of

1007 case lookup n e of

@@ -1062,8 +1065,8 @@ runTac autoSolve ist tac

1062 runT Compute = compute

1065 runT Compute = compute

1063 runT Trivial = do trivial' ist; when autoSolve solveAll

1066 runT Trivial = do trivial' ist; when autoSolve solveAll

1064 runT TCInstance = runT (Exact (PResolveTC emptyFC))

1067 runT TCInstance = runT (Exact (PResolveTC emptyFC))

1065− runT (ProofSearch top n hints)

1068+ runT (ProofSearch top hints)

1066− = do proofSearch' ist top n hints; when autoSolve solveAll

1069+ = do proofSearch' ist top fn hints; when autoSolve solveAll

1067 runT (Focus n) = focus n

1070 runT (Focus n) = focus n

1068 runT Solve = solve

1071 runT Solve = solve

1069 runT (Try l r) = do try' (runT l) (runT r) True

1072 runT (Try l r) = do try' (runT l) (runT r) True

@@ -1142,7 +1145,7 @@ runTac autoSolve ist tac

1142 ctxt <- get_context

1145 ctxt <- get_context

1143 env <- get_env

1146 env <- get_env

1144 let value' = hnf ctxt env value

1147 let value' = hnf ctxt env value

1145− runTac autoSolve ist (Exact $ PQuote (reflect value'))

1148+ runTac autoSolve ist fn (Exact $ PQuote (reflect value'))

1146 runT (Fill v) = do attack -- let x = fill x in ...

1149 runT (Fill v) = do attack -- let x = fill x in ...

1147 tyn <- getNameFrom (sMN 0 "letty")

1150 tyn <- getNameFrom (sMN 0 "letty")

1148 claim tyn RType

1151 claim tyn RType

@@ -1157,7 +1160,7 @@ runTac autoSolve ist tac

1157 env <- get_env

1160 env <- get_env

1158 let value' = normalise ctxt env value

1161 let value' = normalise ctxt env value

1159 rawValue <- reifyRaw value'

1162 rawValue <- reifyRaw value'

1160− runTac autoSolve ist (Exact $ PQuote rawValue)

1163+ runTac autoSolve ist fn (Exact $ PQuote rawValue)

1161 runT (GoalType n tac) = do g <- goal

1164 runT (GoalType n tac) = do g <- goal

1162 case unApply g of

1165 case unApply g of

1163 (P _ n' _, _) ->

1166 (P _ n' _, _) ->

@@ -1170,7 +1173,7 @@ runTac autoSolve ist tac

1170 runT x = fail $ "Not implemented " ++ show x

1173 runT x = fail $ "Not implemented " ++ show x

1171

1174

1172 runReflected t = do t' <- reify ist t

1175 runReflected t = do t' <- reify ist t

1173− runTac autoSolve ist t'

1176+ runTac autoSolve ist fn t'

1174

1177

1175-- | Prefix a name with the "Language.Reflection" namespace

1178-- | Prefix a name with the "Language.Reflection" namespace

1176reflm :: String -> Name

1179reflm :: String -> Name

src/Idris/ErrReverse.hs+2−2

@@ -13,7 +13,7 @@ import Debug.Trace

13-- errors will be more readable

14

15errReverse :: IState -> Term -> Term

16−errReverse ist t = rewrite 5 (elideLambdas t)

16+errReverse ist t = rewrite 5 t -- (elideLambdas t)

17 where

18

19 rewrite 0 t = t

@@ -65,7 +65,7 @@ errReverse ist t = rewrite 5 (elideLambdas t)

65

66 elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)

67 elideLambdas (Bind n (Lam t) sc)

68− | size sc > 100 = P Ref (sUN "...") Erased

68+ | size sc > 200 = P Ref (sUN "...") Erased

69 elideLambdas (Bind n b sc)

70 = Bind n (fmap elideLambdas b) (elideLambdas sc)

71 elideLambdas t = t

src/Idris/IBC.hs+55−50

@@ -24,9 +24,8 @@ import System.Directory

24import Codec.Compression.Zlib (compress)

25import Util.Zlib (decompressEither)

26

27−

28ibcVersion :: Word8

27ibcVersion :: Word8

29−ibcVersion = 60

28+ibcVersion = 62

30

29

31

30

32data IBCFile = IBCFile { ver :: Word8,

31data IBCFile = IBCFile { ver :: Word8,

@@ -53,7 +52,7 @@ data IBCFile = IBCFile { ver :: Word8,

53 ibc_flags :: [(Name, [FnOpt])],

52 ibc_flags :: [(Name, [FnOpt])],

54 ibc_cg :: [(Name, CGInfo)],

53 ibc_cg :: [(Name, CGInfo)],

55 ibc_defs :: [(Name, Def)],

54 ibc_defs :: [(Name, Def)],

56− ibc_docstrings :: [(Name, String)],

55+ ibc_docstrings :: [(Name, (String, [(Name, String)]))],

57 ibc_transforms :: [(Term, Term)],

56 ibc_transforms :: [(Term, Term)],

58 ibc_errRev :: [(Term, Term)],

57 ibc_errRev :: [(Term, Term)],

59 ibc_coercions :: [Name],

58 ibc_coercions :: [Name],

@@ -61,7 +60,8 @@ data IBCFile = IBCFile { ver :: Word8,

61 ibc_namehints :: [(Name, Name)],

60 ibc_namehints :: [(Name, Name)],

62 ibc_metainformation :: [(Name, MetaInformation)],

61 ibc_metainformation :: [(Name, MetaInformation)],

63 ibc_errorhandlers :: [Name],

62 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))]

65 }

66 deriving Show

67{-!

@@ -69,8 +69,7 @@ deriving instance Binary IBCFile

69!-}

70

71initIBC :: IBCFile

72−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

72+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

73−

74

73

75loadIBC :: FilePath -> Idris ()

74loadIBC :: FilePath -> Idris ()

76loadIBC fp = do iLOG $ "Loading ibc " ++ fp

75loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -91,9 +90,9 @@ writeIBC :: FilePath -> FilePath -> Idris ()

91writeIBC src f

90writeIBC src f

92 = do iLOG $ "Writing ibc " ++ show f

91 = do iLOG $ "Writing ibc " ++ show f

93 i <- getIState

92 i <- getIState

94− case (Data.List.map fst (idris_metavars i)) \\ primDefs of

93+-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

95− (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

94+-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

96− [] -> return ()

95+-- [] -> return ()

97 resetNameIdx

96 resetNameIdx

98 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

97 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

99 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

98 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

@@ -222,6 +221,10 @@ ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_

222ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }

221ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }

223ibc i (IBCFunctionErrorHandler fn a n) f =

222ibc i (IBCFunctionErrorHandler fn a n) f =

224 return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }

223 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 }

225

228

226process :: IBCFile -> FilePath -> Idris ()

229process :: IBCFile -> FilePath -> Idris ()

227process i fn

230process i fn

@@ -262,6 +265,7 @@ process i fn

262 pMetaInformation (ibc_metainformation i)

265 pMetaInformation (ibc_metainformation i)

263 pErrorHandlers (ibc_errorhandlers i)

266 pErrorHandlers (ibc_errorhandlers i)

264 pFunctionErrorHandlers (ibc_function_errorhandlers i)

267 pFunctionErrorHandlers (ibc_function_errorhandlers i)

268+ pMetavars (ibc_metavars i)

265

269

266timestampOlder :: FilePath -> FilePath -> IO ()

270timestampOlder :: FilePath -> FilePath -> IO ()

267timestampOlder src ibc = do srct <- getModificationTime src

271timestampOlder src ibc = do srct <- getModificationTime src

@@ -389,7 +393,7 @@ pDefs syms ds

389 updateOrig (Left t) = Left (update t)

393 updateOrig (Left t) = Left (update t)

390 updateOrig (Right (l, r)) = Right (update l, update r)

394 updateOrig (Right (l, r)) = Right (update l, update r)

391

395

392− updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

396+ updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

393 = CaseDefs (ts, fmap update t)

397 = CaseDefs (ts, fmap update t)

394 (cs, fmap update c)

398 (cs, fmap update c)

395 (is, fmap update i)

399 (is, fmap update i)

@@ -401,8 +405,8 @@ pDefs syms ds

401 update (Proj t i) = Proj (update t) i

405 update (Proj t i) = Proj (update t) i

402 update t = t

406 update t = t

403

407

404−pDocs :: [(Name, String)] -> Idris ()

408+pDocs :: [(Name, (String, [(Name, String)]))] -> Idris ()

405−pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds

409+pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

406

410

407pAccess :: [(Name, Accessibility)] -> Idris ()

411pAccess :: [(Name, Accessibility)] -> Idris ()

408pAccess ds = mapM_ (\ (n, a) ->

412pAccess ds = mapM_ (\ (n, a) ->

@@ -451,6 +455,12 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

451pFunctionErrorHandlers [] = return ()

455pFunctionErrorHandlers [] = return ()

452pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]

456pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]

453 pFunctionErrorHandlers ns

457 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+

454----- Generated by 'derive'

464----- Generated by 'derive'

455

465

456instance Binary SizeChange where

466instance Binary SizeChange where

@@ -549,6 +559,7 @@ instance Binary SpecialName where

549 put x1

559 put x1

550 CaseN x1 -> do putWord8 4; put x1

560 CaseN x1 -> do putWord8 4; put x1

551 ElimN x1 -> do putWord8 5; put x1

561 ElimN x1 -> do putWord8 5; put x1

562+ InstanceCtorN x1 -> do putWord8 6; put x1

552 get

563 get

553 = do i <- getWord8

564 = do i <- getWord8

554 case i of

565 case i of

@@ -568,6 +579,8 @@ instance Binary SpecialName where

568 return (CaseN x1)

579 return (CaseN x1)

569 5 -> do x1 <- get

580 5 -> do x1 <- get

570 return (ElimN x1)

581 return (ElimN x1)

582+ 6 -> do x1 <- get

583+ return (InstanceCtorN x1)

571 _ -> error "Corrupted binary data for SpecialName"

584 _ -> error "Corrupted binary data for SpecialName"

572

585

573

586

@@ -607,6 +620,7 @@ instance Binary Const where

607 B32V x1 -> putWord8 23 >> put x1

620 B32V x1 -> putWord8 23 >> put x1

608 B64V x1 -> putWord8 24 >> put x1

621 B64V x1 -> putWord8 24 >> put x1

609 BufferType -> putWord8 25

622 BufferType -> putWord8 25

623+ ManagedPtrType -> putWord8 26

610 get

624 get

611 = do i <- getWord8

625 = do i <- getWord8

612 case i of

626 case i of

@@ -648,6 +662,7 @@ instance Binary Const where

648 23 -> fmap B32V get

662 23 -> fmap B32V get

649 24 -> fmap B64V get

663 24 -> fmap B64V get

650 25 -> return BufferType

664 25 -> return BufferType

665+ 26 -> return ManagedPtrType

651

666

652 _ -> error "Corrupted binary data for Const"

667 _ -> error "Corrupted binary data for Const"

653

668

@@ -1037,7 +1052,7 @@ instance Binary MetaInformation where

1037 return (DataMI x1)

1052 return (DataMI x1)

1038

1053

1039instance Binary IBCFile where

1054instance 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)

1041 = {-# SCC "putIBCFile" #-}

1056 = {-# SCC "putIBCFile" #-}

1042 do put x1

1057 do put x1

1043 put x2

1058 put x2

@@ -1072,6 +1087,7 @@ instance Binary IBCFile where

1072 put x31

1087 put x31

1073 put x32

1088 put x32

1074 put x33

1089 put x33

1090+ put x34

1075

1091

1076 get

1092 get

1077 = do x1 <- get

1093 = do x1 <- get

@@ -1108,7 +1124,8 @@ instance Binary IBCFile where

1108 x31 <- get

1124 x31 <- get

1109 x32 <- get

1125 x32 <- get

1110 x33 <- get

1126 x33 <- get

1127+ x34 <- 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)

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)

1112 else return (initIBC { ver = x1 })

1129 else return (initIBC { ver = x1 })

1113

1130

1114instance Binary DataOpt where

1131instance Binary DataOpt where

@@ -1217,51 +1234,43 @@ instance Binary Static where

1217instance Binary Plicity where

1234instance Binary Plicity where

1218 put x

1235 put x

1219 = case x of

1236 = case x of

1220− Imp x1 x2 x3 x4 ->

1237+ Imp x1 x2 x3 ->

1221 do putWord8 0

1238 do putWord8 0

1222 put x1

1239 put x1

1223 put x2

1240 put x2

1224 put x3

1241 put x3

1225− put x4

1226− Exp x1 x2 x3 x4 ->

1242+ Exp x1 x2 x3 ->

1227 do putWord8 1

1243 do putWord8 1

1228 put x1

1244 put x1

1229 put x2

1245 put x2

1230 put x3

1246 put x3

1231− put x4

1232− Constraint x1 x2 x3 ->

1247+ Constraint x1 x2 ->

1233 do putWord8 2

1248 do putWord8 2

1234 put x1

1249 put x1

1235 put x2

1250 put x2

1236− put x3

1237− TacImp x1 x2 x3 x4 ->

1251+ TacImp x1 x2 x3 ->

1238 do putWord8 3

1252 do putWord8 3

1239 put x1

1253 put x1

1240 put x2

1254 put x2

1241 put x3

1255 put x3

1242− put x4

1243 get

1256 get

1244 = do i <- getWord8

1257 = do i <- getWord8

1245 case i of

1258 case i of

1246 0 -> do x1 <- get

1259 0 -> do x1 <- get

1247 x2 <- get

1260 x2 <- get

1248 x3 <- get

1261 x3 <- get

1249− x4 <- get

1250− return (Imp x1 x2 x3 x4)

1262+ return (Imp x1 x2 x3)

1251 1 -> do x1 <- get

1263 1 -> do x1 <- get

1252 x2 <- get

1264 x2 <- get

1253 x3 <- get

1265 x3 <- get

1254− x4 <- get

1255− return (Exp x1 x2 x3 x4)

1266+ return (Exp x1 x2 x3)

1256 2 -> do x1 <- get

1267 2 -> do x1 <- get

1257 x2 <- get

1268 x2 <- get

1258− x3 <- get

1259− return (Constraint x1 x2 x3)

1269+ return (Constraint x1 x2)

1260 3 -> do x1 <- get

1270 3 -> do x1 <- get

1261 x2 <- get

1271 x2 <- get

1262 x3 <- get

1272 x3 <- get

1263− x4 <- get

1264− return (TacImp x1 x2 x3 x4)

1273+ return (TacImp x1 x2 x3)

1265 _ -> error "Corrupted binary data for Plicity"

1274 _ -> error "Corrupted binary data for Plicity"

1266

1275

1267

1276

@@ -1272,7 +1281,7 @@ instance (Binary t) => Binary (PDecl' t) where

1272 put x1

1281 put x1

1273 put x2

1282 put x2

1274 put x3

1283 put x3

1275− PTy x1 x2 x3 x4 x5 x6

1284+ PTy x1 x2 x3 x4 x5 x6 x7

1276 -> do putWord8 1

1285 -> do putWord8 1

1277 put x1

1286 put x1

1278 put x2

1287 put x2

@@ -1280,18 +1289,20 @@ instance (Binary t) => Binary (PDecl' t) where

1280 put x4

1289 put x4

1281 put x5

1290 put x5

1282 put x6

1291 put x6

1292+ put x7

1283 PClauses x1 x2 x3 x4 -> do putWord8 2

1293 PClauses x1 x2 x3 x4 -> do putWord8 2

1284 put x1

1294 put x1

1285 put x2

1295 put x2

1286 put x3

1296 put x3

1287 put x4

1297 put x4

1288− PData x1 x2 x3 x4 x5 ->

1298+ PData x1 x2 x3 x4 x5 x6 ->

1289 do putWord8 3

1299 do putWord8 3

1290 put x1

1300 put x1

1291 put x2

1301 put x2

1292 put x3

1302 put x3

1293 put x4

1303 put x4

1294 put x5

1304 put x5

1305+ put x6

1295 PParams x1 x2 x3 -> do putWord8 4

1306 PParams x1 x2 x3 -> do putWord8 4

1296 put x1

1307 put x1

1297 put x2

1308 put x2

@@ -1358,7 +1369,8 @@ instance (Binary t) => Binary (PDecl' t) where

1358 x4 <- get

1369 x4 <- get

1359 x5 <- get

1370 x5 <- get

1360 x6 <- get

1371 x6 <- get

1372+ x7 <- get

1361− return (PTy x1 x2 x3 x4 x5 x6)

1373+ return (PTy x1 x2 x3 x4 x5 x6 x7)

1362 2 -> do x1 <- get

1374 2 -> do x1 <- get

1363 x2 <- get

1375 x2 <- get

1364 x3 <- get

1376 x3 <- get

@@ -1369,7 +1381,8 @@ instance (Binary t) => Binary (PDecl' t) where

1369 x3 <- get

1381 x3 <- get

1370 x4 <- get

1382 x4 <- get

1371 x5 <- get

1383 x5 <- get

1384+ x6 <- get

1372− return (PData x1 x2 x3 x4 x5)

1385+ return (PData x1 x2 x3 x4 x5 x6)

1373 4 -> do x1 <- get

1386 4 -> do x1 <- get

1374 x2 <- get

1387 x2 <- get

1375 x3 <- get

1388 x3 <- get

@@ -1907,34 +1920,30 @@ instance (Binary t) => Binary (PDo' t) where

1907instance (Binary t) => Binary (PArg' t) where

1920instance (Binary t) => Binary (PArg' t) where

1908 put x

1921 put x

1909 = case x of

1922 = case x of

1910− PImp x1 x2 x3 x4 x5 x6 ->

1923+ PImp x1 x2 x3 x4 x5 ->

1911 do putWord8 0

1924 do putWord8 0

1912 put x1

1925 put x1

1913 put x2

1926 put x2

1914 put x3

1927 put x3

1915 put x4

1928 put x4

1916 put x5

1929 put x5

1917− put x6

1918− PExp x1 x2 x3 x4 ->

1930+ PExp x1 x2 x3 ->

1919 do putWord8 1

1931 do putWord8 1

1920 put x1

1932 put x1

1921 put x2

1933 put x2

1922 put x3

1934 put x3

1923− put x4

1924− PConstraint x1 x2 x3 x4 ->

1935+ PConstraint x1 x2 x3 ->

1925 do putWord8 2

1936 do putWord8 2

1926 put x1

1937 put x1

1927 put x2

1938 put x2

1928 put x3

1939 put x3

1929− put x4

1930− PTacImplicit x1 x2 x3 x4 x5 x6 ->

1940+ PTacImplicit x1 x2 x3 x4 x5 ->

1931 do putWord8 3

1941 do putWord8 3

1932 put x1

1942 put x1

1933 put x2

1943 put x2

1934 put x3

1944 put x3

1935 put x4

1945 put x4

1936 put x5

1946 put x5

1937− put x6

1938 get

1947 get

1939 = do i <- getWord8

1948 = do i <- getWord8

1940 case i of

1949 case i of

@@ -1943,25 +1952,21 @@ instance (Binary t) => Binary (PArg' t) where

1943 x3 <- get

1952 x3 <- get

1944 x4 <- get

1953 x4 <- get

1945 x5 <- get

1954 x5 <- get

1946− x6 <- get

1947− return (PImp x1 x2 x3 x4 x5 x6)

1955+ return (PImp x1 x2 x3 x4 x5)

1948 1 -> do x1 <- get

1956 1 -> do x1 <- get

1949 x2 <- get

1957 x2 <- get

1950 x3 <- get

1958 x3 <- get

1951− x4 <- get

1952− return (PExp x1 x2 x3 x4)

1959+ return (PExp x1 x2 x3)

1953 2 -> do x1 <- get

1960 2 -> do x1 <- get

1954 x2 <- get

1961 x2 <- get

1955 x3 <- get

1962 x3 <- get

1956− x4 <- get

1957− return (PConstraint x1 x2 x3 x4)

1963+ return (PConstraint x1 x2 x3)

1958 3 -> do x1 <- get

1964 3 -> do x1 <- get

1959 x2 <- get

1965 x2 <- get

1960 x3 <- get

1966 x3 <- get

1961 x4 <- get

1967 x4 <- get

1962 x5 <- get

1968 x5 <- get

1963− x6 <- get

1964− return (PTacImplicit x1 x2 x3 x4 x5 x6)

1969+ return (PTacImplicit x1 x2 x3 x4 x5)

1965 _ -> error "Corrupted binary data for PArg'"

1970 _ -> error "Corrupted binary data for PArg'"

1966

1971

1967

1972

src/Idris/ParseData.hs+26−24

@@ -33,13 +33,15 @@ import qualified Data.HashSet as HS

33import qualified Data.Text as T

34import qualified Data.ByteString.UTF8 as UTF8

35

36+import Debug.Trace

37+

36{- |Parses a record type declaration

38{- |Parses a record type declaration

37Record ::=

39Record ::=

38 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

40 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

39-}

41-}

40record :: SyntaxInfo -> IdrisParser PDecl

42record :: SyntaxInfo -> IdrisParser PDecl

41record syn = do (doc, acc) <- try (do

43record syn = do (doc, acc) <- try (do

42− doc <- option "" (docComment '|')

44+ doc <- option ("", []) docComment

43 acc <- optional accessibility

45 acc <- optional accessibility

44 reserved "record"

46 reserved "record"

45 return (doc, acc))

47 return (doc, acc))

@@ -49,13 +51,13 @@ record syn = do (doc, acc) <- try (do

49 ty <- typeExpr (allowImp syn)

51 ty <- typeExpr (allowImp syn)

50 let tyn = expandNS syn tyn_in

52 let tyn = expandNS syn tyn_in

51 reserved "where"

53 reserved "where"

52− (cdoc, cn, cty, _, _) <- indentedBlockS (constructor syn)

54+ (cdoc, argDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)

53 accData acc tyn [cn]

55 accData acc tyn [cn]

54 let rsyn = syn { syn_namespace = show (nsroot tyn) :

56 let rsyn = syn { syn_namespace = show (nsroot tyn) :

55 syn_namespace syn }

57 syn_namespace syn }

56 let fns = getRecNames rsyn cty

58 let fns = getRecNames rsyn cty

57 mapM_ (\n -> addAcc n acc) fns

59 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

59 <?> "record type declaration"

61 <?> "record type declaration"

60 where

62 where

61 getRecNames :: SyntaxInfo -> PTerm -> [Name]

63 getRecNames :: SyntaxInfo -> PTerm -> [Name]

@@ -100,29 +102,29 @@ SimpleConstructorList ::=

100 ;

102 ;

101-}

103-}

102data_ :: SyntaxInfo -> IdrisParser PDecl

104data_ :: SyntaxInfo -> IdrisParser PDecl

103−data_ syn = do (doc, acc, dataOpts) <- try (do

105+data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

104− doc <- option "" (docComment '|')

106+ (doc, argDocs) <- option ("", []) docComment

105 pushIndent

107 pushIndent

106 acc <- optional accessibility

108 acc <- optional accessibility

107 elim <- dataOpts []

109 elim <- dataOpts []

108 co <- dataI

110 co <- dataI

109 let dataOpts = combineDataOpts(elim ++ co)

111 let dataOpts = combineDataOpts(elim ++ co)

110− return (doc, acc, dataOpts))

112+ return (doc, argDocs, acc, dataOpts))

111 fc <- getFC

113 fc <- getFC

112 tyn_in <- fnName

114 tyn_in <- fnName

113 (do try (lchar ':')

115 (do try (lchar ':')

114 popIndent

116 popIndent

115 ty <- typeExpr (allowImp syn)

117 ty <- typeExpr (allowImp syn)

116 let tyn = expandNS syn tyn_in

118 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

118 reserved "where"

120 reserved "where"

119 cons <- indentedBlock (constructor syn)

121 cons <- indentedBlock (constructor syn)

120− accData acc tyn (map (\ (_, n, _, _, _) -> n) cons)

122+ accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons)

121− return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

123+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

122 args <- many name

124 args <- many name

123 let ty = bindArgs (map (const PType) args) PType

125 let ty = bindArgs (map (const PType) args) PType

124 let tyn = expandNS syn tyn_in

126 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

126 try (lchar '=') <|> do reserved "where"

128 try (lchar '=') <|> do reserved "where"

127 let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

129 let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

128 let n = show tyn_in ++ " "

130 let n = show tyn_in ++ " "

@@ -134,14 +136,14 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

134 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

136 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

135 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

137 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

136 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

138 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

137− cons <- sepBy1 (simpleConstructor syn) (lchar '|')

139+ cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

138 terminator

140 terminator

139 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

141 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) ->

141 do let cty = bindArgs cargs conty

143 do let cty = bindArgs cargs conty

142− return (doc, x, cty, cfc, fs)) cons

144+ return (doc, argDocs, x, cty, cfc, fs)) cons

143− accData acc tyn (map (\ (_, n, _, _, _) -> n) cons')

145+ accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons')

144− return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))

146+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons')))

145 <?> "data type declaration"

147 <?> "data type declaration"

146 where

148 where

147 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

149 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

@@ -150,17 +152,17 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

150 bindArgs :: [PTerm] -> PTerm -> PTerm

152 bindArgs :: [PTerm] -> PTerm -> PTerm

151 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

153 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

152 combineDataOpts :: DataOpts -> DataOpts

154 combineDataOpts :: DataOpts -> DataOpts

153− combineDataOpts opts = if Codata `elem` opts

155+ combineDataOpts opts = if Codata `elem` opts

154− then delete DefaultEliminator opts

156+ then delete DefaultEliminator opts

155 else opts

157 else opts

156

158

157

159

158{- | Parses a type constructor declaration

160{- | Parses a type constructor declaration

159 Constructor ::= DocComment? FnName TypeSig;

161 Constructor ::= DocComment? FnName TypeSig;

160-}

162-}

161−constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC, [Name])

163+constructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, PTerm, FC, [Name])

162constructor syn

164constructor syn

163− = do doc <- option "" (docComment '|')

165+ = do (doc, argDocs) <- option ("", []) docComment

164 cn_in <- fnName; fc <- getFC

166 cn_in <- fnName; fc <- getFC

165 let cn = expandNS syn cn_in

167 let cn = expandNS syn cn_in

166 lchar ':'

168 lchar ':'

@@ -169,21 +171,21 @@ constructor syn

169 fs <- option [] (do lchar '%'; reserved "erase"

171 fs <- option [] (do lchar '%'; reserved "erase"

170 sepBy1 name (lchar ','))

172 sepBy1 name (lchar ','))

171 ty <- typeExpr (allowImp syn)

173 ty <- typeExpr (allowImp syn)

172− return (doc, cn, ty, fc, fs)

174+ return (doc, argDocs, cn, ty, fc, fs)

173 <?> "constructor"

175 <?> "constructor"

174

176

175{- | Parses a constructor for simple discriminative union data types

177{- | Parses a constructor for simple discriminative union data types

176 SimpleConstructor ::= FnName SimpleExpr* DocComment?

178 SimpleConstructor ::= FnName SimpleExpr* DocComment?

177-}

179-}

178−simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC, [Name])

180+simpleConstructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, [PTerm], FC, [Name])

179simpleConstructor syn

181simpleConstructor syn

182+ = do doc <- option ("", []) (try docComment)

180− = do cn_in <- fnName

183+ cn_in <- fnName

181 let cn = expandNS syn cn_in

184 let cn = expandNS syn cn_in

182 fc <- getFC

185 fc <- getFC

183 args <- many (do notEndApp

186 args <- many (do notEndApp

184 simpleExpr syn)

187 simpleExpr syn)

185− doc <- option "" (try $ docComment '^')

186− return (doc, cn, args, fc, [])

188+ return (fst doc, [], cn, args, fc, [])

187 <?> "constructor"

189 <?> "constructor"

188

190

189{- | Parses a dsl block declaration

191{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+7−5

@@ -786,10 +786,9 @@ pi syn =

786 return []

787 st <- static

788 (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

789− doc <- option "" (docComment '^')

790 symbol "->"

789 symbol "->"

791 sc <- expr syn

790 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

793 lchar '{'

792 lchar '{'

794 (do reserved "auto"

793 (do reserved "auto"

795 when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

794 when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

@@ -798,7 +797,7 @@ pi syn =

798 symbol "->"

797 symbol "->"

799 sc <- expr syn

798 sc <- expr syn

800 return (bindList (PPi

799 return (bindList (PPi

801− (TacImp [] Dynamic (PTactics [Trivial]) "")) xt sc))

800+ (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

802 <|> (do

801 <|> (do

803 reserved "default"

802 reserved "default"

804 when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

803 when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

@@ -807,13 +806,13 @@ pi syn =

807 lchar '}'

806 lchar '}'

808 symbol "->"

807 symbol "->"

809 sc <- expr syn

808 sc <- expr syn

810− return (bindList (PPi (TacImp [] Dynamic script "")) xt sc))

809+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

811 <|> (if implicitAllowed syn then do

810 <|> (if implicitAllowed syn then do

812 xt <- typeDeclList syn

811 xt <- typeDeclList syn

813 lchar '}'

812 lchar '}'

814 symbol "->"

813 symbol "->"

815 sc <- expr syn

814 sc <- expr syn

816− return (bindList (PPi (Imp opts st "" False)) xt sc)

815+ return (bindList (PPi (Imp opts st False)) xt sc)

817 else do fail "no implicit arguments allowed here"))

816 else do fail "no implicit arguments allowed here"))

818 <?> "dependent type signature"

817 <?> "dependent type signature"

819

818

@@ -1003,6 +1002,7 @@ Constant ::=

1003 | 'Float'

1002 | 'Float'

1004 | 'String'

1003 | 'String'

1005 | 'Ptr'

1004 | 'Ptr'

1005+ | 'ManagedPtr'

1006 | 'prim__UnsafeBuffer'

1007 | 'Bits8'

1008 | 'Bits16'

@@ -1027,6 +1027,7 @@ constant = do reserved "Integer"; return (AType (ATInt ITBig))

1027 <|> do reserved "Float"; return (AType ATFloat)

1028 <|> do reserved "String"; return StrType

1029 <|> do reserved "Ptr"; return PtrType

1030+ <|> do reserved "ManagedPtr"; return ManagedPtrType

1030 <|> do reserved "prim__UnsafeBuffer"; return BufferType

1031 <|> do reserved "prim__UnsafeBuffer"; return BufferType

1031 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))

1032 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))

1032 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))

1033 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))

@@ -1165,6 +1166,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1165 return $ TSeq t (mergeSeq ts)

1166 return $ TSeq t (mergeSeq ts)

1166 <|> do reserved "compute"; return Compute

1167 <|> do reserved "compute"; return Compute

1167 <|> do reserved "trivial"; return Trivial

1168 <|> do reserved "trivial"; return Trivial

1169+ <|> do reserved "search"; return (ProofSearch Nothing [])

1168 <|> do reserved "instance"; return TCInstance

1170 <|> do reserved "instance"; return TCInstance

1169 <|> do reserved "solve"; return Solve

1171 <|> do reserved "solve"; return Solve

1170 <|> do reserved "attack"; return Attack

1172 <|> do reserved "attack"; return Attack

src/Idris/ParseHelpers.hs+33−32

@@ -17,6 +17,8 @@ import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

19

20+import qualified Util.Pretty as Pretty (text)

21+

20import Control.Applicative

22import Control.Applicative

21import Control.Monad

23import Control.Monad

22import Control.Monad.State.Strict

24import Control.Monad.State.Strict

@@ -33,6 +35,8 @@ import qualified Data.ByteString.UTF8 as UTF8

33

35

34import System.FilePath

36import System.FilePath

35

37

38+import Debug.Trace

39+

36-- | Idris parser with state used during parsing

40-- | Idris parser with state used during parsing

37type IdrisParser = StateT IState IdrisInnerParser

41type IdrisParser = StateT IState IdrisInnerParser

38

42

@@ -51,10 +55,10 @@ runparser p i inputname =

51 parseString (runInnerParser (evalStateT p i))

55 parseString (runInnerParser (evalStateT p i))

52 (Directed (UTF8.fromString inputname) 0 0 0 0)

56 (Directed (UTF8.fromString inputname) 0 0 0 0)

53

57

54−noDocCommentHere :: Char -> String -> IdrisParser ()

58+noDocCommentHere :: String -> IdrisParser ()

55−noDocCommentHere c msg =

59+noDocCommentHere msg =

56 optional (do fc <- getFC

60 optional (do fc <- getFC

57− docComment c

61+ docComment

58 ist <- get

62 ist <- get

59 put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>

63 put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>

60 pure ()

64 pure ()

@@ -86,12 +90,6 @@ isEol _ = False

86eol :: MonadicParsing m => m ()

90eol :: MonadicParsing m => m ()

87eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

91eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

88

92

89−-- | Checks if a character is a documentation comment marker

90−isDocCommentMarker :: Char -> Bool

91−isDocCommentMarker '|' = True

92−isDocCommentMarker '^' = True

93−isDocCommentMarker _ = False

94−

95{- | Consumes a single-line comment

93{- | Consumes a single-line comment

96

94

97@

95@

@@ -103,7 +101,6 @@ isDocCommentMarker _ = False

103singleLineComment :: MonadicParsing m => m ()

101singleLineComment :: MonadicParsing m => m ()

104singleLineComment = try (string "--" *> eol *> pure ())

102singleLineComment = try (string "--" *> eol *> pure ())

105 <|> try (string "--" *> many simpleWhiteSpace *>

103 <|> try (string "--" *> many simpleWhiteSpace *>

106− satisfy (not . isDocCommentMarker) *>

107 many (satisfy (not . isEol)) *>

104 many (satisfy (not . isEol)) *>

108 eol *> pure ())

105 eol *> pure ())

109 <?> ""

106 <?> ""

@@ -127,13 +124,12 @@ singleLineComment = try (string "--" *> eol *> pure ())

127-}

124-}

128multiLineComment :: MonadicParsing m => m ()

125multiLineComment :: MonadicParsing m => m ()

129multiLineComment = try (string "{-" *> (string "-}") *> pure ())

126multiLineComment = try (string "{-" *> (string "-}") *> pure ())

130− <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars

127+ <|> string "{-" *> inCommentChars

131 <?> ""

128 <?> ""

132 where inCommentChars :: MonadicParsing m => m ()

129 where inCommentChars :: MonadicParsing m => m ()

133 inCommentChars = string "-}" *> pure ()

130 inCommentChars = string "-}" *> pure ()

134 <|> try (multiLineComment) *> inCommentChars

131 <|> try (multiLineComment) *> inCommentChars

135− <|> try (docComment '|') *> inCommentChars

136− <|> try (docComment '^') *> inCommentChars

132+ <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

137 <|> skipSome (noneOf startEnd) *> inCommentChars

133 <|> skipSome (noneOf startEnd) *> inCommentChars

138 <|> oneOf startEnd *> inCommentChars

134 <|> oneOf startEnd *> inCommentChars

139 <?> "end of comment"

135 <?> "end of comment"

@@ -148,27 +144,32 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

148 ;

144 ;

149@

145@

150 -}

146 -}

151−docComment :: MonadicParsing m => Char -> m String

147+docComment :: IdrisParser (String, [(Name, String)])

152−docComment marker | isDocCommentMarker marker = do dc <- docComment' marker

148+docComment = do dc <- pushIndent *> docCommentLine

149+ rest <- many (indented docCommentLine)

150+ args <- many (indented argDocCommentLine)

151+ popIndent

153− return (T.unpack $ T.strip $ T.pack dc)

152+ return (T.unpack $ T.strip $ T.pack (dc ++ concat rest), args)

154− | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"

153+

155− where docComment' :: MonadicParsing m => Char -> m String

154+ where docCommentLine :: MonadicParsing m => m String

156− docComment' marker = (do string "--"

155+ docCommentLine = try (do string "|||"

157 many (satisfy isSpace)

156 many (satisfy isSpace)

158− char marker

157+ first <- satisfy (\c -> not (isEol c || c == '@'))

159 res <- many (satisfy (not . isEol))

158 res <- many (satisfy (not . isEol))

160− eol

159+ eol ; someSpace

161− rest <- many (do string "--"

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)

162− stuff <- many (satisfy (not . isEol))

168+ docs <- many (satisfy (not . isEol))

163− eol

164− return stuff)

165− someSpace

169+ eol ; someSpace

166− return (res ++ concat rest))-- ++ concat rest))

170+ return (n, docs)

167− <|> (do string "{-"

171+

168− many (satisfy isSpace)

172+

169− char marker

170− (manyTill anyChar (try (string "-}")) <?> "end of comment"))

171− <?> ""

172

173

173-- | Parses some white space

174-- | Parses some white space

174whiteSpace :: MonadicParsing m => m ()

175whiteSpace :: MonadicParsing m => m ()

src/Idris/ParseOps.hs+1−1

@@ -59,7 +59,7 @@ binary name f = Infix (do fc <- getFC

59 indentPropHolds gtProp

60 reservedOp name

61 indentPropHolds gtProp

62− doc <- option "" (docComment '^')

62+ doc <- option ("", []) docComment

63 return (f fc))

64

65-- | Prefix operator

src/Idris/Parser.hs+72−61

@@ -87,7 +87,7 @@ import System.IO

87@

88-}

89moduleHeader :: IdrisParser [String]

90−moduleHeader = try (do noDocCommentHere '|' "Modules cannot have documentation comments"

90+moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"

91 reserved "module"

92 i <- identifier

93 option ';' (lchar ';')

@@ -315,7 +315,7 @@ fnDecl' syn = checkFixity $

315 do (doc, fc, opts', n, acc) <- try (do

316 pushIndent

317 ist <- get

318− doc <- option "" (docComment '|')

318+ doc <- option ("", []) docComment

319 ist <- get

320 let initOpts = if default_total ist

321 then [TotalFn]

@@ -331,7 +331,7 @@ fnDecl' syn = checkFixity $

331 ty <- typeExpr (allowImp syn)

332 terminator

333 addAcc n acc

334− return (PTy doc syn fc opts' n ty)

334+ return (PTy (fst doc) (snd doc) syn fc opts' n ty)

335 <|> postulate syn

336 <|> caf syn

337 <|> pattern syn

@@ -344,7 +344,7 @@ fnDecl' syn = checkFixity $

344 unless fOk . fail $

345 "Missing fixity declaration for " ++ show n

346 return decl

347− getName (PTy _ _ _ _ n _) = Just n

347+ getName (PTy _ _ _ _ _ n _) = Just n

348 getName _ = Nothing

349 fixityOK (NS n _) = fixityOK n

350 fixityOK (UN n) | all (flip elem opChars) (str n) =

@@ -413,7 +413,7 @@ Postulate ::=

413@

414-}

415postulate :: SyntaxInfo -> IdrisParser PDecl

416−postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

416+postulate syn = do doc <- try $ do doc <- option ("", []) docComment

417 pushIndent

418 reserved "postulate"

419 return doc

@@ -431,7 +431,7 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

431 fc <- getFC

432 terminator

433 addAcc n acc

434− return (PPostulate doc syn fc opts' n ty)

434+ return (PPostulate (fst doc) syn fc opts' n ty)

435 <?> "postulate"

436

437{- | Parses a using declaration

@@ -561,7 +561,7 @@ Class ::=

561-}

562class_ :: SyntaxInfo -> IdrisParser [PDecl]

563class_ syn = do (doc, acc) <- try (do

564− doc <- option "" (docComment '|')

564+ doc <- option ("", []) docComment

565 acc <- optional accessibility

566 return (doc, acc))

567 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

@@ -569,7 +569,7 @@ class_ syn = do (doc, acc) <- try (do

569 cs <- many carg

570 ds <- option [] (classBlock syn)

571 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]

573 <?> "type-class declaration"

574 where

575 carg :: IdrisParser (Name, PTerm)

@@ -1039,18 +1039,25 @@ totality

1039{- | Parses a type provider

1040

1041@

1042−Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;

1042+Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1043+ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1043@

1044@

1044 -}

1045 -}

1045provider :: SyntaxInfo -> IdrisParser [PDecl]

1046provider :: SyntaxInfo -> IdrisParser [PDecl]

1046provider syn = do try (lchar '%' *> reserved "provide");

1047provider syn = do try (lchar '%' *> reserved "provide");

1048+ what <- provideWhat

1047 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1049 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1048 fc <- getFC

1050 fc <- getFC

1049 reserved "with"

1051 reserved "with"

1050 e <- expr syn

1052 e <- expr syn

1051− return [PProvider syn fc n t e]

1053+ return [PProvider syn fc what n t e]

1052 <?> "type provider"

1054 <?> "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")

1054{- | Parses a transform

1061{- | Parses a transform

1055

1062

1056@

1063@

@@ -1219,56 +1226,60 @@ loadSource h lidr f

1219 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

1226 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

1220 let syntax = defaultSyntax{ syn_namespace = reverse mname }

1227 let syntax = defaultSyntax{ syn_namespace = reverse mname }

1221 ds' <- parseProg syntax f file pos

1228 ds' <- parseProg syntax f file pos

1222− unless (null ds') $ do

1229+

1230+ -- Parsing done, now process declarations

1231+

1223− let ds = namespaces mname ds'

1232+ let ds = namespaces mname ds'

1224− logLvl 3 (show $ showDecls True ds)

1233+ logLvl 3 (show $ showDecls True ds)

1225− i <- getIState

1234+ i <- getIState

1226− logLvl 10 (show (toAlist (idris_implicits i)))

1235+ logLvl 10 (show (toAlist (idris_implicits i)))

1227− logLvl 3 (show (idris_infixes i))

1236+ logLvl 3 (show (idris_infixes i))

1228− -- Now add all the declarations to the context

1237+ -- Now add all the declarations to the context

1229− v <- verbose

1238+ v <- verbose

1230− when v $ ihputStrLn h $ "Type checking " ++ f

1239+ when v $ ihputStrLn h $ "Type checking " ++ f

1231− -- we totality check after every Mutual block, so if

1240+ -- we totality check after every Mutual block, so if

1232− -- anything is a single definition, wrap it in a

1241+ -- anything is a single definition, wrap it in a

1233− -- mutual block on its own

1242+ -- mutual block on its own

1234− elabDecls toplevel (map toMutual ds)

1243+ elabDecls toplevel (map toMutual ds)

1235− i <- getIState

1244+ i <- getIState

1236− -- simplify every definition do give the totality checker

1245+ -- simplify every definition do give the totality checker

1237− -- a better chance

1246+ -- a better chance

1238− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1247+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1239− updateContext (simplifyCasedef n))

1248+ updateContext (simplifyCasedef n))

1240− (map snd (idris_totcheck i))

1249+ (map snd (idris_totcheck i))

1241− -- build size change graph from simplified definitions

1250+ -- build size change graph from simplified definitions

1242− iLOG "Totality checking"

1251+ iLOG "Totality checking"

1243− i <- getIState

1252+ i <- getIState

1244− mapM_ buildSCG (idris_totcheck i)

1253+ mapM_ buildSCG (idris_totcheck i)

1245− mapM_ checkDeclTotality (idris_totcheck i)

1254+ mapM_ checkDeclTotality (idris_totcheck i)

1246−

1255+

1247− -- Redo totality check for deferred names

1256+ -- Redo totality check for deferred names

1248− let deftots = idris_defertotcheck i

1257+ let deftots = idris_defertotcheck i

1249− iLOG $ "Totality checking " ++ show deftots

1258+ iLOG $ "Totality checking " ++ show deftots

1250− mapM_ (\x -> do tot <- getTotality x

1259+ mapM_ (\x -> do tot <- getTotality x

1251− case tot of

1260+ case tot of

1252− Total _ -> setTotality x Unchecked

1261+ Total _ -> setTotality x Unchecked

1253− _ -> return ()) (map snd deftots)

1262+ _ -> return ()) (map snd deftots)

1254− mapM_ buildSCG deftots

1263+ mapM_ buildSCG deftots

1255− mapM_ checkDeclTotality deftots

1264+ mapM_ checkDeclTotality deftots

1256−

1265+

1257− iLOG ("Finished " ++ f)

1266+ iLOG ("Finished " ++ f)

1258− ibcsd <- valIBCSubDir i

1267+ ibcsd <- valIBCSubDir i

1259− iLOG "Universe checking"

1268+ iLOG "Universe checking"

1260− iucheck

1269+ iucheck

1261− let ibc = ibcPathNoFallback ibcsd f

1270+ let ibc = ibcPathNoFallback ibcsd f

1262− i <- getIState

1271+ i <- getIState

1263− addHides (hide_list i)

1272+ addHides (hide_list i)

1273+

1274+ -- Finally, write an ibc if checking was successful

1275+

1264− ok <- noErrors

1276+ ok <- noErrors

1265− when ok $

1277+ when ok $

1266− idrisCatch (do writeIBC f ibc; clearIBC)

1278+ idrisCatch (do writeIBC f ibc; clearIBC)

1267− (\c -> return ()) -- failure is harmless

1279+ (\c -> return ()) -- failure is harmless

1268− i <- getIState

1280+ i <- getIState

1269− putIState (i { default_total = def_total,

1281+ putIState (i { default_total = def_total,

1270− hide_list = [] })

1282+ hide_list = [] })

1271− return ()

1272 return ()

1283 return ()

1273 where

1284 where

1274 namespaces :: [String] -> [PDecl] -> [PDecl]

1285 namespaces :: [String] -> [PDecl] -> [PDecl]

src/Idris/PartialEval.hs+2−2

@@ -103,7 +103,7 @@ mkPE_TermDecl ist newname sname ns

103 deImp (PApp fc t as) = PApp fc t (map deImpArg as)

104 deImp t = t

105

106− deImpArg a@(PImp _ _ _ _ _ _) = a { getTm = Placeholder }

106+ deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }

107 deImpArg a = a

108

109data PEArgType = ImplicitS | ImplicitD

@@ -124,7 +124,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

124 | imparg imp = (ImplicitD, tm)

125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

126

127− imparg (PExp _ _ _ _) = False

127+ imparg (PExp _ _ _) = False

128 imparg _ = True

129

130 buildApp env [] [] _ _ = []

src/Idris/Primitives.hs+3−1

@@ -172,7 +172,9 @@ primitives =

172 (0, LStdIn) partial,

173 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

174 (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,

176 -- Buffers

178 -- Buffers

177 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)

179 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)

178 (1, LAllocate) total,

180 (1, LAllocate) total,

src/Idris/ProofSearch.hs+1−1

@@ -109,6 +109,6 @@ proofSearch elab fn nroot hints ist

109 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

110 solve

111

112− isImp (PImp p _ _ _ _ _) = (True, p)

112+ isImp (PImp p _ _ _ _) = (True, p)

113 isImp arg = (False, priority arg)

114

src/Idris/Prover.hs+5−5

@@ -59,7 +59,7 @@ prove :: Context -> Bool -> Name -> Type -> Idris ()

59prove ctxt lit n ty

60 = do let ps = initElaborator n ctxt ty

61 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

63 iLOG $ "Adding " ++ show tm

64 iputStrLn $ showProof lit n prf

65 i <- getIState

@@ -161,8 +161,8 @@ receiveInput e =

161 Just (Interpret cmd) -> return (Just cmd)

162 Nothing -> return Nothing

163

164−ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

164+ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

165−ploop d prompt prf e h

165+ploop fn d prompt prf e h

166 = do i <- getIState

167 when d $ dumpState i (proof e)

168 (x, h') <-

@@ -260,7 +260,7 @@ ploop d prompt prf e h

260 return (False, e, False, prf))

261 (\err -> do putIState ist ; ierror err)

262 Success tac -> do (_, e) <- elabStep e saveState

263− (_, st) <- elabStep e (runTac True i tac)

263+ (_, st) <- elabStep e (runTac True i fn tac)

264-- trace (show (problems (proof st))) $

265 iPrintResult ""

266 return (True, st, False, prf ++ [step]))

@@ -269,5 +269,5 @@ ploop d prompt prf e h

269 ideslavePutSExp "write-proof-state" (prf', length prf')

270 if done then do (tm, _) <- elabStep st get_term

271 return (tm, prf')

272− else ploop d prompt prf' st h'

272+ else ploop fn d prompt prf' st h'

273 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 #-}

1+{-# LANGUAGE PatternGuards, DeriveFunctor #-}

2−module Idris.Providers (providerTy, getProvided) where

2+module Idris.Providers (providerTy, getProvided, Provided(..)) where

3

4import Idris.Core.TT

5import Idris.Core.Evaluate

@@ -11,14 +11,19 @@ import Debug.Trace

11

12-- | Wrap a type provider in the type of type providers

13providerTy :: 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]

15

16ioret = sUN "prim_io_return"

17ermod = sNS (sUN "Error") ["Providers"]

18prmod = sNS (sUN "Provide") ["Providers"]

19+posmod = sNS (sUN "Postulate") ["Providers"]

20+

21+data Provided a = Provide a

22+ | Postulate

23+ deriving (Show, Eq, Functor)

19

24

20-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

25-- | 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))

22getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

27getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

23 , (P _ nm _, [_, err]) <- unApply result

28 , (P _ nm _, [_, err]) <- unApply result

24 , pioret == ioret && nm == ermod

29 , pioret == ioret && nm == ermod

@@ -28,7 +33,11 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

28 | (P _ pioret _, [tp, result]) <- unApply tm

33 | (P _ pioret _, [tp, result]) <- unApply tm

29 , (P _ nm _, [_, res]) <- unApply result

34 , (P _ nm _, [_, res]) <- unApply result

30 , pioret == ioret && nm == prmod

35 , 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

32 | otherwise = ifail $ "Internal type provider error: result was not " ++

41 | otherwise = ifail $ "Internal type provider error: result was not " ++

33 "IO (Provider a), or perhaps missing normalisation."

42 "IO (Provider a), or perhaps missing normalisation."

34

43

src/Idris/REPL.hs+2−2

@@ -724,8 +724,8 @@ process h fn (DoProofSearch updatefile l n hints)

724 Just (t, e, False) -> (t, e, False)

725 _ -> (Nothing, 0, True)

726 let fc = fileFC fn

727− let body t = PProof [Try (TSeq Intros (ProofSearch t n hints))

727+ let body t = PProof [Try (TSeq Intros (ProofSearch t hints))

728− (ProofSearch t n hints)]

728+ (ProofSearch t hints)]

729 let def = PClause fc mn (PRef fc mn) [] (body top) []

730 newmv <- idrisCatch

731 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

src/Pkg/Package.hs+6−6

@@ -57,12 +57,12 @@ buildPkg warnonly (install, fp)

57 _ -> return ()

58 -- Also give up if there are metavariables to solve

59 case (map fst (idris_metavars ist) \\ primDefs) of

60− [] -> when install $ installPkg pkgdesc

60+ _ -> when install $ installPkg pkgdesc

61− ms -> do if install

61+-- ms -> do if install

62− then putStrLn "Can't install: there are undefined metavariables:"

62+-- then putStrLn "Can't install: there are undefined metavariables:"

63− else putStrLn "There are undefined metavariables:"

63+-- else putStrLn "There are undefined metavariables:"

64− putStrLn $ "\t" ++ show ms

64+-- putStrLn $ "\t" ++ show ms

65− exitWith (ExitFailure 1)

65+-- exitWith (ExitFailure 1)

66

67-- | Type check packages only

68--

test/Makefile+1−1

@@ -11,7 +11,7 @@ test_java:

11 perl ./runtest.pl without buffer001 --codegen Java

12

13test_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

15

16test_llvm:

17 @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