Merge branch 'master' into data-map

Author: viktorcsimma

.github/workflows/ci.yml

@@ -23,10 +23,8 @@ jobs:
         os: [ubuntu-latest]   # macOS-latest, windows-latest
         cabal: ["3.8"]
         ghc:
-          - "8.6.5"
           - "8.8.4"
           - "8.10.7"
-          - "9.0.2"
           - "9.2.5"
           - "9.4.3"
           - "9.6.3"

README.md

@@ -2,40 +2,14 @@
 
 # agda2hs
 
-Agda2hs is a tool for producing verified and readable Haskell code by
-extracting it from a (lightly annotated) Agda program. For example,
-the following Agda program encodes well-formed binary search trees:
-
-```agda
-open import Haskell.Prelude
-
-_≤_ : {{Ord a}} → a → a → Set
-x ≤ y = (x <= y) ≡ True
-
-data BST (a : Set) {{@0 _ : Ord a}} (@0 lower upper : a) : Set where
-  Leaf : (@0 pf : lower ≤ upper) → BST a lower upper
-  Node : (x : a) (l : BST a lower x) (r : BST a x upper) → BST a lower upper
-
-{-# COMPILE AGDA2HS BST #-}
-```
-
-agda2hs translates this to the following Haskell datatype:
-
-```haskell
-module BST where
-
-data BST a = Leaf
-           | Node a (BST a) (BST a)
-```
-
-## Objective
-
-The goal of this project is *not* to translate arbitrary Agda code to Haskell.
-Rather it is to carve out a common sublanguage between Agda and Haskell,
-with a straightforward translation from the Agda side to the Haskell side.
-This lets you write your program in the Agda fragment, using full Agda
-to prove properties about it, and then translate it to nice looking readable
-Haskell code that you can show your Haskell colleagues without shame.
+Agda2hs is a tool for producing verified and readable Haskell code by extracting
+it from a (lightly annotated) Agda program. The goal of this project is *not* to
+translate arbitrary Agda code to Haskell. Rather it is to carve out a common
+sublanguage between Agda and Haskell, with a straightforward translation from
+the Agda side to the Haskell side. This lets you write your program in the Agda
+fragment, using full Agda to prove properties about it, and then translate it to
+nice looking readable Haskell code that you can show your Haskell colleagues
+without shame.
 
 ## Documentation
 

agda2hs.cabal

@@ -52,32 +52,38 @@ executable agda2hs
                        Agda2Hs.Compile.TypeDefinition,
                        Agda2Hs.Compile.Types,
                        Agda2Hs.Compile.Utils,
+                       Agda2Hs.Compile.Var,
                        Agda2Hs.Config,
                        Agda2Hs.HsUtils,
                        Agda2Hs.Pragma,
                        Agda2Hs.Render,
                        AgdaInternals,
                        Paths_agda2hs
   autogen-modules:     Paths_agda2hs
-  build-depends:       base >= 4.10 && < 4.20,
-                       Agda >= 2.6.4 && < 2.6.5,
-                       bytestring >= 0.11.5 && < 0.13,
-                       containers >= 0.6 && < 0.8,
-                       unordered-containers >= 0.2.19 && < 0.3,
-                       mtl >= 2.2.2 && < 2.4,
-                       directory >= 1.2.6.2 && < 1.4,
-                       filepath >= 1.4.1.0 && < 1.5,
-                       haskell-src-exts >= 1.23 && < 1.25,
-                       syb >= 0.7.2 && < 0.8,
-                       text >= 2.0.2 && < 2.2,
-                       deepseq >= 1.4.4 && < 1.6,
-                       yaml >= 0.11 && < 0.12,
-                       aeson >= 2.2 && < 2.3,
+  build-depends:       base                 >= 4.13    && < 4.20,
+                       Agda                 >= 2.6.4   && < 2.6.5,
+                       bytestring           >= 0.11.5  && < 0.13,
+                       containers           >= 0.6     && < 0.8,
+                       unordered-containers >= 0.2.19  && < 0.3,
+                       mtl                  >= 2.2     && < 2.3 || >= 2.3.1,
+                       transformers         >= 0.6     && < 0.7,
+                       monad-control        >= 1.0     && < 1.1,
+                       directory            >= 1.2.6.2 && < 1.4,
+                       filepath             >= 1.4.1.0 && < 1.5,
+                       haskell-src-exts     >= 1.23    && < 1.25,
+                       syb                  >= 0.7.2   && < 0.8,
+                       text                 >= 2.0.2   && < 2.2,
+                       deepseq              >= 1.4.4   && < 1.6,
+                       yaml                 >= 0.11    && < 0.12,
+                       aeson                >= 2.2     && < 2.3,
   default-language:    Haskell2010
   default-extensions:  LambdaCase
                        RecordWildCards
                        FlexibleContexts
                        MultiWayIf
                        TupleSections
                        ScopedTypeVariables
-  ghc-options:         -Werror
+                       ViewPatterns
+                       NamedFieldPuns
+                       PatternSynonyms
+  ghc-options:         -Werror -rtsopts

cabal.project

@@ -1 +1,3 @@
 packages: ./agda2hs.cabal
+constraints: Agda +debug
+

docs/source/index.md

@@ -1,5 +1,72 @@
 # agda2hs Documentation
 
+`agda2hs` is a tool for producing verified and readable Haskell code by
+extracting it from a (lightly annotated) Agda program. For example,
+the following Agda program encodes well-formed binary search trees:
+
+```agda
+open import Haskell.Prelude
+
+_≤_ : {{Ord a}} → a → a → Set
+x ≤ y = (x <= y) ≡ True
+
+data BST (a : Set) {{@0 _ : Ord a}} (@0 lower upper : a) : Set where
+  Leaf : (@0 pf : lower ≤ upper) → BST a lower upper
+  Node : (x : a) (l : BST a lower x) (r : BST a x upper) → BST a lower upper
+
+{-# COMPILE AGDA2HS BST #-}
+```
+
+agda2hs translates this to the following Haskell datatype:
+
+```haskell
+module BST where
+
+data BST a = Leaf
+           | Node a (BST a) (BST a)
+```
+
+`agda2hs` is intended to be used together with the provided `Haskell.Prelude`
+module, which provides an Agda implementation of (a large subset of) the Haskell
+Prelude. It also provides proofs for reasoning about Haskell functions under the
+`Haskell.Law` namespace. `agda2hs` is *not* compatible with other Agda libraries
+such as the Agda standard library.
+
+## Objective
+
+The goal of this project is *not* to translate arbitrary Agda code to Haskell.
+Rather it is to carve out a common sublanguage between Agda and Haskell,
+with a straightforward translation from the Agda side to the Haskell side.
+This lets you write your program in the Agda fragment, using full Agda
+to prove properties about it, and then translate it to nice looking readable
+Haskell code that you can show your Haskell colleagues without shame.
+
+If you want to compile arbitrary Agda programs to runnable (but not readable)
+Haskell, you should instead use the built-in
+[GHC backend of Agda](https://agda.readthedocs.io/en/v2.6.4/tools/compilers.html#ghc-backend)
+(a.k.a. MAlonzo).
+
+## Documentation
+
+The documentation you are currently reading is a work in progress, so if you
+have been using `agda2hs` and want to contribute in some way, adding
+documentation or examples would be very welcome.
+
+agda2hs was introduced in the Haskell Symposium '22 paper [Reasonable Agda is
+Correct Haskell: Writing Verified Haskell using
+agda2hs](https://jesper.sikanda.be/files/reasonable-agda-is-correct-haskell.pdf).
+
+## Future work
+
+Currently `agda2hs` is under active development, please take a look at the
+[issue tracker](https://github.com/agda/agda2hs/issues). If you have a
+suggestion for a new feature that is not yet on the issue tracker, you are
+welcome to create a new issue or a PR. Feature requests should be of the form
+"Add support for Haskell feature X", *not* "Add support for Agda feature Y" (see
+"Objective" above). If you want to compile arbitrary Agda code to Haskell, you
+are advised to use Agda's built-in GHC backend instead.
+
+
 ```{toctree}
 ---
 maxdepth: 1

lib/Haskell/Extra/Dec.agda

@@ -41,3 +41,7 @@ mapDec : @0 (a → b)
 mapDec f g (True  ⟨ x ⟩) = True  ⟨ f x   ⟩
 mapDec f g (False ⟨ h ⟩) = False ⟨ h ∘ g ⟩
 {-# COMPILE AGDA2HS mapDec transparent #-}
+
+ifDec : Dec a → (@0 {{a}} → b) → (@0 {{a → ⊥}} → b) → b
+ifDec (b ⟨ p ⟩) x y = if b then (λ where {{refl}} → x {{p}}) else (λ where {{refl}} → y {{p}})
+{-# COMPILE AGDA2HS ifDec inline #-}

lib/Haskell/Extra/Delay.agda

@@ -0,0 +1,39 @@
+{-# OPTIONS --sized-types #-}
+
+module Haskell.Extra.Delay where
+
+open import Agda.Builtin.Size public
+
+open import Haskell.Prelude
+open import Haskell.Prim.Thunk
+open import Haskell.Extra.Refinement
+
+private variable
+  x y z : a
+  @0 i : Size
+
+data Delay (a : Set) (@0 i : Size) : Set where
+  now : a → Delay a i
+  later : Thunk (Delay a) i → Delay a i
+
+data HasResult (x : a) : Delay a i → Set where
+  now   : HasResult x (now x)
+  later : HasResult x (y .force) → HasResult x (later y)
+
+runDelay : {@0 x : a} (y : Delay a ∞) → @0 HasResult x y → a
+runDelay (now x) now = x
+runDelay (later y) (later p) = runDelay (y .force) p
+
+runDelaySound : {@0 x : a} (y : Delay a ∞) → (@0 hr : HasResult x y) → runDelay y hr ≡ x
+runDelaySound (now x) now = refl
+runDelaySound (later y) (later hr) = runDelaySound (y .force) hr
+
+-- tryDelay and unDelay cannot and should not be compiled to Haskell,
+-- so they are marked as erased.
+@0 tryDelay : (y : Delay a ∞) → Nat → Maybe (∃ a (λ x → HasResult x y))
+tryDelay (now x)   _       = Just (x ⟨ now ⟩)
+tryDelay (later y) zero    = Nothing
+tryDelay (later y) (suc n) = fmap (mapRefine later) (tryDelay (y .force) n)
+
+@0 unDelay : (y : Delay a ∞) (n : Nat) → @0 {IsJust (tryDelay y n)} → a
+unDelay y n {p} = fromJust (tryDelay y n) {p} .value

lib/Haskell/Extra/Erase.agda

@@ -42,6 +42,7 @@ module Haskell.Extra.Erase where
   instance
     rezz-id : {x : a} → Rezz a x
     rezz-id = rezz _
+  {-# COMPILE AGDA2HS rezz-id inline #-}
 
   rezzCong : {@0 a : Set} {@0 x : a} (f : a → b) → Rezz a x → Rezz b (f x)
   rezzCong f (Rezzed x p) = Rezzed (f x) (cong f p)

lib/Haskell/Extra/Loop.agda

@@ -3,14 +3,6 @@ open import Haskell.Prelude
 
 module Haskell.Extra.Loop where
 
-IsJust : Maybe a → Set
-IsJust Nothing  = ⊥
-IsJust (Just _) = ⊤
-
-fromJust : (x : Maybe a) → @0 {IsJust x} → a
-fromJust (Just x) = x
-fromJust Nothing  = error "fromJust called on Nothing"
-
 data Fuel (f : a → Either a b) : (x : Either a b) → Set where
   done : ∀ {y} → Fuel f (Right y)
   more : ∀ {x} → Fuel f (f x) → Fuel f (Left x)

lib/Haskell/Extra/Refinement.agda

@@ -6,10 +6,23 @@ open import Agda.Primitive
 private variable
   ℓ ℓ′ : Level
 
-record ∃ (@0 a : Set ℓ) (@0 P : a → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
+record ∃ (a : Set ℓ) (@0 P : a → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
   constructor _⟨_⟩
   field
     value    : a
     @0 proof : P value
 open ∃ public
 {-# COMPILE AGDA2HS ∃ unboxed #-}
+
+mapRefine : {@0 P Q : a → Set ℓ} (@0 f : ∀ {x} → P x → Q x) → ∃ a P → ∃ a Q
+mapRefine f (x ⟨ p ⟩) = x ⟨ f p ⟩
+
+{-# COMPILE AGDA2HS mapRefine transparent #-}
+
+refineMaybe : {@0 P : a → Set ℓ} 
+            → (mx : Maybe a) → @0 (∀ {x} → mx ≡ Just x → P x)
+            → Maybe (∃ a P)
+refineMaybe Nothing f = Nothing
+refineMaybe (Just x) f = Just (x ⟨ f refl ⟩)
+
+{-# COMPILE AGDA2HS refineMaybe transparent #-}

lib/Haskell/Extra/Sigma.agda

@@ -0,0 +1,16 @@
+module Haskell.Extra.Sigma where
+
+record Σ (a : Set) (b : @0 a → Set) : Set where
+  constructor _,_
+  field
+    fst : a
+    snd : b fst
+open Σ public
+
+infix 2 Σ-syntax
+
+Σ-syntax : (a : Set) → (@0 a → Set) → Set
+Σ-syntax = Σ
+{-# COMPILE AGDA2HS Σ-syntax inline #-}
+
+syntax Σ-syntax a (λ x → b) = Σ[ x ∈ a ] b

lib/Haskell/Law.agda

@@ -3,13 +3,18 @@ module Haskell.Law where
 open import Haskell.Prim
 open import Haskell.Prim.Bool
 
+open import Haskell.Law.Def          public
 open import Haskell.Law.Applicative  public
 open import Haskell.Law.Bool         public
+open import Haskell.Law.Either       public
 open import Haskell.Law.Eq           public
 open import Haskell.Law.Equality     public
 open import Haskell.Law.Functor      public
+open import Haskell.Law.Int          public
+open import Haskell.Law.Integer      public
 open import Haskell.Law.List         public
 open import Haskell.Law.Maybe        public
 open import Haskell.Law.Monad        public
 open import Haskell.Law.Monoid       public
+open import Haskell.Law.Nat          public
 open import Haskell.Law.Ord          public

lib/Haskell/Law/Applicative/List.agda

@@ -22,7 +22,11 @@ private
   compositionList : {a b c : Set} → (u : List (b → c)) (v : List (a → b)) (w : List a)
     → ((((pure _∘_) <*> u) <*> v) <*> w) ≡ (u <*> (v <*> w))
   compositionList [] _  _  = refl
-  compositionList us vs ws = trustMe -- TODO
+  compositionList (u ∷ us) v w
+    rewrite sym $ concatMap-++-distr (map (u ∘_) v) (((pure _∘_) <*> us) <*> v) (λ f → map f w)
+      | sym $ map-<*>-recomp v w u
+      | compositionList us v w
+    = refl 
 
   interchangeList : {a b : Set} → (u : List (a → b)) → (y : a)
     → (u <*> (pure y)) ≡ (pure (_$ y) <*> u)

lib/Haskell/Law/Def.agda

@@ -0,0 +1,6 @@
+module Haskell.Law.Def where
+
+open import Haskell.Prim
+
+Injective : (a → b) → Set _
+Injective f = ∀ {x y} → f x ≡ f y → x ≡ y

lib/Haskell/Law/Either.agda

@@ -0,0 +1,12 @@
+module Haskell.Law.Either where
+
+open import Haskell.Prim
+open import Haskell.Prim.Either
+
+open import Haskell.Law.Def
+
+Left-injective : Injective (Left {a}{b})
+Left-injective refl = refl
+
+Right-injective : Injective (Right {a}{b})
+Right-injective refl = refl

lib/Haskell/Law/Eq.agda

@@ -1,6 +1,4 @@
 module Haskell.Law.Eq where
 
-open import Haskell.Law.Eq.Def      public
-open import Haskell.Law.Eq.Bool     public
-open import Haskell.Law.Eq.Maybe    public
-open import Haskell.Law.Eq.Ordering public
+open import Haskell.Law.Eq.Def       public
+open import Haskell.Law.Eq.Instances public