git.iko.soy/Idris-dev
on master help sign in
Added builtins.idr and fixed a bug or two
commit180e97989ec3bc95b07b6a7fdbd0a6c28857d7ee authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 16 Oct 2011, 23:45 (15 years ago) parent834a5e0
4 files changed+32−1
compare with master
unifiedsplit
lib/builtins.idr+24 lib/prelude.idr+1 src/Idris/AbsSyntax.hs+5 src/Idris/Parser.hs+2−1
lib/builtins.idrnew file+24
@@ -0,0 +1,24 @@
1+data Sigma : (a : Set) -> (P : a -> Set) -> Set where
2+ Exists : {P : a -> Set} -> (x : a) -> P x -> Sigma a P;
3+
4+getSigIdx : {P : a -> Set} -> Sigma a P -> a;
5+getSigIdx (Exists a v) = a;
6+
7+getSigVal : {P : a -> Set} -> (s : Sigma a P) -> P (getSigIdx s);
8+getSigVal (Exists a v) = v;
9+
10+id : a -> a;
11+id x = x;
12+
13+fst : (a, b) -> a;
14+fst (x, y) = x;
15+
16+snd : (a, b) -> b;
17+snd (x, y) = y;
18+
19+infixl 9 .;
20+
21+(.) : (b -> c) -> (a -> b) -> a -> c;
22+(.) f g x = f (g x);
23+
24+
lib/prelude.idr+1
@@ -1,3 +1,4 @@
1+import builtins;
12import nat;
23import list;
34import vect;
src/Idris/AbsSyntax.hs+5
@@ -303,6 +303,7 @@ allNamesIn tm = nub $ ni [] tm
303303 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
304304 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
305305 ni env (PHidden tm) = ni env tm
306+ ni env (PPair l r) = ni env l ++ ni env r
306307 ni env _ = []
307308
308309namesIn :: IState -> PTerm -> [Name]
@@ -316,6 +317,7 @@ namesIn ist tm = nub $ ni [] tm
316317 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
317318 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
318319 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
320+ ni env (PPair l r) = ni env l ++ ni env r
319321 ni env (PHidden tm) = ni env tm
320322 ni env _ = []
321323
@@ -396,6 +398,9 @@ implicitise syn ist tm
396398 (decls, ns) <- get -- ignore decls in HO types
397399 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
398400 imps True (n:env) sc
401+ imps top env (PPair l r)
402+ = do (decls, ns) <- get
403+ put (decls, nub (ns ++ namesIn ist l ++ namesIn ist r))
399404 imps top env (PLam n ty sc)
400405 = do imps False env ty
401406 imps False (n:env) sc
src/Idris/Parser.hs+2−1
@@ -174,7 +174,7 @@ pSyntaxRule syn
174174pSynSym :: IParser SSymbol
175175pSynSym = try (do lchar '['; n <- pName; lchar ']'
176176 return (Expr n))
177− <|> do n <- pName
177+ <|> do n <- iName []
178178 return (Keyword n)
179179 <|> do sym <- strlit
180180 return (Symbol sym)
@@ -279,6 +279,7 @@ pExt syn (Rule (s:ssym) ptm)
279279 where upd ns (DoExp t : ds) = DoExp (update ns t) : upd ns ds
280280 upd ns (DoBind n t : ds) = DoBind n (update ns t) : upd (dropn n ns) ds
281281 upd ns (DoLet n t : ds) = DoLet n (update ns t) : upd (dropn n ns) ds
282+ update ns t = t
282283
283284pName = do i <- getState
284285 iName (map show (names (syntax_rules i)))