Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Minor parser fixes; added binary sample

  • Loading branch information...
commit b74161ffb8d16c18f66c44cec9447c56fc7b2264 1 parent dde7fc3
Edwin Brady authored
Showing with 115 additions and 3 deletions.
  1. +95 −0 samples/binary.idr
  2. +3 −1 src/Idris/ElabDecls.hs
  3. +17 −2 src/Idris/Parser.hs
View
95 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;
+}
+
View
4 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
View
19 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
Please sign in to comment.
Something went wrong with that request. Please try again.