mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
76 lines
2.1 KiB
Agda
76 lines
2.1 KiB
Agda
|
{-# OPTIONS --guardedness #-}
|
|||
|
|
|
|||
|
|
-- Take this example as motivation:
|
|||
|
|
-- https://stackoverflow.com/questions/21808186/agda-reading-a-line-of-standard-input-as-a-string-instead-of-a-costring
|
|||
|
|
|
|||
|
|
open import Level
|
|||
|
|
open import Agda.Builtin.Coinduction
|
|||
|
|
module thesis.motivation where
|
|||
|
|
|
|||
|
|
module old-delay where
|
|||
|
|
private
|
|||
|
|
variable
|
|||
|
|
a : Level
|
|||
|
|
data _⊥ (A : Set a) : Set a where
|
|||
|
|
now : A → A ⊥
|
|||
|
|
later : ∞ (A ⊥) → A ⊥
|
|||
|
|
|
|||
|
|
never : ∀ {A : Set a} → A ⊥
|
|||
|
|
never = later (♯ never)
|
|||
|
|
|
|||
|
|
module ReverseInput where
|
|||
|
|
open import Data.Char
|
|||
|
|
open import Data.Nat
|
|||
|
|
open import Data.List using (List; []; _∷_)
|
|||
|
|
open import Data.String
|
|||
|
|
open import Data.Unit.Polymorphic
|
|||
|
|
open import Codata.Musical.Costring
|
|||
|
|
open import Codata.Musical.Colist using ([]; _∷_)
|
|||
|
|
-- open import IO using (IO; seq; bind; return; Main; run; putStrLn)
|
|||
|
|
open import IO.Primitive
|
|||
|
|
open import IO.Primitive.Infinite using (getContents)
|
|||
|
|
open import Agda.Builtin.IO using ()
|
|||
|
|
|
|||
|
|
open old-delay
|
|||
|
|
-- IDEA: start in haskell, then motivate in agda and define delay type
|
|||
|
|
-- next talk about bisimilarity.
|
|||
|
|
-- idea for slide title: dlrowolleh.hs and dlrowolleh.agda
|
|||
|
|
|
|||
|
|
private
|
|||
|
|
variable
|
|||
|
|
a : Level
|
|||
|
|
|
|||
|
|
-- reverse : Costring → String ⊥
|
|||
|
|
-- reverse = go []
|
|||
|
|
-- where
|
|||
|
|
-- go : List Char → Costring → String ⊥
|
|||
|
|
-- go acc [] = now (fromList acc)
|
|||
|
|
-- go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs))
|
|||
|
|
|
|||
|
|
-- putStrLn⊥ : String ⊥ → IO {a} ⊤
|
|||
|
|
-- putStrLn⊥ (now s) = putStrLn s
|
|||
|
|
-- putStrLn⊥ (later s) = seq (♯ return tt) (♯ putStrLn⊥ (♭ s))
|
|||
|
|
|
|||
|
|
-- main : Main
|
|||
|
|
-- main = run (bind (♯ {! getContents !}) {! !}) --(λ c → ♯ putStrLn⊥ (reverse c)))
|
|||
|
|
|
|||
|
|
-- NOTE: This is not very understandable... Better stick to the outdated syntax
|
|||
|
|
module delay where
|
|||
|
|
mutual
|
|||
|
|
data _⊥ (A : Set) : Set where
|
|||
|
|
now : A → A ⊥
|
|||
|
|
later : A ⊥' → A ⊥
|
|||
|
|
|
|||
|
|
record _⊥' (A : Set) : Set where
|
|||
|
|
coinductive
|
|||
|
|
field
|
|||
|
|
force : A ⊥
|
|||
|
|
open _⊥'
|
|||
|
|
|
|||
|
|
mutual
|
|||
|
|
never : ∀ {A : Set} → A ⊥
|
|||
|
|
never = later never'
|
|||
|
|
|
|||
|
|
never' : ∀ {A : Set} → A ⊥'
|
|||
|
|
force never' = never
|