<commit_before>\section{Tm}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, GADTs, KindSignatures,
>     TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables #-}

> module Tm where

> import Control.Applicative
> import Data.Foldable hiding (foldl)
> import Data.Traversable
> import Control.Monad.Identity
> import Data.Either

> import BwdFwd
> import Features

%endif

%format :$ = ":\!\$"
%format :? = "\,:\!\!\!\in"
%format Set = "\star"
%format Pi = "\Pi"
%format :. = "\bullet"

> data Dir    = In | Ex
> data Phase  = TT | VV

> data Tm :: {Dir, Phase} -> * -> * where
>   L     :: Scope p x           -> Tm {In, p} x   -- \(\lambda\)
>   C     :: Can (Tm {In, p} x)  -> Tm {In, p} x   -- canonical
>   N     :: Tm {Ex, p} x        -> Tm {In, p} x   -- |Ex| to |In|
>   P     :: x                   -> Tm {Ex, p} x   -- parameter
>   V     :: Int                 -> Tm {Ex, TT} x  -- variable
>   (:$)  :: Tm {Ex, p} x -> Elim (Tm {In, p} x) -> Tm {Ex, p} x  -- elimination
>   (:?)  :: Tm {In, TT} x -> Tm {In, TT} x -> Tm {Ex, TT} x      -- typing
>
> data Scope :: {Phase} -> * -> * where
>   (:.)  :: String -> Tm {In, TT} x         -> Scope {TT} x  -- binding
>   H     :: Env -> String -> Tm {In, TT} x  -> Scope {VV} x  -- closure
>   K     :: Tm {In, p} x                    -> Scope p x     -- constant
>
> data Can :: * -> * where
>   Set   :: Can t                                        -- set of sets
>   Pi    :: t -> t -> Can t                              -- functions
>   import <- CanConstructors
>   deriving (Show, Eq)
>
> data Elim :: * -> * where
>   A     :: t -> Elim t                                  -- application
>   import <- ElimConstructors
>   deriving (Show, Eq)

> pattern SET       = C Set                   -- set of sets
> pattern Arr s t   = C (Pi s (L (K t)))      -- simple arrow
> pattern PI x s t  = C (Pi s (L (x :. t)))   -- dependent functions

> type InTm  = Tm {In, TT}
> type ExTm  = Tm {Ex, TT}
> type INTM  = InTm REF
> type EXTM  = ExTm REF
> type VAL   = Tm {In, VV} REF
> type NEU   = Tm {Ex, VV} REF
> type Env   = Bwd VAL

> type Spine p x = [Elim (Tm {In, p} x)]
> ($:$) :: Tm {Ex, p} x -> Spine p x -> Tm {Ex, p} x
> ($:$) = foldl (:$)

> data REF = Name := RKind  -- is shared where possible
>
> type Name = [(String, Int)]
>
> instance Show REF where
>   show (n := _) = show n
>
> instance Eq REF where
>   (x := _) == (y := _) = x == y  -- could use cheeky pointer equality?

> data RKind
>   = DECL VAL
>   | DEFN VAL VAL
>   | HOLE VAL
>   deriving Show

We have special pairs for types going in and coming out of stuff.

> data y :>: t = y :>: t
> data t :<: y = t :<: y

> ($$) :: VAL -> Elim VAL -> VAL
> L (K v)      $$ A _  = v
> L (H g _ t)  $$ A v  = eval t (g :< v)
> N n          $$ e    = N (n :$ e)

> pval :: REF -> VAL
> pval (_ := DEFN v _)  = v
> pval r                = N (P r)

> body :: Scope {TT} REF -> Env -> Scope {VV} REF
> body (K v)     g = K (eval v g)
> body (x :. t)  g = H g x t
<commit_msg>added computation aspect<commit_after>\section{Tm}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, GADTs, KindSignatures,
>     TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables #-}

> module Tm where

> import Control.Applicative
> import Data.Foldable hiding (foldl)
> import Data.Traversable
> import Control.Monad.Identity
> import Data.Either

> import BwdFwd
> import Features

%endif

%format :$ = ":\!\$"
%format :? = "\,:\!\!\!\in"
%format Set = "\star"
%format Pi = "\Pi"
%format :. = "\bullet"

> data Dir    = In | Ex
> data Phase  = TT | VV

> data Tm :: {Dir, Phase} -> * -> * where
>   L     :: Scope p x           -> Tm {In, p} x   -- \(\lambda\)
>   C     :: Can (Tm {In, p} x)  -> Tm {In, p} x   -- canonical
>   N     :: Tm {Ex, p} x        -> Tm {In, p} x   -- |Ex| to |In|
>   P     :: x                   -> Tm {Ex, p} x   -- parameter
>   V     :: Int                 -> Tm {Ex, TT} x  -- variable
>   (:$)  :: Tm {Ex, p} x -> Elim (Tm {In, p} x) -> Tm {Ex, p} x  -- elimination
>   (:?)  :: Tm {In, TT} x -> Tm {In, TT} x -> Tm {Ex, TT} x      -- typing
>
> data Scope :: {Phase} -> * -> * where
>   (:.)  :: String -> Tm {In, TT} x         -> Scope {TT} x  -- binding
>   H     :: Env -> String -> Tm {In, TT} x  -> Scope {VV} x  -- closure
>   K     :: Tm {In, p} x                    -> Scope p x     -- constant
>
> data Can :: * -> * where
>   Set   :: Can t                                        -- set of sets
>   Pi    :: t -> t -> Can t                              -- functions
>   import <- CanConstructors
>   deriving (Show, Eq)
>
> data Elim :: * -> * where
>   A     :: t -> Elim t                                  -- application
>   import <- ElimConstructors
>   deriving (Show, Eq)

> pattern SET       = C Set                   -- set of sets
> pattern Arr s t   = C (Pi s (L (K t)))      -- simple arrow
> pattern PI x s t  = C (Pi s (L (x :. t)))   -- dependent functions

> type InTm  = Tm {In, TT}
> type ExTm  = Tm {Ex, TT}
> type INTM  = InTm REF
> type EXTM  = ExTm REF
> type VAL   = Tm {In, VV} REF
> type NEU   = Tm {Ex, VV} REF
> type Env   = Bwd VAL

> type Spine p x = [Elim (Tm {In, p} x)]
> ($:$) :: Tm {Ex, p} x -> Spine p x -> Tm {Ex, p} x
> ($:$) = foldl (:$)

> data REF = Name := RKind  -- is shared where possible
>
> type Name = [(String, Int)]
>
> instance Show REF where
>   show (n := _) = show n
>
> instance Eq REF where
>   (x := _) == (y := _) = x == y  -- could use cheeky pointer equality?

> data RKind
>   =  DECL VAL
>   |  DEFN VAL VAL
>   |  HOLE VAL
>   deriving Show

We have special pairs for types going in and coming out of stuff.

> data y :>: t = y :>: t
> data t :<: y = t :<: y

> ($$) :: VAL -> Elim VAL -> VAL
> L (K v)      $$ A _  = v
> L (H g _ t)  $$ A v  = eval t (g :< v)
> import <- ElimComputation
> N n          $$ e    = N (n :$ e)

> pval :: REF -> VAL
> pval (_ := DEFN v _)  = v
> pval r                = N (P r)

> body :: Scope {TT} REF -> Env -> Scope {VV} REF
> body (K v)     g = K (eval v g)
> body (x :. t)  g = H g x t

{'fraction_non_alphanumeric': 0.18311475409836064, 'fraction_numerical': 0.0, 'mean_word_length': 1.6468546637744035, 'pattern_counts': {'":': 2, '<': 14, '<?xml version=': 0, '>': 222, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4168784', 'n_tokens_mistral': 2431, 'n_tokens_neox': 2366, 'n_words': 828}