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

idris.cabal+3

compare with master

unifiedsplit

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

283 test/reg056/run

284 test/reg056/*.idr

285 test/reg056/expected

286+ test/reg057/run

287+ test/reg057/*.idr

288+ test/reg057/expected

286

289

287 test/basic001/run

290 test/basic001/run

288 test/basic001/*.idr

291 test/basic001/*.idr

src/Idris/AbsSyntax.hs+2−2

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

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

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

1039 = PClass doc info f

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

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

1041 n

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

1043 pDocs

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

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

1046 = PInstance info f

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

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

1048 n

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

1050 (expandParams dec ps ns [] ty)

src/Idris/AbsSyntaxTree.hs+2−2

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

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

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

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

561− [t] -- constraints

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

562 Name

563 [(Name, t)] -- parameters

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

565 [PDecl' t] -- declarations

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

567 -- class name, parameters, method declarations

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

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

569 Name -- class

570 [t] -- parameters

571 t -- full instance type

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

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

53data MArgTy = IA | EA | CA deriving Show

54

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

56− FC -> [PTerm] ->

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

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

58elabClass info syn_in doc fc constraints tn ps pDocs ds

59 = 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

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

116 i <- getIState

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

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

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

119 when (not isConstrained) . tclift

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

121 return ()

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

124 impbind [] x = x

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

126

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

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

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

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

129 conbind [] x = x

130

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

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

160 clause _ = False

161

162 -- Generate a function for chasing a dictionary constraint

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

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

164− cfun cn c syn all con

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

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

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

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

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

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

170 let rhs = PResolveTC (fileFC "HACK")

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

171+ let ty = PPi constraint cnm c con

172 iLOG (showTmImpls ty)

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

174 i <- getIState

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

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

52

53elabInstance :: ElabInfo -> SyntaxInfo ->

54 ElabWhat -> -- phase

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

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

56 Name -> -- the class

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

58 PTerm -> -- full instance type

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

225

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

227

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

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

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

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

230 conbind [] x = x

231

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

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

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

233 coninsert cs sc = conbind cs sc

234 coninsert cs sc = conbind cs sc

234

235

src/Idris/IBC.hs+1−1

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

33import Util.Zlib (decompressEither)

34

35ibcVersion :: Word8

36−ibcVersion = 89

36+ibcVersion = 90

37

38data IBCFile = IBCFile { ver :: Word8,

39 sourcefile :: FilePath,

src/Idris/ParseExpr.hs+10−5

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

731typeExpr :: SyntaxInfo -> IdrisParser PTerm

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

733 sc <- expr syn

734− return (bindList (PPi constraint)

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

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

736 <?> "type signature"

735 <?> "type signature"

737

736

738{- | Parses a lambda expression

737{- | Parses a lambda expression

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

913 ;

912 ;

914@

913@

915-}

914-}

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

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

917constraintList syn = try (do lchar '('

916constraintList syn = try (do lchar '('

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

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

919 lchar ')'

918 lchar ')'

920 reservedOp "=>"

919 reservedOp "=>"

921 return tys)

920 return tys)

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

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

923 reservedOp "=>"

922 reservedOp "=>"

924− return [t])

923+ return [(defname, t)])

925 <|> return []

924 <|> return []

926 <?> "type constraint list"

925 <?> "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"

927

932

928{- | Parses a type declaration list

933{- | Parses a type declaration list

929@

934@

src/Idris/Parser.hs+1−2

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

640 cn <- fnName

641 args <- many (simpleExpr syn)

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

643− let t = bindList (PPi constraint)

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

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

645 ds <- option [] (instanceBlock syn)

644 ds <- option [] (instanceBlock syn)

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

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

647 <?> "instance declaration"

646 <?> "instance declaration"

test/reg057/expectednew file

No changes to the content.

test/reg057/reg057.idrnew file+8

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

1+module Foo

2+

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

6+

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

8+

test/reg057/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ reg057.idr --check

3+rm -f *.ibc