Switching back to vanilla agda2hs

acorn.agda-lib

@@ -1,4 +1,5 @@
 name: acorn
 depend:
-  agda2hs
+  agda2hs-base
+  agda2hs-containers
 include: src

src/Algebra/Order.agda

@@ -7,6 +7,7 @@ open import Haskell.Prim.Either
 open import Haskell.Prim using (⊥)
 open import Haskell.Prim.Tuple
 
+open import Tool.Logic
 open import Tool.ErasureProduct
 open import Tool.Relation
 open import Algebra.Setoid

src/Algebra/SemiRing.agda

@@ -11,9 +11,9 @@ open import Agda.Builtin.Unit
 open import Agda.Builtin.FromNat
 open import Agda.Builtin.Nat using (zero; suc)
 open import Agda.Builtin.Int using (pos; negsuc)
-open import Haskell.Prim.Tuple using (_↔_)
 open import Haskell.Prim using (⊥)
 
+open import Tool.Logic
 open import Tool.Relation
 open import Algebra.Setoid
 

src/Algebra/Setoid.agda

@@ -8,6 +8,7 @@ open import Haskell.Prim using (⊥)
 open import Haskell.Prim.Tuple
 open import Haskell.Prim.Either
 
+open import Tool.Logic
 open import Tool.Relation
 
 record Setoid (a : Set) : Set₁ where

src/Function/AlternatingSeries.agda

@@ -58,6 +58,9 @@ precision 2^k such as n*2^k < epsilon/2.
 -- This way, we can have only one stream and ensure
 -- the denominator is not zero.
 
+-- Whether we are near enough to zero that
+-- we can stop here.
+--
 -- We define this that way because
 -- we will need exactly this function
 -- in sumAlternatingStream.
@@ -75,14 +78,13 @@ thatNearToZero xk ε k = let prec = ratLog2Floor (proj₁ ε) {proj₂ ε} + neg
                                              prec)
                                 + shift one prec)
                           ≤# proj₁ (halvePos ε)
-                          {-
-                          ball (halvePos ε)
-                               (appDiv (num xk) (den xk) (denNotNull xk)
-                                     prec
-                                 + shift one prec)
-                               null)
-                          -}
 {-# COMPILE AGDA2HS thatNearToZero #-}
+
+-- A proposition-as-type meaning that
+-- for all ε, there exists a member in the stream
+-- which is near enough to zero
+-- (and we can stop there).
+-- This also means that the series converges to zero.
 HasThatNearToZero : {a : Set} {{ara : AppRational a}} -> Stream (Frac a) -> Set
 HasThatNearToZero xs = ∀ (ε : PosRational) -> Σ0 Nat (λ k -> IsTrue (thatNearToZero (index xs k) ε k))
 {-# COMPILE AGDA2HS HasThatNearToZero #-}
@@ -112,9 +114,9 @@ autoHasThatNearToZero xs ε = go xs ε 0
 
 -- we will need a tuple here
 IsAlternating : {a : Set} {{ara : AppRational a}} -> Stream (Frac a) -> Set
-IsAlternating xs = Tuple0 (HasThatNearToZero xs)
-                   ( (∀ (i : Nat) -> abs (index xs (suc i)) < abs (index xs i))  -- decreasing
-                   × (∀ (i : Nat) -> index xs i * index xs (suc i) < null) )     -- alternating
+IsAlternating xs = Tuple0 (HasThatNearToZero xs)                                -- converging to 0
+                   ( (∀ (i : Nat) -> abs (index xs (suc i)) < abs (index xs i)) -- decreasing
+                   × (∀ (i : Nat) -> index xs i * index xs (suc i) < null) )    -- alternating
 {-# COMPILE AGDA2HS IsAlternating #-}
 
 -- The sum of the first n elements of a stream.

src/Function/Exp.agda

@@ -58,17 +58,9 @@ smallExpQ : ∀ {a : Set} {{ara : AppRational a}}
 -- The seed is going to be a Nat × Frac a tuple,
 -- containing the index of the step (starting from 1) and the previous fraction.
 smallExpQ (x :&: _) = let xs = (coiteStream snd (λ {(n , fra) -> suc n , MkFrac (num fra * x) (den fra * cast (pos n)) cheat}) (1 , one)) in
-                       sumAlternatingStream xs
-                        -- the index for K&S 5.1:
-                        {-
-                          ∣xᵏ/k!∣ + ε/2k + ε/2k ≤ ε/2
-                          ∣xᵏ/k!∣ + ε/k ≤ ε/2
-                          huh; that won't be easy
-                          but if we have a proof with a rough overapproximation,
-                          we can put it into autoHasThatNearToZero
-                          and now, we can cheat it away
-                        -}
-                        (autoHasThatNearToZero xs cheat :&: cheat)
+                       sumAlternatingStream
+                         xs
+                         (autoHasThatNearToZero xs cheat :&: cheat)
 {-# COMPILE AGDA2HS smallExpQ #-}
 
 -- From Krebbers and Spitters:

src/Operator/Decidable.agda

@@ -7,9 +7,10 @@ module Operator.Decidable where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality
 open import Haskell.Prim.Either
-open import Haskell.Prim.Tuple using (_↔_)
+open import Haskell.Prim.Tuple
 open import Haskell.Prim using (IsTrue; if_then_else_)
 
+open import Tool.Logic
 open import Algebra.Setoid
 open import Tool.Relation
 open import Algebra.Order

src/RealTheory/AppRational.agda

@@ -29,6 +29,7 @@ open import Haskell.Prim using (id; const; IsTrue)
 
 open import Tool.Cheat
 
+open import Tool.Logic
 open import Tool.ErasureProduct
 open import Algebra.SemiRing
 open import Algebra.Ring

src/Tool/Logic.agda

@@ -0,0 +1,15 @@
+-- Some shortenings that don't already exist
+-- in the agda2hs library.
+{-# OPTIONS --erasure #-}
+module Tool.Logic where
+
+open import Agda.Primitive
+open import Haskell.Prim.Tuple
+
+-- I don't erase this for now;
+-- maybe there are some proofs needing those witnesses.
+-- But then, Haskell tuples only work with Set₀.
+infixr 2 _↔_
+_↔_ : Set -> Set -> Set
+A ↔ B = (A -> B) × (B -> A)
+

src/Tool/Witness.agda

@@ -7,9 +7,10 @@ module Tool.Witness where
 open import Agda.Builtin.Nat
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality
-open import Haskell.Prim.Tuple using (_↔_; _,_; fst)
+open import Haskell.Prim.Tuple using (_,_; fst)
 open import Haskell.Prim using (IsTrue; itsTrue)
 
+open import Tool.Logic
 open import Tool.PropositionalEquality
 open import Tool.ErasureProduct