Deal with shadowing better in patterns

Variable names in patterns should override global names, as long as
they are not applied to anything. If the global name is desired (e.g.
if it is the result of a dependency elsewhere, either use a _ or
give the qualified version of the name)

idris.cabal

@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.9.4
+Version:        0.9.4.2
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -45,7 +45,7 @@ Data-files:            rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h
                        rts/libtest.c
 Extra-source-files:    lib/Makefile  lib/*.idr lib/prelude/*.idr lib/network/*.idr
                        lib/control/monad/*.idr lib/language/*.idr
-                       tutorial/examples/*.idr
+                       tutorial/examples/*.idr lib/base.ipkg
                        rts/*.c rts/*.h rts/Makefile
 
 source-repository head
@@ -74,7 +74,7 @@ Executable     idris
 
                               IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
                               IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,
-                              IRTS.Compiler,
+                              IRTS.Compiler, IRTS.CodegenJava, IRTS.BCImp,
 
                               Paths_idris
 

src/Idris/AbsSyntax.hs

@@ -705,13 +705,24 @@ addImpl' inpat env ist ptm = ai env ptm
 
 aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
 aiFn inpat True ist fc f []
-  = case lookupCtxt Nothing f (idris_implicits ist) of
-        [] -> Right $ PRef fc f
-        alts -> if (any (all imp) alts)
+  = case lookupDef Nothing f (tt_ctxt ist) of
+        [] -> Right $ PPatvar fc f
+        alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
+                    -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $ 
+                    if (not (vname f) || tcname f 
+                           || any constructor alts || any allImp ialts)
                         then aiFn inpat False ist fc f [] -- use it as a constructor
-                        else Right $ PRef fc f
+                        else Right $ PPatvar fc f
     where imp (PExp _ _ _) = False
           imp _ = True
+          allImp [] = False
+          allImp xs = all imp xs
+          constructor (TyDecl (DCon _ _) _) = True
+          constructor _ = False
+
+          vname (UN n) = True -- non qualified
+          vname _ = False
+
 aiFn inpat expat ist fc f as
     | f `elem` primNames = Right $ PApp fc (PRef fc f) as
 aiFn inpat expat ist fc f as

src/Idris/AbsSyntaxTree.hs

@@ -342,6 +342,7 @@ updateNs ns t = mapPT updateRef t
 
 data PTerm = PQuote Raw
            | PRef FC Name
+           | PPatvar FC Name
            | PLam Name PTerm PTerm
            | PPi  Plicity Name PTerm PTerm
            | PLet Name PTerm PTerm PTerm 
@@ -650,6 +651,7 @@ prettyImp impl = prettySe 10
         text "![" $$ pretty r <> text "]"
       else
         text "![" <> pretty r <> text "]"
+    prettySe p (PPatvar fc n) = pretty n
     prettySe p (PRef fc n) =
       if impl then
         pretty n
@@ -825,6 +827,7 @@ prettyImp impl = prettySe 10
 showImp :: Bool -> PTerm -> String
 showImp impl tm = se 10 tm where
     se p (PQuote r) = "![" ++ show r ++ "]"
+    se p (PPatvar fc n) = show n
     se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
                                else showbasic n
       where showbasic n@(UN _) = show n

src/Idris/ElabTerm.hs

@@ -153,6 +153,7 @@ elab ist info pattern tcgen fn tm
         = trySeq as
         where trySeq [] = fail "All alternatives fail to elaborate"
               trySeq (x : xs) = try (elab' ina x) (trySeq xs)
+    elab' ina (PPatvar fc n) | pattern = patvar n
     elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
                          = do ctxt <- get_context
                               let iscon = isConName Nothing n ctxt

src/Idris/IBC.hs

@@ -1087,6 +1087,9 @@ instance Binary PTerm where
                 PTactics x1 -> do putWord8 25
                                   put x1
                 PImpossible -> putWord8 27
+                PPatvar x1 x2 -> do putWord8 28
+                                    put x1
+                                    put x2
         get
           = do i <- getWord8
                case i of
@@ -1164,6 +1167,9 @@ instance Binary PTerm where
                    25 -> do x1 <- get
                             return (PTactics x1)
                    27 -> return PImpossible
+                   28 -> do x1 <- get
+                            x2 <- get
+                            return (PPatvar x1 x2)
                    _ -> error "Corrupted binary data for PTerm"
 
 instance (Binary t) => Binary (PTactic' t) where

test/test014/run

@@ -1,4 +1,4 @@
 #!/bin/bash
 idris test014.idr -o test014
 ./test014
-rm -f test014 test014.ibc
+rm -f test014 resimp.ibc test014.ibc

test/test015/expected

@@ -0,0 +1,3 @@
+00101010
+01011001
+010000011

test/test015/parity.idr

@@ -0,0 +1,28 @@
+module parity
+
+data Parity : Nat -> Set where
+   even : Parity (n + n)
+   odd  : Parity (S (n + n))
+
+parity : (n:Nat) -> Parity n
+parity O     = even {n=O}
+parity (S O) = odd {n=O}
+parity (S (S k)) with (parity k)
+    parity (S (S (j + j)))     | even ?= even {n=S j}
+    parity (S (S (S (j + j)))) | odd  ?= odd {n=S j}
+
+
+parity_lemma_2 = proof {
+    intro;
+    intro;
+    rewrite sym (plusSuccRightSucc j j);
+    trivial;
+}
+
+parity_lemma_1 = proof {
+    intro j;
+    intro;
+    rewrite sym (plusSuccRightSucc j j);
+    trivial;
+}
+

test/test015/run

@@ -0,0 +1,4 @@
+#!/bin/bash
+idris test015.idr -o test015
+./test015
+rm -f test015 parity.ibc test015.ibc

test/test015/test015.idr

@@ -0,0 +1,141 @@
+module main
+
+import parity
+import system
+
+data Bit : Nat -> Set where
+     b0 : Bit 0
+     b1 : Bit 1
+
+instance Show (Bit n) where
+     show b0 = "0"
+     show b1 = "1"
+
+infixl 5 #
+
+data Binary : (width : Nat) -> (value : Nat) -> Set where
+     zero : Binary O O
+     (#)  : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
+
+instance Show (Binary w k) where
+     show zero = ""
+     show (bin # bit) = show bin ++ show bit
+
+pad : Binary w n -> Binary (S w) n
+pad zero = zero # b0 
+pad (num # x) = pad num # x
+
+natToBin : (width : Nat) -> (n : Nat) ->
+           Maybe (Binary width n)
+natToBin O (S k) = Nothing
+natToBin O O = Just zero
+natToBin (S k) O = do x <- natToBin k O
+                      Just (pad x)
+natToBin (S w) (S k) with (parity k)
+  natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j
+                                            let value = jbin # b1
+                                            ?ntbEven
+  natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)
+                                               let value = jbin # b0
+                                               ?ntbOdd
+
+testBin : Maybe (Binary 8 42)
+testBin = natToBin _ _
+
+pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
+term    syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
+
+addBit : Bit x -> Bit y -> Bit c -> 
+          (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
+addBit b0 b0 b0 = bitpair b0 b0
+addBit b0 b0 b1 = bitpair b0 b1 
+addBit b0 b1 b0 = bitpair b0 b1
+addBit b0 b1 b1 = bitpair b1 b0
+addBit b1 b0 b0 = bitpair b0 b1 
+addBit b1 b0 b1 = bitpair b1 b0 
+addBit b1 b1 b0 = bitpair b1 b0 
+addBit b1 b1 b1 = bitpair b1 b1 
+
+adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y) 
+adc zero        zero        carry ?= zero # carry
+adc (numx # bx) (numy # by) carry
+   ?= let (bitpair carry0 lsb) = addBit bx by carry in 
+          adc numx numy carry0 # lsb
+
+readNum : IO Nat
+readNum = do putStr "Enter a number:"
+             i <- getLine
+             let n : Int = cast i
+             return (fromInteger n)
+
+main : IO ()
+main = do let Just bin1 = natToBin 8 42
+          print bin1
+          let Just bin2 = natToBin 8 89
+          print bin2
+          print (adc bin1 bin2 b0)
+
+
+
+
+
+
+
+---------- Proofs ----------
+
+main.ntbOdd = proof {
+    intro w,j;
+    rewrite sym (plusZeroRightNeutral j);
+    rewrite plusSuccRightSucc j j;
+    intros;
+    refine Just;
+    trivial;
+}
+
+main.ntbEven = proof {
+    compute;
+    intro w,j;
+    rewrite sym (plusZeroRightNeutral j);
+    intros;
+    refine Just;
+    trivial;
+}
+
+-- There is almost certainly an easier proof. I don't care, for now :)
+
+main.adc_lemma_2 = proof {
+    intro c,w,v,bit0,num0;
+    intro b0,v1,bit1,num1,b1;
+    intro bc,x,x1,bx,bx1;
+    rewrite sym (plusZeroRightNeutral x);
+    rewrite sym (plusZeroRightNeutral v1);
+    rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));
+    rewrite sym (plusZeroRightNeutral v);
+    intros;
+    rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));
+    rewrite  (plusAssociative c (plus bit0 (plus v v)) bit1);
+    rewrite  (plusAssociative bit0 (plus v v) bit1);
+    rewrite plusCommutative bit1 (plus v v);
+    rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
+    rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
+    rewrite sym b;
+    rewrite plusAssociative x1 (plus x x) (plus v v);
+    rewrite plusAssociative x x (plus v v);
+    rewrite sym (plusAssociative x v v);
+    rewrite plusCommutative v (plus x v);
+    rewrite sym (plusAssociative x v (plus x v));
+    rewrite (plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1));
+    rewrite sym (plusAssociative (plus (plus x v) (plus x v)) v1 v1);
+    rewrite  (plusAssociative (plus x v) (plus x v) v1);
+    rewrite (plusCommutative v1 (plus x v));
+    rewrite sym (plusAssociative (plus x v) v1 (plus x v));
+    rewrite (plusAssociative (plus (plus x v) v1) (plus x v) v1);
+    trivial;
+}
+
+main.adc_lemma_1 = proof {
+    intros;
+    rewrite sym (plusZeroRightNeutral c) ;
+    trivial;
+}
+