f49cd3b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Pass options on functions in typeclasses through to instances

commitf49cd3bd8f76ef78eadcc4eb37baf12cf51e7275 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 1 Feb 2012, 19:38 (15 years ago) parent6b6dc72

3 files changed+25−18

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1−1 src/Idris/Coverage.hs+8−2 src/Idris/ElabDecls.hs+16−15

src/Idris/AbsSyntax.hs+1−1

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

579579-- Type class data

580580

581581data ClassInfo = CI { instanceName :: Name,

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

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

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

584584 class_params :: [Name] }

585585 deriving Show

src/Idris/Coverage.hs+8−2

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

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

226226

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

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

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

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

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

231+ xs -> xs

229232

230233 ctot (lhs, rhs)

231234 | (_, args) <- unApply lhs

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

233236 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

235241

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

237243 = do ov <- chkOrd ords args v

src/Idris/ElabDecls.hs+16−15

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

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

556556 conbind [] x = x

557557

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

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

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

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

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

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

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

563563

564564 -- Create default definitions

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

566566 case lookup n mtys of

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

568− let ds = map (decorateid defaultdec)

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

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

571− iLOG (show ds)

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

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

568+ let ds = map (decorateid defaultdec)

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

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

571+ iLOG (show ds)

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

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

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

575575

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

593593 return [PTy syn fc [] cfn ty,

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

595595

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

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

597597 = do let ty' = insertConstraint c ty

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

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

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

604604 iLOG (showImp True ty)

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

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

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

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

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

609609

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

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

650650 let ns = case n of

651651 NS n ns' -> ns'

652652 _ -> []

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

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

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

654+ let t' = substMatches ips t in

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

655656 (class_methods ci)

656657 logLvl 3 (show (mtys, ips))

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

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

675676 iLOG (show idecl)

676677 elabDecl info idecl

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

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

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

681682 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

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

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

706707

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

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

708709

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

710711 conbind [] x = x