11module Generic.Semantics.Printing where
22
3- open import Coinduction
3+ open import Codata.Thunk
4+ open import Codata.Stream as Stream using (Stream; _∷_)
5+
46open import Data.Unit
57open import Data.Bool
68open import Data.Product
79open import Data.Nat.Base
810open import Data.Nat.Show as Nat
9- open import Data.List.Base as L hiding ([_] ; _++_ ; lookup)
11+ open import Data.List.Base using (List; []; _∷_)
12+ open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
1013open import Data.Char
1114open import Data.String using (String ; _++_ ; fromList ; toList)
12- open import Data.Stream as Str hiding (_++_ ; lookup)
1315open import Category.Monad
1416open import Category.Monad.State
1517open import Function
1618
1719
1820-- The Printing Monad we are working with: a state containing a stream
1921-- of *distinct* Strings.
20- open module ST = RawMonadState (StateMonadState (Stream String))
21- M = State (Stream String)
22+ open module ST = RawMonadState (StateMonadState (Stream String _ ))
23+ M = State (Stream String _ )
2224
2325open import var hiding (get)
2426open import environment as E
@@ -45,15 +47,15 @@ module _ {I : Set} where
4547module _ {I : Set } where
4648
4749 fresh : {i : I} {Γ : List I} → M (Name i Γ)
48- fresh = get >>= λ nms →
49- put (tail nms) >>= λ _ →
50- return $ mkN $ head nms
50+ fresh = get >>= λ nms →
51+ put (Stream. tail nms) >>= λ _ →
52+ return $ mkN $ Stream. head nms
5153
5254-- Names are varlike in the monad M: we use the state to generate fresh
5355-- ones. Closure under thinning is a matter of wrapping / unwrapping the
5456-- name.
5557
56- vl^StName : VarLike (λ i Γ → State (Stream String) (Name i Γ))
58+ vl^StName : VarLike (λ i Γ → M (Name i Γ))
5759 new vl^StName = fresh
5860 th^𝓥 vl^StName = λ st _ → mkN ∘ getN ST.<$> st
5961
@@ -104,23 +106,16 @@ module _ {I : Set} {d : Desc I} where
104106 print : Display d → {i : I} → TM d i → String
105107 print dis t = proj₁ $ getP (Sem.closed (printing dis) t) names where
106108
107- flatten : {A : Set } → Stream (A × List A) → Stream A
108- flatten ((a , as) Str.∷ aass) = go a as (♭ aass) where
109- go : {A : Set } → A → List A → Stream (A × List A) → Stream A
110- go a [] aass = a ∷ ♯ flatten aass
111- go a (b ∷ as) aass = a ∷ ♯ go b as aass
112-
113- names : Stream String
114- names = flatten $ Str.zipWith cons letters
115- $ "" ∷ ♯ Str.map Nat.show (allNatsFrom 0 )
116- where
117-
118- cons : (Char × List Char) → String → (String × List String)
119- cons (c , cs) suffix = appendSuffix c , L.map appendSuffix cs where
120- appendSuffix : Char → String
121- appendSuffix c = fromList (c ∷ []) ++ suffix
109+ alphabetWithSuffix : String → List⁺ String
110+ alphabetWithSuffix suffix = List⁺.map (λ c → fromList (c ∷ []) ++ suffix)
111+ $′ 'a' ∷ toList "bcdefghijklmnopqrstuvwxyz"
122112
123- letters = Str.repeat $ 'a' , toList "bcdefghijklmnopqrstuvwxyz"
113+ allNats : Stream ℕ _
114+ allNats = cofix (λ i → ℕ → Stream ℕ i) step 0 where
115+ step : ∀ {i} → Thunk _ i → ℕ → Stream ℕ i
116+ step rec k = k ∷ λ where .force → rec .force (suc k)
124117
125- allNatsFrom : ℕ → Stream ℕ
126- allNatsFrom k = k ∷ ♯ allNatsFrom (1 + k)
118+ names : Stream String _
119+ names = Stream.concat
120+ $′ Stream.map alphabetWithSuffix
121+ $′ "" ∷ λ where .force → Stream.map Nat.show allNats
0 commit comments