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

CHANGELOG+4

compare with master

unifiedsplit

@@ -45,6 +45,10 @@ Minor language changes

45

46 using (xs : Vect n a)

47 bad : Elem x xs -> Elem x (y :: xs)

48+* `Sigma` has been renamed to `DPair`.

49+* Accessor functions for dependent pairs have been renamed to bring them into

50+ line with standard accessor functions for pairs. The function `getWitness`

51+ is now `fst`, and `getProof` is `snd`.

48

52

49New in 0.10:

53New in 0.10:

50============

54============

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

@@ -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+17−9

@@ -37,17 +37,25 @@ namespace Builtins

37 %used MkUPair a

38 %used MkUPair b

39

40− ||| Dependent pairs

40+ ||| Dependent pairs aid in the construction of dependent types by

41+ ||| providing evidence that some value resides in the type.

41 |||

42 |||

43+ ||| Formally, speaking, dependent pairs represent existential

42− ||| Dependent pairs represent existential quantification - they consist of a

44+ ||| quantification - they consist of a witness for the existential

43− ||| witness for the existential claim and a proof that the property holds for

45+ ||| claim and a proof that the property holds for it.

44− ||| it. Another way to see dependent pairs is as just data - for instance, the

45− ||| length of a vector paired with that vector.

46 |||

47− ||| @ a the type of the witness

47+ ||| @a the value to place in the type.

48− ||| @ P the type of the proof

48+ ||| @P the dependent type that requires the value.

49− data Sigma : (a : Type) -> (P : a -> Type) -> Type where

49+ data DPair : (a : Type) -> (P : a -> Type) -> Type where

50− MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P

50+ MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P

51+

52+ Sigma : (a : Type) -> (P : a -> Type) -> Type

53+ Sigma wit prf = DPair wit prf

54+ %deprecate Sigma "This name is being deprecated in favour of `DPair`."

55+

56+ MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DPair a P

57+ MkSigma wit prf = MkDPair wit prf

58+ %deprecate MkSigma "This constructor is being deprecated in favour of `MkDPair`."

51

59

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

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

53|||

61|||

libs/prelude/Prelude/Pairs.idr+14−6

@@ -14,7 +14,7 @@ using (a : Type, P : a -> Type)

14 data Exists : (P : a -> Type) -> Type where

15 Evidence : .(x : a) -> (pf : P x) -> Exists P

16

17− ||| Dependent pair where the second field is erased.

17+ ||| Dependent pair where the second field is erased.

18 data Subset : (a : Type) -> (P : a -> Type) -> Type where

19 Element : (x : a) -> .(pf : P x) -> Subset a P

20

@@ -34,12 +34,20 @@ using (a : Type, P : a -> Type)

34 getProof : (x : Subset a P) -> P (getWitness x)

35 getProof (Element x pf) = pf

36

37− namespace Sigma

37+ namespace DPair

38− getWitness : Sigma a P -> a

38+ fst : DPair a P -> a

39− getWitness (x ** pf) = x

39+ fst (x ** pf) = x

40

41− getProof : (x : Sigma a P) -> P (getWitness x)

41+ snd : (x : DPair a P) -> P (fst x)

42− getProof (x ** pf) = pf

42+ snd (x ** pf) = pf

43+

44+ getWitness : DPair a P -> a

45+ getWitness = fst

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

47+

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

49+ getProof = snd

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

43

51

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

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

45 -- 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 (DPair a p) where

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

src/Idris/AbsSyntaxTree.hs+4−4

@@ -1567,8 +1567,8 @@ falseTy = sUN "Void"

1567pairTy = sNS (sUN "Pair") ["Builtins"]

1568pairCon = sNS (sUN "MkPair") ["Builtins"]

1569

1570−upairTy = sNS (sUN "UPair") ["Builtins"]

1570+upairTy = sNS (sUN "UPair") ["Builtins"]

1571−upairCon = sNS (sUN "MkUPair") ["Builtins"]

1571+upairCon = sNS (sUN "MkUPair") ["Builtins"]

1572

1573eqTy = sUN "="

1574eqCon = sUN "Refl"

@@ -1615,8 +1615,8 @@ modDocName :: Name

1615modDocName = sMN 0 "ModuleDocs"

1616

1617-- Defined in builtins.idr

1618−sigmaTy = sNS (sUN "Sigma") ["Builtins"]

1618+sigmaTy = sNS (sUN "DPair") ["Builtins"]

1619−sigmaCon = sNS (sUN "MkSigma") ["Builtins"]

1619+sigmaCon = sNS (sUN "MkDPair") ["Builtins"]

1620

1621piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1622piBind = piBindp expl

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+ DPair Nat (\ m => Vect m (DPair 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 (DPair 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 (DPair 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 : DPair 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 `(MkDPair ~(Var tH) ~(Var tmH) : DPair 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 : DPair Ty (Tm [])

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

292

293− testElab2 : Sigma Ty (Tm [])

293+ testElab2 : DPair Ty (Tm [])

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

295

296 -- Doesn't work! :-)

297− testElab3 : Sigma Ty (Tm [])

297+ testElab3 : DPair 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+ DPair 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+ DPair 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: DPair A P} ->

4− {s2: Sigma A P} ->

4+ {s2: DPair 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−

test/unique001/unique001c.idr−4

@@ -44,7 +44,3 @@ data MPair : AnyType -> AnyType -> AnyType where

44

45ndup : {a : UniqueType} -> a -> UPair a a

46ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)

47−

48−

49−

50−