f2459a5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added class constraints

f2459a5Edwin Brady15 years ago

lib/builtins.idr+1−1

compare with master

unifiedsplit

@@ -100,7 +100,7 @@ instance EqFloat = instanceEq (boolOp prim__eqFloat) (\x, y => not (x == y));

100

101data Ordering = LT | EQ | GT;

102

103−class Ord a where {

103+class Eq a => Ord a where {

104 compare : a -> a -> Ordering;

105}

106

lib/nat.idr+18

@@ -21,6 +21,24 @@ mult (S k) y = plus y (mult k y);

21instance numNat : Num Nat;

22instance numNat = instanceNum plus sub mult;

24+instance EqNat : Eq Nat;

25+instance EqNat = instanceEq eqNat (\x, y => not (x == y)) where {

26+ eqNat : Nat -> Nat -> Bool;

27+ eqNat O O = True;

28+ eqNat (S x) (S y) = eqNat x y;

29+ eqNat O (S y) = False;

30+ eqNat (S x) O = False;

31+}

32+

33+instance OrdNat : Ord Nat;

34+instance OrdNat = instanceOrd cmpNat where {

35+ cmpNat : Nat -> Nat -> Ordering;

36+ cmpNat O O = EQ;

37+ cmpNat O (S k) = LT;

38+ cmpNat (S k) O = GT;

39+ cmpNat (S x) (S y) = cmpNat x y;

40+}

41+

24plusnO : (m : Nat) -> m + O = m;

42plusnO : (m : Nat) -> m + O = m;

25plusnO O = refl;

43plusnO O = refl;

26plusnO (S k) = eqRespS (plusnO k);

44plusnO (S k) = eqRespS (plusnO k);

src/Idris/AbsSyntax.hs+5−3

@@ -185,7 +185,9 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

185 | PClauses FC Name [PClause' t] -- pattern clause

186 | PData SyntaxInfo FC (PData' t) -- data declaration

187 | PParams FC [(Name, t)] [PDecl' t] -- params block

188− | PClass SyntaxInfo FC Name

188+ | PClass SyntaxInfo FC

189+ [t] -- constraints

190+ Name

189 [(Name, t)] -- parameters

191 [(Name, t)] -- parameters

190 [PDecl' t] -- declarations

192 [PDecl' t] -- declarations

191 | PInstance SyntaxInfo FC Name t [PDecl' t]

193 | PInstance SyntaxInfo FC Name t [PDecl' t]

@@ -832,8 +834,8 @@ dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (sh

832dumpDecl (PData _ _ d) = showDImp True d

834dumpDecl (PData _ _ d) = showDImp True d

833dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

835dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

834dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

836dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

835−dumpDecl (PClass _ _ n ps ds)

837+dumpDecl (PClass _ _ cs n ps ds)

836− = "class " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

838+ = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

837dumpDecl (PInstance _ _ n t ds)

839dumpDecl (PInstance _ _ n t ds)

838 = "instance " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

840 = "instance " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

839-- dumpDecl (PImport i) = "import " ++ i

841-- dumpDecl (PImport i) = "import " ++ i

src/Idris/ElabDecls.hs+8−5

@@ -281,8 +281,9 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

281 updateLHS n wname mvars ns tm w = fail $ "Not implemented " ++ show tm

282

283elabClass :: ElabInfo -> SyntaxInfo ->

284+ FC -> [PTerm] ->

284− FC -> Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

285+ Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

285−elabClass info syn fc tn ps ds

286+elabClass info syn fc constraints tn ps ds

286 = do let cn = UN ["instance" ++ show tn] -- MN 0 ("instance" ++ show tn)

287 = do let cn = UN ["instance" ++ show tn] -- MN 0 ("instance" ++ show tn)

287 let tty = pibind ps PSet

288 let tty = pibind ps PSet

288 let constraint = PApp fc (PRef fc tn)

289 let constraint = PApp fc (PRef fc tn)

@@ -290,7 +291,7 @@ elabClass info syn fc tn ps ds

290 -- build data declaration

291 -- build data declaration

291 ims <- mapM tdecl ds

292 ims <- mapM tdecl ds

292 let (methods, imethods) = unzip ims

293 let (methods, imethods) = unzip ims

293− let cty = impbind ps $ pibind methods constraint

294+ let cty = impbind ps $ conbind constraints $ pibind methods constraint

294 let cons = [(cn, cty, fc)]

295 let cons = [(cn, cty, fc)]

295 let ddecl = PData syn fc (PDatadecl tn tty cons)

296 let ddecl = PData syn fc (PDatadecl tn tty cons)

296 elabDecl info ddecl

297 elabDecl info ddecl

@@ -304,6 +305,8 @@ elabClass info syn fc tn ps ds

304 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

305 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

305 impbind [] x = x

306 impbind [] x = x

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

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

308+ conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

309+ conbind [] x = x

307

310

308 tdecl (PTy syn _ n t) = do t' <- implicit syn n t

311 tdecl (PTy syn _ n t) = do t' <- implicit syn n t

309 return ( (n, (toExp (map fst ps) Exp t')),

312 return ( (n, (toExp (map fst ps) Exp t')),

@@ -400,8 +403,8 @@ elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

400 newb = addAlist dsParams (inblock info) in

403 newb = addAlist dsParams (inblock info) in

401 info { params = newps,

404 info { params = newps,

402 inblock = newb }

405 inblock = newb }

403−elabDecl' info (PClass s f n ps ds) = do iLOG $ "Elaborating class " ++ show n

406+elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show n

404− elabClass info s f n ps ds

407+ elabClass info s f cs n ps ds

405elabDecl' info (PInstance s f n t ds) = do iLOG $ "Elaborating instance " ++ show n

408elabDecl' info (PInstance s f n t ds) = do iLOG $ "Elaborating instance " ++ show n

406 elabInstance info s f n t ds

409 elabInstance info s f n t ds

407

410

src/Idris/Parser.hs+3−2

@@ -145,7 +145,7 @@ collect (c@(PClauses _ _ _) : ds)

145 getfc (PClauses fc _ _) = fc

146

147collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

148−collect (PClass f s n ps ds : ds') = PClass f s n ps (collect ds) : collect ds'

148+collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'

149collect (PInstance f s n t ds : ds') = PInstance f s n t (collect ds) : collect ds'

150collect (d : ds) = d : collect ds

151collect [] = []

@@ -287,12 +287,13 @@ fixity = try (do reserved "infixl"; return Infixl)

287pClass :: SyntaxInfo -> IParser [PDecl]

288pClass syn = do reserved "class"

289 fc <- pfc

290+ cons <- pConstList syn

290 n <- pName

291 n <- pName

291 cs <- many1 carg

292 cs <- many1 carg

292 reserved "where"; lchar '{'

293 reserved "where"; lchar '{'

293 ds <- many1 $ pFunDecl syn;

294 ds <- many1 $ pFunDecl syn;

294 lchar '}'

295 lchar '}'

295− return [PClass syn fc n cs (concat ds)]

296+ return [PClass syn fc cons n cs (concat ds)]

296 where

297 where

297 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

298 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

298 return (i, ty)

299 return (i, ty)