[ fix #698 ] Make reflection module type check under --safe (#799)

* [ float ] bringing in the new agda features

* [ name ] with safe decidable equality

* [ meta ] with safe decidable equality

* [ reflection ] safe and compatible with --without-K

* [ literal ] moved to their own file

* [ reflection ] more deprecations

* [ cleanup ] import list of Reflection

* [ reflection ] extracting Argument, Pattern

Also cleanup, deprecation, new unArg-dec magic.

* [ fix ] removing Reflection from the list of unsafe modules

* [ changelog ] list new modules

* [ deprecation ] of arg-info injectivity proofs

* [ abstraction ] taken to its own module

* [ build ] removing fake unsafe files, cleaning up GenerateEverything

* [ refactor ] introducing DecidableEquality

* [ re #803 ] 'gradual' decidable equality combinator for list

* [ reflection ] putting Term in its own module

Some cleaning up still needed. However I am stuck on a refactoring.

* [ fix ] forgot to add Reflection.Term

+ Additional cleanup

* [ fix ] no need to deprecate *private* definitions!

* [ deprecated ] functions moved to Reflection.Term

* [ reflection ] moving Definition to Reflection.Definition

* [ typo ]

* [ cosmetic ] more uses of DecidableEquality

* [ changelog ] new modules

Author: gallais

.travis.yml

@@ -30,7 +30,7 @@ install:
   # installing the dev version of Agda
   - git clone https://github.com/agda/agda
   - cd agda
-  - git checkout b57260d0ceb1de4a5edc323d8ec2361904b5066e
+  - git checkout 39c273eb6eb3ab68c23b0de7a19eaadd84f0e5fb
   # checking whether .ghc is still valid
   - cabal install alex happy
   - cabal install --only-dependencies --dry -v > $HOME/installplan.txt

CHANGELOG.md

@@ -66,6 +66,9 @@ New modules
   Data.AVL.NonEmpty
   Data.AVL.NonEmpty.Propositional
 
+  Data.Float.Base
+  Data.Float.Properties
+
   Data.List.Membership.Propositional.Properties.WithK
 
   Data.List.Relation.Binary.Disjoint.Propositional
@@ -101,6 +104,18 @@ New modules
   Data.Word.Base
   Data.Word.Properties
 
+  Reflection.Abstraction
+  Reflection.Argument
+  Reflection.Argument.Information
+  Reflection.Argument.Relevance
+  Reflection.Argument.Visibility
+  Reflection.Definition
+  Reflection.Literal
+  Reflection.Meta
+  Reflection.Name
+  Reflection.Pattern
+  Reflection.Term
+
   Relation.Binary.Construct.Closure.Equivalence.Properties
   Relation.Binary.Rewriting
 
@@ -218,8 +233,8 @@ been attached to all deprecated names.
   favour of `⊤` and `tt` from `Data.Unit`, as it turns out that the latter
   have been automatically mapped to the Haskell equivalent for quite some time.
 
-* The module `Data.Word.Unsafe` has been deprecated as there are no
-  longer any unsafe operations.
+* The modules `Data.Word.Unsafe` and `Data.Float.Unsafe` have been removed
+  as there are no longer any unsafe operations.
 
 * Renamed a few `-identity` lemmas in `Codata.Stream.Properties` as they were
   proving two streams bisimilar rather than propositionally equal.
@@ -355,6 +370,9 @@ Other minor additions
   toNatDigits : (base : ℕ) {base≤16 : True (1 ≤? base)} → ℕ → List ℕ
   ```
 
+* Decidable equality over floating point numbers has been made safe and
+  so  `_≟_` has been moved from `Data.Float.Unsafe` to `Data.Float.Properties`.
+
 * Added new pattern synonyms to `Data.Integer`:
   ```agda
   pattern +0       = + 0
@@ -397,6 +415,8 @@ Other minor additions
   foldr-preservesᵇ : (P x → P y → P (f x y)) → P e → All P xs   → P (foldr f e xs)
   foldr-preservesʳ : (P y → P (f x y))       → P e              → P (foldr f e xs)
   foldr-preservesᵒ : (P x ⊎ P y → P (f x y)) → P e ⊎ Any P xs   → P (foldr f e xs)
+
+  ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x List.∷ xs ≡ y ∷ ys)
   ```
 
 * Defined a new utility in `Data.List.Relation.Binary.Permutation.Inductive.Properties`:
@@ -637,8 +657,9 @@ Other minor additions
 
 * Added new definitions in `Relation.Binary.Core`:
   ```agda
-  Universal _∼_    = ∀ x y → x ∼ y
-  Recomputable _~_ = ∀ {x y} → .(x ~ y) → x ~ y
+  Universal _∼_       = ∀ x y → x ∼ y
+  Recomputable _~_    = ∀ {x y} → .(x ~ y) → x ~ y
+  DecidableEquality A = Decidable {A = A} _≡_
   ```
 
 * Added new proof to `Relation.Binary.Consequences`:

GenerateEverything.hs

@@ -1,9 +1,11 @@
 {-# LANGUAGE PatternGuards #-}
 
 import Control.Applicative
+import Control.Monad
 
 import qualified Data.List as List
 
+import System.Directory
 import System.Environment
 import System.Exit
 import System.FilePath
@@ -21,7 +23,7 @@ srcDir         = "src"
 -- | Checks whether a module is declared (un)safe
 
 unsafeModules :: [FilePath]
-unsafeModules = map toAgdaFilePath
+unsafeModules = map modToFile
   [ "Codata.Musical.Cofin"
   , "Codata.Musical.Colist"
   , "Codata.Musical.Colist.Infinite-merge"
@@ -30,37 +32,37 @@ unsafeModules = map toAgdaFilePath
   , "Codata.Musical.Covec"
   , "Codata.Musical.M"
   , "Codata.Musical.Stream"
-  , "Data.Char.Unsafe"
-  , "Data.Float.Unsafe"
-  , "Data.Nat.Unsafe"
-  , "Data.Nat.DivMod.Unsafe"
-  , "Data.String.Unsafe"
-  , "Data.Word.Unsafe"
   , "Debug.Trace"
   , "Foreign.Haskell"
   , "IO"
   , "IO.Primitive"
-  , "Reflection"
   , "Relation.Binary.PropositionalEquality.TrustMe"
   ] where
 
-  toAgdaFilePath :: String -> FilePath
-  toAgdaFilePath name = concat
-    [ "src/"
-    , map (\ c -> if c == '.' then '/' else c) name
-    , ".agda"
-    ]
-
 isUnsafeModule :: FilePath -> Bool
-isUnsafeModule =
-  -- GA 2019-02-24: it is crucial to use an anonymous lambda
-  -- here so that `unsafeModules` is shared between all calls
-  -- to `isUnsafeModule`.
-  \ fp -> unqualifiedModuleName fp == "Unsafe"
-       || fp `elem` unsafeModules
+isUnsafeModule fp =
+    unqualifiedModuleName fp == "Unsafe"
+    || fp `elem` unsafeModules
 
 -- | Checks whether a module is declared as using K
 
+withKModules :: [FilePath]
+withKModules = map modToFile
+  [ "Axiom.Extensionality.Heterogeneous"
+  , "Data.Star.BoundedVec"
+  , "Data.Star.Decoration"
+  , "Data.Star.Environment"
+  , "Data.Star.Fin"
+  , "Data.Star.Pointer"
+  , "Data.Star.Vec"
+  , "Data.String.Unsafe"
+  , "Relation.Binary.HeterogeneousEquality"
+  , "Relation.Binary.HeterogeneousEquality.Core"
+  , "Relation.Binary.HeterogeneousEquality.Quotients.Examples"
+  , "Relation.Binary.HeterogeneousEquality.Quotients"
+  , "Relation.Binary.PropositionalEquality.TrustMe"
+  ]
+
 isWithKModule :: FilePath -> Bool
 isWithKModule =
   -- GA 2019-02-24: it is crucial to use an anonymous lambda
@@ -69,31 +71,6 @@ isWithKModule =
   \ fp -> unqualifiedModuleName fp == "WithK"
        || fp `elem` withKModules
 
-  where
-
-  withKModules :: [FilePath]
-  withKModules = map modToFile
-    [ "Axiom.Extensionality.Heterogeneous"
-    , "Data.Char.Unsafe"
-    , "Data.Float.Unsafe"
-    , "Data.Nat.Unsafe"
-    , "Data.Nat.DivMod.Unsafe"
-    , "Data.Star.BoundedVec"
-    , "Data.Star.Decoration"
-    , "Data.Star.Environment"
-    , "Data.Star.Fin"
-    , "Data.Star.Pointer"
-    , "Data.Star.Vec"
-    , "Data.String.Unsafe"
-    , "Data.Word.Unsafe"
-    , "Reflection"
-    , "Relation.Binary.HeterogeneousEquality"
-    , "Relation.Binary.HeterogeneousEquality.Core"
-    , "Relation.Binary.HeterogeneousEquality.Quotients.Examples"
-    , "Relation.Binary.HeterogeneousEquality.Quotients"
-    , "Relation.Binary.PropositionalEquality.TrustMe"
-    ]
-
 unqualifiedModuleName :: FilePath -> String
 unqualifiedModuleName = dropExtension . takeFileName
 
@@ -104,7 +81,6 @@ isLibraryModule f =
   takeExtension f `elem` [".agda", ".lagda"]
   && unqualifiedModuleName f /= "Core"
 
-
 ---------------------------------------------------------------------------
 -- Analysing library files
 
@@ -209,6 +185,13 @@ analyse fp = do
     , status     = classify fp hd ls
     }
 
+checkFilePaths :: String -> [FilePath] -> IO ()
+checkFilePaths cat fps = forM_ fps $ \ fp -> do
+  b <- doesFileExist fp
+  if b
+    then pure ()
+    else error $ fp ++ " is listed as " ++ cat ++ " but does not exist."
+
 ---------------------------------------------------------------------------
 -- Collecting all non-Core library files, analysing them and generating
 -- 4 files:
@@ -223,6 +206,9 @@ main = do
     [] -> return ()
     _  -> hPutStr stderr usage >> exitFailure
 
+  checkFilePaths "unsafe" unsafeModules
+  checkFilePaths "using K" withKModules
+
   header  <- readFileUTF8 headerFile
   modules <- filter isLibraryModule . List.sort <$>
                find always

lib.cabal

@@ -14,6 +14,7 @@ executable GenerateEverything
   main-is:          GenerateEverything.hs
   default-language: Haskell2010
   build-depends:      base >= 4.9.0.0 && < 4.13
+                    , directory >= 1.0.0.0 && < 1.4
                     , filemanip >= 0.3.6.2 && < 0.4
                     , filepath >= 1.4.1.0 && < 1.5
 

src/Data/Float.agda

@@ -1,27 +1,15 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Floats
+-- Floating point numbers
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Float where
 
-open import Data.String.Base using (String)
-
-------------------------------------------------------------------------
--- Re-export built-ins publically
-
-open import Agda.Builtin.Float public
-  using
-  ( Float
-  ; primFloatEquality
-  ; primShowFloat
-  )
-
 ------------------------------------------------------------------------
--- Operations
+-- Re-export base definitions and decidability of equality
 
-show : Float → String
-show = primShowFloat
+open import Data.Float.Base public
+open import Data.Float.Properties using (_≈?_; _<?_; _≟_; _==_) public

src/Data/Float/Base.agda

@@ -0,0 +1,55 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Floats: basic types and operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Float.Base where
+
+open import Relation.Binary.Core using (Rel)
+import Data.Word.Base as Word
+open import Function using (_on_)
+open import Agda.Builtin.Equality
+
+------------------------------------------------------------------------
+-- Re-export built-ins publically
+
+open import Agda.Builtin.Float public
+  using (Float)
+  renaming
+  -- Relations
+  ( primFloatEquality          to _≡ᵇ_
+  ; primFloatLess              to _≤ᵇ_
+  ; primFloatNumericalEquality to _≈ᵇ_
+  ; primFloatNumericalLess     to _≲ᵇ_
+  -- Conversions
+  ; primShowFloat     to show
+  ; primFloatToWord64 to toWord
+  ; primNatToFloat    to fromℕ
+  -- Operations
+  ; primFloatPlus   to _+_
+  ; primFloatMinus  to _-_
+  ; primFloatTimes  to _*_
+  ; primFloatNegate to -_
+  ; primFloatDiv    to _÷_
+  ; primFloatSqrt   to sqrt
+  ; primRound       to round
+  ; primFloor       to ⌊_⌋
+  ; primCeiling     to ⌈_⌉
+  ; primExp         to e^_
+  ; primLog         to log
+  ; primSin         to sin
+  ; primCos         to cos
+  ; primTan         to tan
+  ; primASin        to asin
+  ; primACos        to acos
+  ; primATan        to atan
+  )
+
+_≈_ : Rel Float _
+_≈_ = Word._≈_ on toWord
+
+_<_ : Rel Float _
+_<_ = Word._<_ on toWord