feat: Datatype of thinnings

brat/Brat/Constructors.hs

@@ -30,6 +30,7 @@ defaultConstructors = M.fromList
   [(CSucc, M.fromList
      [(CNat, CArgs [] Zy R0 (RPr ("value", TNat) R0))
      ,(CInt, CArgs [] Zy R0 (RPr ("value", TInt) R0))
+     ,(CThin, CArgs [VPNum (NP1Plus NPVar), VPNum (NP1Plus NPVar)] (Sy (Sy Zy)) (REx ("wee", Nat) (REx ("big", Nat) R0)) (RPr ("thinning", TThin (VNum (nVar (VInx (VS VZ)))) (VNum (nVar (VInx VZ)))) R0))
      ])
   ,(CDoub, M.fromList
      [(CNat, CArgs [] Zy R0 (RPr ("value", TNat) R0))
@@ -38,6 +39,7 @@ defaultConstructors = M.fromList
   ,(CZero, M.fromList
      [(CNat, CArgs [] Zy R0 R0)
      ,(CInt, CArgs [] Zy R0 R0)
+     ,(CThin, CArgs [VPNum NP0, VPNum NP0] Zy R0 R0)
      ])
   ,(CNil, M.fromList
      [(CList, CArgs [VPVar] (Sy Zy) (REx ("elementType", Star []) R0) R0)
@@ -102,6 +104,13 @@ defaultConstructors = M.fromList
         (RPr ("value", VApp (VInx VZ) B0) R0))])
   ,(CTrue, M.fromList [(CBool, CArgs [] Zy R0 R0)])
   ,(CFalse, M.fromList [(CBool, CArgs [] Zy R0 R0)])
+  ,(COmit, M.fromList
+    [(CThin, CArgs [VPNum NPVar, VPNum (NP1Plus NPVar)] (Sy (Sy Zy))
+      -- args to type constructor
+      (REx ("wee", Nat) (REx ("big", Nat) R0)) -- n <= m'
+      -- Args to val constructor
+      (RPr ("thinning", TThin (VNum (nVar (VInx (VS VZ)))) (VNum (nVar (VInx VZ)))) R0)
+     )])
   ]
 
 kernelConstructors :: ConstructorMap Kernel
@@ -138,6 +147,7 @@ defaultTypeConstructors = M.fromList
   ,((Brat, CNat),    [])
   ,((Brat, CNil),    [])
   ,((Brat, CCons),   [("head", Star []), ("tail", Star [])])
+  ,((Brat, CThin),   [("wee", Nat), ("big", Nat)])
   ,((Kernel, CQubit), [])
   ,((Kernel, CMoney), [])
   ,((Kernel, CVec), [("X", Dollar []), ("n", Nat)])

brat/Brat/Constructors/Patterns.hs

@@ -3,7 +3,7 @@ module Brat.Constructors.Patterns where
 import Brat.QualName
 
 pattern CSucc, CDoub, CFull, CNil, CCons, CSome, CNone, CTrue, CFalse, CZero, CSnoc,
-        CConcatEqEven, CConcatEqOdd, CRiffle :: QualName
+        CConcatEqEven, CConcatEqOdd, CRiffle, COmit :: QualName
 pattern CSucc = PrefixName [] "succ"
 pattern CDoub = PrefixName [] "doub"
 pattern CFull = PrefixName [] "full"
@@ -18,8 +18,10 @@ pattern CSnoc = PrefixName [] "snoc"
 pattern CConcatEqEven = PrefixName [] "concatEqEven"
 pattern CConcatEqOdd = PrefixName [] "concatEqOdd"
 pattern CRiffle = PrefixName [] "riffle"
+-- N.B. The opposite of `COmit` is `CSucc`
+pattern COmit = PrefixName [] "omit"
 
-pattern CList, CVec, CNat, CInt, COption, CBool, CBit, CFloat, CString :: QualName
+pattern CList, CVec, CNat, CInt, COption, CBool, CBit, CFloat, CString, CThin :: QualName
 pattern CList = PrefixName [] "List"
 pattern CVec = PrefixName [] "Vec"
 pattern CNat = PrefixName [] "Nat"
@@ -29,6 +31,7 @@ pattern CBool = PrefixName [] "Bool"
 pattern CBit = PrefixName [] "Bit"
 pattern CFloat = PrefixName [] "Float"
 pattern CString = PrefixName [] "String"
+pattern CThin = PrefixName [] "Thin"
 
 pattern CQubit, CMoney :: QualName
 pattern CQubit = PrefixName [] "Qubit"

brat/Brat/Machine.hs

@@ -320,6 +320,8 @@ evalConstructor CTrue [] = BoolV True
 evalConstructor CFalse [] = BoolV False
 evalConstructor CZero [] = IntV 0
 evalConstructor CSucc [IntV n] = IntV (n + 1)
+evalConstructor CSucc [th@(ThinConsV _ _)] = ThinConsV True th
+evalConstructor COmit [th] = ThinConsV False th
 evalConstructor CDoub [IntV n] = IntV (2 * n)
 evalConstructor CFull [IntV n] = IntV ((2 ^ n) - 1)
 evalConstructor CNil [] = VecV []
@@ -381,6 +383,10 @@ testCtor CBool CTrue (BoolV True) = Just []
 testCtor CBool CFalse (BoolV False) = Just []
 testCtor CNat CZero (IntV 0) = Just []
 testCtor CNat CSucc (IntV x) | x > 0 = Just [IntV (x - 1)]
+testCtor CThin CZero (IntV 0) = Just []
+testCtor CThin CSucc (IntV x) | x > 0 = Just [IntV (x - 1)]
+testCtor CThin CSucc (ThinConsV True th) = Just [th]
+testCtor CThin COmit (ThinConsV False th) = Just [th]
 testCtor CVec CNil (VecV []) = Just []
 testCtor CVec CCons (VecV (v:vs)) = Just [v, VecV vs]
 testCtor CVec CSnoc (VecV vs@(_:_)) = Just [VecV (init vs), last vs]
@@ -414,6 +420,7 @@ data Value =
   | VecV [Value]
   | ThunkV BratThunk
   | KernelV (HG.HugrGraph HG.NodeId)
+  | ThinConsV Bool Value
   | DummyV
   | StringV String
 
@@ -431,6 +438,7 @@ instance Show Value where
   show (ThunkV (VectorisedThunks ths)) = "<vectorized thunk of " ++ show (length ths) ++ ">"
   show (ThunkV _) = "<thunk>"
   show (KernelV k) = "Kernel (" ++ show k ++ ")"
+  show (ThinConsV b val) = (if b then "1" else "0") ++ "-" ++ show val
   show DummyV = "Dummy"
   show (StringV str) = show str
 

brat/Brat/Parser.hs

@@ -222,7 +222,8 @@ abstractor = do ps <- many (try portPull)
       abs <- inBracketsFC Paren (unWC <$> abstractor)
       pure $ WC (spanFCOf str abs) (PCon (plain c) (unWC abs))
 
-    constructorsWithArgs = msum (try . constructorWithArgs <$> ["succ", "doub", "cons", "some"])
+    -- TODO: Consult the constructor table!
+    constructorsWithArgs = msum (try . constructorWithArgs <$> ["succ", "doub", "cons", "some", "omit"])
 
 simpleTerm :: Parser (WC SimpleTerm)
 simpleTerm =

brat/Brat/Syntax/Value.hs

@@ -266,9 +266,10 @@ pattern TList, TOption :: Val n -> Val n
 pattern TList ty = VCon (PrefixName [] "List") [ty]
 pattern TOption ty = VCon (PrefixName [] "Option") [ty]
 
-pattern TVec, TCons :: Val n -> Val n -> Val n
+pattern TVec, TCons, TThin :: Val n -> Val n -> Val n
 pattern TVec ty n = VCon (PrefixName [] "Vec") [ty, n]
 pattern TCons x ys = VCon (PrefixName [] "cons") [x, ys]
+pattern TThin a b = VCon (PrefixName [] "Thin") [a,b]
 
 pattern TQ, TMoney, TBit :: Val n
 pattern TQ = VCon (PrefixName [] "Qubit") []

brat/examples/thin.brat

@@ -1,23 +1,35 @@
---!xfail-parsing
--- Experiments with selecting out of vectors with first class selections
--- This feature has fallen by the wayside, so expect this to fail
+select(X :: *, n :: #, m :: #, Thin(n, m), Vec(X, m)) -> Vec(X, n)
+select(_, _, _, zero, []) = []
+select(_, _, _, succ(th), x ,- xs) = x ,- select(!, !, !, th, xs)
+select(_, _, _, omit(th), _ ,- xs) = select(!, !, !, th, xs)
 
--- This type is WRONG
-test :: Vec(X, 2) <<< Vec(X, 2)
-test = {0..} -- The identity thinning
+identity(n :: #) -> Thin(n, n)
+identity(0) = zero
+identity(succ(_)) = succ(identity(!))
 
-test' :: Vec(X, 1) <<< Vec(X, 9)
-test' = {5} -- just the fifth
+empty(n :: #) -> Thin(0, n)
+empty(0) = zero
+empty(succ(_)) = omit(empty(!))
 
-vec :: Vec(Nat, 5)
-vec = [1, 2, 3, 4, 5]
-
-test'' :: Vec(Nat, 1)
-test'' = vec{0} -- vec{2,4,5}
--- test''' :: Vec Nat 1
--- test''' = <0>
+comp(l :: #, n :: #, m :: #, Thin(l, n), Thin(n, m)) -> Thin(l, m)
+comp(_, _, _, th, omit(ph)) = omit(comp(!, !, !, th, ph))
+comp(_, _, _, omit(th), succ(ph)) = omit(comp(!, !, !, th, ph))
+comp(_, _, _, succ(th), succ(ph)) = succ(comp(!, !, !, th, ph))
+comp(_, _, _, zero, zero) = zero
 
-mapOn :: (th :: x <<< y), (f :: X -> X), Vec(X, y) -> Vec(X, y)
-mapOn = ?mapOn
+thinning1 :: Thin(3, 5)
+thinning1 = succ(omit(succ(succ(omit(zero)))))
 
-map = mapOn {1,4} f vec
+thinning2 :: Thin(1, 3)
+thinning2 = omit(succ(omit(zero)))
+
+thinning :: Thin(1, 5)
+thinning = comp(!, !, !, thinning2, thinning1)
+
+--!exec [[1,3,4]]
+go2 :: Vec(Nat, 3)
+go2 = select(!, !, !, thinning1, [1,2,3,4,5])
+
+--!exec [[3]]
+go :: Vec(Nat, 1)
+go = select(!, !, !, thinning, [1,2,3,4,5])