9d1ecc8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added some syntactic sugar for _|_, () and pairs

commit9d1ecc880f5eef0b03dbf2d1e053845706c197b7 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 14 Oct 2011, 21:27 (15 years ago) parent868409a

5 files changed+50−3

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+27 src/Idris/Delaborate.hs+6−1 src/Idris/ElabDecls.hs+9 src/Idris/Parser.hs+5−1 src/Idris/Primitives.hs+3−1

src/Idris/AbsSyntax.hs+27

@@ -149,6 +149,9 @@ data PTerm = PQuote Raw

149149 | PPi Plicity Name PTerm PTerm

150150 | PLet Name PTerm PTerm PTerm -- not implemented yet

151151 | PApp PTerm [PArg]

152+ | PTrue

153+ | PFalse

154+ | PPair PTerm PTerm

152155 | PHidden PTerm -- irrelevant or hidden pattern

153156 | PSet

154157 | PConstant Const

@@ -232,6 +235,9 @@ showImp impl tm = se 10 tm where

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

233236 ++ concatMap seArg args

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

238+ se p PTrue = "()"

239+ se p PFalse = "_|_"

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

235241 se p PSet = "Set"

236242 se p (PConstant c) = show c

237243 se p Placeholder = "_"

@@ -288,6 +294,27 @@ getInferTerm tm = error ("getInferTerm " ++ show tm)

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

289295getInferType (App (App _ ty) _) = ty

290296

297+-- Handy primitives: Unit, False, Pair, MkPair

298+

299+unitTy = MN 0 "__Unit"

300+unitCon = MN 0 "__II"

301+unitDecl = PDatadecl unitTy PSet

302+ [(unitCon, PRef unitTy)]

303+

304+falseTy = MN 0 "__False"

305+falseDecl = PDatadecl falseTy PSet []

306+

307+pairTy = MN 0 "__Pair"

308+pairCon = MN 0 "__MkPair"

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

310+ [(pairCon, PPi Imp (n "A") PSet (

311+ PPi Imp (n "B") PSet (

312+ PPi Exp (n "a") (PRef (n "A")) (

313+ PPi Exp (n "b") (PRef (n "B"))

314+ (PApp (PRef pairTy) [PExp (PRef (n "A")),

315+ PExp (PRef (n "B"))])))))]

316+ where n a = MN 0 a

317+

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

292319piBind [] t = t

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

src/Idris/Delaborate.hs+6−1

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

1313 where

1414 de env (App f a) = deFn env f [a]

1515 de env (V i) = PRef (env!!i)

16− de env (P _ n _) = PRef n

16+ de env (P _ n _) | n == unitTy = PTrue

17+ | n == unitCon = PTrue

18+ | n == falseTy = PFalse

19+ | otherwise = PRef n

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

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

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

@@ -23,6 +26,8 @@ delab ist tm = de [] tm

2326 de env (Set i) = PSet

2427

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

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

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

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

2732 deFn env f args = PApp (de env f) (map PExp (map (de env) args))

2833

src/Idris/ElabDecls.hs+9

@@ -190,6 +190,15 @@ elab info pattern tm = do elab' tm

190190 elab' PSet = do fill (RSet 0); solve

191191 elab' (PConstant c) = do apply (RConstant c) []; solve

192192 elab' (PQuote r) = do fill r; solve

193+ elab' PTrue = try (elab' (PRef unitCon))

194+ (elab' (PRef unitTy))

195+ elab' PFalse = elab' (PRef falseTy)

196+ elab' (PPair l r) = try (elab' (PApp (PRef pairTy)

197+ [PExp l,PExp r]))

198+ (elab' (PApp (PRef pairCon)

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

200+ PImp (MN 0 "a") Placeholder,

201+ PExp l, PExp r]))

193202 elab' (PRef n) | pattern && not (inparamBlock n)

194203 = try (do apply (Var n) []; solve)

195204 (patvar n)

src/Idris/Parser.hs+5−1

@@ -210,10 +210,14 @@ pSimpleExpr syn =

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

211211 return $ PQuote t)

212212 <|> try (do x <- pfName; return (PRef x))

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

213+ <|> try (do lchar '('; l <- pExpr syn; lchar ','; r <- pExpr syn; lchar ')';

214+ return (PPair l r))

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

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

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

218+ <|> try (do symbol "()"; return PTrue)

219+ <|> try (do symbol "_|_"; return PFalse)

220+ <|> try (do lchar '_'; return Placeholder)

217221

218222pHSimpleExpr syn

219223 = try (pSimpleExpr syn)

src/Idris/Primitives.hs+3−1

@@ -52,6 +52,8 @@ elabPrim :: Prim -> Idris ()

5252elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)

5353

5454elabPrims :: Idris ()

55−elabPrims = do elabDecl toplevel (PData inferDecl)

55+elabPrims = do mapM_ (elabDecl toplevel)

56+ (map PData

57+ [inferDecl, unitDecl, falseDecl, pairDecl])

5658 mapM_ elabPrim primitives

5759