Fix dc example

.github/workflows/ci.yml

@@ -63,6 +63,7 @@ jobs:
         run: |
           lake -R exe cache get # download cache of mathlib docs.
           lake -R build SSA.Projects.CIRCT.DC # compile and check CIRCT's DC Dialect
+          lake -R build SSA.Projects.CIRCT.DCExample # test CIRCT's DC Dialect
 
       - uses: actions/github-script@v6
         if: github.event_name == 'pull_request'

SSA/Projects/CIRCT/DC.lean

@@ -208,7 +208,6 @@ def mkTy2 : String → MLIR.AST.ExceptM (DC) Ty2
   | "Bool" => return (.bool)
   | _ => throw .unsupportedType
 
-
 def mkTy : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM DC DC.Ty
   | MLIR.AST.MLIRType.undefined s => do
     match s.splitOn "_" with

SSA/Projects/CIRCT/DCExample.lean

@@ -3,24 +3,22 @@ import SSA.Core.MLIRSyntax.GenericParser
 import SSA.Projects.CIRCT.DC
 import SSA.Projects.CIRCT.DC.Stream
 
-
-
 /-!
 ## Examples
 -/
 namespace DC
 namespace Examples
 
+unseal String.splitOnAux in
 def BranchEg1 := [dc_com| {
-  ^entry(%0: !Stream_Bool, %1: !Stream_Bool):
-    %out = "dc.branch" (%0, %1) : (!Stream_Bool, !Stream_Bool) -> (!Stream2_Bool)
-    %0 = "dc.fst" (%out) : (!Stream2_Bool) -> (!Stream_Bool)
-    %outs = "dc.snd" (%out) : (!Stream2_Bool) -> (!Stream_Bool)
-    %out2 = "dc.merge" (%outf, %outs) : (!Stream_Bool, !Stream_Bool) -> (!Stream_Bool)
-    "return" (%out) : (!Stream_Bool) -> ()
+  ^entry(%0: !Stream_Int, %1: !Stream_Bool):
+    %out = "dc.branch" (%0, %1) : (!Stream_Int, !Stream_Bool) -> (!Stream2_Int)
+    %outf = "dc.fst" (%out) : (!Stream2_Int) -> (!Stream_Int)
+    %outs = "dc.snd" (%out) : (!Stream2_Int) -> (!Stream_Int)
+    %out2 = "dc.merge" (%outs, %outf) : (!Stream_Int, !Stream_Int) -> (!Stream_Int)
+    "return" (%out2) : (!Stream_Int) -> ()
   }]
 
-
 #check BranchEg1
 #eval BranchEg1
 #reduce BranchEg1
@@ -30,16 +28,15 @@ def BranchEg1 := [dc_com| {
 def ofList (vals : List (Option α)) : Stream α :=
   fun i => (vals.get? i).join
 
-def x : Stream Bool := ofList [some true, none, some false, some true, some false]
-def c : Stream Bool := ofList [some true, some false, none, some true]
+def c : Stream Bool := ofList [some true, none, some false, some true, some false]
+def x : Stream Int := ofList [some 1, some 2, none, some 3]
 
-def test : Stream Bool :=
-  BranchEg1.denote (Valuation.ofPair c x)
+def test : Stream Int :=
+  BranchEg1.denote (Ctxt.Valuation.ofPair c x)
 
 def remNone (lst : List (Option Bool)) : List (Option Bool) :=
   lst.filter (fun | some x => true
                   | none => false)
 
-
 end Examples
 end DC