git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master' into providers
40208c4David Christiansen
CHANGELOG+1
compare with master
unifiedsplit
@@ -14,6 +14,7 @@ User visible changes:
14
14
15Internal changes:
15Internal changes:
16
16
17+* Fix non-linear pattern checking
17* Improved name disambiguation
18* Improved name disambiguation
18* More flexible unification and elaboration of lambdas
19* More flexible unification and elaboration of lambdas
19* Various unification and totality checking bug fixes
20* Various unification and totality checking bug fixes
lib/Data/SortedMap.idrnew file+235
@@ -0,0 +1,235 @@
1+module Data.SortedMap
2+
3+-- TODO: write merge and split
4+
5+data Tree : Nat -> Type -> Type -> Type where
6+ Leaf : k -> v -> Tree O k v
7+ Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v
8+ Branch3 : Tree n k v -> k -> Tree n k v -> k -> Tree n k v -> Tree (S n) k v
9+
10+branch4 :
11+ Tree n k v -> k ->
12+ Tree n k v -> k ->
13+ Tree n k v -> k ->
14+ Tree n k v ->
15+ Tree (S (S n)) k v
16+branch4 a b c d e f g =
17+ Branch2 (Branch2 a b c) d (Branch2 e f g)
18+
19+branch5 :
20+ Tree n k v -> k ->
21+ Tree n k v -> k ->
22+ Tree n k v -> k ->
23+ Tree n k v -> k ->
24+ Tree n k v ->
25+ Tree (S (S n)) k v
26+branch5 a b c d e f g h i =
27+ Branch2 (Branch2 a b c) d (Branch3 e f g h i)
28+
29+branch6 :
30+ Tree n k v -> k ->
31+ Tree n k v -> k ->
32+ Tree n k v -> k ->
33+ Tree n k v -> k ->
34+ Tree n k v -> k ->
35+ Tree n k v ->
36+ Tree (S (S n)) k v
37+branch6 a b c d e f g h i j k =
38+ Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)
39+
40+branch7 :
41+ Tree n k v -> k ->
42+ Tree n k v -> k ->
43+ Tree n k v -> k ->
44+ Tree n k v -> k ->
45+ Tree n k v -> k ->
46+ Tree n k v -> k ->
47+ Tree n k v ->
48+ Tree (S (S n)) k v
49+branch7 a b c d e f g h i j k l m =
50+ Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)
51+
52+merge1 : Tree n k v -> k -> Tree (S n) k v -> k -> Tree (S n) k v -> Tree (S (S n)) k v
53+merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
54+merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
55+merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
56+merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m
57+
58+merge2 : Tree (S n) k v -> k -> Tree n k v -> k -> Tree (S n) k v -> Tree (S (S n)) k v
59+merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
60+merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
61+merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
62+merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m
63+
64+merge3 : Tree (S n) k v -> k -> Tree (S n) k v -> k -> Tree n k v -> Tree (S (S n)) k v
65+merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
66+merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
67+merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
68+merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m
69+
70+treeLookup : Ord k => k -> Tree n k v -> Maybe v
71+treeLookup k (Leaf k' v) =
72+ if k == k' then
73+ Just v
74+ else
75+ Nothing
76+treeLookup k (Branch2 t1 k' t2) =
77+ if k <= k' then
78+ treeLookup k t1
79+ else
80+ treeLookup k t2
81+treeLookup k (Branch3 t1 k1 t2 k2 t3) =
82+ if k <= k1 then
83+ treeLookup k t1
84+ else if k <= k2 then
85+ treeLookup k t2
86+ else
87+ treeLookup k t3
88+
89+treeInsert' : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree n k v, k, Tree n k v)
90+treeInsert' k v (Leaf k' v') =
91+ case compare k k' of
92+ LT => Right (Leaf k v, k, Leaf k' v')
93+ EQ => Left (Leaf k v)
94+ GT => Right (Leaf k' v', k', Leaf k v)
95+treeInsert' k v (Branch2 t1 k' t2) =
96+ if k <= k' then
97+ case treeInsert' k v t1 of
98+ Left t1' => Left (Branch2 t1' k' t2)
99+ Right (a, b, c) => Left (Branch3 a b c k' t2)
100+ else
101+ case treeInsert' k v t2 of
102+ Left t2' => Left (Branch2 t1 k' t2')
103+ Right (a, b, c) => Left (Branch3 t1 k' a b c)
104+treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
105+ if k <= k1 then
106+ case treeInsert' k v t1 of
107+ Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
108+ Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)
109+ else
110+ if k <= k2 then
111+ case treeInsert' k v t2 of
112+ Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
113+ Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)
114+ else
115+ case treeInsert' k v t3 of
116+ Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
117+ Right (a, b, c) => Right (Branch2 t1 k2 t2, k2, Branch2 a b c)
118+
119+treeInsert : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree (S n) k v)
120+treeInsert k v t =
121+ case treeInsert' k v t of
122+ Left t' => Left t'
123+ Right (a, b, c) => Right (Branch2 a b c)
124+
125+delType : Nat -> Type -> Type -> Type
126+delType O k v = ()
127+delType (S n) k v = Tree n k v
128+
129+treeDelete : Ord k => k -> Tree n k v -> Either (Tree n k v) (delType n k v)
130+treeDelete k (Leaf k' v) =
131+ if k == k' then
132+ Right ()
133+ else
134+ Left (Leaf k' v)
135+treeDelete {n=S O} k (Branch2 t1 k' t2) =
136+ if k <= k' then
137+ case treeDelete k t1 of
138+ Left t1' => Left (Branch2 t1' k' t2)
139+ Right () => Right t2
140+ else
141+ case treeDelete k t2 of
142+ Left t2' => Left (Branch2 t1 k' t2')
143+ Right () => Right t1
144+treeDelete {n=S O} k (Branch3 t1 k1 t2 k2 t3) =
145+ if k <= k1 then
146+ case treeDelete k t1 of
147+ Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
148+ Right () => Left (Branch2 t2 k2 t3)
149+ else if k <= k2 then
150+ case treeDelete k t2 of
151+ Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
152+ Right () => Left (Branch2 t1 k1 t3)
153+ else
154+ case treeDelete k t3 of
155+ Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
156+ Right () => Left (Branch2 t1 k1 t2)
157+treeDelete {n=S (S _)} k (Branch2 t1 k' t2) =
158+ if k <= k' then
159+ case treeDelete k t1 of
160+ Left t1' => Left (Branch2 t1' k' t2)
161+ Right t1' =>
162+ case t2 of
163+ Branch2 a b c => Right (Branch3 t1' k' a b c)
164+ Branch3 a b c d e => Left (branch4 t1' k' a b c d e)
165+ else
166+ case treeDelete k t2 of
167+ Left t2' => Left (Branch2 t1 k' t2')
168+ Right t2' =>
169+ case t1 of
170+ Branch2 a b c => Right (Branch3 a b c k' t2')
171+ Branch3 a b c d e => Left (branch4 a b c d e k' t2')
172+treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
173+ if k <= k1 then
174+ case treeDelete k t1 of
175+ Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
176+ Right t1' => Left (merge1 t1' k1 t2 k2 t3)
177+ else if k <= k2 then
178+ case treeDelete k t2 of
179+ Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
180+ Right t2' => Left (merge2 t1 k1 t2' k2 t3)
181+ else
182+ case treeDelete k t3 of
183+ Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
184+ Right t3' => Left (merge3 t1 k1 t2 k2 t3')
185+
186+-- FIXME: this is very inefficient
187+treeToList : Ord k => Tree n k v -> List (k, v)
188+treeToList (Leaf k v) = [(k, v)]
189+treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2
190+treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3
191+
192+data SortedMap : Type -> Type -> Type where
193+ Empty : SortedMap k v
194+ M : (n:Nat) -> Tree n k v -> SortedMap k v
195+
196+empty : SortedMap k v
197+empty = Empty
198+
199+lookup : Ord k => k -> SortedMap k v -> Maybe v
200+lookup _ Empty = Nothing
201+lookup k (M _ t) = treeLookup k t
202+
203+insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v
204+insert k v Empty = M O (Leaf k v)
205+insert k v (M _ t) =
206+ case treeInsert k v t of
207+ Left t' => (M _ t')
208+ Right t' => (M _ t')
209+
210+delete : Ord k => k -> SortedMap k v -> SortedMap k v
211+delete _ Empty = Empty
212+delete k (M O t) =
213+ case treeDelete k t of
214+ Left t' => (M _ t')
215+ Right () => Empty
216+delete k (M (S _) t) =
217+ case treeDelete k t of
218+ Left t' => (M _ t')
219+ Right t' => (M _ t')
220+
221+fromList : Ord k => List (k, v) -> SortedMap k v
222+fromList l = foldl (flip (uncurry insert)) empty l
223+
224+toList : Ord k => SortedMap k v -> List (k, v)
225+toList Empty = []
226+toList (M _ t) = treeToList t
227+
228+instance Functor (Tree n k) where
229+ fmap f (Leaf k v) = Leaf k (f v)
230+ fmap f (Branch2 t1 k t2) = Branch2 (fmap f t1) k (fmap f t2)
231+ fmap f (Branch3 t1 k1 t2 k2 t3) = Branch3 (fmap f t1) k1 (fmap f t2) k2 (fmap f t3)
232+
233+instance Functor (SortedMap k) where
234+ fmap _ Empty = Empty
235+ fmap f (M _ t) = M _ (fmap f t)
lib/Data/SortedSet.idrnew file+25
@@ -0,0 +1,25 @@
1+module Data.SortedSet
2+
3+import Data.SortedMap
4+
5+-- TODO: add intersection, union, difference
6+
7+data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
8+
9+empty : SortedSet k
10+empty = SetWrapper Data.SortedMap.empty
11+
12+insert : Ord k => k -> SortedSet k -> SortedSet k
13+insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
14+
15+delete : Ord k => k -> SortedSet k -> SortedSet k
16+delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
17+
18+contains : Ord k => k -> SortedSet k -> Bool
19+contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
20+
21+fromList : Ord k => List k -> SortedSet k
22+fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
23+
24+toList : Ord k => SortedSet k -> List k
25+toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
lib/Decidable/Decidable.idrnew file+14
@@ -0,0 +1,14 @@
1+module Decidable.Decidable
2+
3+%access public
4+
5+--------------------------------------------------------------------------------
6+-- Typeclass for decidable n-ary Relations
7+--------------------------------------------------------------------------------
8+
9+using (t : Type)
10+ class Rel (p : t) where
11+ total liftRel : (Type -> Type) -> Type
12+
13+ class (Rel p) => Decidable (p : t) where
14+ total decide : liftRel Dec
lib/Decidable/Equality.idr+1−1
@@ -75,7 +75,7 @@ total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _
75leftNotRight refl impossible
75leftNotRight refl impossible
76
76
77instance (DecEq a, DecEq b) => DecEq (Either a b) where
77instance (DecEq a, DecEq b) => DecEq (Either a b) where
78− decEq {b=b} (Left x') (Left y') with (decEq x' y')
78+ decEq (Left x') (Left y') with (decEq x' y')
79 | Yes p = Yes $ cong p
79 | Yes p = Yes $ cong p
80 | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
80 | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
81 decEq (Right x') (Right y') with (decEq x' y')
81 decEq (Right x') (Right y') with (decEq x' y')
lib/Decidable/Order.idrnew file+79
@@ -0,0 +1,79 @@
1+module Decidable.Order
2+
3+import Decidable.Decidable
4+import Decidable.Equality
5+
6+--------------------------------------------------------------------------------
7+-- Utility Lemmas
8+--------------------------------------------------------------------------------
9+
10+--------------------------------------------------------------------------------
11+-- Preorders and Posets
12+--------------------------------------------------------------------------------
13+
14+using (t : Type)
15+ data Preorder : (t -> t -> Type) -> Type where
16+ transRefl : ((a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c) ->
17+ ((a : t) -> po a a) ->
18+ Preorder po
19+
20+
21+ data Poset : (t -> t -> Type) -> Type where
22+ preorderAntisym : Preorder {t = t} po ->
23+ ((a : t) -> (b : t) -> po a b -> po b a -> a = b) ->
24+ Poset po
25+
26+--------------------------------------------------------------------------------
27+-- Natural numbers
28+--------------------------------------------------------------------------------
29+
30+data NatLTE : Nat -> Nat -> Type where
31+ nEqn : NatLTE n n
32+ nLTESm : NatLTE n m -> NatLTE n (S m)
33+
34+total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
35+ NatLTE m n -> NatLTE n o ->
36+ NatLTE m o
37+NatLTEIsTransitive m n n mLTEn (nEqn) = mLTEn
38+NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)
39+ = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)
40+
41+total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
42+NatLTEIsReflexive _ = nEqn
43+
44+NatLTEIsPreorder : Preorder NatLTE
45+NatLTEIsPreorder = transRefl NatLTEIsTransitive NatLTEIsReflexive
46+
47+total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> po m n -> po n m -> m = n
48+NatLTEIsAntisymmetric n n nEqn nEqn = refl
49+NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
50+NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
51+
52+NatLTEIsPoset : Poset NatLTE
53+NatLTEIsPoset = preorderAntisym NatLTEIsPreorder NatLTEIsAntisymmetric
54+
55+total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_
56+zeroNeverGreater {n} (nLTESm _) impossible
57+zeroNeverGreater {n} nEqn impossible
58+
59+total
60+nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_
61+nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)
62+nGTSm {n} {m} disprf (nEqn) impossible
63+
64+total
65+decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)
66+decideNatLTE O O = Yes nEqn
67+decideNatLTE (S x) O = No zeroNeverGreater
68+decideNatLTE x (S y) with (decEq x (S y))
69+ | Yes eq = rewrite eq in Yes nEqn
70+ | No _ with (decideNatLTE x y)
71+ | Yes nLTEm = Yes (nLTESm nLTEm)
72+ | No nGTm = No (nGTSm nGTm)
73+
74+instance Rel NatLTE where
75+ liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
76+
77+instance Decidable NatLTE where
78+ decide = decideNatLTE
79+
lib/Prelude.idr+2−2
@@ -189,12 +189,12 @@ ceiling x = prim__floatCeil x
189
189
190---- Ranges
190---- Ranges
191
191
192−%assert_total
192+partial abstract
193count : (Ord a, Num a) => a -> a -> a -> List a
193count : (Ord a, Num a) => a -> a -> a -> List a
194count a inc b = if a <= b then a :: count (a + inc) inc b
194count a inc b = if a <= b then a :: count (a + inc) inc b
195 else []
195 else []
196
196
197−partial
197+partial abstract
198countFrom : (Ord a, Num a) => a -> a -> List a
198countFrom : (Ord a, Num a) => a -> a -> List a
199countFrom a inc = a :: lazy (countFrom (a + inc) inc)
199countFrom a inc = a :: lazy (countFrom (a + inc) inc)
200
200
lib/base.ipkg+2−1
@@ -13,7 +13,7 @@ modules = Builtins, Prelude, IO, System,
13
13
14 System.Concurrency.Raw, System.Concurrency.Process,
14 System.Concurrency.Raw, System.Concurrency.Process,
15
15
16− Decidable.Equality,
16+ Decidable.Equality, Decidable.Decidable, Decidable.Order,
17
17
18 Uninhabited,
18 Uninhabited,
19
19
@@ -22,6 +22,7 @@ modules = Builtins, Prelude, IO, System,
22 Language.Reflection,
22 Language.Reflection,
23
23
24 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,
24 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,
25+ Data.SortedMap, Data.SortedSet,
25
26
26 Control.Monad.Identity, Control.Monad.State, Control.Category,
27 Control.Monad.Identity, Control.Monad.State, Control.Category,
27 Control.Arrow,
28 Control.Arrow,
src/Core/Elaborate.hs+13
@@ -525,6 +525,19 @@ arg n tyhole = do ty <- unique_hole tyhole
525 claim ty RType
525 claim ty RType
526 forall n (Var ty)
526 forall n (Var ty)
527
527
528+-- try a tactic, if it adds any unification problem, return an error
529+no_errors :: Elab' aux () -> Elab' aux ()
530+no_errors tac
531+ = do ps <- get_probs
532+ tac
533+ ps' <- get_probs
534+ if (length ps' > length ps) then
535+ case reverse ps' of
536+ ((x,y,env,err) : _) ->
537+ let env' = map (\(x, b) -> (x, binderTy b)) env in
538+ lift $ tfail $ CantUnify False x y err env' 0
539+ else return ()
540+
528-- Try a tactic, if it fails, try another
541-- Try a tactic, if it fails, try another
529try :: Elab' aux a -> Elab' aux a -> Elab' aux a
542try :: Elab' aux a -> Elab' aux a -> Elab' aux a
530try t1 t2 = try' t1 t2 False
543try t1 t2 = try' t1 t2 False
src/Core/ProofState.hs+1−1
@@ -162,7 +162,7 @@ unify' ctxt env topx topy =
162-- -- " in " ++ show env ++
162-- -- " in " ++ show env ++
163-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
163-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
164-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"
164-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"
165−-- -- ++ show (pterm ps)
165+-- ++ show (pterm ps)
166-- ++ "\n----------") $
166-- ++ "\n----------") $
167 case fails of
167 case fails of
168-- [] -> return u
168-- [] -> return u
src/Idris/AbsSyntax.hs+2
@@ -1074,6 +1074,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1074-- match (PRef _ n) (PRef _ n') | n == n' = return []
1074-- match (PRef _ n) (PRef _ n') | n == n' = return []
1075-- | otherwise = Nothing
1075-- | otherwise = Nothing
1076 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1076 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1077+ match (PPatvar f n) xr = match (PRef f n) xr
1078+ match xr (PPatvar f n) = match xr (PRef f n)
1077 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1079 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1078 match (PRef _ n) tm@(PRef _ n')
1080 match (PRef _ n) tm@(PRef _ n')
1079 | n == n' && not names &&
1081 | n == n' && not names &&
src/Idris/AbsSyntaxTree.hs+35−1
@@ -979,7 +979,7 @@ prettyImp impl = prettySe 10
979showImp :: Bool -> PTerm -> String
979showImp :: Bool -> PTerm -> String
980showImp impl tm = se 10 tm where
980showImp impl tm = se 10 tm where
981 se p (PQuote r) = "![" ++ show r ++ "]"
981 se p (PQuote r) = "![" ++ show r ++ "]"
982− se p (PPatvar fc n) = show n
982+ se p (PPatvar fc n) = if impl then show n ++ "[p]" else show n
983 se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
983 se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
984 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
984 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
985 else showbasic n
985 else showbasic n
@@ -1014,6 +1014,9 @@ showImp impl tm = se 10 tm where
1014 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1014 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1015 se p (PPi (TacImp _ _ s _) n ty sc)
1015 se p (PPi (TacImp _ _ s _) n ty sc)
1016 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1016 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1017+ se p e
1018+ | Just str <- slist p e = str
1019+ | Just num <- snat p e = show num
1017 se p (PApp _ (PRef _ f) [])
1020 se p (PApp _ (PRef _ f) [])
1018 | not impl = show f
1021 | not impl = show f
1019 se p (PApp _ (PRef _ op@(UN (f:_))) args)
1022 se p (PApp _ (PRef _ op@(UN (f:_))) args)
@@ -1052,6 +1055,37 @@ showImp impl tm = se 10 tm where
1052 se p (PCoerced t) = se p t
1055 se p (PCoerced t) = se p t
1053-- se p x = "Not implemented"
1056-- se p x = "Not implemented"
1054
1057
1058+ slist' p (PApp _ (PRef _ nil) _)
1059+ | nsroot nil == UN "Nil" = Just []
1060+ slist' p (PApp _ (PRef _ cons) args)
1061+ | nsroot cons == UN "::",
1062+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1063+ all isImp imps,
1064+ Just tl' <- slist' p tl
1065+ = Just (hd:tl')
1066+ where
1067+ isImp (PImp {}) = True
1068+ isImp _ = False
1069+ slist' _ _ = Nothing
1070+
1071+ slist p e | Just es <- slist' p e = Just $
1072+ case es of [] -> "[]"
1073+ [x] -> "[" ++ se p x ++ "]"
1074+ xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
1075+ slist _ _ = Nothing
1076+
1077+ -- since Prelude is always imported, S & O are unqualified iff they're the
1078+ -- Nat ones.
1079+ snat p (PRef _ o)
1080+ | show o == (natns++"O") || show o == "O" = Just 0
1081+ snat p (PApp _ s [PExp {getTm=n}])
1082+ | show s == (natns++"S") || show s == "S",
1083+ Just n' <- snat p n
1084+ = Just $ 1 + n'
1085+ snat _ _ = Nothing
1086+
1087+ natns = "Prelude.Nat."
1088+
1055 sArg (PImp _ _ n tm _) = siArg (n, tm)
1089 sArg (PImp _ _ n tm _) = siArg (n, tm)
1056 sArg (PExp _ _ tm _) = seArg tm
1090 sArg (PExp _ _ tm _) = seArg tm
1057 sArg (PConstraint _ _ tm _) = scArg tm
1091 sArg (PConstraint _ _ tm _) = scArg tm
src/Idris/Delaborate.hs+1
@@ -21,6 +21,7 @@ delabTy i n
21 = case lookupTy n (tt_ctxt i) of
21 = case lookupTy n (tt_ctxt i) of
22 (ty:_) -> case lookupCtxt n (idris_implicits i) of
22 (ty:_) -> case lookupCtxt n (idris_implicits i) of
23 (imps:_) -> delabTy' i imps ty False
23 (imps:_) -> delabTy' i imps ty False
24+ _ -> delabTy' i [] ty False
24
25
25delab' :: IState -> Term -> Bool -> PTerm
26delab' :: IState -> Term -> Bool -> PTerm
26delab' i t f = delabTy' i [] t f
27delab' i t f = delabTy' i [] t f
src/Idris/ElabDecls.hs+52−31
@@ -147,7 +147,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
147 ttag <- getName
147 ttag <- getName
148 i <- getIState
148 i <- getIState
149 let as = map (const Nothing) (getArgTys cty)
149 let as = map (const Nothing) (getArgTys cty)
150− let params = findParams (zip as (repeat True)) (map snd cons)
150+ let params = findParams (map snd cons)
151 logLvl 2 $ "Parameters : " ++ show params
151 logLvl 2 $ "Parameters : " ++ show params
152 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
152 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
153 (idris_datatypes i) })
153 (idris_datatypes i) })
@@ -161,32 +161,53 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
161 where
161 where
162 -- parameters are names which are unchanged across the structure,
162 -- parameters are names which are unchanged across the structure,
163 -- which appear exactly once in the return type of a constructor
163 -- which appear exactly once in the return type of a constructor
164− findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]
164+
165− findParams ps [] = mapMaybe (\ ((x, y), n) ->
165+ -- First, find all applications of the constructor, then check over
166− if y then Just n else Nothing)
166+ -- them for repeated arguments
167− (zip ps [0..])
167+
168− findParams ps (t : ts) = findParams (updateParams ps t) ts
168+ findParams :: [Type] -> [Int]
169−
169+ findParams ts = let allapps = concatMap getDataApp ts in
170− updateParams ps (Bind n (Pi t) sc)
170+ paramPos allapps
171− = updateParams (updateParams ps (instantiate (P Bound n t) sc)) t
171+
172− updateParams ps tm@(App f a)
172+ paramPos [] = []
173+ paramPos (args : rest)
174+ = dropNothing $ keepSame (zip [0..] args) rest
175+
176+ dropNothing [] = []
177+ dropNothing ((x, Nothing) : ts) = dropNothing ts
178+ dropNothing ((x, _) : ts) = x : dropNothing ts
179+
180+ keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
181+ [(Int, Maybe Name)]
182+ keepSame as [] = as
183+ keepSame as (args : rest) = keepSame (update as args) rest
184+ where
185+ update [] _ = []
186+ update _ [] = []
187+ update ((n, Just x) : as) (Just x' : args)
188+ | x == x' = (n, Just x) : update as args
189+ update ((n, _) : as) (_ : args) = (n, Nothing) : update as args
190+
191+ getDataApp :: Type -> [[Maybe Name]]
192+ getDataApp f@(App _ _)
173− | (P _ fn _, args) <- unApply tm
193+ | (P _ d _, args) <- unApply f
174− = if fn == n
194+ = if (d == n) then [mParam args args] else []
175− then updateParamsA ps args (tail args)
195+ getDataApp (Bind n (Pi t) sc)
176− else updateParams (updateParams ps f) a
196+ = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
177− | otherwise = updateParams (updateParams ps f) a
197+ getDataApp _ = []
178− updateParams ps _ = ps
198+
179−
199+ -- keep the arguments which are single names, which don't appear
180− updateParamsA ((mn, _) : ns) (p@(P _ n' _) : args) all
200+ -- elsewhere
201+
202+ mParam args [] = []
203+ mParam args (P Bound n _ : rest)
204+ | count n args == 1
205+ = Just n : mParam args rest
206+ where count n [] = 0
207+ count n (t : ts)
181− | n' `elem` concatMap freeNames all
208+ | n `elem` freeNames t = 1 + count n ts
182− = (mn, False) : updateParamsA ns args (p : all)
209+ | otherwise = count n ts
183− updateParamsA ((Nothing, b) : ns) (p@(P _ n' _) : args) all
210+ mParam args (_ : rest) = Nothing : mParam args rest
184− = (Just n', b) : updateParamsA ns args (p : all)
185− updateParamsA ((Just p, b) : ns) (tm@(P _ n' _) : args) all
186− = (Just n', b && p == n') : updateParamsA ns args (tm : all)
187− updateParamsA ((mn, _) : ns) (p : args) all
188− = (mn, False) : updateParamsA ns args (p : all)
189− updateParamsA ps args all = ps
190
211
191-- | Elaborate a type provider
212-- | Elaborate a type provider
192elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
213elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
@@ -712,7 +733,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
712 -- Build the LHS as an "Infer", and pull out its type and
733 -- Build the LHS as an "Infer", and pull out its type and
713 -- pattern bindings
734 -- pattern bindings
714 i <- getIState
735 i <- getIState
715− let lhs = addImpl i lhs_in
736+ let lhs = addImplPat i lhs_in
716 logLvl 5 ("LHS: " ++ showImp True lhs)
737 logLvl 5 ("LHS: " ++ showImp True lhs)
717 ((lhs', dlhs, []), _) <-
738 ((lhs', dlhs, []), _) <-
718 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
739 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
@@ -810,18 +831,18 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
810
831
811 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
832 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
812 = do i <- getIState
833 = do i <- getIState
813− let tm = addImpl i tm_in
834+ let tm = addImplPat i tm_in
814 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
835 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
815 showImp True toplhs)
836 showImp True toplhs)
816 case matchClause i toplhs tm of
837 case matchClause i toplhs tm of
817− Left _ -> fail $ show fc ++ "with clause does not match top level"
838+ Left f -> fail $ show fc ++ ":with clause does not match top level"
818 Right mvars ->
839 Right mvars ->
819 do logLvl 3 ("Match vars : " ++ show mvars)
840 do logLvl 3 ("Match vars : " ++ show mvars)
820 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
841 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
821 return $ PClause fc wname lhs ws rhs wheres
842 return $ PClause fc wname lhs ws rhs wheres
822 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
843 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
823 = do i <- getIState
844 = do i <- getIState
824− let tm = addImpl i tm_in
845+ let tm = addImplPat i tm_in
825 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
846 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
826 showImp True toplhs)
847 showImp True toplhs)
827 withs' <- mapM (mkAuxC wname toplhs ns ns') withs
848 withs' <- mapM (mkAuxC wname toplhs ns ns') withs
src/Idris/ElabTerm.hs+4−2
@@ -695,10 +695,12 @@ collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)
695collectDeferred t = return t
695collectDeferred t = return t
696
696
697-- Running tactics directly
697-- Running tactics directly
698+-- if a tactic adds unification problems, return an error
698
699
699runTac :: Bool -> IState -> PTactic -> ElabD ()
700runTac :: Bool -> IState -> PTactic -> ElabD ()
700−runTac autoSolve ist tac = do env <- get_env
701+runTac autoSolve ist tac
702+ = do env <- get_env
701− runT (fmap (addImplBound ist (map fst env)) tac)
703+ no_errors $ runT (fmap (addImplBound ist (map fst env)) tac)
702 where
704 where
703 runT (Intro []) = do g <- goal
705 runT (Intro []) = do g <- goal
704 attack; intro (bname g)
706 attack; intro (bname g)
src/Idris/IBC.hs+26−16
@@ -18,6 +18,8 @@ import Control.Monad.State hiding (get, put)
18import System.FilePath
18import System.FilePath
19import System.Directory
19import System.Directory
20
20
21+import Debug.Trace
22+
21import Paths_idris
23import Paths_idris
22
24
23ibcVersion :: Word8
25ibcVersion :: Word8
@@ -48,6 +50,7 @@ data IBCFile = IBCFile { ver :: Word8,
48 ibc_docstrings :: [(Name, String)],
50 ibc_docstrings :: [(Name, String)],
49 ibc_coercions :: [Name]
51 ibc_coercions :: [Name]
50 }
52 }
53+ deriving Show
51{-!
54{-!
52deriving instance Binary IBCFile
55deriving instance Binary IBCFile
53!-}
56!-}
@@ -327,16 +330,21 @@ instance Binary FC where
327
330
328instance Binary Name where
331instance Binary Name where
329 put x
332 put x
333+ = {-# SCC "putName" #-}
330− = case x of
334+ case x of
335+ UN x1 -> {-# SCC "putUN" #-}
331− UN x1 -> do putWord8 0
336+ do putWord8 0
332− put x1
337+ {-# SCC "putNString" #-} put x1
338+ NS x1 x2 -> {-# SCC "putNS" #-}
333− NS x1 x2 -> do putWord8 1
339+ do putWord8 1
334 put x1
340 put x1
335 put x2
341 put x2
342+ MN x1 x2 -> {-# SCC "putMN" #-}
336− MN x1 x2 -> do putWord8 2
343+ do putWord8 2
337 put x1
344 put x1
338 put x2
345 put x2
346+ NErased -> {-# SCC "putNErased" #-}
339− NErased -> putWord8 3
347+ putWord8 3
340 get
348 get
341 = do i <- getWord8
349 = do i <- getWord8
342 case i of
350 case i of
@@ -528,9 +536,10 @@ instance Binary NameType where
528 _ -> error "Corrupted binary data for NameType"
536 _ -> error "Corrupted binary data for NameType"
529
537
530
538
531−instance (Binary n) => Binary (TT n) where
539+instance {-(Binary n) =>-} Binary (TT Name) where
532 put x
540 put x
541+ = {-# SCC "putTT" #-}
533− = case x of
542+ case x of
534 P x1 x2 x3 -> do putWord8 0
543 P x1 x2 x3 -> do putWord8 0
535 put x1
544 put x1
536 put x2
545 put x2
@@ -613,7 +622,8 @@ instance Binary SC where
613
622
614instance Binary CaseAlt where
623instance Binary CaseAlt where
615 put x
624 put x
625+ = {-# SCC "putCaseAlt" #-}
616− = case x of
626+ case x of
617 ConCase x1 x2 x3 x4 -> do putWord8 0
627 ConCase x1 x2 x3 x4 -> do putWord8 0
618 put x1
628 put x1
619 put x2
629 put x2
@@ -642,17 +652,16 @@ instance Binary CaseAlt where
642
652
643instance Binary Def where
653instance Binary Def where
644 put x
654 put x
655+ = {-# SCC "putDef" #-}
645− = case x of
656+ case x of
646 Function x1 x2 -> do putWord8 0
657 Function x1 x2 -> do putWord8 0
647 put x1
658 put x1
648 put x2
659 put x2
649 TyDecl x1 x2 -> do putWord8 1
660 TyDecl x1 x2 -> do putWord8 1
650 put x1
661 put x1
651 put x2
662 put x2
663+ -- all primitives just get added at the start, don't write
652− Operator x1 x2 x3 -> do putWord8 2
664+ Operator x1 x2 x3 -> do return ()
653− put x1
654− put x2
655− put x3
656 CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->
665 CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->
657 do putWord8 3
666 do putWord8 3
658 put x1
667 put x1
@@ -750,8 +759,9 @@ instance Binary Totality where
750 _ -> error "Corrupted binary data for Totality"
759 _ -> error "Corrupted binary data for Totality"
751
760
752instance Binary IBCFile where
761instance Binary IBCFile where
753− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)
762+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)
763+ = {-# SCC "putIBCFile" #-}
754− = do put x1
764+ do put x1
755 put x2
765 put x2
756 put x3
766 put x3
757 put x4
767 put x4
src/Idris/Parser.hs+1−1
@@ -613,7 +613,6 @@ pNoExtExpr syn =
613 <|> pRewriteTerm syn
613 <|> pRewriteTerm syn
614 <|> pPi syn
614 <|> pPi syn
615 <|> pDoBlock syn
615 <|> pDoBlock syn
616− <|> pComprehension syn
617
616
618pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
617pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
619pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
618pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
@@ -763,6 +762,7 @@ pSimpleExpr syn =
763 fc <- pfc
762 fc <- pfc
764 return (PInferRef fc x))
763 return (PInferRef fc x))
765 <|> try (pList syn)
764 <|> try (pList syn)
765+ <|> try (pComprehension syn)
766 <|> try (pAlt syn)
766 <|> try (pAlt syn)
767 <|> try (pIdiom syn)
767 <|> try (pIdiom syn)
768 <|> try (do lchar '('
768 <|> try (do lchar '('
tutorial/idris-tutorial.tex+1
@@ -11,6 +11,7 @@
11\input{library.ltx}
11\input{library.ltx}
12
12
13\newcommand{\Idris}{\textsc{Idris}}
13\newcommand{\Idris}{\textsc{Idris}}
14+\newcommand{\version}{0.9.8}
14
15
15\title{Programming in \Idris{}: a tutorial}
16\title{Programming in \Idris{}: a tutorial}
16\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}
17\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}
tutorial/interp.tex+2−2
@@ -339,12 +339,12 @@ type to another if possible. Here, it converts a string to
339an integer, giving 0 if the input is invalid. An example run of this program
339an integer, giving 0 if the input is invalid. An example run of this program
340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
341
341
342−\begin{SaveVerbatim}{factrun}
342+\begin{SaveVerbatim}[commandchars=^\{\}]{factrun}
343
343
344$ idris interp.idr
344$ idris interp.idr
345 ____ __ _
345 ____ __ _
346 / _/___/ /____(_)____
346 / _/___/ /____(_)____
347− / // __ / ___/ / ___/ Version 0.9.7
347+ / // __ / ___/ / ___/ Version ^version{}
348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
349 /___/\__,_/_/ /_/____/ Type :? for help
349 /___/\__,_/_/ /_/____/ Type :? for help
350
350
tutorial/intro.tex+1−1
@@ -62,7 +62,7 @@ verifying systems software.
62\subsection{Example Code}
62\subsection{Example Code}
63
63
64This tutorial includes some example code, which has been tested with \Idris{} version
64This tutorial includes some example code, which has been tested with \Idris{} version
65−0.9.7. The files are available in the \Idris{} distribution,
65+\version{}. The files are available in the \Idris{} distribution,
66so that you can try them out easily,
66so that you can try them out easily,
67under \texttt{tutorial/examples}. However, it is strongly recommended that you
67under \texttt{tutorial/examples}. However, it is strongly recommended that you
68type them in yourself, rather than simply loading and reading them.
68type them in yourself, rather than simply loading and reading them.
tutorial/starting.tex+6−6
@@ -74,12 +74,12 @@ interactive environment.
74Entering \texttt{idris} at the shell prompt starts up the interactive
74Entering \texttt{idris} at the shell prompt starts up the interactive
75environment. You should see something like the following:
75environment. You should see something like the following:
76
76
77−\begin{SaveVerbatim}{prompt1}
77+\begin{SaveVerbatim}[commandchars=^\{\}]{prompt1}
78
78
79$ idris
79$ idris
80 ____ __ _
80 ____ __ _
81 / _/___/ /____(_)____
81 / _/___/ /____(_)____
82− / // __ / ___/ / ___/ Version 0.9.7
82+ / // __ / ___/ / ___/ Version ^version{}
83 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
83 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
84 /___/\__,_/_/ /_/____/ Type :? for help
84 /___/\__,_/_/ /_/____/ Type :? for help
85
85
@@ -98,8 +98,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
98\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
98\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
99the program is compiled to the executable \texttt{hello}.
99the program is compiled to the executable \texttt{hello}.
100
100
101−\begin{SaveVerbatim}{cmds}
101+\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}
102−Idris version 0.9.7
102+Idris version \version{}
103-------------------
103-------------------
104
104
105 Command Arguments Purpose
105 Command Arguments Purpose
@@ -129,12 +129,12 @@ Idris version 0.9.7
129\codefigs{cmds}{Interactive environment commands}
129\codefigs{cmds}{Interactive environment commands}
130
130
131
131
132−\begin{SaveVerbatim}{run1}
132+\begin{SaveVerbatim}[commandchars=^\{\}]{run1}
133
133
134$ idris hello.idr
134$ idris hello.idr
135 ____ __ _
135 ____ __ _
136 / _/___/ /____(_)____
136 / _/___/ /____(_)____
137− / // __ / ___/ / ___/ Version 0.9.7
137+ / // __ / ___/ / ___/ Version ^version{}
138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
139 /___/\__,_/_/ /_/____/ Type :? for help
139 /___/\__,_/_/ /_/____/ Type :? for help
140
140