git.iko.soy/Idris-dev
on master help sign in
Fix compile error
commit6be4eb2b902f9ba05cbc15d8f0232fa11e68976d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 13 Jan 2013, 14:23 (14 years ago) parent0458d81
5 files changed+12−6
compare with master
unifiedsplit
lib/Prelude/Maybe.idr+2−1 papers/impl-paper/impldtp.tex+4−1 src/Core/Elaborate.hs+2−1 src/Core/Unify.hs+2−2 src/Idris/ElabTerm.hs+2−1
lib/Prelude/Maybe.idr+2−1
@@ -1,6 +1,7 @@
11module Prelude.Maybe
22
33import Builtins
4+import Prelude.Algebra
45
56%access public
67%default total
@@ -53,7 +54,7 @@ maybe_bind (Just x) k = k x
5354instance (Semigroup a) => Semigroup (Maybe a) where
5455 Nothing <+> m = m
5556 m <+> Nothing = m
56− Just m1 <+> Just m2 = Just (m1 <+> m2)
57+ (Just m1) <+> (Just m2) = Just (m1 <+> m2)
5758
5859instance (Monoid a) => Monoid (Maybe a) where
5960 neutral = Nothing
papers/impl-paper/impldtp.tex+4−1
@@ -54,7 +54,10 @@
5454
5555
5656\title
57− {Implementing General Purpose Dependently Typed Programming Languages}
57+[Idris, a General Purpose Dependently Typed Programm Language]
58+{Idris, a General Purpose Dependently Typed Programming Language:
59+Design and Implementation}
60+%Implementing General Purpose Dependently Typed Programming Languages}
5861%\subtitle{Implementing Domain Specific Languages by Overloading}
5962
6063\author[Edwin Brady]
src/Core/Elaborate.hs+2−1
@@ -377,7 +377,8 @@ apply fn imps =
377377 map fst (filter (not.snd) (zip args (map fst imps)))
378378 let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $
379379 unified p
380− let unify = dropGiven dont hs
380+ let unify = -- trace ("Not done " ++ show hs) $
381+ dropGiven dont hs
381382 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)
382383 ptm <- get_term
383384 end_unify
src/Core/Unify.hs+2−2
@@ -31,7 +31,7 @@ unify ctxt env topx topy =
3131 case runStateT (un False [] topx topy) (UI 0 [] []) of
3232 OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
3333-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
34− res ->
34+ res ->
3535 let topxn = normalise ctxt env topx
3636 topyn = normalise ctxt env topy in
3737-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
@@ -129,7 +129,7 @@ unify ctxt env topx topy =
129129 sc 1
130130 combine bnames hf ha)
131131 where hnormalise [] _ _ t = t
132− hnormalise ns ctxt env t = hnf ctxt env t
132+ hnormalise ns ctxt env t = normalise ctxt env t
133133 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
134134 | x /= y = unifyFail appx appy
135135 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
src/Idris/ElabTerm.hs+2−1
@@ -297,7 +297,8 @@ elab ist info pattern tcgen fn tm
297297 solve
298298 return ([], False))
299299 when committed $
300− do let (ns', eargs) = unzip $
300+ do ptm <- get_term
301+ let (ns', eargs) = unzip $
301302 sortBy (\(_,x) (_,y) ->
302303 compare (priority x) (priority y))
303304 (zip ns args)