Round trip experiment

src/Lang/2ADT.agda

@@ -19,3 +19,18 @@ Configuration F = F → Bool
 
 2ADTL : (V : 𝕍) → (F : 𝔽) → VariabilityLanguage V
 2ADTL V F = ⟪ 2ADT V F , Configuration F , ⟦_⟧ ⟫
+
+
+open import Data.String as String using (String; _++_; intersperse)
+open import Data.Product using (_,_)
+open import Show.Lines
+
+pretty : {A : 𝔸} → {V : 𝕍} → {F : 𝔽} → (V A → String) → (F → String) → 2ADT V F A → Lines
+pretty pretty-variant show-F (leaf v) = > pretty-variant v
+pretty pretty-variant show-F (D ⟨ l , r ⟩) = do
+  > show-F D ++ "⟨"
+  indent 2 do
+    pretty pretty-variant show-F l
+    > ","
+    pretty pretty-variant show-F r
+  > "⟩"

src/Lang/CCC.lagda.md

@@ -195,10 +195,24 @@ Maybe its smarter to do this for ADDs and then to conclude by transitivity of tr
 ## Show
 
 ```agda
+  open import Show.Lines hiding (map)
   open import Data.String as String using (String; _++_)
 
   show : ∀ {i} → (Dimension → String) → CCC Dimension i (String , String._≟_) → String
   show _ (a -< [] >-) = a
   show show-D (a -< es@(_ ∷ _) >- ) = a ++ "-<" ++ (foldl _++_ "" (map (show show-D) es)) ++ ">-"
   show show-D (D ⟨ es ⟩) = show-D D ++ "⟨" ++ (String.intersperse ", " (toList (map⁺ (show show-D) es))) ++ "⟩"
+
+  pretty : ∀ {i : Size} → (Dimension → String) → CCC Dimension i (String , String._≟_) → Lines
+  pretty show-D (a -< [] >-) = > a
+  pretty show-D (a -< es@(_ ∷ _) >-) = do
+    > a ++ "-<"
+    indent 2 do
+      lines (map (pretty show-D) es)
+    > ">-"
+  pretty show-D (D ⟨ cs ⟩) = do
+    > show-D D ++ "⟨"
+    indent 2 do
+      lines (map (pretty show-D) (toList cs))
+    > "⟩"
 ```

src/Lang/FST.agda

@@ -458,7 +458,7 @@ module Impose (AtomSet : 𝔸) where
   ⟦ r ◀ features ⟧ c = r -< forget-uniqueness (⊛-all (select c features)) >-
 
   open import Data.String using (String; _<+>_)
-  open import Show.Lines
+  open import Show.Lines hiding (map)
 
   module Show (show-F : F → String) (show-A : A → String) where
     mutual

src/Lang/VariantList.lagda.md

@@ -11,7 +11,7 @@ module Lang.VariantList (V : 𝕍) where
 
 ```agda
 open import Data.Fin using (Fin; zero; suc; toℕ)
-open import Data.List using ([]; _∷_)
+open import Data.List as List using ([]; _∷_)
 open import Data.List.NonEmpty using (List⁺; _∷_; toList; length)
 open import Data.Nat using (ℕ; zero; suc)
 open import Data.Product using (∃-syntax; _,_; proj₁; proj₂)
@@ -163,3 +163,17 @@ VariantList-is-Sound e =
   , (λ i → vl-conf i , refl)
   , (λ i → vl-fnoc i , sym (inverse i e))
 ```
+
+## Show
+
+```agda
+open import Data.String as String using (String; _++_; intersperse)
+open import Data.Product using (_,_)
+open import Show.Lines
+
+pretty : {A : 𝔸} → (V A → String) → VariantList A → Lines
+pretty {A} pretty-variant (v ∷ vs) = do
+  > "[ " ++ pretty-variant v
+  lines (List.map (λ v → > ", " ++ pretty-variant v) vs)
+  > "]"
+```

src/Main.agda

@@ -9,7 +9,7 @@ open import Data.List using (List; []; _∷_; map)
 open import Data.Product using (∃-syntax; Σ-syntax; _×_; _,_)
 open import Size using (∞)
 
-open import Show.Lines
+open import Show.Lines hiding (map)
 open import Show.Print
 
 open import Test.Example using (Example)
@@ -27,6 +27,7 @@ open import Test.Experiments.OC-to-2CC
 open import Translation.Experiments.Choice-to-2Choice-Experiment using (exp; all-ex)
 import Test.Experiments.FST-Experiments as FSTs
 open FSTs.Java.Calculator using (toy-calculator-experiment; ex-all)
+open import Test.Experiments.RoundTrip as RoundTrip using (round-trip)
 
 {-|
 A list of programs that we want to run.
@@ -40,8 +41,9 @@ experimentsToRun =
   -- Run some example translations of option calculus to binary choice calculus
   setup exp-oc-to-bcc optex-all ∷
   -- Run some example translations from n to binary choices
-  setup exp all-ex ∷
+  -- setup exp all-ex ∷
   setup toy-calculator-experiment ex-all ∷
+  setup round-trip RoundTrip.examples ∷
   []
 
 {-|

src/Show/Lines.agda

@@ -2,15 +2,18 @@ module Show.Lines where
 
 open import Data.Bool using (true; false; if_then_else_)
 open import Data.Nat using (ℕ; _*_; _∸_; ⌊_/2⌋; ⌈_/2⌉; _≤ᵇ_)
-open import Data.List using (List; _∷_; map; concat; splitAt)
+open import Data.List as List using (List; _∷_; [_]; concat; splitAt)
 open import Data.String using (String; _++_; _==_; replicate; fromChar; toList; fromList; Alignment; fromAlignment)
-open import Data.Product as Prod using (_,_)
+open import Data.Product as Prod using (_,_; proj₁; map₁)
+open import Data.Unit using (⊤; tt)
 open import Function using (id; _∘_)
 
+open import Algebra using (RawMonoid)
 open import Effect.Applicative using (RawApplicative)
+open import Effect.Functor using (RawFunctor)
 open import Effect.Monad using (RawMonad)
-open RawApplicative using (pure)
-open import Data.List.Effectful renaming (applicative to list-applicative; monad to list-monad)
+open import Effect.Monad.Writer as Writer using (RawMonadWriter; Writer; runWriter)
+open import Data.List.Effectful as List using () renaming (applicative to list-applicative; monad to list-monad)
 open import Level using (0ℓ)
 
 open import Util.List using (max)
@@ -35,20 +38,42 @@ length line = Data.String.length (content line)
 
 -- Lines monad.
 -- It captures a sequence of text lines which we aim to print.
--- Under the hood it is just a list of strings but with slightly different behaviour (see _>>_ below).
+Lines' : Set → Set
+Lines' = Writer (List.++-[]-rawMonoid Line)
+
 Lines : Set
-Lines = List Line
+Lines = Lines' (Level.Lift Level.zero ⊤)
+
+-- Export the composition operator to allow do-notation.
+open Writer using (functor; applicative; monad) public
+open RawMonad {f = 0ℓ} (monad {𝕎 = List.++-[]-rawMonoid Line}) using (_>>_; _>>=_) public
 
 -- print a single line
 single : Line → Lines
-single = pure list-applicative
+single line = tell [ line ]
+  where
+  open RawMonadWriter Writer.monadWriter
 
 -- add a sequence of lines to the output at once
 lines : List Lines → Lines
-lines = concat
+lines lines = Level.lift tt <$ sequenceA lines
+  where
+  open List.TraversableA applicative
+  open RawFunctor functor
+
+map-lines : {A : Set} → (List Line → List Line) → Lines' A → Lines' A
+map-lines f = writer ∘ map₁ f ∘ runWriter
+  where
+  open RawMonadWriter Writer.monadWriter
+
+map : {A : Set} → (Line → Line) → Lines' A → Lines' A
+map f = map-lines (List.map f)
+
+raw-lines : Lines → List Line
+raw-lines = proj₁ ∘ runWriter
 
 for-loop : ∀ {ℓ} {A : Set ℓ} → List A → (A → Lines) → Lines
-for-loop items op = lines (map op items)
+for-loop items op = lines (List.map op items)
 
 syntax for-loop items (λ c → l) = foreach [ c ∈ items ] l
 
@@ -58,11 +83,6 @@ align-all width = map (align width)
 overwrite-alignment-with : Alignment → Lines → Lines
 overwrite-alignment-with a = map (λ l → record l { alignment = a })
 
--- Export the composition operator to allow do-notation.
--- We do not rely on _>>_ of the list monad because it forgets the first argument and just keeps the second list. We thus would forget everything we wanted to print except for the last line.
-_>>_ : Lines → Lines → Lines
-_>>_ = Data.List._++_
-
 -- Some smart constructors
 
 [_]>_ : Alignment → String → Lines
@@ -74,7 +94,7 @@ infix 1 [_]>_
 infix 1 >_
 
 >∷_ : List String → Lines
->∷_ = lines ∘ map >_
+>∷_ = lines ∘ List.map >_
 infix 1 >∷_
 
 phantom : String → String
@@ -97,7 +117,7 @@ linebreak : Lines
 linebreak = > ""
 
 width : Lines → ℕ
-width = max ∘ map length
+width = max ∘ List.map length ∘ raw-lines
 
 -- Given a maximum length, this function wraps a given line as often as necessary to not exceed that width,
 -- This is not guaranteed to terminate because the list could be infinite.
@@ -112,9 +132,7 @@ wrap-at max-width line with (length line) ≤ᵇ max-width
 
 -- Wraps all lines at the given maximum width using wrap-at.
 wrap-all-at : ℕ → Lines → Lines
-wrap-all-at max-width lines =
-  let open RawMonad list-monad in
-  lines >>= wrap-at max-width
+wrap-all-at max-width ls = lines (List.map (wrap-at max-width) (raw-lines ls))
 
 -- Dr
 boxed : ℕ → (title : String) → (content : Lines) → Lines

src/Show/Print.agda

@@ -8,12 +8,12 @@ open import IO using (IO; putStrLn)
 open IO.List using (mapM′)
 open import Level using (0ℓ)
 
-open import Show.Lines using (Lines; align; content)
+open import Show.Lines using (Lines; align; content; raw-lines)
 
 open import Data.Nat.Show using (show)
 open import Data.List using (length)
 
 open import Function using (_∘_)
 
 print : ℕ → Lines → IO {0ℓ} ⊤
-print width = mapM′ (putStrLn ∘ content ∘ align width)
+print width = mapM′ (putStrLn ∘ content ∘ align width) ∘ raw-lines

src/Test/Examples/OC.agda

@@ -18,7 +18,7 @@ OCExample : Set
 OCExample = Example (WFOC String ∞ (String , String._≟_))
 
 optex-unary : OCExample
-optex-unary = "unary" ≔ (Root "r" [ opt "O" (oc-leaf "lol") ])
+optex-unary = "unary" ≔ (Root "r" [ opt "O" (oc-leaf "a") ])
 
 optex-lock : OCExample
 optex-lock = "lock" ≔ (Root "void f() {" (
@@ -30,10 +30,10 @@ optex-lock = "lock" ≔ (Root "void f() {" (
 
 optex-sandwich : OCExample
 optex-sandwich = "sandwich" ≔ (Root "Buns" (
-    "Tomato?" ❲ oc-leaf "Tomato" ❳
-  ∷ "Salad?"  ❲ oc-leaf "Salad"  ❳
-  ∷ "Cheese?" ❲ oc-leaf "Cheese" ❳
-  ∷ oc-leaf "Mayonnaise" -- we always put mayo on the sandwich
+    "Tomato?" ❲ oc-leaf "tomato" ❳
+  ∷ "Salad?"  ❲ oc-leaf "salad"  ❳
+  ∷ "Cheese?" ❲ oc-leaf "cheese" ❳
+  ∷ oc-leaf "Mayo" -- we always put mayo on these sandwiches
   ∷ []))
 
 optex-deep : OCExample

src/Test/Experiment.agda

@@ -6,7 +6,7 @@ open import Data.Product using (Σ-syntax; _×_; _,_)
 open import Data.String using (String; _++_; length; replicate)
 open import Level using (suc)
 
-open import Show.Lines
+open import Show.Lines hiding (map)
 
 open import Test.Example
 open import Util.Named

src/Test/Experiments/FST-Experiments.agda

@@ -17,7 +17,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 open import Util.Named
 open import Test.Example
 open import Test.Experiment
-open import Show.Lines
+open import Show.Lines hiding (map)
 open import Util.ShowHelpers
 open import Data.String using (String; _<+>_; _++_) renaming (_≟_ to _≟ˢ_)