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

git.iko.soy/Idris-dev

Sugar for dependent pairs

commit39b934cfab75d64e8c2b235c60b5c9350662de50 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 25 Oct 2011, 12:46 (15 years ago) parent5e92c70

5 files changed+47−5

compare with master

unifiedsplit

Makefile+5 src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntax.hs+23−3 src/Idris/ElabDecls.hs+12 src/Idris/Parser.hs+6−1

Makefile+5

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

22 cabal install

33 make -C lib check

5+pinstall: .PHONY

6+ cabal configure --enable-executable-profiling

7+ cabal install --enable-executable-profiling

8+ make -C lib check

510build: .PHONY

611 cabal build

712

src/Core/CoreParser.hs+1−1

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

1717idrisDef = haskellDef {

1818 opStart = iOpStart,

1919 opLetter = iOpLetter,

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

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

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

2222 "do", "dsl", "import",

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

src/Idris/AbsSyntax.hs+23−3

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

178178 | PTrue FC

179179 | PFalse FC

180180 | PPair FC PTerm PTerm

181+ | PDPair FC PTerm PTerm

181182 | PHidden PTerm -- irrelevant or hidden pattern

182183 | PSet

183184 | PConstant Const

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

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

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

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

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

305307 se p PSet = "Set"

306308 se p (PConstant c) = show c

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

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

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

324326 ni env (PHidden tm) = ni env tm

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

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

326329 ni env _ = []

327330

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

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

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

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

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

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

340344 ni env (PHidden tm) = ni env tm

341345 ni env _ = []

342346

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

374378falseTy = MN 0 "__False"

375379falseDecl = PDatadecl falseTy PSet []

376380

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

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

381+pairTy = MN 0 "__Pair"

382+pairCon = MN 0 "__MkPair"

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

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

381385 PPi Imp (n "B") PSet (

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

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

386390 where n a = MN 0 a

387391

392+-- Defined in builtins.idr

393+sigmaTy = UN ["Sigma"]

394+existsCon = UN ["Exists"]

395+

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

389397piBind [] t = t

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

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

422430 imps True (n:env) sc

423431 imps top env (PPair _ l r)

424432 = 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)))))

426443 imps top env (PLam n ty sc)

427444 = do imps False env ty

428445 imps False (n:env) sc

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

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

444461 r' = ai env r in

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

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

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

448468 aiFn fc env (PRef fc f) as'

src/Idris/ElabDecls.hs+12

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

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

307307 PImp (MN 0 "B") Placeholder,

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

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

310322 = erun fc $

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

src/Idris/Parser.hs+6−1

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

299299 (update (dropn n ns) sc)

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

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

302303 update ns (PHidden t) = PHidden (update ns t)

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

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

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

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

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

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

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

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

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

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

513517 args <- many (pHSimpleExpr syn)

514518 wargs <- many (pWExpr syn)

515519 reserved "with"

516− wval <- pSimpleExpr syn

520+ wval <- pExpr' syn

517521 lchar '{'

518522 ds <- many1 $ pFunDecl syn

519523 let withs = concat ds

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

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

574578 (map (fmap (expandDo dsl)) args)

575579expandDo 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)

576581expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

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

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