git.iko.soy/Idris-dev
on master help sign in
with fix
df49a2aEdwin Brady
lib/nat.idr+3
compare with master
unifiedsplit
@@ -9,6 +9,9 @@ plus (S k) y = S (plus k y);
9eqRespS : m = n -> S m = S n;
9eqRespS : m = n -> S m = S n;
10eqRespS refl = refl;
10eqRespS refl = refl;
11
11
12+eqRespS' : S m = S n -> m = n;
13+eqRespS' refl = refl;
14+
12sub : Nat -> Nat -> Nat;
15sub : Nat -> Nat -> Nat;
13sub O y = O;
16sub O y = O;
14sub (S k) (S y) = sub k y;
17sub (S k) (S y) = sub k y;
src/Core/Typecheck.hs+10−10
@@ -43,7 +43,7 @@ check ctxt env (RApp f a)
43 case fty' of
43 case fty' of
44 Bind x (Pi s) t ->
44 Bind x (Pi s) t ->
45 do converts ctxt env s aty
45 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)
47 return (App fv av, apty)
47 return (App fv av, apty)
48 t -> fail "Can't apply a non-function type"
48 t -> fail "Can't apply a non-function type"
49 -- This rather unpleasant hack is needed because during incomplete
49 -- This rather unpleasant hack is needed because during incomplete
@@ -70,13 +70,13 @@ check ctxt env (RBind n b sc)
70 let tv' = normalise ctxt env tv
70 let tv' = normalise ctxt env tv
71 let tt' = normalise ctxt env tt
71 let tt' = normalise ctxt env tt
72 isSet ctxt env tt'
72 isSet ctxt env tt'
73− return (Lam tv')
73+ return (Lam tv)
74 checkBinder (Pi t)
74 checkBinder (Pi t)
75 = do (tv, tt) <- check ctxt env t
75 = do (tv, tt) <- check ctxt env t
76 let tv' = normalise ctxt env tv
76 let tv' = normalise ctxt env tv
77 let tt' = normalise ctxt env tt
77 let tt' = normalise ctxt env tt
78 isSet ctxt env tt'
78 isSet ctxt env tt'
79− return (Pi tv')
79+ return (Pi tv)
80 checkBinder (Let t v)
80 checkBinder (Let t v)
81 = do (tv, tt) <- check ctxt env t
81 = do (tv, tt) <- check ctxt env t
82 (vv, vt) <- check ctxt env v
82 (vv, vt) <- check ctxt env v
@@ -84,7 +84,7 @@ check ctxt env (RBind n b sc)
84 let tt' = normalise ctxt env tt
84 let tt' = normalise ctxt env tt
85 converts ctxt env tv vt
85 converts ctxt env tv vt
86 isSet ctxt env tt'
86 isSet ctxt env tt'
87− return (Let tv' vv)
87+ return (Let tv vv)
88 checkBinder (NLet t v)
88 checkBinder (NLet t v)
89 = do (tv, tt) <- check ctxt env t
89 = do (tv, tt) <- check ctxt env t
90 (vv, vt) <- check ctxt env v
90 (vv, vt) <- check ctxt env v
@@ -92,19 +92,19 @@ check ctxt env (RBind n b sc)
92 let tt' = normalise ctxt env tt
92 let tt' = normalise ctxt env tt
93 converts ctxt env tv vt
93 converts ctxt env tv vt
94 isSet ctxt env tt'
94 isSet ctxt env tt'
95− return (NLet tv' vv)
95+ return (NLet tv vv)
96 checkBinder (Hole t)
96 checkBinder (Hole t)
97 = do (tv, tt) <- check ctxt env t
97 = do (tv, tt) <- check ctxt env t
98 let tv' = normalise ctxt env tv
98 let tv' = normalise ctxt env tv
99 let tt' = normalise ctxt env tt
99 let tt' = normalise ctxt env tt
100 isSet ctxt env tt'
100 isSet ctxt env tt'
101− return (Hole tv')
101+ return (Hole tv)
102 checkBinder (GHole t)
102 checkBinder (GHole t)
103 = do (tv, tt) <- check ctxt env t
103 = do (tv, tt) <- check ctxt env t
104 let tv' = normalise ctxt env tv
104 let tv' = normalise ctxt env tv
105 let tt' = normalise ctxt env tt
105 let tt' = normalise ctxt env tt
106 isSet ctxt env tt'
106 isSet ctxt env tt'
107− return (GHole tv')
107+ return (GHole tv)
108 checkBinder (Guess t v)
108 checkBinder (Guess t v)
109 = do (tv, tt) <- check ctxt env t
109 = do (tv, tt) <- check ctxt env t
110 (vv, vt) <- check ctxt env v
110 (vv, vt) <- check ctxt env v
@@ -112,19 +112,19 @@ check ctxt env (RBind n b sc)
112 let tt' = normalise ctxt env tt
112 let tt' = normalise ctxt env tt
113 converts ctxt env tv vt
113 converts ctxt env tv vt
114 isSet ctxt env tt'
114 isSet ctxt env tt'
115− return (Guess tv' vv)
115+ return (Guess tv vv)
116 checkBinder (PVar t)
116 checkBinder (PVar t)
117 = do (tv, tt) <- check ctxt env t
117 = do (tv, tt) <- check ctxt env t
118 let tv' = normalise ctxt env tv
118 let tv' = normalise ctxt env tv
119 let tt' = normalise ctxt env tt
119 let tt' = normalise ctxt env tt
120 isSet ctxt env tt'
120 isSet ctxt env tt'
121− return (PVar tv')
121+ return (PVar tv)
122 checkBinder (PVTy t)
122 checkBinder (PVTy t)
123 = do (tv, tt) <- check ctxt env t
123 = do (tv, tt) <- check ctxt env t
124 let tv' = normalise ctxt env tv
124 let tv' = normalise ctxt env tv
125 let tt' = normalise ctxt env tt
125 let tt' = normalise ctxt env tt
126 isSet ctxt env tt'
126 isSet ctxt env tt'
127− return (PVTy tv')
127+ return (PVTy tv)
128
128
129 discharge n (Lam t) scv sct
129 discharge n (Lam t) scv sct
130 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
130 = 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
914 = do mf <- match f f'
914 = do mf <- match f f'
915 ms <- zipWithM matchArg args args'
915 ms <- zipWithM matchArg args args'
916 return (mf ++ concat ms)
916 return (mf ++ concat ms)
917− match (PRef _ n) (PRef _ n') | n == n' = return []
917+-- match (PRef _ n) (PRef _ n') | n == n' = return []
918− | otherwise = Nothing
918+-- | otherwise = Nothing
919 match (PRef _ n) tm = return [(n, tm)]
919 match (PRef _ n) tm = return [(n, tm)]
920 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
920 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
921 mr <- match r r'
921 mr <- match r r'
src/Idris/ElabDecls.hs+2−1
@@ -397,7 +397,8 @@ elabInstance info syn fc cs n ps t ds
397 decorateid (PTy s f n t) = PTy s f (decorate n) t
397 decorateid (PTy s f n t) = PTy s f (decorate n) t
398 decorateid (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs)
398 decorateid (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs)
399 where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds
399 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)
401 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as
402 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as
402 dappname t = t
403 dappname t = t
403 mkTyDecl (n, t) = PTy syn fc n t
404 mkTyDecl (n, t) = PTy syn fc n t
src/Idris/REPL.hs+3−2
@@ -32,7 +32,8 @@ repl orig mods
32 = do let prompt = mkPrompt mods
32 = do let prompt = mkPrompt mods
33 x <- lift $ readline (prompt ++ "> ")
33 x <- lift $ readline (prompt ++ "> ")
34 case x of
34 case x of
35+ Nothing -> do iputStrLn "Bye bye"
35− Nothing -> return ()
36+ return ()
36 Just input -> do lift $ addHistory input
37 Just input -> do lift $ addHistory input
37 ms <- processInput input orig mods
38 ms <- processInput input orig mods
38 case ms of
39 case ms of
@@ -100,7 +101,7 @@ process (Check t) = do (tm, ty) <- elabVal toplevel False t
100 ist <- get
101 ist <- get
101 let ty' = normaliseC ctxt [] ty
102 let ty' = normaliseC ctxt [] ty
102 iputStrLn (show (delab ist tm) ++ " : " ++
103 iputStrLn (show (delab ist tm) ++ " : " ++
103− show (delab ist ty'))
104+ show (delab ist ty))
104process (Defn n) = do ctxt <- getContext
105process (Defn n) = do ctxt <- getContext
105 lift $ print (lookupDef n ctxt)
106 lift $ print (lookupDef n ctxt)
106process (Spec t) = do (tm, ty) <- elabVal toplevel False t
107process (Spec t) = do (tm, ty) <- elabVal toplevel False t