39b934c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Sugar for dependent pairs

39b934cEdwin Brady15 years ago

Makefile+5

compare with master

unifiedsplit

@@ -2,6 +2,11 @@ install: .PHONY

2 cabal install

3 make -C lib check

5+pinstall: .PHONY

6+ cabal configure --enable-executable-profiling

7+ cabal install --enable-executable-profiling

8+ make -C lib check

5build: .PHONY

10build: .PHONY

6 cabal build

11 cabal build

src/Core/CoreParser.hs+1−1

@@ -17,7 +17,7 @@ type TokenParser a = PTok.TokenParser a

17idrisDef = haskellDef {

18 opStart = iOpStart,

19 opLetter = iOpLetter,

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

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

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

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

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

src/Idris/AbsSyntax.hs+23−3

@@ -178,6 +178,7 @@ data PTerm = PQuote Raw

178 | PTrue FC

179 | PFalse FC

180 | PPair FC PTerm PTerm

181+ | PDPair FC PTerm PTerm

181 | PHidden PTerm -- irrelevant or hidden pattern

182 | PHidden PTerm -- irrelevant or hidden pattern

182 | PSet

183 | PSet

183 | PConstant Const

184 | PConstant Const

@@ -302,6 +303,7 @@ showImp impl tm = se 10 tm where

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

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

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

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

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

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

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

305 se p PSet = "Set"

307 se p PSet = "Set"

306 se p (PConstant c) = show c

308 se p (PConstant c) = show c

307 se p (PMetavar n) = "?" ++ show n

309 se p (PMetavar n) = "?" ++ show n

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

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

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

324 ni env (PHidden tm) = ni env tm

326 ni env (PHidden tm) = ni env tm

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

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

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

326 ni env _ = []

329 ni env _ = []

327

330

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

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

@@ -337,6 +340,7 @@ namesIn ist tm = nub $ ni [] tm

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

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

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

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

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

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

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

340 ni env (PHidden tm) = ni env tm

344 ni env (PHidden tm) = ni env tm

341 ni env _ = []

345 ni env _ = []

342

346

@@ -374,8 +378,8 @@ unitDecl = PDatadecl unitTy PSet

374falseTy = MN 0 "__False"

378falseTy = MN 0 "__False"

375falseDecl = PDatadecl falseTy PSet []

379falseDecl = PDatadecl falseTy PSet []

376

380

377−pairTy = UN ["Pair"] -- MN 0 "__Pair"

381+pairTy = MN 0 "__Pair"

378−pairCon = UN ["MkPair"] -- MN 0 "__MkPair"

382+pairCon = MN 0 "__MkPair"

379pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

383pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

380 [(pairCon, PPi Imp (n "A") PSet (

384 [(pairCon, PPi Imp (n "A") PSet (

381 PPi Imp (n "B") PSet (

385 PPi Imp (n "B") PSet (

@@ -385,6 +389,10 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

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

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

386 where n a = MN 0 a

390 where n a = MN 0 a

387

391

392+-- Defined in builtins.idr

393+sigmaTy = UN ["Sigma"]

394+existsCon = UN ["Exists"]

395+

388piBind :: [(Name, PTerm)] -> PTerm -> PTerm

396piBind :: [(Name, PTerm)] -> PTerm -> PTerm

389piBind [] t = t

397piBind [] t = t

390piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)

398piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)

@@ -422,7 +430,16 @@ implicitise syn ist tm

422 imps True (n:env) sc

430 imps True (n:env) sc

423 imps top env (PPair _ l r)

431 imps top env (PPair _ l r)

424 = do (decls, ns) <- get

432 = do (decls, ns) <- get

425− put (decls, nub (ns ++ namesIn ist l ++ namesIn ist r))

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

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

435+ imps top env (PDPair _ (PRef _ n) r)

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

437+ let isn = namesIn ist r \\ [n]

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

439+ imps top env (PDPair _ l r)

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

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

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

426 imps top env (PLam n ty sc)

443 imps top env (PLam n ty sc)

427 = do imps False env ty

444 = do imps False env ty

428 imps False (n:env) sc

445 imps False (n:env) sc

@@ -443,6 +460,9 @@ addImpl ist ptm = ai [] ptm

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

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

444 r' = ai env r in

461 r' = ai env r in

445 PPair fc l' r'

462 PPair fc l' r'

463+ ai env (PDPair fc l r) = let l' = ai env l

464+ r' = ai env r in

465+ PDPair fc l' r'

446 ai env (PApp fc (PRef _ f) as)

466 ai env (PApp fc (PRef _ f) as)

447 = let as' = map (fmap (ai env)) as in

467 = let as' = map (fmap (ai env)) as in

448 aiFn fc env (PRef fc f) as'

468 aiFn fc env (PRef fc f) as'

src/Idris/ElabDecls.hs+12

@@ -306,6 +306,18 @@ elab info pattern tm = do elab' tm

306 [PImp (MN 0 "A") Placeholder,

307 PImp (MN 0 "B") Placeholder,

308 PExp l, PExp r]))

309+ elab' (PDPair fc l@(PRef _ n) r)

310+ = try (elab' (PApp fc (PRef fc sigmaTy)

311+ [PExp Placeholder,

312+ PExp (PLam n Placeholder r)]))

313+ (elab' (PApp fc (PRef fc existsCon)

314+ [PImp (MN 0 "a") Placeholder,

315+ PImp (MN 0 "P") Placeholder,

316+ PExp l, PExp r]))

317+ elab' (PDPair fc l r) = elab' (PApp fc (PRef fc existsCon)

318+ [PImp (MN 0 "a") Placeholder,

319+ PImp (MN 0 "P") Placeholder,

320+ PExp l, PExp r])

309 elab' (PRef fc n) | pattern && not (inparamBlock n)

321 elab' (PRef fc n) | pattern && not (inparamBlock n)

310 = erun fc $

322 = erun fc $

311 try (do apply (Var n) []; solve)

323 try (do apply (Var n) []; solve)

src/Idris/Parser.hs+6−1

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

299 (update (dropn n ns) sc)

300 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

301 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

302+ update ns (PDPair fc l r) = PDPair fc (update ns l) (update ns r)

302 update ns (PHidden t) = PHidden (update ns t)

303 update ns (PHidden t) = PHidden (update ns t)

303 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

304 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

304 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds

305 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds

@@ -326,6 +327,9 @@ pSimpleExpr syn =

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

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

327 r <- pExpr syn; lchar ')';

328 r <- pExpr syn; lchar ')';

328 return (PPair fc l r))

329 return (PPair fc l r))

330+ <|> try (do lchar '('; l <- pExpr syn; reservedOp "**"; fc <- pfc

331+ r <- pExpr syn; lchar ')';

332+ return (PDPair fc l r))

329 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

333 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

330 <|> try (do c <- pConstant; return (PConstant c))

334 <|> try (do c <- pConstant; return (PConstant c))

331 <|> try (do reserved "Set"; return PSet)

335 <|> try (do reserved "Set"; return PSet)

@@ -513,7 +517,7 @@ pClause syn

513 args <- many (pHSimpleExpr syn)

517 args <- many (pHSimpleExpr syn)

514 wargs <- many (pWExpr syn)

518 wargs <- many (pWExpr syn)

515 reserved "with"

519 reserved "with"

516− wval <- pSimpleExpr syn

520+ wval <- pExpr' syn

517 lchar '{'

521 lchar '{'

518 ds <- many1 $ pFunDecl syn

522 ds <- many1 $ pFunDecl syn

519 let withs = concat ds

523 let withs = concat ds

@@ -573,6 +577,7 @@ expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

573expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

577expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

574 (map (fmap (expandDo dsl)) args)

578 (map (fmap (expandDo dsl)) args)

575expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

579expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

580+expandDo dsl (PDPair fc l r) = PDPair fc (expandDo dsl l) (expandDo dsl r)

576expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

581expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

577expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)

582expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)

578expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

583expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds