From 45c53042e9c5b206f0afcc616e19187ffc1b1e39 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Fri, 22 Nov 2024 15:40:21 +0000 Subject: [PATCH 1/4] mkMapFuns -> mkMapFun + foldrM --- brat/Brat/Checker/Helpers.hs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 5e609f14..7e19f0eb 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -39,6 +39,7 @@ import Util (log2) import Control.Monad.Freer (req, Free(Ret)) import Data.Bifunctor +import Data.Foldable (foldrM) import Data.List (intercalate) import Data.Type.Equality (TestEquality(..), (:~:)(..)) import qualified Data.Map as M @@ -344,14 +345,12 @@ mkStaticNum n@(NumValue c gro) = do vectorise :: (Src, Val Z) -> Checking (Src, Val Z) vectorise (src, ty) = do (layers, Some (my :* Flip cty)) <- vecLayers ty - modily my $ mkMapFuns (src, VFun my cty) layers + modily my $ foldrM mkMapFun (src, VFun my cty) layers where - mkMapFuns :: (Src, Val Z) -- The input to the mapfun - -> [(Src, NumVal (VVar Z))] -- Remaining layers + mkMapFun :: (Src, NumVal (VVar Z)) -- Layer to apply + -> (Src, Val Z) -- The input to this level of mapfun -> Checking (Src, Val Z) - mkMapFuns over [] = pure over - mkMapFuns (valSrc, ty) ((lenSrc, len):layers) = do - (valSrc, ty@(VFun my cty)) <- mkMapFuns (valSrc, ty) layers + mkMapFun (lenSrc, len) (valSrc, ty@(VFun my cty)) = do let weak1 = changeVar (Thinning (ThDrop ThNull)) vecFun <- vectorisedFun len my cty (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right vecTy)], _) <- From a6bb951207040db83350174765c8514eb359c03d Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Fri, 22 Nov 2024 16:30:13 +0000 Subject: [PATCH 2/4] golf vecLayers --- brat/Brat/Checker/Helpers.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 7e19f0eb..c9b33f0b 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -291,8 +291,7 @@ vecLayers :: Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes of the vec ) vecLayers (TVec ty (VNum n)) = do src <- mkStaticNum n - (layers, fun) <- vecLayers ty - pure ((src, n):layers, fun) + first ((src, n):) <$> vecLayers ty vecLayers (VFun my cty) = pure ([], Some (my :* Flip cty)) vecLayers ty = typeErr $ "Expected a function or vector of functions, got " ++ show ty From dc6756bbf7ea6e00e777f34dc8a64b86f07b2d06 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Fri, 22 Nov 2024 16:32:07 +0000 Subject: [PATCH 3/4] Make return type of vectorise obvious, so remove some pointless cases --- brat/Brat/Checker/Helpers.hs | 68 ++++++++++--------- .../kernel/kernel_application.brat.golden | 4 +- 2 files changed, 36 insertions(+), 36 deletions(-) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index c9b33f0b..bd5b75f1 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables #-} module Brat.Checker.Helpers {-(pullPortsRow, pullPortsSig ,simpleCheck @@ -259,22 +259,19 @@ getThunks :: Modey m ,Overs m UVerb ) getThunks _ [] = pure ([], [], []) -getThunks Braty row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case - (src, VFun Braty (ss :->> ts)) -> do - (node, unders, overs, _) <- let ?my = Braty in - anext "" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts - (nodes, unders', overs') <- getThunks Braty rest - pure (node:nodes, unders <> unders', overs <> overs') - -- These shouldn't happen - (_, VFun _ _) -> err $ ExpectedThunk (showMode Braty) (showRow row) - v -> typeErr $ "Force called on non-thunk: " ++ show v -getThunks Kerny row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case - (src, VFun Kerny (ss :->> ts)) -> do - (node, unders, overs, _) <- let ?my = Kerny in anext "" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts - (nodes, unders', overs') <- getThunks Kerny rest - pure (node:nodes, unders <> unders', overs <> overs') - (_, VFun _ _) -> err $ ExpectedThunk (showMode Kerny) (showRow row) - v -> typeErr $ "Force called on non-(kernel)-thunk: " ++ show v +getThunks Braty ((src, Right ty):rest) = do + ty <- eval S0 ty + (src, (ss :->> ts)) <- vectorise Braty (src, ty) + (node, unders, overs, _) <- let ?my = Braty in + anext "" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts + (nodes, unders', overs') <- getThunks Braty rest + pure (node:nodes, unders <> unders', overs <> overs') +getThunks Kerny ((src, Right ty):rest) = do + ty <- eval S0 ty + (src, (ss :->> ts)) <- vectorise Kerny (src,ty) + (node, unders, overs, _) <- let ?my = Kerny in anext "" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts + (nodes, unders', overs') <- getThunks Kerny rest + pure (node:nodes, unders <> unders', overs <> overs') getThunks Braty ((src, Left (Star args)):rest) = do (node, unders, overs) <- case bwdStack (B0 <>< args) of Some (_ :* stk) -> do @@ -286,14 +283,15 @@ getThunks Braty ((src, Left (Star args)):rest) = do getThunks m ro = err $ ExpectedThunk (showMode m) (showRow ro) -- The type given here should be normalised -vecLayers :: Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes of the vector layers - ,Some (Modey :* Flip CTy Z) -- The function type at the end - ) -vecLayers (TVec ty (VNum n)) = do +vecLayers :: Modey m -> Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes of the vector layers + ,CTy m Z -- The function type at the end + ) +vecLayers my (TVec ty (VNum n)) = do src <- mkStaticNum n - first ((src, n):) <$> vecLayers ty -vecLayers (VFun my cty) = pure ([], Some (my :* Flip cty)) -vecLayers ty = typeErr $ "Expected a function or vector of functions, got " ++ show ty + first ((src, n):) <$> vecLayers my ty +vecLayers Braty (VFun Braty cty) = pure ([], cty) +vecLayers Kerny (VFun Kerny cty) = pure ([], cty) +vecLayers my ty = typeErr $ "Expected a " ++ showMode my ++ "function or vector of functions, got " ++ show ty mkStaticNum :: NumVal (VVar Z) -> Checking Src mkStaticNum n@(NumValue c gro) = do @@ -341,25 +339,29 @@ mkStaticNum n@(NumValue c gro) = do wire (oneSrc, TNat, rhs) pure src -vectorise :: (Src, Val Z) -> Checking (Src, Val Z) -vectorise (src, ty) = do - (layers, Some (my :* Flip cty)) <- vecLayers ty - modily my $ foldrM mkMapFun (src, VFun my cty) layers +vectorise :: forall m. Modey m -> (Src, Val Z) -> Checking (Src, CTy m Z) +vectorise my (src, ty) = do + (layers, cty) <- vecLayers my ty + modily my $ foldrM mkMapFun (src, cty) layers where mkMapFun :: (Src, NumVal (VVar Z)) -- Layer to apply - -> (Src, Val Z) -- The input to this level of mapfun - -> Checking (Src, Val Z) - mkMapFun (lenSrc, len) (valSrc, ty@(VFun my cty)) = do + -> (Src, CTy m Z) -- The input to this level of mapfun + -> Checking (Src, CTy m Z) + mkMapFun (lenSrc, len) (valSrc, cty) = do let weak1 = changeVar (Thinning (ThDrop ThNull)) vecFun <- vectorisedFun len my cty - (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right vecTy)], _) <- + (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right (VFun my' cty))], _) <- next "" MapFun (S0, Some (Zy :* S0)) (REx ("len", Nat) (RPr ("value", weak1 ty) R0)) (RPr ("vector", weak1 vecFun) R0) defineTgt lenTgt (VNum len) wire (lenSrc, kindType Nat, lenTgt) wire (valSrc, ty, valTgt) - pure (vectorSrc, vecTy) + let vecCTy = case (my,my',cty) of + (Braty,Braty,cty) -> cty + (Kerny,Kerny,cty) -> cty + _ -> error "next returned wrong mode of computation type to that passed in" + pure (vectorSrc, vecCTy) vectorisedFun :: NumVal (VVar Z) -> Modey m -> CTy m Z -> Checking (Val Z) vectorisedFun nv my (ss :->> ts) = do diff --git a/brat/test/golden/kernel/kernel_application.brat.golden b/brat/test/golden/kernel/kernel_application.brat.golden index ed0aa8bf..af09def9 100644 --- a/brat/test/golden/kernel/kernel_application.brat.golden +++ b/brat/test/golden/kernel/kernel_application.brat.golden @@ -2,7 +2,5 @@ Error in test/golden/kernel/kernel_application.brat on line 16: rotate = { q => maybeRotate(true) } ^^^^^^^^^^^ - Expected function to be a (kernel) thunk, but found: - (thunk :: { (a1 :: Bool) -> (a1 :: { (a1 :: Qubit) -o (a1 :: Qubit) }) }) - + Type error: Expected a (kernel) function or vector of functions, got { (a1 :: Bool) -> (a1 :: { (a1 :: Qubit) -o (a1 :: Qubit) }) } From 88ae5a826919601f46db6498b2140817a69d6b4c Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 27 Nov 2024 14:01:07 +0000 Subject: [PATCH 4/4] ScopedTypeVariables already on --- brat/Brat/Checker/Helpers.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index bd5b75f1..7263b81f 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} module Brat.Checker.Helpers {-(pullPortsRow, pullPortsSig ,simpleCheck