13d08bd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Elaborating class declarations

13d08bdEdwin Brady15 years ago

lib/builtins.idr+18−37

compare with master

unifiedsplit

@@ -75,56 +75,37 @@ intToBool x = True;

75boolOp : (a -> a -> Int) -> a -> a -> Bool;

76boolOp op x y = intToBool (op x y);

78−data Num : Set -> Set where

78+class Num a where {

79− NumInstance : (plus : a -> a -> a) ->

80− (sub : a -> a -> a) ->

81− (mult : a -> a -> a) ->

82− Num a;

83−

84− (+) : Num a => a -> a -> a;

79+ (+) : a -> a -> a;

85− (+) @{ NumInstance p s m } x y = p x y;

86−

87− (-) : Num a => a -> a -> a;

80+ (-) : a -> a -> a;

88− (-) @{ NumInstance p s m } x y = s x y;

89−

90− (*) : Num a => a -> a -> a;

81+ (*) : a -> a -> a;

91− (*) @{ NumInstance p s m } x y = m x y;

82+}

93instance numInt : Num Int;

84instance numInt : Num Int;

94−instance numInt = NumInstance prim__addInt prim__subInt prim__mulInt;

85+instance numInt = instanceNum prim__addInt prim__subInt prim__mulInt;

96instance numFloat : Num Float;

87instance numFloat : Num Float;

97−instance numFloat = NumInstance prim__addFloat prim__subFloat prim__mulFloat;

88+instance numFloat = instanceNum prim__addFloat prim__subFloat prim__mulFloat;

98−

99−data Eq : Set -> Set where

100− EqInstance : (eq : a -> a -> Bool) ->

101− (neq : a -> a -> Bool) ->

102− Eq a;

103

104− (==) : Eq a => a -> a -> Bool;

90+class Eq a where {

105− (==) @{ EqInstance eq neq } x y = eq x y;

91+ (==) : a -> a -> Bool;

106−

107− (/=) : Eq a => a -> a -> Bool;

92+ (/=) : a -> a -> Bool;

108− (/=) @{ EqInstance eq neq } x y = neq x y;

93+}

109

110instance EqInt : Eq Int;

95instance EqInt : Eq Int;

111−instance EqInt = EqInstance (boolOp prim__eqInt) (\x, y => not (x == y));

96+instance EqInt = instanceEq (boolOp prim__eqInt) (\x, y => not (x == y));

112

113instance EqFloat : Eq Float;

98instance EqFloat : Eq Float;

114−instance EqFloat = EqInstance (boolOp prim__eqFloat) (\x, y => not (x == y));

99+instance EqFloat = instanceEq (boolOp prim__eqFloat) (\x, y => not (x == y));

115

100

116data Ordering = LT | EQ | GT;

101data Ordering = LT | EQ | GT;

117

102

118−data Ord : Set -> Set where

103+class Ord a where {

119− OrdInstance : Eq a =>

104+ compare : a -> a -> Ordering;

120− (compare : a -> a -> Ordering) ->

105+}

121− Ord a;

122−

123− compare : Ord a => a -> a -> Ordering;

124− compare @{ OrdInstance c } = c;

125

106

126instance OrdInt : Ord Int;

107instance OrdInt : Ord Int;

127−instance OrdInt = OrdInstance cmpInt where {

108+instance OrdInt = instanceOrd cmpInt where {

128 cmpInt : Int -> Int -> Ordering;

109 cmpInt : Int -> Int -> Ordering;

129 cmpInt x y = if (x == y) then EQ else

110 cmpInt x y = if (x == y) then EQ else

130 if (boolOp prim__ltInt x y) then LT else

111 if (boolOp prim__ltInt x y) then LT else

@@ -132,7 +113,7 @@ instance OrdInt = OrdInstance cmpInt where {

132}

113}

133

114

134instance OrdFloat : Ord Float;

115instance OrdFloat : Ord Float;

135−instance OrdFloat = OrdInstance cmpFloat where {

116+instance OrdFloat = instanceOrd cmpFloat where {

136 cmpFloat : Float -> Float -> Ordering;

117 cmpFloat : Float -> Float -> Ordering;

137 cmpFloat x y = if (x == y) then EQ else

118 cmpFloat x y = if (x == y) then EQ else

138 if (boolOp prim__ltFloat x y) then LT else

119 if (boolOp prim__ltFloat x y) then LT else

lib/nat.idr+1−1

@@ -19,7 +19,7 @@ mult O y = O;

19mult (S k) y = plus y (mult k y);

21instance numNat : Num Nat;

22−instance numNat = NumInstance plus sub mult;

22+instance numNat = instanceNum plus sub mult;

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

25plusnO O = refl;

lib/prelude.idr+16−9

@@ -7,33 +7,40 @@ import io;

8-- Show and instances

10−data Show : Set -> Set where

10+class Show a where {

11− ShowInstance : (show : a -> String) -> Show a;

11+ show : a -> String;

12−

12+}

13−show : Show a => a -> String;

14−show @{ShowInstance s} v = s v;

16instance showNat : Show Nat;

14instance showNat : Show Nat;

17−instance showNat = ShowInstance show where {

15+instance showNat = instanceShow show where {

18 show : Nat -> String;

16 show : Nat -> String;

19 show O = "O";

17 show O = "O";

20 show (S k) = "s" ++ show k;

18 show (S k) = "s" ++ show k;

21}

19}

21+{-

22+

23+instance Show Nat where {

24+ show O = "O";

25+ show (S k) = "s" ++ show k;

26+}

27+

28+-}

29+

23instance showInt : Show Int;

30instance showInt : Show Int;

24−instance showInt = ShowInstance show where {

31+instance showInt = instanceShow show where {

25 show : Int -> String;

32 show : Int -> String;

26 show = prim__intToStr;

33 show = prim__intToStr;

27}

34}

29instance showFloat : Show Float;

36instance showFloat : Show Float;

30−instance showFloat = ShowInstance show where {

37+instance showFloat = instanceShow show where {

31 show : Float -> String;

38 show : Float -> String;

32 show = prim__floatToStr;

39 show = prim__floatToStr;

33}

40}

35instance showList : Show a => Show (List a);

42instance showList : Show a => Show (List a);

36−instance showList = ShowInstance lshow where {

43+instance showList = instanceShow lshow where {

37 lshow : Show a => List a -> String;

44 lshow : Show a => List a -> String;

38 lshow xs = "[" ++ show' xs ++ "]" where {

45 lshow xs = "[" ++ show' xs ++ "]" where {

39 show' : Show a => List a -> String;

46 show' : Show a => List a -> String;

src/Idris/AbsSyntax.hs+8−5

@@ -31,6 +31,7 @@ data IState = IState { tt_ctxt :: Context,

31 idris_infixes :: [FixDecl],

32 idris_implicits :: Ctxt [PArg],

33 idris_statics :: Ctxt [Bool],

34+ idris_classes :: Ctxt [Name],

34 idris_log :: String,

35 idris_log :: String,

35 idris_options :: IOption,

36 idris_options :: IOption,

36 idris_name :: Int,

37 idris_name :: Int,

@@ -42,7 +43,7 @@ data IState = IState { tt_ctxt :: Context,

42 errLine :: Maybe Int

43 errLine :: Maybe Int

43 }

44 }

45−idrisInit = IState emptyContext [] emptyContext emptyContext

46+idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext

46 "" defaultOpts 6 [] [] [] [] [] Nothing

47 "" defaultOpts 6 [] [] [] [] [] Nothing

48-- The monad for the main REPL - reading and processing files and updating

49-- The monad for the main REPL - reading and processing files and updating

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

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

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

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

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

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

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

187− | PClass FC Name

188+ | PClass SyntaxInfo FC Name

188 [(Name, t)] -- parameters

189 [(Name, t)] -- parameters

189 [PDecl' t] -- declarations

190 [PDecl' t] -- declarations

190− | PInstance FC Name t [PDecl' t]

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

191 | PSyntax FC Syntax

192 | PSyntax FC Syntax

192 deriving Functor

193 deriving Functor

193

194

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

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

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

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

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

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

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

835+dumpDecl (PClass _ _ n ps ds)

834−dumpDecl (PClass _ n ps ds) = "class " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

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

837+dumpDecl (PInstance _ _ n t ds)

835−dumpDecl (PInstance _ n t ds) = "instance " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

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

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

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

837

840

838-- syntactic match of a against b, returning pair of variables in a

841-- syntactic match of a against b, returning pair of variables in a

src/Idris/ElabDecls.hs+81

@@ -280,6 +280,81 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

280 PApp fc (PRef fc' wname) (map (pexp . (PRef fc')) ns ++ [pexp w])

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

282

283+elabClass :: ElabInfo -> SyntaxInfo ->

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

285+elabClass info syn fc tn ps ds

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

287+ let tty = pibind ps PSet

288+ let constraint = PApp fc (PRef fc tn)

289+ (map (pexp . PRef fc) (map fst ps))

290+ -- build data declaration

291+ ims <- mapM tdecl ds

292+ let (methods, imethods) = unzip ims

293+ let cty = impbind ps $ pibind methods constraint

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

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

296+ elabDecl info ddecl

297+ -- for each method, build a top level function

298+ fns <- mapM (tfun cn constraint (map fst imethods)) imethods

299+ mapM_ (elabDecl info) (concat fns)

300+ i <- get

301+ put (i { idris_classes = addDef tn (map fst methods) (idris_classes i) })

302+ where

303+ pibind [] x = x

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

305+ impbind [] x = x

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

307+

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

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

310+ (n, (toExp (map fst ps) Imp t')) )

311+ tdecl (PClauses _ _ _) = fail "No default definitions allowed yet"

312+ tdecl _ = fail "Not allowed in a class declaration"

313+

314+ tfun cn c all (m, ty)

315+ = do let ty' = insertConstraint c ty

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

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

318+ let margs = getMArgs ty

319+ let anames = map (\x -> MN x "arg") [0..]

320+ let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

321+ let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

322+ iLOG (showImp True ty)

323+ iLOG (show (m, ty', capp, margs))

324+ iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

325+ return [PTy syn fc m ty',

326+ PClauses fc m [PClause m lhs [] rhs []]]

327+

328+ getMArgs (PPi (Imp _ _) n ty sc) = False : getMArgs sc

329+ getMArgs (PPi (Exp _ _) n ty sc) = True : getMArgs sc

330+ getMArgs _ = []

331+

332+ getMeth (m:ms) (a:as) x | x == a = PRef fc m

333+ | otherwise = getMeth ms as x

334+

335+ lhsArgs (True : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns

336+ lhsArgs (False : xs) ns = lhsArgs xs ns

337+ lhsArgs [] _ = []

338+

339+ rhsArgs (True : xs) (n : ns) = pexp (PRef fc n) : rhsArgs xs ns

340+ rhsArgs (False : xs) ns = pexp Placeholder : rhsArgs xs ns

341+ rhsArgs [] _ = []

342+

343+ insertConstraint c (PPi p@(Imp _ _) n ty sc)

344+ = PPi p n ty (insertConstraint c sc)

345+ insertConstraint c sc = PPi constraint (MN 0 "c") c sc

346+

347+ -- make arguments explicit and don't bind class parameters

348+ toExp ns e (PPi (Imp l s) n ty sc)

349+ | n `elem` ns = toExp ns e sc

350+ | otherwise = PPi (e l s) n ty (toExp ns e sc)

351+ toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

352+ toExp ns e sc = sc

353+

354+elabInstance :: ElabInfo -> SyntaxInfo ->

355+ FC -> Name -> PTerm -> [PDecl] -> Idris ()

356+elabInstance info syn fc n t ds = fail "Not implemented"

357+

283pbinds (Bind n (PVar t) sc) = do attack; patbind n

358pbinds (Bind n (PVar t) sc) = do attack; patbind n

284 pbinds sc

359 pbinds sc

285pbinds tm = return ()

360pbinds tm = return ()

@@ -325,6 +400,12 @@ elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

325 newb = addAlist dsParams (inblock info) in

400 newb = addAlist dsParams (inblock info) in

326 info { params = newps,

401 info { params = newps,

327 inblock = newb }

402 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

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

406+ elabInstance info s f n t ds

407+

408+

328-- elabDecl' info (PImport i) = loadModule i

409-- elabDecl' info (PImport i) = loadModule i

329

410

330

411

src/Idris/Parser.hs+4−4

@@ -145,8 +145,8 @@ 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 n ps ds : ds') = PClass f n ps (collect ds) : collect ds'

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

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

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

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

151collect [] = []

152

@@ -292,7 +292,7 @@ pClass syn = do reserved "class"

292 reserved "where"; lchar '{'

293 ds <- many1 $ pFunDecl syn;

294 lchar '}'

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

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

296 where

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

298 return (i, ty)

@@ -310,7 +310,7 @@ pInstance syn = do reserved "instance"

310 reserved "where"; lchar '{'

311 ds <- many1 $ pFunDecl syn;

312 lchar '}'

313− return [PInstance fc cn t (concat ds)]

313+ return [PInstance syn fc cn t (concat ds)]

314

315--------- Expressions ---------

316