Merge branch 'master' into experimental

Author: MatthewDaggitt

CHANGELOG.md

@@ -35,6 +35,7 @@ unsafeModules = map modToFile
   , "Debug.Trace"
   , "Foreign.Haskell"
   , "Foreign.Haskell.Coerce"
+  , "Foreign.Haskell.Either"
   , "Foreign.Haskell.Maybe"
   , "Foreign.Haskell.Pair"
   , "IO"

GenerateEverything.hs

@@ -1,7 +1,7 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 1.2-dev
+-- The Agda standard library, version 1.2
 --
 -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
 -- with contributions from Andreas Abel, Stevan Andjelkovic,
@@ -262,6 +262,10 @@ import IO
 -- More documentation
 ------------------------------------------------------------------------
 
+-- Examples of how decidability is handled in the library.
+
+import README.Decidability
+
 -- Some examples showing how the case expression can be used.
 
 import README.Case

README.agda

@@ -183,6 +183,10 @@ import README.Data.AVL
 
 import README.Data.List
 
+-- Some examples showing how the Fresh list can be used.
+
+import README.Data.List.Fresh
+
 -- Using List's Interleaving to define a fully certified filter function.
 
 import README.Data.Interleaving

README/Data.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example use case for a fresh list: sorted list
+------------------------------------------------------------------------
+
+module README.Data.List.Fresh where
+
+open import Data.Nat
+open import Data.List.Base
+open import Data.List.Fresh
+open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
+open import Data.Product
+open import Relation.Nary using (⌊_⌋; fromWitness)
+
+-- A sorted list of natural numbers can be seen as a fresh list
+-- where the notion of freshness is being smaller than all the
+-- existing entries
+
+SortedList : Set
+SortedList = List# ℕ _<_
+
+_ : SortedList
+_ = cons 0 (cons 1 (cons 3 (cons 10 [] _)
+      (s≤s (s≤s (s≤s (s≤s z≤n))) , _))
+      (s≤s (s≤s z≤n) , s≤s (s≤s z≤n) , _))
+      (s≤s z≤n , s≤s z≤n , s≤s z≤n , _)
+
+-- Clearly, writing these by hand can pretty quickly become quite cumbersome
+-- Luckily, if the notion of freshness we are using is decidable, we can
+-- make most of the proofs inferrable by using the erasure of the relation
+-- rather than the relation itself!
+
+-- We call this new type *I*SortedList because all the proofs will be implicit.
+
+ISortedList : Set
+ISortedList = List# ℕ ⌊ _<?_ ⌋
+
+-- The same example is now much shorter. It looks pretty much like a normal list
+-- except that we know for sure that it is well ordered.
+
+ins : ISortedList
+ins = 0 ∷# 1 ∷# 3 ∷# 10 ∷# []
+
+-- Indeed we can extract the support list together with a proof that it
+-- is ordered thanks to the combined action of toList converting a fresh
+-- list to a pair of a list and a proof and fromWitness which "unerases"
+-- a proof.
+
+ns : List ℕ
+ns = proj₁ (toList ins)
+
+sorted : AllPairs _<_ ns
+sorted = AllPairs.map (fromWitness _<_ _<?_) (proj₂ (toList ins))
+
+-- See the following module for an applied use-case of fresh lists
+open import README.Data.Trie.NonDependent

README/Data/List/Fresh.agda

@@ -51,38 +51,57 @@ module README.Data.Trie.NonDependent where
 open import Level
 open import Data.Unit
 open import Data.Bool
-open import Data.Char          as Char
-import Data.Char.Properties    as Char
-open import Data.List          as List using (List; []; _∷_)
-open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
-open import Data.Maybe         as Maybe
-open import Data.Product       as Prod
-open import Data.String.Base   as String using (String)
-open import Data.These         as These
-
-open import Function using (case_of_; _$_; _∘′_; id)
+open import Data.Char        as Char
+import Data.Char.Properties  as Char
+open import Data.List        as List using (List; []; _∷_)
+open import Data.List.Fresh  as List# using (List#; []; _∷#_)
+open import Data.Maybe       as Maybe
+open import Data.Product     as Prod
+open import Data.String      as String using (String)
+open import Data.These       as These
+
+open import Function using (case_of_; _$_; _∘′_; id; _on_)
+open import Relation.Nary
+open import Relation.Binary using (Rel)
+open import Relation.Nullary.Negation using (¬?)
 
 open import Data.Trie Char.<-strictTotalOrder-≈
 open import Data.AVL.Value
 
 ------------------------------------------------------------------------
 -- Generic lexer
 
-module Lexer
+record Lexer t : Set (suc t) where
+  field
   -- Our lexer is parametrised over the type of tokens
-  {t} {Tok : Set t}
-  -- We start with an association list between
-  -- * keywords (as Strings)
-  -- * keywords (as token values)
-  (lex : List⁺ (String × Tok))
+    Tok : Set t
+
+  -- Keywords are distinguished strings associated to tokens
+  Keyword : Set t
+  Keyword = String × Tok
+
+  -- Two keywords are considered distinct if the strings are not equal
+  Distinct : Rel Keyword 0ℓ
+  Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋
+
+  field
+
+  -- We ask users to provide us with a fresh list of keywords to guarantee
+  -- that no two keywords share the same string representation
+    keywords : List# Keyword Distinct
+
   -- Some characters are special: they are separators, breaking a string
   -- into a list of tokens. Some are associated to a token value
   -- (e.g. parentheses) others are not (e.g. space)
-  (breaking : Char → ∃ λ b → if b then Maybe Tok else Lift _ ⊤)
+    breaking : Char → ∃ λ b → if b then Maybe Tok else Lift _ ⊤
+
   -- Finally, strings which are not decoded as keywords are coerced
   -- using a function to token values.
-  (default  : String → Tok)
-  where
+    default  : String → Tok
+
+
+module _ {t} (L : Lexer t) where
+  open Lexer L
 
   tokenize : String → List Tok
   tokenize = start ∘′ String.toList where
@@ -107,7 +126,7 @@ module Lexer
     -- characters one by one
 
     init : Keywords
-    init = fromList $ List⁺.toList $ List⁺.map (Prod.map₁ String.toList) lex
+    init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords
 
     -- Kickstart the tokeniser with an empty accumulator and the initial
     -- trie.
@@ -148,33 +167,40 @@ module Lexer
 -- A small set of keywords for a language with expressions of the form
 -- `let x = e in b`.
 
-data TOK : Set where
-  LET EQ IN : TOK
-  LPAR RPAR : TOK
-  ID : String → TOK
+module LetIn where
+
+  data TOK : Set where
+    LET EQ IN : TOK
+    LPAR RPAR : TOK
+    ID : String → TOK
+
+  keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋)
+  keywords =  ("let" , LET)
+           ∷# ("="   , EQ)
+           ∷# ("in"  , IN)
+           ∷# []
 
-toks : List⁺ (String × TOK)
-toks = ("let" , LET)
-     ∷ ("="   , EQ)
-     ∷ ("in"  , IN)
-     ∷ []
+  -- Breaking characters: spaces (thrown away) and parentheses (kept)
+  breaking : Char → ∃ (λ b → if b then Maybe TOK else Lift 0ℓ ⊤)
+  breaking c = if isSpace c then true , nothing else parens c where
 
--- Breaking characters: spaces (thrown away) and parentheses (kept)
+    parens : Char → _
+    parens '(' = true , just LPAR
+    parens ')' = true , just RPAR
+    parens _   = false , _
 
-breaking : Char → ∃ λ b → if b then Maybe TOK else Lift _ ⊤
-breaking c = if isSpace c then true , nothing else parens c where
+  default : String → TOK
+  default = ID
 
-  parens : Char → _
-  parens '(' = true , just LPAR
-  parens ')' = true , just RPAR
-  parens _   = false , _
+letIn : Lexer 0ℓ
+letIn = record { LetIn }
 
 open import Agda.Builtin.Equality
-open Lexer toks breaking ID
 
 -- A test case:
 
-_ : tokenize "fix f x = let b = fix f in (f b) x"
+open LetIn
+_ : tokenize letIn "fix f x = let b = fix f in (f b) x"
   ≡ ID "fix"
   ∷ ID "f"
   ∷ ID "x"

README/Data/Trie/NonDependent.agda

@@ -0,0 +1,132 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Examples of decision procedures and how to use them
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module README.Decidability where
+
+-- Reflects and Dec are defined in Relation.Nullary, and operations on them can
+-- be found in Relation.Nullary.Reflects and Relation.Nullary.Decidable.
+
+open import Relation.Nullary as Nullary
+open import Relation.Nullary.Reflects
+open import Relation.Nullary.Decidable
+
+open import Data.Bool
+open import Data.List
+open import Data.List.Properties using (∷-injective)
+open import Data.Nat
+open import Data.Nat.Properties using (suc-injective)
+open import Data.Product
+open import Data.Unit
+open import Function
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nary
+open import Relation.Nullary.Product
+
+infix 4 _≟₀_ _≟₁_ _≟₂_
+
+-- A proof of `Reflects P b` shows that a proposition `P` has the truth value of
+-- the boolean `b`. A proof of `Reflects P true` amounts to a proof of `P`, and
+-- a proof of `Reflects P false` amounts to a refutation of `P`.
+
+ex₀ : (n : ℕ) → Reflects (n ≡ n) true
+ex₀ n = ofʸ refl
+
+ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false
+ex₁ n = ofⁿ λ ()
+
+ex₂ : (b : Bool) → Reflects (T b) b
+ex₂ false = ofⁿ id
+ex₂ true  = ofʸ tt
+
+-- A proof of `Dec P` is a proof of `Reflects P b` for some `b`.
+-- `Dec P` is declared as a record, with fields:
+--   does : Bool
+--   proof : Reflects P does
+
+ex₃ : (b : Bool) → Dec (T b)
+does  (ex₃ b) = b
+proof (ex₃ b) = ex₂ b
+
+-- We also have pattern synonyms `yes` and `no`, allowing both fields to be
+-- given at once.
+
+ex₄ : (n : ℕ) → Dec (zero ≡ suc n)
+ex₄ n = no λ ()
+
+-- It is possible, but not ideal, to define recursive decision procedures using
+-- only the `yes` and `no` patterns. The following procedure decides whether two
+-- given natural numbers are equal.
+
+_≟₀_ : (m n : ℕ) → Dec (m ≡ n)
+zero  ≟₀ zero  = yes refl
+zero  ≟₀ suc n = no λ ()
+suc m ≟₀ zero  = no λ ()
+suc m ≟₀ suc n with m ≟₀ n
+... | yes p = yes (cong suc p)
+... | no ¬p = no (¬p ∘ suc-injective)
+
+-- In this case, we can see that `does (suc m ≟ suc n)` should be equal to
+-- `does (m ≟ n)`, because a `yes` from `m ≟ n` gives rise to a `yes` from the
+-- result, and similarly for `no`. However, in the above definition, this
+-- equality does not hold definitionally, because we always do a case split
+-- before returning a result. To avoid this, we can return the `does` part
+-- separately, before any pattern matching.
+
+_≟₁_ : (m n : ℕ) → Dec (m ≡ n)
+zero  ≟₁ zero  = yes refl
+zero  ≟₁ suc n = no λ ()
+suc m ≟₁ zero  = no λ ()
+does  (suc m ≟₁ suc n) = does (m ≟₁ n)
+proof (suc m ≟₁ suc n) with m ≟₁ n
+... | yes p = ofʸ (cong suc p)
+... | no ¬p = ofⁿ (¬p ∘ suc-injective)
+
+-- We now get definitional equalities such as the following.
+
+_ : (m n : ℕ) → does (5 + m ≟₁ 3 + n) ≡ does (2 + m ≟₁ n)
+_ = λ m n → refl
+
+-- Even better, from a maintainability point of view, is to use `map` or `map′`,
+-- both of which capture the pattern of the `does` field remaining the same, but
+-- the `proof` field being updated.
+
+_≟₂_ : (m n : ℕ) → Dec (m ≡ n)
+zero  ≟₂ zero  = yes refl
+zero  ≟₂ suc n = no λ ()
+suc m ≟₂ zero  = no λ ()
+suc m ≟₂ suc n = map′ (cong suc) suc-injective (m ≟₂ n)
+
+_ : (m n : ℕ) → does (5 + m ≟₂ 3 + n) ≡ does (2 + m ≟₂ n)
+_ = λ m n → refl
+
+-- `map′` can be used in conjunction with combinators such as `_⊎-dec_` and
+-- `_×-dec_` to build complex (simply typed) decision procedures.
+
+module ListDecEq₀ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where
+
+  _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
+  []       ≟ᴸᴬ []       = yes refl
+  []       ≟ᴸᴬ (y ∷ ys) = no λ ()
+  (x ∷ xs) ≟ᴸᴬ []       = no λ ()
+  (x ∷ xs) ≟ᴸᴬ (y ∷ ys) =
+    map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≟ᴬ y ×-dec xs ≟ᴸᴬ ys)
+
+-- The final case says that `x ∷ xs ≡ y ∷ ys` exactly when `x ≡ y` *and*
+-- `xs ≡ ys`. The proofs are updated by the first two arguments to `map′`.
+
+-- In the case of ≡-equality tests, the pattern
+-- `map′ (congₙ c) c-injective (x₀ ≟ y₀ ×-dec ... ×-dec xₙ₋₁ ≟ yₙ₋₁)`
+-- is captured by `≟-mapₙ n c c-injective (x₀ ≟ y₀) ... (xₙ₋₁ ≟ yₙ₋₁)`.
+
+module ListDecEq₁ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where
+
+  _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
+  []       ≟ᴸᴬ []       = yes refl
+  []       ≟ᴸᴬ (y ∷ ys) = no λ ()
+  (x ∷ xs) ≟ᴸᴬ []       = no λ ()
+  (x ∷ xs) ≟ᴸᴬ (y ∷ ys) = ≟-mapₙ 2 _∷_ ∷-injective (x ≟ᴬ y) (xs ≟ᴸᴬ ys)

README/Decidability.agda

@@ -1,5 +1,5 @@
 name:            lib
-version:         1.2-dev
+version:         1.2
 cabal-version:   >= 1.10
 build-type:      Simple
 description:     Helper programs.