git.iko.soy/Idris-dev
on master help sign in
Minor parser fixes; added binary sample
b74161fEdwin Brady
samples/binary.idrnew file+95
compare with master
unifiedsplit
@@ -0,0 +1,95 @@
1+module main
2+
3+data Bit : Nat -> Set where
4+ b0 : Bit 0
5+ b1 : Bit 1
6+
7+instance Show (Bit n) where
8+ show b0 = "0"
9+ show b1 = "1"
10+
11+infixl 5 #
12+
13+data Binary : (width : Nat) -> (value : Nat) -> Set where
14+ zero : Binary O O
15+ (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
16+
17+instance Show (Binary w k) where
18+ show zero = ""
19+ show (bin # bit) = show bin ++ show bit
20+
21+pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
22+term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
23+
24+addBit : Bit x -> Bit y -> Bit c ->
25+ (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
26+addBit b0 b0 b0 = bitpair b0 b0
27+addBit b0 b0 b1 = bitpair b0 b1
28+addBit b0 b1 b0 = bitpair b0 b1
29+addBit b0 b1 b1 = bitpair b1 b0
30+addBit b1 b0 b0 = bitpair b0 b1
31+addBit b1 b0 b1 = bitpair b1 b0
32+addBit b1 b1 b0 = bitpair b1 b0
33+addBit b1 b1 b1 = bitpair b1 b1
34+
35+adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
36+adc zero zero carry ?= zero # carry
37+adc (numx # bx) (numy # by) carry
38+ ?= let (bitpair carry0 lsb) = addBit bx by carry in
39+ adc numx numy carry0 # lsb
40+
41+main : IO ()
42+main = do let n1 = zero # b1 # b0 # b1 # b0
43+ let n2 = zero # b1 # b1 # b1 # b0
44+ print (adc n1 n2 b0)
45+
46+
47+
48+
49+
50+
51+
52+
53+
54+---------- Proofs ----------
55+
56+-- There is almost certainly an easier proof. I don't care, for now :)
57+
58+main.adc_lemma_2 = proof {
59+ intro c,w,v,bit0,num0;
60+ intro b0,v1,bit1,num1,b1;
61+ intro bc,x,x1,bx,bx1,prf;
62+ intro;
63+ rewrite sym (plusZeroRightNeutral v);
64+ rewrite sym (plusZeroRightNeutral v1);
65+ rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));
66+ rewrite (plusAssociative c (plus bit0 (plus v v)) bit1);
67+ rewrite (plusAssociative bit0 (plus v v) bit1);
68+ rewrite sym (plusCommutative (plus v v) bit1);
69+ rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
70+ rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
71+ rewrite sym prf;
72+ rewrite sym (plusZeroRightNeutral x);
73+ rewrite plusAssociative x1 (plus x x) (plus v v);
74+ rewrite plusAssociative x x (plus v v);
75+ rewrite sym (plusAssociative x v v);
76+ rewrite plusCommutative v (plus x v);
77+ rewrite sym (plusAssociative x v (plus x v));
78+ rewrite plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1);
79+ rewrite plusAssociative (plus x v) (plus x v) (plus v1 v1);
80+ rewrite plusAssociative x v (plus v1 v1);
81+ rewrite sym (plusAssociative v v1 v1);
82+ rewrite sym (plusAssociative x (plus v v1) v1);
83+ rewrite sym (plusAssociative x v v1);
84+ rewrite sym (plusCommutative (plus (plus x v) v1) v1);
85+ rewrite plusZeroRightNeutral (plus (plus x v) v1);
86+ rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) O));
87+ trivial;
88+}
89+
90+main.adc_lemma_1 = proof {
91+ intros;
92+ rewrite sym (plusZeroRightNeutral c) ;
93+ trivial;
94+}
95+
src/Idris/ElabDecls.hs+3−1
@@ -224,7 +224,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
224 do ctxt <- getContext
224 do ctxt <- getContext
225 -- Check n actually exists
225 -- Check n actually exists
226 case lookupTy Nothing n ctxt of
226 case lookupTy Nothing n ctxt of
227+ [] -> -- TODO: turn into a CAF if there's no arguments
228+ -- question: CAFs in where blocks?
227− [] -> tclift $ tfail $ (At fc (NoTypeDecl n))
229+ tclift $ tfail $ (At fc (NoTypeDecl n))
228 _ -> return ()
230 _ -> return ()
229 pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs
231 pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs
230
232
src/Idris/Parser.hs+17−2
@@ -412,6 +412,7 @@ pFunDecl' syn = try (do pushIndent
412 addAcc n acc
412 addAcc n acc
413 return (PTy syn fc (opts ++ opts') n ty))
413 return (PTy syn fc (opts ++ opts') n ty))
414 <|> try (pPattern syn)
414 <|> try (pPattern syn)
415+ <|> try (pCAF syn)
415
416
416pUsing :: SyntaxInfo -> IParser [PDecl]
417pUsing :: SyntaxInfo -> IParser [PDecl]
417pUsing syn =
418pUsing syn =
@@ -847,7 +848,7 @@ pLet syn = try (do reserved "let"; n <- pName;
847 v <- pExpr syn
848 v <- pExpr syn
848 reserved "in"; sc <- pExpr syn
849 reserved "in"; sc <- pExpr syn
849 return (PLet n ty v sc))
850 return (PLet n ty v sc))
850− <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
851+ <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
851 symbol "="; v <- pExpr syn
852 symbol "="; v <- pExpr syn
852 reserved "in"; sc <- pExpr syn
853 reserved "in"; sc <- pExpr syn
853 return (PCase fc v [(pat, sc)]))
854 return (PCase fc v [(pat, sc)]))
@@ -1179,18 +1180,32 @@ pPattern syn = do fc <- pfc
1179 clause <- pClause syn
1180 clause <- pClause syn
1180 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1181 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1181
1182
1183+pCAF :: SyntaxInfo -> IParser PDecl
1184+pCAF syn = do reserved "let"
1185+ n_in <- pfName; let n = expandNS syn n_in
1186+ lchar '='
1187+ t <- pExpr syn
1188+ pTerminator
1189+ fc <- pfc
1190+ return (PCAF fc n t)
1191+
1182pArgExpr syn = let syn' = syn { inPattern = True } in
1192pArgExpr syn = let syn' = syn { inPattern = True } in
1183 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1193 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1184
1194
1185pRHS :: SyntaxInfo -> Name -> IParser PTerm
1195pRHS :: SyntaxInfo -> Name -> IParser PTerm
1186pRHS syn n = do lchar '='; pExpr syn
1196pRHS syn n = do lchar '='; pExpr syn
1187 <|> do symbol "?="; rhs <- pExpr syn;
1197 <|> do symbol "?="; rhs <- pExpr syn;
1188− return (PLet (UN "value") Placeholder rhs (PMetavar n'))
1198+ return (addLet rhs)
1189 <|> do reserved "impossible"; return PImpossible
1199 <|> do reserved "impossible"; return PImpossible
1190 where mkN (UN x) = UN (x++"_lemma_1")
1200 where mkN (UN x) = UN (x++"_lemma_1")
1191 mkN (NS x n) = NS (mkN x) n
1201 mkN (NS x n) = NS (mkN x) n
1192 n' = mkN n
1202 n' = mkN n
1193
1203
1204+ addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1205+ addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1206+ where addLetC (l, r) = (l, addLet r)
1207+ addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1208+
1194pClause :: SyntaxInfo -> IParser PClause
1209pClause :: SyntaxInfo -> IParser PClause
1195pClause syn
1210pClause syn
1196 = try (do pushIndent
1211 = try (do pushIndent