diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 786c608..aa6a496 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -1268,6 +1268,13 @@ addOpenHint hintn_in hintn <- toResolvedNames hintn_in put Ctxt (record { openHints $= insert hintn () } defs) +export +dropOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core () +dropOpenHint hintn_in + = do defs <- get Ctxt + hintn <- toResolvedNames hintn_in + put Ctxt (record { openHints $= delete hintn } defs) + export setOpenHints : {auto c : Ref Ctxt Defs} -> NameMap () -> Core () setOpenHints hs diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 7306cba..b3ba739 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -37,22 +37,37 @@ bindConstraints fc p [] ty = ty bindConstraints fc p ((n, ty) :: rest) sc = IPi fc RigW p n ty (bindConstraints fc p rest sc) -addDefaults : FC -> List Name -> List (Name, List ImpClause) -> +addDefaults : FC -> Name -> List Name -> List (Name, List ImpClause) -> List ImpDecl -> (List ImpDecl, List Name) -- Updated body, list of missing methods -addDefaults fc ms defs body - = let missing = dropGot ms body in +addDefaults fc impName allms defs body + = let missing = dropGot allms body in extendBody [] missing body where + -- Given the list of missing names, if any are among the default definitions, + -- add them to the body extendBody : List Name -> List Name -> List ImpDecl -> (List ImpDecl, List Name) extendBody ms [] body = (body, ms) extendBody ms (n :: ns) body = case lookup n defs of Nothing => extendBody (n :: ms) ns body - Just cs => extendBody ms ns - (IDef fc n (map (substLocClause fc) cs) :: body) + Just cs => + -- If any method names appear in the clauses, they should + -- be applied to the constraint name __con because they + -- are going to be referring to the present implementation. + -- That is, default method implementations could depend on + -- other methods. + -- (See test idris2/interface014 for an example!) + let mupdates + = map (\n => (n, IImplicitApp fc (IVar fc n) + (Just (UN "__con")) + (IVar fc impName))) allms + cs' = map (substNamesClause [] mupdates) cs in + extendBody ms ns + (IDef fc n (map (substLocClause fc) cs') :: body) + -- Find which names are missing from the body dropGot : List Name -> List ImpDecl -> List Name dropGot ms [] = ms dropGot ms (IDef _ n _ :: ds) @@ -139,13 +154,12 @@ elabImplementation {vars} fc vis pass env nest cons iname ps impln mbody -- 1.5. Lookup default definitions and add them to to body let (body, missing) - = addDefaults fc (map (dropNS . fst) (methods cdata)) + = addDefaults fc impName (map (dropNS . fst) (methods cdata)) (defaults cdata) body_in log 5 $ "Added defaults: body is " ++ show body log 5 $ "Missing methods: " ++ show missing - -- 2. Elaborate top level function types for this interface defs <- get Ctxt fns <- topMethTypes [] impName methImps impsp (params cdata) diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index 69a34ad..a995e0c 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -111,6 +111,7 @@ mutual = IForce fc (substNames bound ps t) substNames bound ps tm = tm + export substNamesClause : List Name -> List (Name, RawImp) -> ImpClause -> ImpClause substNamesClause bound ps (PatClause fc lhs rhs) diff --git a/tests/Main.idr b/tests/Main.idr index 66e309f..06d059f 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -39,7 +39,7 @@ idrisTests "interface001", "interface002", "interface003", "interface004", "interface005", "interface006", "interface007", "interface008", "interface009", "interface010", "interface011", "interface012", - "interface013", + "interface013", "interface014", "lazy001", "linear001", "linear002", "linear003", "linear004", "linear005", "linear006", "linear007", diff --git a/tests/idris2/error004/expected b/tests/idris2/error004/expected index 208ccb2..5075e25 100644 --- a/tests/idris2/error004/expected +++ b/tests/idris2/error004/expected @@ -2,7 +2,7 @@ Error1.idr:8:9--9:1:While processing right hand side of Main.wrong at Error1.idr:8:1--9:1: Can't find an implementation for Show (Vect (S (S (S (S Z)))) Integer) 1/1: Building Error2 (Error2.idr) -Error2.idr:11:1--15:1:While processing right hand side of Main.showPrec at Error2.idr:11:1--15:1: +Error2.idr:13:38--15:1:While processing right hand side of Main.show at Error2.idr:13:3--15:1: Multiple solutions found in search. Possible correct results: Show implementation at Error2.idr:11:1--15:1 Show implementation at Error2.idr:7:1--11:1 diff --git a/tests/idris2/interface014/DepInt.idr b/tests/idris2/interface014/DepInt.idr new file mode 100644 index 0000000..8332fde --- /dev/null +++ b/tests/idris2/interface014/DepInt.idr @@ -0,0 +1,13 @@ +import Control.Monad.Identity + +public export +interface Foo (sA : Type) where + A : Type + Elem : A -> sA -> Type + Empty : sA -> Type + Empty as = (a : A) -> Not (Elem a as) + +public export +implementation Foo (Identity Bool) where + A = Bool + Elem x (Id y) = x = y diff --git a/tests/idris2/interface014/expected b/tests/idris2/interface014/expected new file mode 100644 index 0000000..5261ac6 --- /dev/null +++ b/tests/idris2/interface014/expected @@ -0,0 +1 @@ +1/1: Building DepInt (DepInt.idr) diff --git a/tests/idris2/interface014/run b/tests/idris2/interface014/run new file mode 100755 index 0000000..ae441de --- /dev/null +++ b/tests/idris2/interface014/run @@ -0,0 +1,3 @@ +$1 DepInt.idr --check + +rm -rf build