{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Explicitly type-preserving bracket abstraction, a la Oleg Kiselyov.
-- Turn elaborated, type-indexed terms into variableless, type-indexed
-- terms with only constants and application.
--
-- For more information, see:
--
--   https://byorgey.wordpress.com/2023/07/13/compiling-to-intrinsically-typed-combinators/
module Swarm.Game.World.Abstract where

import Data.Kind (Type)
import Swarm.Game.World.Typecheck (Applicable (..), Const (..), HasConst (..), Idx (..), TTerm (..), ($$.), (.$$), (.$$.))

------------------------------------------------------------
-- Bracket abstraction
------------------------------------------------------------

--------------------------------------------------
-- Closed terms

-- | Closed, fully abstracted terms.  All computation is represented
--   by combinators.  This is the ultimate target for the bracket
--   abstraction operation.
data BTerm :: Type -> Type where
  BApp :: BTerm (a -> b) -> BTerm a -> BTerm b
  BConst :: Const a -> BTerm a

deriving instance Show (BTerm t)

instance Applicable BTerm where
  $$ :: forall a b. BTerm (a -> b) -> BTerm a -> BTerm b
($$) = BTerm (a -> b) -> BTerm a -> BTerm b
forall a b. BTerm (a -> b) -> BTerm a -> BTerm b
BApp

instance HasConst BTerm where
  embed :: forall a. Const a -> BTerm a
embed = Const a -> BTerm a
forall a. Const a -> BTerm a
BConst

--------------------------------------------------
-- Open terms

-- | These explicitly open terms are an intermediate stage in the
--   bracket abstraction algorithm, /i.e./ they represent terms which have
--   been only partially abstracted.
data OTerm :: [Type] -> Type -> Type where
  -- Embedded closed term.
  E :: BTerm a -> OTerm g a
  -- Reference to the innermost/top environment variable, i.e. Z
  V :: OTerm (a ': g) a
  -- Internalize the topmost env variable as a function argument
  N :: OTerm g (a -> b) -> OTerm (a ': g) b
  -- Ignore the topmost env variable
  W :: OTerm g b -> OTerm (a ': g) b

instance HasConst (OTerm g) where
  embed :: forall a. Const a -> OTerm g a
embed = BTerm a -> OTerm g a
forall a (g :: [*]). BTerm a -> OTerm g a
E (BTerm a -> OTerm g a)
-> (Const a -> BTerm a) -> Const a -> OTerm g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const a -> BTerm a
forall a. Const a -> BTerm a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed

-- | Bracket abstraction: convert the 'TTerm' to an 'OTerm', then
--   project out the embedded 'BTerm'.  GHC can see this is total
--   since 'E' is the only constructor that can produce an 'OTerm'
--   with an empty environment.
bracket :: TTerm '[] a -> BTerm a
bracket :: forall a. TTerm '[] a -> BTerm a
bracket TTerm '[] a
t = case TTerm '[] a -> OTerm '[] a
forall (g :: [*]) a. TTerm g a -> OTerm g a
conv TTerm '[] a
t of
  E BTerm a
t' -> BTerm a
t'

-- | Type-preserving conversion from 'TTerm' to 'OTerm' ('conv' + the
--   'Applicable' instance).  Taken directly from Kiselyov.
conv :: TTerm g a -> OTerm g a
conv :: forall (g :: [*]) a. TTerm g a -> OTerm g a
conv (TVar Idx g a
VZ) = OTerm g a
OTerm (a : g) a
forall a (g :: [*]). OTerm (a : g) a
V
conv (TVar (VS Idx g a
x)) = OTerm g a -> OTerm (x : g) a
forall (g :: [*]) b a. OTerm g b -> OTerm (a : g) b
W (TTerm g a -> OTerm g a
forall (g :: [*]) a. TTerm g a -> OTerm g a
conv (Idx g a -> TTerm g a
forall (a :: [*]) b. Idx a b -> TTerm a b
TVar Idx g a
x))
conv (TLam TTerm (ty1 : g) ty2
t) = case TTerm (ty1 : g) ty2 -> OTerm (ty1 : g) ty2
forall (g :: [*]) a. TTerm g a -> OTerm g a
conv TTerm (ty1 : g) ty2
t of
  OTerm (ty1 : g) ty2
V -> BTerm a -> OTerm g a
forall a (g :: [*]). BTerm a -> OTerm g a
E (Const a -> BTerm a
forall a. Const a -> BTerm a
BConst Const a
Const (ty2 -> ty2)
forall a1. Const (a1 -> a1)
I)
  E BTerm ty2
d -> BTerm a -> OTerm g a
forall a (g :: [*]). BTerm a -> OTerm g a
E (Const (ty2 -> a)
Const (ty2 -> ty1 -> ty2)
forall a1 b. Const (a1 -> b -> a1)
K Const (ty2 -> a) -> BTerm ty2 -> BTerm a
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ BTerm ty2
d)
  N OTerm g (a -> ty2)
e -> OTerm g a
OTerm g (a -> ty2)
e
  W OTerm g ty2
e -> Const (ty2 -> a)
Const (ty2 -> ty1 -> ty2)
forall a1 b. Const (a1 -> b -> a1)
K Const (ty2 -> a) -> OTerm g ty2 -> OTerm g a
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g ty2
OTerm g ty2
e
conv (TApp TTerm g (a1 -> a)
t1 TTerm g a1
t2) = TTerm g (a1 -> a) -> OTerm g (a1 -> a)
forall (g :: [*]) a. TTerm g a -> OTerm g a
conv TTerm g (a1 -> a)
t1 OTerm g (a1 -> a) -> OTerm g a1 -> OTerm g a
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ TTerm g a1 -> OTerm g a1
forall (g :: [*]) a. TTerm g a -> OTerm g a
conv TTerm g a1
t2
conv (TConst Const a
c) = Const a -> OTerm g a
forall a. Const a -> OTerm g a
forall (t :: * -> *) a. HasConst t => Const a -> t a
embed Const a
c

instance Applicable (OTerm g) where
  ($$) :: OTerm g (a -> b) -> OTerm g a -> OTerm g b
  W OTerm g (a -> b)
e1 $$ :: forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
$$ W OTerm g a
e2 = OTerm g b -> OTerm (a : g) b
forall (g :: [*]) b a. OTerm g b -> OTerm (a : g) b
W (OTerm g (a -> b)
e1 OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g a
OTerm g a
e2)
  W OTerm g (a -> b)
e $$ E BTerm a
d = OTerm g b -> OTerm (a : g) b
forall (g :: [*]) b a. OTerm g b -> OTerm (a : g) b
W (OTerm g (a -> b)
e OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ BTerm a -> OTerm g a
forall a (g :: [*]). BTerm a -> OTerm g a
E BTerm a
d)
  E BTerm (a -> b)
d $$ W OTerm g a
e = OTerm g b -> OTerm (a : g) b
forall (g :: [*]) b a. OTerm g b -> OTerm (a : g) b
W (BTerm (a -> b) -> OTerm g (a -> b)
forall a (g :: [*]). BTerm a -> OTerm g a
E BTerm (a -> b)
d OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g a
e)
  W OTerm g (a -> b)
e $$ OTerm g a
V = OTerm g (a -> b) -> OTerm (a : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N OTerm g (a -> b)
e
  OTerm g (a -> b)
V $$ W OTerm g a
e = OTerm g ((a -> b) -> b) -> OTerm ((a -> b) : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (BTerm (a -> (a -> b) -> b) -> OTerm g (a -> (a -> b) -> b)
forall a (g :: [*]). BTerm a -> OTerm g a
E (Const (((a -> b) -> a -> b) -> a -> (a -> b) -> b)
forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C Const (((a -> b) -> a -> b) -> a -> (a -> b) -> b)
-> Const ((a -> b) -> a -> b) -> BTerm (a -> (a -> b) -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. Const ((a -> b) -> a -> b)
forall a1. Const (a1 -> a1)
I) OTerm g (a -> (a -> b) -> b)
-> OTerm g a -> OTerm g ((a -> b) -> b)
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g a
e)
  W OTerm g (a -> b)
e1 $$ N OTerm g (a -> a)
e2 = OTerm g (a -> b) -> OTerm (a : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (Const ((a -> b) -> (a -> a) -> a -> b)
forall b c a1. Const ((b -> c) -> (a1 -> b) -> a1 -> c)
B Const ((a -> b) -> (a -> a) -> a -> b)
-> OTerm g (a -> b) -> OTerm g ((a -> a) -> a -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g (a -> b)
e1 OTerm g ((a -> a) -> a -> b)
-> OTerm g (a -> a) -> OTerm g (a -> b)
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g (a -> a)
OTerm g (a -> a)
e2)
  N OTerm g (a -> a -> b)
e1 $$ W OTerm g a
e2 = OTerm g (a -> b) -> OTerm (a : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (Const ((a -> a -> b) -> a -> a -> b)
forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C Const ((a -> a -> b) -> a -> a -> b)
-> OTerm g (a -> a -> b) -> OTerm g (a -> a -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g (a -> a -> b)
e1 OTerm g (a -> a -> b) -> OTerm g a -> OTerm g (a -> b)
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g a
OTerm g a
e2)
  N OTerm g (a -> a -> b)
e1 $$ N OTerm g (a -> a)
e2 = OTerm g (a -> b) -> OTerm (a : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (Const ((a -> a -> b) -> (a -> a) -> a -> b)
forall a1 b c. Const ((a1 -> b -> c) -> (a1 -> b) -> a1 -> c)
S Const ((a -> a -> b) -> (a -> a) -> a -> b)
-> OTerm g (a -> a -> b) -> OTerm g ((a -> a) -> a -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g (a -> a -> b)
e1 OTerm g ((a -> a) -> a -> b)
-> OTerm g (a -> a) -> OTerm g (a -> b)
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g (a -> a)
OTerm g (a -> a)
e2)
  N OTerm g (a -> a -> b)
e $$ OTerm g a
V = OTerm g (a -> b) -> OTerm (a : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (Const ((a -> a -> b) -> (a -> a) -> a -> b)
forall a1 b c. Const ((a1 -> b -> c) -> (a1 -> b) -> a1 -> c)
S Const ((a -> a -> b) -> (a -> a) -> a -> b)
-> OTerm g (a -> a -> b) -> OTerm g ((a -> a) -> a -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g (a -> a -> b)
e OTerm g ((a -> a) -> a -> b) -> Const (a -> a) -> OTerm g (a -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
t (a -> b) -> Const a -> t b
$$. Const (a -> a)
Const (a -> a)
forall a1. Const (a1 -> a1)
I)
  OTerm g (a -> b)
V $$ N OTerm g (a -> a)
e = OTerm g ((a -> b) -> b) -> OTerm ((a -> b) : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (BTerm (((a -> b) -> a) -> (a -> b) -> b)
-> OTerm g (((a -> b) -> a) -> (a -> b) -> b)
forall a (g :: [*]). BTerm a -> OTerm g a
E (Const (((a -> b) -> a -> b) -> ((a -> b) -> a) -> (a -> b) -> b)
forall a1 b c. Const ((a1 -> b -> c) -> (a1 -> b) -> a1 -> c)
S Const (((a -> b) -> a -> b) -> ((a -> b) -> a) -> (a -> b) -> b)
-> Const ((a -> b) -> a -> b)
-> BTerm (((a -> b) -> a) -> (a -> b) -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. Const ((a -> b) -> a -> b)
forall a1. Const (a1 -> a1)
I) OTerm g (((a -> b) -> a) -> (a -> b) -> b)
-> OTerm g ((a -> b) -> a) -> OTerm g ((a -> b) -> b)
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g (a -> a)
OTerm g ((a -> b) -> a)
e)
  E BTerm (a -> b)
d $$ N OTerm g (a -> a)
e = OTerm g (a -> b) -> OTerm (a : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (BTerm ((a -> a) -> a -> b) -> OTerm g ((a -> a) -> a -> b)
forall a (g :: [*]). BTerm a -> OTerm g a
E (Const ((a -> b) -> (a -> a) -> a -> b)
forall b c a1. Const ((b -> c) -> (a1 -> b) -> a1 -> c)
B Const ((a -> b) -> (a -> a) -> a -> b)
-> BTerm (a -> b) -> BTerm ((a -> a) -> a -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ BTerm (a -> b)
d) OTerm g ((a -> a) -> a -> b)
-> OTerm g (a -> a) -> OTerm g (a -> b)
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g (a -> a)
e)
  E BTerm (a -> b)
d $$ OTerm g a
V = OTerm g (a -> b) -> OTerm (a : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (BTerm (a -> b) -> OTerm g (a -> b)
forall a (g :: [*]). BTerm a -> OTerm g a
E BTerm (a -> b)
d)
  OTerm g (a -> b)
V $$ E BTerm a
d = OTerm g ((a -> b) -> b) -> OTerm ((a -> b) : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (BTerm ((a -> b) -> b) -> OTerm g ((a -> b) -> b)
forall a (g :: [*]). BTerm a -> OTerm g a
E (Const (((a -> b) -> a -> b) -> a -> (a -> b) -> b)
forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C Const (((a -> b) -> a -> b) -> a -> (a -> b) -> b)
-> Const ((a -> b) -> a -> b) -> BTerm (a -> (a -> b) -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. Const ((a -> b) -> a -> b)
forall a1. Const (a1 -> a1)
I BTerm (a -> (a -> b) -> b) -> BTerm a -> BTerm ((a -> b) -> b)
forall a b. BTerm (a -> b) -> BTerm a -> BTerm b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ BTerm a
d))
  N OTerm g (a -> a -> b)
e $$ E BTerm a
d = OTerm g (a -> b) -> OTerm (a : g) b
forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (BTerm ((a -> a -> b) -> a -> b)
-> OTerm g ((a -> a -> b) -> a -> b)
forall a (g :: [*]). BTerm a -> OTerm g a
E (Const
  (((a -> a -> b) -> a -> a -> b) -> a -> (a -> a -> b) -> a -> b)
forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C Const
  (((a -> a -> b) -> a -> a -> b) -> a -> (a -> a -> b) -> a -> b)
-> Const ((a -> a -> b) -> a -> a -> b)
-> BTerm (a -> (a -> a -> b) -> a -> b)
forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. Const ((a -> a -> b) -> a -> a -> b)
forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C BTerm (a -> (a -> a -> b) -> a -> b)
-> BTerm a -> BTerm ((a -> a -> b) -> a -> b)
forall a b. BTerm (a -> b) -> BTerm a -> BTerm b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ BTerm a
d) OTerm g ((a -> a -> b) -> a -> b)
-> OTerm g (a -> a -> b) -> OTerm g (a -> b)
forall a b. OTerm g (a -> b) -> OTerm g a -> OTerm g b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g (a -> a -> b)
e)
  E BTerm (a -> b)
d1 $$ E BTerm a
d2 = BTerm b -> OTerm g b
forall a (g :: [*]). BTerm a -> OTerm g a
E (BTerm (a -> b)
d1 BTerm (a -> b) -> BTerm a -> BTerm b
forall a b. BTerm (a -> b) -> BTerm a -> BTerm b
forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ BTerm a
d2)

-- There are only 15 cases above: GHC can tell that V $$ V is
-- impossible (it would be ill-typed)!