Merge remote-tracking branch 'origin/main' into new/fanout

brat/Brat/Checker.hs

@@ -548,7 +548,7 @@ check' FanIn (overs, ((tgt, ty):unders)) = do
     wire (over, elTy, hungryHead)
     wire (danglingResult, binderToValue ?my ty, hungry)
     faninNodes my (n - 1) (hungryTail, tailTy) elTy overs
-
+check' Identity ((this:leftovers), ()) = pure (((), [this]), (leftovers, ()))
 check' tm _ = error $ "check' " ++ show tm
 
 

brat/Brat/Elaborator.hs

@@ -181,6 +181,7 @@ elaborate' (FAnnotation a ts) = do
 elaborate' (FInto a b) = elaborate' (FApp b a)
 elaborate' (FFn cty) = pure $ SomeRaw' (RFn cty)
 elaborate' (FKernel sty) = pure $ SomeRaw' (RKernel sty)
+elaborate' FIdentity = pure $ SomeRaw' RIdentity
 -- We catch underscores in the top-level elaborate so this case
 -- should never be triggered
 elaborate' FUnderscore = Left (dumbErr (InternalError "Unexpected '_'"))

brat/Brat/Parser.hs

@@ -503,6 +503,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr]
               <|> try (match DotDot $> FPass)
               <|> var
               <|> match Underscore $> FUnderscore
+              <|> match Pipe $> FIdentity
 
 
 cnoun :: Parser Flat -> Parser (WC (Raw 'Chk 'Noun))

brat/Brat/Syntax/Concrete.hs

@@ -45,4 +45,5 @@ data Flat
  | FPass
  | FFanOut
  | FFanIn
+ | FIdentity
  deriving Show

brat/Brat/Syntax/Core.hs

@@ -48,6 +48,7 @@ data Term :: Dir -> Kind -> Type where
   Forget   :: WC (Term d KVerb) -> Term d UVerb
   Pull     :: [PortName] -> WC (Term Chk k) -> Term Chk k
   Var      :: UserName -> Term Syn Noun  -- Look up in noun (value) env
+  Identity :: Term Syn UVerb
   Arith    :: ArithOp -> WC (Term Chk Noun) -> WC (Term Chk Noun) -> Term Chk Noun
   -- Type annotations (annotating a term with its outputs)
   (:::)    :: WC (Term Chk Noun) -> [Output] -> Term Syn Noun
@@ -108,6 +109,7 @@ instance Show (Term d k) where
     showList ps = concatMap (++":") ps
 
   show (Var x) = show x
+  show Identity = "|"
   -- Nested applications should be bracketed too, hence 4 instead of 3
   show (fun :$: arg) = bracket PApp fun ++ ('(' : show arg ++ ")")
   show (tm ::: ty) = bracket PAnn tm ++ " :: " ++ show ty

brat/Brat/Syntax/Raw.hs

@@ -70,6 +70,7 @@ data Raw :: Dir -> Kind -> Type where
   RForget   :: WC (Raw d KVerb) -> Raw d UVerb
   RPull     :: [PortName] -> WC (Raw Chk k) -> Raw Chk k
   RVar      :: UserName -> Raw Syn Noun
+  RIdentity :: Raw Syn UVerb
   RArith    :: ArithOp -> WC (Raw Chk Noun) -> WC (Raw Chk Noun) -> Raw Chk Noun
   (:::::)   :: WC (Raw Chk Noun) -> [RawIO] -> Raw Syn Noun
   (::-::)   :: WC (Raw Syn k) -> WC (Raw d UVerb) -> Raw d k -- vertical juxtaposition (diagrammatic composition)
@@ -112,6 +113,7 @@ instance Show (Raw d k) where
   show (RPull [] x) = "[]:" ++ show x
   show (RPull ps x) = concat ((++":") <$> ps) ++ show x
   show (RVar x) = show x
+  show RIdentity = "|"
   show (RArith op a b) = "(" ++ show op ++ " " ++ show a ++ " " ++ show b ++ ")"
   show (fun ::$:: arg) = show fun ++ ('(' : show arg ++ ")")
   show (tm ::::: ty) = show tm ++ " :: " ++ show ty
@@ -227,6 +229,7 @@ instance (Kindable k) => Desugarable (Raw d k) where
   desugar' (RForget kv) = Forget <$> desugar kv
   desugar' (RPull ps raw) = Pull ps <$> desugar raw
   desugar' (RVar name) = pure $ Var name
+  desugar' RIdentity = pure Identity
   desugar' (RArith op a b) = Arith op <$> desugar a <*> desugar b
   desugar' (fun ::$:: arg) = (:$:) <$> desugar fun <*> desugar arg
   desugar' (tm ::::: outputs) = do

brat/examples/adder.brat

@@ -7,16 +7,13 @@ and(Bool, Bool) -> Bool
 and(true, b) = b
 and(false, b) = false
 
-id(Bool) -> Bool
-id(b) = b
-
 halfAdder(Bool, Bool) -> twos :: Bool, ones :: Bool
 halfAdder(a, b) = and(a,b), xor(a,b)
 
 fullAdder(Bool, Bool, Bool) -> twos :: Bool, ones :: Bool
-fullAdder = halfAdder, id;
-            id, halfAdder;
-            xor, id
+fullAdder = halfAdder, |;
+            |, halfAdder;
+            xor, |
 
 adder(n :: #, Vec(Bool, n), Vec(Bool, n), carryIn :: Bool) -> carryOut :: Bool, Vec(Bool, n)
 adder(0, [], [], b) = b, []

brat/examples/bell.brat

@@ -56,7 +56,7 @@ idq = { q => q }
 
 phasedBell :: { (th :: Float) -> { c :: Qubit, d :: Qubit -o c :: Bit, d :: Bit } }
 phasedBell(th) = {
-  H,qid;
-  Rz(th),qid;
+  H,|;
+  Rz(th),|;
   M,M
 }

brat/examples/compjuxt.brat

@@ -1,7 +1,5 @@
 ext "" f :: { Nat -> Int }
 ext "" g :: { Int -> Nat }
-ext "" idi :: { Int -> Int }
-ext "" idn(Nat) -> Nat
 ext "" addn(Nat, Nat) -> Nat
 
 id2 :: { Nat, Nat -> Nat, Nat }
@@ -21,9 +19,9 @@ id2b = { f,g; (g,f) }
 id2c :: { Nat, Int -> Nat, Int }
 id2c = { (f,g); (g,f) }
 
--- Note brackets here; without them, would be parsed as (idi(), f()); (g(), idn())
+-- Note brackets here; without them, would be parsed as (|, f()); (g(), |)
 mixture :: { Int, Nat, Nat -> Int, Nat, Nat }
-mixture = { idi, (f; g), idn }
+mixture = { |, (f; g), | }
 
 
 swap :: { a :: Nat, b :: Nat -> b :: Nat, a :: Nat }
@@ -36,30 +34,29 @@ funky_application = { x, y => x, y |> addn }
 funky_application' :: { a :: Nat, b :: Nat -> Nat }
 funky_application' = x, y => x, y |> addn
 
-
 int :: { -> Int }
-int = { => idi(1) }
+int = { => |(1 :: Int) }
 int' :: Int
-int' = idi(1)
+int' = |(1 :: Int)
 
 port_pull(Nat) -> n :: Nat, i :: Int
-port_pull = { x => i:(x, x |> f, idn) }
+port_pull = { x => i:(x, x |> f, |) }
 port_pull' :: { Nat -> nat :: Nat, int :: Int }
-port_pull' = x => int:(x, x |> f, idn)
+port_pull' = x => int:(x, x |> f, |)
 
 
 addi(Int, Int) -> Nat
 addi = { g, g; addn }
 
 
 juxt_in_comp2 :: { Nat, Nat, Int -> Int, Nat, Int}
-juxt_in_comp2 = { f,f,idi ; idi,g,idi }
+juxt_in_comp2 = { f,f,| ; |,g,| }
 
 sverb_cverb :: { Int -> Nat }
-sverb_cverb = { idi; (z => 4) }
+sverb_cverb = { |; (z => 4) }
 
 sverb_sverb_cverb :: { Int -> Nat }
-sverb_sverb_cverb = { idi; idi; (z => 4) }
+sverb_sverb_cverb = { |; |; (z => 4) }
 
 num_lit :: { -> Nat, Nat }
 num_lit = { => (1, 2) |> id2 }

brat/examples/cqcconf.brat

@@ -23,6 +23,6 @@ main = add((add,add)(unpack_vec(vec)))
 
 main2 :: { Qubit, Qubit -o Bit, Bit }
 main2 =
- lib.kernel.H,lib.kernel.qid;
+ lib.kernel.H,|;
  lib.kernel.CZ;
  lib.kernel.M,lib.kernel.M

brat/examples/ising.brat

@@ -1,4 +1,4 @@
-open import lib.kernel (Rx, qid, recons, uncons, vid)
+open import lib.kernel (Rx, recons, uncons)
 
 ext "" ZZ(Float) -> { Qubit, Qubit -o Qubit, Qubit }
 
@@ -10,6 +10,6 @@ nn_ising(succ(succ(n)), x, y) = { qs => qs |>
   uncons(succ(n));
   Rx(x), uncons(n);
   ZZ(y), ..;
-  qid, (recons(n); nn_ising(succ(n), x, y));
+  |, (recons(n); nn_ising(succ(n), x, y));
   recons(succ(n))
 }

brat/examples/kernel.brat

@@ -10,9 +10,7 @@ Rz(th :: Float)-> {a::Qubit -o b::Qubit}
 Rz = ?rz
 
 pba(Float)-> {c :: Qubit,d::Qubit -o c::Qubit,d::Qubit}
-pba = th => { x, y => (lib.kernel.H, lib.kernel.qid)(x, y) }
+pba = th => { x, y => (lib.kernel.H, |)(x, y) }
 
 th :: {Bool -> Bool}
 th = ?th
-
-

brat/examples/lib/kernel.brat

@@ -21,23 +21,11 @@ ext "tket.M" M :: { Qubit -o Bit }
 ext "builtin.measure" measure :: { Qubit -o q::Money, b::Bit }
 ext "builtin.fresh" fresh :: { Money -o Qubit }
 
-bid :: { Bit -o Bit }
-bid = { b => b }
-
-qid :: { Qubit -o Qubit }
-qid = { q => q }
-
-mid :: { Money -o Money }
-mid = { m => m }
-
 uncons(n :: #) -> { Vec(Qubit, succ(n)) -o Qubit, Vec(Qubit, n) }
 uncons(_) = { cons(q, qs) => q, qs }
 
 recons(n :: #) -> { Qubit, Vec(Qubit, n) -o Vec(Qubit, succ(n)) }
 recons(_) = { q, qs => cons(q, qs) }
 
-vid(n :: #) -> { Vec(Qubit, n) -o Vec(Qubit, n) }
-vid(_) = { qs => qs }
-
 swap(Qubit, Qubit) -o Qubit, Qubit
 swap(a, b) = b, a

brat/examples/pass.brat

@@ -1,11 +1,9 @@
-open import lib.kernel (qid)
-
 -- All of the lines of this function are the identity
 three_qubit(Qubit, Qubit, Qubit) -o Qubit, Qubit, Qubit
 three_qubit = {
   ..; -- Consumes all output
-  qid, ..; -- Consumes the remainder of the input
-  qid, qid, ..
+  |, ..; -- Consumes the remainder of the input
+  |, |, ..
 }
 
 apply_gate_twice({ Qubit, Qubit -o Qubit, Qubit }) -> { Qubit, Qubit -o Qubit, Qubit }

brat/examples/qft.brat

@@ -10,12 +10,12 @@ entangle(n :: #, Nat)
            Qubit, Vec(Qubit, n) }
 entangle(zero, _) = { q, qs => q, qs }
 entangle(succ(n), x) = {
-    qid, uncons(n);
-    CRx(2.0 * pi / 2.0 ^ to_float(x)), vid(n);
-    swap, vid(n);
-    qid, entangle(n, x + 1);
-    swap, vid(n);
-    qid, recons(n)
+    |, uncons(n);
+    CRx(2.0 * pi / 2.0 ^ to_float(x)), |;
+    swap, |;
+    |, entangle(n, x + 1);
+    swap, |;
+    |, recons(n)
 }
 
 qft(n :: #) ->
@@ -24,8 +24,8 @@ qft(n :: #) ->
 qft(zero) = { [] => [] }
 qft(succ(n)) = {
     uncons(n);
-    H, vid(n);
+    H, |;
     entangle(n, 2);
-    qid, qft(n);
+    |, qft(n);
     recons(n)
 }

brat/examples/teleportation.brat

@@ -20,7 +20,7 @@ packCash(m, m') = [m, m']
 
 bell00 :: { Qubit, Qubit -o Qubit, Qubit }
 bell00 = {
- lib.kernel.H, lib.kernel.qid;
+ lib.kernel.H, |;
  lib.kernel.CX
 }
 
@@ -33,9 +33,9 @@ alice'(a, q) = let (a, q) = lib.kernel.CX(a, q) in
 alice :: { Qubit, Qubit -o Bit, Bit, Vec(Money, 2) }
 alice = {
  lib.kernel.CX;
- lib.kernel.qid, lib.kernel.H;
+ |, lib.kernel.H;
  measure2;
- lib.kernel.bid,lib.kernel.bid,packCash
+ |,|,packCash
 }
 
 bob :: { Qubit, x :: Bit, y :: Bit -o Qubit }
@@ -46,6 +46,6 @@ bob(q, x, y) =
 
 tele(Qubit, Qubit, Qubit) -o Qubit, Vec(Money, 2)
 tele =
- lib.kernel.qid,bell00;
- alice, lib.kernel.qid;
+ |,bell00;
+ alice, |;
  (x, y, ms, q => bob(q, x, y), ms)

brat/examples/vector.brat

@@ -1,21 +1,9 @@
--- id :: Nat -> Nat
--- id = x => x
-
--- fst :: Nat, Nat -> Nat
--- fst = x, y => x
-
 swap(Nat, Nat) -> Nat, Nat
 swap = a, b => b, a
 
 nat :: Nat
 nat = 0
 
--- comp :: Nat, Nat -> Nat
--- comp = x, y => fst(swap(x, y))
-
--- te :: Vec Bool 2
--- te = [true, true]
-
 test :: Nat
 test = 1
 

brat/examples/vlup_covering.brat

@@ -10,7 +10,7 @@ import lib.kernel
 
 maybeRotate(Bool) -> { Qubit -o Qubit }
 maybeRotate(true) = lib.kernel.Rx(30.0)
-maybeRotate(false) = lib.kernel.qid
+maybeRotate(false) = { | }
 
 rotate :: { Qubit -o Qubit }
 rotate = { q => maybeRotate(true)(q) }

brat/test/Test/Compile/Hugr.hs

@@ -31,7 +31,6 @@ invalidExamples = map ((++ ".brat") . ("examples" </>))
   ["adder"
   ,"app"
   ,"dollar_kind"
-  ,"pass"
   ,"portpulling"
   ,"repeated_app" -- missing coercions, https://github.com/CQCL-DEV/brat/issues/413
   ,"thunks"]

brat/test/golden/error/multilambda-id.brat

@@ -0,0 +1,4 @@
+f(Bool) -> { Nat -> Nat }
+f = { true => |
+    | false => |
+    }

brat/test/golden/error/multilambda-id.brat.golden

@@ -0,0 +1,6 @@
+Error in test/golden/error/multilambda-id.brat@FC {start = Pos {line = 2, col = 15}, end = Pos {line = 2, col = 16}}:
+f = { true => |
+              ^
+
+  Elab error "Noun required at this position"
+

brat/test/golden/error/multilambda-id2.brat

@@ -0,0 +1,2 @@
+g(Nat) -> { Qubit -o Qubit }
+g = { 0 => ||succ(n) => | }

brat/test/golden/error/multilambda-id2.brat.golden

@@ -0,0 +1,6 @@
+Error in test/golden/error/multilambda-id2.brat@FC {start = Pos {line = 2, col = 12}, end = Pos {line = 2, col = 13}}:
+g = { 0 => ||succ(n) => | }
+           ^
+
+  Elab error "Noun required at this position"
+

brat/test/golden/error/multilambda-id3.brat

@@ -0,0 +1,2 @@
+f(Bool) -> { Qubit -o Qubit }
+f = { true => |;||false =>|;|;|}

brat/test/golden/error/multilambda-id3.brat.golden

@@ -0,0 +1,6 @@
+Error in test/golden/error/multilambda-id3.brat@FC {start = Pos {line = 2, col = 15}, end = Pos {line = 2, col = 18}}:
+f = { true => |;||false =>|;|;|}
+              ^^^
+
+  Elab error "Noun required at this position"
+