{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UnicodeSyntax #-}

-- | System L with polynomial types and @These@ covariable boundaries.
--
-- This module rebuilds the original hand-rolled @Loop (,) (->)@ interpreter
-- as a @circuits@ client:
--
-- * User-facing types are promoted to 'Circuit.Poly' polynomials via 'SysLTy'.
-- * Command results are expressed with 'Data.These' boundaries, matching the
--   inclusive tensor in "Circuit.Channel".
-- * The syntactic target is the free SMC @SMC (->)@; boundaries use 'These'
--   at the value level.
-- * A streaming reading is provided via 'Circuit.Process'.
--
-- The original four regression tests are preserved as 'testId', 'testThen',
-- 'testIdLoop' and 'testThenLoop'.
module SysL
  ( -- * Types
    Ty (..),
    SysLTy,
    Domain,

    -- * Values and boundaries
    Val (..),
    Output,
    Result,
    Env,

    -- * Syntax
    Command (..),
    Value (..),
    Term (..),
    Coterm (..),

    -- * Direct evaluator
    evalCommand,
    evalValue,
    evalTerm,
    evalCoterm,
    lookupEnv,

    -- * Polynomial view
    PolyVal (..),

    -- * SMC SMC compiler
    SMCThese,
    commandToSMC,
    termToSMC,
    cotermToSMC,

    -- * Process interpreter
    evalProcess,

    -- * Then as optic
    thenLens,
    applyThen,

    -- * Regression tests
    testId,
    testThen,
    testIdLoop,
    testThenLoop,
  )
where

import Circuit.Poly
  ( Eval (..),
    Mono,
    Morphism (..),
    Poly (..),
    applyLens,
    lens,
  )
import Circuit.Process (Process (..))
import Circuit.SMC (SMC, lift)
import Circuit.Syntax (eval)
import Data.Kind (Type)
import Data.These (These (..))
import Data.Void (Void, absurd)
import Prelude hiding (id, (.))

-- ---------------------------------------------------------------------------
-- Types as polynomials
-- ---------------------------------------------------------------------------

-- | User-facing SysL type syntax.
data Ty
  = One
  | Times Ty Ty
  | Zero
  | Plus Ty Ty
  | Hom Ty Ty
  | GradedHom Ty [Ty]
  | Then Ty Ty
  deriving (Int -> Ty -> ShowS
[Ty] -> ShowS
Ty -> String
(Int -> Ty -> ShowS)
-> (Ty -> String) -> ([Ty] -> ShowS) -> Show Ty
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Ty -> ShowS
showsPrec :: Int -> Ty -> ShowS
$cshow :: Ty -> String
show :: Ty -> String
$cshowList :: [Ty] -> ShowS
showList :: [Ty] -> ShowS
Show, Ty -> Ty -> Bool
(Ty -> Ty -> Bool) -> (Ty -> Ty -> Bool) -> Eq Ty
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Ty -> Ty -> Bool
== :: Ty -> Ty -> Bool
$c/= :: Ty -> Ty -> Bool
/= :: Ty -> Ty -> Bool
Eq)

-- | Promoted polynomial encoding of a SysL type.
--
-- 'Hom', 'Then' and the graded variant are represented as monomial
-- lenses / dependent optics, which is the natural polynomial reading of
-- functions with a backward map.
type family SysLTy (t :: Ty) :: Poly where
  SysLTy 'One = 'Const ()
  SysLTy ('Times a b) = 'Prod (SysLTy a) (SysLTy b)
  SysLTy 'Zero = 'Const Void
  SysLTy ('Plus a b) = 'Sum (SysLTy a) (SysLTy b)
  SysLTy ('Hom a b) = Mono (Domain a) (Domain b)
  SysLTy ('Then a b) = Mono (Domain a) (Domain b)
  SysLTy ('GradedHom a bs) = GradedPoly a bs

-- | Closed value domain for a SysL type.
type family Domain (t :: Ty) :: Type where
  Domain 'One = ()
  Domain ('Times a b) = (Domain a, Domain b)
  Domain 'Zero = Void
  Domain ('Plus a b) = Either (Domain a) (Domain b)
  Domain ('Hom a b) = Domain a -> Domain b
  Domain ('Then a b) = Domain a -> Domain b
  Domain ('GradedHom a bs) = Domain a -> GradedResult bs

-- | Result type for a graded list of return types.
type family GradedResult (bs :: [Ty]) :: Type where
  GradedResult '[] = Void
  GradedResult (b ': bs) = Either (Domain b) (GradedResult bs)

-- | Polynomial for a graded homomorphism: a sum of monomial lenses.
type family GradedPoly (a :: Ty) (bs :: [Ty]) :: Poly where
  GradedPoly _ '[] = 'Const Void
  GradedPoly a (b ': bs) = 'Sum (Mono (Domain a) (Domain b)) (GradedPoly a bs)

-- ---------------------------------------------------------------------------
-- Values and boundaries
-- ---------------------------------------------------------------------------

-- | A result is now a covariable boundary using the inclusive @These@ tensor.
--
-- * 'This' carries a residual output (slot >= 1).
-- * 'That' carries a focus output (slot 0).
-- * 'These' carries both residual and focus.
--
-- This follows the convention in "Circuit.Channel": 'This' is the
-- feedback / residual branch and 'That' is the payload / focus branch.
type Result v = These (Output v) (Output v)

-- | An output is a slot together with a value.
type Output v = (Int, Val v)

-- | Runtime values, parametric in the opaque domain type @v@.
data Val v
  = VUnit
  | VPair (Val v) (Val v)
  | VLeft (Val v)
  | VRight (Val v)
  | VFun (Val v -> Result v)
  | VGradedFun (Val v -> Result v)
  | VThen (Val v) (Val v -> Result v)
  | VEmbed v

instance (Eq v) => Eq (Val v) where
  Val v
VUnit == :: Val v -> Val v -> Bool
== Val v
VUnit = Bool
True
  VPair Val v
a Val v
b == VPair Val v
c Val v
d = Val v
a Val v -> Val v -> Bool
forall a. Eq a => a -> a -> Bool
== Val v
c Bool -> Bool -> Bool
&& Val v
b Val v -> Val v -> Bool
forall a. Eq a => a -> a -> Bool
== Val v
d
  VLeft Val v
a == VLeft Val v
b = Val v
a Val v -> Val v -> Bool
forall a. Eq a => a -> a -> Bool
== Val v
b
  VRight Val v
a == VRight Val v
b = Val v
a Val v -> Val v -> Bool
forall a. Eq a => a -> a -> Bool
== Val v
b
  VEmbed v
x == VEmbed v
y = v
x v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
y
  Val v
_ == Val v
_ = Bool
False

instance (Show v) => Show (Val v) where
  show :: Val v -> String
show Val v
VUnit = String
"VUnit"
  show (VPair Val v
a Val v
b) = String
"VPair (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall a. Show a => a -> String
show Val v
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
") (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall a. Show a => a -> String
show Val v
b String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (VLeft Val v
a) = String
"VLeft (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall a. Show a => a -> String
show Val v
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (VRight Val v
b) = String
"VRight (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall a. Show a => a -> String
show Val v
b String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (VFun Val v -> Result v
_) = String
"VFun <fn>"
  show (VGradedFun Val v -> Result v
_) = String
"VGradedFun <fn>"
  show (VThen Val v
a Val v -> Result v
_) = String
"VThen (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall a. Show a => a -> String
show Val v
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
") <fn>"
  show (VEmbed v
v) = String
"VEmbed (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> v -> String
forall a. Show a => a -> String
show v
v String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"

-- | Input environment: de Bruijn indexed list of values.
type Env v = [Val v]

lookupEnv :: Int -> Env v -> Val v
lookupEnv :: forall v. Int -> Env v -> Val v
lookupEnv Int
0 (Val v
x : [Val v]
_) = Val v
x
lookupEnv Int
n (Val v
_ : [Val v]
xs) = Int -> [Val v] -> Val v
forall v. Int -> Env v -> Val v
lookupEnv (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Val v]
xs
lookupEnv Int
_ [] = String -> Val v
forall a. HasCallStack => String -> a
error String
"lookupEnv: index out of range"

-- ---------------------------------------------------------------------------
-- Syntax
-- ---------------------------------------------------------------------------

data Command v = Cut (Term v) (Coterm v)
  deriving (Int -> Command v -> ShowS
[Command v] -> ShowS
Command v -> String
(Int -> Command v -> ShowS)
-> (Command v -> String)
-> ([Command v] -> ShowS)
-> Show (Command v)
forall v. Show v => Int -> Command v -> ShowS
forall v. Show v => [Command v] -> ShowS
forall v. Show v => Command v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> Command v -> ShowS
showsPrec :: Int -> Command v -> ShowS
$cshow :: forall v. Show v => Command v -> String
show :: Command v -> String
$cshowList :: forall v. Show v => [Command v] -> ShowS
showList :: [Command v] -> ShowS
Show)

data Value v
  = Var Int
  | TensorIntro (Value v) (Value v)
  | PlusIntroL (Value v)
  | PlusIntroR (Value v)
  | HomComatch (Command v)
  | GradedHomComatch (Command v)
  | Lit (Val v)
  deriving (Int -> Value v -> ShowS
[Value v] -> ShowS
Value v -> String
(Int -> Value v -> ShowS)
-> (Value v -> String) -> ([Value v] -> ShowS) -> Show (Value v)
forall v. Show v => Int -> Value v -> ShowS
forall v. Show v => [Value v] -> ShowS
forall v. Show v => Value v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> Value v -> ShowS
showsPrec :: Int -> Value v -> ShowS
$cshow :: forall v. Show v => Value v -> String
show :: Value v -> String
$cshowList :: forall v. Show v => [Value v] -> ShowS
showList :: [Value v] -> ShowS
Show)

data Term v
  = Embed (Value v)
  | Mu (Command v)
  | ThenComatch (Command v)
  deriving (Int -> Term v -> ShowS
[Term v] -> ShowS
Term v -> String
(Int -> Term v -> ShowS)
-> (Term v -> String) -> ([Term v] -> ShowS) -> Show (Term v)
forall v. Show v => Int -> Term v -> ShowS
forall v. Show v => [Term v] -> ShowS
forall v. Show v => Term v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> Term v -> ShowS
showsPrec :: Int -> Term v -> ShowS
$cshow :: forall v. Show v => Term v -> String
show :: Term v -> String
$cshowList :: forall v. Show v => [Term v] -> ShowS
showList :: [Term v] -> ShowS
Show)

data Coterm v
  = Covar Int
  | Comu (Command v)
  | TensorMatch (Command v)
  | PlusMatch (Command v) (Command v)
  | HomCointro (Term v) (Coterm v)
  | GradedHomCointro (Term v) [Coterm v]
  | ThenCointro (Coterm v) (Coterm v)
  deriving (Int -> Coterm v -> ShowS
[Coterm v] -> ShowS
Coterm v -> String
(Int -> Coterm v -> ShowS)
-> (Coterm v -> String) -> ([Coterm v] -> ShowS) -> Show (Coterm v)
forall v. Show v => Int -> Coterm v -> ShowS
forall v. Show v => [Coterm v] -> ShowS
forall v. Show v => Coterm v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> Coterm v -> ShowS
showsPrec :: Int -> Coterm v -> ShowS
$cshow :: forall v. Show v => Coterm v -> String
show :: Coterm v -> String
$cshowList :: forall v. Show v => [Coterm v] -> ShowS
showList :: [Coterm v] -> ShowS
Show)

-- ---------------------------------------------------------------------------
-- Polynomial value view
-- ---------------------------------------------------------------------------

-- | Convert between the runtime 'Val' representation and the polynomial
-- 'Eval' representation for a closed SysL type.
class PolyVal (t :: Ty) where
  valToEval :: Val v -> Eval (SysLTy t) v
  evalToVal :: Eval (SysLTy t) v -> Val v

instance PolyVal 'One where
  valToEval :: forall v. Val v -> Eval (SysLTy 'One) v
valToEval Val v
VUnit = () -> Eval ('Const ()) v
forall c x. c -> Eval ('Const c) x
EK ()
  valToEval Val v
v = String -> Eval (SysLTy 'One) v
forall a. HasCallStack => String -> a
error (String -> Eval (SysLTy 'One) v) -> String -> Eval (SysLTy 'One) v
forall a b. (a -> b) -> a -> b
$ String
"valToEval One: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall v. Val v -> String
show' Val v
v
  evalToVal :: forall v. Eval (SysLTy 'One) v -> Val v
evalToVal (EK ()) = Val v
forall v. Val v
VUnit

instance (PolyVal a, PolyVal b) => PolyVal ('Times a b) where
  valToEval :: forall v. Val v -> Eval (SysLTy ('Times a b)) v
valToEval (VPair Val v
x Val v
y) = (Eval (SysLTy a) v, Eval (SysLTy b) v)
-> Eval ('Prod (SysLTy a) (SysLTy b)) v
forall (p1 :: Poly) x (q :: Poly).
(Eval p1 x, Eval q x) -> Eval ('Prod p1 q) x
EP (forall (t :: Ty) v. PolyVal t => Val v -> Eval (SysLTy t) v
valToEval @a Val v
x, forall (t :: Ty) v. PolyVal t => Val v -> Eval (SysLTy t) v
valToEval @b Val v
y)
  valToEval Val v
v = String -> Eval (SysLTy ('Times a b)) v
forall a. HasCallStack => String -> a
error (String -> Eval (SysLTy ('Times a b)) v)
-> String -> Eval (SysLTy ('Times a b)) v
forall a b. (a -> b) -> a -> b
$ String
"valToEval Times: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall v. Val v -> String
show' Val v
v
  evalToVal :: forall v. Eval (SysLTy ('Times a b)) v -> Val v
evalToVal (EP (Eval p1 v
x, Eval q v
y)) = Val v -> Val v -> Val v
forall v. Val v -> Val v -> Val v
VPair (forall (t :: Ty) v. PolyVal t => Eval (SysLTy t) v -> Val v
evalToVal @a Eval p1 v
Eval (SysLTy a) v
x) (forall (t :: Ty) v. PolyVal t => Eval (SysLTy t) v -> Val v
evalToVal @b Eval q v
Eval (SysLTy b) v
y)

instance PolyVal 'Zero where
  valToEval :: forall v. Val v -> Eval (SysLTy 'Zero) v
valToEval Val v
v = String -> Eval (SysLTy 'Zero) v
forall a. HasCallStack => String -> a
error (String -> Eval (SysLTy 'Zero) v)
-> String -> Eval (SysLTy 'Zero) v
forall a b. (a -> b) -> a -> b
$ String
"valToEval Zero: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall v. Val v -> String
show' Val v
v
  evalToVal :: forall v. Eval (SysLTy 'Zero) v -> Val v
evalToVal (EK c
v) = Void -> Val v
forall a. Void -> a
absurd c
Void
v

instance (PolyVal a, PolyVal b) => PolyVal ('Plus a b) where
  valToEval :: forall v. Val v -> Eval (SysLTy ('Plus a b)) v
valToEval (VLeft Val v
x) = Either (Eval (SysLTy a) v) (Eval (SysLTy b) v)
-> Eval ('Sum (SysLTy a) (SysLTy b)) v
forall (p1 :: Poly) x (q :: Poly).
Either (Eval p1 x) (Eval q x) -> Eval ('Sum p1 q) x
ES (Eval (SysLTy a) v -> Either (Eval (SysLTy a) v) (Eval (SysLTy b) v)
forall a b. a -> Either a b
Left (forall (t :: Ty) v. PolyVal t => Val v -> Eval (SysLTy t) v
valToEval @a Val v
x))
  valToEval (VRight Val v
y) = Either (Eval (SysLTy a) v) (Eval (SysLTy b) v)
-> Eval ('Sum (SysLTy a) (SysLTy b)) v
forall (p1 :: Poly) x (q :: Poly).
Either (Eval p1 x) (Eval q x) -> Eval ('Sum p1 q) x
ES (Eval (SysLTy b) v -> Either (Eval (SysLTy a) v) (Eval (SysLTy b) v)
forall a b. b -> Either a b
Right (forall (t :: Ty) v. PolyVal t => Val v -> Eval (SysLTy t) v
valToEval @b Val v
y))
  valToEval Val v
v = String -> Eval (SysLTy ('Plus a b)) v
forall a. HasCallStack => String -> a
error (String -> Eval (SysLTy ('Plus a b)) v)
-> String -> Eval (SysLTy ('Plus a b)) v
forall a b. (a -> b) -> a -> b
$ String
"valToEval Plus: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall v. Val v -> String
show' Val v
v
  evalToVal :: forall v. Eval (SysLTy ('Plus a b)) v -> Val v
evalToVal (ES (Left Eval p1 v
x)) = Val v -> Val v
forall v. Val v -> Val v
VLeft (forall (t :: Ty) v. PolyVal t => Eval (SysLTy t) v -> Val v
evalToVal @a Eval p1 v
Eval (SysLTy a) v
x)
  evalToVal (ES (Right Eval q v
y)) = Val v -> Val v
forall v. Val v -> Val v
VRight (forall (t :: Ty) v. PolyVal t => Eval (SysLTy t) v -> Val v
evalToVal @b Eval q v
Eval (SysLTy b) v
y)

-- ---------------------------------------------------------------------------
-- Direct evaluator with These boundaries
-- ---------------------------------------------------------------------------

evalCommand :: Command v -> Env v -> Result v
evalCommand :: forall v. Command v -> Env v -> Result v
evalCommand (Cut Term v
t Coterm v
k) Env v
env =
  case Term v -> Env v -> These (Output v) (Val v)
forall v. Term v -> Env v -> These (Output v) (Val v)
evalTerm Term v
t Env v
env of
    This Output v
out -> Output v -> Result v
forall a b. a -> These a b
This Output v
out
    That Val v
val -> Coterm v -> Env v -> Val v -> Result v
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k Env v
env Val v
val
    These Output v
res Val v
val -> Output v -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
res (Coterm v -> Env v -> Val v -> Result v
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k Env v
env Val v
val)
  where
    combine :: (a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (a, Val v)
res (This (a, b)
res') = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
res'
    combine (a, Val v)
res (That (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
foc
    combine (a, Val v)
res (These (a, b)
res' (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These ((a, Val v) -> (a, b) -> (a, Val v)
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge (a, Val v)
res (a, b)
res') (a, b)
foc
    merge :: (a, b) -> (a, b) -> (a, Val v)
merge (a
i, b
_) (a
j, b
_) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
i a
j, Val v
forall v. Val v
VUnit) -- residual merge keeps largest slot

evalValue :: Value v -> Env v -> Val v
evalValue :: forall v. Value v -> Env v -> Val v
evalValue (Var Int
i) Env v
env = Int -> Env v -> Val v
forall v. Int -> Env v -> Val v
lookupEnv Int
i Env v
env
evalValue (TensorIntro Value v
v1 Value v
v2) Env v
env = Val v -> Val v -> Val v
forall v. Val v -> Val v -> Val v
VPair (Value v -> Env v -> Val v
forall v. Value v -> Env v -> Val v
evalValue Value v
v1 Env v
env) (Value v -> Env v -> Val v
forall v. Value v -> Env v -> Val v
evalValue Value v
v2 Env v
env)
evalValue (PlusIntroL Value v
v) Env v
env = Val v -> Val v
forall v. Val v -> Val v
VLeft (Value v -> Env v -> Val v
forall v. Value v -> Env v -> Val v
evalValue Value v
v Env v
env)
evalValue (PlusIntroR Value v
v) Env v
env = Val v -> Val v
forall v. Val v -> Val v
VRight (Value v -> Env v -> Val v
forall v. Value v -> Env v -> Val v
evalValue Value v
v Env v
env)
evalValue (HomComatch Command v
cmd) Env v
env =
  (Val v -> Result v) -> Val v
forall v. (Val v -> Result v) -> Val v
VFun ((Val v -> Result v) -> Val v) -> (Val v -> Result v) -> Val v
forall a b. (a -> b) -> a -> b
$ \Val v
x ->
    Command v -> Env v -> Result v
forall v. Command v -> Env v -> Result v
evalCommand Command v
cmd (Val v
x Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
evalValue (GradedHomComatch Command v
cmd) Env v
env =
  (Val v -> Result v) -> Val v
forall v. (Val v -> Result v) -> Val v
VGradedFun ((Val v -> Result v) -> Val v) -> (Val v -> Result v) -> Val v
forall a b. (a -> b) -> a -> b
$ \Val v
x ->
    Command v -> Env v -> Result v
forall v. Command v -> Env v -> Result v
evalCommand Command v
cmd (Val v
x Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
evalValue (Lit Val v
v) Env v
_ = Val v
v

evalTerm :: Term v -> Env v -> These (Output v) (Val v)
evalTerm :: forall v. Term v -> Env v -> These (Output v) (Val v)
evalTerm (Embed Value v
v) Env v
env = Val v -> These (Output v) (Val v)
forall a b. b -> These a b
That (Value v -> Env v -> Val v
forall v. Value v -> Env v -> Val v
evalValue Value v
v Env v
env)
evalTerm (Mu Command v
cmd) Env v
env =
  case Command v -> Env v -> Result v
forall v. Command v -> Env v -> Result v
evalCommand Command v
cmd Env v
env of
    This Output v
out -> Output v -> These (Output v) (Val v)
forall a b. a -> These a b
This Output v
out
    That (Int
0, Val v
val) -> Val v -> These (Output v) (Val v)
forall a b. b -> These a b
That Val v
val
    That Output v
out -> Output v -> These (Output v) (Val v)
forall a b. a -> These a b
This Output v
out
    These Output v
res (Int
0, Val v
val) -> Output v -> Val v -> These (Output v) (Val v)
forall a b. a -> b -> These a b
These Output v
res Val v
val
    These Output v
res Output v
foc -> Output v -> Val v -> These (Output v) (Val v)
forall a b. a -> b -> These a b
These Output v
res (Output v -> Val v
forall a b. (a, b) -> b
snd Output v
foc)
evalTerm (ThenComatch Command v
cmd) Env v
env =
  let fwdA :: Val v
fwdA = case Command v -> Env v -> Result v
forall v. Command v -> Env v -> Result v
evalCommand Command v
cmd Env v
env of
        That (Int
1, Val v
v) -> Val v
v
        These Output v
_ (Int
1, Val v
v) -> Val v
v
        Result v
_ -> String -> Val v
forall a. HasCallStack => String -> a
error String
"ThenComatch: expected slot 1 for fwd a"
      bwCont :: Val v -> Result v
bwCont Val v
bwA = Command v -> Env v -> Result v
forall v. Command v -> Env v -> Result v
evalCommand Command v
cmd (Val v
bwA Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
   in Val v -> These (Output v) (Val v)
forall a b. b -> These a b
That (Val v -> (Val v -> Result v) -> Val v
forall v. Val v -> (Val v -> Result v) -> Val v
VThen Val v
fwdA Val v -> Result v
bwCont)

evalCoterm :: Coterm v -> Env v -> Val v -> Result v
evalCoterm :: forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm (Covar Int
i) Env v
_env Val v
val =
  if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Output v -> These (Output v) (Output v)
forall a b. b -> These a b
That (Int
0, Val v
val) else Output v -> These (Output v) (Output v)
forall a b. a -> These a b
This (Int
i, Val v
val)
evalCoterm (Comu Command v
cmd) Env v
env Val v
val = Command v -> Env v -> These (Output v) (Output v)
forall v. Command v -> Env v -> Result v
evalCommand Command v
cmd (Val v
val Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
evalCoterm (TensorMatch Command v
cmd) Env v
env (VPair Val v
x Val v
y) = Command v -> Env v -> These (Output v) (Output v)
forall v. Command v -> Env v -> Result v
evalCommand Command v
cmd (Val v
x Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Val v
y Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
evalCoterm (TensorMatch Command v
_) Env v
_ Val v
v = String -> These (Output v) (Output v)
forall a. HasCallStack => String -> a
error (String -> These (Output v) (Output v))
-> String -> These (Output v) (Output v)
forall a b. (a -> b) -> a -> b
$ String
"TensorMatch: not a pair: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall v. Val v -> String
show' Val v
v
evalCoterm (PlusMatch Command v
c1 Command v
_) Env v
env (VLeft Val v
x) = Command v -> Env v -> These (Output v) (Output v)
forall v. Command v -> Env v -> Result v
evalCommand Command v
c1 (Val v
x Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
evalCoterm (PlusMatch Command v
_ Command v
c2) Env v
env (VRight Val v
y) = Command v -> Env v -> These (Output v) (Output v)
forall v. Command v -> Env v -> Result v
evalCommand Command v
c2 (Val v
y Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
evalCoterm (PlusMatch Command v
_ Command v
_) Env v
_ Val v
v = String -> These (Output v) (Output v)
forall a. HasCallStack => String -> a
error (String -> These (Output v) (Output v))
-> String -> These (Output v) (Output v)
forall a b. (a -> b) -> a -> b
$ String
"PlusMatch: not a sum: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall v. Val v -> String
show' Val v
v
evalCoterm (HomCointro Term v
t Coterm v
k) Env v
env Val v
f =
  case Term v -> Env v -> These (Output v) (Val v)
forall v. Term v -> Env v -> These (Output v) (Val v)
evalTerm Term v
t Env v
env of
    This Output v
out -> Output v -> These (Output v) (Output v)
forall a b. a -> These a b
This Output v
out
    That Val v
arg -> case Val v
f of
      VFun Val v -> These (Output v) (Output v)
g -> case Val v -> These (Output v) (Output v)
g Val v
arg of
        This Output v
out -> Output v -> These (Output v) (Output v)
forall a b. a -> These a b
This Output v
out
        That (Int
_, Val v
v) -> Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k Env v
env Val v
v
        These Output v
out (Int
_, Val v
v) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
out (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k Env v
env Val v
v)
      Val v
_ -> String -> These (Output v) (Output v)
forall a. HasCallStack => String -> a
error String
"HomCointro: not a function"
    These Output v
res Val v
arg -> case Val v
f of
      VFun Val v -> These (Output v) (Output v)
g -> case Val v -> These (Output v) (Output v)
g Val v
arg of
        This Output v
out -> Output v -> Output v -> These (Output v) (Output v)
forall a b. a -> b -> These a b
These Output v
res Output v
out
        That (Int
_, Val v
v) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
res (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k Env v
env Val v
v)
        These Output v
out (Int
_, Val v
v) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (Output v -> Output v -> Output v
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge Output v
res Output v
out) (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k Env v
env Val v
v)
      Val v
_ -> String -> These (Output v) (Output v)
forall a. HasCallStack => String -> a
error String
"HomCointro: not a function"
  where
    combine :: (a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (a, Val v)
res (This (a, b)
res') = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
res'
    combine (a, Val v)
res (That (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
foc
    combine (a, Val v)
res (These (a, b)
res' (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These ((a, Val v) -> (a, b) -> (a, Val v)
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge (a, Val v)
res (a, b)
res') (a, b)
foc
    merge :: (a, b) -> (a, b) -> (a, Val v)
merge (a
i, b
_) (a
j, b
_) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
i a
j, Val v
forall v. Val v
VUnit)
evalCoterm (GradedHomCointro Term v
t [Coterm v]
coterms) Env v
env Val v
f =
  case Term v -> Env v -> These (Output v) (Val v)
forall v. Term v -> Env v -> These (Output v) (Val v)
evalTerm Term v
t Env v
env of
    This Output v
out -> Output v -> These (Output v) (Output v)
forall a b. a -> These a b
This Output v
out
    That Val v
arg -> case Val v
f of
      VGradedFun Val v -> These (Output v) (Output v)
g -> case Val v -> These (Output v) (Output v)
g Val v
arg of
        This Output v
out -> Output v -> These (Output v) (Output v)
forall a b. a -> These a b
This Output v
out
        That (Int
slot, Val v
v) -> Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm ([Coterm v]
coterms [Coterm v] -> Int -> Coterm v
forall a. HasCallStack => [a] -> Int -> a
!! Int
slot) Env v
env Val v
v
        These Output v
out (Int
slot, Val v
v) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
out (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm ([Coterm v]
coterms [Coterm v] -> Int -> Coterm v
forall a. HasCallStack => [a] -> Int -> a
!! Int
slot) Env v
env Val v
v)
      Val v
_ -> String -> These (Output v) (Output v)
forall a. HasCallStack => String -> a
error String
"GradedHomCointro: not a graded function"
    These Output v
res Val v
arg -> case Val v
f of
      VGradedFun Val v -> These (Output v) (Output v)
g -> case Val v -> These (Output v) (Output v)
g Val v
arg of
        This Output v
out -> Output v -> Output v -> These (Output v) (Output v)
forall a b. a -> b -> These a b
These Output v
res Output v
out
        That (Int
slot, Val v
v) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
res (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm ([Coterm v]
coterms [Coterm v] -> Int -> Coterm v
forall a. HasCallStack => [a] -> Int -> a
!! Int
slot) Env v
env Val v
v)
        These Output v
out (Int
slot, Val v
v) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (Output v -> Output v -> Output v
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge Output v
res Output v
out) (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm ([Coterm v]
coterms [Coterm v] -> Int -> Coterm v
forall a. HasCallStack => [a] -> Int -> a
!! Int
slot) Env v
env Val v
v)
      Val v
_ -> String -> These (Output v) (Output v)
forall a. HasCallStack => String -> a
error String
"GradedHomCointro: not a graded function"
  where
    combine :: (a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (a, Val v)
res (This (a, b)
res') = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
res'
    combine (a, Val v)
res (That (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
foc
    combine (a, Val v)
res (These (a, b)
res' (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These ((a, Val v) -> (a, b) -> (a, Val v)
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge (a, Val v)
res (a, b)
res') (a, b)
foc
    merge :: (a, b) -> (a, b) -> (a, Val v)
merge (a
i, b
_) (a
j, b
_) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
i a
j, Val v
forall v. Val v
VUnit)
evalCoterm (ThenCointro Coterm v
k1 Coterm v
k2) Env v
env Val v
val =
  case Val v
val of
    VThen Val v
fwdA Val v -> These (Output v) (Output v)
cont ->
      case Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k1 Env v
env Val v
fwdA of
        This (Int
_, Val v
residual) ->
          case Val v -> These (Output v) (Output v)
cont Val v
residual of
            This Output v
out -> Output v -> These (Output v) (Output v)
forall a b. a -> These a b
This Output v
out
            That (Int
_, Val v
fwdB) -> Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k2 Env v
env Val v
fwdB
            These Output v
out (Int
_, Val v
fwdB) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
out (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k2 Env v
env Val v
fwdB)
        That (Int
_, Val v
residual) ->
          case Val v -> These (Output v) (Output v)
cont Val v
residual of
            This Output v
out -> Output v -> These (Output v) (Output v)
forall a b. a -> These a b
This Output v
out
            That (Int
_, Val v
fwdB) -> Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k2 Env v
env Val v
fwdB
            These Output v
out (Int
_, Val v
fwdB) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
out (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k2 Env v
env Val v
fwdB)
        These Output v
_ (Int
_, Val v
residual) ->
          case Val v -> These (Output v) (Output v)
cont Val v
residual of
            This Output v
out -> Output v -> These (Output v) (Output v)
forall a b. a -> These a b
This Output v
out
            That (Int
_, Val v
fwdB) -> Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k2 Env v
env Val v
fwdB
            These Output v
out (Int
_, Val v
fwdB) -> Output v
-> These (Output v) (Output v) -> These (Output v) (Output v)
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
out (Coterm v -> Env v -> Val v -> These (Output v) (Output v)
forall v. Coterm v -> Env v -> Val v -> Result v
evalCoterm Coterm v
k2 Env v
env Val v
fwdB)
    Val v
_ -> String -> These (Output v) (Output v)
forall a. HasCallStack => String -> a
error String
"ThenCointro: expected VThen"
  where
    combine :: (a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (a, Val v)
res (This (a, b)
res') = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
res'
    combine (a, Val v)
res (That (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
foc
    combine (a, Val v)
res (These (a, b)
res' (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These ((a, Val v) -> (a, b) -> (a, Val v)
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge (a, Val v)
res (a, b)
res') (a, b)
foc
    merge :: (a, b) -> (a, b) -> (a, Val v)
merge (a
i, b
_) (a
j, b
_) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
i a
j, Val v
forall v. Val v
VUnit)

show' :: Val v -> String
show' :: forall v. Val v -> String
show' Val v
VUnit = String
"VUnit"
show' (VPair Val v
_ Val v
_) = String
"VPair"
show' (VLeft Val v
_) = String
"VLeft"
show' (VRight Val v
_) = String
"VRight"
show' (VFun Val v -> Result v
_) = String
"VFun"
show' (VGradedFun Val v -> Result v
_) = String
"VGradedFun"
show' (VThen Val v
_ Val v -> Result v
_) = String
"VThen"
show' (VEmbed v
_) = String
"VEmbed"

-- ---------------------------------------------------------------------------
-- SMC SMC compiler
-- ---------------------------------------------------------------------------

-- | Type synonym for the free symmetric monoidal target.
--
-- @SMC (->)@ is the free SMC over plain functions.  Boundaries are still
-- expressed with 'These' at the value level, but the free category itself
-- uses the cartesian @(,)@ tensor for 'SMCPar' wiring rather than the
-- inclusive 'These' tensor.  This avoids the impossibility of a 'Traced'
-- instance for 'These'.
type SMCThese = SMC (,) (->)

-- ---------------------------------------------------------------------------

commandToSMC :: Command v -> SMCThese (Env v) (Result v)
commandToSMC :: forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC (Cut Term v
t Coterm v
k) = (Env v -> Result v) -> SMC (,) (->) (Env v) (Result v)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift ((Env v -> Result v) -> SMC (,) (->) (Env v) (Result v))
-> (Env v -> Result v) -> SMC (,) (->) (Env v) (Result v)
forall a b. (a -> b) -> a -> b
$ \Env v
env ->
  case Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (These (Int, Val v) (Val v))
-> Env v -> These (Int, Val v) (Val v)
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Term v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (These (Int, Val v) (Val v))
forall v. Term v -> SMCThese (Env v) (These (Output v) (Val v))
termToSMC Term v
t) Env v
env of
    This (Int, Val v)
out -> (Int, Val v) -> Result v
forall a b. a -> These a b
This (Int, Val v)
out
    That Val v
val -> Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v, Val v)
  (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v, Val v)
     (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k) (Env v
env, Val v
val)
    These (Int, Val v)
res Val v
val -> (Int, Val v) -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (Int, Val v)
res (Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v, Val v)
  (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v, Val v)
     (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k) (Env v
env, Val v
val))
  where
    combine :: (a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (a, Val v)
res (This (a, b)
res') = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
res'
    combine (a, Val v)
res (That (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
foc
    combine (a, Val v)
res (These (a, b)
res' (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These ((a, Val v) -> (a, b) -> (a, Val v)
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge (a, Val v)
res (a, b)
res') (a, b)
foc
    merge :: (a, b) -> (a, b) -> (a, Val v)
merge (a
i, b
_) (a
j, b
_) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
i a
j, Val v
forall v. Val v
VUnit)

termToSMC :: Term v -> SMCThese (Env v) (These (Output v) (Val v))
termToSMC :: forall v. Term v -> SMCThese (Env v) (These (Output v) (Val v))
termToSMC (Embed Value v
v) = (Env v -> These (Output v) (Val v))
-> SMC (,) (->) (Env v) (These (Output v) (Val v))
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift ((Env v -> These (Output v) (Val v))
 -> SMC (,) (->) (Env v) (These (Output v) (Val v)))
-> (Env v -> These (Output v) (Val v))
-> SMC (,) (->) (Env v) (These (Output v) (Val v))
forall a b. (a -> b) -> a -> b
$ \Env v
env -> Val v -> These (Output v) (Val v)
forall a b. b -> These a b
That (Value v -> Env v -> Val v
forall v. Value v -> Env v -> Val v
evalValue Value v
v Env v
env)
termToSMC (Mu Command v
cmd) = (Env v -> These (Output v) (Val v))
-> SMC (,) (->) (Env v) (These (Output v) (Val v))
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift ((Env v -> These (Output v) (Val v))
 -> SMC (,) (->) (Env v) (These (Output v) (Val v)))
-> (Env v -> These (Output v) (Val v))
-> SMC (,) (->) (Env v) (These (Output v) (Val v))
forall a b. (a -> b) -> a -> b
$ \Env v
env ->
  case Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (These (Output v) (Output v))
-> Env v -> These (Output v) (Output v)
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Command v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (These (Output v) (Output v))
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC Command v
cmd) Env v
env of
    This Output v
out -> Output v -> These (Output v) (Val v)
forall a b. a -> These a b
This Output v
out
    That (Int
0, Val v
val) -> Val v -> These (Output v) (Val v)
forall a b. b -> These a b
That Val v
val
    That Output v
out -> Output v -> These (Output v) (Val v)
forall a b. a -> These a b
This Output v
out
    These Output v
res (Int
0, Val v
val) -> Output v -> Val v -> These (Output v) (Val v)
forall a b. a -> b -> These a b
These Output v
res Val v
val
    These Output v
res Output v
foc -> Output v -> Val v -> These (Output v) (Val v)
forall a b. a -> b -> These a b
These Output v
res (Output v -> Val v
forall a b. (a, b) -> b
snd Output v
foc)
termToSMC (ThenComatch Command v
cmd) = (Env v -> These (Output v) (Val v))
-> SMC (,) (->) (Env v) (These (Output v) (Val v))
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift ((Env v -> These (Output v) (Val v))
 -> SMC (,) (->) (Env v) (These (Output v) (Val v)))
-> (Env v -> These (Output v) (Val v))
-> SMC (,) (->) (Env v) (These (Output v) (Val v))
forall a b. (a -> b) -> a -> b
$ \Env v
env ->
  let fwdA :: Val v
fwdA = case Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (These (Output v) (Output v))
-> Env v -> These (Output v) (Output v)
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Command v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (These (Output v) (Output v))
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC Command v
cmd) Env v
env of
        That (Int
1, Val v
v) -> Val v
v
        These Output v
_ (Int
1, Val v
v) -> Val v
v
        These (Output v) (Output v)
_ -> String -> Val v
forall a. HasCallStack => String -> a
error String
"ThenComatch: expected slot 1 for fwd a"
      bwCont :: Val v -> These (Output v) (Output v)
bwCont Val v
bwA = Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (These (Output v) (Output v))
-> Env v -> These (Output v) (Output v)
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Command v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (These (Output v) (Output v))
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC Command v
cmd) (Val v
bwA Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
   in Val v -> These (Output v) (Val v)
forall a b. b -> These a b
That (Val v -> (Val v -> These (Output v) (Output v)) -> Val v
forall v. Val v -> (Val v -> Result v) -> Val v
VThen Val v
fwdA Val v -> These (Output v) (Output v)
bwCont)

cotermToSMC :: Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC :: forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC (Covar Int
i) = ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (((Env v, Val v) -> Result v)
 -> SMC (,) (->) (Env v, Val v) (Result v))
-> ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall a b. (a -> b) -> a -> b
$ \(Env v
_, Val v
val) ->
  if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Output v -> Result v
forall a b. b -> These a b
That (Int
0, Val v
val) else Output v -> Result v
forall a b. a -> These a b
This (Int
i, Val v
val)
cotermToSMC (Comu Command v
cmd) = ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (((Env v, Val v) -> Result v)
 -> SMC (,) (->) (Env v, Val v) (Result v))
-> ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall a b. (a -> b) -> a -> b
$ \(Env v
env, Val v
val) ->
  Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (Result v)
-> Env v -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Command v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (Result v)
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC Command v
cmd) (Val v
val Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
cotermToSMC (TensorMatch Command v
cmd) = ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (((Env v, Val v) -> Result v)
 -> SMC (,) (->) (Env v, Val v) (Result v))
-> ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall a b. (a -> b) -> a -> b
$ \(Env v
env, Val v
val) ->
  case Val v
val of
    VPair Val v
x Val v
y -> Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (Result v)
-> Env v -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Command v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (Result v)
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC Command v
cmd) (Val v
x Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Val v
y Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
    Val v
_ -> String -> Result v
forall a. HasCallStack => String -> a
error (String -> Result v) -> String -> Result v
forall a b. (a -> b) -> a -> b
$ String
"TensorMatch: not a pair: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall v. Val v -> String
show' Val v
val
cotermToSMC (PlusMatch Command v
c1 Command v
c2) = ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (((Env v, Val v) -> Result v)
 -> SMC (,) (->) (Env v, Val v) (Result v))
-> ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall a b. (a -> b) -> a -> b
$ \(Env v
env, Val v
val) ->
  case Val v
val of
    VLeft Val v
x -> Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (Result v)
-> Env v -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Command v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (Result v)
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC Command v
c1) (Val v
x Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
    VRight Val v
y -> Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (Result v)
-> Env v -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Command v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (Result v)
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC Command v
c2) (Val v
y Val v -> Env v -> Env v
forall a. a -> [a] -> [a]
: Env v
env)
    Val v
_ -> String -> Result v
forall a. HasCallStack => String -> a
error (String -> Result v) -> String -> Result v
forall a b. (a -> b) -> a -> b
$ String
"PlusMatch: not a sum: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Val v -> String
forall v. Val v -> String
show' Val v
val
cotermToSMC (HomCointro Term v
t Coterm v
k) = ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (((Env v, Val v) -> Result v)
 -> SMC (,) (->) (Env v, Val v) (Result v))
-> ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall a b. (a -> b) -> a -> b
$ \(Env v
env, Val v
val) ->
  case Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (These (Output v) (Val v))
-> Env v -> These (Output v) (Val v)
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Term v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (These (Output v) (Val v))
forall v. Term v -> SMCThese (Env v) (These (Output v) (Val v))
termToSMC Term v
t) Env v
env of
    This Output v
out -> Output v -> Result v
forall a b. a -> These a b
This Output v
out
    That Val v
arg -> case Val v
val of
      VFun Val v -> Result v
f -> case Val v -> Result v
f Val v
arg of
        This Output v
out -> Output v -> Result v
forall a b. a -> These a b
This Output v
out
        That (Int
_, Val v
v) -> SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k) (Env v
env, Val v
v)
        These Output v
out (Int
_, Val v
v) -> Output v -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
out (SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k) (Env v
env, Val v
v))
      Val v
_ -> String -> Result v
forall a. HasCallStack => String -> a
error String
"HomCointro: not a function"
    These Output v
res Val v
arg -> case Val v
val of
      VFun Val v -> Result v
f -> case Val v -> Result v
f Val v
arg of
        This Output v
out -> Output v -> Output v -> Result v
forall a b. a -> b -> These a b
These Output v
res Output v
out
        That (Int
_, Val v
v) -> Output v -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
res (SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k) (Env v
env, Val v
v))
        These Output v
out (Int
_, Val v
v) -> Output v -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (Output v -> Output v -> Output v
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge Output v
res Output v
out) (SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k) (Env v
env, Val v
v))
      Val v
_ -> String -> Result v
forall a. HasCallStack => String -> a
error String
"HomCointro: not a function"
  where
    combine :: (a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (a, Val v)
res (This (a, b)
res') = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
res'
    combine (a, Val v)
res (That (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
foc
    combine (a, Val v)
res (These (a, b)
res' (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These ((a, Val v) -> (a, b) -> (a, Val v)
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge (a, Val v)
res (a, b)
res') (a, b)
foc
    merge :: (a, b) -> (a, b) -> (a, Val v)
merge (a
i, b
_) (a
j, b
_) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
i a
j, Val v
forall v. Val v
VUnit)
cotermToSMC (GradedHomCointro Term v
t [Coterm v]
coterms) = ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (((Env v, Val v) -> Result v)
 -> SMC (,) (->) (Env v, Val v) (Result v))
-> ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall a b. (a -> b) -> a -> b
$ \(Env v
env, Val v
val) ->
  case Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env v)
  (These (Output v) (Val v))
-> Env v -> These (Output v) (Val v)
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Term v
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env v)
     (These (Output v) (Val v))
forall v. Term v -> SMCThese (Env v) (These (Output v) (Val v))
termToSMC Term v
t) Env v
env of
    This Output v
out -> Output v -> Result v
forall a b. a -> These a b
This Output v
out
    That Val v
arg -> case Val v
val of
      VGradedFun Val v -> Result v
f -> case Val v -> Result v
f Val v
arg of
        This Output v
out -> Output v -> Result v
forall a b. a -> These a b
This Output v
out
        That (Int
slot, Val v
v) -> SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC ([Coterm v]
coterms [Coterm v] -> Int -> Coterm v
forall a. HasCallStack => [a] -> Int -> a
!! Int
slot)) (Env v
env, Val v
v)
        These Output v
out (Int
slot, Val v
v) -> Output v -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
out (SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC ([Coterm v]
coterms [Coterm v] -> Int -> Coterm v
forall a. HasCallStack => [a] -> Int -> a
!! Int
slot)) (Env v
env, Val v
v))
      Val v
_ -> String -> Result v
forall a. HasCallStack => String -> a
error String
"GradedHomCointro: not a graded function"
    These Output v
res Val v
arg -> case Val v
val of
      VGradedFun Val v -> Result v
f -> case Val v -> Result v
f Val v
arg of
        This Output v
out -> Output v -> Output v -> Result v
forall a b. a -> b -> These a b
These Output v
res Output v
out
        That (Int
slot, Val v
v) -> Output v -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
res (SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC ([Coterm v]
coterms [Coterm v] -> Int -> Coterm v
forall a. HasCallStack => [a] -> Int -> a
!! Int
slot)) (Env v
env, Val v
v))
        These Output v
out (Int
slot, Val v
v) -> Output v -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (Output v -> Output v -> Output v
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge Output v
res Output v
out) (SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC ([Coterm v]
coterms [Coterm v] -> Int -> Coterm v
forall a. HasCallStack => [a] -> Int -> a
!! Int
slot)) (Env v
env, Val v
v))
      Val v
_ -> String -> Result v
forall a. HasCallStack => String -> a
error String
"GradedHomCointro: not a graded function"
  where
    combine :: (a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (a, Val v)
res (This (a, b)
res') = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
res'
    combine (a, Val v)
res (That (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
foc
    combine (a, Val v)
res (These (a, b)
res' (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These ((a, Val v) -> (a, b) -> (a, Val v)
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge (a, Val v)
res (a, b)
res') (a, b)
foc
    merge :: (a, b) -> (a, b) -> (a, Val v)
merge (a
i, b
_) (a
j, b
_) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
i a
j, Val v
forall v. Val v
VUnit)
cotermToSMC (ThenCointro Coterm v
k1 Coterm v
k2) = ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (((Env v, Val v) -> Result v)
 -> SMC (,) (->) (Env v, Val v) (Result v))
-> ((Env v, Val v) -> Result v)
-> SMC (,) (->) (Env v, Val v) (Result v)
forall a b. (a -> b) -> a -> b
$ \(Env v
env, Val v
val) ->
  case Val v
val of
    VThen Val v
fwdA Val v -> Result v
cont ->
      case SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k1) (Env v
env, Val v
fwdA) of
        This (Int
_, Val v
residual) -> Val v -> Result v
dispatch Val v
residual
        That (Int
_, Val v
residual) -> Val v -> Result v
dispatch Val v
residual
        These Output v
_ (Int
_, Val v
residual) -> Val v -> Result v
dispatch Val v
residual
      where
        dispatch :: Val v -> Result v
dispatch Val v
residual =
          case Val v -> Result v
cont Val v
residual of
            This Output v
out -> Output v -> Result v
forall a b. a -> These a b
This Output v
out
            That (Int
_, Val v
fwdB) -> SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k2) (Env v
env, Val v
fwdB)
            These Output v
out (Int
_, Val v
fwdB) -> Output v -> Result v -> Result v
forall {a} {v} {b}.
Ord a =>
(a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine Output v
out (SMC (,) (->) (Env v, Val v) (Result v)
-> (Env v, Val v) -> Result v
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (Coterm v -> SMC (,) (->) (Env v, Val v) (Result v)
forall v. Coterm v -> SMCThese (Env v, Val v) (Result v)
cotermToSMC Coterm v
k2) (Env v
env, Val v
fwdB))
        combine :: (a, Val v) -> These (a, b) (a, b) -> These (a, Val v) (a, b)
combine (a, Val v)
res (This (a, b)
res') = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
res'
        combine (a, Val v)
res (That (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These (a, Val v)
res (a, b)
foc
        combine (a, Val v)
res (These (a, b)
res' (a, b)
foc) = (a, Val v) -> (a, b) -> These (a, Val v) (a, b)
forall a b. a -> b -> These a b
These ((a, Val v) -> (a, b) -> (a, Val v)
forall {a} {b} {b} {v}. Ord a => (a, b) -> (a, b) -> (a, Val v)
merge (a, Val v)
res (a, b)
res') (a, b)
foc
        merge :: (a, b) -> (a, b) -> (a, Val v)
merge (a
i, b
_) (a
j, b
_) = (a -> a -> a
forall a. Ord a => a -> a -> a
max a
i a
j, Val v
forall v. Val v
VUnit)
    Val v
_ -> String -> Result v
forall a. HasCallStack => String -> a
error String
"ThenCointro: expected VThen"

-- ---------------------------------------------------------------------------
-- Process interpreter
-- ---------------------------------------------------------------------------

-- | Streaming interpreter: each input is a fresh environment, each output is
-- the focus value of the term.  Residual escape is a run-time error, which is
-- the expected behaviour for a closed term consumed by a process.
evalProcess :: Term v -> Process (Env v) (Val v)
evalProcess :: forall v. Term v -> Process (Env v) (Val v)
evalProcess Term v
t = (Env v -> Env v)
-> (Env v -> Env v -> Env v)
-> (Env v -> Val v)
-> Process (Env v) (Val v)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process Env v -> Env v
forall {p}. p -> p
inject Env v -> Env v -> Env v
forall {p} {p}. p -> p -> p
step Env v -> Val v
extract
  where
    inject :: p -> p
inject p
env = p
env
    step :: p -> p -> p
step p
_ p
env = p
env
    extract :: Env v -> Val v
extract Env v
env =
      case Term v -> Env v -> These (Output v) (Val v)
forall v. Term v -> Env v -> These (Output v) (Val v)
evalTerm Term v
t Env v
env of
        That Val v
val -> Val v
val
        These (Output v) (Val v)
_ -> String -> Val v
forall a. HasCallStack => String -> a
error String
"evalProcess: term escaped to a covariable"

-- ---------------------------------------------------------------------------
-- Then as polynomial optic
-- ---------------------------------------------------------------------------

-- | Build a 'Then'-style lens from explicit forward and backward maps.
--
-- The forward map @a -> b@ and backward map @a -> b -> a@ form a dependent
-- lens @Mono a a -> Mono b b@ in 'Circuit.Poly'.
thenLens ::
  (Val v -> Val v) ->
  (Val v -> Val v -> Val v) ->
  Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v))
thenLens :: forall v.
(Val v -> Val v)
-> (Val v -> Val v -> Val v)
-> Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v))
thenLens Val v -> Val v
f Val v -> Val v -> Val v
g = (Val v -> Val v)
-> (Val v -> Val v -> Val v)
-> Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v))
forall a b db da.
(a -> b) -> (a -> db -> da) -> Morphism (Mono da a) (Mono db b)
lens Val v -> Val v
f (\Val v
a Val v
db -> Val v -> Val v -> Val v
g Val v
a Val v
db)

-- | Apply a 'Then' lens to an input value, returning the forward output and
-- the backward continuation.
applyThen ::
  Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v)) ->
  Val v ->
  (Val v, Val v -> Val v)
applyThen :: forall v.
Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v))
-> Val v -> (Val v, Val v -> Val v)
applyThen Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v))
m Val v
a = Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v))
-> Val v -> (Val v, Val v -> Val v)
forall da a db b.
Morphism (Mono da a) (Mono db b) -> a -> (b, db -> da)
applyLens Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v))
m Val v
a

-- ---------------------------------------------------------------------------
-- Regression tests
-- ---------------------------------------------------------------------------

-- | Identity via Hom: @(\x -> x) VUnit@.
testId :: Result ()
testId :: Result ()
testId =
  Command () -> Env () -> Result ()
forall v. Command v -> Env v -> Result v
evalCommand
    ( Term () -> Coterm () -> Command ()
forall v. Term v -> Coterm v -> Command v
Cut
        (Value () -> Term ()
forall v. Value v -> Term v
Embed (Command () -> Value ()
forall v. Command v -> Value v
HomComatch (Term () -> Coterm () -> Command ()
forall v. Term v -> Coterm v -> Command v
Cut (Value () -> Term ()
forall v. Value v -> Term v
Embed (Int -> Value ()
forall v. Int -> Value v
Var Int
0)) (Int -> Coterm ()
forall v. Int -> Coterm v
Covar Int
0))))
        (Term () -> Coterm () -> Coterm ()
forall v. Term v -> Coterm v -> Coterm v
HomCointro (Value () -> Term ()
forall v. Value v -> Term v
Embed (Int -> Value ()
forall v. Int -> Value v
Var Int
0)) (Int -> Coterm ()
forall v. Int -> Coterm v
Covar Int
0))
    )
    [Val ()
forall v. Val v
VUnit]

-- | Thread a Double through Then.
testThen :: Result Double
testThen :: Result Double
testThen =
  let val :: Val Double
val = Val Double -> (Val Double -> Result Double) -> Val Double
forall v. Val v -> (Val v -> Result v) -> Val v
VThen (Double -> Val Double
forall v. v -> Val v
VEmbed Double
1.0) (\Val Double
x -> Output Double -> Result Double
forall a b. b -> These a b
That (Int
0, Val Double
x))
   in Command Double -> Env Double -> Result Double
forall v. Command v -> Env v -> Result v
evalCommand
        ( Term Double -> Coterm Double -> Command Double
forall v. Term v -> Coterm v -> Command v
Cut
            (Value Double -> Term Double
forall v. Value v -> Term v
Embed (Val Double -> Value Double
forall v. Val v -> Value v
Lit Val Double
val))
            ( Coterm Double -> Coterm Double -> Coterm Double
forall v. Coterm v -> Coterm v -> Coterm v
ThenCointro
                (Command Double -> Coterm Double
forall v. Command v -> Coterm v
Comu (Term Double -> Coterm Double -> Command Double
forall v. Term v -> Coterm v -> Command v
Cut (Value Double -> Term Double
forall v. Value v -> Term v
Embed (Int -> Value Double
forall v. Int -> Value v
Var Int
0)) (Int -> Coterm Double
forall v. Int -> Coterm v
Covar Int
1)))
                (Command Double -> Coterm Double
forall v. Command v -> Coterm v
Comu (Term Double -> Coterm Double -> Command Double
forall v. Term v -> Coterm v -> Command v
Cut (Value Double -> Term Double
forall v. Value v -> Term v
Embed (Int -> Value Double
forall v. Int -> Value v
Var Int
0)) (Int -> Coterm Double
forall v. Int -> Coterm v
Covar Int
0)))
            )
        )
        []

-- | Identity test compiled to SMC.
testIdLoop :: Result ()
testIdLoop :: Result ()
testIdLoop =
  Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env ())
  (Result ())
-> Env () -> Result ()
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval
    ( Command ()
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env ())
     (Result ())
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC
        ( Term () -> Coterm () -> Command ()
forall v. Term v -> Coterm v -> Command v
Cut
            (Value () -> Term ()
forall v. Value v -> Term v
Embed (Command () -> Value ()
forall v. Command v -> Value v
HomComatch (Term () -> Coterm () -> Command ()
forall v. Term v -> Coterm v -> Command v
Cut (Value () -> Term ()
forall v. Value v -> Term v
Embed (Int -> Value ()
forall v. Int -> Value v
Var Int
0)) (Int -> Coterm ()
forall v. Int -> Coterm v
Covar Int
0))))
            (Term () -> Coterm () -> Coterm ()
forall v. Term v -> Coterm v -> Coterm v
HomCointro (Value () -> Term ()
forall v. Value v -> Term v
Embed (Int -> Value ()
forall v. Int -> Value v
Var Int
0)) (Int -> Coterm ()
forall v. Int -> Coterm v
Covar Int
0))
        )
    )
    [Val ()
forall v. Val v
VUnit]

-- | Then test compiled to SMC.
testThenLoop :: Result Double
testThenLoop :: Result Double
testThenLoop =
  let val :: Val Double
val = Val Double -> (Val Double -> Result Double) -> Val Double
forall v. Val v -> (Val v -> Result v) -> Val v
VThen (Double -> Val Double
forall v. v -> Val v
VEmbed Double
1.0) (\Val Double
x -> Output Double -> Result Double
forall a b. b -> These a b
That (Int
0, Val Double
x))
   in Syntax
  (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
  (->)
  (Env Double)
  (Result Double)
-> Env Double -> Result Double
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval
        ( Command Double
-> Syntax
     (SigCompose :+: (SigPar (,) :+: SigSwap (,)))
     (->)
     (Env Double)
     (Result Double)
forall v. Command v -> SMCThese (Env v) (Result v)
commandToSMC
            ( Term Double -> Coterm Double -> Command Double
forall v. Term v -> Coterm v -> Command v
Cut
                (Value Double -> Term Double
forall v. Value v -> Term v
Embed (Val Double -> Value Double
forall v. Val v -> Value v
Lit Val Double
val))
                ( Coterm Double -> Coterm Double -> Coterm Double
forall v. Coterm v -> Coterm v -> Coterm v
ThenCointro
                    (Command Double -> Coterm Double
forall v. Command v -> Coterm v
Comu (Term Double -> Coterm Double -> Command Double
forall v. Term v -> Coterm v -> Command v
Cut (Value Double -> Term Double
forall v. Value v -> Term v
Embed (Int -> Value Double
forall v. Int -> Value v
Var Int
0)) (Int -> Coterm Double
forall v. Int -> Coterm v
Covar Int
1)))
                    (Command Double -> Coterm Double
forall v. Command v -> Coterm v
Comu (Term Double -> Coterm Double -> Command Double
forall v. Term v -> Coterm v -> Command v
Cut (Value Double -> Term Double
forall v. Value v -> Term v
Embed (Int -> Value Double
forall v. Int -> Value v
Var Int
0)) (Int -> Coterm Double
forall v. Int -> Coterm v
Covar Int
0)))
                )
            )
        )
        [Val Double
val]