WIP C bootstrap VM of a classical linear language.

master
James T. Martin 11 months ago
parent 88e9dabddf
commit bb53c1b162
Signed by: james
GPG Key ID: D6FB2F9892F9B225

@ -0,0 +1,9 @@
# https://EditorConfig.org/
root = true
[*]
indent_size = 4
charset = utf-8
indent_style = space
trim_trailing_whitespace = true
insert_final_newline = true

16
.gitignore vendored

@ -1,5 +1,11 @@
_build/
bin/
*.agdai
*~
\#*\#
*
!*/
# source code
!/src/**/*.c
!/src/**/*.h
# top-level configuration
!/.editorconfig
!/.gitignore
!/LICENSE.txt

@ -0,0 +1,5 @@
Copyright (C) 2022 by James Martin <james@jtmar.me>
Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted.
THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

@ -1,4 +0,0 @@
#!/bin/bash
mkdir -p bin/obj/
nasm -felf64 -o bin/obj/darierre.o src/darierre.nasm
ld -lc --dynamic-linker=/usr/lib64/ld-linux-x86-64.so.2 -o bin/darierre bin/obj/darierre.o

@ -1,287 +0,0 @@
EXTERN malloc
EXTERN free
EXTERN printf
SECTION .rodata
message: db `%llu\n\0`
SECTION .text
GLOBAL _start
%macro send 0
; arguments:
; rax: the message
; rbx: "our" stack
; rdx: "their" code
; rbp: "their" stack
;
; returns:
; rax : the response
; rdx : "our" code
; rbx : "our" stack
; [rsp]: "their" code"
; rbp : "their" stack
xchg rbx, rbp
call rdx
%endm
%macro send_quick 0
; like `send`, but "our" code is in rdx and "their" code is in `[rsp]`.
xchg rbx, rbp
xchg rdx, [rsp]
jmp rdx
%endmacro
fib:
; fibonacci sequence represented as infinite stream of unsigned integers.
;
; arguments:
; rbx: consumer code (⊥ + (¬ u64; rec))
; rbp: consumer stack
;
; returns:
; rbx: fib code (⊥)
; rbp: fib stack
; stack layout:
; 0: accumulator 1 (initialized with 0)
; 8: accumulator 2 (initialized with 1)
; 16: consumer code
; 24: consumer stack
mov edi, 32
call malloc
; initialize accumulators
xor ecx, ecx
mov [rax], rcx
inc ecx
mov [rax+8], rcx
; save consumer
mov [rax+16], rbx
mov [rax+24], rbp
; return code and stack
mov rbx, fibk
mov rbp, rax
ret
fibk:
; arguments:
;
; rbx: the stack
;
; returns: doesn't.
; ask the consumer what it wants us to produce next.
mov rdx, [rbx+16]
mov rbp, [rbx+24]
send
test al, al
jnz fib_free
fib_next:
; the next element in the sequence is in [rbx]
mov rax, [rbx]
; update the accumulators to contain the next two elements
mov rcx, [rbx+8]
mov [rbx], rcx
add rcx, rax
mov [rbx+8], rcx
pop rdx
xchg rbx, rbp
mov rcx, fibk
push rcx
jmp rdx
fib_free:
; the consumer wishes for us to terminate.
; free stack
mov rdi, rbx
call free
; continue
mov rbx, rbp
pop rdx
jmp rdx
print_list:
; prints prefix of infinite stream of unsigned integers.
;
; arguments:
; rax: size of prefix to print
; rbx: list code (1 & (u64; rec))
; rbp: list stack
; rcx: continuation code (⊥)
; rdx: continuation stack
;
; returns:
; rbx: print code (⊥)
; rbp: print stack
;
; stack layout:
; 0: remaining prefix
; 8: list code
; 16: list stack
; 24: continuation code
; 32: continuation stack
mov edi, 40
push rax
push rcx
push rdx
call malloc
mov [rax+8], rbx
mov [rax+16], rbp
pop qword [rax+32]
pop qword [rax+24]
pop qword [rax]
mov rbx, print_listk
mov rbp, rax
ret
print_listk:
mov rax, [rbx]
test rax, rax
jz print_list_free
print_list_next:
dec qword [rbx]
; request next element of list
xor eax, eax
mov rdx, [rbx+8]
mov rbp, [rbx+16]
send
; receive next element of list
pop rdx
send
; save new continuation
pop qword [rbx+8]
mov [rbx+16], rbp
; print element
mov rsi, rax
mov rdi, message
xor eax, eax
call printf
jmp print_listk
print_list_free:
; free the list
xor eax, eax
inc eax
mov rdx, [rbx+8]
mov rbp, [rbx+16]
send
; free the stack
mov rdi, rbx
mov rbp, [rdi+24]
mov rbx, [rdi+32]
call free
; continue
mov rdx, rbp
jmp rdx
lem_begin:
; the law of the excluded middle (allows us to join producers with consumers).
;
; returns:
; rax: LEM stack
;
; arguments:
; rbx: continuation code
; rbp: stack code
;
; stack layout:
; 0: message on hold
; 8: code on hold
; 16: stack on hold
; 24: continuation code
; 32: continuation stack
mov edi, 40
call malloc
mov [rax+24], rbx
mov [rax+32], rbp
ret
lem_left:
pop rdx
xchg rdx, [rbx+8]
xchg rbp, [rbx+16]
send
lem_right:
xchg rax, [rbx]
pop rdx
xchg rdx, [rbx+8]
xchg rbp, [rbx+16]
send
jmp lem_left
lem_cleanup:
mov rax, [rbx]
mov rdx, [rbx+8]
mov rbp, [rbx+16]
send
mov rdi, rbx
mov rbp, [rdi+24]
mov rbx, [rdi+32]
call free
mov rdx, rbp
jmp rdx
lem_end:
; finish joining producers with consumers.
;
; arguments:
; rax: LEM stack
; rbx: code 1 (⊥)
; rbp: stack 1
; rcx: code 2 (⊥)
; rdx: stack 2
mov [rax+8], rcx
mov [rax+16], rdx
mov rdx, rbx
mov rbx, rbp
jmp rdx
exit:
mov eax, 60
xor edi, edi
syscall
_start:
mov rbx, exit
call lem_begin
push rax
mov rbx, lem_left
mov rbp, rax
call fib
mov rax, [rsp]
push rbx
push rbp
mov rbx, lem_right
mov rbp, rax
mov rcx, lem_cleanup
mov rdx, rax
mov rax, 30
call print_list
pop rdx
pop rcx
mov rax, [rsp]
call lem_end

@ -1,4 +0,0 @@
name: darius
include: src
flags: --without-K --no-guardedness --no-sized-types --prop -W all --no-exact-split
depend: standard-library

@ -1,166 +0,0 @@
module Darierre where
open import Data.Nat
open import Data.Nat.Properties
open import Data.Vec hiding (split)
open import Relation.Binary.PropositionalEquality renaming (subst to transp)
private variable n n₁ n₂ :
infix 5 _≐_
data _≐_ {} {A : Set } (x : A) : A → Prop where
refl' : x ≐ x
sq-eq : ∀ {} {A : Set } {x y : A} → x ≡ y → x ≐ y
sq-eq refl = refl'
suc-inj-irr : ∀ {n₁ n₂ : } → .suc n₁ ≐ suc n₂ → n₁ ≐ n₂
suc-inj-irr refl' = refl'
infix 18 _⊗_ _&_
infix 17 _⊕_ _⅋_
data Type : Set where
_⊕_ : Type → Type → Type
0' : Type
_&_ : Type → Type → Type
' : Type
_⊗_ : Type → Type → Type
1' : Type
_⅋_ : Type → Type → Type
⊥' : Type
infixl 15 _,,_ _+++_
data Context : -> Set where
∅ : Context 0
_,,_ : Context n → Type → Context (suc n)
variable Γ Γ₁ Γ₂ Δ Δ₁ Δ₂ Λ Λ₁ Λ₂ Θ Θ₁ Θ₂ : Context n
ctx-cast : ∀ {n n'} → n ≐ n' → Context n → Context n'
ctx-cast {zero} {zero} p ∅ = ∅
ctx-cast {suc n} {suc n'} p (Γ ,, τ) = ctx-cast (suc-inj-irr p) Γ ,, τ
ctx-cast-stupid : ∀ {Γ : Context n} {τ} → ctx-cast refl' Γ ,, τ ≡ Γ ,, τ
ctx-cast-stupid {Γ = ∅} = refl
ctx-cast-stupid {Γ = _ ,, _} {τ} = cong (_,, τ) ctx-cast-stupid
_+++_ : ∀ {n₁ n₂} → Context n₁ → Context n₂ → Context (n₂ + n₁)
Γ₁ +++ ∅ = Γ₁
Γ₁ +++ (Γ₂ ,, τ) = Γ₁ +++ Γ₂ ,, τ
+++-id : (Γ : Context n) → ∅ +++ Γ ≡ ctx-cast (sq-eq (sym (+-identityʳ n))) Γ
+++-id ∅ = refl
+++-id {suc n} (Γ ,, x) = cong (_,, x) (+++-id Γ)
data Perm : (Γ : Context n) (Γ₁ : Context n₁) (Γ₂ : Context n₂) → Set where
perm-done : Perm ∅ ∅ ∅
perm-left : ∀ {τ} → Perm Γ Γ₁ Γ₂ → Perm (Γ ,, τ) (Γ₁ ,, τ) Γ₂
perm-right : ∀ {τ} → Perm Γ Γ₁ Γ₂ → Perm (Γ ,, τ) Γ₁ (Γ₂ ,, τ)
data Expr : {vars covars : } (Γ : Context vars) (Δ : Context covars) → Set where
var : ∀ {vars covars} {Γ : Context vars} {Δ : Context covars} {τ}
→ (pv : vars ≡ 1) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ ∅ ,, τ)
→ (pc : covars ≡ 1) → (pΔ : ctx-cast (sq-eq pc) Δ ≡ ∅ ,, τ)
→ Expr Γ Δ
match : ∀ {vars vars₁ vars₂ covars} {Γ : Context vars} {Γ₁ : Context vars₁} {Γ₂ : Context vars₂} {Δ : Context covars} {τ₁ τ₂}
→ (pv : vars ≡ vars₂ + vars₁) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ Γ₁ +++ Γ₂)
-- Expression to pattern match against.
→ (x : Expr Γ₁ (∅ ,, τ₁ ⊕ τ₂))
-- Expression handling each possible case.
→ (f : Expr (Γ₂ ,, τ₁) Δ)
→ (g : Expr (Γ₂ ,, τ₂) Δ)
--------------------------
→ Expr Γ Δ
case : ∀ {vars vars₁ vars₂ covars} {Γ : Context vars} {Γ₁ : Context vars₁} {Γ₂ : Context vars₂} {Δ : Context covars} {τ₁ τ₂}
→ (pv : vars ≡ vars₂ + vars₁) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ Γ₁ +++ Γ₂)
→ (f : Expr Γ₁ (∅ ,, τ₁))
→ (g : Expr Γ₁ (∅ ,, τ₂))
→ (w : Expr Γ₂ Δ)
→ Expr Γ (Δ ,, τ₁ & τ₂)
inj₁ : ∀ {vars} {Γ : Context vars} {τ₁} τ₂
→ (x : Expr Γ (∅ ,, τ₁))
→ Expr Γ (∅ ,, τ₁ ⊕ τ₂)
inj₂ : ∀ {vars} {Γ : Context vars} τ₁ {τ₂}
→ (y : Expr Γ (∅ ,, τ₂))
→ Expr Γ (∅ ,, τ₁ ⊕ τ₂)
proj₁ : ∀ {vars vars₁ vars₂ covars} {Γ : Context vars} {Γ₁ : Context vars₁} {Γ₂ : Context vars₂} {Δ : Context covars} {τ₁} τ₂
→ (pv : vars ≡ vars₂ + suc vars₁) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ Γ₁ ,, τ₁ & τ₂ +++ Γ₂)
→ (f : Expr (Γ₁ ,, τ₁ +++ Γ₂) Δ)
→ Expr Γ Δ
proj₂ : ∀ {vars vars₁ vars₂ covars} {Γ : Context vars} {Γ₁ : Context vars₁} {Γ₂ : Context vars₂} {Δ : Context covars} τ₁ {τ₂}
→ (pv : vars ≡ vars₂ + suc vars₁) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ Γ₁ ,, τ₁ & τ₂ +++ Γ₂)
→ (g : Expr (Γ₁ ,, τ₂ +++ Γ₂) Δ)
→ Expr Γ Δ
absurd : ∀ {vars vars₁ vars₂ covars} {Γ : Context vars} {Γ₁ : Context vars₁} {Γ₂ : Context vars₂} {Δ : Context covars}
→ (pv : vars ≡ vars₂ + suc vars₁) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ Γ₁ ,, 0' +++ Γ₂)
→ Expr Γ Δ
forget : ∀ {vars covars} {Γ : Context vars} {Δ : Context covars}
→ (pc : covars ≡ 1) → (pΔ : ctx-cast (sq-eq pc) Δ ≡ ∅ ,, ')
→ Expr Γ Δ
pair : ∀ {vars vars₁ vars₂} {Γ : Context vars} {Γ₁ : Context vars₁} {Γ₂ : Context vars₂} {τ₁ τ₂}
→ (pv : vars ≡ vars₂ + vars₁) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ Γ₁ +++ Γ₂)
→ (x : Expr Γ₁ (∅ ,, τ₁))
→ (y : Expr Γ₂ (∅ ,, τ₂))
→ Expr Γ (∅ ,, τ₁ ⊗ τ₂)
copair : ∀ {vars varsA varsB covars covarsA covarsB} {ΓΛ : Context vars} {ΔΘ : Context covars} {Γ : Context varsA} {Δ : Context covarsA} {Λ : Context varsB} {Θ : Context covarsB} {τ₁ τ₂}
→ (pv : vars ≡ varsB + suc varsA) → (pΓΛ : ctx-cast (sq-eq pv) ΓΛ ≡ Γ ,, τ₁ ⅋ τ₂ +++ Λ)
→ (pc : covars ≡ covarsB + covarsA) → (pΔΘ : ctx-cast (sq-eq pc) ΔΘ ≡ Δ +++ Θ)
→ (w : Expr (Γ ,, τ₁) Δ)
→ (z : Expr (Λ ,, τ₂) Θ)
→ Expr ΓΛ ΔΘ
split : ∀ {vars vars₁ vars₂ covars} {Γ : Context vars} {Γ₁ : Context vars₁} {Γ₂ : Context vars₂} {Δ : Context covars} {τ₁ τ₂}
→ (pv : vars ≡ vars₂ + suc vars₁) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ Γ₁ ,, τ₁ ⊗ τ₂ +++ Γ₂)
→ (f : Expr (Γ₁ ,, τ₁ ,, τ₂ +++ Γ₂) Δ)
→ Expr Γ Δ
cosplit : ∀ {vars} {Γ : Context vars} {τ₁ τ₂}
→ (x : Expr Γ (∅ ,, τ₁ ,, τ₂))
→ Expr Γ (∅ ,, τ₁ ⅋ τ₂)
unit : ∀ {vars} {Γ : Context vars}
→ (pv : vars ≡ 0)
→ Expr Γ (∅ ,, 1')
done : ∀ {vars} {Γ : Context vars}
→ (pv : vars ≡ 1) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ ∅ ,, ⊥')
→ Expr Γ ∅
ununit : ∀ {vars vars₁ vars₂ covars} {Γ : Context vars} {Γ₁ : Context vars₁} {Γ₂ : Context vars₂} {Δ : Context covars}
→ (pv : vars ≡ vars₂ + vars₁) → (pΓ : ctx-cast (sq-eq pv) Γ ≡ Γ₁ +++ Γ₂)
→ (f : Expr (Γ₁ ,, 1' +++ Γ₂) Δ)
→ Expr Γ Δ
undone : ∀ {vars} {Γ : Context vars}
→ (w : Expr Γ ∅)
→ Expr Γ (∅ ,, ⊥')
postulate
expr-cast : ∀ {vars vars' covars covars'} {Γ : Context vars} {Γ' : Context vars'} {Δ : Context covars} {Δ' : Context covars'}
→ (pv : vars ≐ vars') → (pc : covars ≐ covars') → ctx-cast pv Γ ≐ Γ' → ctx-cast pc Δ ≐ Δ'
→ Expr Γ Δ → Expr Γ' Δ'
cut' : ∀ {vars covars} {Δ : Context covars} {Λ : Context vars} {τ}
→ (x : Expr (∅ ,, τ) Δ)
→ (y : Expr Λ (∅ ,, τ))
→ Expr Λ Δ
{-
cutL : ∀ {varsA varsB covars} {Γ : Context varsA} {Δ : Context covars} {Λ : Context varsB} {τ}
→ (x : Expr (Γ ,, τ) Δ)
→ (y : Expr Λ (∅ ,, τ))
→ Expr (Γ +++ Λ) Δ
cutR : ∀ {vars covarsA covarsB} {Γ : Context varsA} {Δ : Context covarsA} {Λ : Context varsB} {Θ : Context covarsB} {τ}
→ (x : Expr (∅ ,, τ) Δ)
→ (y : Expr Λ (Θ ,, τ))
→ Expr (Γ +++ Λ) (Θ +++ Δ)
-}
cut : ∀ {varsA₁ varsA₂ varsB covarsA covarsB₁ covarsB₂}
{Γ₁ : Context varsA₁} (Γ₂ : Context varsA₂) {Δ : Context covarsA}
{Λ : Context varsB} {Θ₁ : Context covarsB₁} (Θ₂ : Context covarsB₂)
{τ}
→ (x : Expr (Γ₁ ,, τ +++ Γ₂) Δ)
→ (y : Expr Λ (Θ₁ ,, τ +++ Θ₂))
→ Expr (Γ₁ +++ Λ +++ Γ₂) (Θ₁ +++ Δ +++ Θ₂)
cut' = {!!}
cut Γ₂ Θ₂ x y = {!!}

@ -1,157 +0,0 @@
Require Import Coq.Program.Basics.
Inductive ty : Type :=
(* additive conjunction; *)
| with' : ty -> ty -> ty
(* dually, additive disjunction. *)
| plus : ty -> ty -> ty
(* additive truth; *)
| top : ty
(* dually, additive falsity. *)
| zero : ty
(* multiplicative conjunction; *)
| times : ty -> ty -> ty
(* dually, multiplicative disjunction. *)
| par : ty -> ty -> ty
(* multiplicative truth; *)
| one : ty
(* dually, multiplicative falsity. *)
| bottom : ty
.
Notation "τ₁ '⊕' τ₂" := (plus τ τ) (at level 50).
Notation "τ₁ '⅋' τ₂" := (par τ τ) (at level 50).
Notation "''" := top.
Notation "'0'" := zero.
Notation "τ₁ '⊗' τ₂" := (times τ τ) (at level 40).
Notation "τ₁ '&' τ₂" := (with' τ τ) (at level 40).
Notation "'1'" := one.
Notation "'⊥'" := bottom.
Inductive ctx : nat -> Type :=
| empty : ctx 0
| cons {vars : nat} (Γ : ctx vars) (τ : ty) : ctx (S vars)
.
Notation "'∅'" := empty.
Notation "Γ ',' τ" := (cons Γ τ) (at level 61, left associativity).
Definition append_ctx : forall {n n : nat} (Γ : ctx n) (Γ : ctx n), ctx (n + n).
intros.
induction Γ; simpl.
- assumption.
- constructor; assumption.
Defined.
Notation "Γ ',+' Δ"
:= (append_ctx Γ Δ)
(at level 61, left associativity).
Reserved Notation "Γ '⊢' Δ" (at level 90).
Inductive entails : forall {vars covars} (Γ : ctx vars) (Δ : ctx covars), Type :=
(* identity axiom. *)
| var : forall {τ}, , τ , τ
(* formation rule for additive conjunction; *)
| match' {covars} {Δ : ctx covars} {τ τ}
(f : , τ Δ)
(f : , τ Δ)
: , τ τ Δ
(* dually, formation rule for additive disjunction; *)
| case {vars} {Γ : ctx vars} {τ τ}
(f : Γ , τ)
(f : Γ , τ)
: Γ , τ & τ
(* conversely, reflection rule for additive conjunction; *)
| proj {covars} {Δ : ctx covars} {τ} τ
(x : , τ Δ)
: , τ & τ Δ
| proj {covars} {Δ : ctx covars} τ {τ}
(x : , τ Δ)
: , τ & τ Δ
(* dually, reflection rule for additive disjunction. *)
| inj {vars} {Γ : ctx vars} {τ} τ
(x : Γ , τ)
: Γ , τ τ
| inj {vars} {Γ : ctx vars} τ τ
(x : Γ , τ)
: Γ , τ τ
(* reflection rule for additive truth; *)
| forget {vars} (Γ : ctx vars)
: Γ ,
(* dually, reflection rule for additive falsity; *)
| absurd {covars} (Δ : ctx covars)
: , 0 Δ
(* there is no converse formation rule. *)
(* formation rule for multiplicative conjunction; *)
| split {covars} {Δ : ctx covars} {τ τ}
(f : , τ, τ Δ)
: , τ τ Δ
(* dually, formation rule for multiplicative disjunction; *)
| cosplit {vars} {Γ : ctx vars} {τ τ}
(f : Γ , τ, τ)
: Γ , τ τ
(* conversely, reflection rule for multiplicative conjunction; *)
| pair {vars vars} {Γ : ctx vars} {Γ : ctx vars} {τ τ}
(x : Γ , τ)
(x : Γ , τ)
: Γ ,+ Γ , τ τ
(* dually, reflection rule for multiplicative disjunction. *)
| copair {covars covars} {Δ : ctx covars} {Δ : ctx covars} {τ τ}
(x : , τ Δ)
(x : , τ Δ)
: , τ τ Δ ,+ Δ
(* formation rule for multiplicative truth; *)
| ununit {covars} {Δ : ctx covars}
(f : Δ)
: , 1 Δ
(* dually, formation rule for multiplicative falsity; *)
| done {vars} {Γ : ctx vars}
(f : Γ )
: Γ ,
(* conversely, reflection rule for multiplicative truth; *)
| unit : , 1
(* dually, reflection rule for multiplicative falsity. *)
| undone : ,
where "Γ '⊢' Δ" := (entails Γ Δ).
Fixpoint cut {vars covars} {Γ : ctx vars} {Δ : ctx covars} {τ}
(x : Γ , τ)
(y : , τ Δ)
: Γ Δ.
destruct x eqn:Ex.
- assumption.
- admit.
-admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- apply absurd.
- admit.
- admit.
- admit.
- admit.
- apply ununit.
Admitted.
(*.
intros.
induction x eqn:Ex, y eqn:Ey;
try constructor; try assumption;
try (apply (IHe1 e1)); try (apply (IHe2 e2)); try assumption; try reflexivity.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
-
(*
induction x eqn:Ex, y eqn:Ey;
(* cuts involving an axiom *)
try (constructor; try assumption).
- discriminate.*)
Admitted.*)

@ -1,79 +0,0 @@
{-# OPTIONS --safe --without-K #-}
module Darius.Basic where
import Data.Fin as Fin
open Fin using (Fin)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product hiding (zip)
open import Data.Sum
open import Data.Vec hiding (zip; unzip; split)
open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary.PropositionalEquality hiding (subst)
variable n n₁ n₂ n₃ n₄ n₅ :
-- This system is not dependently-typed.
data Type : Set where
-- multiplicative conjunction & unit
_⊗_ : Type → Type → Type
1' : Type
-- additive disjunction & zero
_⊕_ : Type → Type → Type
0' : Type
-- additive conjunction & top
_&_ : Type → Type → Type
: Type
-- multiplicative disjunction & bottom
_⅋_ : Type → Type → Type
⊥ : Type
-- implication
_⇒_ : Type → Type → Type
-- exclusion
_⇐_ : Type → Type → Type
infix 18 _⊗_ _&_
infix 17 _⊕_ _⅋_
infix 16 _⇒_ _⇐_
-- A term with `leftCtx` variables in the left context
-- and `rightCtx` variables in the right context.
data Term : (leftCtx rightCtx : ) → Set where
-- variable
var : Term 1 1
-- constructors and eliminators for multiplicative conjunction
pair : ∀ {left₁ left₂} → (x : Term left₁ 1) → (y : Term left₂ 1) → Term (left₁ + left₂) 1
unpair : ∀ {right} → (xy : Term 2 right) → Term 1 right
unit : Term 0 1
ununit : ∀ {right} → (x : Term 0 right) → Term 1 right
-- additive disjunction
σ₁ σ₂ : ∀ {left} → (τ : Type) → (x : Term left 1) → Term left 1
case : ∀ {right} → (f g : Term 1 right) → Term 1 right
forget : ∀ {left} → Term left 1
-- additive conjunction
split : ∀ {left} → (f g : Term left 1) → Term left 1
π₁ π₂ : ∀ {right} → (τ : Type) → (x : Term 1 right) → Term 1 right
absurd : ∀ {right} → Term 1 right
-- multiplicative disjunction
par : ∀ {left} → (xy : Term left 2) → Term left 1
unpar : ∀ {right₁ right₂} → Term 1 right₁ → Term 1 right₂ → Term 1 (right₁ + right₂)
bot : ∀ {left} → Term left 0 → Term left 1
-- implication
λ' : Term 1 1 → Term 0 1
app : ∀ {right} → Term 0 1 → Term 1 right → Term 1 right
-- exclusion
Λ' : ∀ {left} → Term left 1 → Term 1 0 → Term left 1
App : Term 1 1 → Term 1 0
`Γ , var : τ' , Λ ⊢ expr : τ` and `Δ ⊢ val : τ'` then `Γ , Δ , Λ ⊢ expr {var := val} : τ`

@ -1,239 +0,0 @@
{-# OPTIONS --with-K --guardedness #-}
module Darius.Derivation where
open import Darius.Derivation.Type
open import Darius.Permutation
open import Darius.Term
import Data.Fin as Fin
open Fin using (Fin)
open import Data.Maybe hiding (zip)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product hiding (zip)
open import Relation.Binary.PropositionalEquality renaming (subst to transp)
infix 10 _⊢_↦_∷_ _⊢_↦*_∷_ _⊢_↓_∷_
data _⊢_↦_∷_ : (Γ : Context n) (x₁ x₂ : Term n) (τ : Type) → Set
↦∷₁ : ∀ {Γ : Context n} {τ x₁ x₂} → Γ ⊢ x₁ ↦ x₂ ∷ τ → Γ ⊢ x₁ ∷ τ
↦∷₂ : ∀ {Γ : Context n} {τ x₁ x₂} → Γ ⊢ x₁ ↦ x₂ ∷ τ → Γ ⊢ x₂ ∷ τ
subst↦ : ∀ {Γ : Context n₁} {Δ : Context n₂} {Λ : Context n₃} {τe τx e x}
→ Δ ⊢ x ∷ τx
→ Γ ,c τx ++c Λ ⊢ e ∷ τe
→ ∃ λ e' → Γ ++c Δ ++c Λ ⊢ e' ∷ τe
data _⊢_↦_∷_ where
-- | Reduce arbitrary subterms.
↦-subst
: ∀ {size} {Γ : Context n₁} {Δ : Context size} {Λ : Context n₃} {τe τx}
{e : TermZ (n₃ + n₁) 0} {x₁ x₂ : Term size}
→ (xr : Δ ⊢ x₁ ↦ x₂ ∷ τx)
→ (ety : Γ ,c τx ++c Λ ⊢ zip (tz-cast₁ (sq-eq (sym (+-suc _ _))) (dilate1 e)) var ∷ τe)
--------------------------------------------------------------------------------
→ Γ ++c Δ ++c Λ ⊢ zip (tz-cast₁ (sq-eq (trans (sym (+-assoc size n₃ n₁)) (trans (cong (_+ n₁) (+-comm size n₃)) (+-assoc n₃ size n₁)))) (dilate e)) (term-cast (sq-eq (sym (+-identityʳ _))) x₁)
↦ zip (tz-cast₁ (sq-eq ((trans (sym (+-assoc size n₃ n₁)) (trans (cong (_+ n₁) (+-comm size n₃)) (+-assoc n₃ size n₁))))) (dilate e)) (term-cast (sq-eq (sym (+-identityʳ _))) x₂) ∷ τe
σ₁-β
: ∀ {Γ : Context n₁} {Δ : Context n₂} {τ τ₁ τ₂ x f g}
→ (xty : Δ ⊢ x ∷ τ₁)
→ (fty : Γ ,c τ₁ ⊢ f ∷ τ)
→ (gty : Γ ,c τ₂ ⊢ g ∷ τ) -- opt
--------------------------------------------------------------
→ Γ ++c Δ ⊢ rec⊕ permu-split (σ₁ τ₂ x) f g ↦ subst1 f x ∷ τ
σ₂-β
: ∀ {Γ : Context n₁} {Δ : Context n₂} {τ τ₁ τ₂ y f g}
→ (yty : Δ ⊢ y ∷ τ₂)
→ (fty : Γ ,c τ₁ ⊢ f ∷ τ) -- opt
→ (gty : Γ ,c τ₂ ⊢ g ∷ τ)
--------------------------------------------------------------
→ Γ ++c Δ ⊢ rec⊕ permu-split (σ₂ τ₁ y) f g ↦ subst1 g y ∷ τ
rec⊕-η
: ∀ {Γ : Context n} {τ₁ τ₂ x}
→ (xty : Γ ⊢ x ∷ τ₁ ⊕ τ₂) -- opt
-----------------------------------------------------------------------------
→ Γ ⊢ rec⊕ permu-all-left x (σ₁ τ₂ var) (σ₂ τ₁ var) ↦ x ∷ τ₁ ⊕ τ₂
π₁-β
: ∀ {Γ : Context n} {τ₁ τ₂ f g}
→ (fty : Γ ⊢ f ∷ τ₁) -- opt
→ (gty : Γ ⊢ g ∷ τ₂) -- opt
----------------------------
→ Γ ⊢ π₁ τ₂ (pro& f g) ↦ f ∷ τ₁
π₂-β
: ∀ {Γ : Context n} {τ₁ τ₂ f g}
→ (fty : Γ ⊢ f ∷ τ₁) -- opt
→ (gty : Γ ⊢ g ∷ τ₂) -- opt
----------------------------
→ Γ ⊢ π₂ τ₁ (pro& f g) ↦ g ∷ τ₂
pro&-η
: ∀ {Γ : Context n} {τ₁ τ₂ x}
→ (xty : Γ ⊢ x ∷ τ₁ & τ₂) -- opt
--------------------------------------
→ Γ ⊢ pro& (π₁ τ₂ x) (π₂ τ₁ x) ↦ x ∷ τ₁ & τ₂
unit-β
: ∀ {Γ : Context n} {τ x}
→ (xty : Γ ⊢ x ∷ τ) -- opt
-------------------------------
→ Γ ⊢ rec1 permu-all-right unit x ↦ x ∷ τ
rec1-η
: ∀ {Γ : Context n} {x}
→ (xty : Γ ⊢ x ∷ 1') -- opt
-----------------------------------------------------------
→ Γ ⊢ rec1 permu-all-left x unit ↦ x ∷ 1'
pair-β
: ∀ {Γ : Context n₁} {Δ : Context n₂} {Λ : Context n₃} {τ τ₁ τ₂ x y f}
→ (xty : Δ ⊢ x ∷ τ₁)
→ (yty : Γ ⊢ y ∷ τ₂)
→ (fty : Λ ,c τ₁ ,c τ₂ ⊢ f ∷ τ)
---------------------------------------------------------------------------------
→ Λ ++c Γ ++c Δ
⊢ rec⊗ (permu-assoc-left n₂) (pair permu-split x y) f
↦ subst (transp Term (+-suc n₁ n₃) (subst f Fin.zero y)) (Fin.cast (+-suc _ _) (n₁ Fin.↑ʳ Fin.from n₃)) x
∷ τ
rec⊗-η
: ∀ {Γ : Context n} {τ₁ τ₂ x}
→ (xty : Γ ⊢ x ∷ τ₁ ⊗ τ₂) -- opt
--------------------------------------------------------------------------------
→ Γ ⊢ rec⊗ permu-all-left x (pair permu-split var var)
↦ x ∷ τ₁ ⊗ τ₂
λ-β
: ∀ {Γ : Context n₁} {Δ : Context n₂} {τ₁ τ₂ f x}
→ (fty : Γ ,c τ₁ ⊢ f ∷ τ₂)
→ (xty : Δ ⊢ x ∷ τ₁)
--------------------------------------------------------------------------------
→ Γ ++c Δ ⊢ app permu-split-comm (λ' τ₁ f) x ↦ subst1 f x ∷ τ₂
app-η
: ∀ {Γ : Context n} {τ₁ τ₂ f}
→ (fty : Γ ⊢ f ∷ τ₁ ⊸ τ₂) -- opt
----------------------------------------------------------
→ Γ ⊢ λ' τ₁ (app (permu-right permu-all-left) f var) ↦ f ∷ τ₁ ⊸ τ₂
zero-β
: ∀ {Γ : Context n} {τ base rec}
→ (basety : Γ ⊢ base ∷ τ) -- opt
→ (recty : ∅c ,c τ ⊢ rec ∷ τ)
------------------------------------------
→ Γ ⊢ rec permu-all-right zero' base rec ↦ base ∷ τ
suc-β
: ∀ {Γ : Context n₁} {Δ : Context n₂} {τ x base rec}
→ (xty : Γ ⊢ x ∷ ')
→ (basety : Δ ⊢ base ∷ τ)
→ (recty : ∅c ,c τ ⊢ rec ∷ τ)
---------------------------------------------------------------------------------------------
→ ∅c ++c (Γ ++c Δ)
⊢ rec (transp (λ i → Permute i n₁ n₂) (sym (+-identityʳ _)) permu-split-comm) (suc' x) base rec
↦ subst1 rec (rec permu-split-comm x base rec)
∷ τ
rec
: ∀ {Γ : Context n} {x}
→ (xty : Γ ⊢ x ∷ ') -- opt
-----------------------------------------------------------------------
→ Γ ⊢ rec permu-all-left x zero' (suc' var) ↦ x ∷ '
data _⊢_↦*_∷_ (Γ : Context n) : (x₁ x₂ : Term n) (τ : Type) → Set where
↦*-refl : ∀ {τ x} → Γ ⊢ x ∷ τ → Γ ⊢ x ↦* x ∷ τ
↦*-step : ∀ {τ x₁ x₂ x₃} → Γ ⊢ x₁ ↦* x₂ ∷ τ → Γ ⊢ x₂ ↦ x₃ ∷ τ → Γ ⊢ x₁ ↦* x₃ ∷ τ
_⊢_↓_∷_ : (Γ : Context n) (x₁ x₂ : Term n) (τ : Type) → Set
Γ ⊢ x₁ ↓ x₂ ∷ τ = ∃ λ x₃ → Γ ⊢ x₁ ↦ x₃ ∷ τ × Γ ⊢ x₂ ↦ x₃ ∷ τ
{-
↦∷₁ (↦-subst r ety) = proj₂ (subst↦ (↦∷₁ r) ety)
↦∷₁ (σ₁-β xty fty gty) = rec⊕-type (perm-comm perm-split) {_} {refl} (σ₁-type xty) fty gty
↦∷₁ (σ₂-β yty fty gty) = rec⊕-type (perm-comm perm-split) {_} {refl} (σ₂-type yty) fty gty
↦∷₁ (rec⊕-η xty) = rec⊕-type perm-all-left {_} {refl} xty (σ₁-type var-type) (σ₂-type var-type)
↦∷₁ (π₁-β fty gty) = π₁-type (pro&-type fty gty)
↦∷₁ (π₂-β fty gty) = π₂-type (pro&-type fty gty)
↦∷₁ (pro&-η xty) = pro&-type (π₁-type xty) (π₂-type xty)
↦∷₁ (unit-β xty) = rec1-type perm-all-right {_} {refl} unit-type xty
↦∷₁ (rec1-η xty) = rec1-type perm-all-left {_} {refl} xty unit-type
↦∷₁ (pair-β {Γ = Γ} xty yty fty) = rec⊗-type (perm-thing Γ) {_} {refl} (pair-type perm-split {_} {refl} xty yty) fty
↦∷₁ (rec⊗-η xty) = rec⊗-type perm-all-left {_} {refl} xty (pair-type (perm-right (perm-left perm-done)) {_} {refl} var-type var-type)
↦∷₁ (λ-β fty xty) = app-type perm-split {_} {refl} (λ-type fty) xty
↦∷₁ (app-η fty) = λ-type (app-type perm-split {_} {refl} fty var-type)
↦∷₁ (zero-β basety recty) = rec-type perm-all-right {_} {refl} zero-type basety recty
↦∷₁ (suc-β {Γ = Γ} xty basety recty) = rec-type (perm-unfuck perm-split) {_} {refl} (suc-type xty) basety recty
↦∷₁ (rec-η xty) = rec-type perm-all-left {_} {refl} xty zero-type (suc-type var-type)
-}
↦∷₂ (↦-subst r ety) = {!!}
↦∷₂ (σ₁-β xty fty gty) = {!!}
↦∷₂ (σ₂-β yty fty gty) = {!!}
↦∷₂ (rec⊕-η xty) = xty
↦∷₂ (π₁-β fty gty) = fty
↦∷₂ (π₂-β fty gty) = gty
↦∷₂ (pro&-η xty) = xty
↦∷₂ (unit-β xty) = xty
↦∷₂ (rec1-η xty) = xty
↦∷₂ (pair-β xty yty fty) = {!!}
↦∷₂ (rec⊗-η xty) = xty
↦∷₂ (λ-β fty xty) = {!!}
↦∷₂ (app-η fty) = fty
↦∷₂ (zero-β basety recty) = basety
↦∷₂ (suc-β xty basety recty) = {!!}
↦∷₂ (rec-η xty) = xty
↦*∷₁ : ∀ {Γ : Context n} {τ x₁ x₂} → Γ ⊢ x₁ ↦* x₂ ∷ τ → Γ ⊢ x₁ ∷ τ
↦*∷₁ (↦*-refl x) = x
↦*∷₁ (↦*-step xr x) = ↦*∷₁ xr
↦*∷₂ : ∀ {Γ : Context n} {τ x₁ x₂} → Γ ⊢ x₁ ↦* x₂ ∷ τ → Γ ⊢ x₂ ∷ τ
↦*∷₂ (↦*-refl x) = x
↦*∷₂ (↦*-step xr x) = ↦∷₂ x
{-
subst↦ {Γ = Γ} {Δ = Δ} {Λ = Λ} {τx = τx} xty ety = subst (help Λ (subst-next subst-empty xty)) ety
where
help : (Θ : Context n) → Subst (Γ ,c τx) (Γ ++c Δ) → Subst (Γ ,c τx ++c Θ) (Γ ++c Δ ++c Θ)
help ∅c ss = ss
help (Θ ,c x) ss = subst-next (help Θ ss) var-type
↦*-subst
: ∀ {Γ : Context n₁} {Δ : Context n₂} {Λ : Context n₃} {τe τx e x₁ x₂}
→ (xr : Δ ⊢ x₁ ↦* x₂ ∷ τx)
→ (ty₁ : Δ ⊢ x₁ ∷ τx)
→ (ty₂ : Δ ⊢ x₂ ∷ τx)
→ (ety : Γ ,c τx ++c Λ ⊢ e ∷ τe)
-----------------------------------------------------------------------------------
→ Γ ++c Δ ++c Λ ⊢ proj₁ (subst↦ ty₁ ety) ↦* proj₁ (subst↦ ty₂ ety) ∷ τe
↦*-subst (↦*-refl x) ty₁ ty₂ ety with unique-type-deriv ty₁ ty₂
... | refl = ↦*-refl (proj₂ (subst↦ ty₁ ety))
↦*-subst (↦*-step xr x) ty₁ ty₂ ety with unique-type-deriv (↦∷₂ x) ty₂
... | refl = ↦*-step (↦*-subst xr ty₁ (↦∷₁ x) ety) (↦-subst x ety)
fuck-↦* : ∀ {Γ : Context n} {τ x₁ x₂} → ∅c ++c Γ ⊢ x₁ ↦* x₂ ∷ τ → Γ ⊢ transp Term (+-identityʳ n) x₁ ↦* transp Term (+-identityʳ n) x₂ ∷ τ
fuck-↦* = coerce
reduce-step : ∀ {Γ : Context n} {τ} {x} (xty : Γ ⊢ x ∷ τ) → Maybe (∃ λ x' → Γ ⊢ x ↦* x' ∷ τ)
reduce-step var-type = nothing
reduce-step (absurd-type {τ = τ} xty) with reduce-step xty
... | just (x , r) rewrite unique-type-deriv xty (↦*∷₁ r) = just (absurd τ x , {!fuck-↦* (↦*-subst {Γ = ∅c} {Λ = ∅c} r xty (↦*∷₂ r) (absurd-type {τ = τ} var-type))!})
... | nothing = nothing
reduce-step (σ₁-type xty) = {!!}
reduce-step (σ₂-type xty) = {!!}
reduce-step (rec⊕-type p xty xty₁ xty₂) = {!!}
reduce-step (forget-type xty) = {!!}
reduce-step (π₁-type xty) = {!!}
reduce-step (π₂-type xty) = {!!}
reduce-step (pro&-type xty xty₁) = {!!}
reduce-step unit-type = {!!}
reduce-step (rec1-type p xty xty₁) = {!!}
reduce-step (pair-type p xty xty₁) = {!!}
reduce-step (rec⊗-type p xty xty₁) = {!!}
reduce-step (λ-type xty) = {!!}
reduce-step (app-type p xty xty₁) = {!!}
reduce-step zero-type = nothing
reduce-step (suc-type xty) = {!!}
reduce-step (rec-type p xty xty₁ xty₂) = {!!}
-}
x + y = (x +' y ⊔ y +' x) (+'-comm x y)
where
x +' zero = x
x +' suc y = suc (x + y)
+'-comm x y = -- ...

@ -1,269 +0,0 @@
{-# OPTIONS --safe --with-K #-}
module Darius.Derivation.Type where
open import Darius.Permutation
open import Darius.Term
import Data.Fin as Fin
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product hiding (zip)
open import Relation.Binary.PropositionalEquality hiding (subst)
-- | A context of `n` types.
data Context : (n : ) → Set where
∅c : Context 0
_,c_ : (Γ : Context n) → (τ : Type) → Context (suc n)
infixl 15 _,c_ _++c_
variable Γ Γ₁ Γ₂ Δ Δ₁ Δ₂ Λ Λ₁ Λ₂ : Context n
ctx-cast : ∀ {n n'} → n ≐ n' → Context n → Context n'
ctx-cast {zero} {zero} p ∅c = ∅c
ctx-cast {suc n} {suc n'} p (Γ ,c τ) = ctx-cast (suc-inj-irr p) Γ ,c τ
_++c_ : (Γ₁ : Context n₁) (Γ₂ : Context n₂) → Context (n₂ + n₁)
Γ₁ ++c ∅c = Γ₁
Γ₁ ++c (Γ₂ ,c x) = (Γ₁ ++c Γ₂) ,c x
++-id : (Γ : Context n) → ∅c ++c Γ ≡ ctx-cast (sq-eq (sym (+-identityʳ n))) Γ
++-id ∅c = refl
++-id {suc n} (Γ ,c x) = cong (_,c x) (++-id Γ)
perm : Permute n n₁ n₂ → Context n₁ → Context n₂ → Context n
perm permu-done ∅c ∅c = ∅c
perm (permu-left p) (Γ ,c x) Δ = perm p Γ Δ ,c x
perm (permu-right p) Γ (Δ ,c x) = perm p Γ Δ ,c x
,c-inj : ∀ {x₁ x₂ : Context n} {y₁ y₂} → x₁ ,c y₁ ≡ x₂ ,c y₂ → x₁ ≡ x₂ × y₁ ≡ y₂
,c-inj refl = refl , refl
perm-eq : {p : Permute n n₁ n₂} {Δ₁ Δ₂ : Context n₁} {Λ₁ Λ₂ : Context n₂}
→ perm p Δ₁ Λ₁ ≡ perm p Δ₂ Λ₂ → Δ₁ ≡ Δ₂ × Λ₁ ≡ Λ₂
perm-eq {p = permu-done} {∅c} {∅c} {∅c} {∅c} _ = refl , refl
perm-eq {p = permu-left p} {Δ₁ ,c x} {Δ₂ ,c x₁} q with ,c-inj q
... | q' , refl with perm-eq q'
... | refl , refl = refl , refl
perm-eq {p = permu-right p} {_} {_} {Λ₁ ,c x} {Λ₂ ,c x₁} q with ,c-inj q
... | q' , refl with perm-eq q'
... | refl , refl = refl , refl
infix 10 _⊢_∷_
data _⊢_∷_ : (Γ : Context n) → Term n → Type → Set where
var-type
: ∀ {τ}
-------------------
→ ∅c ,c τ ⊢ var ∷ τ
absurd-type
: ∀ {Γ : Context n} {τ x}
→ (xty : Γ ⊢ x ∷ 0')
------------------
→ Γ ⊢ absurd τ x ∷ τ
σ₁-type
: ∀ {τ₁ τ₂ x}
→ (xty : Γ ⊢ x ∷ τ₁)
---------------------
→ Γ ⊢ σ₁ τ₂ x ∷ τ₁ ⊕ τ₂
σ₂-type
: ∀ {τ₁ τ₂ x}
→ (xty : Γ ⊢ x ∷ τ₂)
---------------------
→ Γ ⊢ σ₂ τ₁ x ∷ τ₁ ⊕ τ₂
rec⊕-type
: ∀ {Γ : Context n} {Δ : Context n₁} {Λ : Context n₂} {τ₁ τ₂ τ₃ x f g}
→ (pu : Permute n n₁ n₂) {pr : Γ ≡ perm pu Δ Λ}
→ (xty : Δ ⊢ x ∷ τ₁ ⊕ τ₂)
→ (fty : Λ ,c τ₁ ⊢ f ∷ τ₃)
→ (gty : Λ ,c τ₂ ⊢ g ∷ τ₃)
-----------------------------
→ Γ ⊢ rec⊕ pu x f g ∷ τ₃
forget-type
: ∀ {τ x}
→ (xty : Γ ⊢ x ∷ τ)
-------------------
→ Γ ⊢ forget x ∷ '
π₁-type
: ∀ {τ₁} τ₂ {x}
→ (xty : Γ ⊢ x ∷ τ₁ & τ₂)
------------------
→ Γ ⊢ π₁ τ₂ x ∷ τ₁
π₂-type
: ∀ τ₁ {τ₂ x}
→ (xty : Γ ⊢ x ∷ τ₁ & τ₂)
------------------
→ Γ ⊢ π₂ τ₁ x ∷ τ₂
pro&-type
: ∀ {τ₁ τ₂ x₁ x₂}
→ (fty : Γ ⊢ x₁ ∷ τ₁)
→ (gty : Γ ⊢ x₂ ∷ τ₂)
--------------------------
→ Γ ⊢ pro& x₁ x₂ ∷ τ₁ & τ₂
unit-type
----------------
: ∅c ⊢ unit ∷ 1'
rec1-type
: ∀ {Γ : Context n} {Δ : Context n₁} {Λ : Context n₂} {τ u x}
→ (pu : Permute n n₁ n₂) {pr : Γ ≡ perm pu Δ Λ}
→ (xty : Δ ⊢ u ∷ 1')
→ (fty : Λ ⊢ x ∷ τ)
--------------------------
→ Γ ⊢ rec1 pu u x ∷ τ
pair-type
: ∀ {Γ : Context n} {Δ : Context n₁} {Λ : Context n₂} {τ₁ τ₂ x₁ x₂}
→ (pu : Permute n n₁ n₂) {pr : Γ ≡ perm pu Δ Λ}
→ (xty : Δ ⊢ x₁ ∷ τ₁)
→ (yty : Λ ⊢ x₂ ∷ τ₂)
-----------------------------------
→ Γ ⊢ pair pu x₁ x₂ ∷ τ₁ ⊗ τ₂
rec⊗-type
: ∀ {Γ : Context n} {Δ : Context n₁} {Λ : Context n₂} {τ₁ τ₂ τ₃ x f}
→ (pu : Permute n n₁ n₂) {pr : Γ ≡ perm pu Δ Λ}
→ (xty : Δ ⊢ x ∷ τ₁ ⊗ τ₂)
→ (fty : Λ ,c τ₁ ,c τ₂ ⊢ f ∷ τ₃)
---------------------------
→ Γ ⊢ rec⊗ pu x f ∷ τ₃
λ-type
: ∀ {τ₂ f}
→ (τ₁ : Type)
→ (fty : Γ ,c τ₁ ⊢ f ∷ τ₂)
--------------------
→ Γ ⊢ λ' τ₁ f ∷ τ₁ ⊸ τ₂
app-type
: ∀ {Γ : Context n} {Γ₁ : Context n₁} {Γ₂ : Context n₂} {τ₁ τ₂ f x}
→ (pu : Permute n n₁ n₂) {pr : Γ ≡ perm pu Γ₁ Γ₂}
→ (fty : Γ₁ ⊢ f ∷ τ₁ ⊸ τ₂)
→ (xty : Γ₂ ⊢ x ∷ τ₁)
--------------------------
→ Γ ⊢ app pu f x ∷ τ₂
zero-type
-----------------
: ∅c ⊢ zero' ∷ '
suc-type
: ∀ {x}
→ (xty : Γ ⊢ x ∷ ')
-----------------
→ Γ ⊢ suc' x ∷ '
rec-type
: ∀ {Γ : Context n} {Γ₁ : Context n₁} {Γ₂ : Context n₂} {τ x base rec}
→ (pu : Permute n n₁ n₂) {pr : Γ ≡ perm pu Γ₁ Γ₂}
→ (xty : Γ₁ ⊢ x ∷ ')
→ (basety : Γ₂ ⊢ base ∷ τ)
→ (recty : ∅c ,c τ ⊢ rec ∷ τ)
→ Γ ⊢ rec pu x base rec ∷ τ
{-
ty-castΓ : ∀ {Γ Γ' : Context n} {τ x} → Γ ⊢ x ∷ τ → Γ ≐ Γ' → Γ' ⊢ x ∷ τ
ty-castΓ {Γ = ∅c} {∅c} ty p = ty
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (absurd-type ty) p = absurd-type (ty-castΓ ty p)
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (σ₁-type ty) p = σ₁-type (ty-castΓ ty p)
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (σ₂-type ty) p = σ₂-type (ty-castΓ ty p)
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (rec⊕-type pu ty ty₁ ty₂) p = rec⊕-type pu (ty-castΓ ty {!p!}) (ty-castΓ ty₁ {!!}) (ty-castΓ ty₂ {!!})
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (forget-type ty) p = forget-type (ty-castΓ ty p)
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (π₁-type τ₂ ty) p = π₁-type τ₂ (ty-castΓ ty p)
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (π₂-type τ₂ ty) p = π₂-type τ₂ (ty-castΓ ty p)
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (pro&-type ty ty₁) p = pro&-type (ty-castΓ ty p) (ty-castΓ ty₁ p)
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (rec1-type pu ty ty₁) p = rec1-type pu {!!} {!!}
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (pair-type pu ty ty₁) p = pair-type pu {!!} {!!}
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (rec⊗-type pu ty ty₁) p = rec⊗-type pu {!!} {!!}
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (λ-type τ₂ ty) p = λ-type τ₂ (ty-castΓ ty (cong-irr (_,c τ₂) p))
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (app-type pu ty ty₁) p = app-type pu {!!} {!!}
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (suc-type ty) p = suc-type (ty-castΓ ty p)
ty-castΓ {Γ = Γ ,c τ} {Γ' ,c τ₁} (rec-type pu ty ty₁ ty₂) p = rec-type pu {!!} {!!} {!!}
ty-castΓ {Γ = .∅c ,c τ} {∅c ,c τ₁} var-type p = {!var-type!}
-}
-- | Every well-typed term has a unique type in a context.
unique-type : ∀ {Γ : Context n} {τ₁ τ₂ x} → Γ ⊢ x ∷ τ₁ → Γ ⊢ x ∷ τ₂ → τ₁ ≡ τ₂
-- | There is only one way to derive that a term has a type in a context.
unique-type-deriv : ∀ {Γ : Context n} {τ x} → (ty₁ ty₂ : Γ ⊢ x ∷ τ) → ty₁ ≡ ty₂
-- | Substitution of well-typed terms preserves typing.
ty-subst : ∀ {size ctx ix} {Δ : Context size} {Γ : Context ctx} {τ₁ τ₂ x val}
→ (Λ : Context ix)
→ Γ ,c τ₁ ++c Λ ⊢ x ∷ τ₂
→ Δ ⊢ val ∷ τ₁
→ Γ ++c Δ ++c Λ ⊢ term-cast (sq-eq (trans (sym (+-assoc size ix ctx)) (trans (cong (_+ ctx) (+-comm size ix)) (+-assoc ix size ctx))))
(subst (term-cast (sq-eq (+-suc ix ctx))
x) (Fin.from _) val) ∷ τ₂
unique-type var-type var-type = refl
unique-type (absurd-type ty₁) (absurd-type ty₂) = refl
unique-type (σ₁-type ty₁) (σ₁-type ty₂) rewrite unique-type ty₁ ty₂ = refl
unique-type (σ₂-type ty₁) (σ₂-type ty₂) rewrite unique-type ty₁ ty₂ = refl
unique-type (rec⊕-type pu {pr} ty₁ ty₃ ty₄) (rec⊕-type .pu {refl} ty₂ ty₅ ty₆) with perm-eq pr
... | refl , refl with ⊕-injective (unique-type ty₁ ty₂)
... | refl , refl rewrite unique-type ty₃ ty₅ = refl
unique-type (forget-type ty₁) (forget-type ty₂) rewrite unique-type ty₁ ty₂ = refl
unique-type (π₁-type τ ty₁) (π₁-type .τ ty₂) rewrite proj₁ (&-injective (unique-type ty₁ ty₂)) = refl
unique-type (π₂-type τ ty₁) (π₂-type .τ ty₂) rewrite proj₂ (&-injective (unique-type ty₁ ty₂)) = refl
unique-type (pro&-type ty₁ ty₃) (pro&-type ty₂ ty₄) rewrite unique-type ty₁ ty₂ | unique-type ty₃ ty₄ = refl
unique-type unit-type unit-type = refl
unique-type (rec1-type pu {pr} ty₁ ty₃) (rec1-type .pu {refl} ty₂ ty₄) with perm-eq pr
... | refl , refl rewrite unique-type ty₁ ty₂ | unique-type ty₃ ty₄ = refl
unique-type (pair-type pu {pr} ty₁ ty₃) (pair-type .pu {refl} ty₂ ty₄) with perm-eq pr
... | refl , refl rewrite unique-type ty₁ ty₂ | unique-type ty₃ ty₄ = refl
unique-type (rec⊗-type pu {pr} ty₁ ty₃) (rec⊗-type .pu {refl} ty₂ ty₄) with perm-eq pr
... | refl , refl with ⊗-injective (unique-type ty₁ ty₂)
... | refl , refl rewrite unique-type ty₃ ty₄ = refl
unique-type (λ-type τ ty₁) (λ-type τ₁ ty₂) rewrite unique-type ty₁ ty₂ = refl
unique-type (app-type pu {pr} ty₁ ty₃) (app-type .pu {refl} ty₂ ty₄) with perm-eq pr
... | refl , refl with ⊸-injective (unique-type ty₁ ty₂)
... | refl , refl = refl
unique-type zero-type zero-type = refl
unique-type (suc-type ty₁) (suc-type ty₂) = refl
unique-type (rec-type pu {pr} ty₁ ty₃ ty₄) (rec-type .pu {refl} ty₂ ty₅ ty₆) with perm-eq pr
... | refl , refl rewrite unique-type ty₃ ty₅ = refl
unique-type-deriv var-type var-type = refl
unique-type-deriv (absurd-type ty₁) (absurd-type ty₂) rewrite unique-type-deriv ty₁ ty₂ = refl
unique-type-deriv (σ₁-type ty₁) (σ₁-type ty₂) rewrite unique-type-deriv ty₁ ty₂ = refl
unique-type-deriv (σ₂-type ty₁) (σ₂-type ty₂) rewrite unique-type-deriv ty₁ ty₂ = refl
unique-type-deriv (rec⊕-type pu {pr} ty₁ ty₃ ty₄) (rec⊕-type .pu {refl} ty₂ ty₅ ty₆) with perm-eq pr
... | refl , refl with ⊕-injective (unique-type ty₁ ty₂)
unique-type-deriv (rec⊕-type _ {refl} ty₁ ty₃ ty₄) (rec⊕-type _ {refl} ty₂ ty₅ ty₆) | refl , refl | refl , refl rewrite unique-type-deriv ty₁ ty₂ | unique-type-deriv ty₃ ty₅ | unique-type-deriv ty₄ ty₆ = refl
unique-type-deriv (forget-type ty₁) (forget-type ty₂) with unique-type ty₁ ty₂
... | refl rewrite unique-type-deriv ty₁ ty₂ = refl
unique-type-deriv (π₁-type τ₂ ty₁) (π₁-type .τ₂ ty₂) rewrite unique-type-deriv ty₁ ty₂ = refl
unique-type-deriv (π₂-type τ₁ ty₁) (π₂-type .τ₁ ty₂) rewrite unique-type-deriv ty₁ ty₂ = refl
unique-type-deriv (pro&-type ty₁ ty₃) (pro&-type ty₂ ty₄) rewrite unique-type-deriv ty₁ ty₂ | unique-type-deriv ty₃ ty₄ = refl
unique-type-deriv unit-type unit-type = refl
unique-type-deriv (rec1-type pu {pr} ty₁ ty₃) (rec1-type .pu {refl} ty₂ ty₄) with perm-eq pr
unique-type-deriv (rec1-type _ {refl} ty₁ ty₃) (rec1-type _ {refl} ty₂ ty₄) | refl , refl rewrite unique-type-deriv ty₁ ty₂ | unique-type-deriv ty₃ ty₄ = refl
unique-type-deriv (pair-type pu {pr} ty₁ ty₃) (pair-type .pu {refl} ty₂ ty₄) with perm-eq pr
unique-type-deriv (pair-type _ {refl} ty₁ ty₃) (pair-type _ {refl} ty₂ ty₄) | refl , refl rewrite unique-type-deriv ty₁ ty₂ | unique-type-deriv ty₃ ty₄ = refl
unique-type-deriv (rec⊗-type pu {pr} ty₁ ty₃) (rec⊗-type .pu {refl} ty₂ ty₄) with perm-eq pr
... | refl , refl with ⊗-injective (unique-type ty₁ ty₂)
unique-type-deriv (rec⊗-type _ {refl} ty₁ ty₃) (rec⊗-type _ {refl} ty₂ ty₄) | refl , refl | refl , refl rewrite unique-type-deriv ty₁ ty₂ | unique-type-deriv ty₃ ty₄ = refl
unique-type-deriv (λ-type τ ty₁) (λ-type τ₁ ty₂) rewrite unique-type-deriv ty₁ ty₂ = refl
unique-type-deriv (app-type pu {pr} ty₁ ty₃) (app-type .pu {refl} ty₂ ty₄) with perm-eq pr
... | refl , refl with ⊸-injective (unique-type ty₁ ty₂)
unique-type-deriv (app-type _ {refl} ty₁ ty₃) (app-type _ {refl} ty₂ ty₄) | refl , refl | refl , refl rewrite unique-type-deriv ty₁ ty₂ | unique-type-deriv ty₃ ty₄ = refl
unique-type-deriv zero-type zero-type = refl
unique-type-deriv (suc-type ty₁) (suc-type ty₂) rewrite unique-type-deriv ty₁ ty₂ = refl
unique-type-deriv (rec-type pu {pr} ty₁ ty₃ ty₄) (rec-type .pu {refl} ty₂ ty₅ ty₆) with perm-eq pr
unique-type-deriv (rec-type _ {refl} ty₁ ty₃ ty₄) (rec-type _ {refl} ty₂ ty₅ ty₆) | refl , refl rewrite unique-type-deriv ty₁ ty₂ | unique-type-deriv ty₃ ty₅ | unique-type-deriv ty₄ ty₆ = refl
ty-subst ∅c var-type valty = {!!}
ty-subst {ctx = ctx} {ix = ix} Λ xty valty = {!!}
{-
ty-subst var-type valty = {!!}
ty-subst (absurd-type xty) valty = absurd-type (ty-subst xty valty)
ty-subst (σ₁-type xty) valty = σ₁-type {!!}
ty-subst (σ₂-type xty) valty = σ₂-type {!!}
ty-subst (rec⊕-type pu xty xty₁ xty₂) valty = {!!}
ty-subst (forget-type xty) valty = forget-type (ty-subst xty valty)
ty-subst (π₁-type τ₂ xty) valty = π₁-type τ₂ (ty-subst xty valty)
ty-subst (π₂-type τ₁ xty) valty = π₂-type τ₁ {!!}
ty-subst (pro&-type xty xty₁) valty = pro&-type {!!} {!!}
ty-subst (rec1-type pu xty xty₁) valty = rec1-type {!!} {!!} {!!}
ty-subst (pair-type pu xty xty₁) valty = pair-type {!!} {!!} {!!}
ty-subst (rec⊗-type pu xty xty₁) valty = rec⊗-type {!!} {!!} {!!}
ty-subst (λ-type τ xty) valty = λ-type τ {!ty-subst xty valty!}
ty-subst (app-type pu xty xty₁) valty = app-type {!!} {!!} {!!}
ty-subst (suc-type xty) valty = suc-type {!!}
ty-subst (rec-type pu xty xty₁ xty₂) valty = rec-type {!!} {!!} {!!} {!!}
-}

@ -1,166 +0,0 @@
{-# OPTIONS --safe #-}
module Darius.Permutation where
import Data.Fin as Fin
open Fin using (Fin)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality renaming (subst to transp)
private variable n n₁ n₂ n₃ n₄ n₅ :
infix 5 _≐_
data _≐_ {} {A : Set } (x : A) : A → Prop where
refl' : x ≐ x
sq-eq : ∀ {} {A : Set } {x y : A} → x ≡ y → x ≐ y
sq-eq refl = refl'
suc-inj-irr : ∀ {n₁ n₂ : } → .suc n₁ ≐ suc n₂ → n₁ ≐ n₂
suc-inj-irr refl' = refl'
trans-irr : ∀ {} {A : Set } {x₁ x₂ x₃ : A} → x₁ ≐ x₂ → x₁ ≐ x₃ → x₂ ≐ x₃
trans-irr refl' refl' = refl'
cong-irr : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A → B) {x₁ x₂} → x₁ ≐ x₂ → f x₁ ≐ f x₂
cong-irr _ refl' = refl'
recover-eq : (n₁ ≐ n₂) → n₁ ≡ n₂
recover-eq {zero} {zero} p = refl
recover-eq {suc n₁} {suc n₂} p = cong suc (recover-eq (suc-inj-irr p))
-- | Permutes its first argument across two sides: left and right.
data Permute : → Set where
permu-done : Permute 0 0 0
permu-left : Permute n n₁ n₂ → Permute (suc n) (suc n₁) n₂
permu-right : Permute n n₁ n₂ → Permute (suc n) n₁ (suc n₂)
permu-lefts : Permute n n₁ n₂ → Permute (n₃ + n) (n₃ + n₁) n₂
permu-lefts {n₃ = zero} perm = perm
permu-lefts {n₃ = suc n₃} perm = permu-left (permu-lefts perm)
permu-rights : Permute n n₁ n₂ → Permute (n₃ + n) n₁ (n₃ + n₂)
permu-rights {n₃ = zero} perm = perm
permu-rights {n₃ = suc n₃} perm = permu-right (permu-rights perm)
permu-all-left : Permute n n 0
permu-all-left {zero} = permu-done
permu-all-left {suc _} = permu-left permu-all-left
permu-all-right : Permute n 0 n
permu-all-right {zero} = permu-done
permu-all-right {suc _} = permu-right permu-all-right
permu-sym : Permute n n₁ n₂ → Permute n n₂ n₁
permu-sym permu-done = permu-done
permu-sym (permu-left perm) = permu-right (permu-sym perm)
permu-sym (permu-right perm) = permu-left (permu-sym perm)
permu-zero₁ : Permute 0 n₁ n₂ → n₁ ≡ 0
permu-zero₁ permu-done = refl
permu-zero₂ : Permute 0 n₁ n₂ → n₂ ≡ 0
permu-zero₂ permu-done = refl
permu-eq₁ : Permute n₁ n₂ 0 → n₁ ≡ n₂
permu-eq₁ permu-done = refl
permu-eq₁ (permu-left x) = cong suc (permu-eq₁ x)
permu-eq₂ : Permute n₁ 0 n₂ → n₁ ≡ n₂
permu-eq₂ permu-done = refl
permu-eq₂ (permu-right p) = cong suc (permu-eq₂ p)
permsu-suc₁ : Permute n₁ (suc n₂) n₃ → Permute n₁ n₂ (suc n₃)
permsu-suc₁ (permu-left p) = permu-right p
permsu-suc₁ (permu-right p) = permu-right (permsu-suc₁ p)
permsu-suc₂ : Permute n₁ n₂ (suc n₃) → Permute n₁ (suc n₂) n₃
permsu-suc₂ (permu-left p) = permu-left (permsu-suc₂ p)
permsu-suc₂ (permu-right p) = permu-left p
permsu-eq : Permute n₁ n₂ n₃ → Permute n₄ n₂ n₃ → n₁ ≡ n₄
permsu-eq permu-done permu-done = refl
permsu-eq (permu-left p₁) (permu-left p₂) = cong suc (permsu-eq p₁ p₂)
permsu-eq (permu-right p₁) (permu-left p₂) = cong suc (permsu-eq p₁ (permsu-suc₂ p₂))
permsu-eq (permu-left p₁) (permu-right p₂) = cong suc (permsu-eq p₁ (permsu-suc₁ p₂))
permsu-eq (permu-right p₁) (permu-right p₂) = cong suc (permsu-eq p₁ p₂)
permu-sum : Permute n n₁ n₂ → n₁ + n₂ ≡ n
permu-sum permu-done = refl
permu-sum (permu-left p) = cong suc (permu-sum p)
permu-sum (permu-right p) = trans (+-suc _ _) (cong suc (permu-sum p))
permu-split : Permute (n₁ + n₂) n₁ n₂
permu-split {n₁ = zero} = permu-all-right
permu-split {n₁ = suc _} = permu-left permu-split
permu-split-comm : Permute (n₁ + n₂) n₂ n₁
permu-split-comm {n₁ = zero} = permu-all-left
permu-split-comm {n₁ = suc _} = permu-right permu-split-comm
permu-assoc-left : ∀ n₁ → Permute (n₁ + (n₂ + n₃)) (n₁ + n₂) (n₃)
permu-assoc-left {n₂} {zero} _ rewrite +-identityʳ n₂ = permu-all-left
permu-assoc-left {n₂} {suc n₃} n₁ rewrite +-suc n₂ n₃ | +-suc n₁ (n₂ + n₃) = permu-right (permu-assoc-left n₁)
permu-cast : ∀ {n n' n₁ n₂} → n ≐ n' → Permute n n₁ n₂ → Permute n' n₁ n₂
permu-cast {zero} {zero} q p = p
permu-cast {suc n} {suc n'} q (permu-left p) = permu-left (permu-cast (suc-inj-irr q) p)
permu-cast {suc n} {suc n'} q (permu-right p) = permu-right (permu-cast (suc-inj-irr q) p)
permu-cast₁ : ∀ {n n₁ n₁' n₂} → n₁ ≐ n₁' → Permute n n₁ n₂ → Permute n n₁' n₂
permu-cast₁ q (permu-right p) = permu-right (permu-cast₁ q p)
permu-cast₁ {n₁' = zero} q permu-done = permu-done
permu-cast₁ {n₁' = suc n₁'} q (permu-left p) = permu-left (permu-cast₁ (suc-inj-irr q) p)
permu-cast₂ : ∀ {n n₁ n₂ n₂'} → n₂ ≐ n₂' → Permute n n₁ n₂ → Permute n n₁ n₂'
permu-cast₂ q (permu-left p) = permu-left (permu-cast₂ q p)
permu-cast₂ {n₂' = zero} q permu-done = permu-done
permu-cast₂ {n₂' = suc n₁'} q (permu-right p) = permu-right (permu-cast₂ (suc-inj-irr q) p)
data Permutation : → Set where
pm-done : Permutation 0
pm-pick : (pm : Permutation n) → (ix : Fin (suc n)) → Permutation (suc n)
fin-ge : Fin n → ∃ λ n' → n ≡ suc n' × Fin (suc n')
fin-ge Fin.zero = _ , refl , Fin.zero
fin-ge (Fin.suc ix) = _ , refl , Fin.suc ix
permu-choose : Permute (suc n) n₁ n₂ → Fin (suc n) → ∃ λ n' → (Fin n₁ × n₁ ≡ suc n' × Permute n n' n₂)
⊎ (Fin n₂ × n₂ ≡ suc n' × Permute n n₁ n')
permu-choose (permu-left p) Fin.zero = _ , inj₁ (Fin.zero , refl , p)
permu-choose (permu-left p) (Fin.suc ix) with fin-ge ix
... | _ , refl , ix'' with permu-choose p ix''
... | _ , inj₁ (ix' , refl , p') = _ , inj₁ (Fin.suc ix' , refl , permu-left p')
... | _ , inj₂ (ix' , refl , p') = _ , inj₂ (ix' , refl , permu-left p')
permu-choose (permu-right p) Fin.zero = _ , inj₂ (Fin.zero , refl , p)
permu-choose (permu-right p) (Fin.suc ix) with fin-ge ix
... | _ , refl , ix'' with permu-choose p ix''
... | _ , inj₁ (ix' , refl , p') = _ , inj₁ (ix' , refl , permu-right p')
... | _ , inj₂ (ix' , refl , p') = _ , inj₂ (Fin.suc ix' , refl , permu-right p')
pick-permute : Permute (suc n) n₁ n₂
→ Fin (suc n)
→ ∃ λ n'
------------------------------------------
→ (n₁ ≡ suc n' × Fin n₁ × Permute n n' n₂)
⊎ (n₂ ≡ suc n' × Fin n₂ × Permute n n₁ n')
pick-permute (permu-left p) Fin.zero = _ , inj₁ (refl , Fin.zero , p)
pick-permute (permu-left p) (Fin.suc ix) with fin-ge ix
... | _ , refl , ix' with pick-permute p ix'
... | _ , inj₁ (refl , ix'' , p') = _ , inj₁ (refl , Fin.suc ix'' , permu-left p')
... | _ , inj₂ (refl , ix'' , p') = _ , inj₂ (refl , ix'' , permu-left p')
pick-permute (permu-right p) Fin.zero = _ , inj₂ (refl , Fin.zero , p)
pick-permute (permu-right p) (Fin.suc ix) with fin-ge ix
... | _ , refl , ix' with pick-permute p ix'
... | _ , inj₁ (refl , ix'' , p') = _ , inj₁ (refl , ix'' , permu-right p')
... | _ , inj₂ (refl , ix'' , p') = _ , inj₂ (refl , Fin.suc ix'' , permu-right p')
split-permutation : Permutation n → Permute n n₁ n₂ → Permute n n₁ n₂ × Permutation n₁ × Permutation n₂
split-permutation (pm-pick pm ix) p with pick-permute p ix
split-permutation (pm-pick pm ix) p | _ , inj₁ (refl , ix' , p') with split-permutation pm p'
... | p'' , pm₁ , pm₂ = permu-left p'' , pm-pick pm₁ ix' , pm₂
split-permutation (pm-pick pm ix) p | _ , inj₂ (refl , ix' , p') with split-permutation pm p'
... | p'' , pm₁ , pm₂ = permu-right p'' , pm₁ , pm-pick pm₂ ix'
split-permutation pm-done permu-done = permu-done , pm-done , pm-done

@ -1,197 +0,0 @@
{-# OPTIONS --safe #-}
module Darius.Term where
open import Darius.Permutation
import Data.Fin as Fin
open Fin using (Fin)
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product hiding (zip)
open import Data.Sum
open import Data.Vec hiding (zip; unzip)
open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary.PropositionalEquality hiding (subst)
variable n n₁ n₂ n₃ n₄ n₅ :
data Type : Set where
0' ' 1' ⊥' 2' ' : Type
_⊕_ _&_ _⊗_ _⊸_ : Type → Type → Type
infix 18 _⊗_ _&_
infix 17 _⊕_
infix 16 _⊸_
-- | A term with `n` variables in the context.
--
-- Usually denoted `x, x₁, x₂, ...` for values, `τ, τ₁, τ₂, ...` for types.
data Term : → Set where
var : Term 1
absurd : (τ : Type) → (x : Term n) → Term n
σ₁ σ₂ : (τ : Type) → (x : Term n) → Term n
rec⊕ : (p : Permute n n₁ n₂) → (x : Term n₁) → (f : Term (suc n₂)) → (g : Term (suc n₂)) → Term n
forget : (x : Term n) → Term n
π₁ π₂ : (τ : Type) → (x : Term n) → Term n
pro& : (f : Term n) → (g : Term n) → Term n
unit : Term 0
rec1 : (p : Permute n n₁ n₂) → (x : Term n₁) → (f : Term n₂) → Term n
pair : (p : Permute n n₁ n₂) → (x : Term n₁) → (y : Term n₂) → Term n
rec⊗ : (p : Permute n n₁ n₂) → (x : Term n₁) → (f : Term (suc (suc n₂))) → Term n
λ' : (τ : Type) → (f : Term (suc n)) → Term n
app : (p : Permute n n₁ n₂) → (f : Term n₁) → (x : Term n₂) → Term n
zero' : Term 0
suc' : (x : Term n) → Term n
rec : (p : Permute n n₁ n₂) → (x : Term n₁) → (base : Term n₂) → (rec : Term 1) → Term n
-- Cast which (unlike subst) computes on constructors.
term-cast : ∀ {n₁ n₂} → n₁ ≐ n₂ → Term n₁ → Term n₂
-- | Replace the `ix`th variable in the term with the provided value.
subst : ∀ {size ctx} → (x : Term (suc ctx)) → (ix : Fin (suc ctx)) → (val : Term size) → Term (size + ctx)
subst1 : ∀ {size ctx} → (x : Term (suc ctx)) → (val : Term size) → Term (size + ctx)
subst1 x = subst x Fin.zero
-- | Apply a permutation to the context.
repermute : (x : Term n) → (pm : Permutation n) → Term n
term-cast {zero} {zero} p x = x
term-cast {suc n₁} {suc n₂} p (absurd τ x) = absurd τ (term-cast p x)
term-cast {suc n₁} {suc n₂} p (σ₁ τ x) = σ₁ τ (term-cast p x)
term-cast {suc n₁} {suc n₂} p (σ₂ τ x) = σ₂ τ (term-cast p x)
term-cast {suc n₁} {suc n₂} p (rec⊕ p₁ x x₁ x₂) = rec⊕ (permu-cast p p₁) x x₁ x₂
term-cast {suc n₁} {suc n₂} p (forget x) = forget (term-cast p x)
term-cast {suc n₁} {suc n₂} p (π₁ τ x) = π₁ τ (term-cast p x)
term-cast {suc n₁} {suc n₂} p (π₂ τ x) = π₂ τ (term-cast p x)
term-cast {suc n₁} {suc n₂} p (pro& x x₁) = pro& (term-cast p x) (term-cast p x₁)
term-cast {suc n₁} {suc n₂} p (rec1 p₁ x x₁) = rec1 (permu-cast p p₁) x x₁
term-cast {suc n₁} {suc n₂} p (pair p₁ x x₁) = pair (permu-cast p p₁) x x₁
term-cast {suc n₁} {suc n₂} p (rec⊗ p₁ x x₁) = rec⊗ (permu-cast p p₁) x x₁
term-cast {suc n₁} {suc n₂} p (λ' τ x) = λ' τ (term-cast (cong-irr suc p) x)
term-cast {suc n₁} {suc n₂} p (app p₁ x x₁) = app (permu-cast p p₁) x x₁
term-cast {suc n₁} {suc n₂} p (suc' x) = suc' (term-cast p x)
term-cast {suc n₁} {suc n₂} p (rec p₁ x x₁ x₂) = rec (permu-cast p p₁) x x₁ x₂
term-cast {suc .0} {suc zero} p var = var
repermute var pm = var
repermute (absurd τ x) pm = absurd τ (repermute x pm)
repermute (σ₁ τ x) pm = σ₁ τ (repermute x pm)
repermute (σ₂ τ x) pm = σ₂ τ (repermute x pm)
repermute (rec⊕ p x x₁ x₂) pm with split-permutation pm p
... | p' , pm₁ , pm₂ = rec⊕ p' (repermute x pm₁) (repermute x₁ (pm-pick pm₂ Fin.zero)) (repermute x₂ (pm-pick pm₂ Fin.zero))
repermute (forget x) pm = forget (repermute x pm)
repermute (π₁ τ x) pm = π₁ τ (repermute x pm)
repermute (π₂ τ x) pm = π₁ τ (repermute x pm)
repermute (pro& x x₁) pm = pro& (repermute x pm) (repermute x₁ pm)
repermute unit pm = unit
repermute (rec1 p x x₁) pm with split-permutation pm p
... | p' , pm₁ , pm₂ = rec1 p' (repermute x pm₁) (repermute x₁ pm₂)
repermute (pair p x x₁) pm with split-permutation pm p
... | p' , pm₁ , pm₂ = pair p' (repermute x pm₁) (repermute x₁ pm₂)
repermute (rec⊗ p x x₁) pm with split-permutation pm p
... | p' , pm₁ , pm₂ = rec⊗ p' (repermute x pm₁) (repermute x₁ (pm-pick (pm-pick pm₂ Fin.zero) Fin.zero))
repermute (λ' τ x) pm = λ' τ (repermute x (pm-pick pm Fin.zero))
repermute (app p x x₁) pm with split-permutation pm p
... | p' , pm₁ , pm₂ = app p' (repermute x pm₁) (repermute x₁ pm₂)
repermute zero' pm = zero'
repermute (suc' x) pm = suc' (repermute x pm)
repermute (rec p x x₁ x₂) pm with split-permutation pm p
... | p' , pm₁ , pm₂ = rec p' (repermute x pm₁) (repermute x₁ pm₂) x₂
&-injective : ∀ {τ₁ τ₂ τ₃ τ₄} → τ₁ & τ₂ ≡ τ₃ & τ₄ → τ₁ ≡ τ₃ × τ₂ ≡ τ₄
&-injective refl = refl , refl
⊗-injective : ∀ {τ₁ τ₂ τ₃ τ₄} → τ₁ ⊗ τ₂ ≡ τ₃ ⊗ τ₄ → τ₁ ≡ τ₃ × τ₂ ≡ τ₄
⊗-injective refl = refl , refl
⊕-injective : ∀ {τ₁ τ₂ τ₃ τ₄} → τ₁ ⊕ τ₂ ≡ τ₃ ⊕ τ₄ → τ₁ ≡ τ₃ × τ₂ ≡ τ₄
⊕-injective refl = refl , refl
⊸-injective : ∀ {τ₁ τ₂ τ₃ τ₄} → τ₁ ⊸ τ₂ ≡ τ₃ ⊸ τ₄ → τ₁ ≡ τ₃ × τ₂ ≡ τ₄
⊸-injective refl = refl , refl
subst'-ix : (ctx : ) → Set
subst'-ix ctx = Maybe (∃ λ ctx' → ctx ≡ suc ctx' × Fin (suc ctx'))
subst'-type : ∀ {ctx} → → subst'-ix ctx →
subst'-type {ctx} _ nothing = ctx
subst'-type size (just (ctx' , _)) = size + ctx'
subst'-type-help : ∀ {size} → (ix' : subst'-ix 0) → 0 ≐ subst'-type size ix'
subst'-type-help nothing = refl'
subst'-helper : ∀ {size ctx n₁ n₂}
→ Permute ctx n₁ n₂
→ (ix : subst'-ix ctx)
→ ∃ λ ((ixₗ , ixᵣ) : subst'-ix n₁ × subst'-ix n₂)
→ Permute (subst'-type size ix) (subst'-type size ixₗ) (subst'-type size ixᵣ)
subst'-helper p nothing = (nothing , nothing) , p
subst'-helper {size} {ctx} {n₁} {n₂} p (just (ctx' , refl , ix))
= (ixₗ , ixᵣ) , p'
where
pick : _
pick = pick-permute p ix
ixₗ : subst'-ix n₁
ixₗ with pick
... | fst , inj₁ (refl , ix' , _) = just (fst , refl , ix')
... | _ , inj₂ _ = nothing
ixᵣ : subst'-ix n₂
ixᵣ with pick
... | _ , inj₁ _ = nothing
... | fst , inj₂ (refl , ix' , _) = just (fst , refl , ix')
p' : Permute (size + ctx') (subst'-type size ixₗ) (subst'-type size ixᵣ)
p' with pick
... | _ , inj₁ (refl , _ , p') = permu-lefts p'
... | _ , inj₂ (refl , _ , p') = permu-rights p'
subst'-suc : ∀ {ctx} → subst'-ix ctx → subst'-ix (suc ctx)
subst'-suc (just (fst , refl , ix)) = just (suc fst , refl , Fin.suc ix)
subst'-suc nothing = nothing
subst'-suc-eq : ∀ {ctx} {size} ix → subst'-type size (subst'-suc {ctx} ix) ≡ suc (subst'-type size ix)
subst'-suc-eq (just (_ , refl , _)) = +-suc _ _
subst'-suc-eq nothing = refl
-- | Replace the `ix`th variable in the term with the provided value.
--subst : ∀ {size ctx} → (x : Term (suc ctx)) → (ix : Fin (suc ctx)) → (val : Term size) → Term (size + ctx)
subst' : ∀ {size ctx} → (ix : Maybe (∃ λ ctx' → ctx ≡ suc ctx' × Fin (suc ctx'))) → (val : Term size) → (x : Term ctx) → Term (subst'-type size ix)
subst' ix val (absurd τ x) = absurd τ (subst' ix val x)
subst' ix val (σ₁ τ x) = σ₁ τ (subst' ix val x)
subst' ix val (σ₂ τ x) = σ₁ τ (subst' ix val x)
subst' ix val (rec⊕ p x x₁ x₂) =
let (ixₗ , ixᵣ) , p' = subst'-helper p ix
in rec⊕ p' (subst' ixₗ val x) (term-cast (sq-eq (subst'-suc-eq ixᵣ)) (subst' (subst'-suc ixᵣ) val x₁)) (term-cast (sq-eq (subst'-suc-eq ixᵣ)) (subst' (subst'-suc ixᵣ) val x₂))
subst' ix val (forget x) = forget (subst' ix val x)
subst' ix val (π₁ τ x) = π₁ τ (subst' ix val x)
subst' ix val (π₂ τ x) = π₂ τ (subst' ix val x)
subst' ix val (pro& x x₁) = pro& (subst' ix val x) (subst' ix val x₁)
subst' ix val unit = term-cast (subst'-type-help ix) unit
subst' ix val (rec1 p x x₁) =
let (ixₗ , ixᵣ) , p' = subst'-helper p ix
in rec1 p' (subst' ixₗ val x) (subst' ixᵣ val x₁)
subst' ix val (pair p x x₁) =
let (ixₗ , ixᵣ) , p' = subst'-helper p ix
in pair p' (subst' ixₗ val x) (subst' ixᵣ val x₁)
subst' ix val (rec⊗ p x x₁) =
let (ixₗ , ixᵣ) , p' = subst'-helper p ix
in rec⊗ p' (subst' ixₗ val x) (term-cast (sq-eq (trans (subst'-suc-eq (subst'-suc ixᵣ)) (cong suc (subst'-suc-eq ixᵣ)))) (subst' (subst'-suc (subst'-suc ixᵣ)) val x₁))
subst' ix val (λ' τ x) = λ' τ (term-cast (sq-eq (subst'-suc-eq ix)) (subst' (subst'-suc ix) val x))
subst' ix val (app p x x₁) =
let (ixₗ , ixᵣ) , p' = subst'-helper p ix
in app p' (subst' ixₗ val x) (subst' ixᵣ val x₁)
subst' ix val zero' = term-cast (subst'-type-help ix) zero'
subst' ix val (suc' x) = suc' (subst' ix val x)
subst' ix val (rec p x x₁ x₂) =
let (ixₗ , ixᵣ) , p' = subst'-helper p ix
in rec p' (subst' ixₗ val x) (subst' ixᵣ val x₁) x₂
subst' (just (.0 , refl , snd)) val var = term-cast (sq-eq (sym (+-identityʳ _))) val
subst' nothing val var = var
subst x ix val = subst' (just (_ , refl , ix)) val x

@ -0,0 +1,296 @@
#include <assert.h>
#include <stdlib.h>
#include <stdio.h>
enum instruction_type {
// construct a new object using a class_table (constructor for additive conjunction)
I_NEW,
// invoke a method on an object (eliminator for additive conjunction)
I_INVOKE,
// construct a struct (constructor for multiplicative conjunction)
I_CONSTRUCT,
// destruct a struct (eliminator for multiplicative conjunction)
I_DESTRUCT,
// tag a value (constructor for additive disjunction)
I_TAG,
// switch against a tagged value (eliminator for additive disjunction)
I_SWITCH,
// create a code block with access to delimited continuations specified by a control_table
// (constructor for multiplicative disjunction)
I_CONTROL,
// handle a controller (eliminator for multiplicative disjunction)
I_HANDLE,
// call a static method (cut)
I_CALL,
// swap an element with the top of the stack (structural exchange)
I_SWAP,
};
struct instruction {
enum instruction_type type;
union {
// used by: new, switch
const struct class_table* class_table;
// used by: control
const struct control_table* control_table;
// used by: handle
const struct handler_table* handler_table;
// used by: call
const struct method* method;
// used by: invoke, tag, swap
size_t index;
// used by: construct
size_t count;
// nothing used by: destruct, return
} args;
};
union data {
struct object* object;
struct struct_* struct_;
struct enum_* enum_;
struct controller* controller;
struct method* method;
};
struct frame {
size_t top;
size_t length;
union data data[];
};
struct object {
const struct class_table* class_table;
union data fields[];
};
struct struct_ {
size_t length;
union data fields[]</