6be4eb2 · Idris-dev · git.iko.soy

lib/Prelude/Maybe.idr+2−1

compare with master

unifiedsplit

@@ -1,6 +1,7 @@

1module Prelude.Maybe

2

3import Builtins

4+import Prelude.Algebra

4

5

5%access public

6%access public

6%default total

7%default total

@@ -53,7 +54,7 @@ maybe_bind (Just x) k = k x

53instance (Semigroup a) => Semigroup (Maybe a) where

54instance (Semigroup a) => Semigroup (Maybe a) where

54 Nothing <+> m = m

55 Nothing <+> m = m

55 m <+> Nothing = m

56 m <+> Nothing = m

56− Just m1 <+> Just m2 = Just (m1 <+> m2)

57+ (Just m1) <+> (Just m2) = Just (m1 <+> m2)

57

58

58instance (Monoid a) => Monoid (Maybe a) where

59instance (Monoid a) => Monoid (Maybe a) where

59 neutral = Nothing

60 neutral = Nothing

papers/impl-paper/impldtp.tex+4−1

@@ -54,7 +54,10 @@

54

55

56\title

57+[Idris, a General Purpose Dependently Typed Programm Language]

58+{Idris, a General Purpose Dependently Typed Programming Language:

59+Design and Implementation}

57− {Implementing General Purpose Dependently Typed Programming Languages}

60+%Implementing General Purpose Dependently Typed Programming Languages}

58%\subtitle{Implementing Domain Specific Languages by Overloading}

61%\subtitle{Implementing Domain Specific Languages by Overloading}

59

62

60\author[Edwin Brady]

63\author[Edwin Brady]

src/Core/Elaborate.hs+2−1

@@ -377,7 +377,8 @@ apply fn imps =

377 map fst (filter (not.snd) (zip args (map fst imps)))

378 let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

379 unified p

380+ let unify = -- trace ("Not done " ++ show hs) $

380− let unify = dropGiven dont hs

381+ dropGiven dont hs

381 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

382 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

382 ptm <- get_term

383 ptm <- get_term

383 end_unify

384 end_unify

src/Core/Unify.hs+2−2

@@ -31,7 +31,7 @@ unify ctxt env topx topy =

31 case runStateT (un False [] topx topy) (UI 0 [] []) of

32 OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

33-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

34− res ->

34+ res ->

35 let topxn = normalise ctxt env topx

36 topyn = normalise ctxt env topy in

37-- 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 =

129 sc 1

130 combine bnames hf ha)

131 where hnormalise [] _ _ t = t

132− hnormalise ns ctxt env t = hnf ctxt env t

132+ hnormalise ns ctxt env t = normalise ctxt env t

133 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

134 | x /= y = unifyFail appx appy

135 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

src/Idris/ElabTerm.hs+2−1

@@ -297,7 +297,8 @@ elab ist info pattern tcgen fn tm

297 solve

298 return ([], False))

299 when committed $

300+ do ptm <- get_term

300− do let (ns', eargs) = unzip $

301+ let (ns', eargs) = unzip $

301 sortBy (\(_,x) (_,y) ->

302 sortBy (\(_,x) (_,y) ->

302 compare (priority x) (priority y))

303 compare (priority x) (priority y))

303 (zip ns args)

304 (zip ns args)