5a937cc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More flexibility in constraint arguments

5a937ccEdwin Brady10 years ago

CHANGELOG.md+3

compare with master

unifiedsplit

@@ -43,6 +43,9 @@

43 test x = x <+> x <+> neutral

44 ```

46+* Constraint arguments can now appear anywhere in function types, not just

47+ at the top level or after an implicit argument binding.

48+

46* Experimental extended `with` syntax, which allows calling functions defined

49* Experimental extended `with` syntax, which allows calling functions defined

47 in a with block directly. For example:

50 in a with block directly. For example:

libs/contrib/Classes/Verified.idr+1−1

@@ -28,7 +28,7 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->

28 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

29 (<*>) {f} (pure g) (pure x) = pure {f} (g x)

30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

31− g <*> pure x = pure (\g' : a -> b => g' x) <*> g

31+ g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g

33interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

34 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

src/Idris/AbsSyntaxTree.hs+2−1

@@ -1549,6 +1549,7 @@ data SyntaxInfo = Syn { using :: [Using],

1549 decoration :: Name -> Name,

1550 inPattern :: Bool,

1551 implicitAllowed :: Bool,

1552+ constraintAllowed :: Bool,

1552 maxline :: Maybe Int,

1553 maxline :: Maybe Int,

1553 mut_nesting :: Int,

1554 mut_nesting :: Int,

1554 dsl_info :: DSL,

1555 dsl_info :: DSL,

@@ -1561,7 +1562,7 @@ deriving instance NFData SyntaxInfo

1561deriving instance Binary SyntaxInfo

1562deriving instance Binary SyntaxInfo

1562!-}

1563!-}

1563

1564

1564−defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True True

1565+defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True

1565

1566

1566expandNS :: SyntaxInfo -> Name -> Name

1567expandNS :: SyntaxInfo -> Name -> Name

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

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

src/Idris/DeepSeq.hs+2−2

@@ -684,13 +684,13 @@ instance NFData Using where

684 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

685

686instance NFData SyntaxInfo where

687− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

687+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

688 = rnf x1 `seq`

689 rnf x2 `seq`

690 rnf x3 `seq`

691 rnf x4 `seq`

692 rnf x5 `seq`

693− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` ()

693+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` ()

694

695instance NFData OutputMode where

696 rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong

src/Idris/IBC.hs+5−3

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

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 141

43+ibcVersion = 142

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

@@ -1591,7 +1591,7 @@ instance Binary Using where

1591 _ -> error "Corrupted binary data for Using"

1592

1593instance Binary SyntaxInfo where

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

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

1595 = do put x1

1596 put x2

1597 put x3

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

1599 put x5

1600 put x6

1601 put x7

1602+ put x8

1602 get

1603 get

1603 = do x1 <- get

1604 = do x1 <- get

1604 x2 <- get

1605 x2 <- get

@@ -1607,7 +1608,8 @@ instance Binary SyntaxInfo where

1607 x5 <- get

1608 x5 <- get

1608 x6 <- get

1609 x6 <- get

1609 x7 <- get

1610 x7 <- get

1611+ x8 <- get

1610− return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True True)

1612+ return (Syn x1 x2 x3 x4 [] id x5 x6 x7 Nothing 0 x8 0 True True)

1611

1613

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

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

1613 put x

1615 put x

src/Idris/Parser.hs+2−3

@@ -1238,13 +1238,12 @@ clause syn

1238 return $ PWith fc n capp wargs wval pn withs)

1239 <|> do pushIndent

1240 (n_in, nfc) <- fnName; let n = expandNS syn n_in

1241− cargs <- many (constraintArg syn)

1242 fc <- getFC

1241 fc <- getFC

1243 args <- many (try (implicitArg (syn { inPattern = True } ))

1242 args <- many (try (implicitArg (syn { inPattern = True } ))

1243+ <|> try (constraintArg (syn { inPattern = True }))

1244 <|> (fmap pexp (argExpr syn)))

1245 wargs <- many (wExpr syn)

1246− let capp = PApp fc (PRef nfc [nfc] n)

1246+ let capp = PApp fc (PRef nfc [nfc] n) args

1247− (cargs ++ args)

1248 (do r <- rhs syn n

1247 (do r <- rhs syn n

1249 ist <- get

1248 ist <- get

1250 let ctxt = tt_ctxt ist

1249 let ctxt = tt_ctxt ist

src/Idris/Parser/Expr.hs+30−13

@@ -36,11 +36,17 @@ import Debug.Trace

37-- | Allow implicit type declarations

38allowImp :: SyntaxInfo -> SyntaxInfo

39−allowImp syn = syn { implicitAllowed = True }

39+allowImp syn = syn { implicitAllowed = True,

40+ constraintAllowed = False }

41-- | Disallow implicit type declarations

42-- | Disallow implicit type declarations

42disallowImp :: SyntaxInfo -> SyntaxInfo

43disallowImp :: SyntaxInfo -> SyntaxInfo

43−disallowImp syn = syn { implicitAllowed = False }

44+disallowImp syn = syn { implicitAllowed = False,

45+ constraintAllowed = False }

46+

47+-- | Allow scoped constraint arguments

48+allowConstr :: SyntaxInfo -> SyntaxInfo

49+allowConstr syn = syn { constraintAllowed = True }

45{-| Parses an expression as a whole

51{-| Parses an expression as a whole

46@

52@

@@ -327,7 +333,7 @@ CaseOption ::=

327@

333@

328-}

334-}

329caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

335caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

330−caseOption syn = do lhs <- expr (syn { inPattern = True })

336+caseOption syn = do lhs <- expr (disallowImp (syn { inPattern = True }))

331 r <- impossible <|> symbol "=>" *> expr syn

337 r <- impossible <|> symbol "=>" *> expr syn

332 return (lhs, r)

338 return (lhs, r)

333 <?> "case option"

339 <?> "case option"

@@ -432,7 +438,7 @@ simpleExpr syn =

432 <|> do lchar '_'; return Placeholder

438 <|> do lchar '_'; return Placeholder

433 <?> "expression"

439 <?> "expression"

434

440

435−{- |Parses an expression in braces

441+{- |Parses an expression in parentheses

436@

442@

437Bracketed ::= '(' Bracketed'

443Bracketed ::= '(' Bracketed'

438@

444@

@@ -477,8 +483,8 @@ bracketed' open syn =

477 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder

483 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder

478 (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,

484 (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,

479 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

485 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

480− <|> do l <- expr syn

486+ <|> do l <- expr (allowConstr syn)

481− bracketedExpr syn open l

487+ bracketedExpr (allowConstr syn) open l

482

488

483

489

484

490

@@ -891,7 +897,7 @@ TypeExpr ::= ConstraintList? Expr;

891 -}

897 -}

892typeExpr :: SyntaxInfo -> IdrisParser PTerm

898typeExpr :: SyntaxInfo -> IdrisParser PTerm

893typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

899typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

894− sc <- expr syn

900+ sc <- expr (allowConstr syn)

895 return (bindList (PPi constraint) cs sc)

901 return (bindList (PPi constraint) cs sc)

896 <?> "type signature"

902 <?> "type signature"

897

903

@@ -916,13 +922,13 @@ LambdaTail ::=

916-}

922-}

917lambda :: SyntaxInfo -> IdrisParser PTerm

923lambda :: SyntaxInfo -> IdrisParser PTerm

918lambda syn = do lchar '\\' <?> "lambda expression"

924lambda syn = do lchar '\\' <?> "lambda expression"

919− ((do xt <- try $ tyOptDeclList syn

925+ ((do xt <- try $ tyOptDeclList (disallowImp syn)

920 fc <- getFC

926 fc <- getFC

921 sc <- lambdaTail

927 sc <- lambdaTail

922 return (bindList (PLam fc) xt sc))

928 return (bindList (PLam fc) xt sc))

923 <|>

929 <|>

924 (do ps <- sepBy (do fc <- getFC

930 (do ps <- sepBy (do fc <- getFC

925− e <- simpleExpr (syn { inPattern = True })

931+ e <- simpleExpr (disallowImp (syn { inPattern = True }))

926 return (fc, e))

932 return (fc, e))

927 (lchar ',')

933 (lchar ',')

928 sc <- lambdaTail

934 sc <- lambdaTail

@@ -1055,7 +1061,7 @@ bindsymbol opts st syn

1055explicitPi opts st syn

1061explicitPi opts st syn

1056 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

1062 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

1057 binder <- bindsymbol opts st syn

1063 binder <- bindsymbol opts st syn

1058− sc <- expr syn

1064+ sc <- expr (allowConstr syn)

1059 return (bindList (PPi binder) xt sc)

1065 return (bindList (PPi binder) xt sc)

1060

1066

1061autoImplicit opts st syn

1067autoImplicit opts st syn

@@ -1064,7 +1070,7 @@ autoImplicit opts st syn

1064 xt <- typeDeclList syn

1070 xt <- typeDeclList syn

1065 lchar '}'

1071 lchar '}'

1066 symbol "->"

1072 symbol "->"

1067− sc <- expr syn

1073+ sc <- expr (allowConstr syn)

1068 highlightP kw AnnKeyword

1074 highlightP kw AnnKeyword

1069 return (bindList (PPi

1075 return (bindList (PPi

1070 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)

1076 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)

@@ -1078,7 +1084,7 @@ defaultImplicit opts st syn = do

1078 xt <- typeDeclList syn

1084 xt <- typeDeclList syn

1079 lchar '}'

1085 lchar '}'

1080 symbol "->"

1086 symbol "->"

1081− sc <- expr syn

1087+ sc <- expr (allowConstr syn)

1082 highlightP kw AnnKeyword

1088 highlightP kw AnnKeyword

1083 return (bindList (PPi (TacImp [] Dynamic script)) xt sc)

1089 return (bindList (PPi (TacImp [] Dynamic script)) xt sc)

1084

1090

@@ -1096,6 +1102,14 @@ normalImplicit opts st syn = do

1096 return (bindList (PPi im) xt

1102 return (bindList (PPi im) xt

1097 (bindList (PPi cl) cs sc))

1103 (bindList (PPi cl) cs sc))

1098

1104

1105+constraintPi opts st syn =

1106+ do cs <- constraintList1 syn

1107+ sc <- expr syn

1108+ if implicitAllowed syn

1109+ then return (bindList (PPi constraint) cs sc)

1110+ else return (bindList (PPi (Imp opts st False (Just (Impl True False)) True))

1111+ cs sc)

1112+

1099implicitPi opts st syn =

1113implicitPi opts st syn =

1100 autoImplicit opts st syn

1114 autoImplicit opts st syn

1101 <|> defaultImplicit opts st syn

1115 <|> defaultImplicit opts st syn

@@ -1114,7 +1128,10 @@ pi syn =

1114 st <- static

1128 st <- static

1115 explicitPi opts st syn

1129 explicitPi opts st syn

1116 <|> try (do lchar '{'; implicitPi opts st syn)

1130 <|> try (do lchar '{'; implicitPi opts st syn)

1131+ <|> if constraintAllowed syn

1132+ then try (constraintPi opts st syn)

1117− <|> unboundPi opts st syn

1133+ <|> unboundPi opts st syn

1134+ else unboundPi opts st syn

1118 <?> "dependent type signature"

1135 <?> "dependent type signature"

1119

1136

1120{- | Parses Possible Options for Pi Expressions

1137{- | Parses Possible Options for Pi Expressions

test/interfaces005/interfaces005.idr+9−6

@@ -2,11 +2,14 @@ module Set

3public export

4interface SetSig a where

5− data Set : Type -> Type

5+ data SetT : Type -> Type

7− new : Set a

7+ new : SetT a

8− insert : a -> Set a -> Set a

8+ insert : a -> SetT a -> SetT a

9− member : a -> Set a -> Bool

9+ member : a -> SetT a -> Bool

10+

11+Set : (a : Type) -> SetSig a => Type

12+Set (a) @{sig} = SetT @{sig} a

11data Tree a = Leaf | Node (Tree a) a (Tree a)

14data Tree a = Leaf | Node (Tree a) a (Tree a)

@@ -17,7 +20,7 @@ namespace TreeSet

17 export

20 export

18 [TreeSet] Ord a => SetSig a where

21 [TreeSet] Ord a => SetSig a where

20− Set = Tree

23+ SetT = Tree

22 new = Leaf

25 new = Leaf

@@ -35,7 +38,7 @@ namespace TreeSet

36using implementation TreeSet

39using implementation TreeSet

38− test : Set @{TreeSet {a=Nat}} Nat

41+ test : Set Nat

39 test = insert 3 $

42 test = insert 3 $

40 insert 2 $

43 insert 2 $

41 insert 7 $

44 insert 7 $