git.iko.soy/Idris-dev
on master help sign in
Elaborating class declarations
commit13d08bd6e22d3e72e2e32d5d59db8cd85fbc8159 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 8 Nov 2011, 14:20 (15 years ago) parent33710ab
6 files changed+128−56
compare with master
unifiedsplit
lib/builtins.idr+18−37 lib/nat.idr+1−1 lib/prelude.idr+16−9 src/Idris/AbsSyntax.hs+8−5 src/Idris/ElabDecls.hs+81 src/Idris/Parser.hs+4−4
lib/builtins.idr+18−37
@@ -75,56 +75,37 @@ intToBool x = True;
7575boolOp : (a -> a -> Int) -> a -> a -> Bool;
7676boolOp op x y = intToBool (op x y);
7777
78−data Num : Set -> Set 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;
85− (+) @{ NumInstance p s m } x y = p x y;
86−
87− (-) : Num a => a -> a -> a;
88− (-) @{ NumInstance p s m } x y = s x y;
89−
90− (*) : Num a => a -> a -> a;
91− (*) @{ NumInstance p s m } x y = m x y;
78+class Num a where {
79+ (+) : a -> a -> a;
80+ (-) : a -> a -> a;
81+ (*) : a -> a -> a;
82+}
9283
9384instance numInt : Num Int;
94−instance numInt = NumInstance prim__addInt prim__subInt prim__mulInt;
85+instance numInt = instanceNum prim__addInt prim__subInt prim__mulInt;
9586
9687instance numFloat : Num Float;
97−instance numFloat = NumInstance 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;
88+instance numFloat = instanceNum prim__addFloat prim__subFloat prim__mulFloat;
10389
104− (==) : Eq a => a -> a -> Bool;
105− (==) @{ EqInstance eq neq } x y = eq x y;
106−
107− (/=) : Eq a => a -> a -> Bool;
108− (/=) @{ EqInstance eq neq } x y = neq x y;
90+class Eq a where {
91+ (==) : a -> a -> Bool;
92+ (/=) : a -> a -> Bool;
93+}
10994
11095instance 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));
11297
11398instance 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));
115100
116101data Ordering = LT | EQ | GT;
117102
118−data Ord : Set -> Set where
119− OrdInstance : Eq a =>
120− (compare : a -> a -> Ordering) ->
121− Ord a;
122−
123− compare : Ord a => a -> a -> Ordering;
124− compare @{ OrdInstance c } = c;
103+class Ord a where {
104+ compare : a -> a -> Ordering;
105+}
125106
126107instance OrdInt : Ord Int;
127−instance OrdInt = OrdInstance cmpInt where {
108+instance OrdInt = instanceOrd cmpInt where {
128109 cmpInt : Int -> Int -> Ordering;
129110 cmpInt x y = if (x == y) then EQ else
130111 if (boolOp prim__ltInt x y) then LT else
@@ -132,7 +113,7 @@ instance OrdInt = OrdInstance cmpInt where {
132113}
133114
134115instance OrdFloat : Ord Float;
135−instance OrdFloat = OrdInstance cmpFloat where {
116+instance OrdFloat = instanceOrd cmpFloat where {
136117 cmpFloat : Float -> Float -> Ordering;
137118 cmpFloat x y = if (x == y) then EQ else
138119 if (boolOp prim__ltFloat x y) then LT else
lib/nat.idr+1−1
@@ -19,7 +19,7 @@ mult O y = O;
1919mult (S k) y = plus y (mult k y);
2020
2121instance numNat : Num Nat;
22−instance numNat = NumInstance plus sub mult;
22+instance numNat = instanceNum plus sub mult;
2323
2424plusnO : (m : Nat) -> m + O = m;
2525plusnO O = refl;
lib/prelude.idr+16−9
@@ -7,33 +7,40 @@ import io;
77
88-- Show and instances
99
10−data Show : Set -> Set where
11− ShowInstance : (show : a -> String) -> Show a;
12−
13−show : Show a => a -> String;
14−show @{ShowInstance s} v = s v;
10+class Show a where {
11+ show : a -> String;
12+}
1513
1614instance showNat : Show Nat;
17−instance showNat = ShowInstance show where {
15+instance showNat = instanceShow show where {
1816 show : Nat -> String;
1917 show O = "O";
2018 show (S k) = "s" ++ show k;
2119}
2220
21+{-
22+
23+instance Show Nat where {
24+ show O = "O";
25+ show (S k) = "s" ++ show k;
26+}
27+
28+-}
29+
2330instance showInt : Show Int;
24−instance showInt = ShowInstance show where {
31+instance showInt = instanceShow show where {
2532 show : Int -> String;
2633 show = prim__intToStr;
2734}
2835
2936instance showFloat : Show Float;
30−instance showFloat = ShowInstance show where {
37+instance showFloat = instanceShow show where {
3138 show : Float -> String;
3239 show = prim__floatToStr;
3340}
3441
3542instance showList : Show a => Show (List a);
36−instance showList = ShowInstance lshow where {
43+instance showList = instanceShow lshow where {
3744 lshow : Show a => List a -> String;
3845 lshow xs = "[" ++ show' xs ++ "]" where {
3946 show' : Show a => List a -> String;
src/Idris/AbsSyntax.hs+8−5
@@ -31,6 +31,7 @@ data IState = IState { tt_ctxt :: Context,
3131 idris_infixes :: [FixDecl],
3232 idris_implicits :: Ctxt [PArg],
3333 idris_statics :: Ctxt [Bool],
34+ idris_classes :: Ctxt [Name],
3435 idris_log :: String,
3536 idris_options :: IOption,
3637 idris_name :: Int,
@@ -42,7 +43,7 @@ data IState = IState { tt_ctxt :: Context,
4243 errLine :: Maybe Int
4344 }
4445
45−idrisInit = IState emptyContext [] emptyContext emptyContext
46+idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext
4647 "" defaultOpts 6 [] [] [] [] [] Nothing
4748
4849-- 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
184185 | PClauses FC Name [PClause' t] -- pattern clause
185186 | PData SyntaxInfo FC (PData' t) -- data declaration
186187 | PParams FC [(Name, t)] [PDecl' t] -- params block
187− | PClass FC Name
188+ | PClass SyntaxInfo FC Name
188189 [(Name, t)] -- parameters
189190 [PDecl' t] -- declarations
190− | PInstance FC Name t [PDecl' t]
191+ | PInstance SyntaxInfo FC Name t [PDecl' t]
191192 | PSyntax FC Syntax
192193 deriving Functor
193194
@@ -831,8 +832,10 @@ dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (sh
831832dumpDecl (PData _ _ d) = showDImp True d
832833dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
833834dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
834−dumpDecl (PClass _ n ps ds) = "class " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
835−dumpDecl (PInstance _ n t ds) = "instance " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
835+dumpDecl (PClass _ _ n ps ds)
836+ = "class " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
837+dumpDecl (PInstance _ _ n t ds)
838+ = "instance " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
836839-- dumpDecl (PImport i) = "import " ++ i
837840
838841-- 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)
280280 PApp fc (PRef fc' wname) (map (pexp . (PRef fc')) ns ++ [pexp w])
281281 updateLHS n wname mvars ns tm w = fail $ "Not implemented " ++ show tm
282282
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+
283358pbinds (Bind n (PVar t) sc) = do attack; patbind n
284359 pbinds sc
285360pbinds tm = return ()
@@ -325,6 +400,12 @@ elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps
325400 newb = addAlist dsParams (inblock info) in
326401 info { params = newps,
327402 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+
328409-- elabDecl' info (PImport i) = loadModule i
329410
330411
src/Idris/Parser.hs+4−4
@@ -145,8 +145,8 @@ 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 n ps ds : ds') = PClass f n ps (collect ds) : collect ds'
149−collect (PInstance f n t ds : ds') = PInstance f n t (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 s n t ds : ds') = PInstance f s n t (collect ds) : collect ds'
150150collect (d : ds) = d : collect ds
151151collect [] = []
152152
@@ -292,7 +292,7 @@ pClass syn = do reserved "class"
292292 reserved "where"; lchar '{'
293293 ds <- many1 $ pFunDecl syn;
294294 lchar '}'
295− return [PClass fc n cs (concat ds)]
295+ return [PClass syn fc n cs (concat ds)]
296296 where
297297 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
298298 return (i, ty)
@@ -310,7 +310,7 @@ pInstance syn = do reserved "instance"
310310 reserved "where"; lchar '{'
311311 ds <- many1 $ pFunDecl syn;
312312 lchar '}'
313− return [PInstance fc cn t (concat ds)]
313+ return [PInstance syn fc cn t (concat ds)]
314314
315315--------- Expressions ---------
316316