f49cd3b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Pass options on functions in typeclasses through to instances

f49cd3bEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -579,7 +579,7 @@ type PArg = PArg' PTerm

579-- Type class data

580

581data ClassInfo = CI { instanceName :: Name,

582− class_methods :: [(Name, PTerm)],

582+ class_methods :: [(Name, (FnOpts, PTerm))],

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

584 class_params :: [Name] }

585 deriving Show

src/Idris/Coverage.hs+8−2

@@ -225,13 +225,19 @@ calcTotality path fc n pats

225 (ns, rest) -> map (drop (length ns)) v

226

227 -- argument positions which are never LT are no use to us

228+ stripNoLT [] = [] -- no recursive calls

228− stripNoLT xs = transpose (filter (any (==LexLT)) (transpose xs))

229+ stripNoLT xs = case transpose (filter (any (==LexLT)) (transpose xs)) of

230+ [] -> [[]] -- recursive calls are all useless...

231+ xs -> xs

229

232

230 ctot (lhs, rhs)

233 ctot (lhs, rhs)

231 | (_, args) <- unApply lhs

234 | (_, args) <- unApply lhs

232 = do -- check lhs doesn't use any dodgy names

235 = do -- check lhs doesn't use any dodgy names

233 lhsOK <- mapM (chkOrd [] []) args

236 lhsOK <- mapM (chkOrd [] []) args

234− chkOrd (concat lhsOK) args rhs

237+ chkOrd (filter isLeft (concat lhsOK)) args rhs

238+

239+ isLeft (Left _) = True

240+ isLeft _ = False

235

241

236 chkOrd ords args (Bind n (Let t v) sc)

242 chkOrd ords args (Bind n (Let t v) sc)

237 = do ov <- chkOrd ords args v

243 = do ov <- chkOrd ords args v

src/Idris/ElabDecls.hs+16−15

@@ -555,21 +555,21 @@ elabClass info syn fc constraints tn ps ds

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

556 conbind [] x = x

557

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

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

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

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

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

561− (n, (syn, t) ) )

561+ (n, (syn, o, t) ) )

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

563

564 -- Create default definitions

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

566 case lookup n mtys of

567− Just (syn, ty) -> do let ty' = insertConstraint c ty

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

568− let ds = map (decorateid defaultdec)

568+ let ds = map (decorateid defaultdec)

569− [PTy syn fc [] n ty',

569+ [PTy syn fc [] n ty',

570− PClauses fc (TCGen:opts) n cs]

570+ PClauses fc (TCGen:o ++ opts) n cs]

571− iLOG (show ds)

571+ iLOG (show ds)

572− return (n, (defaultdec n, ds))

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

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

574 defdecl _ _ _ = fail "Can't happen (defdecl)"

575

@@ -593,7 +593,7 @@ elabClass info syn fc constraints tn ps ds

593 return [PTy syn fc [] cfn ty,

594 PClauses fc [Inlinable,TCGen] cfn [PClause cfn lhs [] rhs []]]

595

596− tfun cn c syn all (m, ty)

596+ tfun cn c syn all (m, (o, ty))

597 = do let ty' = insertConstraint c ty

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

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

@@ -604,7 +604,7 @@ elabClass info syn fc constraints tn ps ds

604 iLOG (showImp True ty)

605 iLOG (show (m, ty', capp, margs))

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

607− return [PTy syn fc [] m ty',

607+ return [PTy syn fc o m ty',

608 PClauses fc [Inlinable,TCGen] m [PClause m lhs [] rhs []]]

609

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

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

650 let ns = case n of

651 NS n ns' -> ns'

652 _ -> []

653+ let mtys = map (\ (n, (op, t)) ->

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

654+ let t' = substMatches ips t in

654− (decorate ns n, coninsert cs t', t'))

655+ (decorate ns n, op, coninsert cs t', t'))

655 (class_methods ci)

656 (class_methods ci)

656 logLvl 3 (show (mtys, ips))

657 logLvl 3 (show (mtys, ips))

657 let ds' = insertDefaults (class_defaults ci) ns ds

658 let ds' = insertDefaults (class_defaults ci) ns ds

@@ -675,7 +676,7 @@ elabInstance info syn fc cs n ps t ds

675 iLOG (show idecl)

676 iLOG (show idecl)

676 elabDecl info idecl

677 elabDecl info idecl

677 where

678 where

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

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

679 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

680 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

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

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

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

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

@@ -704,7 +705,7 @@ elabInstance info syn fc cs n ps t ds

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

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

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

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

706

707

707− mkTyDecl (n, t, _) = PTy syn fc [] n t

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

708

709

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

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

710 conbind [] x = x

711 conbind [] x = x