Skip to content

Instantly share code, notes, and snippets.

@BekaValentine

BekaValentine/PlutusCore.agda

Created October 26, 2017 16:29
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save BekaValentine/b6fb4fa24d8a1578dedd889c4db99af1 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save BekaValentine/b6fb4fa24d8a1578dedd889c4db99af1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
PlutusCore.agda
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
_!!_ : {A : Set} {n : ℕ} (xs : Vec A n) → Fin n → A
[] !! ()
cons x xs !! zero = x
cons x xs !! suc i = xs !! i
_!_ : {A : Set} (xs : List A) → Fin (length xs) → A
[] ! ()
cons x xs ! zero = x
cons x xs ! suc i = xs ! i
infixl 10 _,_
data Ctx (A : Set) : Set where
<> : Ctx A
_,_ : Ctx A → A → Ctx A
infix 9 _∋_
data _∋_ {A : Set} : (Γ : Ctx A) → (J : A) → Set where
top : ∀ {Γ J} → Γ , J ∋ J
pop : ∀ {Γ J J'} → Γ ∋ J → Γ , J' ∋ J
data SortedString {S : Set} : S → Set where
sorted : (s : S) → String → SortedString s
record QualifiedName : Set where
constructor _∙_
field
moduleName : String
unqualifiedName : String
record QualifiedConstructor : Set where
constructor _∙_
field
moduleName : String
unqualifiedConstructor : String
postulate Integer Float ByteString : Set
data Sort : Set where
tm ty : Sort
data Kind : Set where
typeK : Kind
funK : Kind → Kind → Kind
mutual
data Syntax : Sort → Set where
var : ∀ {s} → (x : SortedString s) → Syntax s
nameT : (ν^ : QualifiedName) → Syntax ty
funT : (S T : Syntax ty) → Syntax ty
conT : {n : ℕ} (κ^ : QualifiedConstructor) (T* : Vec (Syntax ty) n) → Syntax ty
compT : (T : Syntax ty) → Syntax ty
forallT : (α : String) (K : Kind) (T : Syntax ty) → Syntax ty
integerT : Syntax ty
floatT : Syntax ty
bytestringT : Syntax ty
lamT : (α : String) (K : Kind) (T : Syntax ty) → Syntax ty
appT : (S T : Syntax ty) → Syntax ty
name : (n : QualifiedName) → Syntax tm
isa : (T : Syntax ty) (M : Syntax tm) → Syntax tm
abs : String → (M : Syntax tm) → Syntax tm
inst : (M : Syntax tm) (T : Syntax ty) → Syntax tm
lam : String → (M : Syntax tm) → Syntax tm
app : (M N : Syntax tm) → Syntax tm
con : {n : ℕ} (c : QualifiedConstructor) (M* : Vec (Syntax tm) n) → Syntax tm
case : (M : Syntax tm) (C* : List Clause) → Syntax tm
success : (M : Syntax tm) → Syntax tm
failure : Syntax tm
compbuiltin : (cbi : String) → Syntax tm
bind : (M : Syntax tm) (x : String) (N : Syntax tm) → Syntax tm
integer : (i : Integer) → Syntax tm
float : (f : Float) → Syntax tm
bytestring : (b : ByteString) → Syntax tm
builtin : {n : ℕ} (bi : String) (M* : Vec (Syntax tm) n) → Syntax tm
record Clause : Set where
inductive
constructor cl
field
ctor : QualifiedConstructor
x* : List String
body : Syntax tm
Term : Set
Term = Syntax tm
Type : Set
Type = Syntax ty
[_/_] : ∀ {s s'} → Syntax s → String → Syntax s' → Syntax s'
[ M / x ] N = {!!}
[_/_]* : ∀ {n s s'} → Vec (Syntax s) n → Vec String n → Syntax s' → Syntax s'
[ M / x ]* N = {!!}
record TermNameInfo : Set where
constructor _∶_
field
termName : QualifiedName
termType : Type
record TermConstructorSignature : Set where
constructor tmcon
field
{m n} : ℕ
params : Vec String m
kinds : Vec Kind m
args : Vec Type n
tycon : QualifiedConstructor
record TermConstructorInfo : Set where
constructor _∶_
field
termConstructorName : QualifiedConstructor
termConstructorSignature : TermConstructorSignature
record TypeNameInfo : Set where
constructor _∷_
field
typeName : QualifiedName
typeKind : Kind
record TypeConstructorSignature : Set where
constructor tycon
field
{n} : ℕ
kinds : Vec Kind n
record TypeConstructorInfo : Set where
constructor _∷_
field
typeConstructorName : QualifiedConstructor
typeConstructorSignature : TypeConstructorSignature
record NominalContext : Set where
constructor nomctx
field
typeNames : List TypeNameInfo
typeConstructors : List TypeConstructorInfo
termNames : List TermNameInfo
termConstructors : List TermConstructorInfo
infix 11 _∶_ _∷_
data HypJ : Set where
_∷_ : String → Kind → HypJ
_∶_ : String → Type → HypJ
infix 10 _chk_ _syn_
data ConJ : Set where
_chk_ : Type → Term → ConJ
_syn_ : Term → Type → ConJ
_∷_ : Type → Kind → ConJ
record Context : Set where
constructor ctx
field
currentModule : String
knownModules : List String
nominalContext : NominalContext
hypotheticalContext : Ctx HypJ
infixl 10 _,,_
_,,_ : Context → HypJ → Context
ctx currentModule knownModules nominalContext hypotheticalContext ,, J =
ctx currentModule knownModules nominalContext (hypotheticalContext , J)
infixr 10 _+++_
_+++_ : ∀ {n} → Context → Vec HypJ n → Context
Θ +++ js = {!!}
_⊩con_ : Context → TermConstructorInfo → Set
_⊩con_ = {!!}
_⊩name_ : Context → TermNameInfo → Set
_⊩name_ = {!!}
_⊩tycon_ : Context → TypeConstructorInfo → Set
_⊩tycon_ = {!!}
_⊩tyname_ : Context → TypeNameInfo → Set
_⊩tyname_ = {!!}
_is_ : String → Type → Set
cbi is T = {!!}
_is_=>_ : ∀ {n} → String → Vec Type n → Type → Set
bi is S* => T = {!!}
-------------------------------------------------------
-- --
-- Most of the Natural Deduction for Plutus Core --
-- --
-------------------------------------------------------
infix 9 _⊢_
mutual
data _⊢_ (Θ : Context) : ConJ → Set where
-- [ Θ ⊢ T ∷ K ]
varT : ∀ {α K} → Context.hypotheticalContext Θ ∋ α ∷ K
---
→ Θ ⊢ var (sorted ty α) ∷ K
nameT : ∀ {ν^ K} → Θ ⊩tyname (ν^ ∷ K)
---
→ Θ ⊢ nameT ν^ ∷ K
funT : ∀ {S T} → Θ ⊢ S ∷ typeK → Θ ⊢ T ∷ typeK
--
→ Θ ⊢ funT S T ∷ typeK
tyconT : ∀ {n} {κ^} {T* : Vec Type n} {K* : Vec Kind n} → Θ ⊩tycon (κ^ ∷ tycon K*) → (∀ i → Θ ⊢ (T* !! i) ∷ (K* !! i))
----------------------------------------------------------------
→ Θ ⊢ conT κ^ T* ∷ typeK
compT : ∀ {T} → Θ ⊢ T ∷ typeK
-------------------
→ Θ ⊢ compT T ∷ typeK
forallT : ∀ {α K T} → Θ ,, α ∷ K ⊢ T ∷ typeK
-------------------------
→ Θ ⊢ forallT α K T ∷ typeK
integerT : Θ ⊢ integerT ∷ typeK
floatT : Θ ⊢ floatT ∷ typeK
bytestringT : Θ ⊢ bytestringT ∷ typeK
lamT : ∀ {α J T K} → Θ ,, α ∷ J ⊢ T ∷ K
-------------------------
→ Θ ⊢ lamT α J T ∷ funK J K
appT : ∀ {S T K J} → Θ ⊢ S ∷ funK J K → Θ ⊢ T ∷ J
--------------------------------
→ Θ ⊢ appT S T ∷ K
-- [ Θ ⊢ T chk M ]
abs : ∀ {α K T M} → Θ ,, α ∷ K ⊢ T chk M
-----------------------------
→ Θ ⊢ forallT α K T chk abs α M
lam : ∀ {S T x M} → Θ ,, x ∶ S ⊢ T chk M
------------------------
→ Θ ⊢ funT S T chk lam x M
con : ∀ {m n} {κ^ T* c^} {M* : Vec Term n} {α* K*} {S* : Vec Type n} → Θ ⊩con (c^ ∶ tmcon {m} {n} α* K* S* κ^) → (∀ i → Θ ⊢ [ T* / α* ]* (S* !! i) chk (M* !! i))
----------------------------------------------------------------------------------------------
→ Θ ⊢ conT κ^ T* chk con c^ M*
case : ∀ {T M C* S} → Θ ⊢ M syn S → (∀ i → Θ / S ⊢ T ∋ (C* ! i))
---
→ Θ ⊢ T chk case M C*
success : ∀ {T M} → Θ ⊢ T chk M
-------------------------
→ Θ ⊢ compT T chk success M
failure : ∀ {T} → Θ ⊢ compT T chk failure
bind : ∀ {T M x N S} → Θ ⊢ M syn compT S → Θ ,, x ∶ S ⊢ compT T chk N
--------------------------------------------------
→ Θ ⊢ compT T chk bind M x N
dir-change : ∀ {T M} → Θ ⊢ M syn T
-----------
→ Θ ⊢ T chk M
-- [ Θ ⊢ M syn T ]
var : ∀ {x T} → Context.hypotheticalContext Θ ∋ x ∶ T
-------------------------------------
→ Θ ⊢ var (sorted tm x) syn T
name : ∀ {n^ T} → Θ ⊩name (n^ ∶ T)
-----------------
→ Θ ⊢ name n^ syn T
isa : ∀ {T M} → Θ ⊢ T chk M
-----------------
→ Θ ⊢ isa T M syn T
inst : ∀ {M S α T K} → Θ ⊢ M syn forallT α K T → Θ ⊢ S ∷ K
---------------------------------------
→ Θ ⊢ inst M S syn [ S / α ] T
app : ∀ {M N T S} → Θ ⊢ M syn funT S T → Θ ⊢ S chk N
------------------------------------
→ Θ ⊢ app M N syn T
compbuiltin : ∀ {cbi T} → cbi is T
-------------------------------
→ Θ ⊢ compbuiltin cbi syn compT T
intval : ∀ {i} → Θ ⊢ integer i syn integerT
floatval : ∀ {f} → Θ ⊢ float f syn floatT
bytestring : ∀ {b} → Θ ⊢ bytestring b syn bytestringT
builtin : ∀ {n bi} {M* : Vec Term n} {T} {S* : Vec Type n} → bi is S* => T → (∀ i → Θ ⊢ (S* !! i) chk (M* !! i))
→ Θ ⊢ builtin bi M* syn T
data _/_⊢_∋_ (Θ : Context) : (S T : Type) (C : Clause) → Set where
clause : ∀ {m n} {κ^} {S* : Vec Type m} {T c^ x* M} {α* : Vec String m} {K* : Vec Kind m} {R* : Vec Type n} → Θ ⊩con (c^ ∶ (tmcon {m} {n} α* K* R* κ^)) → (Θ +++ Data.Vec.zipWith _∷_ α* K*) ⊢ T chk M
--------------------------------------------------------------------------------------------
→ Θ / conT κ^ S* ⊢ T ∋ cl c^ x* M
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment