f26b42f · Idris-dev · git.iko.soy

idris.cabal+3−3

compare with master

unifiedsplit

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

1Name: idris

2−Version: 0.9.4

2+Version: 0.9.4.2

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -45,7 +45,7 @@ Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h

45 rts/libtest.c

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

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

48− tutorial/examples/*.idr

48+ tutorial/examples/*.idr lib/base.ipkg

49 rts/*.c rts/*.h rts/Makefile

50

51source-repository head

@@ -74,7 +74,7 @@ Executable idris

74

75 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

76 IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,

77− IRTS.Compiler,

77+ IRTS.Compiler, IRTS.CodegenJava, IRTS.BCImp,

78

79 Paths_idris

80

src/Idris/AbsSyntax.hs+15−4

@@ -705,13 +705,24 @@ addImpl' inpat env ist ptm = ai env ptm

705

706aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

707aiFn inpat True ist fc f []

708− = case lookupCtxt Nothing f (idris_implicits ist) of

708+ = case lookupDef Nothing f (tt_ctxt ist) of

709− [] -> Right $ PRef fc f

709+ [] -> Right $ PPatvar fc f

710− alts -> if (any (all imp) alts)

710+ alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in

711+ -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

712+ if (not (vname f) || tcname f

713+ || any constructor alts || any allImp ialts)

711 then aiFn inpat False ist fc f [] -- use it as a constructor

714 then aiFn inpat False ist fc f [] -- use it as a constructor

712− else Right $ PRef fc f

715+ else Right $ PPatvar fc f

713 where imp (PExp _ _ _) = False

716 where imp (PExp _ _ _) = False

714 imp _ = True

717 imp _ = True

718+ allImp [] = False

719+ allImp xs = all imp xs

720+ constructor (TyDecl (DCon _ _) _) = True

721+ constructor _ = False

722+

723+ vname (UN n) = True -- non qualified

724+ vname _ = False

725+

715aiFn inpat expat ist fc f as

726aiFn inpat expat ist fc f as

716 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

727 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

717aiFn inpat expat ist fc f as

728aiFn inpat expat ist fc f as

src/Idris/AbsSyntaxTree.hs+3

@@ -342,6 +342,7 @@ updateNs ns t = mapPT updateRef t

342

343data PTerm = PQuote Raw

344 | PRef FC Name

345+ | PPatvar FC Name

345 | PLam Name PTerm PTerm

346 | PLam Name PTerm PTerm

346 | PPi Plicity Name PTerm PTerm

347 | PPi Plicity Name PTerm PTerm

347 | PLet Name PTerm PTerm PTerm

348 | PLet Name PTerm PTerm PTerm

@@ -650,6 +651,7 @@ prettyImp impl = prettySe 10

650 text "![" $$ pretty r <> text "]"

651 text "![" $$ pretty r <> text "]"

651 else

652 else

652 text "![" <> pretty r <> text "]"

653 text "![" <> pretty r <> text "]"

654+ prettySe p (PPatvar fc n) = pretty n

653 prettySe p (PRef fc n) =

655 prettySe p (PRef fc n) =

654 if impl then

656 if impl then

655 pretty n

657 pretty n

@@ -825,6 +827,7 @@ prettyImp impl = prettySe 10

825showImp :: Bool -> PTerm -> String

827showImp :: Bool -> PTerm -> String

826showImp impl tm = se 10 tm where

828showImp impl tm = se 10 tm where

827 se p (PQuote r) = "![" ++ show r ++ "]"

829 se p (PQuote r) = "![" ++ show r ++ "]"

830+ se p (PPatvar fc n) = show n

828 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"

831 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"

829 else showbasic n

832 else showbasic n

830 where showbasic n@(UN _) = show n

833 where showbasic n@(UN _) = show n

src/Idris/ElabTerm.hs+1

@@ -153,6 +153,7 @@ elab ist info pattern tcgen fn tm

153 = trySeq as

154 where trySeq [] = fail "All alternatives fail to elaborate"

155 trySeq (x : xs) = try (elab' ina x) (trySeq xs)

156+ elab' ina (PPatvar fc n) | pattern = patvar n

156 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

157 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

157 = do ctxt <- get_context

158 = do ctxt <- get_context

158 let iscon = isConName Nothing n ctxt

159 let iscon = isConName Nothing n ctxt

src/Idris/IBC.hs+6

@@ -1087,6 +1087,9 @@ instance Binary PTerm where

1087 PTactics x1 -> do putWord8 25

1088 put x1

1089 PImpossible -> putWord8 27

1090+ PPatvar x1 x2 -> do putWord8 28

1091+ put x1

1092+ put x2

1090 get

1093 get

1091 = do i <- getWord8

1094 = do i <- getWord8

1092 case i of

1095 case i of

@@ -1164,6 +1167,9 @@ instance Binary PTerm where

1164 25 -> do x1 <- get

1167 25 -> do x1 <- get

1165 return (PTactics x1)

1168 return (PTactics x1)

1166 27 -> return PImpossible

1169 27 -> return PImpossible

1170+ 28 -> do x1 <- get

1171+ x2 <- get

1172+ return (PPatvar x1 x2)

1167 _ -> error "Corrupted binary data for PTerm"

1173 _ -> error "Corrupted binary data for PTerm"

1168

1174

1169instance (Binary t) => Binary (PTactic' t) where

1175instance (Binary t) => Binary (PTactic' t) where

test/test014/run+1−1

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

1#!/bin/bash

2idris test014.idr -o test014

3./test014

4−rm -f test014 test014.ibc

4+rm -f test014 resimp.ibc test014.ibc

test/test015/expectednew file+3

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

1+00101010

2+01011001

3+010000011

test/test015/parity.idrnew file+28

@@ -0,0 +1,28 @@

1+module parity

2+

3+data Parity : Nat -> Set where

4+ even : Parity (n + n)

5+ odd : Parity (S (n + n))

6+

7+parity : (n:Nat) -> Parity n

8+parity O = even {n=O}

9+parity (S O) = odd {n=O}

10+parity (S (S k)) with (parity k)

11+ parity (S (S (j + j))) | even ?= even {n=S j}

12+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

13+

14+

15+parity_lemma_2 = proof {

16+ intro;

17+ intro;

18+ rewrite sym (plusSuccRightSucc j j);

19+ trivial;

20+}

21+

22+parity_lemma_1 = proof {

23+ intro j;

24+ intro;

25+ rewrite sym (plusSuccRightSucc j j);

26+ trivial;

27+}

28+

test/test015/runnew file+4

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

1+#!/bin/bash

2+idris test015.idr -o test015

3+./test015

4+rm -f test015 parity.ibc test015.ibc

test/test015/test015.idrnew file+141

@@ -0,0 +1,141 @@

1+module main

2+

3+import parity

4+import system

5+

6+data Bit : Nat -> Set where

7+ b0 : Bit 0

8+ b1 : Bit 1

9+

10+instance Show (Bit n) where

11+ show b0 = "0"

12+ show b1 = "1"

13+

14+infixl 5 #

15+

16+data Binary : (width : Nat) -> (value : Nat) -> Set where

17+ zero : Binary O O

18+ (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

19+

20+instance Show (Binary w k) where

21+ show zero = ""

22+ show (bin # bit) = show bin ++ show bit

23+

24+pad : Binary w n -> Binary (S w) n

25+pad zero = zero # b0

26+pad (num # x) = pad num # x

27+

28+natToBin : (width : Nat) -> (n : Nat) ->

29+ Maybe (Binary width n)

30+natToBin O (S k) = Nothing

31+natToBin O O = Just zero

32+natToBin (S k) O = do x <- natToBin k O

33+ Just (pad x)

34+natToBin (S w) (S k) with (parity k)

35+ natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j

36+ let value = jbin # b1

37+ ?ntbEven

38+ natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)

39+ let value = jbin # b0

40+ ?ntbOdd

41+

42+testBin : Maybe (Binary 8 42)

43+testBin = natToBin _ _

44+

45+pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))

46+term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))

47+

48+addBit : Bit x -> Bit y -> Bit c ->

49+ (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))

50+addBit b0 b0 b0 = bitpair b0 b0

51+addBit b0 b0 b1 = bitpair b0 b1

52+addBit b0 b1 b0 = bitpair b0 b1

53+addBit b0 b1 b1 = bitpair b1 b0

54+addBit b1 b0 b0 = bitpair b0 b1

55+addBit b1 b0 b1 = bitpair b1 b0

56+addBit b1 b1 b0 = bitpair b1 b0

57+addBit b1 b1 b1 = bitpair b1 b1

58+

59+adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)

60+adc zero zero carry ?= zero # carry

61+adc (numx # bx) (numy # by) carry

62+ ?= let (bitpair carry0 lsb) = addBit bx by carry in

63+ adc numx numy carry0 # lsb

64+

65+readNum : IO Nat

66+readNum = do putStr "Enter a number:"

67+ i <- getLine

68+ let n : Int = cast i

69+ return (fromInteger n)

70+

71+main : IO ()

72+main = do let Just bin1 = natToBin 8 42

73+ print bin1

74+ let Just bin2 = natToBin 8 89

75+ print bin2

76+ print (adc bin1 bin2 b0)

77+

78+

79+

80+

81+

82+

83+

84+---------- Proofs ----------

85+

86+main.ntbOdd = proof {

87+ intro w,j;

88+ rewrite sym (plusZeroRightNeutral j);

89+ rewrite plusSuccRightSucc j j;

90+ intros;

91+ refine Just;

92+ trivial;

93+}

94+

95+main.ntbEven = proof {

96+ compute;

97+ intro w,j;

98+ rewrite sym (plusZeroRightNeutral j);

99+ intros;

100+ refine Just;

101+ trivial;

102+}

103+

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

105+

106+main.adc_lemma_2 = proof {

107+ intro c,w,v,bit0,num0;

108+ intro b0,v1,bit1,num1,b1;

109+ intro bc,x,x1,bx,bx1;

110+ rewrite sym (plusZeroRightNeutral x);

111+ rewrite sym (plusZeroRightNeutral v1);

112+ rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));

113+ rewrite sym (plusZeroRightNeutral v);

114+ intros;

115+ rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));

116+ rewrite (plusAssociative c (plus bit0 (plus v v)) bit1);

117+ rewrite (plusAssociative bit0 (plus v v) bit1);

118+ rewrite plusCommutative bit1 (plus v v);

119+ rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));

120+ rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));

121+ rewrite sym b;

122+ rewrite plusAssociative x1 (plus x x) (plus v v);

123+ rewrite plusAssociative x x (plus v v);

124+ rewrite sym (plusAssociative x v v);

125+ rewrite plusCommutative v (plus x v);

126+ rewrite sym (plusAssociative x v (plus x v));

127+ rewrite (plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1));

128+ rewrite sym (plusAssociative (plus (plus x v) (plus x v)) v1 v1);

129+ rewrite (plusAssociative (plus x v) (plus x v) v1);

130+ rewrite (plusCommutative v1 (plus x v));

131+ rewrite sym (plusAssociative (plus x v) v1 (plus x v));

132+ rewrite (plusAssociative (plus (plus x v) v1) (plus x v) v1);

133+ trivial;

134+}

135+

136+main.adc_lemma_1 = proof {

137+ intros;

138+ rewrite sym (plusZeroRightNeutral c) ;

139+ trivial;

140+}

141+