5c9a88a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

uppercase modulenames

commit5c9a88a7aca9f79a34f980c210f8cb3e78952c8c authorraichoo <raichoo@googlemail.com> dateMon 22 Oct 2012, 21:37 (14 years ago) parent0fd9a47

54 files changed+174−170

compare with master

unifiedsplit

.gitignore+5−1

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

11dist

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

2−import prelude.list

1+module Sqlexpr

2+import Prelude.List

44-----------------------------------------------------------------------------

55-- |

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

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

1−module sqlite3

2−import sqlexpr

1+module Sqlite3

2+import Sqlexpr

55%lib "sqlite3"

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

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

1−module main

2−import sqlite3

1+module Main

2+import Sqlite3

55testexpr : DB()

idris.cabal+2−2

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

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

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

4545 rts/libtest.c

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

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

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

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

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

4949 rts/*.c rts/*.h rts/Makefile

5050

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

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

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

3131believe_me x = prim__believe_me _ _ x

3232

33−namespace builtins {

33+namespace Builtins {

3434

3535id : a -> a

3636id x = x

lib/Checkall.idrnew file+31

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

1+module Checkall

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

4+-- Add imports here

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

3−import prelude.morphisms

4−import control.category

3+import Prelude.Morphisms

4+import Control.Category

66infixr 3 ***

77infixr 3 &&&

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

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

1−module control.category

1+module Control.Category

3−import prelude.morphisms

3+import Prelude.Morphisms

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

66 id : cat a a

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

99instance Category Morphism where

10− id = Homo builtins.id

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

10+ id = Homo Builtins.id

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

1212

1313infixr 1 >>>

1414(>>>) : 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

3−import prelude.monad

3+import Prelude.Monad

55public record Identity : Set -> Set where

66 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

3−import control.monad.identity

4−import prelude.monad

3+import Control.Monad.Identity

4+import Prelude.Monad

66%access public

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

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

1−import prelude.list

1+import Prelude.List

33%access public

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

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

1−module language.reflection

1+module Language.Reflection

33TTName : Set

44TTName = String

lib/Makefile+1−1

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

1111 $(IDRIS) --clean base.ipkg

1212

1313linecount: .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

1515

1616.PHONY:

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

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

1−module network.cgi

1+module Network.Cgi

3−import system

3+import System

55public

66Vars : Set

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

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

1−module prelude

2−

3−import builtins

4−import io

5−

6−import prelude.cast

7−import prelude.nat

8−import prelude.fin

9−import prelude.list

10−import prelude.maybe

11−import prelude.monad

12−import prelude.applicative

13−import prelude.either

14−import prelude.vect

15−import prelude.strings

16−import prelude.char

1+module Prelude

3+import Builtins

4+import IO

6+import Prelude.Cast

7+import Prelude.Nat

8+import Prelude.Fin

9+import Prelude.List

10+import Prelude.Maybe

11+import Prelude.Monad

12+import Prelude.Applicative

13+import Prelude.Either

14+import Prelude.Vect

15+import Prelude.Strings

16+import Prelude.Chars

1717

1818%access public

1919

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

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

1−module prelude.algebra

1+module Prelude.Algebra

3−import builtins

3+import Builtins

55-- XXX: change?

66infixl 6 <->

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

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

1−module prelude.applicative

1+module Prelude.Applicative

3−import builtins

3+import Builtins

55---- Applicative functors/Idioms

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

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

1−module prelude.cast

1+module Prelude.Cast

33class Cast from to where

44 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

3−import builtins

3+import Builtins

55isUpper : Char -> Bool

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

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

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

33-}

6−module prelude.complex

6+module Prelude.Complex

8−import builtins

9−import prelude

8+import Builtins

9+import Prelude

1010

1111------------------------------ Rectangular form

1212

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

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

1−module prelude.either

1+module Prelude.Either

3−import builtins

3+import Builtins

5−import prelude.maybe

6−import prelude.list

5+import Prelude.Maybe

6+import Prelude.List

88data Either a b

99 = Left a

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

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

1−module prelude.fin

1+module Prelude.Fin

3−import prelude.nat

3+import Prelude.Nat

55data Fin : Nat -> Set where

66 fO : Fin (S k)

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

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

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

44--------------------------------------------------------------------------------

6−module prelude.heap

6+module Prelude.Heap

8−import builtins

8+import Builtins

10−import prelude

11−import prelude.algebra

12−import prelude.list

13−import prelude.nat

10+import Prelude

11+import Prelude.Algebra

12+import Prelude.List

13+import Prelude.Nat

1414

1515%access public

1616

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

110110fromList = foldr insert empty

111111

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

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

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

114114

115115--------------------------------------------------------------------------------

116116-- Class instances

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

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

1−module prelude.list

1+module Prelude.List

3−import builtins

3+import Builtins

5−import prelude.algebra

6−import prelude.maybe

7−import prelude.nat

5+import Prelude.Algebra

6+import Prelude.Maybe

7+import Prelude.Nat

99%access public

1010

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

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

1−module prelude.maybe

1+module Prelude.Maybe

3−import builtins

3+import Builtins

55data Maybe a

66 = Nothing

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

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

33-- Monads and Functors

5−import builtins

6−import prelude.list

5+import Builtins

6+import Prelude.List

88%access public

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

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

1−module prelude.morphisms

1+module Prelude.Morphisms

33data Morphism : Set -> Set -> Set where

44 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

3−import builtins

3+import Builtins

5−import prelude.algebra

6−import prelude.cast

5+import Prelude.Algebra

6+import Prelude.Cast

88%access public

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

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

1−module prelude.strings

1+module Prelude.Strings

3−import builtins

4−import prelude.list

5−import prelude.char

6−import prelude.cast

3+import Builtins

4+import Prelude.List

5+import Prelude.Chars

6+import Prelude.Cast

88-- Some more complex string operations

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

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

1−module prelude.vect

1+module Prelude.Vect

3−import prelude.fin

4−import prelude.list

5−import prelude.nat

3+import Prelude.Fin

4+import Prelude.List

5+import Prelude.Nat

77%access public

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

292292-- Proofs

293293--------------------------------------------------------------------------------

294294

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

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

296296 intros;

297297 rewrite (plusSuccRightSucc m n1);

298298 exact value;

299299}

300300

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

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

302302 intros;

303303 rewrite sym (plusZeroRightNeutral m);

304304 exact value;

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

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

1−module system

1+module System

3−import prelude

3+import Prelude

55%access public

lib/base.ipkg+9−9

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

11package base

33opts = "--noprelude"

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

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

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

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

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

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

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

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

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

9+ Prelude.Complex, Prelude.Morphisms,

1010

11− network.cgi,

11+ Network.Cgi,

1212

13− language.reflection,

13+ Language.Reflection,

1414

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

16− control.arrow

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

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)

162162 showImp imp (delab ist ty'))

163163process fn (ExecVal t)

164164 = 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"]))

166166-- [pexp t])

167167 (tmpn, tmph) <- liftIO tempfile

168168 liftIO $ hClose tmph

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

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

308308 (PApp fc

309309 (PRef fc (UN "run__IO"))

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

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

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

312312 (tmpn, tmph) <- liftIO tempfile

313313 liftIO $ hClose tmph

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

318318process fn (NewCompile f)

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

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

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

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

322322 compileEpic f m

323323 where fc = FC "main" 0

324324process fn (Compile target f)

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

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

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

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

328328 compile target f m

329329 where fc = FC "main" 0

330330process fn (LogLvl i) = setLogLevel i

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

485485 addPkgDir "base"

486486 mapM_ addPkgDir pkgdirs

487487 elabPrims

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

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

489489 return ()

490490 when runrepl $ iputStrLn banner

491491 ist <- get

src/Idris/Transforms.hs+2−2

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

3939

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

4141

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

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

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

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

4444

4545zero :: TT Name -> TT Name

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

test/reg002/reg002.idr+2−2

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

1−module main

1+module Main

33%default total

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

1010S (Co n) = Co (S n)

1111S Infinity = Infinity

1212

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

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

1414Sn_notzero = believe_me

1515

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

test/test001/test001.idr+1−1

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

1−module main

1+module Main

33data Ty = TyInt | TyBool| TyFun Ty Ty

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

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

1−> module lit

1+> module Lit

33Test some string primitives while we're at it

test/test003/run+1−1

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

22idris test003a.lidr --check

33idris test003.lidr -o test003

44./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

33Import the literate module

5−> import lit

5+> import Lit

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

33dumpFile : String -> IO ()

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

test/test005/test005.idr+1−1

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

1−module main

1+module Main

33tstr : String

44tstr = "abc123"

test/test006/test006.idr+3−3

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

1−module main

1+module Main

33data Parity : Nat -> Set where

44 even : Parity (n + n)

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

2222

2323---------- Proofs ----------

2424

25−main.parity_lemma_2 = proof {

25+Main.parity_lemma_2 = proof {

2626 intro;

2727 intro;

2828 rewrite sym (plusSuccRightSucc j j);

2929 trivial;

3030};

3131

32−main.parity_lemma_1 = proof {

32+Main.parity_lemma_1 = proof {

3333 intro j;

3434 intro;

3535 rewrite sym (plusSuccRightSucc j j);

test/test007/test007.idr+1−1

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

1−module main

1+module Main

33data Expr = Var String

44 | Val Int

test/test008/test008.idr+1−1

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

1−module main

1+module Main

33testlist : List (String, Int)

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

test/test009/test009.idr+1−1

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

1−module main

1+module Main

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

44pythag 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

33record Foo : Nat -> Set where

44 MkFoo : (name : String) ->

test/test012/test012a.idr+1−1

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

1−module main

1+module Main

33f : Nat -> Nat

44f x = x + 1

test/test013/test013.idr+1−1

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

1−module main

1+module Main

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

44forLoop [] f = return ()

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

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

1−module resimp

1+module Resimp

33-- IO operations which read a resource

44data Reader : Set -> Set where

test/test014/test014.idr+2−2

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

1−module main

1+module Main

3−import resimp

3+import Resimp

55data Purpose = Reading | Writing

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

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

1−module parity

1+module Parity

33data Parity : Nat -> Set where

44 even : Parity (n + n)

test/test015/test015.idr+7−7

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

1−module main

1+module Main

3−import parity

4−import system

3+import Parity

4+import System

66data Bit : Nat -> Set where

77 b0 : Bit O

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

8787

8888---------- Proofs ----------

8989

90−main.ntbOdd = proof {

90+Main.ntbOdd = proof {

9191 intro w,j;

9292 rewrite sym (plusZeroRightNeutral j);

9393 rewrite plusSuccRightSucc j j;

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

9696 trivial;

9797}

9898

99−main.ntbEven = proof {

99+Main.ntbEven = proof {

100100 compute;

101101 intro w,j;

102102 rewrite sym (plusZeroRightNeutral j);

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

107107

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

109109

110−main.adc_lemma_2 = proof {

110+Main.adc_lemma_2 = proof {

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

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

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

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

137137 trivial;

138138}

139139

140−main.adc_lemma_1 = proof {

140+Main.adc_lemma_1 = proof {

141141 intros;

142142 rewrite sym (plusZeroRightNeutral c) ;

143143 trivial;