Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update to agda-2.8.0, but there are broken files #1

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Update to agda-2.8.0, but there are broken files
andreasabel committed Nov 25, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit 2afc44d105a1a86ccfdcae6f493a4f59caa41004
20 changes: 9 additions & 11 deletions src/NativePolyIO.agda
Original file line number Diff line number Diff line change
@@ -7,34 +7,32 @@ open import Level
record Unit {α} : Set α where
constructor unit

{-# HASKELL type AgdaUnit a = () #-}
{-# FOREIGN GHC type AgdaUnit a = () #-}

{-# COMPILED_DATA Unit AgdaUnit () #-}
{-# COMPILE GHC Unit = data AgdaUnit () #-}

postulate
NativeIO : ∀ {ℓ} → Set ℓ → Set ℓ
nativeReturn : ∀ {a} {A : Set a} → A → NativeIO A
_native>>=_ : ∀ {a b} {A : Set a} {B : Set b} → NativeIO A → (A → NativeIO B) → NativeIO B


{-# COMPILED_TYPE NativeIO MAlonzo.Code.NativePolyIO.AgdaIO #-}
{-# COMPILE GHC NativeIO = type MAlonzo.Code.NativePolyIO.AgdaIO #-}
{-# BUILTIN IO NativeIO #-}

{-# HASKELL type AgdaIO a b = IO b #-}
{-# FOREIGN GHC type AgdaIO a b = IO b #-}


{-# COMPILED nativeReturn (\_ _ -> return :: a -> IO a) #-}
{-# COMPILED _native>>=_ (\_ _ _ _ ->
{-# COMPILE GHC nativeReturn = (\_ _ -> return :: a -> IO a) #-}
{-# COMPILE GHC _native>>=_ = (\_ _ _ _ ->
(>>=) :: IO a -> (a -> IO b) -> IO b) #-}

{-# IMPORT Data.Text.IO #-}
{-# FOREIGN GHC import Data.Text.IO #-}

postulate
nativePutStrLn : ∀ {ℓ} → String → NativeIO (Unit{ℓ})
nativeGetLine : NativeIO String




{-# COMPILED nativePutStrLn (\ _ s -> Data.Text.IO.putStrLn s) #-}
{-# COMPILED nativeGetLine Data.Text.IO.getLine #-}
{-# COMPILE GHC nativePutStrLn = (\ _ s -> Data.Text.IO.putStrLn s) #-}
{-# COMPILE GHC nativeGetLine = Data.Text.IO.getLine #-}
4 changes: 2 additions & 2 deletions src/SizedIO/Base.agda
Original file line number Diff line number Diff line change
@@ -2,10 +2,10 @@

module SizedIO.Base where

open import Data.Maybe.Base hiding ( _>>=_ )
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Sum renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)

open import Function
open import Function using (case_of_)
--open import Level using (_⊔_) renaming (suc to lsuc)
open import Size
open import Data.List
4 changes: 2 additions & 2 deletions src/SizedIO/coIOIOObject.agda
Original file line number Diff line number Diff line change
@@ -19,7 +19,7 @@ record IOObject' (i : Size) (iface : Interface)(C : Set)(R : C → Set) : Set
coinductive
field
method : ∀{j : Size< i} (m : Method iface) →
IO j C R (Response iface m × IOObject' j iface C R)
IO iface j (Response iface m × IOObject' j iface C R)
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Type error:

SizedIO/coIOIOObject.agda:22.17-22: error: [UnequalTerms]
Interface !=< IOInterface
when checking that the expression iface has type IOInterface

But I cannot see how this was supposed to work.

open IOObject' public


@@ -63,7 +63,7 @@ mutual
compileSelfRefaux i j iface Cext Rext A (coIO².return (r , obj)) = return' (r , compileSelfRef i iface Cext Rext obj)
compileSelfRefaux i j iface Cext Rext A (dof i' m f) = {! >>=!}
compileSelfRefaux i j iface Cext Rext A (do∞ c f) =
do' c (λ r → compileSelfRefaux'' i j iface Cext Rext A (f r))
exec' c (λ r → compileSelfRefaux'' i j iface Cext Rext A (f r))



12 changes: 6 additions & 6 deletions src/SizedPolyIO/Base.agda
Original file line number Diff line number Diff line change
@@ -2,10 +2,10 @@

module SizedPolyIO.Base where

open import Data.Maybe.Base
open import Data.Sum renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Sum.Base renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)

open import Function
open import Function using (case_of_)
open import Level using (_⊔_) renaming (suc to lsuc)
open import Size

@@ -40,11 +40,11 @@ module _ {γ ρ} {I : IOInterface γ ρ} (let C = Command I) (let R = Response I
return : ∀{i α}{A : Set α} (a : A) → IO I i A
force (return a) = return' a

do : ∀{i α}{A : Set α} (c : C) (f : R c → IO I i A) → IO I i A
force (do c f) = do' c f
do! : ∀{i α}{A : Set α} (c : C) (f : R c → IO I i A) → IO I i A
force (do! c f) = do' c f

do1 : ∀{i} (c : C) → IO I i (R c)
do1 c = do c return
do1 c = do! c return

infixl 2 _>>=_ _>>='_ _>>_

8 changes: 4 additions & 4 deletions src/StateSizedIO/Base.agda
Original file line number Diff line number Diff line change
@@ -29,7 +29,7 @@ module _ (ioi : IOInterface) (let C = Command ioi) (let R = Response ioi)
(let n = nextˢ oi)
where

record IOObjectˢ (i : Size) (s : Stateˢ) : Set where
record IOObjectˢ (i : Size) (s : S) : Set where
coinductive
field
method : ∀{j : Size< i} (m : M s) → IO ioi ∞ ( Σ[ r ∈ Rt s m ] IOObjectˢ j (n s m r))
@@ -40,7 +40,7 @@ open IOObjectˢ public

module _ (I : IOInterfaceˢ )
(let S = IOStateˢ I) (let C = Commandˢ I)
(let R = Responseˢ I) (let n = nextˢ I)
(let R = Responseˢ I) (let n = IOnextˢ I)
where

mutual
@@ -60,8 +60,8 @@ module _ (I : IOInterfaceˢ )
open IOˢ public

module _ {I : IOInterfaceˢ }
(let S = Stateˢ I) (let C = Commandˢ I)
(let R = Responseˢ I) (let n = nextˢ I)
(let S = IOStateˢ I) (let C = Commandˢ I)
(let R = Responseˢ I) (let n = IOnextˢ I)
where
returnˢ : ∀{i}{A : S → Set} (s : S) (a : A s) → IOˢ I i A s
forceˢ (returnˢ s a) = returnˢ' a
2 changes: 2 additions & 0 deletions src/StateSizedIO/IOObject.agda
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --guardedness #-}

module StateSizedIO.IOObject where

open import Data.Product
2 changes: 2 additions & 0 deletions src/StateSizedIO/Object.agda
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --guardedness #-}

module StateSizedIO.Object where

open import Data.Product
7 changes: 4 additions & 3 deletions src/UnSizedIO/Base.agda
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
{-# OPTIONS --guardedness #-}
{-# OPTIONS --postfix-projections #-}

module UnSizedIO.Base where

open import Data.Maybe.Base
open import Data.Sum renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)
open import Function
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Sum.Base renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)
open import Function using (case_of_)

open import NativeIO

2 changes: 2 additions & 0 deletions src/UnSizedIO/Console.agda
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --guardedness #-}

module UnSizedIO.Console where

open import NativeIO
2 changes: 2 additions & 0 deletions src/UnSizedIO/ConsoleObject.agda
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --guardedness #-}

module UnSizedIO.ConsoleObject where

open import UnSizedIO.Console
2 changes: 2 additions & 0 deletions src/UnSizedIO/IOObject.agda
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --guardedness #-}

module UnSizedIO.IOObject where

open import Data.Product
1 change: 0 additions & 1 deletion src/UnSizedIO/Object.agda
Original file line number Diff line number Diff line change
@@ -2,7 +2,6 @@ module UnSizedIO.Object where

open import Data.Product


record Interface : Set₁ where
field
Method : Set
2 changes: 2 additions & 0 deletions src/ooAgda.agda-lib
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
name: ooAgda
depend: standard-library
include: . ../examples
flags:
--sized-types