git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master' into providers
commit40208c464b3e504f7f44f0d9b6aadfe88cdd2178 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 22 Apr 2013, 22:20 (14 years ago) parent173e3572a17e4f
21 files changed+504−65
compare with master
unifiedsplit
CHANGELOG+1 lib/Data/SortedMap.idr+235 lib/Data/SortedSet.idr+25 lib/Decidable/Decidable.idr+14 lib/Decidable/Equality.idr+1−1 lib/Decidable/Order.idr+79 lib/Prelude.idr+2−2 lib/base.ipkg+2−1 src/Core/Elaborate.hs+13 src/Core/ProofState.hs+1−1 src/Idris/AbsSyntax.hs+2 src/Idris/AbsSyntaxTree.hs+35−1 src/Idris/Delaborate.hs+1 src/Idris/ElabDecls.hs+52−31 src/Idris/ElabTerm.hs+4−2 src/Idris/IBC.hs+26−16 src/Idris/Parser.hs+1−1 tutorial/idris-tutorial.tex+1 tutorial/interp.tex+2−2 tutorial/intro.tex+1−1 tutorial/starting.tex+6−6
CHANGELOG+1
@@ -14,6 +14,7 @@ User visible changes:
1414
1515Internal changes:
1616
17+* Fix non-linear pattern checking
1718* Improved name disambiguation
1819* More flexible unification and elaboration of lambdas
1920* 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 -> _
7575leftNotRight refl impossible
7676
7777instance (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')
7979 | Yes p = Yes $ cong p
8080 | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
8181 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
189189
190190---- Ranges
191191
192−%assert_total
192+partial abstract
193193count : (Ord a, Num a) => a -> a -> a -> List a
194194count a inc b = if a <= b then a :: count (a + inc) inc b
195195 else []
196196
197−partial
197+partial abstract
198198countFrom : (Ord a, Num a) => a -> a -> List a
199199countFrom a inc = a :: lazy (countFrom (a + inc) inc)
200200
lib/base.ipkg+2−1
@@ -13,7 +13,7 @@ modules = Builtins, Prelude, IO, System,
1313
1414 System.Concurrency.Raw, System.Concurrency.Process,
1515
16− Decidable.Equality,
16+ Decidable.Equality, Decidable.Decidable, Decidable.Order,
1717
1818 Uninhabited,
1919
@@ -22,6 +22,7 @@ modules = Builtins, Prelude, IO, System,
2222 Language.Reflection,
2323
2424 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,
25+ Data.SortedMap, Data.SortedSet,
2526
2627 Control.Monad.Identity, Control.Monad.State, Control.Category,
2728 Control.Arrow,
src/Core/Elaborate.hs+13
@@ -525,6 +525,19 @@ arg n tyhole = do ty <- unique_hole tyhole
525525 claim ty RType
526526 forall n (Var ty)
527527
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+
528541-- Try a tactic, if it fails, try another
529542try :: Elab' aux a -> Elab' aux a -> Elab' aux a
530543try t1 t2 = try' t1 t2 False
src/Core/ProofState.hs+1−1
@@ -162,7 +162,7 @@ unify' ctxt env topx topy =
162162-- -- " in " ++ show env ++
163163-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
164164-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"
165−-- -- ++ show (pterm ps)
165+-- ++ show (pterm ps)
166166-- ++ "\n----------") $
167167 case fails of
168168-- [] -> return u
src/Idris/AbsSyntax.hs+2
@@ -1074,6 +1074,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
10741074-- match (PRef _ n) (PRef _ n') | n == n' = return []
10751075-- | otherwise = Nothing
10761076 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)
10771079 match (PApp _ x []) (PRef f n) = match x (PRef f n)
10781080 match (PRef _ n) tm@(PRef _ n')
10791081 | n == n' && not names &&
src/Idris/AbsSyntaxTree.hs+35−1
@@ -979,7 +979,7 @@ prettyImp impl = prettySe 10
979979showImp :: Bool -> PTerm -> String
980980showImp impl tm = se 10 tm where
981981 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
983983 se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
984984 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
985985 else showbasic n
@@ -1014,6 +1014,9 @@ showImp impl tm = se 10 tm where
10141014 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
10151015 se p (PPi (TacImp _ _ s _) n ty sc)
10161016 = 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
10171020 se p (PApp _ (PRef _ f) [])
10181021 | not impl = show f
10191022 se p (PApp _ (PRef _ op@(UN (f:_))) args)
@@ -1052,6 +1055,37 @@ showImp impl tm = se 10 tm where
10521055 se p (PCoerced t) = se p t
10531056-- se p x = "Not implemented"
10541057
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+
10551089 sArg (PImp _ _ n tm _) = siArg (n, tm)
10561090 sArg (PExp _ _ tm _) = seArg tm
10571091 sArg (PConstraint _ _ tm _) = scArg tm
src/Idris/Delaborate.hs+1
@@ -21,6 +21,7 @@ delabTy i n
2121 = case lookupTy n (tt_ctxt i) of
2222 (ty:_) -> case lookupCtxt n (idris_implicits i) of
2323 (imps:_) -> delabTy' i imps ty False
24+ _ -> delabTy' i [] ty False
2425
2526delab' :: IState -> Term -> Bool -> PTerm
2627delab' 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)
147147 ttag <- getName
148148 i <- getIState
149149 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)
151151 logLvl 2 $ "Parameters : " ++ show params
152152 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
153153 (idris_datatypes i) })
@@ -161,32 +161,53 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
161161 where
162162 -- parameters are names which are unchanged across the structure,
163163 -- which appear exactly once in the return type of a constructor
164− findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]
165− findParams ps [] = mapMaybe (\ ((x, y), n) ->
166− if y then Just n else Nothing)
167− (zip ps [0..])
168− findParams ps (t : ts) = findParams (updateParams ps t) ts
169−
170− updateParams ps (Bind n (Pi t) sc)
171− = updateParams (updateParams ps (instantiate (P Bound n t) sc)) t
172− updateParams ps tm@(App f a)
173− | (P _ fn _, args) <- unApply tm
174− = if fn == n
175− then updateParamsA ps args (tail args)
176− else updateParams (updateParams ps f) a
177− | otherwise = updateParams (updateParams ps f) a
178− updateParams ps _ = ps
179−
180− updateParamsA ((mn, _) : ns) (p@(P _ n' _) : args) all
181− | n' `elem` concatMap freeNames all
182− = (mn, False) : updateParamsA ns args (p : all)
183− updateParamsA ((Nothing, b) : ns) (p@(P _ n' _) : args) all
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
164+
165+ -- First, find all applications of the constructor, then check over
166+ -- them for repeated arguments
167+
168+ findParams :: [Type] -> [Int]
169+ findParams ts = let allapps = concatMap getDataApp ts in
170+ paramPos allapps
171+
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 _ _)
193+ | (P _ d _, args) <- unApply f
194+ = if (d == n) then [mParam args args] else []
195+ getDataApp (Bind n (Pi t) sc)
196+ = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
197+ getDataApp _ = []
198+
199+ -- keep the arguments which are single names, which don't appear
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)
208+ | n `elem` freeNames t = 1 + count n ts
209+ | otherwise = count n ts
210+ mParam args (_ : rest) = Nothing : mParam args rest
190211
191212-- | Elaborate a type provider
192213elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
@@ -712,7 +733,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
712733 -- Build the LHS as an "Infer", and pull out its type and
713734 -- pattern bindings
714735 i <- getIState
715− let lhs = addImpl i lhs_in
736+ let lhs = addImplPat i lhs_in
716737 logLvl 5 ("LHS: " ++ showImp True lhs)
717738 ((lhs', dlhs, []), _) <-
718739 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
@@ -810,18 +831,18 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
810831
811832 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
812833 = do i <- getIState
813− let tm = addImpl i tm_in
834+ let tm = addImplPat i tm_in
814835 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
815836 showImp True toplhs)
816837 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"
818839 Right mvars ->
819840 do logLvl 3 ("Match vars : " ++ show mvars)
820841 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
821842 return $ PClause fc wname lhs ws rhs wheres
822843 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
823844 = do i <- getIState
824− let tm = addImpl i tm_in
845+ let tm = addImplPat i tm_in
825846 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
826847 showImp True toplhs)
827848 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)
695695collectDeferred t = return t
696696
697697-- Running tactics directly
698+-- if a tactic adds unification problems, return an error
698699
699700runTac :: Bool -> IState -> PTactic -> ElabD ()
700−runTac autoSolve ist tac = do env <- get_env
701− runT (fmap (addImplBound ist (map fst env)) tac)
701+runTac autoSolve ist tac
702+ = do env <- get_env
703+ no_errors $ runT (fmap (addImplBound ist (map fst env)) tac)
702704 where
703705 runT (Intro []) = do g <- goal
704706 attack; intro (bname g)
src/Idris/IBC.hs+26−16
@@ -18,6 +18,8 @@ import Control.Monad.State hiding (get, put)
1818import System.FilePath
1919import System.Directory
2020
21+import Debug.Trace
22+
2123import Paths_idris
2224
2325ibcVersion :: Word8
@@ -48,6 +50,7 @@ data IBCFile = IBCFile { ver :: Word8,
4850 ibc_docstrings :: [(Name, String)],
4951 ibc_coercions :: [Name]
5052 }
53+ deriving Show
5154{-!
5255deriving instance Binary IBCFile
5356!-}
@@ -327,16 +330,21 @@ instance Binary FC where
327330
328331instance Binary Name where
329332 put x
330− = case x of
331− UN x1 -> do putWord8 0
332− put x1
333− NS x1 x2 -> do putWord8 1
333+ = {-# SCC "putName" #-}
334+ case x of
335+ UN x1 -> {-# SCC "putUN" #-}
336+ do putWord8 0
337+ {-# SCC "putNString" #-} put x1
338+ NS x1 x2 -> {-# SCC "putNS" #-}
339+ do putWord8 1
334340 put x1
335341 put x2
336− MN x1 x2 -> do putWord8 2
342+ MN x1 x2 -> {-# SCC "putMN" #-}
343+ do putWord8 2
337344 put x1
338345 put x2
339− NErased -> putWord8 3
346+ NErased -> {-# SCC "putNErased" #-}
347+ putWord8 3
340348 get
341349 = do i <- getWord8
342350 case i of
@@ -528,9 +536,10 @@ instance Binary NameType where
528536 _ -> error "Corrupted binary data for NameType"
529537
530538
531−instance (Binary n) => Binary (TT n) where
539+instance {-(Binary n) =>-} Binary (TT Name) where
532540 put x
533− = case x of
541+ = {-# SCC "putTT" #-}
542+ case x of
534543 P x1 x2 x3 -> do putWord8 0
535544 put x1
536545 put x2
@@ -613,7 +622,8 @@ instance Binary SC where
613622
614623instance Binary CaseAlt where
615624 put x
616− = case x of
625+ = {-# SCC "putCaseAlt" #-}
626+ case x of
617627 ConCase x1 x2 x3 x4 -> do putWord8 0
618628 put x1
619629 put x2
@@ -642,17 +652,16 @@ instance Binary CaseAlt where
642652
643653instance Binary Def where
644654 put x
645− = case x of
655+ = {-# SCC "putDef" #-}
656+ case x of
646657 Function x1 x2 -> do putWord8 0
647658 put x1
648659 put x2
649660 TyDecl x1 x2 -> do putWord8 1
650661 put x1
651662 put x2
652− Operator x1 x2 x3 -> do putWord8 2
653− put x1
654− put x2
655− put x3
663+ -- all primitives just get added at the start, don't write
664+ Operator x1 x2 x3 -> do return ()
656665 CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->
657666 do putWord8 3
658667 put x1
@@ -750,8 +759,9 @@ instance Binary Totality where
750759 _ -> error "Corrupted binary data for Totality"
751760
752761instance 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)
754− = do put x1
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" #-}
764+ do put x1
755765 put x2
756766 put x3
757767 put x4
src/Idris/Parser.hs+1−1
@@ -613,7 +613,6 @@ pNoExtExpr syn =
613613 <|> pRewriteTerm syn
614614 <|> pPi syn
615615 <|> pDoBlock syn
616− <|> pComprehension syn
617616
618617pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
619618pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
@@ -763,6 +762,7 @@ pSimpleExpr syn =
763762 fc <- pfc
764763 return (PInferRef fc x))
765764 <|> try (pList syn)
765+ <|> try (pComprehension syn)
766766 <|> try (pAlt syn)
767767 <|> try (pIdiom syn)
768768 <|> try (do lchar '('
tutorial/idris-tutorial.tex+1
@@ -11,6 +11,7 @@
1111\input{library.ltx}
1212
1313\newcommand{\Idris}{\textsc{Idris}}
14+\newcommand{\version}{0.9.8}
1415
1516\title{Programming in \Idris{}: a tutorial}
1617\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
339339an integer, giving 0 if the input is invalid. An example run of this program
340340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
341341
342−\begin{SaveVerbatim}{factrun}
342+\begin{SaveVerbatim}[commandchars=^\{\}]{factrun}
343343
344344$ idris interp.idr
345345 ____ __ _
346346 / _/___/ /____(_)____
347− / // __ / ___/ / ___/ Version 0.9.7
347+ / // __ / ___/ / ___/ Version ^version{}
348348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
349349 /___/\__,_/_/ /_/____/ Type :? for help
350350
tutorial/intro.tex+1−1
@@ -62,7 +62,7 @@ verifying systems software.
6262\subsection{Example Code}
6363
6464This 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,
6666so that you can try them out easily,
6767under \texttt{tutorial/examples}. However, it is strongly recommended that you
6868type them in yourself, rather than simply loading and reading them.
tutorial/starting.tex+6−6
@@ -74,12 +74,12 @@ interactive environment.
7474Entering \texttt{idris} at the shell prompt starts up the interactive
7575environment. You should see something like the following:
7676
77−\begin{SaveVerbatim}{prompt1}
77+\begin{SaveVerbatim}[commandchars=^\{\}]{prompt1}
7878
7979$ idris
8080 ____ __ _
8181 / _/___/ /____(_)____
82− / // __ / ___/ / ___/ Version 0.9.7
82+ / // __ / ___/ / ___/ Version ^version{}
8383 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
8484 /___/\__,_/_/ /_/____/ Type :? for help
8585
@@ -98,8 +98,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
9898\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
9999the program is compiled to the executable \texttt{hello}.
100100
101−\begin{SaveVerbatim}{cmds}
102−Idris version 0.9.7
101+\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}
102+Idris version \version{}
103103-------------------
104104
105105 Command Arguments Purpose
@@ -129,12 +129,12 @@ Idris version 0.9.7
129129\codefigs{cmds}{Interactive environment commands}
130130
131131
132−\begin{SaveVerbatim}{run1}
132+\begin{SaveVerbatim}[commandchars=^\{\}]{run1}
133133
134134$ idris hello.idr
135135 ____ __ _
136136 / _/___/ /____(_)____
137− / // __ / ___/ / ___/ Version 0.9.7
137+ / // __ / ___/ / ___/ Version ^version{}
138138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
139139 /___/\__,_/_/ /_/____/ Type :? for help
140140