a76f8b3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

More sane scoping rules for where/type classes

Parameters in the type signature get propagated, indices do not. So you no longer need to pass parameters explicitly if you need them in a where clause, and you no longer need to give explicitly typed helpers in type class instances for types with indices.

commita76f8b39a5c37bb7fd18f24245420a18f0227eda authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 7 Feb 2013, 17:37 (14 years ago) parent75e7758

6 files changed+60−22

compare with master

unifiedsplit

lib/Control/Arrow.idr+5−4 lib/Prelude.idr+1−1 lib/Prelude/Fin.idr+3−5 src/Idris/ElabDecls.hs+46−3 test/test015/test015.idr+2−4 tutorial/examples/binary.idr+3−5

lib/Control/Arrow.idr+5−4

@@ -24,16 +24,17 @@ instance Arrow Homomorphism where

2424

2525instance Monad m => Arrow (Kleislimorphism m) where

2626 arrow f = Kleisli (return . f)

27− first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a

28− return (x, b)

27+ first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a

28+ return (x, b)

2929

3030 second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b

3131 return (a, x)

3232

33− (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a

33+ (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a

3434 y <- g b

3535 return (x, y)

3636

37− (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a

37+ (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a

3838 y <- g a

3939 return (x, y)

40+

lib/Prelude.idr+1−1

@@ -328,7 +328,7 @@ readFile fn = do h <- openFile fn Read

328328 c <- readFile' h ""

329329 closeFile h

330330 return c

331− where

331+ where

332332 partial

333333 readFile' : File -> String -> IO String

334334 readFile' h contents =

lib/Prelude/Fin.idr+3−5

@@ -8,11 +8,9 @@ data Fin : Nat -> Type where

88 fS : Fin k -> Fin (S k)

1010instance Eq (Fin n) where

11− (==) = eq where

12− eq : Fin m -> Fin m -> Bool

13− eq fO fO = True

14− eq (fS k) (fS k') = eq k k'

15− eq _ _ = False

11+ (==) fO fO = True

12+ (==) (fS k) (fS k') = k == k'

13+ (==) _ _ = False

1614

1715weaken : Fin n -> Fin (S n)

1816weaken 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)

538538 -- Build the LHS as an "Infer", and pull out its type and

539539 -- pattern bindings

540540 i <- get

541− let lhs = addImplPat i lhs_in

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

549+ let lhs = addImplPat i (propagateParams params lhs_in)

542550 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)

551+ logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

543552 ((lhs', dlhs, []), _) <-

544553 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

545554 (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)

631640 -- _ -> MN i (show n)) . l

632641 }

633642

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+

634677elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

635678 = do ctxt <- getContext

636679 -- 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

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

853896 let ds = map (decorateid defaultdec)

854897 [PTy "" syn fc [] n ty',

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

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

856899 iLOG (show ds)

857900 return (n, ((defaultdec n, ds!!1), ds))

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

@@ -981,7 +1024,7 @@ elabInstance info syn fc cs n ps t expn ds

9811024 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

9821025 show (concat (nub wparams))

9831026 let lhs = case concat (nub wparams) of

984− [] -> PRef fc iname

1027+ _ -> PRef fc iname

9851028 as -> PApp fc (PRef fc iname) as

9861029 let rhs = PApp fc (PRef fc (instanceName ci))

9871030 (map (pexp . mkMethApp) mtys)

test/test015/test015.idr+2−4

@@ -20,10 +20,8 @@ data Binary : (width : Nat) -> (value : Nat) -> Type where

2020 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

2121

2222instance Show (Binary w k) where

23− show = show' where

24− show' : Binary w' k' -> String

25− show' zero = ""

26− show' (bin # bit) = show bin ++ show bit

23+ show zero = ""

24+ show (bin # bit) = show bin ++ show bit

2725

2826pad : Binary w n -> Binary (S w) n

2927pad zero = zero # b0

tutorial/examples/binary.idr+3−5

@@ -6,11 +6,9 @@ data Binary : Nat -> Type where

66 bI : Binary n -> Binary (S (n + n))

88instance Show (Binary n) where

9− show = show' where

10− show' : Binary n' -> String

11− show' (bO x) = show x ++ "0"

12− show' (bI x) = show x ++ "1"

13− show' bEnd = ""

9+ show (bO x) = show x ++ "0"

10+ show (bI x) = show x ++ "1"

11+ show bEnd = ""

1412

1513data Parity : Nat -> Type where

1614 even : Parity (n + n)