Permalink
Browse files

Sugar for dependent pairs

  • Loading branch information...
1 parent 5e92c70 commit 39b934cfab75d64e8c2b235c60b5c9350662de50 Edwin Brady committed Oct 25, 2011
Showing with 47 additions and 5 deletions.
  1. +5 −0 Makefile
  2. +1 −1 src/Core/CoreParser.hs
  3. +23 −3 src/Idris/AbsSyntax.hs
  4. +12 −0 src/Idris/ElabDecls.hs
  5. +6 −1 src/Idris/Parser.hs
View
@@ -2,6 +2,11 @@ install: .PHONY
cabal install
make -C lib check
+pinstall: .PHONY
+ cabal configure --enable-executable-profiling
+ cabal install --enable-executable-profiling
+ make -C lib check
+
build: .PHONY
cabal build
View
@@ -17,7 +17,7 @@ type TokenParser a = PTok.TokenParser a
idrisDef = haskellDef {
opStart = iOpStart,
opLetter = iOpLetter,
- reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>"],
+ reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
"do", "dsl", "import",
"infix", "infixl", "infixr", "prefix",
View
@@ -178,6 +178,7 @@ data PTerm = PQuote Raw
| PTrue FC
| PFalse FC
| PPair FC PTerm PTerm
+ | PDPair FC PTerm PTerm
| PHidden PTerm -- irrelevant or hidden pattern
| PSet
| PConstant Const
@@ -302,6 +303,7 @@ showImp impl tm = se 10 tm where
se p (PTrue _) = "()"
se p (PFalse _) = "_|_"
se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
+ se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
se p PSet = "Set"
se p (PConstant c) = show c
se p (PMetavar n) = "?" ++ show n
@@ -323,6 +325,7 @@ allNamesIn tm = nub $ ni [] tm
ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
ni env (PHidden tm) = ni env tm
ni env (PPair _ l r) = ni env l ++ ni env r
+ ni env (PDPair _ l r) = ni env l ++ ni env r
ni env _ = []
namesIn :: IState -> PTerm -> [Name]
@@ -337,6 +340,7 @@ namesIn ist tm = nub $ ni [] tm
ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
ni env (PPair _ l r) = ni env l ++ ni env r
+ ni env (PDPair _ l r) = ni env l ++ ni env r
ni env (PHidden tm) = ni env tm
ni env _ = []
@@ -374,8 +378,8 @@ unitDecl = PDatadecl unitTy PSet
falseTy = MN 0 "__False"
falseDecl = PDatadecl falseTy PSet []
-pairTy = UN ["Pair"] -- MN 0 "__Pair"
-pairCon = UN ["MkPair"] -- MN 0 "__MkPair"
+pairTy = MN 0 "__Pair"
+pairCon = MN 0 "__MkPair"
pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
[(pairCon, PPi Imp (n "A") PSet (
PPi Imp (n "B") PSet (
@@ -385,6 +389,10 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
PExp (PRef bi (n "B"))])))), bi)]
where n a = MN 0 a
+-- Defined in builtins.idr
+sigmaTy = UN ["Sigma"]
+existsCon = UN ["Exists"]
+
piBind :: [(Name, PTerm)] -> PTerm -> PTerm
piBind [] t = t
piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
@@ -422,7 +430,16 @@ implicitise syn ist tm
imps True (n:env) sc
imps top env (PPair _ l r)
= do (decls, ns) <- get
- put (decls, nub (ns ++ namesIn ist l ++ namesIn ist r))
+ let isn = namesIn ist l ++ namesIn ist r
+ put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
+ imps top env (PDPair _ (PRef _ n) r)
+ = do (decls, ns) <- get
+ let isn = namesIn ist r \\ [n]
+ put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
+ imps top env (PDPair _ l r)
+ = do (decls, ns) <- get
+ let isn = namesIn ist l ++ namesIn ist r
+ put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
imps top env (PLam n ty sc)
= do imps False env ty
imps False (n:env) sc
@@ -443,6 +460,9 @@ addImpl ist ptm = ai [] ptm
ai env (PPair fc l r) = let l' = ai env l
r' = ai env r in
PPair fc l' r'
+ ai env (PDPair fc l r) = let l' = ai env l
+ r' = ai env r in
+ PDPair fc l' r'
ai env (PApp fc (PRef _ f) as)
= let as' = map (fmap (ai env)) as in
aiFn fc env (PRef fc f) as'
View
@@ -306,6 +306,18 @@ elab info pattern tm = do elab' tm
[PImp (MN 0 "A") Placeholder,
PImp (MN 0 "B") Placeholder,
PExp l, PExp r]))
+ elab' (PDPair fc l@(PRef _ n) r)
+ = try (elab' (PApp fc (PRef fc sigmaTy)
+ [PExp Placeholder,
+ PExp (PLam n Placeholder r)]))
+ (elab' (PApp fc (PRef fc existsCon)
+ [PImp (MN 0 "a") Placeholder,
+ PImp (MN 0 "P") Placeholder,
+ PExp l, PExp r]))
+ elab' (PDPair fc l r) = elab' (PApp fc (PRef fc existsCon)
+ [PImp (MN 0 "a") Placeholder,
+ PImp (MN 0 "P") Placeholder,
+ PExp l, PExp r])
elab' (PRef fc n) | pattern && not (inparamBlock n)
= erun fc $
try (do apply (Var n) []; solve)
View
@@ -299,6 +299,7 @@ pExt syn (Rule (s:ssym) ptm)
(update (dropn n ns) sc)
update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
+ update ns (PDPair fc l r) = PDPair fc (update ns l) (update ns r)
update ns (PHidden t) = PHidden (update ns t)
update ns (PDoBlock ds) = PDoBlock $ upd ns ds
where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
@@ -326,6 +327,9 @@ pSimpleExpr syn =
<|> try (do lchar '('; l <- pExpr syn; lchar ','; fc <- pfc
r <- pExpr syn; lchar ')';
return (PPair fc l r))
+ <|> try (do lchar '('; l <- pExpr syn; reservedOp "**"; fc <- pfc
+ r <- pExpr syn; lchar ')';
+ return (PDPair fc l r))
<|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)
<|> try (do c <- pConstant; return (PConstant c))
<|> try (do reserved "Set"; return PSet)
@@ -513,7 +517,7 @@ pClause syn
args <- many (pHSimpleExpr syn)
wargs <- many (pWExpr syn)
reserved "with"
- wval <- pSimpleExpr syn
+ wval <- pExpr' syn
lchar '{'
ds <- many1 $ pFunDecl syn
let withs = concat ds
@@ -573,6 +577,7 @@ expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
(map (fmap (expandDo dsl)) args)
expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)
+expandDo dsl (PDPair fc l r) = PDPair fc (expandDo dsl l) (expandDo dsl r)
expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)
expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

0 comments on commit 39b934c

Please sign in to comment.