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

git.iko.soy/Idris-dev

Added = and refl

commit95a558b78c6ba549e5b43245b37ce0dec643e99c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 25 Oct 2011, 16:04 (15 years ago) parent5fbca2a

7 files changed+67−14

compare with master

unifiedsplit

lib/nat.idr+7 src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntax.hs+49−11 src/Idris/Delaborate.hs+2 src/Idris/ElabDecls.hs+5 src/Idris/Parser.hs+2−1 src/Idris/Primitives.hs+1−1

lib/nat.idr+7

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

55plus O y = y;

66plus (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 {

1919 opLetter = iOpLetter,

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

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

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

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

2323 "infix", "infixl", "infixr", "prefix",

2424 "where", "with", "forall", "syntax",

2525 "using", "params", "namespace",

src/Idris/AbsSyntax.hs+49−11

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

177177 | PApp FC PTerm [PArg]

178178 | PTrue FC

179179 | PFalse FC

180+ | PRefl FC

181+ | PEq FC PTerm PTerm

180182 | PPair FC PTerm PTerm

181183 | PDPair FC PTerm PTerm

182184 | PHidden PTerm -- irrelevant or hidden pattern

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

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

303305 ++ concatMap seArg args

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

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

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

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

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

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

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

309313 se p PSet = "Set"

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

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

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

328332 ni env (PHidden tm) = ni env tm

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

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

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

331336 ni env _ = []

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

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

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

343348 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

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

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

346352 ni env (PHidden tm) = ni env tm

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

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

370376getInferType (App (App _ ty) _) = ty

371377

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

373−

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

374379

375380unitTy = MN 0 "__Unit"

376381unitCon = MN 0 "__II"

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

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

392397 where n a = MN 0 a

393398

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+

394412-- Defined in builtins.idr

395413sigmaTy = UN ["Sigma"]

396414existsCon = UN ["Exists"]

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

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

405423-- argument position.

406424

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

426+

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

408428implicitise syn ist tm

409429 = let uvars = using syn

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

414434 then (tm, reverse declimps)

415435 else implicitise syn ist (pibind uvars ns tm)

416436 where

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

438+ | otherwise = x : dropAll xs ys

439+ dropAll [] ys = []

440+

417441 imps top env (PApp _ f as)

418442 = do (decls, ns) <- get

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

421445 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]

423447 (decls , ns) <- get

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

448+ put (PImp n ty : decls,

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

425450 imps True (n:env) sc

426451 imps top env (PPi Exp n ty sc)

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

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

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

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

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

454+ _ -> [])

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

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

456+ put (PExp ty : decls,

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

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

433463 imps top env (PPair _ l r)

434464 = do (decls, ns) <- get

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

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

438468 = do (decls, ns) <- get

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

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

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

441471 imps top env (PDPair _ l r)

442472 = do (decls, ns) <- get

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

459489addImpl ist ptm = ai [] ptm

460490 where

461491 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'

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

463496 r' = ai env r in

464497 PPair fc l' r'

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

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

543576 | otherwise = Nothing

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

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

546582 mr <- match r r'

547583 return (ml ++ mr)

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

549585 mr <- match r r'

550586 return (ml ++ mr)

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

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

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

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

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

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

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

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

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

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

576614 sm (PHidden x) = PHidden (sm x)

src/Idris/Delaborate.hs+2

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

3232

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

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

35+ | n == eqCon = PRefl un

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

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

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

3840

src/Idris/ElabDecls.hs+5

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

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

308308 (elab' (PRef fc unitTy))

309309 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])

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

311316 [PExp l,PExp r]))

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

src/Idris/Parser.hs+2−1

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

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

323323 return $ PQuote t)

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

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

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

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

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

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

421422table fixes

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

423424 ++ 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],

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

426427

427428toTable fs = map (map toBin)

src/Idris/Primitives.hs+1−1

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

9595elabPrims :: Idris ()

9696elabPrims = do mapM_ (elabDecl toplevel)

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

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

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

9999 mapM_ elabPrim primitives

100100