Created
April 12, 2021 10:27
-
-
Save umazalakain/4cab6c4dc4f553e3b152b7f3c1989abf to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open import Function using (_∘_) | |
open import Data.Integer.Base as ℤ using (ℤ) | |
open import Data.Fin.Base as Nat using (Fin; zero; suc) | |
open import Data.Nat.Base as ℕ using (ℕ; zero; suc) | |
open import Data.Vec.Base as Vec using (Vec; []; _∷_) | |
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just) | |
private variable n m l : ℕ | |
data UnOp : Set where | |
neg : UnOp | |
data BinOp : Set where | |
add : BinOp | |
data Expr : ℕ → Set where | |
pinf : Expr n | |
ninf : Expr n | |
lit : ℤ → Expr n | |
var : Fin n → Expr n | |
abs : Expr (suc n) → Expr n | |
app : Expr n → Expr n → Expr n | |
uop : UnOp → Expr n → Expr n | |
bop : BinOp → Expr n → Expr n → Expr n | |
record Range (n : ℕ) : Set where | |
constructor [_,_] | |
field | |
min max : Expr n | |
data Type (n : ℕ) : Set where | |
int : Range n → Type n | |
depfun : Type n → Type (suc n) → Type n | |
data univ : Set where | |
expr type : univ | |
U[_∶_] : univ → ℕ → Set | |
U[_∶_] expr = Expr | |
U[_∶_] type = Type | |
private variable u : univ | |
|> : (Fin n → Fin m) → (Fin n → U[ u ∶ m ]) | |
|> {u = expr} f i = var (f i) | |
|> {u = type} f i = int [ var (f i) , var (f i) ] | |
lift : U[ u ∶ m ] → U[ u ∶ suc m ] | |
lift {expr} pinf = pinf | |
lift {expr} ninf = ninf | |
lift {expr} (lit x) = lit x | |
lift {expr} (var x) = var (suc x) | |
lift {expr} (abs t) = abs (lift t) | |
lift {expr} (app t t₁) = app (lift t) (lift t₁) | |
lift {expr} (uop x t) = uop x (lift t) | |
lift {expr} (bop x t t₁) = bop x (lift t) (lift t₁) | |
lift {type} (int [ min , max ]) = int [ (lift min) , (lift max) ] | |
lift {type} (depfun t t₁) = depfun (lift t) (lift t₁) | |
_<|_ : (Fin n → Expr m) → (Expr n → Expr m) | |
_<|_ f pinf = pinf | |
_<|_ f ninf = ninf | |
_<|_ f (lit x) = lit x | |
_<|_ f (var x) = f x | |
_<|_ f (abs t) = abs ((λ { zero → |> (λ x → x) zero ; (suc x) → lift (f x)}) <| t) | |
_<|_ f (app t₁ t₂) = app (f <| t₁) (f <| t₂) | |
_<|_ f (uop x t) = uop x (f <| t) | |
_<|_ f (bop x t₁ t₂) = bop x (f <| t₁) (f <| t₂) | |
_<|ₜ_ : (∀ {u} → Fin n → U[ u ∶ m ]) → (U[ u ∶ n ] → U[ u ∶ m ]) | |
_<|ₜ_ {u = expr } f e = f <| e | |
_<|ₜ_ {u = type } f (int [ min , max ]) = int [ f <| min , f <| max ] | |
_<|ₜ_ {u = type } f (depfun s t) = depfun (f <|ₜ s) ((λ { zero → |> (λ x → x) zero ; (suc x) → lift (f x)}) <|ₜ t) | |
_<>_ : (∀ {u} → Fin n → U[ u ∶ m ]) → (∀ {u} → Fin l → U[ u ∶ n ]) → (∀ {u} → Fin l → U[ u ∶ m ]) | |
(f <> g) x = f <|ₜ g x | |
thin : Fin (suc n) → Fin n → Fin (suc n) | |
thin zero y = suc y | |
thin (suc x) zero = zero | |
thin (suc x) (suc y) = suc (thin x y) | |
thick : Fin (suc n) → Fin (suc n) → Maybe (Fin n) | |
thick zero zero = nothing | |
thick zero (suc y) = just y | |
thick {suc _} (suc x) zero = just zero | |
thick {suc _} (suc x) (suc y) = thick x y Maybe.>>= just ∘ suc | |
_for_ : Expr n → Fin (suc n) → Fin (suc n) → Expr n | |
(e for r) x = Maybe.maybe var e (thick r x) | |
_∶_for_ : Expr n → Type n → Fin (suc n) → (∀ {u} → Fin (suc n) → U[ u ∶ n ]) | |
(e ∶ t for r) {expr} x = (e for r) x | |
(e ∶ t for r) {type} x = Maybe.maybe (λ e → int [ var e , var e ]) t (thick r x) | |
check : Fin (suc n) → U[ u ∶ (suc n) ] → Maybe (U[ u ∶ n ]) | |
check {u = expr} r pinf = just pinf | |
check {u = expr} r ninf = just ninf | |
check {u = expr} r (lit x) = just (lit x) | |
check {u = expr} r (var x) = thick r x Maybe.>>= just ∘ var | |
check {u = expr} r (abs t) = check (suc r) t Maybe.>>= just ∘ abs | |
check {u = expr} r (app t t₁) = check r t Maybe.>>= λ t' → check r t₁ Maybe.>>= λ t₁' → just (app t' t₁') | |
check {u = expr} r (uop x t) = check r t Maybe.>>= just ∘ uop x | |
check {u = expr} r (bop x t t₁) = check r t Maybe.>>= λ t' → check r t₁ Maybe.>>= λ t₁' → just (bop x t' t₁') | |
check {u = type} r (int [ min , max ]) = check r min Maybe.>>= λ min' → check r max Maybe.>>= λ max' → just (int [ min' , max' ]) | |
check {u = type} r (depfun t t₁) = check r t Maybe.>>= λ t' → check (suc r) t₁ Maybe.>>= λ t₁' → just (depfun t' t₁') | |
data Ctx : ℕ → Set where | |
∅ : Ctx zero | |
_-,_ : Ctx n → Type n → Ctx (suc n) | |
private | |
variable | |
i : Fin n | |
e e₁ e₂ lb lb₁ lb₂ ub ub₁ ub₂ : Expr n | |
Γ : Ctx n | |
t s : Type n | |
data _∋_∶_ : Ctx n → Fin n → Type n → Set where | |
zero : (Γ -, t) ∋ zero ∶ (|> suc <|ₜ t) | |
suc : Γ ∋ i ∶ t → (Γ -, s) ∋ suc i ∶ (|> suc <|ₜ t) | |
data _⊢_∶_ : Ctx n → Expr n → Type n → Set where | |
pinf : Γ ⊢ pinf ∶ int [ pinf , pinf ] | |
ninf : Γ ⊢ ninf ∶ int [ ninf , ninf ] | |
lit : (l : ℤ) → Γ ⊢ lit l ∶ int [ lit l , lit l ] | |
var : Γ ∋ i ∶ t → Γ ⊢ var i ∶ t | |
abs : (Γ -, s) ⊢ e ∶ t → Γ ⊢ abs e ∶ depfun s t | |
app : Γ ⊢ e₁ ∶ depfun s t → Γ ⊢ e₂ ∶ s → Γ ⊢ app e₁ e₂ ∶ ((e₂ ∶ s for zero) <|ₜ t) | |
neg : Γ ⊢ e ∶ int [ lb , ub ] → Γ ⊢ uop neg e ∶ int [ uop neg ub , uop neg lb ] | |
add : Γ ⊢ e₁ ∶ int [ lb₁ , ub₁ ] → Γ ⊢ e₂ ∶ int [ lb₂ , ub₂ ] → Γ ⊢ bop add e₁ e₂ ∶ int [ bop add lb₁ lb₂ , bop add ub₁ ub₂ ] | |
data _~>_ : Expr m → Expr n → Set where | |
beta : app (abs e) e₁ ~> ((e₁ for zero) <| e) | |
subject-reduction : Γ ⊢ e ∶ t → e ~> e₁ → Γ ⊢ e₁ ∶ t | |
subject-reduction {Γ = Γ} (app (abs e) e₁) beta = {!!} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment