180e979 · Idris-dev · git.iko.soy

lib/builtins.idrnew file+24

compare with master

unifiedsplit

@@ -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;

1import nat;

2import nat;

2import list;

3import list;

3import vect;

4import vect;

src/Idris/AbsSyntax.hs+5

@@ -303,6 +303,7 @@ allNamesIn tm = nub $ ni [] tm

303 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

304 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

305 ni env (PHidden tm) = ni env tm

306+ ni env (PPair l r) = ni env l ++ ni env r

306 ni env _ = []

307 ni env _ = []

307

308

308namesIn :: IState -> PTerm -> [Name]

309namesIn :: IState -> PTerm -> [Name]

@@ -316,6 +317,7 @@ namesIn ist tm = nub $ ni [] tm

316 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)

317 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)

317 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

318 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

318 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

319 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

319 ni env (PHidden tm) = ni env tm

321 ni env (PHidden tm) = ni env tm

320 ni env _ = []

322 ni env _ = []

321

323

@@ -396,6 +398,9 @@ implicitise syn ist tm

396 (decls, ns) <- get -- ignore decls in HO types

398 (decls, ns) <- get -- ignore decls in HO types

397 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

399 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

398 imps True (n:env) sc

400 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))

399 imps top env (PLam n ty sc)

404 imps top env (PLam n ty sc)

400 = do imps False env ty

405 = do imps False env ty

401 imps False (n:env) sc

406 imps False (n:env) sc

src/Idris/Parser.hs+2−1

@@ -174,7 +174,7 @@ pSyntaxRule syn

174pSynSym :: IParser SSymbol

175pSynSym = try (do lchar '['; n <- pName; lchar ']'

176 return (Expr n))

177− <|> do n <- pName

177+ <|> do n <- iName []

178 return (Keyword n)

179 <|> do sym <- strlit

180 return (Symbol sym)

@@ -279,6 +279,7 @@ pExt syn (Rule (s:ssym) ptm)

279 where upd ns (DoExp t : ds) = DoExp (update ns t) : upd ns ds

280 upd ns (DoBind n t : ds) = DoBind n (update ns t) : upd (dropn n ns) ds

281 upd ns (DoLet n t : ds) = DoLet n (update ns t) : upd (dropn n ns) ds

282+ update ns t = t

282

283

283pName = do i <- getState

284pName = do i <- getState

284 iName (map show (names (syntax_rules i)))

285 iName (map show (names (syntax_rules i)))