git.iko.soy/Idris-dev
on master help sign in
Change DecEq primitives to use believe_me

This at least ensures they won't reduce and mess up type checking elsewhere. Postulates would be better, but the current erasure analysis can't necessarily identify that they aren't reachable in a higher order setting. Re-fixes #4090

commita08a1e6dd3e8e7cfb50cc7d1420d7483a8eef851 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 29 May 2018, 10:45 (8 years ago) parentfe79d87
3 files changed+86−9
compare with master
unifiedsplit
libs/prelude/Decidable/Equality.idr+16−8 test/regression001/reg007.idr+69 test/regression001/run+1−1
libs/prelude/Decidable/Equality.idr+16−8
@@ -157,8 +157,10 @@ implementation DecEq a => DecEq (List a) where
157157
158158
159159-- For the primitives, we have to cheat because we don't have access to their
160−-- internal implementations. We postulate the inequality proofs because we're
161−-- never going to have to compute anything from them.
160+-- internal implementations. We use believe_me for the inequality proofs
161+-- because we don't them to reduce (and they should never be needed anyway...)
162+-- A postulate would be better, but erasure analysis may think they're needed
163+-- for computation in a higher order setting.
162164
163165--------------------------------------------------------------------------------
164166-- Int
@@ -170,7 +172,8 @@ implementation DecEq Int where
170172 False => No primitiveNotEq
171173 where primitiveEq : x = y
172174 primitiveEq = really_believe_me (Refl {x})
173− postulate primitiveNotEq : x = y -> Void
175+ primitiveNotEq : x = y -> Void
176+ primitiveNotEq prf = believe_me {b = Void} ()
174177
175178--------------------------------------------------------------------------------
176179-- Char
@@ -182,7 +185,8 @@ implementation DecEq Char where
182185 False => No primitiveNotEq
183186 where primitiveEq : x = y
184187 primitiveEq = really_believe_me (Refl {x})
185− postulate primitiveNotEq : x = y -> Void
188+ primitiveNotEq : x = y -> Void
189+ primitiveNotEq prf = believe_me {b = Void} ()
186190
187191--------------------------------------------------------------------------------
188192-- Integer
@@ -194,7 +198,8 @@ implementation DecEq Integer where
194198 False => No primitiveNotEq
195199 where primitiveEq : x = y
196200 primitiveEq = really_believe_me (Refl {x})
197− postulate primitiveNotEq : x = y -> Void
201+ primitiveNotEq : x = y -> Void
202+ primitiveNotEq prf = believe_me {b = Void} ()
198203
199204--------------------------------------------------------------------------------
200205-- String
@@ -206,7 +211,8 @@ implementation DecEq String where
206211 False => No primitiveNotEq
207212 where primitiveEq : x = y
208213 primitiveEq = really_believe_me (Refl {x})
209− postulate primitiveNotEq : x = y -> Void
214+ primitiveNotEq : x = y -> Void
215+ primitiveNotEq prf = believe_me {b = Void} ()
210216
211217--------------------------------------------------------------------------------
212218-- Ptr
@@ -218,7 +224,8 @@ implementation DecEq Ptr where
218224 False => No primitiveNotEq
219225 where primitiveEq : x = y
220226 primitiveEq = really_believe_me (Refl {x})
221− postulate primitiveNotEq : x = y -> Void
227+ primitiveNotEq : x = y -> Void
228+ primitiveNotEq prf = believe_me {b = Void} ()
222229
223230--------------------------------------------------------------------------------
224231-- ManagedPtr
@@ -230,4 +237,5 @@ implementation DecEq ManagedPtr where
230237 False => No primitiveNotEq
231238 where primitiveEq : x = y
232239 primitiveEq = really_believe_me (Refl {x})
233− postulate primitiveNotEq : x = y -> Void
240+ primitiveNotEq : x = y -> Void
241+ primitiveNotEq prf = believe_me {b = Void} ()
test/regression001/reg007.idrnew file+69
@@ -0,0 +1,69 @@
1+{-
2+See: http://lpaste.net/104020
3+ and https://github.com/gonzaw/extensible-records
4+-}
5+module Record
6+
7+import Data.List
8+
9+%default total
10+
11+data HList : List Type -> Type where
12+ Nil : HList []
13+ (::) : a -> HList xs -> HList (a :: xs)
14+
15+infix 5 :=
16+
17+data Field : lbl -> Type -> Type where
18+ (:=) : (label : lbl) ->
19+ (value : b) -> Field label b
20+
21+labelsOf : List (lbl, Type) -> List lbl
22+labelsOf [] = []
23+labelsOf ((label, _) :: xs) = label :: labelsOf xs
24+
25+toFields : List (lbl, Type) -> List Type
26+toFields [] = []
27+toFields ((l, t) :: xs) = (Field l t) :: toFields xs
28+
29+data IsSet : List t -> Type where
30+ IsSetNil : IsSet []
31+ IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs)
32+
33+data Record : List (lty, Type) -> Type where
34+ MkRecord : IsSet (labelsOf ts) -> HList (toFields ts) ->
35+ Record ts
36+
37+infixr 6 +:
38+
39+rnil : Record []
40+rnil = MkRecord IsSetNil []
41+
42+prepend : { label : lbl,
43+ xs : List (lbl, Type),
44+ prf : Not (Elem label (labelsOf xs))
45+ } ->
46+ Field label t ->
47+ Record xs ->
48+ Record ((label, t) :: xs)
49+prepend {prf} f (MkRecord isSet fs) = MkRecord (IsSetCons prf isSet) (f :: fs)
50+
51+data IsNo : Dec prop -> Type where
52+ ItIsNo : IsNo (No yprf)
53+
54+(+:) : DecEq lbl =>
55+ { label : lbl, xs : List (lbl, Type) } ->
56+ Field label t ->
57+ Record xs ->
58+ { auto isno : IsNo (isElem label $ labelsOf xs) } ->
59+ Record ((label, t) :: xs)
60+
61+(+:) {label} {xs} f r with (isElem label $ labelsOf xs)
62+ (+:) { isno = ItIsNo } _ _ | (Yes _) impossible
63+ (+:) f r | (No no) = prepend {prf = no} f r
64+
65+foo : Record [("Year", Integer)]
66+
67+bar : Record [("Title", String), ("Year", Integer)]
68+bar = (+:) ("Title" := "test") foo
69+
test/regression001/run+1−1
@@ -1,7 +1,7 @@
11#!/usr/bin/env bash
22${IDRIS:-idris} $@ --check \
33 reg001.idr reg002.idr reg003.idr reg004.lidr reg005.idr \
4− reg006.idr reg036.idr reg037.idr reg038.idr reg046.idr \
4+ reg006.idr reg007.idr reg036.idr reg037.idr reg038.idr reg046.idr \
55 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \
66 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \
77 reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \