BekaValentine

module SystemF-Proof-Theory where


open import Data.Bool hiding (if_then_else_ ; _≟_)
open import Data.String
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

BekaValentine

open import Data.List
open import Data.Nat
open import Data.Product
open import Data.Vec renaming (_++_ to _++V_ ; replicate to replicateV)
open import Relation.Binary.PropositionalEquality



data Tree (A : Set) : Set where
  leaf : A → Tree A

BekaValentine

module BidiInversion where

open import Data.Bool hiding (_≟_ ; if_then_else_)
open import Data.Empty
open import Data.List hiding ([_])
open import Data.Nat hiding (_*_ ; _+_ ; _≟_ ; _>_ ; _<_)
open import Data.Product hiding (<_,_> ; swap ; map) renaming (_,_ to pr)
open import Data.String renaming (_++_ to _++s_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

BekaValentine

module PlutusCore where

open import Data.Fin
open import Data.List renaming (_∷_ to cons)
open import Data.Nat
open import Data.Vec renaming (_∷_ to cons)
open import Data.String

BekaValentine

module ABT1 where

  {-# NO_POSITIVITY_CHECK #-}
  data Syntax {S : Set} (F : (S → Set) → S → Set) : S → Set where
    var : ∀ {s} → ℕ → Syntax F s
    <_> : ∀ {s} → F (Syntax F) s → Syntax F s


module ABT2 where

BekaValentine

sum : List Integer -> Integer
sum Nil = 0
sum (Cons x xs) = x + sum xs


-- Plutus Core w/ global statements, data, etc.

(declare sum (fun (con Prelude.List (integer)) (integer)))
(define sum (lambda xs
  (case xs

BekaValentine

module SystemF where

data Kind : Set where
  * : Kind
  _=>_ : Kind -> Kind -> Kind

data KindContext : Set where
  [] : KindContext
  _,_ : KindContext -> Kind -> KindContext

BekaValentine

module RevRev  where

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

Rev : {A : Set} (_~_ : A -> A -> Set) (x y : A) -> Set
Rev _~_ y x = x ~ y

data All {A} (P : A -> Set) : List A -> Set where

BekaValentine

-- Define names for convenience, these aren't real, just meta-level

Data_Bool :: forall r :: *.
               (forall bool :: *.
                 bool ->
                 bool ->
                 (forall a. bool -> (() -> a) -> (() -> a) -> a) ->
                 r)
               -> r
Data_Bool dependee =

BekaValentine

Data_List :: forall r :: *.
               (forall list :: * -> *.
                 (forall a. list a) ->
                 (forall a. a -> list a -> list a) ->
                 (forall a b. (() -> b) -> (a -> list a -> b) -> b) ->
                 r)
               -> r
Data_List dependee =
  dependee {\a -> Fix l. (forall b. (() -> b) -> (a -> l a -> b) -> b)}
           <scott encoded nil>