e8c2bad · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -1,5 +1,5 @@

1Name: idris

2−Version: 0.9.8

2+Version: 0.9.8.1

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

lib/Decidable/Decidable.idr+6−1

@@ -6,6 +6,11 @@ module Decidable.Decidable

6-- Typeclass for decidable n-ary Relations

7--------------------------------------------------------------------------------

8

9+{-

10+This can't work yet! The class parameters must appear in the method type

11+signatures otherwise when defining the instances class resolution doesn't

12+have any clues...

13+

9using (t : Type)

14using (t : Type)

10 class Rel (p : t) where

15 class Rel (p : t) where

11 total liftRel : (Type -> Type) -> Type

16 total liftRel : (Type -> Type) -> Type

@@ -16,4 +21,4 @@ using (t : Type)

16using (P : Type, p : P)

21using (P : Type, p : P)

17 data Given : Dec P -> Type where

22 data Given : Dec P -> Type where

18 always : Given (Yes p)

23 always : Given (Yes p)

19−

24+-}

lib/Decidable/Order.idr+8

@@ -1,5 +1,10 @@

1module Decidable.Order

2

3+%access public

4+

5+{-

6+Doesn't work yet, see note in Decidable.idr

7+

3import Decidable.Decidable

8import Decidable.Decidable

4import Decidable.Equality

9import Decidable.Equality

5

10

@@ -77,3 +82,6 @@ instance Decidable NatLTE where

77

82

78lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)

83lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)

79lte m n = decide {p = NatLTE} m n

84lte m n = decide {p = NatLTE} m n

85+

86+-}

87+

src/Idris/ElabTerm.hs+9−1

@@ -615,9 +615,11 @@ resolveTC depth fn ist

615 if True -- all (\n -> not (n `elem` hs)) (freeNames g)

616 then try' (trivial ist)

617 (do t <- goal

618− let insts = findInstances ist t

619 let (tc, ttypes) = unApply t

618 let (tc, ttypes) = unApply t

620 scopeOnly <- needsDefault t tc ttypes

619 scopeOnly <- needsDefault t tc ttypes

620+ let insts_in = findInstances ist t

621+ let insts = if scopeOnly then filter chaser insts_in

622+ else insts_in

621 tm <- get_term

623 tm <- get_term

622-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

624-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

623-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

625-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

@@ -633,6 +635,12 @@ resolveTC depth fn ist

633 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

635 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

634 | otherwise = (fail "Can't resolve", show n)

636 | otherwise = (fail "Can't resolve", show n)

635

637

638+ -- HACK! Rather than giving a special name, better to have some kind

639+ -- of flag in ClassInfo structure

640+ chaser (UN ('@':'@':_)) = True

641+ chaser (NS n _) = chaser n

642+ chaser _ = False

643+

636 needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _]

644 needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _]

637 = do focus a

645 = do focus a

638 fill (RConstant IType) -- default Int

646 fill (RConstant IType) -- default Int