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

git.iko.soy/Idris-dev

More flexibility in constraint arguments

They can now appear in the scope of an explicit function type (not just under implicit arguments or at the top level) so they are now allowed anywhere in function types.

commit5a937ccface10d99d31eaf0ad3212247a72923fd authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 11 May 2016, 22:27 (10 years ago) parentec3b4a2

8 files changed+54−29

compare with master

unifiedsplit

CHANGELOG.md+3 libs/contrib/Classes/Verified.idr+1−1 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/DeepSeq.hs+2−2 src/Idris/IBC.hs+5−3 src/Idris/Parser.hs+2−3 src/Idris/Parser/Expr.hs+30−13 test/interfaces005/interfaces005.idr+9−6

CHANGELOG.md+3

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

4343 test x = x <+> x <+> neutral

4444 ```

4545

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

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

48+

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

4750 in a with block directly. For example:

4851

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

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

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

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

3030 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

3232

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

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

src/Idris/AbsSyntaxTree.hs+2−1

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

15491549 decoration :: Name -> Name,

15501550 inPattern :: Bool,

15511551 implicitAllowed :: Bool,

1552+ constraintAllowed :: Bool,

15521553 maxline :: Maybe Int,

15531554 mut_nesting :: Int,

15541555 dsl_info :: DSL,

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

15611562deriving instance Binary SyntaxInfo

15621563!-}

15631564

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

15651566

15661567expandNS :: SyntaxInfo -> Name -> Name

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

src/Idris/DeepSeq.hs+2−2

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

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

685685

686686instance 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)

688688 = rnf x1 `seq`

689689 rnf x2 `seq`

690690 rnf x3 `seq`

691691 rnf x4 `seq`

692692 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` ()

694694

695695instance NFData OutputMode where

696696 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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 141

43+ibcVersion = 142

4444

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

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

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

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

15921592

15931593instance Binary SyntaxInfo where

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

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

15951595 = do put x1

15961596 put x2

15971597 put x3

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

15991599 put x5

16001600 put x6

16011601 put x7

1602+ put x8

16021603 get

16031604 = do x1 <- get

16041605 x2 <- get

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

16071608 x5 <- get

16081609 x6 <- get

16091610 x7 <- get

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

1611+ x8 <- get

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

16111613

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

16131615 put x

src/Idris/Parser.hs+2−3

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

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

12391239 <|> do pushIndent

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

1241− cargs <- many (constraintArg syn)

12421241 fc <- getFC

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

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

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

12451245 wargs <- many (wExpr syn)

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

1247− (cargs ++ args)

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

12481247 (do r <- rhs syn n

12491248 ist <- get

12501249 let ctxt = tt_ctxt ist

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

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

3636

3737-- | Allow implicit type declarations

3838allowImp :: SyntaxInfo -> SyntaxInfo

39−allowImp syn = syn { implicitAllowed = True }

39+allowImp syn = syn { implicitAllowed = True,

40+ constraintAllowed = False }

4041

4142-- | Disallow implicit type declarations

4243disallowImp :: 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 }

4450

4551{-| Parses an expression as a whole

4652@

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

327333@

328334-}

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

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

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

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

332338 return (lhs, r)

333339 <?> "case option"

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

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

433439 <?> "expression"

434440

435−{- |Parses an expression in braces

441+{- |Parses an expression in parentheses

436442@

437443Bracketed ::= '(' Bracketed'

438444@

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

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

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

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

480− <|> do l <- expr syn

481− bracketedExpr syn open l

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

487+ bracketedExpr (allowConstr syn) open l

482488

483489

484490

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

891897 -}

892898typeExpr :: SyntaxInfo -> IdrisParser PTerm

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

894− sc <- expr syn

900+ sc <- expr (allowConstr syn)

895901 return (bindList (PPi constraint) cs sc)

896902 <?> "type signature"

897903

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

916922-}

917923lambda :: SyntaxInfo -> IdrisParser PTerm

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

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

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

920926 fc <- getFC

921927 sc <- lambdaTail

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

923929 <|>

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

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

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

926932 return (fc, e))

927933 (lchar ',')

928934 sc <- lambdaTail

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

10551061explicitPi opts st syn

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

10571063 binder <- bindsymbol opts st syn

1058− sc <- expr syn

1064+ sc <- expr (allowConstr syn)

10591065 return (bindList (PPi binder) xt sc)

10601066

10611067autoImplicit opts st syn

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

10641070 xt <- typeDeclList syn

10651071 lchar '}'

10661072 symbol "->"

1067− sc <- expr syn

1073+ sc <- expr (allowConstr syn)

10681074 highlightP kw AnnKeyword

10691075 return (bindList (PPi

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

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

10781084 xt <- typeDeclList syn

10791085 lchar '}'

10801086 symbol "->"

1081− sc <- expr syn

1087+ sc <- expr (allowConstr syn)

10821088 highlightP kw AnnKeyword

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

10841090

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

10961102 return (bindList (PPi im) xt

10971103 (bindList (PPi cl) cs sc))

10981104

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+

10991113implicitPi opts st syn =

11001114 autoImplicit opts st syn

11011115 <|> defaultImplicit opts st syn

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

11141128 st <- static

11151129 explicitPi opts st syn

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

1117− <|> unboundPi opts st syn

1131+ <|> if constraintAllowed syn

1132+ then try (constraintPi opts st syn)

1133+ <|> unboundPi opts st syn

1134+ else unboundPi opts st syn

11181135 <?> "dependent type signature"

11191136

11201137{- | Parses Possible Options for Pi Expressions

test/interfaces005/interfaces005.idr+9−6

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

33public export

44interface SetSig a where

5− data Set : Type -> Type

5+ data SetT : Type -> Type

7− new : Set a

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

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

7+ new : SetT a

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

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

10+

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

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

1013

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

1215

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

1720 export

1821 [TreeSet] Ord a => SetSig a where

1922

20− Set = Tree

23+ SetT = Tree

2124

2225 new = Leaf

2326

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

3538

3639using implementation TreeSet

3740

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

41+ test : Set Nat

3942 test = insert 3 $

4043 insert 2 $

4144 insert 7 $