From 2afc44d105a1a86ccfdcae6f493a4f59caa41004 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Mon, 25 Nov 2024 17:27:26 +0100 Subject: [PATCH] Update to agda-2.8.0, but there are broken files --- src/NativePolyIO.agda | 20 +++++++++----------- src/SizedIO/Base.agda | 4 ++-- src/SizedIO/coIOIOObject.agda | 4 ++-- src/SizedPolyIO/Base.agda | 12 ++++++------ src/StateSizedIO/Base.agda | 8 ++++---- src/StateSizedIO/IOObject.agda | 2 ++ src/StateSizedIO/Object.agda | 2 ++ src/UnSizedIO/Base.agda | 7 ++++--- src/UnSizedIO/Console.agda | 2 ++ src/UnSizedIO/ConsoleObject.agda | 2 ++ src/UnSizedIO/IOObject.agda | 2 ++ src/UnSizedIO/Object.agda | 1 - src/ooAgda.agda-lib | 2 ++ 13 files changed, 39 insertions(+), 29 deletions(-) diff --git a/src/NativePolyIO.agda b/src/NativePolyIO.agda index d7e2a66..6961f20 100644 --- a/src/NativePolyIO.agda +++ b/src/NativePolyIO.agda @@ -7,9 +7,9 @@ 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 ℓ @@ -17,24 +17,22 @@ postulate _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 #-} diff --git a/src/SizedIO/Base.agda b/src/SizedIO/Base.agda index a6946b7..cc3ff2a 100644 --- a/src/SizedIO/Base.agda +++ b/src/SizedIO/Base.agda @@ -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 diff --git a/src/SizedIO/coIOIOObject.agda b/src/SizedIO/coIOIOObject.agda index 390a007..05041e1 100644 --- a/src/SizedIO/coIOIOObject.agda +++ b/src/SizedIO/coIOIOObject.agda @@ -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) 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)) diff --git a/src/SizedPolyIO/Base.agda b/src/SizedPolyIO/Base.agda index 6b6ab46..88b017c 100644 --- a/src/SizedPolyIO/Base.agda +++ b/src/SizedPolyIO/Base.agda @@ -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 _>>=_ _>>='_ _>>_ diff --git a/src/StateSizedIO/Base.agda b/src/StateSizedIO/Base.agda index d4539c7..2f41dbc 100644 --- a/src/StateSizedIO/Base.agda +++ b/src/StateSizedIO/Base.agda @@ -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 diff --git a/src/StateSizedIO/IOObject.agda b/src/StateSizedIO/IOObject.agda index 7e0f661..25f4168 100644 --- a/src/StateSizedIO/IOObject.agda +++ b/src/StateSizedIO/IOObject.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --guardedness #-} + module StateSizedIO.IOObject where open import Data.Product diff --git a/src/StateSizedIO/Object.agda b/src/StateSizedIO/Object.agda index 9a4aa66..011d62a 100644 --- a/src/StateSizedIO/Object.agda +++ b/src/StateSizedIO/Object.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --guardedness #-} + module StateSizedIO.Object where open import Data.Product diff --git a/src/UnSizedIO/Base.agda b/src/UnSizedIO/Base.agda index 456a07f..18bc33b 100644 --- a/src/UnSizedIO/Base.agda +++ b/src/UnSizedIO/Base.agda @@ -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 diff --git a/src/UnSizedIO/Console.agda b/src/UnSizedIO/Console.agda index 16914c3..6085254 100644 --- a/src/UnSizedIO/Console.agda +++ b/src/UnSizedIO/Console.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --guardedness #-} + module UnSizedIO.Console where open import NativeIO diff --git a/src/UnSizedIO/ConsoleObject.agda b/src/UnSizedIO/ConsoleObject.agda index e91282f..742cc72 100644 --- a/src/UnSizedIO/ConsoleObject.agda +++ b/src/UnSizedIO/ConsoleObject.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --guardedness #-} + module UnSizedIO.ConsoleObject where open import UnSizedIO.Console diff --git a/src/UnSizedIO/IOObject.agda b/src/UnSizedIO/IOObject.agda index 96ad0aa..aafc6b4 100644 --- a/src/UnSizedIO/IOObject.agda +++ b/src/UnSizedIO/IOObject.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --guardedness #-} + module UnSizedIO.IOObject where open import Data.Product diff --git a/src/UnSizedIO/Object.agda b/src/UnSizedIO/Object.agda index c5a9907..3e16b9e 100644 --- a/src/UnSizedIO/Object.agda +++ b/src/UnSizedIO/Object.agda @@ -2,7 +2,6 @@ module UnSizedIO.Object where open import Data.Product - record Interface : Set₁ where field Method : Set diff --git a/src/ooAgda.agda-lib b/src/ooAgda.agda-lib index 7522874..57b51a3 100644 --- a/src/ooAgda.agda-lib +++ b/src/ooAgda.agda-lib @@ -1,3 +1,5 @@ name: ooAgda depend: standard-library include: . ../examples +flags: + --sized-types