ed2bda5 · Idris-dev · git.iko.soy

libs/effects/Effect/Logging/Category.idr+1−1

compare with master

unifiedsplit

@@ -147,7 +147,7 @@ logN : (Show a, Eq a) => (l : Nat)

147 -> (cs : List a)

148 -> (m : String)

149 -> Eff () [LOG a]

150−logN l cs msg = call $ Log (getProof lvl) cs msg

150+logN l cs msg = call $ Log (snd lvl) cs msg

151 where

152 lvl : (n ** LogLevel n)

153 lvl = case cast {to=String} (cast {to=Int} l) of

libs/effects/Effect/Logging/Default.idr+1−1

@@ -84,7 +84,7 @@ log l msg = call $ Log l msg

84||| @l The level to log.

85||| @m The message to log.

86logN : (l : Nat) -> {auto prf : LTE l 70} -> (m : String) -> Eff () [LOG]

87−logN l msg = call $ Log (getProof lvl) msg

87+logN l msg = call $ Log (snd lvl) msg

88 where

89 lvl : (n ** LogLevel n)

90 lvl = case cast {to=String} (cast {to=Int} l) of

libs/prelude/Builtins.idr+2

@@ -47,9 +47,11 @@ namespace Builtins

47

48 Sigma : (a : Type) -> (P : a -> Type) -> Type

49 Sigma wit prf = DepPair wit prf

50+ %deprecate Sigma "This name is being deprecated in favour of `DepPair`."

50

51

51 MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DepPair a P

52 MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DepPair a P

52 MkSigma wit prf = MkDepPair wit prf

53 MkSigma wit prf = MkDepPair wit prf

54+ %deprecate MkSigma "This constructor is being deprecated in favour of `MkDepPair`."

53

55

54||| The empty type, also known as the trivially false proposition.

56||| The empty type, also known as the trivially false proposition.

55|||

57|||

libs/prelude/Prelude/Pairs.idr+3−1

@@ -43,9 +43,11 @@ using (a : Type, P : a -> Type)

43

44 getWitness : DepPair a P -> a

45 getWitness = fst

46+ %deprecate DepPair.getWitness "This is being deprecated in favour of `fst`."

46

47

47− getProof : (x : Sigma a P) -> P (fst x)

48+ getProof : (x : DepPair a P) -> P (fst x)

48 getProof = snd

49 getProof = snd

50+ %deprecate DepPair.getProof "This is being deprecated in favour of `snd`."

49

51

50 -- Polymorphic (class-based) projections have been removed

52 -- Polymorphic (class-based) projections have been removed

51 -- because type-directed name disambiguation works better.

53 -- because type-directed name disambiguation works better.

libs/prelude/Prelude/Show.idr+1−1

@@ -192,5 +192,5 @@ Show a => Show (Maybe a) where

192 showPrec d (Left x) = showCon d "Left" $ showArg x

193 showPrec d (Right x) = showCon d "Right" $ showArg x

194

195−(Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

195+(Show a, {y : a} -> Show (p y)) => Show (DepPair a p) where

196 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

test/disambig002/disambig002.idr+10−12

@@ -6,7 +6,7 @@ Dec0 : Type -> Type

6Dec0 = Dec

7

8Dec1 : {A : Type} -> (P : A -> Type) -> Type

9−Dec1 {A} P = (a : A) -> Dec0 (P a)

9+Dec1 {A} P = (a : A) -> Dec0 (P a)

10

11Unique : Type -> Type

12Unique t = (p : t) -> (q : t) -> p = q

@@ -53,8 +53,8 @@ namespace Finite

53filterTag : {A : Type} ->

54 {P : A -> Type} ->

55 Dec1 P ->

56− Vect n A ->

56+ Vect n A ->

57− Sigma Nat (\ m => Vect m (Sigma A P))

57+ DepPair Nat (\ m => Vect m (DepPair A P))

58filterTag d1P Nil = (_ ** Nil)

59filterTag d1P (a :: as) with (filterTag d1P as)

60 | (_ ** tail) with (d1P a)

@@ -66,7 +66,7 @@ toVect : {A : Type} ->

66 {P : A -> Type} ->

67 Finite A ->

68 Dec1 P ->

69− (n : Nat ** Vect n (Sigma A P))

69+ (n : Nat ** Vect n (DepPair A P))

70toVect fA d1P = filterTag d1P (toVect fA)

71

72sigmaUniqueLemma1 : {A : Type} ->

@@ -74,16 +74,14 @@ sigmaUniqueLemma1 : {A : Type} ->

74 Unique1 {t0 = A} P ->

75 (a : A) ->

76 (p : P a) ->

77− (ss : Vect n (Sigma A P)) ->

77+ (ss : Vect n (DepPair A P)) ->

78− Elem a (map getWitness ss) ->

78+ Elem a (map fst ss) ->

79 Elem (a ** p) ss

80

81toVectComplete : {A : Type} ->

82 {P : A -> Type} ->

83− (fA : Finite A) ->

83+ (fA : Finite A) ->

84− (d1P : Dec1 P) ->

84+ (d1P : Dec1 P) ->

85 Unique1 {t0 = A} P ->

86− (s : Sigma A P) ->

86+ (s : DepPair A P) ->

87− Elem s (getProof (toVect fA d1P))

87+ Elem s (snd (toVect fA d1P))

88−

89−

test/meta002/Tacs.idr+4−5

@@ -208,7 +208,7 @@ namespace STLC

208

209 -- Now we put this hole variable into our sigma constructor

210 -- prior to elaboration, so it doesn't disappear too soon

211− fill `(MkSigma ~(Var tH) ~(Var tmH) : Sigma Ty (Tm []))

211+ fill `(MkDepPair ~(Var tH) ~(Var tmH) : DepPair Ty (Tm []))

212 solve

213 focus tmH

214 mkTerm [] tm

@@ -287,18 +287,17 @@ namespace STLC

287 apply `(UnitCon {env=~(Var envH)})

288 []

289 solve

290− testElab : Sigma Ty (Tm [])

290+ testElab : DepPair Ty (Tm [])

291 testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))

292

293− testElab2 : Sigma Ty (Tm [])

293+ testElab2 : DepPair Ty (Tm [])

294 testElab2 = %runElab (elaborateSTLC (App (Lam "x" (Var 0)) UnitCon))

295

296 -- Doesn't work! :-)

297− testElab3 : Sigma Ty (Tm [])

297+ testElab3 : DepPair Ty (Tm [])

298 testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))

299 (Lam "x" (App (Var 0) (Var 0)))))

300 -- Error is:

301 -- Tacs.idr line 247 col 14:

302 -- When elaborating right hand side of testElab3:

303 -- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value

304−

test/meta002/expected+1−1

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

1Tacs.idr:298:15:

2When checking right hand side of testElab3 with expected type

3− Sigma Ty (Tm [])

3+ DepPair Ty (Tm [])

4

5Unifying ty and ARR ty t would lead to infinite value

6AgdaStyleReflection.idr:328:5:

test/proof002/Reflect.idr+2−4

@@ -44,7 +44,7 @@ using (xs : List a, ys : List a, G : List (List a))

44 let (yl ** (yr, yprf)) = expr_r ey in

45 appRExpr _ _ xr yr xprf yprf

46 where

47− appRExpr : (xs', ys' : List a) ->

47+ appRExpr : (xs', ys' : List a) ->

48 {G : List (List a)} -> {xs, ys : List a} ->

49 RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->

50 (ws' ** (RExpr G ws', xs' ++ ys' = ws'))

@@ -206,6 +206,4 @@ Reflect.bp1 = proof {

206-- prover.

207

208syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in

209− getJust (prove (getProof x)) ItIsJust

209+ getJust (prove (snd x)) ItIsJust

210−

211−

test/proof002/expected+1−1

@@ -12,7 +12,7 @@ When checking an application of function Reflect.getJust:

12 Type mismatch between

13 IsJust (Just x1) (Type of ItIsJust)

14 and

15− IsJust (prove (getProof x)) (Expected type)

15+ IsJust (prove (snd x)) (Expected type)

16

17 Specifically:

18 Type mismatch between

test/proof002/test030.idr−1

@@ -10,4 +10,3 @@ total

10testReflect1 : (xs, ys : List a) ->

11 ((xs ++ (x :: ys ++ xs)) = ((xs ++ [x]) ++ (ys ++ xs)))

12testReflect1 {a} xs ys = AssocProof a

13−

test/reg001/reg001.idr+13−14

@@ -37,7 +37,7 @@ filterTagP {n = S m} p (a :: as) q with (p a)

37 **

38 ((a ** believe_me Oh)

39 ::

40− (fst (getProof (filterTagP p as (believe_me Oh)))),

40+ (fst (snd (filterTagP p as (believe_me Oh)))),

41 Oh

42 )

43 )

@@ -95,7 +95,7 @@ mytranspose (x :: y :: xs)

95

96using (A : Type, B : A->Type, C : Type)

97 foo2 : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)

98− foo2 f p = f (getWitness p) (getProof p)

98+ foo2 f p = f (fst p) (snd p)

99

100

101m_add : Maybe (Either Bool Int) -> Maybe (Either Bool Int) ->

@@ -144,7 +144,7 @@ X : Nat -> Type

144X t = (c : Nat ** So (c < 5))

145

146column : X t -> Nat

147−column = getWitness

147+column = fst

148

149data Action = Left | Ahead | Right

150

@@ -161,31 +161,31 @@ isSubsetOf : Set univ => univ -> univ -> Type

161isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)

162

163interface Set univ => HasPower univ where

164− Powerset : (a : univ) ->

164+ Powerset : (a : univ) ->

165− Sigma univ (\Pa => (c : univ) ->

165+ DepPair univ (\Pa => (c : univ) ->

166 (isSubsetOf c a) -> member c Pa)

167

168powerset : HasPower univ => univ -> univ

169−powerset {univ} a = getWitness (Powerset a)

169+powerset {univ} a = fst (Powerset a)

170

171mapFilter : (alpha -> beta) ->

172− (alpha -> Bool) ->

172+ (alpha -> Bool) ->

173− Vect n alpha ->

173+ Vect n alpha ->

174 (n : Nat ** Vect n beta)

175mapFilter f p Nil = (_ ** Nil)

176mapFilter f p (a :: as) with (p a)

177− | True = (_ ** (f a) :: (getProof (mapFilter f p as)))

177+ | True = (_ ** (f a) :: (snd (mapFilter f p as)))

178 | False = mapFilter f p as

179

180hVectEx1 : HVect [String, List Nat, Nat, (Nat, Nat)]

181hVectEx1 = ["Hello",[1,2,3],42,(0,10)]

182−

182+

183vecfoo : HVect [String, List Nat, Nat, (Nat, Nat)]

184vecfoo = put (S (S Z)) hVectEx1

185

186foom : Monad m => Int -> m Int

187−foom = pure

187+foom = pure

188−

188+

189bar : IO ()

190bar = case foom 5 of

191 Nothing => print 42

@@ -193,7 +193,7 @@ bar = case foom 5 of

193

194Max : (Nat -> Type) -> Type

195Max p = (Nat , (k : Nat) -> p k -> Nat)

196−

196+

197maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat

198maxEquiv a n1 pr1 = snd a n1 pr1

199

@@ -207,4 +207,3 @@ data Kappa : (r : Rho) -> Type where K : Kappa r

207kappa : Kappa (rho r) -> Kappa (rho r)

208kappa {r} k = k' where -- k' : Kappa (rho r)

209 k' = k

210−

test/reg064/reg064.idr+6−7

@@ -1,9 +1,8 @@

1−sigmaEq2 : {A : Type} ->

1+sigmaEq2 : {A : Type} ->

2− {P : A -> Type} ->

2+ {P : A -> Type} ->

3− {s1: Sigma A P} ->

3+ {s1: DepPair A P} ->

4− {s2: Sigma A P} ->

4+ {s2: DepPair A P} ->

5− getWitness s1 = getWitness s2 ->

5+ fst s1 = fst s2 ->

6− getProof s1 = getProof s2 ->

6+ snd s1 = snd s2 ->

7 s1 = s2

8sigmaEq2 {A} {P} {s1 = (x ** prf)} {s2 = (x ** prf)} Refl Refl = Refl

9−