diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 618fc4f6..0e580768 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -23,6 +23,7 @@ import Control.Monad.Freer import Control.Monad.State.Lazy (StateT(..), runStateT) import Data.Bifunctor import Data.Foldable (foldrM) +import Data.Kind (Type) import Data.List (partition) import Data.Maybe (isJust) import Data.Type.Equality (TestEquality(..), (:~:)(..)) @@ -183,8 +184,8 @@ anext' :: forall m i j k anext' str th vals0 ins outs skol = do node <- req (Fresh str) -- Pick a name for the thunk -- Use the new name to generate Ends with which to instantiate types - (unders, vals1) <- endPorts node InEnd In 0 vals0 ins - (overs, vals2) <- endPorts node ExEnd Ex 0 vals1 outs + (unders, vals1) <- endPorts node InputRow 0 vals0 ins + (overs, vals2) <- endPorts node OutputRow 0 vals1 outs () <- sequence_ $ [ declareTgt tgt (modey @m) ty | (tgt, ty) <- unders ] ++ [ req (Declare (ExEnd (end src)) (modey @m) ty skol) | (src, ty) <- overs ] @@ -204,25 +205,39 @@ mkNode Kerny = KernelNode type Endz = Ny :* Stack Z End +data RowPolarity :: Type -> Type where + InputRow :: RowPolarity InPort + OutputRow :: RowPolarity OutPort + +port2End :: RowPolarity port -> port -> End +port2End InputRow = InEnd +port2End OutputRow = ExEnd + +mkPort :: RowPolarity port -> Name -> Int -> port +mkPort InputRow = In +mkPort OutputRow = Ex + -- endPorts instantiates the de Bruijn variables in a row with Ends endPorts :: forall m i j port . EvMode m - => Name -> (port -> End) -> (Name -> Int -> port) + => Name + -> RowPolarity port -> Int -- Next free port on the node -> (Semz i, Some Endz) -> Ro m i j -> Checking ([(NamedPort port, BinderType m)], (Semz j, Some Endz)) -endPorts _ _ _ _ stuff R0 = pure ([], stuff) -endPorts node port2End mkPort n (ga, ez) (RPr (p,ty) ro) = do +endPorts _ _ _ stuff R0 = pure ([], stuff) +endPorts node polarity n (ga, ez) (RPr (p,ty) ro) = do ty <- eval ga ty - (row, stuff) <- endPorts node port2End mkPort (n + 1) (ga, ez) ro - pure ((NamedPort (mkPort node n) p, tyBinder @m ty):row, stuff) -endPorts node port2End mkPort n (ga, Some (ny :* endz)) (REx (p, k) ro) = do - let port = mkPort node n - let end = port2End port - (row, stuff) <- endPorts node port2End mkPort (n + 1) + (row, stuff) <- endPorts node polarity (n + 1) (ga, ez) ro + pure ((NamedPort (mkPort polarity node n) p, tyBinder @m ty):row, stuff) +endPorts node polarity n (ga, Some (ny :* endz)) (REx (p, k) ro) = do + let port = mkPort polarity node n + let end = port2End polarity port + (row, stuff) <- endPorts node polarity (n + 1) (ga :<< SApp (SPar end) B0, Some (Sy ny :* (endz :<< end))) ro pure ((NamedPort port p, Left k):row, stuff) + next :: String -> NodeType Brat -> (Semz i, Some Endz) -> Ro Brat i j -> Ro Brat j k