95a558b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added = and refl

95a558bEdwin Brady15 years ago

lib/nat.idr+7

compare with master

unifiedsplit

@@ -5,3 +5,10 @@ plus : Nat -> Nat -> Nat;

5plus O y = y;

6plus (S k) y = S (plus k y);

8+eqRespS : m = n -> S m = S n;

9+eqRespS refl = refl;

10+

11+plusnO : (m : Nat) -> plus m O = m;

12+plusnO O = refl;

13+plusnO (S k) = eqRespS (plusnO k);

14+

src/Core/CoreParser.hs+1−1

@@ -19,7 +19,7 @@ idrisDef = haskellDef {

19 opLetter = iOpLetter,

20 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

22− "do", "dsl", "import",

22+ "do", "dsl", "import", "return", "refl",

23 "infix", "infixl", "infixr", "prefix",

24 "where", "with", "forall", "syntax",

25 "using", "params", "namespace",

src/Idris/AbsSyntax.hs+49−11

@@ -177,6 +177,8 @@ data PTerm = PQuote Raw

177 | PApp FC PTerm [PArg]

178 | PTrue FC

179 | PFalse FC

180+ | PRefl FC

181+ | PEq FC PTerm PTerm

180 | PPair FC PTerm PTerm

182 | PPair FC PTerm PTerm

181 | PDPair FC PTerm PTerm

183 | PDPair FC PTerm PTerm

182 | PHidden PTerm -- irrelevant or hidden pattern

184 | PHidden PTerm -- irrelevant or hidden pattern

@@ -302,8 +304,10 @@ showImp impl tm = se 10 tm where

302 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")

304 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")

303 ++ concatMap seArg args

305 ++ concatMap seArg args

304 se p (PHidden tm) = "." ++ se 0 tm

306 se p (PHidden tm) = "." ++ se 0 tm

307+ se p (PRefl _) = "refl"

305 se p (PTrue _) = "()"

308 se p (PTrue _) = "()"

306 se p (PFalse _) = "_|_"

309 se p (PFalse _) = "_|_"

310+ se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

307 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

311 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

308 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

312 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

309 se p PSet = "Set"

313 se p PSet = "Set"

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

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

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

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

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

328 ni env (PHidden tm) = ni env tm

332 ni env (PHidden tm) = ni env tm

333+ ni env (PEq _ l r) = ni env l ++ ni env r

329 ni env (PPair _ l r) = ni env l ++ ni env r

334 ni env (PPair _ l r) = ni env l ++ ni env r

330 ni env (PDPair _ l r) = ni env l ++ ni env r

335 ni env (PDPair _ l r) = ni env l ++ ni env r

331 ni env _ = []

336 ni env _ = []

@@ -341,6 +346,7 @@ namesIn ist tm = nub $ ni [] tm

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

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

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

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

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

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

349+ ni env (PEq _ l r) = ni env l ++ ni env r

344 ni env (PPair _ l r) = ni env l ++ ni env r

350 ni env (PPair _ l r) = ni env l ++ ni env r

345 ni env (PDPair _ l r) = ni env l ++ ni env r

351 ni env (PDPair _ l r) = ni env l ++ ni env r

346 ni env (PHidden tm) = ni env tm

352 ni env (PHidden tm) = ni env tm

@@ -369,8 +375,7 @@ getInferTerm tm = error ("getInferTerm " ++ show tm)

369getInferType (Bind n b sc) = Bind n b $ getInferType sc

375getInferType (Bind n b sc) = Bind n b $ getInferType sc

370getInferType (App (App _ ty) _) = ty

376getInferType (App (App _ ty) _) = ty

371

377

372−-- Handy primitives: Unit, False, Pair, MkPair, mkForeign

378+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

373−

374

379

375unitTy = MN 0 "__Unit"

380unitTy = MN 0 "__Unit"

376unitCon = MN 0 "__II"

381unitCon = MN 0 "__II"

@@ -391,6 +396,19 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

391 PExp (PRef bi (n "B"))])))), bi)]

396 PExp (PRef bi (n "B"))])))), bi)]

392 where n a = MN 0 a

397 where n a = MN 0 a

393

398

399+eqTy = UN ["="]

400+eqCon = UN ["refl"]

401+eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),

402+ (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]

403+ PSet)

404+ [(eqCon, PPi Imp (n "a") PSet (

405+ PPi Imp (n "x") (PRef bi (n "a"))

406+ (PApp bi (PRef bi eqTy) [PImp (n "a") Placeholder,

407+ PImp (n "b") Placeholder,

408+ PExp (PRef bi (n "x")),

409+ PExp (PRef bi (n "x"))])), bi)]

410+ where n a = MN 0 a

411+

394-- Defined in builtins.idr

412-- Defined in builtins.idr

395sigmaTy = UN ["Sigma"]

413sigmaTy = UN ["Sigma"]

396existsCon = UN ["Exists"]

414existsCon = UN ["Exists"]

@@ -404,6 +422,8 @@ piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)

404-- Add implicit Pi bindings for any names in the term which appear in an

422-- Add implicit Pi bindings for any names in the term which appear in an

405-- argument position.

423-- argument position.

406

424

425+-- This has become a right mess already. Better redo it some time...

426+

407implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

427implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

408implicitise syn ist tm

428implicitise syn ist tm

409 = let uvars = using syn

429 = let uvars = using syn

@@ -414,29 +434,39 @@ implicitise syn ist tm

414 then (tm, reverse declimps)

434 then (tm, reverse declimps)

415 else implicitise syn ist (pibind uvars ns tm)

435 else implicitise syn ist (pibind uvars ns tm)

416 where

436 where

437+ dropAll (x:xs) ys | x `elem` ys = dropAll xs ys

438+ | otherwise = x : dropAll xs ys

439+ dropAll [] ys = []

440+

417 imps top env (PApp _ f as)

441 imps top env (PApp _ f as)

418 = do (decls, ns) <- get

442 = do (decls, ns) <- get

419 let isn = concatMap (namesIn ist) (map getTm as)

443 let isn = concatMap (namesIn ist) (map getTm as)

420− put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

444+ put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

421 imps top env (PPi Imp n ty sc)

445 imps top env (PPi Imp n ty sc)

422− = do let isn = namesIn ist ty \\ [n]

446+ = do let isn = nub (namesIn ist ty) `dropAll` [n]

423 (decls , ns) <- get

447 (decls , ns) <- get

448+ put (PImp n ty : decls,

424− put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

449+ nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

425 imps True (n:env) sc

450 imps True (n:env) sc

426 imps top env (PPi Exp n ty sc)

451 imps top env (PPi Exp n ty sc)

427− = do let isn = (namesIn ist ty ++ case sc of

452+ = do let isn = nub (namesIn ist ty ++ case sc of

428− (PRef _ x) -> namesIn ist sc

453+ (PRef _ x) -> namesIn ist sc `dropAll` [n]

429− _ -> []) \\ [n]

454+ _ -> [])

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

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

456+ put (PExp ty : decls,

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

457+ nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

432 imps True (n:env) sc

458 imps True (n:env) sc

459+ imps top env (PEq _ l r)

460+ = do (decls, ns) <- get

461+ let isn = namesIn ist l ++ namesIn ist r

462+ put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

433 imps top env (PPair _ l r)

463 imps top env (PPair _ l r)

434 = do (decls, ns) <- get

464 = do (decls, ns) <- get

435 let isn = namesIn ist l ++ namesIn ist r

465 let isn = namesIn ist l ++ namesIn ist r

436− put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

466+ put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

437 imps top env (PDPair _ (PRef _ n) r)

467 imps top env (PDPair _ (PRef _ n) r)

438 = do (decls, ns) <- get

468 = do (decls, ns) <- get

439− let isn = namesIn ist r \\ [n]

469+ let isn = nub (namesIn ist r) \\ [n]

440 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

470 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

441 imps top env (PDPair _ l r)

471 imps top env (PDPair _ l r)

442 = do (decls, ns) <- get

472 = do (decls, ns) <- get

@@ -459,6 +489,9 @@ addImpl :: IState -> PTerm -> PTerm

459addImpl ist ptm = ai [] ptm

489addImpl ist ptm = ai [] ptm

460 where

490 where

461 ai env (PRef fc f) = aiFn fc env (PRef fc f) []

491 ai env (PRef fc f) = aiFn fc env (PRef fc f) []

492+ ai env (PEq fc l r) = let l' = ai env l

493+ r' = ai env r in

494+ PEq fc l' r'

462 ai env (PPair fc l r) = let l' = ai env l

495 ai env (PPair fc l r) = let l' = ai env l

463 r' = ai env r in

496 r' = ai env r in

464 PPair fc l' r'

497 PPair fc l' r'

@@ -542,12 +575,16 @@ matchClause x y = match x y where

542 match (PRef _ n) (PRef _ n') | n == n' = return []

575 match (PRef _ n) (PRef _ n') | n == n' = return []

543 | otherwise = Nothing

576 | otherwise = Nothing

544 match (PRef _ n) tm = return [(n, tm)]

577 match (PRef _ n) tm = return [(n, tm)]

578+ match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'

579+ mr <- match r r'

580+ return (ml ++ mr)

545 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'

581 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'

546 mr <- match r r'

582 mr <- match r r'

547 return (ml ++ mr)

583 return (ml ++ mr)

548 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'

584 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'

549 mr <- match r r'

585 mr <- match r r'

550 return (ml ++ mr)

586 return (ml ++ mr)

587+ match (PRefl _) (PRefl _) = return []

551 match (PTrue _) (PTrue _) = return []

588 match (PTrue _) (PTrue _) = return []

552 match (PFalse _) (PFalse _) = return []

589 match (PFalse _) (PFalse _) = return []

553 match (PReturn _) (PReturn _) = return []

590 match (PReturn _) (PReturn _) = return []

@@ -571,6 +608,7 @@ substMatch n tm t = sm t where

571 sm (PLam x t sc) = PLam x (sm t) (sm sc)

608 sm (PLam x t sc) = PLam x (sm t) (sm sc)

572 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

609 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

573 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

610 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

611+ sm (PEq f x y) = PEq f (sm x) (sm y)

574 sm (PPair f x y) = PPair f (sm x) (sm y)

612 sm (PPair f x y) = PPair f (sm x) (sm y)

575 sm (PDPair f x y) = PDPair f (sm x) (sm y)

613 sm (PDPair f x y) = PDPair f (sm x) (sm y)

576 sm (PHidden x) = PHidden (sm x)

614 sm (PHidden x) = PHidden (sm x)

src/Idris/Delaborate.hs+2

@@ -32,7 +32,9 @@ delab ist tm = de [] tm

33 deFn env (App f a) args = deFn env f (a:args)

34 deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)

35+ | n == eqCon = PRefl un

35 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

36 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

37+ | n == eqTy = PEq un (de env l) (de env r)

36 deFn env (P _ n _) args = mkPApp n (map (de env) args)

38 deFn env (P _ n _) args = mkPApp n (map (de env) args)

37 deFn env f args = PApp un (de env f) (map PExp (map (de env) args))

39 deFn env f args = PApp un (de env f) (map PExp (map (de env) args))

src/Idris/ElabDecls.hs+5

@@ -307,6 +307,11 @@ elab info pattern tm = do elab' tm

307 elab' (PTrue fc) = try (elab' (PRef fc unitCon))

308 (elab' (PRef fc unitTy))

309 elab' (PFalse fc) = elab' (PRef fc falseTy)

310+ elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [PImp (MN 0 "a") Placeholder,

311+ PImp (MN 0 "x") Placeholder])

312+ elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [PImp (MN 0 "a") Placeholder,

313+ PImp (MN 0 "b") Placeholder,

314+ PExp l, PExp r])

310 elab' (PPair fc l r) = try (elab' (PApp fc (PRef fc pairTy)

315 elab' (PPair fc l r) = try (elab' (PApp fc (PRef fc pairTy)

311 [PExp l,PExp r]))

316 [PExp l,PExp r]))

312 (elab' (PApp fc (PRef fc pairCon)

317 (elab' (PApp fc (PRef fc pairCon)

src/Idris/Parser.hs+2−1

@@ -322,6 +322,7 @@ pSimpleExpr syn =

322 try (do symbol "!["; t <- pTerm; lchar ']'

323 return $ PQuote t)

324 <|> try (do lchar '?'; x <- pName; return (PMetavar x))

325+ <|> try (do fc <- pfc; reserved "refl"; return (PRefl fc))

325 <|> try (do fc <- pfc; reserved "return"; return (PReturn fc))

326 <|> try (do fc <- pfc; reserved "return"; return (PReturn fc))

326 <|> try (do fc <- pfc; x <- pfName; return (PRef fc x))

327 <|> try (do fc <- pfc; x <- pfName; return (PRef fc x))

327 <|> try (do lchar '('; l <- pExpr syn; lchar ','; fc <- pfc

328 <|> try (do lchar '('; l <- pExpr syn; lchar ','; fc <- pfc

@@ -421,7 +422,7 @@ pConstant = do reserved "Int"; return IType

421table fixes

422table fixes

422 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]

423 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]

423 ++ toTable (reverse fixes) ++

424 ++ toTable (reverse fixes) ++

424− [[binary "=" (\fc x y -> PApp fc (PRef fc (UN ["="])) [PExp x,PExp y]) AssocLeft],

425+ [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],

425 [binary "->" (\fc x y -> PPi Exp (MN 0 "X") x y) AssocRight]]

426 [binary "->" (\fc x y -> PPi Exp (MN 0 "X") x y) AssocRight]]

426

427

427toTable fs = map (map toBin)

428toTable fs = map (map toBin)

src/Idris/Primitives.hs+1−1

@@ -95,6 +95,6 @@ elabPrim (Prim n ty i def epic)

95elabPrims :: Idris ()

96elabPrims = do mapM_ (elabDecl toplevel)

97 (map (PData (FC "builtin" 0))

98− [inferDecl, unitDecl, falseDecl, pairDecl])

98+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

99 mapM_ elabPrim primitives

100