From 393b34a8888ef227d4e816444879da9b0751b9ce Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 01:24:22 +0200 Subject: [PATCH 1/8] Generalize `Lines` to a `Writer` monad This gives the flexibility of computing (e.g. translating expressions) while, at the same time, also outputting more lines. --- src/Lang/FST.agda | 2 +- src/Main.agda | 2 +- src/Show/Lines.agda | 56 +++++++++++++++-------- src/Show/Print.agda | 4 +- src/Test/Experiment.agda | 2 +- src/Test/Experiments/FST-Experiments.agda | 2 +- 6 files changed, 43 insertions(+), 25 deletions(-) diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index a75925df..d8474e99 100644 --- a/src/Lang/FST.agda +++ b/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 diff --git a/src/Main.agda b/src/Main.agda index 5ea4b6fb..6bfb17c1 100644 --- a/src/Main.agda +++ b/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) diff --git a/src/Show/Lines.agda b/src/Show/Lines.agda index 087a092b..feb2c7ed 100644 --- a/src/Show/Lines.agda +++ b/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 diff --git a/src/Show/Print.agda b/src/Show/Print.agda index bfca6f52..89a86e4f 100644 --- a/src/Show/Print.agda +++ b/src/Show/Print.agda @@ -8,7 +8,7 @@ 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) @@ -16,4 +16,4 @@ 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 diff --git a/src/Test/Experiment.agda b/src/Test/Experiment.agda index 6c237dd4..e9ef8b85 100644 --- a/src/Test/Experiment.agda +++ b/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 diff --git a/src/Test/Experiments/FST-Experiments.agda b/src/Test/Experiments/FST-Experiments.agda index 285acb56..673173ae 100644 --- a/src/Test/Experiments/FST-Experiments.agda +++ b/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 _β‰ŸΛ’_) From d9de67e79287b7bd85663fcdf94645a9faa68040 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 02:27:24 +0200 Subject: [PATCH 2/8] Implement 2ADT pretty printing --- src/Lang/2ADT.agda | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Lang/2ADT.agda b/src/Lang/2ADT.agda index 7a28a841..3ec41c0c 100644 --- a/src/Lang/2ADT.agda +++ b/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 + > "⟩" From e713aa605f7b73d7de293fcde9977957e2142021 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 02:27:41 +0200 Subject: [PATCH 3/8] Implement VariantList pretty printing --- src/Lang/VariantList.lagda.md | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/Lang/VariantList.lagda.md b/src/Lang/VariantList.lagda.md index de404732..6ccddfd5 100644 --- a/src/Lang/VariantList.lagda.md +++ b/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) + > "]" +``` From 3d7f85469b10e26f928689f993e464a1972c590d Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 02:34:52 +0200 Subject: [PATCH 4/8] Implement CCC pretty printing --- src/Lang/CCC.lagda.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Lang/CCC.lagda.md b/src/Lang/CCC.lagda.md index 4e554a81..9efc5a83 100644 --- a/src/Lang/CCC.lagda.md +++ b/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)) + > "⟩" ``` From 5f46e8181f31b9e942c7e2150172ead4b8ac25c3 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 02:28:01 +0200 Subject: [PATCH 5/8] Create a round trip experiment --- src/Main.agda | 2 + src/Test/Experiments/RoundTrip.agda | 126 ++++++++++++++++++++++++++++ 2 files changed, 128 insertions(+) create mode 100644 src/Test/Experiments/RoundTrip.agda diff --git a/src/Main.agda b/src/Main.agda index 6bfb17c1..4b23f357 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -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. @@ -42,6 +43,7 @@ experimentsToRun = -- Run some example translations from n to binary choices setup exp all-ex ∷ setup toy-calculator-experiment ex-all ∷ + setup round-trip RoundTrip.examples ∷ [] {-| diff --git a/src/Test/Experiments/RoundTrip.agda b/src/Test/Experiments/RoundTrip.agda new file mode 100644 index 00000000..070aa21a --- /dev/null +++ b/src/Test/Experiments/RoundTrip.agda @@ -0,0 +1,126 @@ +{-# OPTIONS --sized-types #-} + +module Test.Experiments.RoundTrip where + +open import Data.Bool using (Bool; true; false) +import Data.Fin as Fin +open import Data.List using (List; _∷_; []) +open import Data.List.NonEmpty using (_∷_) +open import Data.Nat using (_+_) +open import Data.Product using (_,_; proj₁; projβ‚‚; mapβ‚‚) +open import Data.String as String using (String; _++_; unlines; _==_) +open import Effect.Applicative using (RawApplicative) + +open import Size using (Size; ∞) +open import Function using (id; _∘_) +open import Level using (0β„“) + +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≑_; refl) + +open import Framework.Compiler using (LanguageCompiler) +open import Framework.Definitions using (β„‚; 𝔸) +open import Framework.Variants using (Rose; Artifactβˆˆβ‚›Rose; show-rose) +open import Framework.VariabilityLanguage using (VariabilityLanguage; Expression) +open import Util.AuxProofs using (decidableEquality-Γ—) +open import Util.Nat.AtLeast using (β„•β‰₯) +import Util.String as String + +open import Lang.All +open import Translation.LanguageMap +import Translation.Lang.CCC-to-NCC +module CCC-to-NCC = Translation.Lang.CCC-to-NCC.Exact Variant mkArtifact +import Translation.Lang.NCC-to-2CC +open Translation.Lang.NCC-to-2CC.2Ary Variant mkArtifact using () renaming (NCCβ†’2CC to NCC-2β†’2CC) + +open import Show.Lines +open import Util.Named +open import Show.Eval + +open import Test.Experiment +open import Test.Example +open import Test.Examples.OC + +Feature = String +Artifact : 𝔸 +Artifact = String , String._β‰Ÿ_ + +open CCC-to-NCC using (⌈_βŒ‰; numberOfAlternativesβ‰€βŒˆ_βŒ‰) + +CCCβ†’NCC-Exact : (e : CCC.CCC Feature ∞ Artifact) β†’ NCC.NCC ⌈ e βŒ‰ Feature ∞ Artifact +CCCβ†’NCC-Exact e = CCC-to-NCC.translate ⌈ e βŒ‰ e (numberOfAlternativesβ‰€βŒˆ_βŒ‰ e) + + +translate : {E₁ : Set} β†’ {Eβ‚‚ : E₁ β†’ Set} β†’ (e : E₁) β†’ String β†’ ((e : E₁) β†’ Eβ‚‚ e) β†’ (Eβ‚‚ e β†’ Lines) β†’ Lines' (Eβ‚‚ e) +translate e Eβ‚‚-name translator show = do + linebreak + [ Center ]> "β”‚" + [ Center ]> " β”‚ translate" + [ Center ]> "↓" + linebreak + let e' = translator e + pretty-e' = show e' + [ Center ]> Eβ‚‚-name + overwrite-alignment-with Center + (boxed (6 + width pretty-e') "" pretty-e') + [ Center ]> "proven to have the same semantics as the previous expression" + pure e' + where + open RawApplicative applicative + +compile : βˆ€ {VL₁ VLβ‚‚ : VariabilityLanguage Variant} + β†’ Expression VL₁ Artifact + β†’ String + β†’ LanguageCompiler VL₁ VLβ‚‚ + β†’ (Expression VLβ‚‚ Artifact β†’ Lines) + β†’ Lines' (Expression VLβ‚‚ Artifact) +compile e VLβ‚‚-name compiler show = translate e VLβ‚‚-name (LanguageCompiler.compile compiler) show + +round-trip : Experiment (CCC.CCC Feature ∞ (String , String._β‰Ÿ_)) +getName round-trip = "Translate CCC in one round-trip into equally expressive variability languages" +get round-trip ex@(name ≔ ccc) = do + [ Center ]> "CCC, original expression" + let pretty-ccc = CCC.pretty id ccc + overwrite-alignment-with Center + (boxed (6 + width pretty-ccc) "" pretty-ccc) + + ncc ← translate ccc "NCC" CCCβ†’NCC-Exact (NCC.Pretty.pretty id) + ncc2 ← compile ncc "NCC" (shrinkTo2Compiler ⌈ ccc βŒ‰) (NCC.Pretty.pretty (String.diagonal-β„• ∘ mapβ‚‚ Fin.toβ„•)) + 2cc ← compile ncc2 "2CC" NCC-2β†’2CC (2CC.Pretty.pretty (String.diagonal-β„• ∘ mapβ‚‚ Fin.toβ„•)) + 2adt ← compile 2cc "2ADT" 2CCβ†’2ADT (2ADT.pretty (show-rose id) (String.diagonal-β„• ∘ mapβ‚‚ Fin.toβ„•)) + variantList ← compile 2adt "VariantList" (2ADTβ†’VariantList (decidableEquality-Γ— String._β‰Ÿ_ Fin._β‰Ÿ_)) (VariantList.pretty (show-rose id)) + ccc' ← compile variantList "CCC" (VariantListβ†’CCC "default feature") (CCC.pretty id) + linebreak + + +open CCC using (_⟨_⟩; _-<_>-) + +ex-trivial : Example (CCC.CCC Feature ∞ Artifact) +ex-trivial = "trivial" ≔ "f1" ⟨ "a1" -< [] >- ∷ "a2" -< [] >- ∷ [] ⟩ + +ex-sandwich : Example (CCC.CCC Feature ∞ Artifact) +ex-sandwich = "sandwich" ≔ + "bread" + -< "salad?" + ⟨ "salad" -< [] >- + ∷ "no salad" -< [] >- + ∷ [] + ⟩ + ∷ "cheese" -< [] >- + ∷ "patty?" + ⟨ "meat" -< [] >- + ∷ "tofu" -< [] >- + ∷ [] + ⟩ + ∷ "sauce?" + ⟨ "no souce" -< [] >- + ∷ "mayonnaise" -< [] >- + ∷ "ketchup" -< [] >- + ∷ "mayonnaise and ketchup" -< [] >- + ∷ [] + ⟩ + ∷ [] + >- + +examples : List (Example (CCC.CCC Feature ∞ Artifact)) +examples = ex-trivial ∷ ex-sandwich ∷ [] From 86b4801f6fd3bd57f5c2e72a547e75dc7a2de05a Mon Sep 17 00:00:00 2001 From: pmbittner Date: Sat, 6 Apr 2024 08:51:47 +0200 Subject: [PATCH 6/8] update names to fit to paper --- src/Test/Experiments/RoundTrip.agda | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Test/Experiments/RoundTrip.agda b/src/Test/Experiments/RoundTrip.agda index 070aa21a..90fae295 100644 --- a/src/Test/Experiments/RoundTrip.agda +++ b/src/Test/Experiments/RoundTrip.agda @@ -96,27 +96,27 @@ get round-trip ex@(name ≔ ccc) = do open CCC using (_⟨_⟩; _-<_>-) ex-trivial : Example (CCC.CCC Feature ∞ Artifact) -ex-trivial = "trivial" ≔ "f1" ⟨ "a1" -< [] >- ∷ "a2" -< [] >- ∷ [] ⟩ +ex-trivial = "trivial" ≔ "D" ⟨ "l" -< [] >- ∷ "r" -< [] >- ∷ [] ⟩ ex-sandwich : Example (CCC.CCC Feature ∞ Artifact) -ex-sandwich = "sandwich" ≔ - "bread" - -< "salad?" +ex-sandwich = "Sandwich Recipe" ≔ + "Bread" + -< "Salad?" ⟨ "salad" -< [] >- - ∷ "no salad" -< [] >- + ∷ "Ξ΅" -< [] >- ∷ [] ⟩ ∷ "cheese" -< [] >- - ∷ "patty?" + ∷ "Patty?" ⟨ "meat" -< [] >- ∷ "tofu" -< [] >- ∷ [] ⟩ - ∷ "sauce?" - ⟨ "no souce" -< [] >- - ∷ "mayonnaise" -< [] >- + ∷ "Sauce?" + ⟨ "Ξ΅" -< [] >- + ∷ "mayo" -< [] >- ∷ "ketchup" -< [] >- - ∷ "mayonnaise and ketchup" -< [] >- + ∷ "mayo+ketchup" -< [] >- ∷ [] ⟩ ∷ [] From af6f92eb1636377a6a0697ed40a4106ff8bb75a8 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Sat, 6 Apr 2024 08:52:00 +0200 Subject: [PATCH 7/8] consistency name fixes --- src/Test/Examples/OC.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Test/Examples/OC.agda b/src/Test/Examples/OC.agda index 1adf171a..52cf71a0 100644 --- a/src/Test/Examples/OC.agda +++ b/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 From 4f5ee06ce0fbff216cba09b120a2f8274e6c6aaa Mon Sep 17 00:00:00 2001 From: pmbittner Date: Sat, 6 Apr 2024 08:52:08 +0200 Subject: [PATCH 8/8] disable redundant CCC experiments for now --- src/Main.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Main.agda b/src/Main.agda index 4b23f357..93d8ba79 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -41,7 +41,7 @@ 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 ∷ []