git.iko.soy/Idris-dev
on master help sign in
Injectivity assumptions
53ffd07Edwin Brady
src/Idris/Elab/Clause.hs+5−2
compare with master
unifiedsplit
@@ -543,7 +543,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
543 let fn_is = case lookupCtxt fname (idris_implicits i) of
543 let fn_is = case lookupCtxt fname (idris_implicits i) of
544 [t] -> t
544 [t] -> t
545 _ -> []
545 _ -> []
546− let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)
546+ let norm_ty = normalise ctxt [] fn_ty
547+ let params = getParamsInType i [] fn_is norm_ty
548+ let tcparams = getTCParamsInType i [] fn_is norm_ty
549+
547 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
550 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
548 propagateParams i params fn_ty (addImplPat i lhs_in)
551 propagateParams i params fn_ty (addImplPat i lhs_in)
549-- let lhs = mkLHSapp $
552-- let lhs = mkLHSapp $
@@ -634,7 +637,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
634 (do pbinds ist lhs_tm
637 (do pbinds ist lhs_tm
635 -- proof search can use explicitly written names
638 -- proof search can use explicitly written names
636 mapM_ addPSname (allNamesIn lhs_in)
639 mapM_ addPSname (allNamesIn lhs_in)
637− mapM_ setinj (nub (params ++ inj))
640+ mapM_ setinj (nub (tcparams ++ inj))
638 setNextName
641 setNextName
639 (ElabResult _ _ is ctxt' newDecls highlights) <-
642 (ElabResult _ _ is ctxt' newDecls highlights) <-
640 errAt "right hand side of " fname
643 errAt "right hand side of " fname
src/Idris/Elab/Utils.hs+19
@@ -16,6 +16,7 @@ import Control.Applicative hiding (Const)
16import Control.Monad.State
16import Control.Monad.State
17import Control.Monad
17import Control.Monad
18import Data.List
18import Data.List
19+import Data.Maybe
19import qualified Data.Traversable as Traversable
20import qualified Data.Traversable as Traversable
20
21
21import Debug.Trace
22import Debug.Trace
@@ -211,6 +212,24 @@ getParamsInType i env ps t = let fix = getFixedInType i env ps t
211 flex = getFlexInType i env fix t in
212 flex = getFlexInType i env fix t in
212 [x | x <- fix, not (x `elem` flex)]
213 [x | x <- fix, not (x `elem` flex)]
213
214
215+getTCinj i (Bind n (Pi _ t _) sc)
216+ = getTCinj i t ++ getTCinj i (instantiate (P Bound n t) sc)
217+getTCinj i ap@(App _ f a)
218+ | (P _ n _, args) <- unApply ap,
219+ isTCName n = mapMaybe getInjName args
220+ | otherwise = []
221+ where
222+ isTCName n = case lookupCtxtExact n (idris_classes i) of
223+ Just _ -> True
224+ _ -> False
225+ getInjName t | (P _ x _, _) <- unApply t = Just x
226+ | otherwise = Nothing
227+getTCinj _ _ = []
228+
229+getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
230+getTCParamsInType i env ps t = let params = getParamsInType i env ps t
231+ tcs = nub $ getTCinj i t in
232+ filter (flip elem tcs) params
214paramNames args env [] = []
233paramNames args env [] = []
215paramNames args env (p : ps)
234paramNames args env (p : ps)
216 | length args > p = case args!!p of
235 | length args > p = case args!!p of