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

git.iko.soy/Idris-dev

Allow type class constraints in 'using' clauses

e.g. if a using block is given as using (C a b c) block Then any declaration in the block which uses all of a, b and c in its type will have the class constraint C a b c added implicitly. See test027 for an example

commit5b2f0910a9ad403cc38c205241e03de070e50e56 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 16 May 2013, 19:27 (13 years ago) parentd79a445

10 files changed+112−4

compare with master

unifiedsplit

CHANGELOG+1 src/Idris/AbsSyntax.hs+44−1 src/Idris/AbsSyntaxTree.hs+8−1 src/Idris/ElabDecls.hs+3−1 src/Idris/IBC.hs+9 src/Idris/Parser.hs+14−1 test/README+1 test/test027/expected+3 test/test027/run+4 test/test027/test027.idr+25

CHANGELOG+1

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

44User visible changes:

66* Added "rewrite ... in ..." construct

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

78* Renamed EFF to EFFECT in Effect package

89* Experimental Java backend

910* Tab completion in REPL

src/Idris/AbsSyntax.hs+44−1

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

733733

734734-- Dealing with implicit arguments

735735

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+

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

737776-- argument position.

738777

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

762801 then (tm, reverse declimps)

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

764803 where

765− uvars = using syn

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

766805 pvars = syn_params syn

767806

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

808+ uimplicit (UImplicit _ _) = True

809+ uimplicit _ = False

810+

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

769812 | otherwise = x : dropAll xs ys

770813 dropAll [] ys = []

src/Idris/AbsSyntaxTree.hs+8−1

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

723723 Nothing

724724 where f = FC "(builtin)" 0

725725

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

726+data Using = UImplicit Name PTerm

727+ | UConstraint Name [Name]

728+ deriving (Show, Eq)

729+{-!

730+deriving instance Binary Using

731+!-}

732+

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

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

728735 syn_namespace :: [String],

729736 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

4949 ctxt <- getContext

5050 i <- getIState

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

52+ ty' <- addUsingConstraints syn fc ty'

5253 ty' <- implicit syn n ty'

5354 let ty = addImpl i ty'

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

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

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

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

924925 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 }

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

927929 mapM_ (elabDecl EAll info) (concat fns)

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

src/Idris/IBC.hs+9

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

10961096 return (PPostulate x1 x2 x3 x4 x5 x6)

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

10981098

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+

10991108instance Binary SyntaxInfo where

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

11011110 = do put x1

src/Idris/Parser.hs+14−1

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

471471

472472pUsing :: SyntaxInfo -> IParser [PDecl]

473473pUsing syn =

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

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

475475 openBlock

476476 let uvars = using syn

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

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

10321032 return [t])

10331033 <|> return []

10341034

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+

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

10361049 t <- pTSig (noImp syn)

10371050 return (x,t))

test/README+1

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

2626024: interpreter I/O

2727025: memory effects

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

29+027: class constraints in using block

2930

3031regxxx: 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

3+using (Ord a, Num n)

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+