f2e3a76 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Default definitions in classes, plus some bug fixing

f2e3a76Edwin Brady15 years ago

lib/builtins.idr+25−26

compare with master

unifiedsplit

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

84class Eq a where {

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

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

87+

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

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

87}

90}

89instance Eq Int where {

92instance Eq Int where {

90 (==) = boolOp prim__eqInt;

93 (==) = boolOp prim__eqInt;

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

92}

94}

94instance Eq Integer where {

96instance Eq Integer where {

95 (==) = boolOp prim__eqBigInt;

97 (==) = boolOp prim__eqBigInt;

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

97}

98}

99instance Eq Float where {

100instance Eq Float where {

100 (==) = boolOp prim__eqFloat;

101 (==) = boolOp prim__eqFloat;

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

102}

103

104data Ordering = LT | EQ | GT;

105

106class Eq a => Ord a where {

107 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;

108}

129}

109

130

131+

110instance Ord Int where {

132instance Ord Int where {

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

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

112 if (boolOp prim__ltInt x y) then LT else

134 if (boolOp prim__ltInt x y) then LT else

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

154div : Int -> Int -> Int;

176div : Int -> Int -> Int;

155div = prim__divInt;

177div = prim__divInt;

156

178

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;

168

179

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

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

170(/) = prim__divFloat;

181(/) = prim__divFloat;

171

182

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−

184--- string operators

183--- string operators

185

184

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

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

lib/prelude/nat.idr−2

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

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

29 O == (S y) = False;

30 (S x) == O = False;

31−

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

33}

31}

35instance Num Nat where {

33instance Num Nat where {

src/Core/Elaborate.hs+1

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

315

316 mkMN n@(MN _ _) = n

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

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

318

319

319simple_app :: Elab () -> Elab () -> Elab ()

320simple_app :: Elab () -> Elab () -> Elab ()

320simple_app fun arg =

321simple_app fun arg =

src/Idris/AbsSyntax.hs+4

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

141iputStrLn :: String -> Idris ()

142iputStrLn = lift.putStrLn

143

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

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

146+

144setLogLevel :: Int -> Idris ()

147setLogLevel :: Int -> Idris ()

145setLogLevel l = do i <- get

148setLogLevel l = do i <- get

146 let opts = idris_options i

149 let opts = idris_options i

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

390

393

391data ClassInfo = CI { instanceName :: Name,

394data ClassInfo = CI { instanceName :: Name,

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

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

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

393 class_params :: [Name] }

397 class_params :: [Name] }

394 deriving Show

398 deriving Show

395

399

src/Idris/ElabDecls.hs+81−25

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

284+

283elabClass :: ElabInfo -> SyntaxInfo ->

285elabClass :: ElabInfo -> SyntaxInfo ->

284 FC -> [PTerm] ->

286 FC -> [PTerm] ->

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

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

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

289 let constraint = PApp fc (PRef fc tn)

291 let constraint = PApp fc (PRef fc tn)

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

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

291 -- build data declaration

293 -- build data declaration

292− ims <- mapM tdecl ds

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

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

296+ (filter clause ds)

293− let (methods, imethods) = unzip ims

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

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

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

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

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

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

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

297 elabDecl info ddecl

301 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

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

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

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

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

301 mapM_ (elabDecl info) (concat fns)

305 mapM_ (elabDecl info) (concat fns)

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

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

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

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

304 mapM_ (elabDecl info) (concat fns)

308 mapM_ (elabDecl info) (concat fns)

309+ -- add the default definitions

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

305 i <- get

311 i <- get

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

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

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

307 (idris_classes i) })

314 (idris_classes i) })

308 where

315 where

309 pibind [] x = x

316 pibind [] x = x

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

315

322

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

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

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

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

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

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

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

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

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

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

321

328

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+

322 cfun cn c syn all con

348 cfun cn c syn all con

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

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

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

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

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

345 return [PTy syn fc m ty',

371 return [PTy syn fc m ty',

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

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

347

373

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

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

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

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

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

350 getMArgs _ = []

377 getMArgs _ = []

351

378

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

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

353 | otherwise = getMeth ms as x

380 | otherwise = getMeth ms as x

354

381

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

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

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

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

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

357 lhsArgs [] _ = []

385 lhsArgs [] _ = []

358

386

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

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

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

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

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

361 rhsArgs [] _ = []

390 rhsArgs [] _ = []

362

391

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

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

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

385 let ns = case n of

414 let ns = case n of

386 NS n ns' -> ns'

415 NS n ns' -> ns'

387 _ -> []

416 _ -> []

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

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

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

389 (class_methods ci)

419 (class_methods ci)

390 logLvl 3 (show (mtys, ips))

420 logLvl 3 (show (mtys, ips))

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

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

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

392 let lhs = PRef fc iname

425 let lhs = PRef fc iname

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

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

394 (map (pexp . mkMethApp) mtys)

427 (map (pexp . mkMethApp) mtys)

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

396 iLOG (show idecl)

429 iLOG (show idecl)

397 elabDecl info idecl

430 elabDecl info idecl

398 where

431 where

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

432+ 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'

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

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

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

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

402 lamBind i _ sc = sc

436 lamBind i _ sc = sc

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

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

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

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

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

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

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

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

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

408− = methArgs i sc

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

409 methArgs i _ = []

443 methArgs i _ = []

410

444

411 papp fc f [] = f

445 papp fc f [] = f

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

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

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

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

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

416

450

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

425

452

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

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

427 conbind [] x = x

454 conbind [] x = x

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

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

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

430 coninsert cs sc = conbind cs sc

457 coninsert cs sc = conbind cs sc

431

458

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+

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

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

433 pbinds sc

489 pbinds sc

434pbinds tm = return ()

490pbinds tm = return ()

src/Idris/ElabTerm.hs+2−2

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

242 = do focus a

243 fill (RConstant IType) -- default Int

244 solve

245− needsDefault t f as

245+-- needsDefault t f as

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

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

247 needsDefault t f a = return ()

248

249 boundVar (P Bound _ _) = True