3b37daf · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

271 test/basic009/*.idr

272 test/basic009/expected

273 test/basic009/B/*.idr

274+ test/basic010/run

275+ test/basic010/*.idr

276+ test/basic010/expected

274

277

275 test/buffer001-disabled/*.idr

278 test/buffer001-disabled/*.idr

276 test/buffer001-disabled/run

279 test/buffer001-disabled/run

libs/prelude/Builtins.idr+3−11

@@ -6,16 +6,8 @@

6||| Dependent pairs, in their internal representation

7||| @ a the type of the witness

8||| @ P the type of the proof

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

9+data Sigma : (a : Type) -> (P : a -> Type) -> Type where

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

10+ Sg_intro : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P

11−

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

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

14−getWitness (a ** v) = a

15−

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

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

18−getProof (a ** v) = v

19

11

20||| The eliminator for the empty type.

12||| The eliminator for the empty type.

21FalseElim : _|_ -> a

13FalseElim : _|_ -> a

@@ -47,7 +39,7 @@ data LazyType = LazyCodata | LazyEval

47data Lazy' : LazyType -> Type -> Type where

39data Lazy' : LazyType -> Type -> Type where

48 ||| A delayed computation.

40 ||| A delayed computation.

49 |||

41 |||

50− |||Delay is inserted automatically by the elaborator where necessary.

42+ ||| Delay is inserted automatically by the elaborator where necessary.

51 |||

43 |||

52 ||| Note that compiled code gives `Delay` special semantics.

44 ||| Note that compiled code gives `Delay` special semantics.

53 ||| @ t whether this is laziness from codata or normal lazy evaluation

45 ||| @ t whether this is laziness from codata or normal lazy evaluation

libs/prelude/Prelude.idr+1

@@ -21,6 +21,7 @@ import Prelude.Traversable

21import Prelude.Bits

22import Prelude.Stream

23import Prelude.Uninhabited

24+import Prelude.Pairs

24

25

25import Decidable.Equality

26import Decidable.Equality

26

27

libs/prelude/Prelude/Pairs.idrnew file+42

@@ -0,0 +1,42 @@

1+module Prelude.Pairs

2+

3+import Builtins

4+

5+%access public

6+%default total

7+

8+using (a : Type, P : a -> Type)

9+

10+ ||| Dependent pair where the first field is erased.

11+ data Exists : (P : a -> Type) -> Type where

12+ evidence : .(x : a) -> (pf : P x) -> Exists P

13+

14+ ||| Dependent pair where the second field is erased.

15+ data Subset : (a : Type) -> (P : a -> Type) -> Type where

16+ element : (x : a) -> .(pf : P x) -> Subset a P

17+

18+ -- Monomorphic projections

19+

20+ namespace Exists

21+ getWitness : Exists {a} P -> a

22+ getWitness (evidence x pf) = x

23+

24+ getProof : (x : Exists {a} P) -> P (getWitness x)

25+ getProof (evidence x pf) = pf

26+

27+ namespace Subset

28+ getWitness : Subset a P -> a

29+ getWitness (element x pf) = x

30+

31+ getProof : (x : Subset a P) -> P (getWitness x)

32+ getProof (element x pf) = pf

33+

34+ namespace Sigma

35+ getWitness : Sigma a P -> a

36+ getWitness (x ** pf) = x

37+

38+ getProof : (x : Sigma a P) -> P (getWitness x)

39+ getProof (x ** pf) = pf

40+

41+ -- Polymorphic (class-based) projections have been removed

42+ -- because type-directed name disambiguation works better.

libs/prelude/prelude.ipkg+1−1

@@ -8,7 +8,7 @@ modules = Builtins, Prelude, IO,

8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

9 Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11− Prelude.Uninhabited,

11+ Prelude.Uninhabited, Prelude.Pairs,

12

13 Decidable.Equality

14

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1100,8 +1100,8 @@ elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defau

1100 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1101

1102-- Defined in builtins.idr

1103−sigmaTy = sUN "Exists"

1103+sigmaTy = sUN "Sigma"

1104−existsCon = sUN "Ex_intro"

1104+existsCon = sUN "Sg_intro"

1105

1106piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1107piBind = piBindp expl

src/Idris/Delaborate.hs+2−2

@@ -92,13 +92,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

92 | n == eqCon = PRefl un (de env [] r)

93 | n == sUN "lazy" = de env [] r

94 deFn env (P _ n _) [ty, Bind x (Lam _) r]

95− | n == sUN "Exists"

95+ | n == sUN "Sigma"

96 = PDPair un IsType (PRef un x) (de env [] ty)

97 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

98 deFn env (P _ n _) [_,_,l,r]

99 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

100 | n == eqTy = PEq un (de env [] l) (de env [] r)

101− | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder

101+ | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

102 (de env [] r)

103 deFn env f@(P _ n _) args

104 | n `elem` map snd env

test/basic010/Main.idrnew file+43

@@ -0,0 +1,43 @@

1+module Main

2+

3+%default total

4+

5+-- An expensive function.

6+qib : Nat -> Nat

7+qib Z = 1

8+qib (S Z) = 2

9+qib (S (S n)) = qib n * qib (S n)

10+

11+-- An equality whose size reflects the size of numbers.

12+data equals : Nat -> Nat -> Type where

13+ eqZ : Z `equals` Z

14+ eqS : m `equals` n -> S m `equals` S n

15+

16+eq_refl : {n : Nat} -> n `equals` n

17+eq_refl {n = Z} = eqZ

18+eq_refl {n = S n} = eqS eq_refl

19+

20+-- Here, the proof is very expensive to compute.

21+-- We add a recursive argument to prevent Idris from inlining the function.

22+f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)

23+f Z n = element n eq_refl

24+f (S r) n = f r n

25+

26+-- A (contrived) relation, just to have something to show.

27+data represents : Nat -> Nat -> Type where

28+ axiom : (n : Nat) -> qib n `represents` n

29+

30+-- Here, the witness is very expensive to compute.

31+-- We add a recursive argument to prevent Idris from inlining the function.

32+g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)

33+g Z n = evidence (qib n) (axiom n)

34+g (S r) n = g r n

35+

36+fmt : qib n `represents` n -> String

37+fmt (axiom n) = "axiom " ++ show n

38+

39+main : IO ()

40+main = do

41+ n <- map (const 10000) (putStrLn "*oink*")

42+ putStrLn . show $ getWitness (f 4 n)

43+ putStrLn . fmt $ getProof (g 4 n)

test/basic010/expectednew file+3

@@ -0,0 +1,3 @@

1+*oink*

2+10000

3+axiom 10000

test/basic010/runnew file+35

@@ -0,0 +1,35 @@

1+#!/usr/bin/env bash

2+

3+# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

4+# Here copied from reg039.

5+#

6+# Executes command with a timeout

7+# Params:

8+# $1 timeout in seconds

9+# $2 command

10+# Returns 1 if timed out 0 otherwise

11+timeout() {

12+

13+ time=$1

14+

15+ # start the command in a subshell to avoid problem with pipes

16+ # (spawn accepts one command)

17+ command="/bin/sh -c \"$2\""

18+

19+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

20+

21+ if [ $? = 1 ] ; then

22+ echo "Timeout after ${time} seconds"

23+ fi

24+

25+}

26+

27+declare -a extraargs

28+for arg in "$@"

29+do

30+ extraargs=("${extraargs[@]}" "'$arg'")

31+done

32+

33+timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"

34+timeout 5 "./basic010"

35+rm -f *.ibc basic010

test/reg030/reg030.idr+1−1

@@ -8,7 +8,7 @@ isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)

8

9class Set univ => HasPower univ where

10 Powerset : (a : univ) ->

11− Exists univ (\Pa => (c : univ) ->

11+ Sigma univ (\Pa => (c : univ) ->

12 (isSubsetOf c a) -> member c Pa)

13

14powerset : HasPower univ => univ -> univ