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

src/Idris/AbsSyntax.hs+27

compare with master

unifiedsplit

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

149 | PPi Plicity Name PTerm PTerm

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

151 | PApp PTerm [PArg]

152+ | PTrue

153+ | PFalse

154+ | PPair PTerm PTerm

152 | PHidden PTerm -- irrelevant or hidden pattern

155 | PHidden PTerm -- irrelevant or hidden pattern

153 | PSet

156 | PSet

154 | PConstant Const

157 | PConstant Const

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

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

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

233 ++ concatMap seArg args

236 ++ concatMap seArg args

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

237 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 ++ ")"

235 se p PSet = "Set"

241 se p PSet = "Set"

236 se p (PConstant c) = show c

242 se p (PConstant c) = show c

237 se p Placeholder = "_"

243 se p Placeholder = "_"

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

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

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

289getInferType (App (App _ ty) _) = ty

295getInferType (App (App _ ty) _) = ty

290

296

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+

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

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

292piBind [] t = t

319piBind [] t = t

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

320piBind ((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

13 where

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

15 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

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

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

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

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

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

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

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

23 de env (Set i) = PSet

26 de env (Set i) = PSet

24

27

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

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

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

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

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

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

28

33

src/Idris/ElabDecls.hs+9

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

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

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

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

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

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

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

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

195 (patvar n)

204 (patvar n)

src/Idris/Parser.hs+5−1

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

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

211 return $ PQuote t)

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

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

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

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

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

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

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

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

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

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

217

221

218pHSimpleExpr syn

222pHSimpleExpr syn

219 = try (pSimpleExpr syn)

223 = try (pSimpleExpr syn)

src/Idris/Primitives.hs+3−1

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

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

53

54elabPrims :: Idris ()

55−elabPrims = do elabDecl toplevel (PData inferDecl)

55+elabPrims = do mapM_ (elabDecl toplevel)

56+ (map PData

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

56 mapM_ elabPrim primitives

58 mapM_ elabPrim primitives

57

59