[ new ] Factoring out unsafe parts of the library (#414)

.travis.yml

@@ -63,15 +63,20 @@ install:
   # generating Everything.agda
   - cabal install lib.cabal
   - runghc GenerateEverything.hs
+  # setting up travis-specific scripts and files
+  - cp travis/* .
 
 script:
   # generating index.agda
   - ./index.sh
   # detecting whitespace violations
   - make check-whitespace
+  # checking safe modules build with --safe
+  # - agda -i . -i src/ --safe safe.agda
   # detecting basic compilation errors
-  - agda -i . -i src -c --no-main Everything.agda
+  - agda -i . -i src/ -c --no-main Everything.agda
   # building the docs
+  - agda -i . -i src/ --html safe.agda
   - agda -i . -i src/ --html index.agda
   # moving everything at the root
   - mv html/* .

CHANGELOG.md

@@ -8,6 +8,47 @@ Important changes since 0.16:
 Non-backwards compatible changes
 --------------------------------
 
+#### Overhaul of safety of the library
+
+* Currently the library is very difficult to type check with the `--safe`
+  flag as there are unsafe functions scattered throughout the key modules.
+  This means that it is almost impossible to verify the safety of any code
+  depending on the standard library. The following reorganisation will fix
+  this problem after the NEXT full release of Agda. (Agda 2.5.4.1 uses
+  postulates in the `Agda.Builtin.X` that will be removed in the next release).
+
+* The following new modules `Unsafe` have been created. The contents of
+  these are  nearly all marked as unsafe as they use the `trustMe` functionality,
+  either for performance reasons or for informative decidable equality tests.
+  ```
+  Data.Char.Unsafe
+  Data.Float.Unsafe
+  Data.Nat.Unsafe
+  Data.Nat.DivMod.Unsafe
+  Data.String.Unsafe
+  Data.Word.Unsafe
+  ```
+
+* Another module affected is `Relation.Binary.HeterogeneousEquality.Quotients(.Examples)`
+  which previously postulated function extensionality. The relevant submodules
+  now take extensionality as a module parameter instead of postulating it. If you
+  want to use these results then you should postulate it yourself.
+
+* The full list of unsafe modules is:
+  ```
+  Data.Char.Unsafe
+  Data.Float.Unsafe
+  Data.Nat.Unsafe
+  Data.Nat.DivMod.Unsafe
+  Data.String.Unsafe
+  Data.Word.Unsafe
+  IO
+  IO.Primitives
+  Reflection
+  Relation.Binary.PropositionalEquality.TrustMe
+  ```
+
+
 #### New codata library
 
 * A new `Codata` library using copatterns and sized types rather

README.md

@@ -59,3 +59,21 @@ If you're using a development version of Agda rather than the latest official re
 you should use the `experimental` branch of the standard library rather than `master`.
 The `experimental` branch contains non-backwards compatible patches for upcoming
 changes to the language.
+
+## Type-checking with the `--safe` flag
+
+After the next full release of Agda, most of the library will be able to
+be type-checked with the `--safe` flag. Only the following modules are
+not compatible:
+```
+  Data.Char.Unsafe
+  Data.Float.Unsafe
+  Data.Nat.Unsafe
+  Data.Nat.DivMod.Unsafe
+  Data.String.Unsafe
+  Data.Word.Unsafe
+  IO
+  IO.Primitives
+  Reflection
+  Relation.Binary.PropositionalEquality.TrustMe
+```

README/Function/Reasoning.agda

@@ -33,10 +33,11 @@ module _ {A B C : Set} {A→B : A → B} {B→C : B → C} where
 open import Data.Nat
 open import Data.List.Base
 open import Data.Char.Base
-open import Data.String using (String ; toList ; fromList ; _==_)
+open import Data.String using (String; toList; fromList)
+open import Data.String.Unsafe using (_==_)
 open import Function
 open import Data.Bool
-open import Data.Product as P using (_×_ ; <_,_> ; uncurry ; proj₁)
+open import Data.Product as P using (_×_; <_,_>; uncurry; proj₁)
 open import Agda.Builtin.Equality
 
 -- This can give us for instance this decomposition of a function

README/Record.agda

@@ -11,6 +11,7 @@ module README.Record where
 
 open import Data.Product
 open import Data.String
+open import Data.String.Unsafe
 open import Function using (flip)
 open import Level
 import Record

src/Data/Char.agda

@@ -6,60 +6,23 @@
 
 module Data.Char where
 
-open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (<-strictTotalOrder)
-open import Data.Bool.Base using (Bool; true; false)
-open import Relation.Nullary
-open import Relation.Nullary.Decidable
-open import Relation.Binary
+open import Relation.Binary using (Setoid; StrictTotalOrder)
 import Relation.Binary.On as On
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
-open import Relation.Binary.PropositionalEquality.TrustMe
+import Relation.Binary.PropositionalEquality as PropEq
 
-open import Agda.Builtin.Char using (primCharEquality)
-open import Data.String.Base using (String)
-open import Data.Char.Base
-open        Data.Char.Base public using (Char; show; toNat; fromNat)
-
--- Informative equality test.
-
-infix 4 _≟_
-
-_≟_ : Decidable {A = Char} _≡_
-s₁ ≟ s₂ with primCharEquality s₁ s₂
-... | true  = yes trustMe
-... | false = no whatever
-  where postulate whatever : _
-
--- Boolean equality test.
---
--- Why is the definition _==_ = primCharEquality not used? One reason
--- is that the present definition can sometimes improve type
--- inference, at least with the version of Agda that is current at the
--- time of writing: see unit-test below.
-
-infix 4 _==_
-
-_==_ : Char → Char → Bool
-c₁ == c₂ = ⌊ c₁ ≟ c₂ ⌋
-
-private
-
-  -- The following unit test does not type-check (at the time of
-  -- writing) if _==_ is replaced by primCharEquality.
+------------------------------------------------------------------------
+-- Re-export base definitions publically
 
-  data P : (Char → Bool) → Set where
-    p : (c : Char) → P (_==_ c)
+open import Data.Char.Base public
 
-  unit-test : P (_==_ 'x')
-  unit-test = p _
+------------------------------------------------------------------------
+-- Equality over characters
 
 setoid : Setoid _ _
 setoid = PropEq.setoid Char
 
-decSetoid : DecSetoid _ _
-decSetoid = PropEq.decSetoid _≟_
-
+------------------------------------------------------------------------
 -- An ordering induced by the toNat function.
 
 strictTotalOrder : StrictTotalOrder _ _ _

src/Data/Char/Base.agda

@@ -5,6 +5,7 @@
 ------------------------------------------------------------------------
 module Data.Char.Base where
 
+open import Agda.Builtin.String using (primShowChar)
 open import Data.Nat.Base    using (ℕ)
 open import Data.Bool.Base   using (Bool)
 open import Data.String.Base using (String)
@@ -19,7 +20,6 @@ open AgdaChar using (Char) public
 -- Primitive operations
 
 open AgdaChar
-open import Agda.Builtin.String using (primShowChar)
 
 show : Char → String
 show = primShowChar

src/Data/Char/Unsafe.agda

@@ -0,0 +1,58 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe Char operations and proofs
+------------------------------------------------------------------------
+
+module Data.Char.Unsafe where
+
+open import Data.Bool.Base using (Bool; true; false)
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (⌊_⌋)
+open import Relation.Binary using (Decidable; DecSetoid)
+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
+open import Relation.Binary.PropositionalEquality.TrustMe
+
+open import Agda.Builtin.Char using (primCharEquality)
+open import Data.Char
+
+------------------------------------------------------------------------
+-- An informative equality test.
+
+infix 4 _≟_
+
+_≟_ : Decidable {A = Char} _≡_
+s₁ ≟ s₂ with primCharEquality s₁ s₂
+... | true  = yes trustMe
+... | false = no whatever
+  where postulate whatever : _
+
+------------------------------------------------------------------------
+-- Boolean equality test.
+--
+-- Why is the definition _==_ = primCharEquality not used? One reason
+-- is that the present definition can sometimes improve type
+-- inference, at least with the version of Agda that is current at the
+-- time of writing: see unit-test below.
+
+infix 4 _==_
+
+_==_ : Char → Char → Bool
+c₁ == c₂ = ⌊ c₁ ≟ c₂ ⌋
+
+private
+
+  -- The following unit test does not type-check (at the time of
+  -- writing) if _==_ is replaced by primCharEquality.
+
+  data P : (Char → Bool) → Set where
+    p : (c : Char) → P (c ==_)
+
+  unit-test : P ('x' ==_)
+  unit-test = p _
+
+------------------------------------------------------------------------
+-- Decidable equality
+
+decSetoid : DecSetoid _ _
+decSetoid = PropEq.decSetoid _≟_

src/Data/Digit.agda

@@ -112,4 +112,3 @@ toDigits (suc (suc k)) n = <′-rec Pred helper n
   helper .(toℕ r + 0     * base) rec | result zero    r refl = ([ r ] , refl)
   helper .(toℕ r + suc x * base) rec | result (suc x) r refl =
     cons r (rec (suc x) (lem (pred (suc x)) k (toℕ r)))
-

src/Data/Float.agda

@@ -6,23 +6,20 @@
 
 module Data.Float where
 
-open import Data.Bool.Base using (Bool; false; true)
-open import Relation.Nullary.Decidable
-open import Relation.Nullary
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
-open import Relation.Binary.PropositionalEquality.TrustMe
 open import Data.String.Base using (String)
 
+------------------------------------------------------------------------
+-- Re-export built-ins publically
+
 open import Agda.Builtin.Float public
-  using ( Float; primFloatEquality; primShowFloat )
+  using
+  ( Float
+  ; primFloatEquality
+  ; primShowFloat
+  )
+
+------------------------------------------------------------------------
+-- Operations
 
 show : Float → String
 show = primShowFloat
-
-infix 4 _≟_
-
-_≟_ : (x y : Float) → Dec (x ≡ y)
-x ≟ y with primFloatEquality x y
-... | true  = yes trustMe
-... | false = no whatever
-  where postulate whatever : _

src/Data/Float/Unsafe.agda

@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe Float operations
+------------------------------------------------------------------------
+
+module Data.Float.Unsafe where
+
+open import Data.Float
+open import Data.Bool.Base using (false; true)
+open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.TrustMe
+
+------------------------------------------------------------------------
+-- Equality testing
+
+infix 4 _≟_
+
+_≟_ : (x y : Float) → Dec (x ≡ y)
+x ≟ y with primFloatEquality x y
+... | true  = yes trustMe
+... | false = no whatever
+  where postulate whatever : _

src/Data/Nat/Base.agda

@@ -11,7 +11,7 @@ open import Function using (_∘_)
 open import Relation.Binary
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core
-import Relation.Binary.PropositionalEquality.TrustMe as TrustMe
+
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
 infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_
@@ -86,9 +86,6 @@ m ≥″ n = n ≤″ m
 _>″_ : Rel ℕ 0ℓ
 m >″ n = n <″ m
 
-erase : ∀ {m n} → m ≤″ n → m ≤″ n
-erase (less-than-or-equal eq) = less-than-or-equal (TrustMe.erase eq)
-
 ------------------------------------------------------------------------
 -- Arithmetic