BekaValentine

{-# OPTIONS -Wall #-}
{-# LANGUAGE BangPatterns #-}

import Control.Monad (zipWithM)
import Data.List (elemIndex,intercalate)

data Term
  = Var String
  | Lam Scope
  | App Term Term

BekaValentine

data family Lin a r

class Linearizable a where
  linearize :: a -> r -> Lin a r
  delinearize :: Lin a r -> (a,r)



data instance Lin Bool r where
  LinBool :: Bool -> r -> Lin Bool r

BekaValentine

import Control.Monad.State



-- Introduction forms, including variables. We parameterize by the type of a
-- scope argument `s` and scope body `b`, as well as the type of auxiliary
-- terms `a`

data Intro s b a
  = Var String

BekaValentine

data Proposition : Set where
  UNIT   : Proposition
  _=>_   : Proposition -> Proposition -> Proposition
  BOX    : Proposition -> Proposition

infixr 0 _=>_

postulate World : Set
          FIRST : World
          NEXT : World -> World

BekaValentine

  module STLC where
    
    infixr 9 _⇒_
    data Ty : Set where
      _⇒_ : Ty → Ty → Ty
    
    data Context : Set where
      <> : Context
      _,_ : Context → Ty → Context
    

BekaValentine

record Model : Set₁ where
  field
    Atomic : Set
    True : Atomic → Set

open Model


data Proposition (M : Model) : Set where
  [_] : (A : Atomic M) → Proposition M

BekaValentine

open import Data.Fin
open import Data.Nat
open import Function using (_∘_)

module SmartLambda where

data Term : ℕ → Set where
  var : ∀ {n} → Fin n → Term n
  lam : ∀ {n} → Term (suc n) → Term n
  _$_ : ∀ {n} → Term n → Term n → Term n

BekaValentine

data Term
  = Lit Int
  | Pair Term Term
  | Fst Term
  | Snd Term
  | Lam (Term -> Term)
  | App Term Term

instance Show Term where
  show (Lit i) = show i

BekaValentine

data Term
  = Lit Int
  | Pair Term Term
  | Fst Term
  | Snd Term
  | Lam (Term -> Term)
  | App Term Term

instance Show Term where
  show (Lit i) = show i

BekaValentine

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}