diff --git a/brat/Brat/Constructors.hs b/brat/Brat/Constructors.hs index 16b196bc..545e943f 100644 --- a/brat/Brat/Constructors.hs +++ b/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)]) diff --git a/brat/Brat/Constructors/Patterns.hs b/brat/Brat/Constructors/Patterns.hs index 4fd6fac1..39a3b93e 100644 --- a/brat/Brat/Constructors/Patterns.hs +++ b/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" diff --git a/brat/Brat/Machine.hs b/brat/Brat/Machine.hs index 45037279..a6b0c8fc 100644 --- a/brat/Brat/Machine.hs +++ b/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)) = "" show (ThunkV _) = "" 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 diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 84b34aae..33875be5 100644 --- a/brat/Brat/Parser.hs +++ b/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 = diff --git a/brat/Brat/Syntax/Value.hs b/brat/Brat/Syntax/Value.hs index 1af8b94e..ed8aa188 100644 --- a/brat/Brat/Syntax/Value.hs +++ b/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") [] diff --git a/brat/examples/thin.brat b/brat/examples/thin.brat index 92c99e46..8cd5eed0 100644 --- a/brat/examples/thin.brat +++ b/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])