git.iko.soy/Idris-dev
on master help sign in
with fix
commitdf49a2a03e36293d19acaf66736bd27c12c59787 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 17 Nov 2011, 21:21 (15 years ago) parentbe2d7fa
5 files changed+20−15
compare with master
unifiedsplit
lib/nat.idr+3 src/Core/Typecheck.hs+10−10 src/Idris/AbsSyntax.hs+2−2 src/Idris/ElabDecls.hs+2−1 src/Idris/REPL.hs+3−2
lib/nat.idr+3
@@ -9,6 +9,9 @@ plus (S k) y = S (plus k y);
99eqRespS : m = n -> S m = S n;
1010eqRespS refl = refl;
1111
12+eqRespS' : S m = S n -> m = n;
13+eqRespS' refl = refl;
14+
1215sub : Nat -> Nat -> Nat;
1316sub O y = O;
1417sub (S k) (S y) = sub k y;
src/Core/Typecheck.hs+10−10
@@ -43,7 +43,7 @@ check ctxt env (RApp f a)
4343 case fty' of
4444 Bind x (Pi s) t ->
4545 do converts ctxt env s aty
46− let apty = normalise ctxt env (Bind x (Let aty av) t)
46+ let apty = normalise emptyContext env (Bind x (Let aty av) t)
4747 return (App fv av, apty)
4848 t -> fail "Can't apply a non-function type"
4949 -- This rather unpleasant hack is needed because during incomplete
@@ -70,13 +70,13 @@ check ctxt env (RBind n b sc)
7070 let tv' = normalise ctxt env tv
7171 let tt' = normalise ctxt env tt
7272 isSet ctxt env tt'
73− return (Lam tv')
73+ return (Lam tv)
7474 checkBinder (Pi t)
7575 = do (tv, tt) <- check ctxt env t
7676 let tv' = normalise ctxt env tv
7777 let tt' = normalise ctxt env tt
7878 isSet ctxt env tt'
79− return (Pi tv')
79+ return (Pi tv)
8080 checkBinder (Let t v)
8181 = do (tv, tt) <- check ctxt env t
8282 (vv, vt) <- check ctxt env v
@@ -84,7 +84,7 @@ check ctxt env (RBind n b sc)
8484 let tt' = normalise ctxt env tt
8585 converts ctxt env tv vt
8686 isSet ctxt env tt'
87− return (Let tv' vv)
87+ return (Let tv vv)
8888 checkBinder (NLet t v)
8989 = do (tv, tt) <- check ctxt env t
9090 (vv, vt) <- check ctxt env v
@@ -92,19 +92,19 @@ check ctxt env (RBind n b sc)
9292 let tt' = normalise ctxt env tt
9393 converts ctxt env tv vt
9494 isSet ctxt env tt'
95− return (NLet tv' vv)
95+ return (NLet tv vv)
9696 checkBinder (Hole t)
9797 = do (tv, tt) <- check ctxt env t
9898 let tv' = normalise ctxt env tv
9999 let tt' = normalise ctxt env tt
100100 isSet ctxt env tt'
101− return (Hole tv')
101+ return (Hole tv)
102102 checkBinder (GHole t)
103103 = do (tv, tt) <- check ctxt env t
104104 let tv' = normalise ctxt env tv
105105 let tt' = normalise ctxt env tt
106106 isSet ctxt env tt'
107− return (GHole tv')
107+ return (GHole tv)
108108 checkBinder (Guess t v)
109109 = do (tv, tt) <- check ctxt env t
110110 (vv, vt) <- check ctxt env v
@@ -112,19 +112,19 @@ check ctxt env (RBind n b sc)
112112 let tt' = normalise ctxt env tt
113113 converts ctxt env tv vt
114114 isSet ctxt env tt'
115− return (Guess tv' vv)
115+ return (Guess tv vv)
116116 checkBinder (PVar t)
117117 = do (tv, tt) <- check ctxt env t
118118 let tv' = normalise ctxt env tv
119119 let tt' = normalise ctxt env tt
120120 isSet ctxt env tt'
121− return (PVar tv')
121+ return (PVar tv)
122122 checkBinder (PVTy t)
123123 = do (tv, tt) <- check ctxt env t
124124 let tv' = normalise ctxt env tv
125125 let tt' = normalise ctxt env tt
126126 isSet ctxt env tt'
127− return (PVTy tv')
127+ return (PVTy tv)
128128
129129 discharge n (Lam t) scv sct
130130 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
src/Idris/AbsSyntax.hs+2−2
@@ -914,8 +914,8 @@ matchClause x y = match x y where
914914 = do mf <- match f f'
915915 ms <- zipWithM matchArg args args'
916916 return (mf ++ concat ms)
917− match (PRef _ n) (PRef _ n') | n == n' = return []
918− | otherwise = Nothing
917+-- match (PRef _ n) (PRef _ n') | n == n' = return []
918+-- | otherwise = Nothing
919919 match (PRef _ n) tm = return [(n, tm)]
920920 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
921921 mr <- match r r'
src/Idris/ElabDecls.hs+2−1
@@ -397,7 +397,8 @@ elabInstance info syn fc cs n ps t ds
397397 decorateid (PTy s f n t) = PTy s f (decorate n) t
398398 decorateid (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs)
399399 where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds
400− dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w ds
400+ dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w
401+ (map decorateid ds)
401402 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as
402403 dappname t = t
403404 mkTyDecl (n, t) = PTy syn fc n t
src/Idris/REPL.hs+3−2
@@ -32,7 +32,8 @@ repl orig mods
3232 = do let prompt = mkPrompt mods
3333 x <- lift $ readline (prompt ++ "> ")
3434 case x of
35− Nothing -> return ()
35+ Nothing -> do iputStrLn "Bye bye"
36+ return ()
3637 Just input -> do lift $ addHistory input
3738 ms <- processInput input orig mods
3839 case ms of
@@ -100,7 +101,7 @@ process (Check t) = do (tm, ty) <- elabVal toplevel False t
100101 ist <- get
101102 let ty' = normaliseC ctxt [] ty
102103 iputStrLn (show (delab ist tm) ++ " : " ++
103− show (delab ist ty'))
104+ show (delab ist ty))
104105process (Defn n) = do ctxt <- getContext
105106 lift $ print (lookupDef n ctxt)
106107process (Spec t) = do (tm, ty) <- elabVal toplevel False t