7c34217 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow class constraints to be named

Like so: foo : (c : Show a) => List a -> String This means that type classes can be used as indices/parameteres of data types (e.g. to ensure a dictionary is unchanging across a structure). Fixes #646

commit7c34217af9dca228704714fef76237064ab51bb1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 1 Jan 2015, 22:51 (12 years ago) parentee32989

11 files changed+41−22

compare with master

unifiedsplit

idris.cabal+3 src/Idris/AbsSyntax.hs+2−2 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Elab/Class.hs+7−7 src/Idris/Elab/Instance.hs+4−3 src/Idris/IBC.hs+1−1 src/Idris/ParseExpr.hs+10−5 src/Idris/Parser.hs+1−2 test/reg057/expected test/reg057/reg057.idr+8 test/reg057/run+3

idris.cabal+3

@@ -283,6 +283,9 @@ Extra-source-files:

283283 test/reg056/run

284284 test/reg056/*.idr

285285 test/reg056/expected

286+ test/reg057/run

287+ test/reg057/*.idr

288+ test/reg057/expected

286289

287290 test/basic001/run

288291 test/basic001/*.idr

src/Idris/AbsSyntax.hs+2−2

@@ -1037,14 +1037,14 @@ expandParamsD rhs ist dec ps ns (PMutual f pds)

10371037 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

10381038expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)

10391039 = PClass doc info f

1040− (map (expandParams dec ps ns []) cs)

1040+ (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

10411041 n

10421042 (map (mapsnd (expandParams dec ps ns [])) params)

10431043 pDocs

10441044 (map (expandParamsD rhs ist dec ps ns) decls)

10451045expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)

10461046 = PInstance info f

1047− (map (expandParams dec ps ns []) cs)

1047+ (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

10481048 n

10491049 (map (expandParams dec ps ns []) params)

10501050 (expandParams dec ps ns [] ty)

src/Idris/AbsSyntaxTree.hs+2−2

@@ -558,14 +558,14 @@ data PDecl' t

558558 | PNamespace String [PDecl' t] -- ^ New namespace

559559 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration

560560 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

561− [t] -- constraints

561+ [(Name, t)] -- constraints

562562 Name

563563 [(Name, t)] -- parameters

564564 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

565565 [PDecl' t] -- declarations

566566 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

567567 -- class name, parameters, method declarations

568− | PInstance SyntaxInfo FC [t] -- constraints

568+ | PInstance SyntaxInfo FC [(Name, t)] -- constraints

569569 Name -- class

570570 [t] -- parameters

571571 t -- full instance type

src/Idris/Elab/Class.hs+7−7

@@ -53,7 +53,7 @@ import Util.Pretty(pretty, text)

5353data MArgTy = IA | EA | CA deriving Show

5454

5555elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

56− FC -> [PTerm] ->

56+ FC -> [(Name, PTerm)] ->

5757 Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [PDecl] -> Idris ()

5858elabClass info syn_in doc fc constraints tn ps pDocs ds

5959 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

@@ -115,7 +115,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

115115 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

116116 i <- getIState

117117 let t = PApp fc (PRef fc n) (map pexp ps)

118− let isConstrained = any (== t) constraints

118+ let isConstrained = any (== t) (map snd constraints)

119119 when (not isConstrained) . tclift

120120 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

121121 return ()

@@ -124,8 +124,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

124124 impbind [] x = x

125125 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

126126

127− conbind :: [PTerm] -> PTerm -> PTerm

128− conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

127+ conbind :: [(Name, PTerm)] -> PTerm -> PTerm

128+ conbind ((c, ty) : ns) x = PPi constraint c ty (conbind ns x)

129129 conbind [] x = x

130130

131131 getMName (PTy _ _ _ _ _ n _) = nsroot n

@@ -160,15 +160,15 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

160160 clause _ = False

161161

162162 -- Generate a function for chasing a dictionary constraint

163− cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> PTerm -> Idris [PDecl' PTerm]

164− cfun cn c syn all con

163+ cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> (Name, PTerm) -> Idris [PDecl' PTerm]

164+ cfun cn c syn all (cnm, con)

165165 = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

166166 -- SN (ParentN cn (show con))

167167 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

168168 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

169169 let lhs = PApp fc (PRef fc cfn) [pconst capp]

170170 let rhs = PResolveTC (fileFC "HACK")

171− let ty = PPi constraint (sMN 0 "pc") c con

171+ let ty = PPi constraint cnm c con

172172 iLOG (showTmImpls ty)

173173 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

174174 i <- getIState

src/Idris/Elab/Instance.hs+4−3

@@ -52,7 +52,7 @@ import Util.Pretty(pretty, text)

5252

5353elabInstance :: ElabInfo -> SyntaxInfo ->

5454 ElabWhat -> -- phase

55− FC -> [PTerm] -> -- constraints

55+ FC -> [(Name, PTerm)] -> -- constraints

5656 Name -> -- the class

5757 [PTerm] -> -- class parameters (i.e. instance)

5858 PTerm -> -- full instance type

@@ -225,10 +225,11 @@ elabInstance info syn what fc cs n ps t expn ds = do

225225

226226 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

227227

228− conbind (ty : ns) x = PPi (constraint) -- { pstatic = Dynamic })

229− (sMN 0 "class") ty (conbind ns x)

228+ conbind :: [(Name, PTerm)] -> PTerm -> PTerm

229+ conbind ((c,ty) : ns) x = PPi constraint c ty (conbind ns x)

230230 conbind [] x = x

231231

232+ coninsert :: [(Name, PTerm)] -> PTerm -> PTerm

232233 coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

233234 coninsert cs sc = conbind cs sc

234235

src/Idris/IBC.hs+1−1

@@ -33,7 +33,7 @@ import Codec.Compression.Zlib (compress)

3333import Util.Zlib (decompressEither)

3434

3535ibcVersion :: Word8

36−ibcVersion = 89

36+ibcVersion = 90

3737

3838data IBCFile = IBCFile { ver :: Word8,

3939 sourcefile :: FilePath,

src/Idris/ParseExpr.hs+10−5

@@ -731,8 +731,7 @@ TypeExpr ::= ConstraintList? Expr;

731731typeExpr :: SyntaxInfo -> IdrisParser PTerm

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

733733 sc <- expr syn

734− return (bindList (PPi constraint)

735− (map (\x -> (sMN 0 "constrarg", x)) cs) sc)

734+ return (bindList (PPi constraint) cs sc)

736735 <?> "type signature"

737736

738737{- | Parses a lambda expression

@@ -913,17 +912,23 @@ ConstraintList ::=

913912 ;

914913@

915914-}

916−constraintList :: SyntaxInfo -> IdrisParser [PTerm]

915+constraintList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

917916constraintList syn = try (do lchar '('

918− tys <- sepBy1 (expr' (disallowImp syn)) (lchar ',')

917+ tys <- sepBy1 nexpr (lchar ',')

919918 lchar ')'

920919 reservedOp "=>"

921920 return tys)

922921 <|> try (do t <- expr (disallowImp syn)

923922 reservedOp "=>"

924− return [t])

923+ return [(defname, t)])

925924 <|> return []

926925 <?> "type constraint list"

926+ where nexpr = try (do n <- name; lchar ':'

927+ e <- expr' (disallowImp syn)

928+ return (n, e))

929+ <|> do e <- expr' (disallowImp syn)

930+ return (defname, e)

931+ defname = sMN 0 "constrarg"

927932

928933{- | Parses a type declaration list

929934@

src/Idris/Parser.hs+1−2

@@ -640,8 +640,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

640640 cn <- fnName

641641 args <- many (simpleExpr syn)

642642 let sc = PApp fc (PRef fc cn) (map pexp args)

643− let t = bindList (PPi constraint)

644− (map (\x -> (sMN 0 "constraint", x)) cs) sc

643+ let t = bindList (PPi constraint) cs sc

645644 ds <- option [] (instanceBlock syn)

646645 return [PInstance syn fc cs cn args t en ds]

647646 <?> "instance declaration"

test/reg057/expectednew file

No changes to the content.

test/reg057/reg057.idrnew file+8

@@ -0,0 +1,8 @@

1+module Foo

3+data CrappySet : (a : Type) -> Ord a -> Type where

4+ Empty : (inst : Ord a) => CrappySet a inst

5+ Item : (inst : Ord a) => a -> CrappySet a inst -> CrappySet a inst

7+empty : (inst : Ord a) => CrappySet a inst

test/reg057/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ reg057.idr --check

3+rm -f *.ibc