Skip to content

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

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.

Sign up for GitHub

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

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2afc44d
Update to agda-2.8.0, but there are broken files
andreasabel Nov 25, 2024
49586f1
More porting to Agda-2.8.0
andreasabel Jun 2, 2025
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
6 changes: 3 additions & 3 deletions examples/Sized/ConsoleExample.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,9 @@ open import SizedIO.Console hiding (main)
open import NativeIO

myProgram : ∀{i} → IOConsole i Unit
force myProgram = do' getLine λ line →
do (putStrLn line) λ _ →
do (putStrLn line) λ _ →
force myProgram = exec' getLine λ line →
exec (putStrLn line) λ _ →
exec (putStrLn line) λ _ →
myProgram


Expand Down
6 changes: 3 additions & 3 deletions examples/SizedPoly/Console.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ open import Level using () renaming (zero to lzero)

{-# TERMINATING #-}
myProgram : ∀{i} → IOConsole i (Unit {lzero})
myProgram = exec getLine λ line →
exec (putStrLn line) λ _ →
exec (putStrLn line) λ _ →
myProgram = do! getLine λ line →
do! (putStrLn line) λ _ →
do! (putStrLn line) λ _ →
myProgram


Expand Down
8 changes: 4 additions & 4 deletions examples/SizedPoly/SimpleCell.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,10 +35,10 @@ CellC i = ConsoleObject i (cellI String)
-- cellP is constructor for the consoleObject for interface (cellI String)
cellP : ∀{i} (s : String) → CellC i
force (method (cellP s) get) =
exec' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
do' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
return (s , cellP s)
force (method (cellP s) (put x)) =
exec' (putStrLn ("putting (" ++ x ++ ")")) λ _ →
do' (putStrLn ("putting (" ++ x ++ ")")) λ _ →
return (_ , (cellP x))


Expand All @@ -47,10 +47,10 @@ program : String → IOConsole ∞ Unit
program arg =
let c₀ = cellP "Start" in
method c₀ get >>= λ{ (s , c₁) →
exec1 (putStrLn s) >>
do1 (putStrLn s) >>
method c₁ (put arg) >>= λ{ (_ , c₂) →
method c₂ get >>= λ{ (s' , c₃) →
exec1 (putStrLn s') }}}
do1 (putStrLn s') }}}

main : NativeIO Unit
main = translateIOConsole (program "hello")
2 changes: 1 addition & 1 deletion examples/consoleExamples/simpleLoop.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module consoleExamples.simpleLoop where

open import ConsoleLib
open import Data.Bool renaming (not to ¬)
open import Data.String hiding (_==_)
open import Data.String renaming (_==_ to _==str_)
open import SizedIO.Base
open import Size

Expand Down
2 changes: 1 addition & 1 deletion examples/examplesPaperJFP/BasicIO.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module examplesPaperJFP.BasicIO where

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

open import examplesPaperJFP.NativeIOSafe
open import examplesPaperJFP.triangleRightOperator
Expand Down
2 changes: 0 additions & 2 deletions examples/examplesPaperJFP/ExampleDrawingProgram.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,6 @@ open import Data.String.Base
open import Data.Maybe.Base
open import Agda.Builtin.Char using (primCharEquality)

open import Function

open import SizedIO.Base
open import SizedIO.IOGraphicsLib hiding (translateIOGraphics) renaming (translateIOGraphicsLocal to translateNative)

Expand Down
2 changes: 1 addition & 1 deletion examples/examplesPaperJFP/StatefulObject.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ open import Size

open import NativeIO

open import SizedIO.Base
open import SizedIO.Base using (IOInterface; IO)


StackStateˢ = ℕ
Expand Down
2 changes: 1 addition & 1 deletion examples/examplesPaperJFP/safeFibStackMachineObjectOriented.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module examplesPaperJFP.safeFibStackMachineObjectOriented where
open import Data.Nat
open import Data.List
open import Data.Vec
open import Data.Sum
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Fin renaming (_+_ to _+f_)
open import Data.Product
open import examplesPaperJFP.StatefulObject
Expand Down
3 changes: 3 additions & 0 deletions examples/ooAgdaExamples.agda-lib
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
name: ooAgdaExamples
depend: standard-library
include: . ../src
flags:
--guardedness
--sized-types
20 changes: 9 additions & 11 deletions src/NativePolyIO.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/SizedIO/coIOIOObject.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down Expand Up @@ -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))



Expand Down
12 changes: 6 additions & 6 deletions src/SizedPolyIO/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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 _>>=_ _>>='_ _>>_

Expand Down
8 changes: 4 additions & 4 deletions src/StateSizedIO/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 2 additions & 0 deletions src/StateSizedIO/IOObject.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --guardedness #-}

module StateSizedIO.IOObject where

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

module StateSizedIO.Object where

open import Data.Product
Expand Down
7 changes: 4 additions & 3 deletions src/UnSizedIO/Base.agda
View file
Open in desktop
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

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

module UnSizedIO.Console where

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

module UnSizedIO.ConsoleObject where

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

module UnSizedIO.IOObject where

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

open import Data.Product


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