{-# 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
($$) = forall a b. BTerm (a -> b) -> BTerm a -> BTerm b
BApp

instance HasConst BTerm where
  embed :: forall a. Const a -> BTerm a
embed = 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 = forall a (g :: [*]). BTerm a -> OTerm g a
E forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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) = forall a (g :: [*]). OTerm (a : g) a
V
conv (TVar (VS Idx g a
x)) = forall (g :: [*]) b a. OTerm g b -> OTerm (a : g) b
W (forall (g :: [*]) a. TTerm g a -> OTerm g a
conv (forall (a :: [*]) b. Idx a b -> TTerm a b
TVar Idx g a
x))
conv (TLam TTerm (ty1 : g) ty2
t) = case forall (g :: [*]) a. TTerm g a -> OTerm g a
conv TTerm (ty1 : g) ty2
t of
  OTerm (ty1 : g) ty2
V -> forall a (g :: [*]). BTerm a -> OTerm g a
E (forall a. Const a -> BTerm a
BConst forall a1. Const (a1 -> a1)
I)
  E BTerm ty2
d -> forall a (g :: [*]). BTerm a -> OTerm g a
E (forall a1 b. Const (a1 -> b -> a1)
K 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 -> ty2)
e
  W OTerm g ty2
e -> forall a1 b. Const (a1 -> b -> a1)
K forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g ty2
e
conv (TApp TTerm g (a1 -> a)
t1 TTerm g a1
t2) = forall (g :: [*]) a. TTerm g a -> OTerm g a
conv TTerm g (a1 -> a)
t1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ forall (g :: [*]) a. TTerm g a -> OTerm g a
conv TTerm g a1
t2
conv (TConst Const a
c) = 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 = forall (g :: [*]) b a. OTerm g b -> OTerm (a : g) b
W (OTerm g (a -> b)
e1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g a
e2)
  W OTerm g (a -> b)
e $$ E BTerm a
d = forall (g :: [*]) b a. OTerm g b -> OTerm (a : g) b
W (OTerm g (a -> b)
e forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ forall a (g :: [*]). BTerm a -> OTerm g a
E BTerm a
d)
  E BTerm (a -> b)
d $$ W OTerm g a
e = forall (g :: [*]) b a. OTerm g b -> OTerm (a : g) b
W (forall a (g :: [*]). BTerm a -> OTerm g a
E BTerm (a -> b)
d 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 = 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 = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a (g :: [*]). BTerm a -> OTerm g a
E (forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. forall a1. Const (a1 -> a1)
I) 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 = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall b c a1. Const ((b -> c) -> (a1 -> b) -> a1 -> c)
B forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g (a -> b)
e1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g (a -> a)
e2)
  N OTerm g (a -> a -> b)
e1 $$ W OTerm g a
e2 = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g (a -> a -> b)
e1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g a
e2)
  N OTerm g (a -> a -> b)
e1 $$ N OTerm g (a -> a)
e2 = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a1 b c. Const ((a1 -> b -> c) -> (a1 -> b) -> a1 -> c)
S forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g (a -> a -> b)
e1 forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g (a -> a)
e2)
  N OTerm g (a -> a -> b)
e $$ OTerm g a
V = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a1 b c. Const ((a1 -> b -> c) -> (a1 -> b) -> a1 -> c)
S forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ OTerm g (a -> a -> b)
e forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
t (a -> b) -> Const a -> t b
$$. forall a1. Const (a1 -> a1)
I)
  OTerm g (a -> b)
V $$ N OTerm g (a -> a)
e = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a (g :: [*]). BTerm a -> OTerm g a
E (forall a1 b c. Const ((a1 -> b -> c) -> (a1 -> b) -> a1 -> c)
S forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. forall a1. Const (a1 -> a1)
I) forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ OTerm g (a -> a)
e)
  E BTerm (a -> b)
d $$ N OTerm g (a -> a)
e = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a (g :: [*]). BTerm a -> OTerm g a
E (forall b c a1. Const ((b -> c) -> (a1 -> b) -> a1 -> c)
B forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> t a -> t b
.$$ BTerm (a -> b)
d) 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 = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a (g :: [*]). BTerm a -> OTerm g a
E BTerm (a -> b)
d)
  OTerm g (a -> b)
V $$ E BTerm a
d = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a (g :: [*]). BTerm a -> OTerm g a
E (forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. forall a1. Const (a1 -> a1)
I 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 = forall (g :: [*]) a b. OTerm g (a -> b) -> OTerm (a : g) b
N (forall a (g :: [*]). BTerm a -> OTerm g a
E (forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C forall (t :: * -> *) a b.
(HasConst t, Applicable t) =>
Const (a -> b) -> Const a -> t b
.$$. forall a1 b c. Const ((a1 -> b -> c) -> b -> a1 -> c)
C forall (t :: * -> *) a b. Applicable t => t (a -> b) -> t a -> t b
$$ BTerm a
d) 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 = forall a (g :: [*]). BTerm a -> OTerm g a
E (BTerm (a -> b)
d1 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)!