git.iko.soy/Idris-dev
on master help sign in
Allow types on let in do blocks
commit6196bbcec977ab83ae1ceb762b258b40717d7edb authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 12:08 (15 years ago) parent947c2b3
3 files changed+38−13
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−1 src/Idris/IBC.hs+25−7 src/Idris/Parser.hs+12−5
src/Idris/AbsSyntax.hs+1−1
@@ -449,7 +449,7 @@ type PTactic = PTactic' PTerm
449449data PDo' t = DoExp FC t
450450 | DoBind FC Name t
451451 | DoBindP FC t t
452− | DoLet FC Name t
452+ | DoLet FC Name t t
453453 | DoLetP FC t t
454454 deriving (Eq, Functor)
455455{-!
src/Idris/IBC.hs+25−7
@@ -840,7 +840,7 @@ instance (Binary t) => Binary (PTactic' t) where
840840 15 -> return Qed
841841 _ -> error "Corrupted binary data for PTactic'"
842842
843−
843+
844844instance (Binary t) => Binary (PDo' t) where
845845 put x
846846 = case x of
@@ -851,10 +851,19 @@ instance (Binary t) => Binary (PDo' t) where
851851 put x1
852852 put x2
853853 put x3
854− DoLet x1 x2 x3 -> do putWord8 2
855− put x1
856− put x2
857− put x3
854+ DoBindP x1 x2 x3 -> do putWord8 2
855+ put x1
856+ put x2
857+ put x3
858+ DoLet x1 x2 x3 x4 -> do putWord8 3
859+ put x1
860+ put x2
861+ put x3
862+ put x4
863+ DoLetP x1 x2 x3 -> do putWord8 4
864+ put x1
865+ put x2
866+ put x3
858867 get
859868 = do i <- getWord8
860869 case i of
@@ -868,10 +877,19 @@ instance (Binary t) => Binary (PDo' t) where
868877 2 -> do x1 <- get
869878 x2 <- get
870879 x3 <- get
871− return (DoLet x1 x2 x3)
880+ return (DoBindP x1 x2 x3)
881+ 3 -> do x1 <- get
882+ x2 <- get
883+ x3 <- get
884+ x4 <- get
885+ return (DoLet x1 x2 x3 x4)
886+ 4 -> do x1 <- get
887+ x2 <- get
888+ x3 <- get
889+ return (DoLetP x1 x2 x3)
872890 _ -> error "Corrupted binary data for PDo'"
873891
874−
892+
875893instance (Binary t) => Binary (PArg' t) where
876894 put x
877895 = case x of
src/Idris/Parser.hs+12−5
@@ -474,7 +474,12 @@ pExt syn (Rule (s:ssym) ptm _)
474474 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
475475 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
476476 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
477− upd ns (DoLet fc n t : ds) = DoLet fc n (update ns t) : upd (dropn n ns) ds
477+ upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
478+ : upd (dropn n ns) ds
479+ upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
480+ : upd ns ds
481+ upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
482+ : upd ns ds
478483 update ns t = t
479484
480485pName = do i <- getState
@@ -702,9 +707,11 @@ pDoBlock syn
702707 return (PDoBlock ds)
703708
704709pDo syn
705− = try (do reserved "let"; i <- pName; reservedOp "="; fc <- pfc
710+ = try (do reserved "let"; i <- pName;
711+ ty <- option Placeholder (do lchar ':'; pExpr' syn)
712+ reservedOp "="; fc <- pfc
706713 e <- pExpr syn
707− return (DoLet fc i e))
714+ return (DoLet fc i ty e))
708715 <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc
709716 sc <- pExpr syn
710717 return (DoLetP fc i sc))
@@ -1048,8 +1055,8 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
10481055 = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder
10491056 (PCase fc (PRef fc (MN 0 "bpat"))
10501057 [(p, block b rest)]))]
1051− block b (DoLet fc n tm : rest)
1052− = PLet n Placeholder tm (block b rest)
1058+ block b (DoLet fc n ty tm : rest)
1059+ = PLet n ty tm (block b rest)
10531060 block b (DoLetP fc p tm : rest)
10541061 = PCase fc tm [(p, block b rest)]
10551062 block b (DoExp fc tm : rest)