1155e79 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Laziness annotations

1155e79Edwin Brady15 years ago

lib/builtins.idr+4−1

compare with master

unifiedsplit

@@ -7,6 +7,9 @@ getSigIdx (Exists a v) = a;

7getSigVal : {P : a -> Set} -> (s : Sigma a P) -> P (getSigIdx s);

8getSigVal (Exists a v) = v;

10+lazy : a -> a;

11+lazy x = x; -- compiled specially

12+

10id : a -> a;

13id : a -> a;

11id x = x;

14id x = x;

@@ -28,7 +31,7 @@ f $ a = f a;

29data Bool = False | True;

32data Bool = False | True;

31−boolElim : (x:Bool) -> a -> a -> a;

34+boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;

32boolElim True t e = t;

35boolElim True t e = t;

33boolElim False t e = e;

36boolElim False t e = e;

src/Idris/AbsSyntax.hs+50−39

@@ -33,11 +33,12 @@ data IState = IState { tt_ctxt :: Context,

33 idris_name :: Int,

34 idris_metavars :: [Name],

35 syntax_rules :: [Syntax],

36+ syntax_keywords :: [String],

36 imported :: [FilePath],

37 imported :: [FilePath],

37 idris_prims :: [(Name, ([E.Name], E.Term))]

38 idris_prims :: [(Name, ([E.Name], E.Term))]

38 }

39 }

40−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 6 [] [] [] []

41+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 6 [] [] [] [] []

42-- The monad for the main REPL - reading and processing files and updating

43-- The monad for the main REPL - reading and processing files and updating

43-- global state (hence the IO inner monad).

44-- global state (hence the IO inner monad).

@@ -139,7 +140,11 @@ data FixDecl = Fix Fixity String

139instance Ord FixDecl where

140instance Ord FixDecl where

140 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)

141 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)

141

142

143+-- Mark bindings with their explicitness, and laziness

142−data Plicity = Imp | Exp deriving (Show, Eq)

144+data Plicity = Imp Bool | Exp Bool deriving (Show, Eq)

145+

146+impl = Imp False

147+expl = Exp False

143

148

144data PDecl' t = PFix FC Fixity [String] -- fixity declaration

149data PDecl' t = PFix FC Fixity [String] -- fixity declaration

145 | PTy FC Name t -- type declaration

150 | PTy FC Name t -- type declaration

@@ -205,10 +210,13 @@ data PDo = DoExp FC PTerm

205 | DoLet FC Name PTerm

210 | DoLet FC Name PTerm

206 deriving Eq

211 deriving Eq

207

212

208−data PArg' t = PImp { pname :: Name, getTm :: t }

213+data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }

209− | PExp { getTm :: t }

214+ | PExp { lazyarg :: Bool, getTm :: t }

210 deriving (Show, Eq, Functor)

215 deriving (Show, Eq, Functor)

211

216

217+pimp = PImp False

218+pexp = PExp False

219+

212type PArg = PArg' PTerm

220type PArg = PArg' PTerm

213

221

214-- Syntactic sugar info (TODO: namespaces, modules)

222-- Syntactic sugar info (TODO: namespaces, modules)

@@ -275,12 +283,12 @@ showDImp impl (PDatadecl n ty cons)

275

283

276getImps :: [PArg] -> [(Name, PTerm)]

284getImps :: [PArg] -> [(Name, PTerm)]

277getImps [] = []

285getImps [] = []

278−getImps (PImp n tm : xs) = (n, tm) : getImps xs

286+getImps (PImp _ n tm : xs) = (n, tm) : getImps xs

279getImps (_ : xs) = getImps xs

287getImps (_ : xs) = getImps xs

280

288

281getExps :: [PArg] -> [PTerm]

289getExps :: [PArg] -> [PTerm]

282getExps [] = []

290getExps [] = []

283−getExps (PExp tm : xs) = tm : getExps xs

291+getExps (PExp _ tm : xs) = tm : getExps xs

284getExps (_ : xs) = getExps xs

292getExps (_ : xs) = getExps xs

285

293

286getAll :: [PArg] -> [PTerm]

294getAll :: [PArg] -> [PTerm]

@@ -293,13 +301,15 @@ showImp impl tm = se 10 tm where

293 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc

301 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc

294 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

302 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

295 " in " ++ se 10 sc

303 " in " ++ se 10 sc

296− se p (PPi Exp n ty sc)

304+ se p (PPi (Exp l) n ty sc)

297 | n `elem` allNamesIn sc = bracket p 2 $

305 | n `elem` allNamesIn sc = bracket p 2 $

306+ if l then "|(" else "(" ++

298− "(" ++ show n ++ " : " ++ se 10 ty ++

307+ show n ++ " : " ++ se 10 ty ++

299 ") -> " ++ se 10 sc

308 ") -> " ++ se 10 sc

300 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc

309 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc

301− se p (PPi Imp n ty sc)

310+ se p (PPi (Imp l) n ty sc)

311+ | impl = bracket p 2 $ if l then "|{" else "{" ++

302− | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++

312+ show n ++ " : " ++ se 10 ty ++

303 "} -> " ++ se 10 sc

313 "} -> " ++ se 10 sc

304 | otherwise = se 10 sc

314 | otherwise = se 10 sc

305 se p (PApp _ (PRef _ f) [])

315 se p (PApp _ (PRef _ f) [])

@@ -369,11 +379,11 @@ inferTy = MN 0 "__Infer"

369inferCon = MN 0 "__infer"

379inferCon = MN 0 "__infer"

370inferDecl = PDatadecl inferTy

380inferDecl = PDatadecl inferTy

371 PSet

381 PSet

372− [(inferCon, PPi Imp (MN 0 "A") PSet (

382+ [(inferCon, PPi impl (MN 0 "A") PSet (

373− PPi Exp (MN 0 "a") (PRef bi (MN 0 "A"))

383+ PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

374 (PRef bi inferTy)), bi)]

384 (PRef bi inferTy)), bi)]

375

385

376−infTerm t = PApp bi (PRef bi inferCon) [PImp (MN 0 "A") Placeholder, PExp t]

386+infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]

377infP = P (TCon 6 0) inferTy (Set 0)

387infP = P (TCon 6 0) inferTy (Set 0)

378

388

379getInferTerm, getInferType :: Term -> Term

389getInferTerm, getInferType :: Term -> Term

@@ -397,12 +407,12 @@ falseDecl = PDatadecl falseTy PSet []

397pairTy = MN 0 "__Pair"

407pairTy = MN 0 "__Pair"

398pairCon = MN 0 "__MkPair"

408pairCon = MN 0 "__MkPair"

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

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

400− [(pairCon, PPi Imp (n "A") PSet (

410+ [(pairCon, PPi impl (n "A") PSet (

401− PPi Imp (n "B") PSet (

411+ PPi impl (n "B") PSet (

402− PPi Exp (n "a") (PRef bi (n "A")) (

412+ PPi expl (n "a") (PRef bi (n "A")) (

403− PPi Exp (n "b") (PRef bi (n "B"))

413+ PPi expl (n "b") (PRef bi (n "B"))

404− (PApp bi (PRef bi pairTy) [PExp (PRef bi (n "A")),

414+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

405− PExp (PRef bi (n "B"))])))), bi)]

415+ pexp (PRef bi (n "B"))])))), bi)]

406 where n a = MN 0 a

416 where n a = MN 0 a

407

417

408eqTy = UN ["="]

418eqTy = UN ["="]

@@ -410,12 +420,12 @@ eqCon = UN ["refl"]

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

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

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

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

412 PSet)

422 PSet)

413− [(eqCon, PPi Imp (n "a") PSet (

423+ [(eqCon, PPi impl (n "a") PSet (

414− PPi Imp (n "x") (PRef bi (n "a"))

424+ PPi impl (n "x") (PRef bi (n "a"))

415− (PApp bi (PRef bi eqTy) [PImp (n "a") Placeholder,

425+ (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,

416− PImp (n "b") Placeholder,

426+ pimp (n "b") Placeholder,

417− PExp (PRef bi (n "x")),

427+ pexp (PRef bi (n "x")),

418− PExp (PRef bi (n "x"))])), bi)]

428+ pexp (PRef bi (n "x"))])), bi)]

419 where n a = MN 0 a

429 where n a = MN 0 a

420

430

421-- Defined in builtins.idr

431-- Defined in builtins.idr

@@ -424,7 +434,7 @@ existsCon = UN ["Exists"]

424

434

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

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

426piBind [] t = t

436piBind [] t = t

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

437+piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)

428

438

429-- Dealing with implicit arguments

439-- Dealing with implicit arguments

430

440

@@ -451,18 +461,18 @@ implicitise syn ist tm

451 = do (decls, ns) <- get

461 = do (decls, ns) <- get

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

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

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

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

454− imps top env (PPi Imp n ty sc)

464+ imps top env (PPi (Imp l) n ty sc)

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

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

456 (decls , ns) <- get

466 (decls , ns) <- get

457− put (PImp n ty : decls,

467+ put (PImp l n ty : decls,

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

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

459 imps True (n:env) sc

469 imps True (n:env) sc

460− imps top env (PPi Exp n ty sc)

470+ imps top env (PPi (Exp l) n ty sc)

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

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

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

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

463 _ -> [])

473 _ -> [])

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

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

465− put (PExp ty : decls,

475+ put (PExp l ty : decls,

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

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

467 imps True (n:env) sc

477 imps True (n:env) sc

468 imps top env (PEq _ l r)

478 imps top env (PEq _ l r)

@@ -488,9 +498,10 @@ implicitise syn ist tm

488 imps top env _ = return ()

498 imps top env _ = return ()

489

499

490 pibind using [] sc = sc

500 pibind using [] sc = sc

501+ pibind using (n:ns) sc

491− pibind using (n:ns) sc = case lookup n using of

502+ = case lookup n using of

492− Just ty -> PPi Imp n ty (pibind using ns sc)

503+ Just ty -> PPi (Imp False) n ty (pibind using ns sc)

493− Nothing -> PPi Imp n Placeholder (pibind using ns sc)

504+ Nothing -> PPi (Imp False) n Placeholder (pibind using ns sc)

494

505

495-- Add implicit arguments in function calls

506-- Add implicit arguments in function calls

496

507

@@ -541,17 +552,17 @@ addImpl ist ptm = ai [] ptm

541 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as

552 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as

542

553

543 insertImpl :: [PArg] -> [PArg] -> [PArg]

554 insertImpl :: [PArg] -> [PArg] -> [PArg]

544− insertImpl (PExp ty : ps) (PExp tm : given) =

555+ insertImpl (PExp l ty : ps) (PExp _ tm : given) =

545− PExp tm : insertImpl ps given

556+ PExp l tm : insertImpl ps given

546− insertImpl (PImp n ty : ps) given =

557+ insertImpl (PImp l n ty : ps) given =

547 case find n given [] of

558 case find n given [] of

548− Just (tm, given') -> PImp n tm : insertImpl ps given'

559+ Just (tm, given') -> PImp l n tm : insertImpl ps given'

549− Nothing -> PImp n Placeholder : insertImpl ps given

560+ Nothing -> PImp l n Placeholder : insertImpl ps given

550 insertImpl expected [] = []

561 insertImpl expected [] = []

551 insertImpl [] given = given

562 insertImpl [] given = given

552

563

553 find n [] acc = Nothing

564 find n [] acc = Nothing

554− find n (PImp n' t : gs) acc

565+ find n (PImp _ n' t : gs) acc

555 | n == n' = Just (t, reverse acc ++ gs)

566 | n == n' = Just (t, reverse acc ++ gs)

556 find n (g : gs) acc = find n gs (g : acc)

567 find n (g : gs) acc = find n gs (g : acc)

557

568

src/Idris/Compiler.hs+3

@@ -51,6 +51,9 @@ instance ToEpic (TT Name) where

51 epic' env tm@(App f a)

52 | (P _ (UN ["mkForeign"]) _, args) <- unApply tm

53 = doForeign args

54+ | (P _ (UN ["lazy"]) _, [_, arg]) <- unApply tm

55+ = do arg' <- epic' env arg

56+ return $ lazy_ arg'

54 epic' env (P (DCon t a) n _) = return $ con_ t

57 epic' env (P (DCon t a) n _) = return $ con_ t

55 epic' env (P (TCon t a) n _) = return $ con_ t

58 epic' env (P (TCon t a) n _) = return $ con_ t

56 epic' env (P _ n _) = return $ ref (ename n)

59 epic' env (P _ n _) = return $ ref (ename n)

src/Idris/Delaborate.hs+6−6

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

23 | n == falseTy = PFalse un

24 | otherwise = PRef un n

25 de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de (n:env) sc)

26− de env (Bind n (Pi ty) sc) = PPi Exp n (de env ty) (de (n:env) sc)

26+ de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de (n:env) sc)

27 de env (Bind n (Let ty val) sc)

28 = PLet n (de env ty) (de env val) (de (n:env) sc)

29 de env (Bind n _ sc) = de (n:env) sc

@@ -36,13 +36,13 @@ delab ist tm = de [] tm

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)

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

39− 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))

41 mkPApp n args

42 | Just imps <- lookupCtxt n (idris_implicits ist)

43− = PApp un (PRef un n) (zipWith imp (imps ++ repeat (PExp undefined)) args)

43+ = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

44− | otherwise = PApp un (PRef un n) (map PExp args)

44+ | otherwise = PApp un (PRef un n) (map pexp args)

46− imp (PImp n _) arg = PImp n arg

46+ imp (PImp l n _) arg = PImp l n arg

47− imp (PExp _) arg = PExp arg

47+ imp (PExp l _) arg = PExp l arg

src/Idris/ElabDecls.hs+32−24

@@ -188,8 +188,8 @@ elabClause info fc (PWith fname lhs withs wval withblock)

188 mapM_ (elabDecl info) wb

189

190 -- rhs becomes: fname' ps wval

191− let rhs = PApp fc (PRef fc wname) (map (PExp . (PRef fc) . fst) bargs ++

191+ let rhs = PApp fc (PRef fc wname) (map (pexp . (PRef fc) . fst) bargs ++

192− [PExp wval])

192+ [pexp wval])

193 logLvl 3 ("New RHS " ++ show rhs)

194 ctxt <- getContext -- New context with block added

195 ((rhs', defer), _) <-

@@ -225,7 +225,7 @@ elabClause info fc (PWith fname lhs withs wval withblock)

225

226 updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w

227 = return $ substMatches mvars $

228− PApp fc (PRef fc' wname) (map (PExp . (PRef fc')) ns ++ [PExp w])

228+ PApp fc (PRef fc' wname) (map (pexp . (PRef fc')) ns ++ [pexp w])

229 updateLHS n wname mvars ns tm w = fail $ "Not implemented " ++ show tm

230

231pbinds (Bind n (PVar t) sc) = do attack; patbind n

@@ -310,29 +310,29 @@ elab info pattern tm = do elab' tm

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

311 (elab' (PRef fc unitTy))

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

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

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

314− PImp (MN 0 "x") Placeholder])

314+ pimp (MN 0 "x") Placeholder])

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

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

316− PImp (MN 0 "b") Placeholder,

316+ pimp (MN 0 "b") Placeholder,

317− PExp l, PExp r])

317+ pexp l, pexp r])

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

319− [PExp l,PExp r]))

319+ [pexp l,pexp r]))

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

321− [PImp (MN 0 "A") Placeholder,

321+ [pimp (MN 0 "A") Placeholder,

322− PImp (MN 0 "B") Placeholder,

322+ pimp (MN 0 "B") Placeholder,

323− PExp l, PExp r]))

323+ pexp l, pexp r]))

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

325 = try (elab' (PApp fc (PRef fc sigmaTy)

326− [PExp Placeholder,

326+ [pexp Placeholder,

327− PExp (PLam n Placeholder r)]))

327+ pexp (PLam n Placeholder r)]))

328 (elab' (PApp fc (PRef fc existsCon)

329− [PImp (MN 0 "a") Placeholder,

329+ [pimp (MN 0 "a") Placeholder,

330− PImp (MN 0 "P") Placeholder,

330+ pimp (MN 0 "P") Placeholder,

331− PExp l, PExp r]))

331+ pexp l, pexp r]))

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

333− [PImp (MN 0 "a") Placeholder,

333+ [pimp (MN 0 "a") Placeholder,

334− PImp (MN 0 "P") Placeholder,

334+ pimp (MN 0 "P") Placeholder,

335− PExp l, PExp r])

335+ pexp l, pexp r])

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

337 = erun fc $

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

@@ -372,12 +372,12 @@ elab info pattern tm = do elab' tm

372 elab' (PApp fc (PRef _ f) args)

373 | Just ps <- lookupCtxt f (inblock info)

374 = erun fc $

375− elabApp (liftname info f) (map (PExp . (PRef fc)) ps ++ args)

375+ elabApp (liftname info f) (map (pexp . (PRef fc)) ps ++ args)

376 | otherwise = erun fc $ elabApp f args

377 where elabApp f args

378 = try (do ns <- apply (Var f) (map isph args)

379 solve

380− elabArgs ns (map getTm args))

380+ elabArgs ns (map (\x -> (lazyarg x, getTm x)) args))

381 (do apply_elab f (map toElab args)

382 solve)

383 elab' (PApp fc f [arg])

@@ -391,8 +391,16 @@ elab info pattern tm = do elab' tm

391 elab' x = fail $ "Not implemented " ++ show x

392

393 elabArgs [] _ = return ()

394− elabArgs (n:ns) (Placeholder : args) = elabArgs ns args

394+ elabArgs (n:ns) ((_, Placeholder) : args) = elabArgs ns args

395− elabArgs (n:ns) (t : args) = do focus n; elab' t; elabArgs ns args

395+ elabArgs (n:ns) ((lazy, t) : args)

396+ | lazy && not pattern

397+ = do focus n; elab' (PApp bi (PRef bi (UN ["lazy"]))

398+ [pimp (UN ["a"]) Placeholder,

399+ pexp t]);

400+ elabArgs ns args

401+ | otherwise

402+ = do focus n; elab' t; elabArgs ns args

403+

396

404

397collectDeferred :: Term -> State [(Name, Type)] Term

405collectDeferred :: Term -> State [(Name, Type)] Term

398collectDeferred (Bind n (GHole t) app) =

406collectDeferred (Bind n (GHole t) app) =

src/Idris/Parser.hs+71−62

@@ -170,9 +170,17 @@ pSyntaxDecl :: SyntaxInfo -> IParser PDecl

170pSyntaxDecl syn

171 = do s <- pSyntaxRule syn

172 i <- getState

173+ let rs = syntax_rules i

174+ let ns = syntax_keywords i

175+ let ks = map show (names s)

173− setState (i { syntax_rules = s : syntax_rules i })

176+ setState (i { syntax_rules = s : rs,

177+ syntax_keywords = ks ++ ns })

174 fc <- pfc

178 fc <- pfc

175 return (PSyntax fc s)

179 return (PSyntax fc s)

180+ where

181+ names (Rule syms _) = mapMaybe ename syms

182+ ename (Keyword n) = Just n

183+ ename _ = Nothing

176

184

177pSyntaxRule :: SyntaxInfo -> IParser Syntax

185pSyntaxRule :: SyntaxInfo -> IParser Syntax

178pSyntaxRule syn

186pSyntaxRule syn

@@ -201,8 +209,8 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

201 return (Symbol sym)

209 return (Symbol sym)

202

210

203pFunDecl' :: SyntaxInfo -> IParser PDecl

211pFunDecl' :: SyntaxInfo -> IParser PDecl

204−pFunDecl' syn = try (do fc <- pfc

205− n <- pfName; ty <- pTSig syn

212+pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

213+ fc <- pfc

206 lchar ';'

214 lchar ';'

207 ty' <- implicit syn n ty

215 ty' <- implicit syn n ty

208 return (PTy fc n ty'))

216 return (PTy fc n ty'))

@@ -268,8 +276,8 @@ pNoExtExpr syn =

268 <|> pSimpleExpr syn

276 <|> pSimpleExpr syn

269 <|> try (pLambda syn)

277 <|> try (pLambda syn)

270 <|> try (pLet syn)

278 <|> try (pLet syn)

271− <|> try (pPi syn)

279+ <|> pPi syn

272− <|> try (pDoBlock syn)

280+ <|> pDoBlock syn

273

281

274pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

282pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

275pExtensions syn rules = choice (map (\x -> try (pExt syn x)) rules)

283pExtensions syn rules = choice (map (\x -> try (pExt syn x)) rules)

@@ -308,12 +316,8 @@ pExt syn (Rule (s:ssym) ptm)

308 update ns t = t

316 update ns t = t

309

317

310pName = do i <- getState

318pName = do i <- getState

311− iName (map show (names (syntax_rules i)))

319+ iName (syntax_keywords i)

312 where

320 where

313− names rs = concatMap namesR rs

314− namesR (Rule syms _) = mapMaybe ename syms

315− ename (Keyword n) = Just n

316− ename _ = Nothing

317

321

318pfName = try pName

322pfName = try pName

319 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

323 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

@@ -322,21 +326,24 @@ pSimpleExpr syn =

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

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

323 return $ PQuote t)

327 return $ PQuote t)

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

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

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

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

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

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

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

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

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

332+ <|> try (pPair syn)

329− r <- pExpr syn; lchar ')';

330− return (PPair fc l r))

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

332− r <- pExpr syn; lchar ')';

333− return (PDPair fc l r))

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

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

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

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

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

335+ <|> do reserved "Set"; return PSet

337− <|> try (do fc <- pfc; symbol "()"; return (PTrue fc))

336+ <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))

338− <|> try (do fc <- pfc; symbol "_|_"; return (PFalse fc))

337+ <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))

339− <|> try (do lchar '_'; return Placeholder)

338+ <|> do lchar '_'; return Placeholder

339+

340+pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp

341+ fc <- pfc

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

343+ return (op fc l r)

344+ where

345+ pairOp = do lchar ','; return PPair

346+ <|> do reservedOp "**"; return PDPair

340

347

341pHSimpleExpr syn

348pHSimpleExpr syn

342 = try (pSimpleExpr syn)

349 = try (pSimpleExpr syn)

@@ -352,13 +359,13 @@ pApp syn = do f <- pSimpleExpr syn

352pArg :: SyntaxInfo -> IParser PArg

359pArg :: SyntaxInfo -> IParser PArg

353pArg syn = pImplicitArg syn

360pArg syn = pImplicitArg syn

354 <|> do e <- pSimpleExpr syn

361 <|> do e <- pSimpleExpr syn

355− return (PExp e)

362+ return (pexp e)

356

363

357pImplicitArg syn = do lchar '{'; n <- pName

364pImplicitArg syn = do lchar '{'; n <- pName

358 fc <- pfc

365 fc <- pfc

359 v <- option (PRef fc n) (do lchar '='; pExpr syn)

366 v <- option (PRef fc n) (do lchar '='; pExpr syn)

360 lchar '}'

367 lchar '}'

361− return (PImp n v)

368+ return (pimp n v)

362

369

363pTSig syn = do lchar ':'

370pTSig syn = do lchar ':'

364 pExpr syn

371 pExpr syn

@@ -373,14 +380,16 @@ pLet syn = do reserved "let"; n <- pName; lchar '='; v <- pExpr syn

373 reserved "in"; sc <- pExpr syn

380 reserved "in"; sc <- pExpr syn

374 return (PLet n Placeholder v sc)

381 return (PLet n Placeholder v sc)

375

382

383+pPi syn = do lazy <- option False (do lchar '|'; return True)

376−pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'

384+ lchar '('; xt <- tyDeclList syn; lchar ')'

377 symbol "->"

385 symbol "->"

378 sc <- pExpr syn

386 sc <- pExpr syn

379− return (bindList (PPi Exp) xt sc)

387+ return (bindList (PPi (Exp lazy)) xt sc)

388+ <|> do lazy <- option False (do lchar '|'; return True)

380− <|> do lchar '{'; xt <- tyDeclList syn; lchar '}'

389+ lchar '{'; xt <- tyDeclList syn; lchar '}'

381 symbol "->"

390 symbol "->"

382 sc <- pExpr syn

391 sc <- pExpr syn

383− return (bindList (PPi Imp) xt sc)

392+ return (bindList (PPi (Imp lazy)) xt sc)

384

393

385tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

394tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

386 (lchar ',')

395 (lchar ',')

@@ -399,14 +408,14 @@ pDoBlock syn

399 return (PDoBlock ds)

408 return (PDoBlock ds)

400

409

401pDo syn

410pDo syn

402− = try (do fc <- pfc

411+ = try (do i <- pName; symbol "<-"; fc <- pfc

403− i <- pName; symbol "<-"; e <- pExpr syn;

412+ e <- pExpr syn;

404 return (DoBind fc i e))

413 return (DoBind fc i e))

405− <|> try (do fc <- pfc

406− reserved "let"; i <- pName; reservedOp "="; e <- pExpr syn

414+ <|> try (do reserved "let"; i <- pName; reservedOp "="; fc <- pfc

415+ e <- pExpr syn

407 return (DoLet fc i e))

416 return (DoLet fc i e))

408− <|> try (do fc <- pfc

417+ <|> try (do e <- pExpr syn; fc <- pfc

409− e <- pExpr syn; return (DoExp fc e))

418+ return (DoExp fc e))

410

419

411pConstant :: IParser Const

420pConstant :: IParser Const

412pConstant = do reserved "Int"; return IType

421pConstant = do reserved "Int"; return IType

@@ -420,38 +429,38 @@ pConstant = do reserved "Int"; return IType

420 <|> try (do c <- chlit; return $ Ch c)

429 <|> try (do c <- chlit; return $ Ch c)

421

430

422table fixes

431table fixes

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

432+ = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [pexp (PConstant (I 0)), pexp x])]]

424 ++ toTable (reverse fixes) ++

433 ++ toTable (reverse fixes) ++

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

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

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

435+ [binary "->" (\fc x y -> PPi expl (MN 0 "X") x y) AssocRight]]

427

436

428toTable fs = map (map toBin)

437toTable fs = map (map toBin)

429 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

438 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

430 where toBin (Fix (PrefixN _) op) = prefix op

439 where toBin (Fix (PrefixN _) op) = prefix op

431− (\fc x -> PApp fc (PRef fc (UN [op])) [PExp x])

440+ (\fc x -> PApp fc (PRef fc (UN [op])) [pexp x])

432 toBin (Fix f op)

441 toBin (Fix f op)

433− = binary op (\fc x y -> PApp fc (PRef fc (UN [op])) [PExp x,PExp y]) (assoc f)

442+ = binary op (\fc x y -> PApp fc (PRef fc (UN [op])) [pexp x,pexp y]) (assoc f)

434 assoc (Infixl _) = AssocLeft

443 assoc (Infixl _) = AssocLeft

435 assoc (Infixr _) = AssocRight

444 assoc (Infixr _) = AssocRight

436 assoc (InfixN _) = AssocNone

445 assoc (InfixN _) = AssocNone

437

446

438−binary name f assoc = Infix (do { fc <- pfc;

447+binary name f assoc = Infix (do { reservedOp name; fc <- pfc;

439− reservedOp name; return (f fc) }) assoc

448+ return (f fc) }) assoc

440−prefix name f = Prefix (do { fc <- pfc;

449+prefix name f = Prefix (do { reservedOp name; fc <- pfc;

441− reservedOp name; return (f fc) })

450+ return (f fc) })

442

451

443--------- Data declarations ---------

452--------- Data declarations ---------

444

453

445pData :: SyntaxInfo -> IParser PDecl

454pData :: SyntaxInfo -> IParser PDecl

446−pData syn = try (do fc <- pfc

455+pData syn = try (do reserved "data"; fc <- pfc

447− reserved "data"; tyn <- pfName; ty <- pTSig syn

456+ tyn <- pfName; ty <- pTSig syn

448 reserved "where"

457 reserved "where"

449 ty' <- implicit syn tyn ty

458 ty' <- implicit syn tyn ty

450 cons <- sepBy (pConstructor syn) (lchar '|')

459 cons <- sepBy (pConstructor syn) (lchar '|')

451 lchar ';'

460 lchar ';'

452 return $ PData fc (PDatadecl tyn ty' cons))

461 return $ PData fc (PDatadecl tyn ty' cons))

453− <|> do fc <- pfc

462+ <|> do reserved "data"; fc <- pfc

454− reserved "data"; tyn <- pfName; args <- many pName

463+ tyn <- pfName; args <- many pName

455 lchar '='

464 lchar '='

456 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

465 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

457 lchar ';'

466 lchar ';'

@@ -465,31 +474,31 @@ pData syn = try (do fc <- pfc

465 return $ PData fc (PDatadecl tyn ty' cons')

474 return $ PData fc (PDatadecl tyn ty' cons')

466

475

467mkPApp fc t [] = t

476mkPApp fc t [] = t

468−mkPApp fc t xs = PApp fc t (map PExp xs)

477+mkPApp fc t xs = PApp fc t (map pexp xs)

469

478

470bindArgs :: [PTerm] -> PTerm -> PTerm

479bindArgs :: [PTerm] -> PTerm -> PTerm

471bindArgs [] t = t

480bindArgs [] t = t

472−bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)

481+bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)

473

482

474pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

483pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

475pConstructor syn

484pConstructor syn

476− = do fc <- pfc

485+ = do cn <- pfName; fc <- pfc

477− cn <- pfName; ty <- pTSig syn

486+ ty <- pTSig syn

478 ty' <- implicit syn cn ty

487 ty' <- implicit syn cn ty

479 return (cn, ty', fc)

488 return (cn, ty', fc)

480

489

481pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

490pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

482pSimpleCon syn

491pSimpleCon syn

492+ = do cn <- pfName

483− = do fc <- pfc

493+ fc <- pfc

484− cn <- pfName

485 args <- many (pSimpleExpr syn)

494 args <- many (pSimpleExpr syn)

486 return (cn, args, fc)

495 return (cn, args, fc)

487

496

488--------- Pattern match clauses ---------

497--------- Pattern match clauses ---------

489

498

490pPattern :: SyntaxInfo -> IParser PDecl

499pPattern :: SyntaxInfo -> IParser PDecl

491−pPattern syn = do fc <- pfc

500+pPattern syn = do clause <- pClause syn

492− clause <- pClause syn

501+ fc <- pfc

493 return (PClauses fc (MN 2 "_") [clause]) -- collect together later

502 return (PClauses fc (MN 2 "_") [clause]) -- collect together later

494

503

495whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo

504whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo

@@ -511,7 +520,7 @@ pClause syn

511 let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)

520 let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)

512 wheres <- choice [pWhereblock wsyn, do lchar ';'; return []]

521 wheres <- choice [pWhereblock wsyn, do lchar ';'; return []]

513 return $ PClause n (PApp fc (PRef fc n)

522 return $ PClause n (PApp fc (PRef fc n)

514− (iargs ++ map PExp args)) wargs rhs wheres)

523+ (iargs ++ map pexp args)) wargs rhs wheres)

515 <|> try (do n <- pfName

524 <|> try (do n <- pfName

516 iargs <- many (pImplicitArg syn)

525 iargs <- many (pImplicitArg syn)

517 fc <- pfc

526 fc <- pfc

@@ -524,7 +533,7 @@ pClause syn

524 let withs = concat ds

533 let withs = concat ds

525 lchar '}'

534 lchar '}'

526 return $ PWith n (PApp fc (PRef fc n)

535 return $ PWith n (PApp fc (PRef fc n)

527− (iargs ++ map PExp args)) wargs wval withs)

536+ (iargs ++ map pexp args)) wargs wval withs)

528

537

529 <|> do l <- pSimpleExpr syn

538 <|> do l <- pSimpleExpr syn

530 op <- operator

539 op <- operator

@@ -535,7 +544,7 @@ pClause syn

535 lchar '='

544 lchar '='

536 rhs <- pExpr syn

545 rhs <- pExpr syn

537 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

546 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

538− return $ PClause n (PApp fc (PRef fc n) [PExp l,PExp r]) wargs rhs wheres

547+ return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r]) wargs rhs wheres

539

548

540 <|> do l <- pSimpleExpr syn

549 <|> do l <- pSimpleExpr syn

541 op <- operator

550 op <- operator

@@ -549,7 +558,7 @@ pClause syn

549 ds <- many1 $ pFunDecl syn

558 ds <- many1 $ pFunDecl syn

550 let withs = concat ds

559 let withs = concat ds

551 lchar '}'

560 lchar '}'

552− return $ PWith n (PApp fc (PRef fc n) [PExp l, PExp r]) wargs wval withs

561+ return $ PWith n (PApp fc (PRef fc n) [pexp l, pexp r]) wargs wval withs

553

562

554pWExpr :: SyntaxInfo -> IParser PTerm

563pWExpr :: SyntaxInfo -> IParser PTerm

555pWExpr syn = do lchar '|'; pExpr' syn

564pWExpr syn = do lchar '|'; pExpr' syn

@@ -587,11 +596,11 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

587 block b [DoExp fc tm] = tm

596 block b [DoExp fc tm] = tm

588 block b [a] = PElabError "Last statement in do block must be an expression"

597 block b [a] = PElabError "Last statement in do block must be an expression"

589 block b (DoBind fc n tm : rest)

598 block b (DoBind fc n tm : rest)

590− = PApp fc (PRef fc b) [PExp tm, PExp (PLam n Placeholder (block b rest))]

599+ = PApp fc (PRef fc b) [pexp tm, pexp (PLam n Placeholder (block b rest))]

591 block b (DoExp fc tm : rest)

600 block b (DoExp fc tm : rest)

592 = PApp fc (PRef fc b)

601 = PApp fc (PRef fc b)

593− [PExp tm,

602+ [pexp tm,

594− PExp (PLam (MN 0 "bindx") Placeholder (block b rest))]

603+ pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

595expandDo dsl t = t

604expandDo dsl t = t

596

605

597

606