f2459a5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added class constraints

commitf2459a5677a9517f31c3f8c4772eba792e33e1be authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 8 Nov 2011, 14:41 (15 years ago) parent13d08bd

5 files changed+35−11

compare with master

unifiedsplit

lib/builtins.idr+1−1 lib/nat.idr+18 src/Idris/AbsSyntax.hs+5−3 src/Idris/ElabDecls.hs+8−5 src/Idris/Parser.hs+3−2

lib/builtins.idr+1−1

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

100100

101101data Ordering = LT | EQ | GT;

102102

103−class Ord a where {

103+class Eq a => Ord a where {

104104 compare : a -> a -> Ordering;

105105}

106106

lib/nat.idr+18

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

2121instance numNat : Num Nat;

2222instance numNat = instanceNum plus sub mult;

2323

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+

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

2543plusnO O = refl;

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

src/Idris/AbsSyntax.hs+5−3

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

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

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

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

188− | PClass SyntaxInfo FC Name

188+ | PClass SyntaxInfo FC

189+ [t] -- constraints

190+ Name

189191 [(Name, t)] -- parameters

190192 [PDecl' t] -- declarations

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

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

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

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

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

835−dumpDecl (PClass _ _ n ps ds)

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

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

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

837839dumpDecl (PInstance _ _ n t ds)

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

839841-- 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)

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

282282

283283elabClass :: ElabInfo -> SyntaxInfo ->

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

285−elabClass info syn fc tn ps ds

284+ FC -> [PTerm] ->

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

286+elabClass info syn fc constraints tn ps ds

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

287288 let tty = pibind ps PSet

288289 let constraint = PApp fc (PRef fc tn)

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

290291 -- build data declaration

291292 ims <- mapM tdecl ds

292293 let (methods, imethods) = unzip ims

293− let cty = impbind ps $ pibind methods constraint

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

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

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

296297 elabDecl info ddecl

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

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

305306 impbind [] x = x

306307 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

307310

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

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

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

400403 newb = addAlist dsParams (inblock info) in

401404 info { params = newps,

402405 inblock = newb }

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

404− elabClass info s f n ps ds

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

407+ elabClass info s f cs n ps ds

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

406409 elabInstance info s f n t ds

407410

src/Idris/Parser.hs+3−2

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

145145 getfc (PClauses fc _ _) = fc

146146

147147collect (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'

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

150150collect (d : ds) = d : collect ds

151151collect [] = []

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

287287pClass :: SyntaxInfo -> IParser [PDecl]

288288pClass syn = do reserved "class"

289289 fc <- pfc

290+ cons <- pConstList syn

290291 n <- pName

291292 cs <- many1 carg

292293 reserved "where"; lchar '{'

293294 ds <- many1 $ pFunDecl syn;

294295 lchar '}'

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

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

296297 where

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

298299 return (i, ty)