git.iko.soy/Idris-dev
on master help sign in
Move normalisation of deferred types

No need to do this when collecting deferred names, just do it for display purposes. It's safer anyway, due to potential name clashes in the normalisation. Fixes #2806

commit140d06ab0a2ca4c0b5369e476002753930df31d0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 15 Nov 2015, 13:21 (11 years ago) parent6592938
9 files changed+107−33
compare with master
unifiedsplit
idris.cabal+4 src/Idris/Elab/Term.hs+18−31 src/Idris/REPL.hs+2−1 test/basic002/test006.idr+1−1 test/interactive012/expected+33 test/interactive012/input+9 test/interactive012/interactive012.idr+26 test/interactive012/run+3 test/reg001/reg001.idr+11
idris.cabal+4
@@ -545,6 +545,10 @@ Extra-source-files:
545545 test/interactive011/input
546546 test/interactive011/run
547547 test/interactive011/*.idr
548+ test/interactive012/expected
549+ test/interactive012/input
550+ test/interactive012/run
551+ test/interactive012/*.idr
548552
549553 test/io001/run
550554 test/io001/*.idr
src/Idris/Elab/Term.hs+18−31
@@ -1721,38 +1721,25 @@ resolveTC' di mv depth tm n ist
17211721
17221722collectDeferred :: Maybe Name -> [Name] -> Context ->
17231723 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
1724−collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =
1725− do ds <- get
1726− t' <- collectDeferred top casenames ctxt t
1727− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])
1728− collectDeferred top casenames ctxt app
1724+collectDeferred top casenames ctxt tm = cd [] tm
17291725 where
1730− -- Evaluate the top level functions in arguments, if possible, and if it's
1731− -- not a name we're immediately going to define in a case block, so that
1732− -- any immediate specialisation of the function applied to constructors
1733− -- can be done
1734− tidyArg env (Bind n b@(Pi im t k) sc)
1735− = Bind n (Pi im (tidy ctxt env t) k)
1736− (tidyArg ((n, b) : env) sc)
1737− tidyArg env t = tidy ctxt env t
1738−
1739− tidy ctxt env t = normalise ctxt env t
1740−
1741− getFn (Bind n (Lam _) t) = getFn t
1742− getFn t | (f, a) <- unApply t = f
1743−
1744−collectDeferred top ns ctxt (Bind n b t)
1745− = do b' <- cdb b
1746− t' <- collectDeferred top ns ctxt t
1747− return (Bind n b' t')
1748− where
1749− cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1750− cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1751− cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)
1752− return (b { binderTy = ty' })
1753−collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f)
1754− (collectDeferred top ns ctxt a)
1755−collectDeferred top ns ctxt t = return t
1726+ cd env (Bind n (GHole i psns t) app) =
1727+ do ds <- get
1728+ t' <- collectDeferred top casenames ctxt t
1729+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])
1730+ cd env app
1731+ cd env (Bind n b t)
1732+ = do b' <- cdb b
1733+ t' <- cd ((n, b) : env) t
1734+ return (Bind n b' t')
1735+ where
1736+ cdb (Let t v) = liftM2 Let (cd env t) (cd env v)
1737+ cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)
1738+ cdb b = do ty' <- cd env (binderTy b)
1739+ return (b { binderTy = ty' })
1740+ cd env (App s f a) = liftM2 (App s) (cd env f)
1741+ (cd env a)
1742+ cd env t = return t
17561743
17571744case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
17581745case_ ind autoSolve ist fn tm = do
src/Idris/REPL.hs+2−1
@@ -943,7 +943,8 @@ process fn (Check (PRef _ _ n))
943943 where
944944 showMetavarInfo ppo ist n i
945945 = case lookupTy n (tt_ctxt ist) of
946− (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
946+ (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in
947+ putTy ppo ist i [] (delab ist (errReverse ist ty'))
947948 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
948949 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
949950 putTy ppo ist i bnd (PPi _ n _ t sc)
test/basic002/test006.idr+1−1
@@ -23,7 +23,7 @@ main = do printLn (natToBin 42)
2323---------- Proofs ----------
2424
2525Main.parity_lemma_2 = proof {
26− intro;
26+ intro j;
2727 intro;
2828 rewrite sym (plusSuccRightSucc j j);
2929 trivial;
test/interactive012/expectednew file+33
@@ -0,0 +1,33 @@
1+ x : Int
2+--------------------------------------
3+mkString_rhs_1 : String
4+ x : String
5+--------------------------------------
6+mkString_rhs_2 : String
7+--------------------------------------
8+mkThing_rhs_1 : Int
9+--------------------------------------
10+mkThing_rhs_2 : String
11+ str : Bool
12+ x : IntString str
13+--------------------------------------
14+mkString2_rhs : String
15+ x : ?what
16+--------------------------------------
17+mkString3_rhs_1 : String
18+ x : ?what
19+--------------------------------------
20+mkString3_rhs_2 : String
21+ a : Type
22+ m : Nat
23+ ys : Vect m a
24+--------------------------------------
25+append_rhs_1 : Vect m a
26+ a : Type
27+ x : a
28+ k : Nat
29+ xs : Vect k a
30+ m : Nat
31+ ys : Vect m a
32+--------------------------------------
33+append_rhs_2 : Vect (S (plus k m)) a
test/interactive012/inputnew file+9
@@ -0,0 +1,9 @@
1+:t mkString_rhs_1
2+:t mkString_rhs_2
3+:t mkThing_rhs_1
4+:t mkThing_rhs_2
5+:t mkString2_rhs
6+:t mkString3_rhs_1
7+:t mkString3_rhs_2
8+:t append_rhs_1
9+:t append_rhs_2
test/interactive012/interactive012.idrnew file+26
@@ -0,0 +1,26 @@
1+IntString : Bool -> Type
2+IntString False = Int
3+IntString True = String
4+
5+mkString : (str : Bool) -> IntString str -> String
6+mkString False x = ?mkString_rhs_1
7+mkString True x = ?mkString_rhs_2
8+
9+mkThing : (str : Bool) -> IntString str
10+mkThing False = ?mkThing_rhs_1
11+mkThing True = ?mkThing_rhs_2
12+
13+mkString2 : (str : Bool) -> IntString str -> String
14+mkString2 str x = ?mkString2_rhs
15+
16+mkString3 : (str : Bool) -> ?what -> String
17+mkString3 False x = ?mkString3_rhs_1
18+mkString3 True x = ?mkString3_rhs_2
19+
20+data Vect : Nat -> Type -> Type where
21+ Nil : Vect Z a
22+ (::) : a -> Vect k a -> Vect (S k) a
23+
24+append : Vect n a -> Vect m a -> Vect (n + m) a
25+append [] ys = ?append_rhs_1
26+append (x :: xs) ys = ?append_rhs_2
test/interactive012/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --quiet interactive012.idr < input
3+rm -f *.ibc
test/reg001/reg001.idr+11
@@ -197,3 +197,14 @@ Max p = (Nat , (k : Nat) -> p k -> Nat)
197197maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat
198198maxEquiv a n1 pr1 = snd a n1 pr1
199199
200+data Rho = R
201+
202+rho : Rho -> Rho
203+rho r = case r of R => r
204+
205+data Kappa : (r : Rho) -> Type where K : Kappa r
206+
207+kappa : Kappa (rho r) -> Kappa (rho r)
208+kappa {r} k = k' where -- k' : Kappa (rho r)
209+ k' = k
210+