git.iko.soy/Idris-dev
on master help sign in
More sane scoping rules for where/type classes
a76f8b3Edwin Brady
lib/Control/Arrow.idr+5−4
compare with master
unifiedsplit
@@ -24,16 +24,17 @@ instance Arrow Homomorphism where
24
24
25instance Monad m => Arrow (Kleislimorphism m) where
25instance Monad m => Arrow (Kleislimorphism m) where
26 arrow f = Kleisli (return . f)
26 arrow f = Kleisli (return . f)
27− first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a
27+ first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a
28− return (x, b)
28+ return (x, b)
29
29
30 second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
30 second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
31 return (a, x)
31 return (a, x)
32
32
33− (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
33+ (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
34 y <- g b
34 y <- g b
35 return (x, y)
35 return (x, y)
36
36
37− (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
37+ (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
38 y <- g a
38 y <- g a
39 return (x, y)
39 return (x, y)
40+
lib/Prelude.idr+1−1
@@ -328,7 +328,7 @@ readFile fn = do h <- openFile fn Read
328 c <- readFile' h ""
328 c <- readFile' h ""
329 closeFile h
329 closeFile h
330 return c
330 return c
331− where
331+ where
332 partial
332 partial
333 readFile' : File -> String -> IO String
333 readFile' : File -> String -> IO String
334 readFile' h contents =
334 readFile' h contents =
lib/Prelude/Fin.idr+3−5
@@ -8,11 +8,9 @@ data Fin : Nat -> Type where
8 fS : Fin k -> Fin (S k)
8 fS : Fin k -> Fin (S k)
9
9
10instance Eq (Fin n) where
10instance Eq (Fin n) where
11− (==) = eq where
12− eq : Fin m -> Fin m -> Bool
13− eq fO fO = True
11+ (==) fO fO = True
14− eq (fS k) (fS k') = eq k k'
12+ (==) (fS k) (fS k') = k == k'
15− eq _ _ = False
13+ (==) _ _ = False
16
14
17weaken : Fin n -> Fin (S n)
15weaken : Fin n -> Fin (S n)
18weaken fO = fO
16weaken fO = fO
src/Idris/ElabDecls.hs+46−3
@@ -538,8 +538,17 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
538 -- Build the LHS as an "Infer", and pull out its type and
538 -- Build the LHS as an "Infer", and pull out its type and
539 -- pattern bindings
539 -- pattern bindings
540 i <- get
540 i <- get
541+ -- get the parameters first, to pass through to any where block
542+ let fn_ty = case lookupTy Nothing fname (tt_ctxt i) of
543+ [t] -> t
544+ _ -> error "Can't happen (elabClause function type)"
545+ let fn_is = case lookupCtxt Nothing fname (idris_implicits i) of
546+ [t] -> t
547+ _ -> []
548+ let params = getParamsInType i [] fn_is fn_ty
541− let lhs = addImplPat i lhs_in
549+ let lhs = addImplPat i (propagateParams params lhs_in)
542 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)
550 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)
551+ logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
543 ((lhs', dlhs, []), _) <-
552 ((lhs', dlhs, []), _) <-
544 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
553 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
545 (erun fc (buildTC i info True tcgen fname (infTerm lhs)))
554 (erun fc (buildTC i info True tcgen fname (infTerm lhs)))
@@ -631,6 +640,40 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
631 -- _ -> MN i (show n)) . l
640 -- _ -> MN i (show n)) . l
632 }
641 }
633
642
643+ getParamsInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
644+ = getParamsInType i env is (instantiate (P Bound n t) sc)
645+ getParamsInType i env (_ : is) (Bind n (Pi t) sc)
646+ = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)
647+ getParamsInType i env is tm@(App f a)
648+ | (P _ tn _, args) <- unApply tm
649+ = case lookupCtxt Nothing tn (idris_datatypes i) of
650+ [t] -> nub $ paramNames args env (param_pos t) ++
651+ getParamsInType i env is f ++
652+ getParamsInType i env is a
653+ [] -> nub $ getParamsInType i env is f ++
654+ getParamsInType i env is a
655+ | otherwise = nub $ getParamsInType i env is f ++
656+ getParamsInType i env is a
657+ getParamsInType i _ _ _ = []
658+
659+ paramNames args env [] = []
660+ paramNames args env (p : ps)
661+ | length args > p = case args!!p of
662+ P _ n _ -> if n `elem` env
663+ then n : paramNames args env ps
664+ else paramNames args env ps
665+ _ -> paramNames args env ps
666+ | otherwise = paramNames args env ps
667+
668+ propagateParams :: [Name] -> PTerm -> PTerm
669+ propagateParams ps (PApp _ (PRef fc n) args)
670+ = PApp fc (PRef fc n) (map addP args)
671+ where addP imp@(PImp _ _ _ Placeholder _)
672+ | pname imp `elem` ps = imp { getTm = PRef fc (pname imp) }
673+ addP t = t
674+ propagateParams ps (PRef fc n)
675+ = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps)
676+
634elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
677elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
635 = do ctxt <- getContext
678 = do ctxt <- getContext
636 -- Build the LHS as an "Infer", and pull out its type and
679 -- Build the LHS as an "Infer", and pull out its type and
@@ -852,7 +895,7 @@ elabClass info syn doc fc constraints tn ps ds
852 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
895 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
853 let ds = map (decorateid defaultdec)
896 let ds = map (decorateid defaultdec)
854 [PTy "" syn fc [] n ty',
897 [PTy "" syn fc [] n ty',
855− PClauses fc (TCGen:o ++ opts) n cs]
898+ PClauses fc (Inlinable:TCGen:o ++ opts) n cs]
856 iLOG (show ds)
899 iLOG (show ds)
857 return (n, ((defaultdec n, ds!!1), ds))
900 return (n, ((defaultdec n, ds!!1), ds))
858 _ -> fail $ show n ++ " is not a method"
901 _ -> fail $ show n ++ " is not a method"
@@ -981,7 +1024,7 @@ elabInstance info syn fc cs n ps t expn ds
981 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
1024 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
982 show (concat (nub wparams))
1025 show (concat (nub wparams))
983 let lhs = case concat (nub wparams) of
1026 let lhs = case concat (nub wparams) of
984− [] -> PRef fc iname
1027+ _ -> PRef fc iname
985 as -> PApp fc (PRef fc iname) as
1028 as -> PApp fc (PRef fc iname) as
986 let rhs = PApp fc (PRef fc (instanceName ci))
1029 let rhs = PApp fc (PRef fc (instanceName ci))
987 (map (pexp . mkMethApp) mtys)
1030 (map (pexp . mkMethApp) mtys)
test/test015/test015.idr+2−4
@@ -20,10 +20,8 @@ data Binary : (width : Nat) -> (value : Nat) -> Type where
20 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
20 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
21
21
22instance Show (Binary w k) where
22instance Show (Binary w k) where
23− show = show' where
24− show' : Binary w' k' -> String
25− show' zero = ""
23+ show zero = ""
26− show' (bin # bit) = show bin ++ show bit
24+ show (bin # bit) = show bin ++ show bit
27
25
28pad : Binary w n -> Binary (S w) n
26pad : Binary w n -> Binary (S w) n
29pad zero = zero # b0
27pad zero = zero # b0
tutorial/examples/binary.idr+3−5
@@ -6,11 +6,9 @@ data Binary : Nat -> Type where
6 bI : Binary n -> Binary (S (n + n))
6 bI : Binary n -> Binary (S (n + n))
7
7
8instance Show (Binary n) where
8instance Show (Binary n) where
9− show = show' where
10− show' : Binary n' -> String
11− show' (bO x) = show x ++ "0"
9+ show (bO x) = show x ++ "0"
12− show' (bI x) = show x ++ "1"
10+ show (bI x) = show x ++ "1"
13− show' bEnd = ""
11+ show bEnd = ""
14
12
15data Parity : Nat -> Type where
13data Parity : Nat -> Type where
16 even : Parity (n + n)
14 even : Parity (n + n)