991ee91 · Idris-dev · git.iko.soy

.gitignore+5−1

compare with master

unifiedsplit

@@ -1,2 +1,6 @@

1dist

2−*.ibc

2+*.ibc

3+*.o

4+*.a

5+test/output

6+test/test???/output

contribs/lib/SQLite3/sqlexpr.idr+2−2

@@ -1,5 +1,5 @@

1−module sqlexpr

1+module Sqlexpr

2−import prelude.list

2+import Prelude.List

3

4-----------------------------------------------------------------------------

5-- |

contribs/lib/SQLite3/sqlite3.idr+2−2

@@ -1,5 +1,5 @@

1−module sqlite3

1+module Sqlite3

2−import sqlexpr

2+import Sqlexpr

3

4

5%lib "sqlite3"

contribs/lib/SQLite3/testunit.idr+2−2

@@ -1,5 +1,5 @@

1−module main

1+module Main

2−import sqlite3

2+import Sqlite3

3

4

5testexpr : DB()

idris.cabal+2−2

@@ -45,8 +45,8 @@ Build-type: Custom

45Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h

46 rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h

47 rts/libtest.c

48−Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr

48+Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr lib/Network/*.idr

49− lib/control/monad/*.idr lib/language/*.idr

49+ lib/Control/Monad/*.idr lib/Language/*.idr

50 tutorial/examples/*.idr lib/base.ipkg

51 rts/*.c rts/*.h rts/Makefile

52

lib/builtins.idr → lib/Builtins.idrrenamed+1−1

@@ -30,7 +30,7 @@ trace_malloc x = x -- compiled specially

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

31believe_me x = prim__believe_me _ _ x

32

33−namespace builtins {

33+namespace Builtins {

34

35id : a -> a

36id x = x

lib/Checkall.idrnew file+31

@@ -0,0 +1,31 @@

1+module Checkall

2+

3+-- This file just exists to typecheck all the prelude modules

4+-- Add imports here

5+

6+import Builtins

7+import Prelude

8+import IO

9+import System

10+

11+import Prelude.Algebra

12+import Prelude.Cast

13+import Prelude.Nat

14+import Prelude.Fin

15+import Prelude.List

16+import Prelude.Maybe

17+import Prelude.Monad

18+import Prelude.Applicative

19+import Prelude.Either

20+import Prelude.Vect

21+import Prelude.Strings

22+import Prelude.Chars

23+import Prelude.Heap

24+import Prelude.Complex

25+

26+import Network.Cgi

27+

28+import Language.Reflection

29+

30+import Control.Monad.Identity

31+import Control.Monad.State

lib/control/arrow.idr → lib/Control/Arrow.idrrenamed+3−3

@@ -1,7 +1,7 @@

1−module category.arrow

1+module Category.Arrow

2

3−import prelude.morphisms

3+import Prelude.Morphisms

4−import control.category

4+import Control.Category

5

6infixr 3 ***

7infixr 3 &&&

lib/control/category.idr → lib/Control/Category.idrrenamed+4−4

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

1−module control.category

1+module Control.Category

2

3−import prelude.morphisms

3+import Prelude.Morphisms

4

5class Category (cat : Set -> Set -> Set) where

6 id : cat a a

7 (.) : cat b c -> cat a b -> cat a c

8

9instance Category Morphism where

10− id = Homo builtins.id

10+ id = Homo Builtins.id

11− (Homo f) . (Homo g) = Homo $ builtins.(.) f g

11+ (Homo f) . (Homo g) = Homo $ Builtins.(.) f g

12

13infixr 1 >>>

14(>>>) : Category cat => cat a b -> cat b c -> cat a c

lib/control/monad/identity.idr → lib/Control/Monad/Identity.idrrenamed+2−2

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

1−module control.monad.identity

1+module Control.Monad.Identity

2

3−import prelude.monad

3+import Prelude.Monad

4

5public record Identity : Set -> Set where

6 Id : (runIdentity : a) -> Identity a

lib/control/monad/state.idr → lib/Control/Monad/State.idrrenamed+3−3

@@ -1,7 +1,7 @@

1−module control.monad.state

1+module Control.Monad.State

2

3−import control.monad.identity

3+import Control.Monad.Identity

4−import prelude.monad

4+import Prelude.Monad

5

6%access public

7

lib/io.idr → lib/IO.idrrenamed+1−1

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

1−import prelude.list

1+import Prelude.List

2

3%access public

4

lib/language/reflection.idr → lib/Language/Reflection.idrrenamed+1−1

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

1−module language.reflection

1+module Language.Reflection

2

3TTName : Set

4TTName = String

lib/Makefile+1−1

@@ -11,6 +11,6 @@ clean: .PHONY

11 $(IDRIS) --clean base.ipkg

12

13linecount: .PHONY

14− wc -l *.idr network/*.idr language/*.idr prelude/*.idr control/monad/*.idr

14+ wc -l *.idr Network/*.idr Language/*.idr Prelude/*.idr Control/Monad/*.idr

15

16.PHONY:

lib/network/cgi.idr → lib/Network/Cgi.idrrenamed+2−2

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

1−module network.cgi

1+module Network.Cgi

2

3−import system

3+import System

4

5public

6Vars : Set

lib/prelude.idr → lib/Prelude.idrrenamed+16−16

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

1−module prelude

1+module Prelude

2−

2+

3−import builtins

3+import Builtins

4−import io

4+import IO

5−

5+

6−import prelude.cast

6+import Prelude.Cast

7−import prelude.nat

7+import Prelude.Nat

8−import prelude.fin

8+import Prelude.Fin

9−import prelude.list

9+import Prelude.List

10−import prelude.maybe

10+import Prelude.Maybe

11−import prelude.monad

11+import Prelude.Monad

12−import prelude.applicative

12+import Prelude.Applicative

13−import prelude.either

13+import Prelude.Either

14−import prelude.vect

14+import Prelude.Vect

15−import prelude.strings

15+import Prelude.Strings

16−import prelude.char

16+import Prelude.Chars

17

18%access public

19

lib/prelude/algebra.idr → lib/Prelude/Algebra.idrrenamed+2−2

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

1−module prelude.algebra

1+module Prelude.Algebra

2

3−import builtins

3+import Builtins

4

5-- XXX: change?

6infixl 6 <->

lib/prelude/applicative.idr → lib/Prelude/Applicative.idrrenamed+2−2

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

1−module prelude.applicative

1+module Prelude.Applicative

2

3−import builtins

3+import Builtins

4

5---- Applicative functors/Idioms

6

lib/prelude/cast.idr → lib/Prelude/Cast.idrrenamed+1−1

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

1−module prelude.cast

1+module Prelude.Cast

2

3class Cast from to where

4 cast : from -> to

lib/prelude/char.idr → lib/Prelude/Chars.idrrenamed+2−2

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

1−module prelude.char

1+module Prelude.Char

2

3−import builtins

3+import Builtins

4

5isUpper : Char -> Bool

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

lib/prelude/complex.idr → lib/Prelude/Complex.idrrenamed+3−3

@@ -3,10 +3,10 @@

3-}

4

5

6−module prelude.complex

6+module Prelude.Complex

7

8−import builtins

8+import Builtins

9−import prelude

9+import Prelude

10

11------------------------------ Rectangular form

12

lib/prelude/either.idr → lib/Prelude/Either.idrrenamed+4−4

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

1−module prelude.either

1+module Prelude.Either

2

3−import builtins

3+import Builtins

4

5−import prelude.maybe

5+import Prelude.Maybe

6−import prelude.list

6+import Prelude.List

7

8data Either a b

9 = Left a

lib/prelude/fin.idr → lib/Prelude/Fin.idrrenamed+2−2

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

1−module prelude.fin

1+module Prelude.Fin

2

3−import prelude.nat

3+import Prelude.Nat

4

5data Fin : Nat -> Set where

6 fO : Fin (S k)

lib/prelude/heap.idr → lib/Prelude/Heap.idrrenamed+7−7

@@ -3,14 +3,14 @@

3-- ``Fun with binary heap trees'', Chris Okasaki, Fun of programming, 2003.

4--------------------------------------------------------------------------------

5

6−module prelude.heap

6+module Prelude.Heap

7

8−import builtins

8+import Builtins

9

10−import prelude

10+import Prelude

11−import prelude.algebra

11+import Prelude.Algebra

12−import prelude.list

12+import Prelude.List

13−import prelude.nat

13+import Prelude.Nat

14

15%access public

16

@@ -110,7 +110,7 @@ fromList : Ord a => List a -> MaxiphobicHeap a

110fromList = foldr insert empty

111

112sort : Ord a => List a -> List a

113−sort = prelude.heap.toList . prelude.heap.fromList

113+sort = Prelude.Heap.toList . Prelude.Heap.fromList

114

115--------------------------------------------------------------------------------

116-- Class instances

lib/prelude/list.idr → lib/Prelude/List.idrrenamed+5−5

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

1−module prelude.list

1+module Prelude.List

2

3−import builtins

3+import Builtins

4

5−import prelude.algebra

5+import Prelude.Algebra

6−import prelude.maybe

6+import Prelude.Maybe

7−import prelude.nat

7+import Prelude.Nat

8

9%access public

10

lib/prelude/maybe.idr → lib/Prelude/Maybe.idrrenamed+2−2

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

1−module prelude.maybe

1+module Prelude.Maybe

2

3−import builtins

3+import Builtins

4

5data Maybe a

6 = Nothing

lib/prelude/monad.idr → lib/Prelude/Monad.idrrenamed+2−2

@@ -2,8 +2,8 @@ module prelude.monad

2

3-- Monads and Functors

4

5−import builtins

5+import Builtins

6−import prelude.list

6+import Prelude.List

7

8%access public

9

lib/prelude/morphisms.idr → lib/Prelude/Morphisms.idrrenamed+1−1

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

1−module prelude.morphisms

1+module Prelude.Morphisms

2

3data Morphism : Set -> Set -> Set where

4 Homo : (a -> b) -> Morphism a b

lib/prelude/nat.idr → lib/Prelude/Nat.idrrenamed+4−4

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

1−module prelude.nat

1+module Prelude.Nat

2

3−import builtins

3+import Builtins

4

5−import prelude.algebra

5+import Prelude.Algebra

6−import prelude.cast

6+import Prelude.Cast

7

8%access public

9

lib/prelude/strings.idr → lib/Prelude/Strings.idrrenamed+5−5

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

1−module prelude.strings

1+module Prelude.Strings

2

3−import builtins

3+import Builtins

4−import prelude.list

4+import Prelude.List

5−import prelude.char

5+import Prelude.Chars

6−import prelude.cast

6+import Prelude.Cast

7

8-- Some more complex string operations

9

lib/prelude/vect.idr → lib/Prelude/Vect.idrrenamed+6−6

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

1−module prelude.vect

1+module Prelude.Vect

2

3−import prelude.fin

3+import Prelude.Fin

4−import prelude.list

4+import Prelude.List

5−import prelude.nat

5+import Prelude.Nat

6

7%access public

8

@@ -292,13 +292,13 @@ catMaybes ((Just j)::xs) with (catMaybes xs)

292-- Proofs

293--------------------------------------------------------------------------------

294

295−prelude.vect.reverse'_lemma_2 = proof {

295+Prelude.Vect.reverse'_lemma_2 = proof {

296 intros;

297 rewrite (plusSuccRightSucc m n1);

298 exact value;

299}

300

301−prelude.vect.reverse'_lemma_1 = proof {

301+Prelude.Vect.reverse'_lemma_1 = proof {

302 intros;

303 rewrite sym (plusZeroRightNeutral m);

304 exact value;

lib/system.idr → lib/System.idrrenamed+2−2

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

1−module system

1+module System

2

3−import prelude

3+import Prelude

4

5%access public

6

lib/base.ipkg+9−9

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

1package base

2

3opts = "--noprelude"

4−modules = builtins, prelude, io, system,

4+modules = Builtins, Prelude, IO, System,

5

6− prelude.algebra, prelude.cast, prelude.nat, prelude.fin,

6+ Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,

7− prelude.list, prelude.maybe, prelude.monad, prelude.applicative,

7+ Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,

8− prelude.either, prelude.vect, prelude.strings, prelude.char,

8+ Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Heap,

9− prelude.heap, prelude.complex, prelude.morphisms,

9+ Prelude.Complex, Prelude.Morphisms,

10

11− network.cgi,

11+ Network.Cgi,

12

13− language.reflection,

13+ Language.Reflection,

14

15− control.monad.identity, control.monad.state, control.category,

15+ Control.Monad.Identity, Control.Monad.State, Control.Category,

16− control.arrow

16+ Control.Arrow

lib/checkall.idrdeleted−31

@@ -1,31 +0,0 @@

1−module checkall

2−

3−-- This file just exists to typecheck all the prelude modules

4−-- Add imports here

5−

6−import builtins

7−import prelude

8−import io

9−import system

10−

11−import prelude.algebra

12−import prelude.cast

13−import prelude.nat

14−import prelude.fin

15−import prelude.list

16−import prelude.maybe

17−import prelude.monad

18−import prelude.applicative

19−import prelude.either

20−import prelude.vect

21−import prelude.strings

22−import prelude.char

23−import prelude.heap

24−import prelude.complex

25−

26−import network.cgi

27−

28−import language.reflection

29−

30−import control.monad.identity

31−import control.monad.state

src/Idris/REPL.hs+5−5

@@ -162,7 +162,7 @@ process fn (Eval t)

162 showImp imp (delab ist ty'))

163process fn (ExecVal t)

164 = do (tm, ty) <- elabVal toplevel False t

165−-- (PApp fc (PRef fc (NS (UN "print") ["prelude"]))

165+-- (PApp fc (PRef fc (NS (UN "print") ["Prelude"]))

166-- [pexp t])

167 (tmpn, tmph) <- liftIO tempfile

168 liftIO $ hClose tmph

@@ -307,7 +307,7 @@ process fn TTShell = do ist <- get

307process fn Execute = do (m, _) <- elabVal toplevel False

308 (PApp fc

309 (PRef fc (UN "run__IO"))

310− [pexp $ PRef fc (NS (UN "main") ["main"])])

310+ [pexp $ PRef fc (NS (UN "main") ["Main"])])

311-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

312 (tmpn, tmph) <- liftIO tempfile

313 liftIO $ hClose tmph

@@ -318,13 +318,13 @@ process fn Execute = do (m, _) <- elabVal toplevel False

318process fn (NewCompile f)

319 = do (m, _) <- elabVal toplevel False

320 (PApp fc (PRef fc (UN "run__IO"))

321− [pexp $ PRef fc (NS (UN "main") ["main"])])

321+ [pexp $ PRef fc (NS (UN "main") ["Main"])])

322 compileEpic f m

323 where fc = FC "main" 0

324process fn (Compile target f)

325 = do (m, _) <- elabVal toplevel False

326 (PApp fc (PRef fc (UN "run__IO"))

327− [pexp $ PRef fc (NS (UN "main") ["main"])])

327+ [pexp $ PRef fc (NS (UN "main") ["Main"])])

328 compile target f m

329 where fc = FC "main" 0

330process fn (LogLvl i) = setLogLevel i

@@ -485,7 +485,7 @@ idrisMain opts =

485 addPkgDir "base"

486 mapM_ addPkgDir pkgdirs

487 elabPrims

488− when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

488+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

489 return ()

490 when runrepl $ iputStrLn banner

491 ist <- get

src/Idris/Transforms.hs+2−2

@@ -39,8 +39,8 @@ instance Transform CaseAlt where

39

40natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]

41

42−zname = NS (UN "O") ["nat","prelude"]

42+zname = NS (UN "O") ["Nat","Prelude"]

43−sname = NS (UN "S") ["nat","prelude"]

43+sname = NS (UN "S") ["Nat","Prelude"]

44

45zero :: TT Name -> TT Name

46zero (P _ n _) | n == zname

test/reg002/reg002.idr+2−2

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

1−module main

1+module Main

2

3%default total

4

@@ -10,7 +10,7 @@ S : CoNat -> CoNat

10S (Co n) = Co (S n)

11S Infinity = Infinity

12

13−Sn_notzero : main.S n = Co 0 -> _|_

13+Sn_notzero : Main.S n = Co 0 -> _|_

14Sn_notzero = believe_me

15

16S_Co_not_Inf : S (Co n) = Infinity -> _|_

test/test001/test001.idr+1−1

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

1−module main

1+module Main

2

3data Ty = TyInt | TyBool| TyFun Ty Ty

4

test/test003/lit.lidr → test/test003/Lit.lidrrenamed+1−1

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

1−> module lit

1+> module Lit

2

3Test some string primitives while we're at it

4

test/test003/run+1−1

@@ -2,4 +2,4 @@

2idris test003a.lidr --check

3idris test003.lidr -o test003

4./test003

5−rm -f test003 test003.ibc lit.ibc

5+rm -f test003 test003.ibc Lit.ibc

test/test003/test003.lidr+3−3

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

1−> module main

1+> module Main

2

3Import the literate module

4

5−> import lit

5+> import Lit

6

7> main : IO ()

8−> main = lit.main

8+> main = Lit.main

test/test004/test004.idr+1−1

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

1−module main

1+module Main

2

3dumpFile : String -> IO ()

4dumpFile fn = do { h <- openFile fn Read

test/test005/test005.idr+1−1

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

1−module main

1+module Main

2

3tstr : String

4tstr = "abc123"

test/test006/test006.idr+3−3

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

1−module main

1+module Main

2

3data Parity : Nat -> Set where

4 even : Parity (n + n)

@@ -22,14 +22,14 @@ main = do print (natToBin 42)

22

23---------- Proofs ----------

24

25−main.parity_lemma_2 = proof {

25+Main.parity_lemma_2 = proof {

26 intro;

27 intro;

28 rewrite sym (plusSuccRightSucc j j);

29 trivial;

30};

31

32−main.parity_lemma_1 = proof {

32+Main.parity_lemma_1 = proof {

33 intro j;

34 intro;

35 rewrite sym (plusSuccRightSucc j j);

test/test007/test007.idr+1−1

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

1−module main

1+module Main

2

3data Expr = Var String

4 | Val Int

test/test008/test008.idr+1−1

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

1−module main

1+module Main

2

3testlist : List (String, Int)

4testlist = [("foo", 1), ("bar", 2)]

test/test009/test009.idr+1−1

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

1−module main

1+module Main

2

3pythag : Int -> List (Int, Int, Int)

4pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],

test/test011/test011.idr+1−1

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

1−module main

1+module Main

2

3record Foo : Nat -> Set where

4 MkFoo : (name : String) ->

test/test012/test012a.idr+1−1

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

1−module main

1+module Main

2

3f : Nat -> Nat

4f x = x + 1

test/test013/test013.idr+1−1

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

1−module main

1+module Main

2

3forLoop : List a -> (a -> IO ()) -> IO ()

4forLoop [] f = return ()

test/test014/resimp.idr → test/test014/Resimp.idrrenamed+1−1

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

1−module resimp

1+module Resimp

2

3-- IO operations which read a resource

4data Reader : Set -> Set where

test/test014/test014.idr+2−2

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

1−module main

1+module Main

2

3−import resimp

3+import Resimp

4

5data Purpose = Reading | Writing

6

test/test015/parity.idr → test/test015/Parity.idrrenamed+1−1

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

1−module parity

1+module Parity

2

3data Parity : Nat -> Set where

4 even : Parity (n + n)

test/test015/test015.idr+7−7

@@ -1,7 +1,7 @@

1−module main

1+module Main

2

3−import parity

3+import Parity

4−import system

4+import System

5

6data Bit : Nat -> Set where

7 b0 : Bit O

@@ -87,7 +87,7 @@ main = do let Just bin1 = natToBin 8 42

87

88---------- Proofs ----------

89

90−main.ntbOdd = proof {

90+Main.ntbOdd = proof {

91 intro w,j;

92 rewrite sym (plusZeroRightNeutral j);

93 rewrite plusSuccRightSucc j j;

@@ -96,7 +96,7 @@ main.ntbOdd = proof {

96 trivial;

97}

98

99−main.ntbEven = proof {

99+Main.ntbEven = proof {

100 compute;

101 intro w,j;

102 rewrite sym (plusZeroRightNeutral j);

@@ -107,7 +107,7 @@ main.ntbEven = proof {

107

108-- There is almost certainly an easier proof. I don't care, for now :)

109

110−main.adc_lemma_2 = proof {

110+Main.adc_lemma_2 = proof {

111 intro c,w,v,bit0,num0;

112 intro b0,v1,bit1,num1,b1;

113 intro bc,x,x1,bx,bx1;

@@ -137,7 +137,7 @@ main.adc_lemma_2 = proof {

137 trivial;

138}

139

140−main.adc_lemma_1 = proof {

140+Main.adc_lemma_1 = proof {

141 intros;

142 rewrite sym (plusZeroRightNeutral c) ;

143 trivial;