46338e2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Parsing restrictions for implicit argument types

46338e2Edwin Brady14 years ago

src/Idris/AbsSyntax.hs+2−1

compare with master

unifiedsplit

@@ -799,13 +799,14 @@ data SyntaxInfo = Syn { using :: [(Name, PTerm)],

799 no_imp :: [Name],

800 decoration :: Name -> Name,

801 inPattern :: Bool,

802+ implicitAllowed :: Bool,

802 dsl_info :: DSL }

803 dsl_info :: DSL }

803 deriving Show

804 deriving Show

804{-!

805{-!

805deriving instance Binary SyntaxInfo

806deriving instance Binary SyntaxInfo

806!-}

807!-}

807

808

808−defaultSyntax = Syn [] [] [] [] id False initDSL

809+defaultSyntax = Syn [] [] [] [] id False False initDSL

809

810

810expandNS :: SyntaxInfo -> Name -> Name

811expandNS :: SyntaxInfo -> Name -> Name

811expandNS syn n@(NS _ _) = n

812expandNS syn n@(NS _ _) = n

src/Idris/Delaborate.hs+2−1

@@ -73,7 +73,8 @@ delab' ist tm fullname = de [] tm

73pshow :: IState -> Err -> String

74pshow i (Msg s) = s

75pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

76+ "\nThis is probably a bug, or a missing error message.\n" ++

76− "\nThis is probably a bug. Please consider reporting at " ++ bugaddr

77+ "Please consider reporting at " ++ bugaddr

77pshow i (CantUnify x y e sc s)

78pshow i (CantUnify x y e sc s)

78 = "Can't unify " ++ show (delab i x)

79 = "Can't unify " ++ show (delab i x)

79 ++ " with " ++ show (delab i y) ++

80 ++ " with " ++ show (delab i y) ++

src/Idris/IBC.hs+5−3

@@ -21,7 +21,7 @@ import System.Directory

21import Paths_idris

23ibcVersion :: Word8

24−ibcVersion = 18

24+ibcVersion = 19

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

@@ -913,7 +913,7 @@ instance (Binary t) => Binary (PDecl' t) where

913 _ -> error "Corrupted binary data for PDecl'"

914

915instance Binary SyntaxInfo where

916− put (Syn x1 x2 x3 x4 x5 x6 x7)

916+ put (Syn x1 x2 x3 x4 x5 x6 x7 x8)

917 = do put x1

918 put x2

919 put x3

@@ -921,6 +921,7 @@ instance Binary SyntaxInfo where

921 put x5

922 put x6

923 put x7

924+ put x8

924 get

925 get

925 = do x1 <- get

926 = do x1 <- get

926 x2 <- get

927 x2 <- get

@@ -929,7 +930,8 @@ instance Binary SyntaxInfo where

929 x5 <- get

930 x5 <- get

930 x6 <- get

931 x6 <- get

931 x7 <- get

932 x7 <- get

933+ x8 <- get

932− return (Syn x1 x2 x3 x4 x5 x6 x7)

934+ return (Syn x1 x2 x3 x4 x5 x6 x7 x8)

933

935

934instance (Binary t) => Binary (PClause' t) where

936instance (Binary t) => Binary (PClause' t) where

935 put x

937 put x

src/Idris/Parser.hs+22−17

@@ -409,7 +409,7 @@ pFunDecl' syn = try (do push_indent

409 opts' <- pFnOpts

410 n_in <- pfName

411 let n = expandNS syn n_in

412− ty <- pTSig syn

412+ ty <- pTSig (impOK syn)

413 fc <- pfc

414 pTerminator

415-- ty' <- implicit syn n ty

@@ -656,7 +656,7 @@ pSimpleExpr syn =

656 <|> try (pList syn)

657 <|> try (pAlt syn)

658 <|> try (pIdiom syn)

659− <|> try (do lchar '('; bracketed syn)

659+ <|> try (do lchar '('; bracketed (noImp syn))

660 <|> try (do c <- pConstant; fc <- pfc

661 return (modifyConst syn fc (PConstant c)))

662 <|> do reserved "Set"; return PSet

@@ -793,9 +793,12 @@ mkSet (UN n) = UN ("set_" ++ n)

793mkSet (MN 0 n) = MN 0 ("set_" ++ n)

794mkSet (NS n s) = NS (mkSet n) s

795

796+noImp syn = syn { implicitAllowed = False }

797+impOK syn = syn { implicitAllowed = True }

798+

796pTSig syn = do lchar ':'

799pTSig syn = do lchar ':'

797− cs <- pConstList syn

800+ cs <- if implicitAllowed syn then pConstList syn else return []

798− sc <- pExpr syn

801+ sc <- pExpr syn

799 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

802 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

800

803

801pLambda syn = do lchar '\\'

804pLambda syn = do lchar '\\'

@@ -832,12 +835,14 @@ pPi syn =

832 symbol "->"

835 symbol "->"

833 sc <- pExpr syn

836 sc <- pExpr syn

834 return (bindList (PPi (Exp lazy st)) xt sc))

837 return (bindList (PPi (Exp lazy st)) xt sc))

838+ <|> try (if implicitAllowed syn then

835− <|> try (do lazy <- option False (do lchar '|'; return True)

839+ do lazy <- option False (do lchar '|'; return True)

836− st <- pStatic

840+ st <- pStatic

837− lchar '{'; xt <- tyDeclList syn; lchar '}'

841+ lchar '{'; xt <- tyDeclList syn; lchar '}'

838− symbol "->"

842+ symbol "->"

839− sc <- pExpr syn

843+ sc <- pExpr syn

840− return (bindList (PPi (Imp lazy st)) xt sc))

844+ return (bindList (PPi (Imp lazy st)) xt sc)

845+ else fail "No implicit arguments allowed here")

841 <|> try (do lchar '{'; reserved "auto"

846 <|> try (do lchar '{'; reserved "auto"

842 xt <- tyDeclList syn; lchar '}'

847 xt <- tyDeclList syn; lchar '}'

843 symbol "->"

848 symbol "->"

@@ -858,19 +863,19 @@ pPi syn =

858

863

859pConstList :: SyntaxInfo -> IParser [PTerm]

864pConstList :: SyntaxInfo -> IParser [PTerm]

860pConstList syn = try (do lchar '('

865pConstList syn = try (do lchar '('

861− tys <- sepBy1 (pExpr' syn) (lchar ',')

866+ tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')

862 lchar ')'

867 lchar ')'

863 reservedOp "=>"

868 reservedOp "=>"

864 return tys)

869 return tys)

865− <|> try (do t <- pExpr syn

870+ <|> try (do t <- pExpr (noImp syn)

866 reservedOp "=>"

871 reservedOp "=>"

867 return [t])

872 return [t])

868 <|> return []

873 <|> return []

869

874

870−tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

875+tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig (noImp syn); return (x,t))

871 (lchar ','))

876 (lchar ','))

872 <|> do ns <- sepBy1 pName (lchar ',')

877 <|> do ns <- sepBy1 pName (lchar ',')

873− t <- pTSig syn

878+ t <- pTSig (noImp syn)

874 return (map (\x -> (x, t)) ns)

879 return (map (\x -> (x, t)) ns)

875

880

876tyOptDeclList syn = sepBy1 (do x <- pfName;

881tyOptDeclList syn = sepBy1 (do x <- pfName;

@@ -978,7 +983,7 @@ accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns

978pRecord :: SyntaxInfo -> IParser PDecl

983pRecord :: SyntaxInfo -> IParser PDecl

979pRecord syn = do acc <- pAccessibility

984pRecord syn = do acc <- pAccessibility

980 reserved "record"; fc <- pfc

985 reserved "record"; fc <- pfc

981− tyn_in <- pfName; ty <- pTSig syn

986+ tyn_in <- pfName; ty <- pTSig (impOK syn)

982 let tyn = expandNS syn tyn_in

987 let tyn = expandNS syn tyn_in

983 reserved "where"

988 reserved "where"

984 open_block

989 open_block

@@ -1004,7 +1009,7 @@ pRecord syn = do acc <- pAccessibility

1004pData :: SyntaxInfo -> IParser PDecl

1009pData :: SyntaxInfo -> IParser PDecl

1005pData syn = try (do acc <- pAccessibility

1010pData syn = try (do acc <- pAccessibility

1006 reserved "data"; fc <- pfc

1011 reserved "data"; fc <- pfc

1007− tyn_in <- pfName; ty <- pTSig syn

1012+ tyn_in <- pfName; ty <- pTSig (impOK syn)

1008 let tyn = expandNS syn tyn_in

1013 let tyn = expandNS syn tyn_in

1009 reserved "where"

1014 reserved "where"

1010 open_block

1015 open_block

@@ -1044,7 +1049,7 @@ pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

1044pConstructor syn

1049pConstructor syn

1045 = do cn_in <- pfName; fc <- pfc

1050 = do cn_in <- pfName; fc <- pfc

1046 let cn = expandNS syn cn_in

1051 let cn = expandNS syn cn_in

1047− ty <- pTSig syn

1052+ ty <- pTSig (impOK syn)

1048-- ty' <- implicit syn cn ty

1053-- ty' <- implicit syn cn ty

1049 return (cn, ty, fc)

1054 return (cn, ty, fc)

1050

1055