f2e3a76 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Default definitions in classes, plus some bug fixing

commitf2e3a76491b4853f9fb56725b132e0f845f64261 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 30 Nov 2011, 21:39 (15 years ago) parentbe33671

6 files changed+113−55

compare with master

unifiedsplit

lib/builtins.idr+25−26 lib/prelude/nat.idr−2 src/Core/Elaborate.hs+1 src/Idris/AbsSyntax.hs+4 src/Idris/ElabDecls.hs+81−25 src/Idris/ElabTerm.hs+2−2

lib/builtins.idr+25−26

@@ -84,29 +84,51 @@ boolOp op x y = intToBool (op x y);

8484class Eq a where {

8585 (==) : a -> a -> Bool;

8686 (/=) : a -> a -> Bool;

87+

88+ (/=) x y = not (x == y);

89+ (==) x y = not (x /= y);

8790}

8891

8992instance Eq Int where {

9093 (==) = boolOp prim__eqInt;

91− (/=) x y = not (x == y);

9294}

9395

9496instance Eq Integer where {

9597 (==) = boolOp prim__eqBigInt;

96− (/=) x y = not (x == y);

9798}

9899

99100instance Eq Float where {

100101 (==) = boolOp prim__eqFloat;

101− (/=) x y = not (x == y);

102102}

103103

104104data Ordering = LT | EQ | GT;

105105

106106class Eq a => Ord a where {

107107 compare : a -> a -> Ordering;

108+

109+ (<) : a -> a -> Bool;

110+ (<) x y with compare x y {

111+ (<) x y | LT = True;

112+ (<) x y | _ = False;

113+ }

114+

115+ (>) : a -> a -> Bool;

116+ (>) x y with compare x y {

117+ (>) x y | GT = True;

118+ (>) x y | _ = False;

119+ }

120+

121+ (<=) : a -> a -> Bool;

122+ (<=) x y = x < y || x == y;

123+

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

125+ (>=) x y = x > y || x == y;

126+

127+ max : a -> a -> a;

128+ max x y = if (x > y) then x else y;

108129}

109130

131+

110132instance Ord Int where {

111133 compare x y = if (x == y) then EQ else

112134 if (boolOp prim__ltInt x y) then LT else

@@ -154,33 +176,10 @@ instance Num Float where {

154176div : Int -> Int -> Int;

155177div = prim__divInt;

156178

157−(<) : Int -> Int -> Bool;

158−(<) = boolOp prim__ltInt;

159−

160−(<=) : Int -> Int -> Bool;

161−(<=) = boolOp prim__lteInt;

162−

163−(>) : Int -> Int -> Bool;

164−(>) = boolOp prim__gtInt;

165−

166−(>=) : Int -> Int -> Bool;

167−(>=) = boolOp prim__gteInt;

168179

169180(/) : Float -> Float -> Float;

170181(/) = prim__divFloat;

171182

172−(<.) : Float -> Float -> Bool;

173−(<.) = boolOp prim__ltFloat;

174−

175−(<=.) : Float -> Float -> Bool;

176−(<=.) = boolOp prim__lteFloat;

177−

178−(>.) : Float -> Float -> Bool;

179−(>.) = boolOp prim__gtFloat;

180−

181−(>=.) : Float -> Float -> Bool;

182−(>=.) = boolOp prim__gteFloat;

183−

184183--- string operators

185184

186185(++) : String -> String -> String;

lib/prelude/nat.idr−2

@@ -28,8 +28,6 @@ instance Eq Nat where {

2828 (S x) == (S y) = x == y;

2929 O == (S y) = False;

3030 (S x) == O = False;

31−

32− x /= y = not (x == y);

3331}

3432

3533instance Num Nat where {

src/Core/Elaborate.hs+1

@@ -315,6 +315,7 @@ apply_elab n args =

315315

316316 mkMN n@(MN _ _) = n

317317 mkMN n@(UN x) = MN 0 x

318+ mkMN (NS n ns) = NS (mkMN n) ns

318319

319320simple_app :: Elab () -> Elab () -> Elab ()

320321simple_app fun arg =

src/Idris/AbsSyntax.hs+4

@@ -141,6 +141,9 @@ solveDeferred n = do i <- get

141141iputStrLn :: String -> Idris ()

142142iputStrLn = lift.putStrLn

143143

144+iWarn :: FC -> String -> Idris ()

145+iWarn fc err = do lift $ putStrLn (show fc ++ ":" ++ err)

146+

144147setLogLevel :: Int -> Idris ()

145148setLogLevel l = do i <- get

146149 let opts = idris_options i

@@ -390,6 +393,7 @@ type PArg = PArg' PTerm

390393

391394data ClassInfo = CI { instanceName :: Name,

392395 class_methods :: [(Name, PTerm)],

396+ class_defaults :: [(Name, Name)], -- method name -> default impl

393397 class_params :: [Name] }

394398 deriving Show

395399

src/Idris/ElabDecls.hs+81−25

@@ -280,6 +280,8 @@ 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+data MArgTy = IA | EA | CA deriving Show

284+

283285elabClass :: ElabInfo -> SyntaxInfo ->

284286 FC -> [PTerm] ->

285287 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

@@ -289,21 +291,26 @@ elabClass info syn fc constraints tn ps ds

289291 let constraint = PApp fc (PRef fc tn)

290292 (map (pexp . PRef fc) (map fst ps))

291293 -- build data declaration

292− ims <- mapM tdecl ds

293− let (methods, imethods) = unzip ims

294+ ims <- mapM tdecl (filter tydecl ds)

295+ defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

296+ (filter clause ds)

297+ let (methods, imethods) = unzip (map (\ (x,y,z) -> (x, y)) ims)

294298 let cty = impbind ps $ conbind constraints $ pibind methods constraint

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

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

297301 elabDecl info ddecl

298− -- for each constraint, bui;d a top level function to chase it

302+ -- for each constraint, build a top level function to chase it

299303 let usyn = syn { using = ps ++ using syn }

300304 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

301305 mapM_ (elabDecl info) (concat fns)

302306 -- for each method, build a top level function

303307 fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods

304308 mapM_ (elabDecl info) (concat fns)

309+ -- add the default definitions

310+ mapM_ (elabDecl info) (concat (map (snd.snd) defs))

305311 i <- get

306− put (i { idris_classes = addDef tn (CI cn imethods (map fst ps))

312+ let defaults = map (\ (x, (y, z)) -> (x,y)) defs

313+ put (i { idris_classes = addDef tn (CI cn imethods defaults (map fst ps))

307314 (idris_classes i) })

308315 where

309316 pibind [] x = x

@@ -315,10 +322,29 @@ elabClass info syn fc constraints tn ps ds

315322

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

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

318− (n, (toExp (map fst ps) Imp t')) )

319− tdecl (PClauses _ _ _ _) = fail "No default definitions allowed yet"

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

326+ (n, (syn, t) ) )

320327 tdecl _ = fail "Not allowed in a class declaration"

321328

329+ -- Create default definitions

330+ defdecl mtys c d@(PClauses fc opts n cs) =

331+ case lookup n mtys of

332+ Just (syn, ty) -> do let ty' = insertConstraint c ty

333+ let ds = map (decorateid defaultdec)

334+ [PTy syn fc n ty', d]

335+ iLOG (show ds)

336+ return (n, (defaultdec n, ds))

337+ _ -> fail $ show n ++ " is not a method"

338+ defdecl _ _ _ = fail "Can't happen (defdecl)"

339+

340+ defaultdec (UN n) = UN ("default#" ++ n)

341+ defaultdec (NS n ns) = NS (defaultdec n) ns

342+

343+ tydecl (PTy _ _ _ _) = True

344+ tydecl _ = False

345+ clause (PClauses _ _ _ _) = True

346+ clause _ = False

347+

322348 cfun cn c syn all con

323349 = do let cfn = UN ('@':show cn ++ "#" ++ show con)

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

@@ -345,19 +371,22 @@ elabClass info syn fc constraints tn ps ds

345371 return [PTy syn fc m ty',

346372 PClauses fc True m [PClause m lhs [] rhs []]]

347373

348− getMArgs (PPi (Imp _ _) n ty sc) = False : getMArgs sc

349− getMArgs (PPi (Exp _ _) n ty sc) = True : getMArgs sc

374+ getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc

375+ getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc

376+ getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

350377 getMArgs _ = []

351378

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

353380 | otherwise = getMeth ms as x

354381

355− lhsArgs (True : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns

356− lhsArgs (False : xs) ns = lhsArgs xs ns

382+ lhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns

383+ lhsArgs (IA : xs) ns = lhsArgs xs ns

384+ lhsArgs (CA : xs) ns = lhsArgs xs ns

357385 lhsArgs [] _ = []

358386

359− rhsArgs (True : xs) (n : ns) = pexp (PRef fc n) : rhsArgs xs ns

360− rhsArgs (False : xs) ns = pexp Placeholder : rhsArgs xs ns

387+ rhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : rhsArgs xs ns

388+ rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns

389+ rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

361390 rhsArgs [] _ = []

362391

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

@@ -385,10 +414,14 @@ elabInstance info syn fc cs n ps t ds

385414 let ns = case n of

386415 NS n ns' -> ns'

387416 _ -> []

388− let mtys = map (\ (n, t) -> (decorate ns n, coninsert cs $ substMatches ips t))

417+ let mtys = map (\ (n, t) -> let t' = substMatches ips t in

418+ (decorate ns n, coninsert cs t', t'))

389419 (class_methods ci)

390420 logLvl 3 (show (mtys, ips))

391− let wb = map mkTyDecl mtys ++ map (decorateid ns) ds

421+ let ds' = insertDefaults (class_defaults ci) ns ds

422+ iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)

423+ mapM_ (warnMissing ds' ns) (map fst (class_methods ci))

424+ let wb = map mkTyDecl mtys ++ map (decorateid (decorate ns)) ds'

392425 let lhs = PRef fc iname

393426 let rhs = PApp fc (PRef fc (instanceName ci))

394427 (map (pexp . mkMethApp) mtys)

@@ -396,8 +429,9 @@ elabInstance info syn fc cs n ps t ds

396429 iLOG (show idecl)

397430 elabDecl info idecl

398431 where

399− mkMethApp (n, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

400− lamBind i (PPi (Constraint _ _) _ _ sc) sc' = lamBind i sc sc'

432+ mkMethApp (n, _, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

433+ lamBind i (PPi (Constraint _ _) _ _ sc) sc'

434+ = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

401435 lamBind i (PPi _ n ty sc) sc' = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

402436 lamBind i _ sc = sc

403437 methArgs i (PPi (Imp _ _) n ty sc)

@@ -405,7 +439,7 @@ elabInstance info syn fc cs n ps t ds

405439 methArgs i (PPi (Exp _ _) n ty sc)

406440 = PExp 0 False (PRef fc (MN i "meth")) : methArgs (i+1) sc

407441 methArgs i (PPi (Constraint _ _) n ty sc)

408− = methArgs i sc

442+ = PConstraint 0 False (PResolveTC fc) : methArgs (i+1) sc

409443 methArgs i _ = []

410444

411445 papp fc f [] = f

@@ -414,14 +448,7 @@ elabInstance info syn fc cs n ps t ds

414448 decorate ns (UN n) = NS (UN ('!':n)) ns

415449 decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns

416450

417− decorateid ns (PTy s f n t) = PTy s f (decorate ns n) t

418− decorateid ns (PClauses f o n cs) = PClauses f o (decorate ns n) (map dc cs)

419− where dc (PClause n t as w ds) = PClause (decorate ns n) (dappname t) as w ds

420− dc (PWith n t as w ds) = PWith (decorate ns n) (dappname t) as w

421− (map (decorateid ns) ds)

422− dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate ns n)) as

423− dappname t = t

424− mkTyDecl (n, t) = PTy syn fc n t

451+ mkTyDecl (n, t, _) = PTy syn fc n t

425452

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

427454 conbind [] x = x

@@ -429,6 +456,35 @@ elabInstance info syn fc cs n ps t ds

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

430457 coninsert cs sc = conbind cs sc

431458

459+ insertDefaults :: [(Name, Name)] -> [String] -> [PDecl] -> [PDecl]

460+ insertDefaults [] ns ds = ds

461+ insertDefaults ((n,dn) : defs) ns ds

462+ = insertDefaults defs ns (insertDef n dn ns ds)

463+

464+ insertDef meth def ns decls

465+ | null $ filter (clauseFor meth ns) decls

466+ = decls ++ [PClauses fc True meth

467+ [PClause meth (PApp fc (PRef fc meth) []) []

468+ (PApp fc (PRef fc def) []) []]]

469+ | otherwise = decls

470+

471+ warnMissing decls ns meth

472+ | null $ filter (clauseFor meth ns) decls

473+ = iWarn fc $ "method " ++ show meth ++ " not defined"

474+ | otherwise = return ()

475+

476+ clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m'

477+ clauseFor m ns _ = False

478+

479+decorateid decorate (PTy s f n t) = PTy s f (decorate n) t

480+decorateid decorate (PClauses f o n cs)

481+ = PClauses f o (decorate n) (map dc cs)

482+ where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds

483+ dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w

484+ (map (decorateid decorate) ds)

485+ dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

486+ dappname t = t

487+

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

433489 pbinds sc

434490pbinds tm = return ()

src/Idris/ElabTerm.hs+2−2

@@ -242,8 +242,8 @@ resolveTC depth ist

242242 = do focus a

243243 fill (RConstant IType) -- default Int

244244 solve

245− needsDefault t f as

246− | all boundVar as = fail $ "Can't resolve " ++ show t

245+-- needsDefault t f as

246+-- | all boundVar as = fail $ "Can't resolve " ++ show t

247247 needsDefault t f a = return ()

248248

249249 boundVar (P Bound _ _) = True