6196bbc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow types on let in do blocks

6196bbcEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -449,7 +449,7 @@ type PTactic = PTactic' PTerm

449data PDo' t = DoExp FC t

450 | DoBind FC Name t

451 | DoBindP FC t t

452− | DoLet FC Name t

452+ | DoLet FC Name t t

453 | DoLetP FC t t

454 deriving (Eq, Functor)

455{-!

src/Idris/IBC.hs+25−7

@@ -840,7 +840,7 @@ instance (Binary t) => Binary (PTactic' t) where

840 15 -> return Qed

841 _ -> error "Corrupted binary data for PTactic'"

842

843−

843+

844instance (Binary t) => Binary (PDo' t) where

845 put x

846 = case x of

@@ -851,10 +851,19 @@ instance (Binary t) => Binary (PDo' t) where

851 put x1

852 put x2

853 put x3

854+ DoBindP x1 x2 x3 -> do putWord8 2

855+ put x1

856+ put x2

857+ put x3

854− DoLet x1 x2 x3 -> do putWord8 2

858+ DoLet x1 x2 x3 x4 -> do putWord8 3

855− put x1

859+ put x1

856− put x2

860+ put x2

861+ put x3

862+ put x4

863+ DoLetP x1 x2 x3 -> do putWord8 4

864+ put x1

865+ put x2

857− put x3

866+ put x3

858 get

867 get

859 = do i <- getWord8

868 = do i <- getWord8

860 case i of

869 case i of

@@ -868,10 +877,19 @@ instance (Binary t) => Binary (PDo' t) where

868 2 -> do x1 <- get

877 2 -> do x1 <- get

869 x2 <- get

878 x2 <- get

870 x3 <- get

879 x3 <- get

880+ return (DoBindP x1 x2 x3)

881+ 3 -> do x1 <- get

882+ x2 <- get

883+ x3 <- get

884+ x4 <- get

871− return (DoLet x1 x2 x3)

885+ return (DoLet x1 x2 x3 x4)

886+ 4 -> do x1 <- get

887+ x2 <- get

888+ x3 <- get

889+ return (DoLetP x1 x2 x3)

872 _ -> error "Corrupted binary data for PDo'"

890 _ -> error "Corrupted binary data for PDo'"

873

891

874−

892+

875instance (Binary t) => Binary (PArg' t) where

893instance (Binary t) => Binary (PArg' t) where

876 put x

894 put x

877 = case x of

895 = case x of

src/Idris/Parser.hs+12−5

@@ -474,7 +474,12 @@ pExt syn (Rule (s:ssym) ptm _)

474 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

475 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds

476 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

478 update ns t = t

483 update ns t = t

479

484

480pName = do i <- getState

485pName = do i <- getState

@@ -702,9 +707,11 @@ pDoBlock syn

702 return (PDoBlock ds)

707 return (PDoBlock ds)

703

708

704pDo syn

709pDo 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

706 e <- pExpr syn

713 e <- pExpr syn

707− return (DoLet fc i e))

714+ return (DoLet fc i ty e))

708 <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc

715 <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc

709 sc <- pExpr syn

716 sc <- pExpr syn

710 return (DoLetP fc i sc))

717 return (DoLetP fc i sc))

@@ -1048,8 +1055,8 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

1048 = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder

1055 = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder

1049 (PCase fc (PRef fc (MN 0 "bpat"))

1056 (PCase fc (PRef fc (MN 0 "bpat"))

1050 [(p, block b rest)]))]

1057 [(p, block b rest)]))]

1051− block b (DoLet fc n tm : rest)

1058+ block b (DoLet fc n ty tm : rest)

1052− = PLet n Placeholder tm (block b rest)

1059+ = PLet n ty tm (block b rest)

1053 block b (DoLetP fc p tm : rest)

1060 block b (DoLetP fc p tm : rest)

1054 = PCase fc tm [(p, block b rest)]

1061 = PCase fc tm [(p, block b rest)]

1055 block b (DoExp fc tm : rest)

1062 block b (DoExp fc tm : rest)