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

CHANGELOG+1

compare with master

unifiedsplit

@@ -4,6 +4,7 @@ New in 0.9.8:

4User visible changes:

5

6* Added "rewrite ... in ..." construct

7+* Allow type class constraints in 'using' clauses

7* Renamed EFF to EFFECT in Effect package

8* Renamed EFF to EFFECT in Effect package

8* Experimental Java backend

9* Experimental Java backend

9* Tab completion in REPL

10* Tab completion in REPL

src/Idris/AbsSyntax.hs+44−1

@@ -733,6 +733,45 @@ addStatics n tm ptm =

733

734-- Dealing with implicit arguments

735

736+-- Add constraint bindings from using block

737+

738+addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm

739+addUsingConstraints syn fc t

740+ = do ist <- get

741+ let ns = namesIn [] ist t

742+ let cs = getConstraints t -- check declared constraints

743+ let addconsts = uconsts \\ cs

744+ -- if all names in the arguments of addconsts appear in ns,

745+ -- add the constraint implicitly

746+ return (doAdd addconsts ns t)

747+ where uconsts = filter uconst (using syn)

748+ uconst (UConstraint _ _) = True

749+ uconst _ = False

750+

751+ doAdd [] _ t = t

752+ -- if all of args in ns, then add it

753+ doAdd (UConstraint c args : cs) ns t

754+ | all (\n -> elem n ns) args

755+ = PPi (Constraint False Dynamic "") (MN 0 "cu")

756+ (mkConst c args) (doAdd cs ns t)

757+ | otherwise = doAdd cs ns t

758+

759+ mkConst c args = PApp fc (PRef fc c)

760+ (map (\n -> PExp 0 False (PRef fc n) "") args)

761+

762+ getConstraints (PPi (Constraint _ _ _) _ c sc)

763+ = getcapp c ++ getConstraints sc

764+ getConstraints (PPi _ _ c sc) = getConstraints sc

765+ getConstraints _ = []

766+

767+ getcapp (PApp _ (PRef _ c) args)

768+ = do ns <- mapM getName args

769+ return (UConstraint c ns)

770+ getcapp _ = []

771+

772+ getName (PExp _ _ (PRef _ n) _) = return n

773+ getName _ = []

774+

736-- Add implicit Pi bindings for any names in the term which appear in an

775-- Add implicit Pi bindings for any names in the term which appear in an

737-- argument position.

776-- argument position.

738

777

@@ -762,9 +801,13 @@ implicitise syn ignore ist tm

762 then (tm, reverse declimps)

801 then (tm, reverse declimps)

763 else implicitise syn ignore ist (pibind uvars ns tm)

802 else implicitise syn ignore ist (pibind uvars ns tm)

764 where

803 where

765− uvars = using syn

804+ uvars = map ipair (filter uimplicit (using syn))

766 pvars = syn_params syn

805 pvars = syn_params syn

767

806

807+ ipair (UImplicit x y) = (x, y)

808+ uimplicit (UImplicit _ _) = True

809+ uimplicit _ = False

810+

768 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys

811 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys

769 | otherwise = x : dropAll xs ys

812 | otherwise = x : dropAll xs ys

770 dropAll [] ys = []

813 dropAll [] ys = []

src/Idris/AbsSyntaxTree.hs+8−1

@@ -723,7 +723,14 @@ initDSL = DSL (PRef f (UN ">>="))

723 Nothing

724 where f = FC "(builtin)" 0

725

726+data Using = UImplicit Name PTerm

727+ | UConstraint Name [Name]

728+ deriving (Show, Eq)

729+{-!

730+deriving instance Binary Using

731+!-}

732+

726−data SyntaxInfo = Syn { using :: [(Name, PTerm)],

733+data SyntaxInfo = Syn { using :: [Using],

727 syn_params :: [(Name, PTerm)],

734 syn_params :: [(Name, PTerm)],

728 syn_namespace :: [String],

735 syn_namespace :: [String],

729 no_imp :: [Name],

736 no_imp :: [Name],

src/Idris/ElabDecls.hs+3−1

@@ -49,6 +49,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

49 ctxt <- getContext

50 i <- getIState

51 logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'

52+ ty' <- addUsingConstraints syn fc ty'

52 ty' <- implicit syn n ty'

53 ty' <- implicit syn n ty'

53 let ty = addImpl i ty'

54 let ty = addImpl i ty'

54 logLvl 2 $ show n ++ " type " ++ showImp True ty

55 logLvl 2 $ show n ++ " type " ++ showImp True ty

@@ -922,7 +923,8 @@ elabClass info syn doc fc constraints tn ps ds

922 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl

923 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl

923 -- for each constraint, build a top level function to chase it

924 -- for each constraint, build a top level function to chase it

924 logLvl 5 $ "Building functions"

925 logLvl 5 $ "Building functions"

925− let usyn = syn { using = ps ++ using syn }

926+ let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

927+ ++ using syn }

926 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

928 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

927 mapM_ (elabDecl EAll info) (concat fns)

929 mapM_ (elabDecl EAll info) (concat fns)

928 -- for each method, build a top level function

930 -- for each method, build a top level function

src/Idris/IBC.hs+9

@@ -1096,6 +1096,15 @@ instance (Binary t) => Binary (PDecl' t) where

1096 return (PPostulate x1 x2 x3 x4 x5 x6)

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

1098

1099+instance Binary Using where

1100+ put (UImplicit x1 x2) = do putWord8 0; put x1; put x2

1101+ put (UConstraint x1 x2) = do putWord8 1; put x1; put x2

1102+

1103+ get = do i <- getWord8

1104+ case i of

1105+ 0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)

1106+ 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1107+

1099instance Binary SyntaxInfo where

1108instance Binary SyntaxInfo where

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

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

1101 = do put x1

1110 = do put x1

src/Idris/Parser.hs+14−1

@@ -471,7 +471,7 @@ pPostulate syn = do doc <- option "" (pDocComment '|')

471

472pUsing :: SyntaxInfo -> IParser [PDecl]

473pUsing syn =

474− do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'

474+ do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'

475 openBlock

476 let uvars = using syn

477 ds <- many1 (pDecl (syn { using = uvars ++ ns }))

@@ -1032,6 +1032,19 @@ pConstList syn = try (do lchar '('

1032 return [t])

1033 <|> return []

1034

1035+usingDeclList syn

1036+ = try (sepBy1 (usingDecl syn) (lchar ','))

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

1038+ t <- pTSig (noImp syn)

1039+ return (map (\x -> UImplicit x t) ns)

1040+

1041+usingDecl syn = try (do x <- pfName

1042+ t <- pTSig (noImp syn)

1043+ return (UImplicit x t))

1044+ <|> do c <- pfName

1045+ xs <- many1 pfName

1046+ return (UConstraint c xs)

1047+

1035tyDeclList syn = try (sepBy1 (do x <- pfName

1048tyDeclList syn = try (sepBy1 (do x <- pfName

1036 t <- pTSig (noImp syn)

1049 t <- pTSig (noImp syn)

1037 return (x,t))

1050 return (x,t))

test/README+1

@@ -26,5 +26,6 @@ Tests:

26024: interpreter I/O

27025: memory effects

28026: simple file-I/O-based type provider

29+027: class constraints in using block

29

30

30regxxx: various regression tests

31regxxx: various regression tests

test/test027/expectednew file+3

@@ -0,0 +1,3 @@

1+[1, 1, 3, 5, 5, 8, 9]

2+55

3+3628800

test/test027/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris $@ test027.idr -o test027

3+./test027

4+rm -f test027 *.ibc

test/test027/test027.idrnew file+25

@@ -0,0 +1,25 @@

1+module Main

2+

3+using (Ord a, Num n)

4+

5+ isort : List a -> List a

6+ isort [] = []

7+ isort (x :: xs) = insert x (isort xs)

8+ where -- insert : a -> List a -> List a

9+ insert x [] = [x]

10+ insert x (y :: ys) = if x < y then x :: y :: ys

11+ else y :: insert x ys

12+

13+ msum : Num n => List n -> n

14+ msum [] = 0

15+ msum (x :: xs) = x + msum xs

16+

17+ mprod : List n -> n

18+ mprod [] = 1

19+ mprod (x :: xs) = x * mprod xs

20+

21+main : IO ()

22+main = do print $ isort [1,5,3,5,1,9,8]

23+ print $ msum [1..10]

24+ print $ mprod [1..10]

25+