Integrate indifferent elimination into the ADT-to-TikZ experiment

VariantSync · Sep 26, 2024 · 06f55e3 · 06f55e3
1 parent 36ac3a3
commit 06f55e3
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/Vatras/Test/Experiments/ADT-to-TikZ-Forest.agda b/src/Vatras/Test/Experiments/ADT-to-TikZ-Forest.agda
@@ -13,6 +13,7 @@ open import Vatras.Lang.CCC as CCC using (CCC)
 open import Vatras.Lang.2CC using (2CC)
 open import Vatras.Lang.ADT
 open import Vatras.Translation.LanguageMap
+open import Vatras.Translation.Lang.2CC.Indifferent String String._≟_ using (eliminate-indifferent)
 
 open import Vatras.Test.Experiment
 open import Vatras.Show.Lines
@@ -50,8 +51,11 @@ CCC-to-ADT ccc = adt
     bcc : STR2CC
     bcc = proj₁ (2CC≽CCC ccc)
 
+    bcc' : STR2CC
+    bcc' = eliminate-indifferent bcc
+
     adt : STRADT
-    adt = proj₁ (ADT≽2CC bcc)
+    adt = proj₁ (ADT≽2CC bcc')
 
 tikz-export-experiment : Experiment STRCCC
 getName tikz-export-experiment = "Tikz-Export"