{-# OPTIONS --copatterns #-} {-# OPTIONS -v tc.cover.splittree:10 #-} module DeduktiTalk-2014-May-16 where -- C-c C-l load data ℕ : Set where -- \ b n zero : ℕ suc : ℕ → ℕ {-# BUILTIN NATURAL ℕ #-} module Explicit where data Fin : (n : ℕ) → Set where zero : (n : ℕ) → Fin (suc n) suc : (n : ℕ) → Fin n → Fin (suc n) id : (A : Set) → A → A id A x = x syntax id A x = x ∈ A i : Fin 2 i = (suc _ (zero _)) -- ∈ Fin 2 -- C-c C-= constraints -- C-c C-s solve {- _n = 1 --------------------- _n : ℕ zero _m : Fin _n Fin (suc _n) <= Fin 2 -------------------------------------------------- suc : (n : ℕ) → Fin n → Fin (suc n) suc _n (zero _m) : Fin 2 -} data Vec (A : Set) : (n : ℕ) → Set where [] : Vec A zero cons : ∀ n → A → Vec A n → Vec A (suc n) lookup : (A : Set) (n : ℕ) (i : Fin n) (xs : Vec A n) → A lookup A .(suc n) (zero n) (cons .n x xs) = x lookup A .(suc n) (suc n i) (cons .n x xs) = lookup A n i xs {- lookup A n i xs | case i of zero n -> case xs of cons .n x xs -> x suc n i -> case xs of cons .n x xs -> lookup A n i xs -} -- C-c C-c case split data Fin : (n : ℕ) → Set where zero : {n : ℕ} → Fin (suc n) suc : {n : ℕ} → Fin n → Fin (suc n) data Vec (A : Set) : (n : ℕ) → Set where [] : Vec A zero _∷_ : ∀{n} → A → Vec A n → Vec A (suc n) lookup : ∀ {A n} → Fin n → Vec A n → A lookup zero (x ∷ xs) = x lookup (suc i) (x ∷ xs) = lookup i xs -- C-c C-SPACE give expression -- C-c C-r refine data Tm (n : ℕ) : Set where var : (x : Fin n) → Tm n abs : (t : Tm (suc n)) → Tm n app : (r s : Tm n) → Tm n record Val : Set where constructor clos field {n} : ℕ body : Tm (suc n) env : Vec Val n Env = Vec Val -- v = clos (var zero) [] -- \ [ [ = ⟦ -- C-c C-, Show goal and hypotheses -- C-c C-. Show goal and hypotheses and type of term module NonTerm where mutual {-# NO_TERMINATION_CHECK #-} ⟦_⟧_ : ∀{n} → Tm n → Env n → Val ⟦ var x ⟧ ρ = lookup x ρ ⟦ abs t ⟧ ρ = clos t ρ ⟦ app r s ⟧ ρ = apply (⟦ r ⟧ ρ) (⟦ s ⟧ ρ) apply : Val → Val → Val apply (clos t ρ) v = ⟦ t ⟧ (v ∷ ρ) {- Termination checker ⟦ app r s ⟧ ρ = ⟦ r ⟧ ρ ⟦ app r s ⟧ ρ = ⟦ s ⟧ ρ ⟦ app r s ⟧ ρ = apply _ _ apply (clos t ρ) v = ⟦ t ⟧ _ -} -- Delay monad Delay' A = ν X. A + X data DelayF (A B : Set) : Set where return : A → DelayF A B later : B → DelayF A B module NonSized where record Delay' (A : Set) : Set where coinductive constructor delay field force : DelayF A (Delay' A) open Delay' {- module Delay' {A : Set} (r : Delay' A) where force : DelayF A (Delay' A) Delay'.force : {A : Set} (r : Delay' A) → DelayF A (Delay' A) -} forever : ∀{A} → Delay' A force forever = later forever Delay = λ A → DelayF A (Delay' A) mutual _>>=_ : ∀{A B} → Delay A → (A → Delay B) → Delay B return a >>= k = k a later a' >>= k = later (a' >>=' k) _>>='_ : ∀{A B} → Delay' A → (A → Delay B) → Delay' B force (a' >>=' k) = force a' >>= k -- bla : ℕ -- bla = {!f!} -- where open Delay' {ℕ} forever renaming (force to f) mutual {-# NO_TERMINATION_CHECK #-} ⟦_⟧_ : ∀{n} → Tm n → Env n → Delay Val ⟦ var x ⟧ ρ = return (lookup x ρ) ⟦ abs t ⟧ ρ = return (clos t ρ) ⟦ app r s ⟧ ρ = apply (⟦ r ⟧ ρ) (⟦ s ⟧ ρ) apply : Delay Val → Delay Val → Delay Val apply u? v? = u? >>= λ u → v? >>= λ v → later (apply' u v) apply' : Val → Val → Delay' Val force (apply' (clos t ρ) v) = ⟦ t ⟧ (v ∷ ρ) postulate Size : Set Size< : Size -> Set ∞ : Size ↑ : Size → Size {-# BUILTIN SIZE Size #-} {-# BUILTIN SIZELT Size< #-} {-# BUILTIN SIZEINF ∞ #-} {-# BUILTIN SIZESUC ↑ #-} record Delay' (i : Size) (A : Set) : Set where coinductive constructor delay field force : ∀(j : Size< i) → DelayF A (Delay' j A) open Delay' forever : ∀{A} i → Delay' i A force (forever i) j = later (forever j) forever' = forever {ℕ} ∞ Delay = λ i A → DelayF A (Delay' i A) mutual bind : ∀{A B} i → Delay i A → (A → Delay i B) → Delay i B bind i (return a) k = k a bind i (later a') k = later (bind' i a' k) bind' : ∀{A B} i → Delay' i A → (A → Delay i B) → Delay' i B force (bind' i a' k) j = bind j (force a' j) k -- bla : ℕ -- bla = {!f!} -- where open Delay' {ℕ} forever renaming (force to f) mutual eval : ∀ i {n} → Tm n → Env n → Delay i Val eval i (var x) ρ = return (lookup x ρ) eval i (abs t) ρ = return (clos t ρ) eval i (app r s) ρ = apply i (eval i r ρ) (eval i s ρ) apply : ∀ i → Delay i Val → Delay i Val → Delay i Val apply i u? v? = bind i u? λ u → bind i v? λ v → later (apply' i u v) apply' : ∀ i → Val → Val → Delay' i Val force (apply' i (clos t ρ) v) j = eval j t (v ∷ ρ) {- eval i (app r s) ρ = eval i r ρ eval i (app r s) ρ = eval i s ρ eval i (app r s) ρ = apply i _ _ apply i u? v? = apply' i _ _ force (apply' i _ _) (j : Size< i) = eval j t _ Lexicographic order (i, t) -} -- Y f = (λ x. f (x x)) (λ x. f (x x)) sapp : Tm 0 sapp = abs (app (var zero) (var zero)) Omega : Tm 0 Omega = app sapp sapp test = eval ∞ Omega [] cl = clos (app (var zero) (var zero)) []