Minor parser fixes; added binary sample

samples/binary.idr

@@ -0,0 +1,95 @@
+module main
+
+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
+
+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
+
+main : IO ()
+main = do let n1 = zero # b1 # b0 # b1 # b0
+          let n2 = zero # b1 # b1 # b1 # b0
+          print (adc n1 n2 b0)
+
+
+
+
+
+
+
+
+
+---------- Proofs ----------
+
+-- 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,prf;
+    intro;
+    rewrite sym (plusZeroRightNeutral v);
+    rewrite sym (plusZeroRightNeutral v1);
+    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 sym (plusCommutative (plus v v) bit1);
+    rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
+    rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
+    rewrite sym prf;
+    rewrite sym (plusZeroRightNeutral x);
+    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 plusAssociative (plus x v) (plus x v) (plus v1 v1);
+    rewrite plusAssociative x v (plus v1 v1);
+    rewrite sym (plusAssociative v v1 v1);
+    rewrite sym (plusAssociative x (plus v v1) v1);
+    rewrite sym (plusAssociative x v v1);
+    rewrite sym (plusCommutative (plus (plus x v) v1) v1);
+    rewrite plusZeroRightNeutral (plus (plus x v) v1);
+    rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) O));
+    trivial;
+}
+
+main.adc_lemma_1 = proof {
+    intros;
+    rewrite sym (plusZeroRightNeutral c) ;
+    trivial;
+}
+

src/Idris/ElabDecls.hs

@@ -224,7 +224,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
       do ctxt <- getContext
          -- Check n actually exists
          case lookupTy Nothing n ctxt of
-            [] -> tclift $ tfail $ (At fc (NoTypeDecl n))
+            [] -> -- TODO: turn into a CAF if there's no arguments
+                  -- question: CAFs in where blocks?
+                  tclift $ tfail $ (At fc (NoTypeDecl n))
             _ -> return ()
          pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs
 

src/Idris/Parser.hs

@@ -412,6 +412,7 @@ pFunDecl' syn = try (do pushIndent
                         addAcc n acc
                         return (PTy syn fc (opts ++ opts') n ty))
             <|> try (pPattern syn)
+            <|> try (pCAF syn)
 
 pUsing :: SyntaxInfo -> IParser [PDecl]
 pUsing syn = 
@@ -847,7 +848,7 @@ pLet syn = try (do reserved "let"; n <- pName;
                    v <- pExpr syn
                    reserved "in";  sc <- pExpr syn
                    return (PLet n ty v sc))
-           <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
+           <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
                    symbol "="; v <- pExpr syn
                    reserved "in"; sc <- pExpr syn
                    return (PCase fc v [(pat, sc)]))
@@ -1179,18 +1180,32 @@ pPattern syn = do fc <- pfc
                   clause <- pClause syn
                   return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
 
+pCAF :: SyntaxInfo -> IParser PDecl
+pCAF syn = do reserved "let"
+              n_in <- pfName; let n = expandNS syn n_in
+              lchar '='
+              t <- pExpr syn
+              pTerminator
+              fc <- pfc
+              return (PCAF fc n t)
+
 pArgExpr syn = let syn' = syn { inPattern = True } in
                    try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
 
 pRHS :: SyntaxInfo -> Name -> IParser PTerm
 pRHS syn n = do lchar '='; pExpr syn
          <|> do symbol "?="; rhs <- pExpr syn;
-                return (PLet (UN "value") Placeholder rhs (PMetavar n')) 
+                return (addLet rhs)
          <|> do reserved "impossible"; return PImpossible
   where mkN (UN x)   = UN (x++"_lemma_1")
         mkN (NS x n) = NS (mkN x) n
         n' = mkN n
 
+        addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
+        addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
+          where addLetC (l, r) = (l, addLet r)
+        addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n')) 
+
 pClause :: SyntaxInfo -> IParser PClause
 pClause syn
          = try (do pushIndent