;;;; Structural Rules
-(define-rule formation-1 ()
- ((Γ ⊢ (type A))
- (Γ (: x A) ⊢ (type (B x)))))
-
-(define-rule formation-2 ()
- ((Γ ⊢ (type A))
- (Γ ⊢ (≐ A B))))
-
-(define-rule formation-3 ()
- ((Γ ⊢ (type B))
- (Γ ⊢ (≐ A B))))
-
-(define-rule formation-4 ()
- ((Γ ⊢ (type A))
- (Γ ⊢ (: a A))))
-
-(define-rule formation-5 ()
- ((Γ ⊢ (: a A))
- (Γ ⊢ (≐ a b A))))
-
-(define-rule formation-6 ()
- ((Γ ⊢ (: b A))
- (Γ ⊢ (≐ a b A))))
-
-(define-rule type-reflexive ()
- ((Γ ⊢ (≐ A A))
- (Γ ⊢ (type A))))
-
-(define-rule type-symmetric ()
- ((Γ ⊢ (≐ B A))
- (Γ ⊢ (≐ A B))))
-
-(define-rule type-transitive ()
- ((Γ ⊢ (≐ A C))
- (Γ ⊢ (≐ A B))
- (Γ ⊢ (≐ B C))))
-
-(define-rule :-reflexive ()
- ((Γ ⊢ (≐ a a A))
- (Γ ⊢ (: a A))))
-
-(define-rule :-symmetric ()
- ((Γ ⊢ (≐ b a A))
- (Γ ⊢ (≐ a b A))))
-
-(define-rule :-transitive ()
- ((Γ ⊢ (≐ a c A))
- (Γ ⊢ (≐ a b A))
- (Γ ⊢ (≐ b c A))))
-
-(define-rule variable-conversion ()
- ((Γ (: x A') Δ ⊢ J)
- (Γ ⊢ (≐ A A'))
- (Γ (: x A) Δ ⊢ J)))
-
-(define-rule substitution ()
- ((Γ (/ Δ a x) ⊢ (/ J a x))
- (Γ ⊢ (: a A))
- (Γ (: x A) Δ ⊢ J)))
-
-(define-rule substitution-type-congruence ()
- ((Γ (/ Δ a x) ⊢ (≐ (/ B a x) (/ B a' x)))
- (Γ ⊢ (≐ a a' A))
- (Γ (: x A) Δ ⊢ (type B))))
-
-(define-rule substitution-:-congruence ()
- ((Γ (/ Δ a x) ⊢ (≐ (/ b a x) (/ b a' x) (/ B a x)))
- (Γ ⊢ (≐ a a' A))
- (Γ (: x A) Δ ⊢ (: b B))))
-
-(define-rule weakening ()
- ((Γ (: x A) Δ ⊢ J)
- (Γ ⊢ (type A))
- (Γ Δ ⊢ J)))
-
-(define-rule generic-element ()
- ((Γ (: x A) ⊢ (: x A))
- (Γ ⊢ (type A))))
-
-;;;; Ordinary Function Type
-
-(define-rule → ()
- ((Γ ⊢ (type (→ A B)))
- (Γ ⊢ (type A))
- (Γ ⊢ (type B))))
-
-(define-rule →-eq ()
- ((Γ ⊢ (≐ (→ A B)
- (→ A' B')))
- (Γ ⊢ (≐ A A'))
- (Γ ⊢ (≐ B B'))))
-
-(define-rule λ ()
- ((Γ ⊢ (: (λ x (b x))
- (→ A B)))
- (Γ ⊢ (type B))
- (Γ (: x A) ⊢ (: (b x) B))))
-
-(define-rule λ-eq ()
- ((Γ ⊢ (≐ (λ x (b x))
- (λ x (b' x))
- (→ A B)))
- (Γ (: x A) ⊢ (≐ (b x) (b' x) B))))
-
-(define-rule ev ()
- ((Γ (: x A) ⊢ (: (f x) B))
- (Γ ⊢ (: f (→ A B)))))
-
-(define-rule ev-eq ()
- ((Γ (: x A) ⊢ (≐ (f x) (f' x) B))
- (Γ ⊢ (≐ f f' (→ A B)))))
-
-(define-rule β ()
- ((Γ (: x A) ⊢ (≐ ((λ y (b y)) x)
- (b x)
- B))
- (Γ ⊢ (type B))
- (Γ (: x A) ⊢ (: (b x) B))))
-
-(define-rule η ()
- ((Γ ⊢ (≐ (λ x (f x))
- f
- (→ A B)))
- (Γ ⊢ (: f (→ A B)))))
-
-;;;; Boolean Type
-
-(define-rule bool-formation ()
- ((⊢ (type Bool))))
-
-(define-rule bool-introduction-1 ()
- ((⊢ (: true Bool))))
-
-(define-rule bool-introduction-2 ()
- ((⊢ (: false Bool))))
-
-(define-rule bool-elimination ()
- ((⊢ (: if (→ Bool (→ A (→ A A)))))
- (⊢ (type A))))
-
-(define-rule bool-computation-1 ()
- ((⊢ (≐ (((if true) x) y)
- x
- Bool))))
-
-(define-rule bool-computation-2 ()
- ((⊢ (≐ (((if false) x) y)
- y
- Bool))))
-
-;;;; Ordinary Pair Type
-
-(define-rule pair-formation ()
- ((⊢ (type (Pair A B)))
- (⊢ (type A))
- (⊢ (type B))))
-
-(define-rule pair-introduction ()
- ((⊢ (: (pair a b) (Pair A B)))
- (⊢ (: a A))
- (⊢ (: b B))))
-
-(define-rule pair-elimination-1 ()
- ((⊢ (: first (→ (Pair A B)
- A)))
- (⊢ (type A))
- (⊢ (type B))))
-
-(define-rule pair-elimination-2 ()
- ((⊢ (: second (→ (Pair A B)
- B)))
- (⊢ (type A))
- (⊢ (type B))))
-
-(define-rule pair-computation-1 ()
- ((⊢ (≐ (first (pair a b))
- a A))
- (⊢ (: a A))
- (⊢ (: b B))))
-
-(define-rule pair-computation-2 ()
- ((⊢ (≐ (second (pair a b))
- b B))
- (⊢ (: a A))
- (⊢ (: b B))))
-
-;;;; Derivations
+(define-rule formation-1
+ (Γ ⊢ (type A))
+ (Γ (: x A) ⊢ (type (B x))))
+
+(define-rule formation-2
+ (Γ ⊢ (type A))
+ (Γ ⊢ (≐ A B)))
+
+(define-rule formation-3
+ (Γ ⊢ (type B))
+ (Γ ⊢ (≐ A B)))
+
+(define-rule formation-4
+ (Γ ⊢ (type A))
+ (Γ ⊢ (: a A)))
+
+(define-rule formation-5
+ (Γ ⊢ (: a A))
+ (Γ ⊢ (≐ a b A)))
+
+(define-rule formation-6
+ (Γ ⊢ (: b A))
+ (Γ ⊢ (≐ a b A)))
+
+(define-rule type-reflexive
+ (Γ ⊢ (≐ A A))
+ (Γ ⊢ (type A)))
+
+(define-rule type-symmetric
+ (Γ ⊢ (≐ B A))
+ (Γ ⊢ (≐ A B)))
+
+(define-rule type-transitive
+ (Γ ⊢ (≐ A C))
+ (Γ ⊢ (≐ A B))
+ (Γ ⊢ (≐ B C)))
+
+(define-rule element-reflexive
+ (Γ ⊢ (≐ a a A))
+ (Γ ⊢ (: a A)))
+
+(define-rule element-symmetric
+ (Γ ⊢ (≐ b a A))
+ (Γ ⊢ (≐ a b A)))
+
+(define-rule element-transitive
+ (Γ ⊢ (≐ a c A))
+ (Γ ⊢ (≐ a b A))
+ (Γ ⊢ (≐ b c A)))
+
+(define-rule variable-conversion
+ (Γ (: x A') Δ ⊢ J)
+ (Γ ⊢ (≐ A A'))
+ (Γ (: x A) Δ ⊢ J))
+
+(define-rule substitution
+ (Γ (/ Δ a x) ⊢ (/ J a x))
+ (Γ ⊢ (: a A))
+ (Γ (: x A) Δ ⊢ J))
+
+(define-rule substitution-type-congruence
+ (Γ (/ Δ a x) ⊢ (≐ (/ B a x) (/ B a' x)))
+ (Γ ⊢ (≐ a a' A))
+ (Γ (: x A) Δ ⊢ (type B)))
+
+(define-rule substitution-element-congruence
+ (Γ (/ Δ a x) ⊢ (≐ (/ b a x) (/ b a' x) (/ B a x)))
+ (Γ ⊢ (≐ a a' A))
+ (Γ (: x A) Δ ⊢ (: b B)))
+
+(define-rule weakening
+ (Γ (: x A) Δ ⊢ J)
+ (Γ ⊢ (type A))
+ (Γ Δ ⊢ J))
+
+(define-rule generic-element
+ (Γ (: x A) ⊢ (: x A))
+ (Γ ⊢ (type A)))
+
+;;;; Structural Derivations
(define-derivation change-of-variables ((Γ (: x' A) Δ ⊢ J)
(Γ ⊢ (type A))
(Γ (: x A) Δ ⊢ J))
- (substitution #:index 2 a x' x x A A)
- (generic-element #:index 1)
+ (substitution #:start 1 a x' x x A A)
+ (generic-element)
(exact)
- (weakening #:index 1)
+ (weakening #:end 1)
(exact)
(exact))
(Γ ⊢ (type B))
(Γ ⊢ (type A))
(Γ (: x A) (: y B) Δ ⊢ J))
- (substitution #:index 3 a y x y' A B)
- (weakening #:index 2)
- (weakening #:index 1)
+ (substitution #:start 2 a y x y' A B)
+ (weakening #:start 1)
+ (weakening)
(exact)
(exact)
- (generic-element #:index 1)
+ (generic-element)
(exact)
- (weakening #:index 1)
+ (weakening #:end 1)
(exact)
- (substitution #:index 3 a y' x y A B)
- (weakening #:index 1)
+ (substitution #:start 2 a y' x y A B)
+ (weakening #:end 1)
(exact)
- (generic-element #:index 1)
+ (generic-element)
(exact)
- (weakening #:index 2)
- (weakening #:index 1)
+ (weakening #:start 1 #:end 2)
+ (weakening)
(exact)
(exact)
(exact))
(Γ ⊢ (≐ A A')))
(substitution a a x a' A A)
(exact)
- (variable-conversion #:index 1 A A')
+ (variable-conversion A A')
(type-symmetric)
(exact)
- (generic-element #:index 1)
+ (generic-element)
(formation-3 A A)
(exact))
(define-derivation congruence ((Γ ⊢ (≐ a b A'))
(Γ ⊢ (≐ a b A))
(Γ ⊢ (≐ A A')))
- (substitution-:-congruence #:index 1 a a a' b x x A A)
+ (substitution-element-congruence a a a' b x x A A)
+ (exact)
+ (variable-conversion A A')
+ (type-symmetric)
+ (exact)
+ (generic-element)
+ (formation-3 A A)
+ (exact))
+
+;;;; Dependent Function Type
+
+(define-rule Π
+ (Γ ⊢ (type (Π (: x A) (B x))))
+ (Γ (: x A) ⊢ (type (B x))))
+
+(define-rule Π-eq
+ (Γ ⊢ (≐ (Π (: x A) (B x))
+ (Π (: x A') (B' x))))
+ (Γ ⊢ (≐ A A'))
+ (Γ (: x A) ⊢ (≐ (B x) (B' x))))
+
+(define-rule λ
+ (Γ ⊢ (: (λ x (b x))
+ (Π (: x A) (B x))))
+ (Γ (: x A) ⊢ (: (b x) (B x))))
+
+(define-rule λ-eq
+ (Γ ⊢ (≐ (λ x (b x))
+ (λ x (b' x))
+ (Π (: x A) (B x))))
+ (Γ (: x A) ⊢ (≐ (b x)
+ (b' x)
+ (B x))))
+
+(define-rule evaluation
+ (Γ (: x A) ⊢ (: (f x) (B x)))
+ (Γ ⊢ (: f (Π (: x A) (B x)))))
+
+(define-rule evaluation-eq
+ (Γ (: x A) ⊢ (≐ (f x) (f' x) (B x)))
+ (Γ ⊢ (≐ f f' (Π (: x A) (B x)))))
+
+(define-rule β
+ (Γ (: x A) ⊢ (≐ ((λ y (b y)) x)
+ (b x)
+ (B x)))
+ (Γ (: x A) ⊢ (: (b x) (B x))))
+
+(define-rule η
+ (Γ ⊢ (≐ (λ x (f x))
+ f
+ (Π (: x A) (B x))))
+ (Γ ⊢ (: f (Π (: x A) (B x)))))
+
+;;;; Ordinary Function Type
+
+(define-derivation → ((Γ ⊢ (:= (→ A B) (type (Π (: x A) B))))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (type B)))
+ (Π)
+ (weakening)
+ (exact)
+ (exact))
+
+(define-derivation →-eq ((Γ ⊢ (≐ (→ A B) (→ A' B')))
+ (Γ ⊢ (≐ A A'))
+ (Γ ⊢ (≐ B B')))
+ (type-transitive B (Π (: x A) B))
+ (definition)
+ (formation-2 B A')
+ (exact)
+ (formation-2 B B')
+ (exact)
+ (type-transitive B (Π (: x A') B'))
+ (Π-eq)
+ (exact)
+ (weakening)
+ (formation-2 B A')
+ (exact)
+ (exact)
+ (type-symmetric)
+ (definition)
+ (formation-3 A A)
+ (exact)
+ (formation-3 A B)
+ (exact))
+
+(define-derivation →-λ ((Γ ⊢ (: (λ x (b x)) (→ A B)))
+ (Γ (: x A) ⊢ (: (b x) B))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (type B)))
+ (element-conversion A (Π (: x A) B))
+ (λ)
+ (exact)
+ (type-symmetric)
+ (definition)
+ (exact)
+ (exact))
+
+(define-derivation →-λ-eq ((Γ ⊢ (≐ (λ x (b x))
+ (λ x (b' x))
+ (→ A B)))
+ (Γ (: x A) ⊢ (≐ (b x) (b' x) B))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (type B)))
+ (congruence A (Π (: x A) B))
+ (λ-eq)
+ (exact)
+ (type-symmetric)
+ (definition)
+ (exact)
+ (exact))
+
+(define-derivation →-evaluation ((Γ (: x A) ⊢ (: (f x) B))
+ (Γ ⊢ (: f (→ A B)))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (type B)))
+ (evaluation f f)
+ (element-conversion A (→ A B))
+ (exact)
+ (definition)
+ (exact)
+ (exact))
+
+(define-derivation →-evaluation-eq ((Γ (: x A) ⊢ (≐ (f x) (f' x) B))
+ (Γ ⊢ (≐ f f' (→ A B)))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (type B)))
+ (evaluation-eq f f f' f')
+ (congruence A (→ A B))
+ (exact)
+ (definition)
+ (exact)
+ (exact))
+
+(define-derivation →-β ((Γ (: x A) ⊢ (≐ ((λ x (b x)) x)
+ (b x)
+ B))
+ (Γ (: x A) ⊢ (: (b x) B)))
+ (β)
+ (exact))
+
+(define-derivation →-η ((Γ ⊢ (≐ (λ x (f x)) f (→ A B)))
+ (Γ ⊢ (: f (→ A B)))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (type B)))
+ (congruence A (Π (: x A) B))
+ (η)
+ (element-conversion A (→ A B))
+ (exact)
+ (definition)
+ (exact)
(exact)
- (variable-conversion #:index 1 A A')
(type-symmetric)
+ (definition)
(exact)
- (generic-element #:index 1)
- (formation-3)
(exact))
+;;;; Identity Type
+
+(define-rule =-formation
+ (Γ (: x A) ⊢ (type (= a x)))
+ (Γ ⊢ (: a A)))
+
+(define-rule =-introduction
+ (Γ ⊢ (: refl (= a a)))
+ (Γ ⊢ (: a A)))
+
+(define-rule =-elimination
+ (Γ ⊢ (: ind-eq
+ (→ (P a refl)
+ (Π (: x A)
+ (Π (: p (= a x))
+ (P x p))))))
+ (Γ ⊢ (: a A))
+ (Γ (: x A) (: p (= a x)) ⊢ (type (P x p))))
+
+(define-rule =-computation
+ (Γ (: u (P a refl)) ⊢ (≐ (((ind-eq u) a) refl)
+ u
+ (P a refl)))
+ (Γ ⊢ (: a A))
+ (Γ (: x A) (: p (= a x)) ⊢ (type (P x p))))
+
+;;;; Dependent Pair Type
+
+(define-rule Σ-formation
+ (Γ ⊢ (type (Σ (: x A) (B x))))
+ (Γ (: x A) ⊢ (type (B x))))
+
+(define-rule Σ-eq
+ (Γ ⊢ (≐ (Σ (: x A) (B x))
+ (Σ (: x A') (B' x))))
+ (Γ ⊢ (≐ A A'))
+ (Γ (: x A) ⊢ (≐ (B x) (B' x))))
+
+(define-rule Σ-introduction
+ (Γ ⊢ (: pair (Π (: x A)
+ (→ (B x)
+ (Σ (: y A)
+ (B y))))))
+ (Γ (: x A) ⊢ (type (B x))))
+
+(define-rule Σ-elimination
+ (Γ ⊢ (: ind-Σ (→ (Π (: x A)
+ (Π (: y (B x))
+ (P ((pair x) y))))
+ (Π (: z (Σ (: x A)
+ (B x)))
+ (P z)))))
+ (Γ (: x A) ⊢ (type (B x)))
+ (Γ (: z (Σ (: x A) (B x))) ⊢ (type (P z))))
+
+(define-rule Σ-computation
+ (Γ (: x A) (: y (B x)) (: g (Π (: x A)
+ (Π (: y (B x))
+ (P ((pair x) y)))))
+ ⊢ (≐ ((ind-Σ g) ((pair x) y))
+ ((g x) y)
+ (P ((pair x) y))))
+ (Γ (: z (Σ (: x A) (B x))) ⊢ (type (P z))))
+
+;;;; Natural Numbers
+
+(define-rule ℕ-formation
+ (⊢ (type ℕ)))
+
+(define-rule ℕ-introduction-1
+ (⊢ (: 0 ℕ)))
+
+(define-rule ℕ-introduction-2
+ (⊢ (: succ (→ ℕ ℕ))))
+
+(define-rule ℕ-elimination
+ (Γ ⊢ (: (ind-ℕ p0 ps)
+ (Π (: n ℕ)
+ (P n))))
+ (Γ (: n ℕ) ⊢ (type (P n)))
+ (Γ ⊢ (: p0 (P 0)))
+ (Γ ⊢ (: ps (Π (: n ℕ)
+ (→ (P n)
+ (P (succ n)))))))
+
+(define-rule ℕ-computation-1
+ (Γ ⊢ (≐ ((ind-ℕ p0 ps) 0)
+ p0
+ (P 0)))
+ (Γ (: n ℕ) ⊢ (type (P n)))
+ (Γ ⊢ (: p0 (P 0)))
+ (Γ ⊢ (: ps (Π (: n ℕ)
+ (→ (P n)
+ (P (succ n)))))))
+
+(define-rule ℕ-computation-2
+ (Γ (: n ℕ) ⊢ (≐ ((ind-ℕ p0 ps) (succ n))
+ (ps n ((ind-ℕ p0 ps) n))
+ (P (succ n))))
+ (Γ (: n ℕ) ⊢ (type (P n)))
+ (Γ ⊢ (: p0 (P 0)))
+ (Γ ⊢ (: ps (Π (: n ℕ)
+ (→ (P n)
+ (P (succ n)))))))
+
+;;;; Boolean Type
+
+(define-rule bool-formation
+ (⊢ (type Bool)))
+
+(define-rule bool-introduction-1
+ (⊢ (: false Bool)))
+
+(define-rule bool-introduction-2
+ (⊢ (: true Bool)))
+
+(define-rule bool-elimination
+ (Γ ⊢ (: (ind-Bool p0 p1)
+ (Π (: x Bool)
+ (P x))))
+ (Γ (: x Bool) ⊢ (type (P x)))
+ (Γ ⊢ (: p0 (P false)))
+ (Γ ⊢ (: p1 (P true))))
+
+(define-rule bool-computation-1
+ (Γ ⊢ (≐ ((ind-Bool p0 p1) false)
+ p0
+ (P false)))
+ (Γ (: x Bool) ⊢ (type (P x)))
+ (Γ ⊢ (: p0 (P false)))
+ (Γ ⊢ (: p1 (P true))))
+
+(define-rule bool-computation-2
+ (Γ ⊢ (≐ ((ind-Bool p0 p1) true)
+ p1
+ (P true)))
+ (Γ (: x Bool) ⊢ (type (P x)))
+ (Γ ⊢ (: p0 (P false)))
+ (Γ ⊢ (: p1 (P true))))
+
+;;;; List Type
+
+(define-rule list-formation
+ (Γ ⊢ (type (List A)))
+ (Γ ⊢ (type A)))
+
+(define-rule list-introduction-1
+ (Γ ⊢ (: nil (List A)))
+ (Γ ⊢ (type A)))
+
+(define-rule list-introduction-2
+ (Γ ⊢ (: cons (→ A (→ (List A)
+ (List A)))))
+ (Γ ⊢ (type A)))
+
+(define-rule list-elimination
+ (Γ ⊢ (: (ind-List p0 ps)
+ (Π (: xs (List A))
+ (P xs))))
+ (Γ ⊢ (type A))
+ (Γ (: xs (List A)) ⊢ (type (P xs)))
+ (Γ ⊢ (: p0 (P nil)))
+ (Γ ⊢ (: ps (Π (: x A)
+ (Π (: xs (List A))
+ (→ (P xs)
+ (P ((cons x) xs))))))))
+
+(define-rule list-computation-1
+ (Γ ⊢ (≐ ((ind-List p0 ps) nil)
+ p0
+ (P nil)))
+ (Γ ⊢ (type A))
+ (Γ (: xs (List A)) ⊢ (type (P xs)))
+ (Γ ⊢ (: p0 (P nil)))
+ (Γ ⊢ (: ps (Π (: x A)
+ (Π (: xs (List A))
+ (→ (P xs)
+ (P ((cons x) xs))))))))
+
+(define-rule list-computation-2
+ (Γ (: x A) (: xs (List A)) ⊢ (≐ ((ind-List p0 ps) ((cons x) xs))
+ (((ps x) xs) ((ind-List p0 ps) xs))
+ (P ((cons x) xs))))
+ (Γ ⊢ (type A))
+ (Γ (: xs (List A)) ⊢ (type (P xs)))
+ (Γ ⊢ (: p0 (P nil)))
+ (Γ ⊢ (: ps (Π (: x A)
+ (Π (: xs (List A))
+ (→ (P xs)
+ (P ((cons x) xs))))))))
+
+;;;; Vector Type
+
+(define-rule vector-formation
+ (Γ ⊢ (type (Vector A n)))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (: n ℕ)))
+
+(define-rule vector-introduction-1
+ (Γ ⊢ (: #() (Vector A 0)))
+ (Γ ⊢ (type A)))
+
+(define-rule vector-introduction-2
+ (Γ ⊢ (: :: (Π (: n ℕ)
+ (→ A (→ (Vector A n)
+ (Vector A (succ n)))))))
+ (Γ ⊢ (type A)))
+
+(define-rule vector-elimination
+ (Γ ⊢ (: (ind-Vector p0 ps)
+ (Π (: n ℕ)
+ (Π (: xs (Vector A n))
+ (P xs)))))
+ (Γ ⊢ (type A))
+ (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
+ (Γ ⊢ (: p0 (P #())))
+ (Γ ⊢ (: ps (Π (: n ℕ)
+ (Π (: x A)
+ (Π (: xs (Vector A n))
+ (→ (P xs)
+ (P (((:: n) x) xs)))))))))
+
+(define-rule vector-computation-1
+ (Γ ⊢ (≐ ((ind-Vector p0 ps) #())
+ p0
+ (P #())))
+ (Γ ⊢ (type A))
+ (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
+ (Γ ⊢ (: p0 (P #())))
+ (Γ ⊢ (: ps (Π (: n ℕ)
+ (Π (: x A)
+ (Π (: xs (Vector A n))
+ (→ (P xs)
+ (P (((:: n) x) xs)))))))))
+
+(define-rule vector-computation-2
+ (Γ (: x A) (: n ℕ) (: xs (Vector A n)) ⊢ (≐ (((ind-Vector p0 ps) n) (((:: n) x) xs))
+ ((((ps n) x) xs)
+ (((ind-Vector p0 ps) n) xs))
+ (P (((:: n) x) xs))))
+ (Γ ⊢ (type A))
+ (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
+ (Γ ⊢ (: p0 (P #())))
+ (Γ ⊢ (: ps (Π (: n ℕ)
+ (Π (: x A)
+ (Π (: xs (Vector A n))
+ (→ (P xs)
+ (P (((:: n) x) xs)))))))))
+
+;;;; More Derivations
+
(define-derivation identity ((Γ ⊢ (: (λ x x) (→ A A)))
(Γ ⊢ (type A)))
- (λ)
+ (→-λ)
+ (generic-element)
+ (exact)
(exact)
- (generic-element #:index 1)
(exact))
-(define-derivation not ((⊢ (: (λ x (((if x) false) true))
- (→ Bool Bool))))
+(define-derivation if ((Γ ⊢ (: (λ z (λ x (λ y ((ind-Bool y x) z))))
+ (Π (: z Bool)
+ (→ (P true)
+ (→ (P false)
+ (P z))))))
+ (Γ (: z Bool) ⊢ (type (P z))))
(λ)
+ (→-λ #:start 1)
+ (→-λ #:start 2)
+ (interchange #:end 2)
(bool-formation)
- (substitution a true x y A Bool)
- (weakening #:index 0)
+ (substitution A Bool a true x z)
+ (bool-introduction-2)
+ (exact)
+ (interchange #:start 1)
+ (weakening)
+ (substitution A Bool a true x z)
+ (bool-introduction-2)
+ (exact)
+ (bool-formation)
+ (weakening)
+ (substitution A Bool a true x z)
+ (bool-introduction-2)
+ (exact)
+ (substitution A Bool a false x z)
+ (bool-introduction-1)
+ (exact)
+ (evaluation #:start 2 f (ind-Bool y x))
+ (bool-elimination #:start 2 (P false) (P false) (P true) (P true))
+ (weakening #:end 1)
+ (substitution A Bool a true x z)
+ (bool-introduction-2)
+ (exact)
+ (weakening #:end 1)
+ (substitution A Bool a false x z)
+ (bool-introduction-1)
+ (exact)
+ (exact)
+ (weakening #:end 1)
+ (substitution A Bool a true x z)
+ (bool-introduction-2)
+ (exact)
+ (generic-element)
+ (substitution A Bool a false x z)
+ (bool-introduction-1)
+ (exact)
+ (weakening #:start 1)
+ (weakening)
+ (substitution A Bool a true x z)
+ (bool-introduction-2)
+ (exact)
+ (substitution A Bool a false x z)
+ (bool-introduction-1)
+ (exact)
+ (generic-element)
+ (substitution A Bool a true x z)
+ (bool-introduction-2)
+ (exact)
+ (weakening #:end 1)
(bool-formation)
+ (weakening)
+ (substitution A Bool a true x z)
+ (bool-introduction-2)
+ (exact)
+ (substitution A Bool a false x z)
(bool-introduction-1)
- (ev #:index 1)
- (substitution a false x y A Bool)
- (weakening #:index 0)
+ (exact)
+ (weakening #:start 1)
+ (weakening)
+ (bool-formation)
+ (substitution #:start 1 A Bool a true x z)
+ (bool-introduction-2 #:start 1)
+ (exact)
+ (exact)
+ (weakening)
(bool-formation)
+ (substitution A Bool a true x z)
(bool-introduction-2)
- (ev #:index 1)
- (ev #:index 0)
- (bool-elimination)
+ (exact)
+ (→ #:start 1)
+ (weakening)
+ (bool-formation)
+ (substitution A Bool a false x z)
+ (bool-introduction-1)
+ (exact)
+ (exact))
+
+(define-derivation not ((Γ ⊢ (: (ind-Bool true false)
+ (→ Bool Bool))))
+ (element-conversion A (Π (: x Bool) Bool))
+ (bool-elimination (P false) Bool (P true) Bool)
+ (weakening)
+ (bool-formation)
+ (bool-formation)
+ (bool-introduction-2)
+ (bool-introduction-1)
+ (type-symmetric)
+ (definition)
+ (bool-formation)
(bool-formation))
(define-derivation constant ((Γ (: y B) ⊢ (: (λ x y) (→ A B)))
(Γ ⊢ (type A))
(Γ ⊢ (type B)))
+ (→-λ #:start 1)
+ (weakening #:start 1)
+ (weakening)
+ (exact)
+ (exact)
+ (generic-element)
+ (exact)
+ (weakening)
+ (exact)
+ (exact)
+ (weakening)
+ (exact)
+ (exact))
+
+(define-derivation =-inverse ((Γ ⊢ (: (λ x (ind-eq refl))
+ (Π (: x A)
+ (Π (: y A)
+ (→ (= x y)
+ (= y x))))))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (: x A)))
(λ)
- (weakening #:index 1)
+ (substitution #:start 1 a refl x u A (= x x))
+ (=-introduction #:start 1 A A)
+ (generic-element)
+ (exact)
+ (→-evaluation #:start 1 f ind-eq)
+ (element-conversion #:start 1 A (→ (= x x) (Π (: y A) (Π (: p (= x y)) (= y x)))))
+ (=-elimination #:start 1)
+ (generic-element)
+ (exact)
+ (weakening #:start 2)
+ (=-formation #:start 1)
+ (generic-element)
+ (exact)
+ (interchange)
+ (exact)
+ (exact)
+ (=-formation #:start 1)
+ (generic-element)
+ (exact)
+ (→-eq #:start 1)
+ (type-reflexive #:start 1)
+ (=-formation)
(exact)
+ (Π-eq #:start 1)
+ (weakening)
(exact)
- (weakening #:index 2)
- (weakening #:index 1)
+ (type-reflexive)
(exact)
+ (type-symmetric #:start 2)
+ (definition #:start 2)
+ (=-formation #:start 1)
+ (generic-element)
(exact)
- (generic-element #:index 1)
+ (interchange)
+ (exact)
+ (exact)
+ (=-formation #:start 1)
+ (generic-element)
+ (exact)
+ (=-formation)
+ (exact)
+ (Π #:start 1)
+ (→ #:start 2)
+ (=-formation #:start 1)
+ (generic-element)
+ (exact)
+ (interchange)
+ (exact)
+ (exact)
+ (=-formation #:start 1)
+ (generic-element)
(exact))
+
+(define-derivation add (((: m ℕ) ⊢ (: (ind-ℕ m ((λ n succ) m)) (→ ℕ ℕ))))
+ (element-conversion #:start 1 A (Π (: x ℕ) ℕ))
+ (ℕ-elimination #:start 1 (P 0) ℕ (P n) ℕ (P (succ n)) ℕ)
+ (weakening #:start 1)
+ (weakening)
+ (ℕ-formation)
+ (ℕ-formation)
+ (weakening)
+ (ℕ-formation)
+ (ℕ-formation)
+ (generic-element)
+ (ℕ-formation)
+ (element-conversion #:start 1 A (→ ℕ ℕ))
+ (→-evaluation f (λ n succ))
+ (→-λ)
+ (weakening)
+ (ℕ-formation)
+ (ℕ-introduction-2)
+ (ℕ-formation)
+ (→)
+ (ℕ-formation)
+ (ℕ-formation)
+ (ℕ-formation)
+ (→)
+ (ℕ-formation)
+ (ℕ-formation)
+ (definition #:start 1)
+ (weakening)
+ (ℕ-formation)
+ (ℕ-formation)
+ (weakening)
+ (ℕ-formation)
+ (ℕ-formation)
+ (weakening)
+ (ℕ-formation)
+ (type-symmetric)
+ (definition)
+ (ℕ-formation)
+ (ℕ-formation))
+
+(define-derivation add-2-length ((Γ ⊢ (:= add-2-length
+ (: (λ x (λ xs succ))
+ (Π (: x A)
+ (Π (: xs (List A))
+ (→ ℕ ℕ))))))
+ (Γ ⊢ (type A)))
+ (λ)
+ (λ #:start 1)
+ (weakening #:start 1)
+ (weakening)
+ (exact)
+ (list-formation)
+ (exact)
+ (weakening)
+ (exact)
+ (ℕ-introduction-2))
+
+(define-derivation length ((Γ ⊢ (: (λ xs ((ind-List 0 add-2-length) xs))
+ (→ (List A) ℕ)))
+ (Γ ⊢ (type A)))
+ (→-λ)
+ (evaluation f (ind-List 0 add-2-length))
+ (list-elimination (P nil) ℕ x x (P ((cons x) xs)) ℕ)
+ (exact)
+ (weakening)
+ (list-formation)
+ (exact)
+ (ℕ-formation)
+ (ℕ-introduction-1)
+ (add-2-length)
+ (exact)
+ (list-formation)
+ (exact)
+ (ℕ-formation))
#:use-module (srfi srfi-9)
#:use-module (vouivre misc)
#:export
- (*rules*
+ (d
apply-rule
- apply-rules
- conclusion
- d
+ derivation?
+ derivation-tree
+ derivation-steps
define-derivation
define-rule
- exact
- list-hypotheses))
+ define-derivation-list
+ *rules*
+ *definition-rules*))
-(define *rules* (make-hash-table))
-(define reserved-symbols '(: ≐ ⊢ type /))
-
-(define-record-type derivation
- (make-derivation tree points)
- derivation?
- (tree derivation-tree)
- (points derivation-points derivation-points-set!))
-
-(define-record-type evaluation
- (make-evaluation function value)
- evaluation?
- (function evaluation-function)
- (value evaluation-value))
+;;;; miscellaneous routines
(define (papply proc . args)
(lambda (. rest)
(apply proc (append args rest))))
-(define (all pred lst)
- "Like `every', but return the list of all `pred' return values on success."
- (call/cc
- (lambda (break)
- (reverse
- (fold
- (lambda (x prev)
- (if-let (y (pred x))
- (cons y prev)
- (break #f)))
- '() lst)))))
-
-(define (unreserved-symbol? x)
- (and (symbol? x)
- (not (member x reserved-symbols))))
-
-(define (parse-unreserved-symbol expr)
- (if (and (symbol? expr)
- (not (member expr reserved-symbols)))
- expr
- #f))
-
-(define (parse-type-variable expr)
- (parse-unreserved-symbol expr))
-
-(define (parse-type expr)
- (match expr
- ((? parse-unreserved-symbol A)
- expr)
- (((? parse-unreserved-symbol B)
- (? parse-type x)
- ..1)
- expr)
- (_ #f)))
-
-(define (parse-type-variable-declaration expr)
- (match expr
- ((': (? parse-type-variable x)
- (? parse-type A))
- (list ': x A))
- (_ #f)))
-
-(define (parse-context expr)
- (match expr
- (((? parse-type-variable-declaration X) ...)
- expr)
- (((? parse-unreserved-symbol Γ)
- (? parse-type-variable-declaration X)
- ...
- (? parse-unreserved-symbol Δ))
- expr)
- (((? parse-unreserved-symbol Γ)
- (? parse-type-variable-declaration X)
- ...
- ('/ (? parse-unreserved-symbol Δ)
- (? unreserved-symbol? x)
- (? unreserved-symbol? y)))
- expr)
- (((? parse-unreserved-symbol Γ)
- (? parse-type-variable-declaration X)
- ...)
- expr)
- (_ #f)))
-
-(define (parse-element expr)
- (match expr
- ((? parse-unreserved-symbol a)
- expr)
- (((? parse-unreserved-symbol b)
- (? parse-element x)
- ...)
- expr)
- (((? parse-element b)
- (? parse-type-variable x))
- expr)
- (_ #f)))
-
-(define (parse-judgment expr)
- (match expr
- ((context ... '⊢ J)
- (and (parse-context context)
- (match J
- ;; generic judgment thesis
- ((? unreserved-symbol? J)
- expr)
- (('/ (? unreserved-symbol? J)
- (? unreserved-symbol? a)
- (? unreserved-symbol? x))
- expr)
- ;; type
- (('type (? parse-type A))
- expr)
- ;; judgmentally equal types
- (('≐ ('/ (? parse-type A)
- (? unreserved-symbol? x)
- (? unreserved-symbol? y))
- ('/ (? parse-type B)
- (? unreserved-symbol? x')
- (? unreserved-symbol? y)))
- expr)
- (('≐ (? parse-type A)
- (? parse-type B))
- expr)
- ;; judgmentally equal elements of a type
- (('≐ ('/ (? parse-element a)
- (? unreserved-symbol? x)
- (? unreserved-symbol? y))
- ('/ (? parse-element b)
- (? unreserved-symbol? x')
- (? unreserved-symbol? y))
- ('/ (? parse-type A)
- (? unreserved-symbol? x)
- (? unreserved-symbol? y)))
- expr)
- (('≐ (? parse-element a)
- (? parse-element b)
- (? parse-type A))
- expr)
- ;; element of a type
- ((': (? parse-element a)
- (? parse-type A))
- expr)
- ;;
- (_ #f))))
- (_ #f)))
-
-(define (parse literals judgments)
- "Parse literals and judgments of a rule returning them as a cons cell on
-success and `#f' on failure."
- (and (list? literals)
- (every symbol? literals)
- (match judgments
- ((C Hs ...)
- (and=> (all parse-judgment judgments)
- (papply cons literals)))
- (_ #f))))
-
-(defmacro define-rule (name literals judgments)
- (let ((x (parse literals judgments)))
- (ifn x
- (error "SYNTAX ERROR")
- (begin
- (hash-set! *rules* name `,x)
- `(hash-set! *rules* ',name ',x)))))
-
-(define* (apply-rule derivation name #:key index . args)
- (if (eq? name 'exact)
- (exact derivation)
- (if-let (rule (hash-ref *rules* name))
- (match-let (((literals . (C Hs ...)) rule))
- (let* ((ps (derivation-points derivation))
- (p (car ps))
- (expr (car p)))
- (and=>
- (match-judgment
- expr C
- ;; When `#:index' is provided the evaluator adds it to
- ;; the head of the `args' list (see the documentation
- ;; `define*') followed by its value, and they must be
- ;; removed.
- (alist<-plist (ifn index args (cddr args)))
- index)
- (lambda (bindings)
- (and=>
- (call/cc
- (lambda (break)
- ;; Each hypothesis, with bindings replaced, is wrapped
- ;; in a cons cell, to be added to the derivation
- ;; points.
- (map (lambda (hypothesis)
- (list (or (replace-in-judgment hypothesis bindings)
- (break #f))))
- Hs)))
- (lambda (points)
- (set-cdr! p points)
- ;; Remove the current point, adding its leaves as new
- ;; points.
- (derivation-points-set! derivation (append points
- (cdr ps)))
- derivation))))))
- (error "Rule undefined."))))
-
-(define (apply-rules derivation rules)
+(define-syntax-rule (second-value expr)
+ (receive (x y . rest)
+ expr y))
+
+(define (unzip lst)
+ (map reverse
+ (let rec ((lst lst)
+ (acc (map (const '())
+ (car lst))))
+ (if (null? lst)
+ acc
+ (rec (cdr lst)
+ (map cons (car lst) acc))))))
+
+;;;; data
+
+(define *constructors* (make-hash-table))
+(define *rules* (make-hash-table))
+(define *definition-rules* (make-hash-table))
+(define *types* (make-hash-table))
+(define *ctxs* (make-parameter #f))
+
+(define-record-type derivation
+ (make-derivation tree steps)
+ derivation?
+ (tree derivation-tree)
+ (steps derivation-steps))
+
+(define-record-type substitution
+ (make-substitution pattern source destination)
+ substitution?
+ (pattern substitution-pattern)
+ (source substitution-source)
+ (destination substitution-destination))
+
+(define element-of-:xX second)
+(define judgment-context (papply take-while (compose not (papply eq? '⊢))))
+(define judgment-content last)
+(define meta-conclusion car)
+(define meta-hypotheses cdr)
+(define constructor-ref (papply hash-ref *constructors*))
+(define (context-ref ctx var)
+ (find (lambda (:xX)
+ (eq? var (element-of-:xX :xX)))
+ ctx))
+(define rule-ref (papply hash-ref *rules*))
+(define type-ref (papply hash-ref *types*))
+
+;; NOTE: The requirement that for declared types and constructors we can list
+;; the kind of its arguments, if any, imposes additional constraints that
+;; must be checked in `define-rule'. Incidentally, we can dispense with
+;; some checks here because we know that interned metas satisfy these
+;; constraints.
+(define (meta-arguments-kinds meta)
+ (let ((content (judgment-content (meta-conclusion meta))))
+ (ifn (list? content)
+ (parse-error
+ "meta-arguments-kinds: requires a type kind of judgment.")
+ (case (first content)
+ ((type)
+ (case (car (second content))
+ ((→)
+ '(type type))
+ ((Π)
+ '(binding type))
+ ((=)
+ '(element element))
+ ((Σ)
+ '(binding type))
+ ((List)
+ '(type))
+ ((Vector)
+ '(type element))
+ (else (parse-error "unsupported type."))))
+ (else
+ (parse-error
+ "meta-arguments-kinds: requires a type kind of judgment."))))))
+
+(define (d judgment)
+ (make-derivation (cons judgment #f) '()))
+
+(define (derivation-point derivation)
(call/cc
(lambda (break)
- (fold (lambda (rule prev)
- (if-let (x (apply apply-rule prev (car rule) (cdr rule)))
- x
- (break #f)))
- derivation rules))))
+ (let rec ((tree (derivation-tree derivation)))
+ (ifn (cdr tree)
+ (break (car tree))
+ (ifn (list? (cdr tree))
+ #f
+ (fold (lambda (x _)
+ (rec x))
+ #f (cdr tree))))))))
+
+(define (expand-derivation-point derivation step stuff)
+ (match-let (((expanded? . tree)
+ (let rec ((tree (derivation-tree derivation)))
+ (ifn (cdr tree)
+ (cons #t (cons (car tree) stuff))
+ (ifn (list? (cdr tree))
+ (cons #f tree)
+ (match-let (((expanded? . rlst)
+ (fold (lambda (x prev)
+ (if (car prev)
+ (cons #t (cons x (cdr prev)))
+ (let ((r (rec x)))
+ (cons (car r)
+ (cons (cdr r) (cdr prev))))))
+ '(#f . ())
+ (cdr tree))))
+ (cons expanded? (cons (car tree) (reverse rlst)))))))))
+ (values (make-derivation tree (cons step (derivation-steps derivation)))
+ expanded?)))
+
+(define (list-hypotheses derivation)
+ (delete-duplicates
+ (let rec ((tree (derivation-tree derivation))
+ (lst '()))
+ (if (or (not (cdr tree))
+ (not (list? (cdr tree))))
+ (cons (car tree) lst)
+ (fold rec lst (cdr tree))))
+ equal?))
+
+;;;; parsing routines
+
+;;; In what follows, we want to do for judgments what `map' and `fold' do for
+;;; lists – to evaluate a function on the judgment's intrinsics. We proceed by
+;;; implementing map/fold routines in a "Russian doll" kind of way from big to
+;;; small (although they appear in this file in reverse order i.e from callee to
+;;; caller): judgment, content and context, type, and element. For each of these
+;;; we have a "dispatch" routine to abstract away the structural analysis and
+;;; validation that is common to the corresponding map and fold. Follows, a
+;;; simple application of `judgment-map'. The others work in a similar fashion.
+;;;
+;;; (define (prime x) (string->symbol (string-append (symbol->string x) "'")))
+;;;
+;;; (judgment-map (lambda (kind x y)
+;;; (case kind
+;;; ((type)
+;;; (prime y))
+;;; (else x)))
+;;; #f
+;;; '(Λ ⊢ (type A))
+;;; '(Ξ ⊢ (type B)))
+;;; => (Λ ⊢ (type B'))
+;;;
+;;; As you can see, there are two differences with `map'. The first is `kind',
+;;; which binds to the kind of intrinsics currently being mapped (either
+;;; 'element, 'type, 'Γ, or 'Δ). The second is the range, `#f' here, which
+;;; allows the split of variable declarations between Γs and Δs.
+
+(define (parse-error str . format-args)
+ (error (string-append "parsing error: "
+ (apply format #f str format-args))))
+
+(define just cdr)
+
+(define (pre-destruct kind expr)
+ (define fmt "destruct: unknown expression ~a of kind ~a.")
+ ;; Since the name can be any expression including `#f' we wrap it as a
+ ;; "Maybe" so that we can distinguish the absence of a name from the name
+ ;; `#f'.
+ (ifn (list? expr)
+ (values (cons 'just expr) '())
+ (if (or (null? expr)
+ (null? (cdr expr)))
+ (parse-error fmt expr kind)
+ (if (list? (car expr))
+ (if (eq? kind 'type)
+ (parse-error fmt expr kind)
+ ;; When instead of a name we have an s-expression the
+ ;; expression must have a size of exactly two.
+ (ifn (null? (cddr expr))
+ (parse-error fmt expr kind)
+ (values #f (cdr expr))))
+ (values (cons 'just (car expr))
+ (cdr expr))))))
+
+(define (destruct kind expr)
+ "Destructure an element or type into its head, tail, and meta data, raising an
+ error if the expression has an unexpected format.
+
+ kind: The kind of expression to destructure. This is either 'type or
+ 'element.
+
+ expr: The expression to destructure.
+
+ Returns Maybe name, List arguments, and either `#f' or the name's meta data,
+ as multiple values."
+ (define referee (if (eq? kind 'element) constructor-ref type-ref))
+ (define fmt "destruct: unknown expression ~a of kind ~a.")
+ (receive (maybe-name args) (pre-destruct kind expr)
+ (ifn maybe-name
+ (values maybe-name args #f)
+ (if-let (meta (referee (just maybe-name)))
+ (let ((n-args (length args))
+ (n-meta-args (length (second-value
+ (pre-destruct
+ kind
+ (element-of-:xX
+ (judgment-content
+ (meta-conclusion meta))))))))
+ (if (= n-args n-meta-args)
+ (values maybe-name args meta)
+ ;; We allow constructors declared with no arguments to be
+ ;; curried applications.
+ (if (and (eq? kind 'element)
+ (= 1 n-args)
+ (zero? n-meta-args))
+ (values maybe-name args meta)
+ (parse-error "destruct: declared expression ~a has ~a arguments, but expected ~a." expr n-args n-meta-args))))
+ (values maybe-name args #f)))))
+
+(define (element-dispatch function exprs)
+ "Dispatch a function based on the given elements or raise an error if they
+ have an unexpcted format. There are three kinds of expressions: declared
+ constructors, undeclared constructors, and curried application to an
+ argument.
+
+ function: A function of one argument called with 'declared, 'undeclared, or
+ 'applied if, respectively, expressions are: all declared, any are
+ undeclared, or all are applied.
+
+ exprs: List of expressions.
+
+ Returns the result of the function application."
+ (define element-destruct (papply destruct 'element))
+ (receive (maybe-names argss metas)
+ (unzip3 (map (lambda (expr) (receive vals (element-destruct expr) vals))
+ exprs))
+ ;; All declared constructors must have the same meta data and their number
+ ;; of arguments must match.
+ (unless (apply eq? (remove not metas))
+ (parse-error "element-dispatch: declared constructors don't match."))
+ (if (every (lambda (maybe-name args meta)
+ (or (not maybe-name)
+ (and meta
+ (= 1 (length args))
+ (zero? (length (second-value
+ (pre-destruct
+ 'element
+ (element-of-:xX
+ (judgment-content
+ (meta-conclusion meta))))))))))
+ maybe-names argss metas)
+ (function 'applied maybe-names argss metas)
+ (if (every identity metas)
+ (function 'declared maybe-names argss metas)
+ (function 'undeclared maybe-names argss metas)))))
+
+(define (element-map function expr . more)
+ "Map a function on the given elements or raise an error if they have unexpected
+ format.
+
+ function: A function that will always be called with 'element as its first
+ argument, to be consistant with `type-map', and then with the
+ corresponding intrinsics of each expression.
+
+ expr . more: One or more expressions.
+
+ Returns an element that is the result of mapping the function to the
+ corresponding intrinsics."
+ (let ((exprs (cons expr more)))
+ (element-dispatch
+ (lambda (kind maybe-names argss metas)
+ (case kind
+ ((declared)
+ (if (null? (car argss))
+ (apply function 'element exprs)
+ (cons (just (car maybe-names)) ; all expressions have the same name
+ (apply map
+ (lambda formals
+ (apply element-map function formals))
+ argss))))
+ ((undeclared)
+ (apply function 'element exprs))
+ ((applied)
+ ;; Each expression is of the form '(f x).
+ (list (apply element-map function (map first exprs))
+ (apply element-map function (map second exprs))))))
+ exprs)))
+
+(define (element-fold function init expr . more)
+ "Fold a function over the given elements or raise an error if they have
+ unexpected format.
+
+ function: A function that will always be called with 'element as its first
+ argument, to be consistant with `type-fold', and then with the
+ corresponding intrinsics of each expression, followed by the
+ latest accumulator.
+
+ expr . more: One or more expressions.
+
+ Returns an element that is the result of folding the function over the
+ corresponding intrinsics."
+ (let ((exprs (cons expr more)))
+ (element-dispatch
+ (lambda (kind maybe-names argss metas)
+ (case kind
+ ((declared)
+ (if (null? (car argss))
+ (apply function 'element `(,@exprs ,init))
+ (apply fold
+ (lambda formals
+ (apply element-fold function
+ (last formals)
+ (but-last formals)))
+ init argss)))
+ ((undeclared)
+ (apply function 'element `(,@exprs ,init)))
+ ((applied)
+ (apply element-fold function
+ (apply element-fold function init
+ (map first exprs))
+ (map second exprs)))))
+ exprs)))
+
+(define (type-dispatch function exprs)
+ "Dispatch a function based on the given types or raise an error if they
+ have an unexpcted format. There are two kinds of expressions: declared
+ types, and undeclared types.
+
+ function: A function of one argument called with 'declared or 'undeclared if,
+ respectively, expressions are: all declared, or any are undeclared.
+
+ exprs: List of expressions.
+
+ Returns the result of the function application."
+ (define type-destruct (papply destruct 'type))
+ (receive (maybe-names argss metas)
+ (unzip3 (map (lambda (expr) (receive vals (type-destruct expr) vals)) exprs))
+ ;; All declared types must have the same meta data and their number
+ ;; of arguments must match.
+ (unless (apply eq? (remove not metas))
+ (parse-error "type-dispatch: declared types don't match."))
+ (if (every identity metas)
+ (function 'declared maybe-names argss metas)
+ (function 'undeclared maybe-names argss metas))))
+
+(define (type-map function expr . more)
+ "Map a function to type-expressions. See the documentation of `element-map' which
+ has analogous behaviour except for the function who's called on a kind that
+ alternates between 'type and 'element based on the intrinsic."
+ (let ((exprs (cons expr more)))
+ (type-dispatch
+ (lambda (kind maybe-names argss metas)
+ (case kind
+ ((declared)
+ (if (null? (car argss))
+ (apply function 'type exprs)
+ (cons (just (car maybe-names)) ; all expressions have the same name
+ (apply map
+ (lambda formals
+ (if (eq? 'binding (car formals))
+ (match (cdr formals)
+ (((': xs Xs) ...)
+ (list ':
+ (apply element-map function xs)
+ (apply type-map function Xs)))
+ (_
+ (parse-error "type-map: declared types don't match.")))
+ (apply (case (car formals)
+ ((element)
+ element-map)
+ ((type)
+ type-map))
+ function (cdr formals))))
+ (cons (meta-arguments-kinds (type-ref (car expr)))
+ argss)))))
+ ((undeclared)
+ (apply function 'type exprs))))
+ exprs)))
+
+(define (type-fold function init expr . more)
+ "Fold a function over type-expressions. See the documentation of `element-fold'
+ which has analogous behaviour except for the function who's called on a kind
+ that alternates between 'type and 'element based on the intrinsic."
+ (let ((exprs (cons expr more)))
+ (type-dispatch
+ (lambda (kind maybe-names argss metas)
+ (case kind
+ ((declared)
+ (if (null? (car argss))
+ (apply function 'type `(,@exprs ,init))
+ (apply fold
+ (lambda formals
+ (if (eq? 'binding (car formals))
+ (match (but-last (cdr formals))
+ (((': xs Xs) ...)
+ (apply element-fold function
+ (apply type-fold function
+ (last formals)
+ Xs)
+ xs))
+ (_
+ (parse-error "type-fold: declared types don't match.")))
+ (apply (case (car formals)
+ ((element)
+ element-fold)
+ ((type)
+ type-fold))
+ function
+ (last formals)
+ (but-last (cdr formals)))))
+ init (cons (meta-arguments-kinds (type-ref (car expr)))
+ argss))))
+ ((undeclared)
+ (apply function 'type `(,@exprs ,init)))))
+ exprs)))
(define (split-in-three lst start end)
"Split the given list in three with `start' and `end' the indices delimiting
(cons (car zs) ys)
(cdr zs))))))
-(define (sub e x y)
- (define (sub% e x y)
- (if (eq? e x)
- y
- (if (symbol? e)
- e
- (map (lambda (e) (sub e x y)) e))))
- (ifn x e (sub% e x y)))
-
-(define* (match-context expr pattern bindings #:optional index)
- "Match a context pattern to a context expression, binding symbols in the
-process. Return `#f' if the pattern fails to match or the updated bindings
-otherwise.
-
-expr: Context expression.
-
-pattern: Context pattern. For examples, look at the left side of `⊢' in
- instances of `define-rule'.
-
-bindings: Association list of symbols to matched sub-expressions.
-
-index: Index of the first type variable in the expression that corresponds to
- an explicit type variable in the pattern. This is for cases like the
- expression (: x1 A1) ... (: xn An) with the pattern (Γ (: x X) Δ)
- where it is unclear from the pattern alone which variable `x'
- corresponds to."
- ;; NOTE: By construction, `expr' has the proper syntax.
- (let* ((m (length expr))
- (index (or index m))
- (bind-symbols
- (lambda* (Γ xs As Δ #:optional u v)
- (let ((n (length xs)))
- (if (> n (- m index))
- #f
- (receive (gammas explicit deltas)
- (split-in-three expr index (+ index n))
- (fold (lambda (x A z prev)
- (match-let (((': x' A') z))
- (acons x x' (acons A A' prev))))
- (ifn Γ
- (ifn Δ
- bindings
- (acons Δ (sub deltas u v)
- bindings))
- (ifn Δ
- (acons Γ gammas bindings)
- (acons Γ gammas (acons Δ (sub deltas u v)
- bindings))))
- xs As explicit)))))))
- (match pattern
- (()
- (and (= 0 m) bindings))
- (((? symbol? Γ) (': x A) ...)
- (bind-symbols Γ x A #f))
- (((? symbol? Γ) (': x A) ... ('/ Δ u v))
- (bind-symbols Γ x A Δ u v))
- (((? symbol? Γ) (': x A) ... Δ)
- (bind-symbols Γ x A Δ))
- (((': x A) ...)
- (bind-symbols #f x A #f))
- (((': x A) ... ('/ Δ u v))
- (bind-symbols #f x A Δ u v))
- (((': x A) ... Δ)
- (bind-symbols #f x A Δ))
- (_ (error "Unsupported context pattern syntax.")))))
-
-(define (match-content expr pattern bindings)
- "See the documentation for `match-context', only here we match the content of
-judgments, i.e. anything right of a `⊢' in instances of `define-rule', and no
-ambiguity arises."
- ;; NOTE: By construction, `expr' has the proper syntax.
- (define (equal-expr? v e x y)
- (or (and (not y)
- (eq? v e))
- (and (eq? v y)
- (eq? e x))
- (and (list? v)
- (list? e)
- (= (length v)
- (length e))
- (every (lambda (v e)
- (equal-expr? v e x y))
- v e))))
- (define* (bind-symbols expr pattern bindings
- #:optional generic-judgment? x y)
- (cond
- ((member pattern reserved-symbols)
- (and (eq? pattern expr)
- bindings))
- (generic-judgment?
- (if (assoc-ref bindings pattern)
- (error "Generic judgment thesis already bound.")
- (acons pattern (sub expr x y) bindings)))
- ((symbol? pattern)
- (if-let (val (assoc-ref bindings pattern))
- (and (equal-expr? val expr x y)
- bindings)
- (acons pattern (sub expr x y) bindings)))
- ((list? pattern)
- (match pattern
- (('/ B x' y')
- (let ((x' (assoc-ref bindings x'))
- (y' (assoc-ref bindings y')))
- (unless (and x' y')
- (error "Unbound substitution element."))
- (bind-symbols expr B bindings #f x' y')))
- (((? unreserved-symbol? b)
- x)
- (if (list? expr)
- (and
- (= 2 (length expr))
- (or (not (assoc-ref bindings b))
- (equal-expr? (first expr)
- (assoc-ref bindings b)
- #f #f))
- (or (not (assoc-ref bindings x))
- (equal-expr? (second expr)
- (assoc-ref bindings x)
- #f #f))
- (acons b
- (make-evaluation (first expr)
- (second expr))
- bindings))
- ;; a symbol
- (acons b
- (make-evaluation #f expr)
- bindings)))
- (else
- (and (list? expr)
- (= (length pattern)
- (length expr))
- (call/cc
- (lambda (break)
- (fold-right (lambda (e p prev)
- (if prev
- (bind-symbols e p prev #f x y)
- (break #f)))
- bindings expr pattern)))))))))
- (define* (match-content% expr pattern bindings
- #:optional generic-judgment? x y)
- (match pattern
+(define (context-dispatch function ranges exprs)
+ (define (expand-range range start end)
+ (ifn range
+ (list start end)
+ (list (or (first range) start)
+ (or (second range) end))))
+ (apply function
+ (receive (Γs :xXss Δs)
+ (unzip3
+ (map (lambda (range expr)
+ (match expr
+ (((? symbol? Γ) :xXs ... (? symbol? Δ))
+ (receive (a b c)
+ (apply split-in-three
+ :xXs
+ (expand-range range 0 (length :xXs)))
+ (list (cons Γ a) b `(,@c ,Δ))))
+ (((? symbol? Γ) :xXs ... ('/ (? symbol? Δ) x y))
+ (receive (a b c)
+ (apply split-in-three
+ :xXs
+ (expand-range range 0 (length :xXs)))
+ (list (cons Γ a) b `(,@c ,Δ))))
+ (((? symbol? Γ) :xXs ...)
+ (receive (a b c)
+ (apply split-in-three
+ :xXs
+ (expand-range range 0 (length :xXs)))
+ (list (cons Γ a) b c)))
+ ((:xXs ...)
+ (receive (a b c)
+ (apply split-in-three
+ :xXs
+ (expand-range range 0 (length :xXs)))
+ (list a b c)))
+ (_ (parse-error "context-fold: unknown expression."))))
+ (or ranges (list-tabulate (length exprs) not))
+ exprs))
+ (if (apply = (map length :xXss))
+ (list Γs :xXss Δs)
+ (parse-error "context-dispatch: contexts should have the same range, but got ~{~a~^ ~}." :xXss)))))
+
+(define (context-map function ranges expr . more)
+ (context-dispatch
+ (lambda (Γs :xXss Δs)
+ (append
+ (if (null? (car Γs)) '() (apply function 'Γ Γs))
+ (reverse
+ (cdr
+ (apply fold
+ (lambda formals
+ (let* ((:xXs (but-last formals)) ; one decl per judgment
+ (z (last formals))
+ (ctxs (car z))
+ (prev (cdr z)))
+ (if (any identity (map (lambda (ctx :xX)
+ (context-ref ctx (second :xX)))
+ ctxs :xXs))
+ (parse-error "context-map: variable can only be declared once.")
+ (cons (map cons :xXs ctxs)
+ (cons
+ (list ':
+ (apply function 'variable (map second :xXs))
+ (apply type-map function (map third :xXs)))
+ prev)))))
+ (cons (list-tabulate (length :xXss) (const '()))
+ '())
+ :xXss)))
+ (if (null? (car Δs)) '() (apply function 'Δ Δs))))
+ ranges (cons expr more)))
+
+(define (context-fold function ranges init expr . more)
+ (context-dispatch
+ (lambda (Γs :xXss Δs)
+ ;; See `context-map' for the format of Γs :xXss Δs.
+ (apply
+ (ifn (null? (car Δs)) function (lambda formals (last formals)))
+ 'Δ
+ `(,@Δs
+ ,(apply fold
+ (lambda formals
+ (let* ((:xXs (but-last formals)) ; one decl per judgment
+ (prev (last formals)))
+ (if (any identity
+ (map (lambda (ctx :xX)
+ (context-ref ctx (element-of-:xX :xX)))
+ (*ctxs*)
+ :xXs))
+ (parse-error "context-fold: variable can only be declared once.")
+ (begin
+ (*ctxs* (map cons :xXs (*ctxs*)))
+ (apply function 'variable
+ `(,@(map element-of-:xX :xXs)
+ ,(apply function 'type `(,@(map third :xXs)
+ ,prev))))))))
+ (apply (ifn (null? (car Γs)) function (lambda formals (last formals)))
+ 'Γ `(,@Γs ,init))
+ :xXss))))
+ ranges (cons expr more)))
+
+(define (content-dispatch function exprs)
+ (define (content-match expr)
+ (match expr
+ ;; generic judgment
+ (('/ (? symbol? J) (? symbol? a) (? symbol? b))
+ (list 'generic (make-substitution J a b)))
+ ((? symbol? J)
+ (list 'generic J))
+ ;; type
(('type A)
- (bind-symbols expr pattern bindings #f x y))
- ((': a A)
- (bind-symbols expr pattern bindings #f x y))
+ (list 'type A))
+ ;; judgmentally equal types
+ (('≐ ('/ A
+ (? symbol? x)
+ (? symbol? y))
+ ('/ B
+ (? symbol? x')
+ (? symbol? y)))
+ (list 'type-eq
+ (make-substitution A x y)
+ (make-substitution B x' y)))
(('≐ A B)
- (bind-symbols expr pattern bindings #f x y))
+ (list 'type-eq A B))
+ ;; judgmentally equal elements of a type
+ (('≐ ('/ a
+ (? symbol? x)
+ (? symbol? y))
+ ('/ b
+ (? symbol? x')
+ (? symbol? y))
+ ('/ A
+ (? symbol? x)
+ (? symbol? y)))
+ (list 'element-eq
+ (make-substitution a x y)
+ (make-substitution b x' y)
+ (make-substitution A x y)))
(('≐ a b A)
- (bind-symbols expr pattern bindings #f x y))
- ((? symbol? J)
- (bind-symbols expr J bindings #t x y))
- (('/ J (? symbol? x) (? symbol? y))
- (let ((x (assoc-ref bindings x))
- (y (assoc-ref bindings y)))
- (unless (and x y)
- (error "Unbound substitution element."))
- (match-content% expr J bindings (symbol? J) x y)))
- (_ (error "Unsupported content pattern syntax."))))
- (match-content% expr pattern bindings))
-
-(define* (match-judgment expr pattern bindings #:optional index)
- ;; NOTE: By construction, `expr' has the proper syntax.
- (match pattern
- ((ctx ... '⊢ J)
- (match expr
- ((ctx' ... '⊢ J')
- (and=> (match-context ctx' ctx bindings index)
- (lambda (bindings)
- (match-content J' J bindings))))))
- (_ (error "Unsupported judgment pattern syntax."))))
-
-(define (replace-in-judgment pattern bindings)
- "Replace all bound symbols (leaves) in the pattern (tree)."
- (define (replace-in-ctx x)
- (if (symbol? x)
- (or (assoc-ref bindings x)
- x)
- (map replace-in-ctx x)))
- (define (replace-in-content x)
- (match x
- ((? symbol? x)
- (if-let (y (assoc-ref bindings x))
- (ifn (evaluation? y)
- y
- (if (evaluation-function y)
- (evaluation-function y)
- (error "Can't separate function from value.")))
- x))
- (((? unreserved-symbol? b)
- (? symbol? y))
- (let ((z (assoc-ref bindings b)))
- (ifn (evaluation-function z)
- (evaluation-value z)
- (list (evaluation-function z)
- (evaluation-value z)))))
- (else
- (map replace-in-content x))))
- (match pattern
- ((ctx ... '⊢ J)
- (append
- (concatenate
- (map (lambda (x)
- (if (list? x)
- (list (replace-in-ctx x))
- (let ((y (replace-in-ctx x)))
- (if (symbol? y)
- (list y)
- y))))
- ctx))
- (list '⊢ (replace-in-content J))))
- (_ (error "Unsupported judgment pattern syntax."))))
-
-(define (d expr)
- (let ((tree (list expr)))
- (make-derivation tree (list tree))))
-
-(define (exact derivation)
- (let* ((ps (derivation-points derivation))
- (p (car ps)))
- (set-cdr! p '.)
- (derivation-points-set! derivation (cdr ps))
- derivation))
-
-(define (list-hypotheses derivation)
- (delete-duplicates
- (let rec ((tree (derivation-tree derivation)))
- (if (eq? '. (cdr tree))
- (list (car tree))
- (fold-right
- (lambda (x prev)
- (append (rec x) prev))
- '()
- (cdr tree))))
- equal?))
-
-(define conclusion (compose car derivation-tree))
-
-(defmacro define-derivation% (name conclusion hypotheses . rules)
- (let ((C (parse-judgment conclusion))
- (Hs (all parse-judgment hypotheses)))
- (ifn (and C Hs)
- (error "SYNTAX")
- (if-let (derivation (apply-rules (d C) rules))
- (let ((Hs' (list-hypotheses derivation)))
- (ifn (and (null? (lset-difference equal? Hs' Hs))
- (null? (lset-difference equal? Hs Hs')))
- (error "DERIVATION 1")
- (begin
- (hash-set! *rules*
- name
- (cons '() `(,conclusion ,@hypotheses)))
- `(hash-set! *rules*
- ',name
- (cons '() '(,conclusion ,@hypotheses))))))
- (error "DERIVATION 2")))))
-
-(define-syntax-rule (define-derivation name
- (conclusion hypothesis ...)
- (rule arg ...) ...)
- (define-derivation% name conclusion (hypothesis ...)
- (rule arg ...)
- ...))
+ (list 'element-eq a b A))
+ ;; element of a type
+ ((': a A)
+ (list 'element a A))
+ (_ (parse-error "content-dispatch: unknown expression."))))
+ (let* ((xs (map content-match exprs))
+ (generic? (papply eq? 'generic))
+ (kinds (map car xs)))
+ (unless (apply eq? (remove generic? kinds))
+ (parse-error "content-dispatch: contents don't match."))
+ (ifn (any generic? kinds)
+ (apply function (find (compose not generic?)
+ kinds)
+ (unzip (map cdr xs)))
+ (apply function 'generic
+ (map (lambda (kind x)
+ (if (generic? kind)
+ (second x)
+ (match x
+ (('type A)
+ x)
+ (('type-eq A B)
+ (list '≐ A B))
+ (('element-eq a b A)
+ (list '≐ a b A))
+ (('element a A)
+ (list ': a A)))))
+ kinds xs)))))
+
+(define (content-map function expr . more)
+ (content-dispatch
+ (lambda (kind . args)
+ (case kind
+ ((generic)
+ (apply function 'generic args))
+ ((type)
+ (list 'type (apply type-map function (first args))))
+ ((element)
+ (list ':
+ (apply element-map function (first args))
+ (apply type-map function (second args))))
+ ((type-eq)
+ (list '≐
+ (apply type-map function (first args))
+ (apply type-map function (second args))))
+ ((element-eq)
+ (list '≐
+ (apply element-map function (first args))
+ (apply element-map function (second args))
+ (apply type-map function (third args))))))
+ (cons expr more)))
+
+(define (content-fold function init expr . more)
+ (content-dispatch
+ (lambda (kind . args)
+ (case kind
+ ((generic)
+ (apply function 'generic `(,@args ,init)))
+ ((type)
+ (apply type-fold function init (first args)))
+ ((element)
+ (apply element-fold function
+ (apply type-fold function init (second args))
+ (first args)))
+ ((type-eq)
+ (apply type-fold function
+ (apply type-fold function init (second args))
+ (first args)))
+ ((element-eq)
+ (apply element-fold function
+ (apply element-fold function
+ (apply type-fold function init (third args))
+ (first args))
+ (second args)))))
+ (cons expr more)))
+
+(define (judgment-dispatch function exprs)
+ (match exprs
+ (((contexts ... '⊢ contents) ...)
+ (function contexts contents))
+ (_ (parse-error "judgment-dispatch: unknown expression."))))
+
+(define (judgment-map function ranges expr . more)
+ (judgment-dispatch (lambda (ctxs cnts)
+ (append (apply context-map function ranges ctxs)
+ (list '⊢)
+ (list (apply content-map function cnts))))
+ (cons expr more)))
+
+(define (judgment-fold function ranges init expr . more)
+ (parameterize ((*ctxs* (map (const '()) (cons expr more))))
+ (judgment-dispatch (lambda (ctxs cnts)
+ (apply content-fold function
+ (apply context-fold function ranges init ctxs)
+ cnts))
+ (cons expr more))))
+
+(defmacro define-rule (name judgment . more)
+ (begin
+ (when (eq? name 'exact)
+ (parse-error "define-rule: the rule name \"exact\" is reserved."))
+ (for-each (lambda (judgment)
+ (judgment-fold
+ (lambda (kind x prev)
+ prev)
+ #f #f judgment))
+ (cons judgment more))
+ ;; We declare types or constructors when they occur.
+ (let ((content (judgment-content judgment)))
+ (when (list? content)
+ (let ((kind (case (first content)
+ ((type) 'type)
+ ((:) 'element)
+ (else 'else))))
+ (when (member kind '(type element))
+ (if-let (maybe-name (pre-destruct kind (second content)))
+ (unless (and (eq? 'element kind)
+ (judgment-fold
+ (lambda (kind' x prev)
+ (ifn (eq? kind kind')
+ prev
+ (or prev (context-ref (car (*ctxs*))
+ (just maybe-name)))))
+ #f #f judgment))
+ (unless (any (lambda (judgment)
+ (judgment-fold
+ (lambda (kind' x prev)
+ (ifn (eq? kind kind')
+ prev
+ (or prev (equal? x (just maybe-name)))))
+ #f #f judgment))
+ more)
+ (hash-set! (if (eq? kind 'type)
+ *types*
+ *constructors*)
+ (just maybe-name)
+ (cons judgment more)))))))))
+ (hash-set! *rules* name `,(cons judgment more))
+ `(begin
+ (hash-set! *rules* ',name ',(cons judgment more))
+ (values))))
+
+(define (replace-judgment mappings judgment)
+ (judgment-map
+ (lambda (kind x)
+ (or
+ (if (member kind '(Γ Δ))
+ (assoc-ref mappings (car x))
+ (if (member kind '(element variable type generic))
+ (assoc-ref mappings x)
+ x))
+ (parse-error "replace-judgment: expression ~a not mapped in ~a." x mappings)))
+ #f judgment))
+
+(define (substitute mapper x y mapping)
+ (acons (substitution-pattern x)
+ (mapper
+ (lambda (kind z)
+ (if (and (eq? kind 'type)
+ (receive (maybe-name args meta) (destruct 'type z)
+ (and (not meta) (= 1 (length args)))))
+ (ifn (equal? (second z) (assoc-ref mapping (substitution-source x)))
+ z
+ (list (first z)
+ (assoc-ref mapping (substitution-destination x))))
+ (ifn (equal? z (assoc-ref mapping (substitution-source x)))
+ z
+ (assoc-ref mapping (substitution-destination x)))))
+ y)
+ mapping))
+
+(define* (apply-rule derivation name #:key start end . args)
+ (let ((err1 "apply-rule: derivation is pointless.")
+ (err2 "apply-rule: substitutions are only allowed in rules.")
+ (err3 "apply-rule: can't apply a specific judgment rule to a generic judgment expression.")
+ (err4 "define-derivation: rule ~s is undefined."))
+ (expand-derivation-point
+ derivation
+ (if start
+ (if end
+ `(,name #:start ,start #:end ,end ,@args)
+ `(,name #:start ,start ,@args))
+ `(,name ,@args))
+ (let ((Jp (derivation-point derivation)))
+ (unless Jp
+ (parse-error err1))
+ (if (eq? name 'exact)
+ #t
+ (if-let (m (ifn (eq? name 'definition)
+ (rule-ref name)
+ (hash-ref *definition-rules* (just (pre-destruct 'type (second (judgment-content Jp)))))))
+ ;; NOTE: Computing the mapping is essential to be sure
+ ;; the meta-conclusion matches the judgment point even
+ ;; in cases where there are no hypotheses.
+ (let ((mapping
+ (judgment-fold
+ (lambda (kind x y prev)
+ (case kind
+ ((Γ)
+ (if (substitution? y)
+ (parse-error err2)
+ (ifn (substitution? x)
+ (acons (car x) y prev)
+ (ifn (null? (cdr y))
+ (parse-error "TBD")
+ (acons (substitution-pattern x)
+ y prev)))))
+ ((Δ)
+ (if (substitution? y)
+ (parse-error err2)
+ (ifn (substitution? x)
+ (acons (car x) y prev)
+ (ifn (null? (cdr y))
+ (parse-error "TBD")
+ (acons (substitution-pattern x)
+ y prev)))))
+ ((element)
+ (if (substitution? y)
+ (parse-error err2)
+ (ifn (substitution? x)
+ (acons x y prev)
+ (substitute element-map x y prev))))
+ ((type)
+ (if (substitution? y)
+ (parse-error err2)
+ (ifn (substitution? x)
+ (acons x y prev)
+ (substitute type-map x y prev))))
+ ((generic)
+ (if (and (not (list? y))
+ (list? x))
+ ;; if y is generic so must x.
+ (parse-error err3)
+ (ifn (substitution? x)
+ (acons x y prev)
+ (if (not (list? y))
+ (acons (substitution-pattern x)
+ y prev)
+ (substitute content-map x y prev)))))
+ ((variable)
+ (acons x y prev))
+ (else
+ prev)))
+ (list #f (list start end))
+ ;; When `#:start'/`#:end' is provided the evaluator
+ ;; adds it to the head of the `args' list (see the
+ ;; documentation for `define*') followed by its value,
+ ;; and must be removed.
+ (alist<-plist
+ (if start
+ (if end
+ (drop args 4)
+ (drop args 2))
+ (if end
+ (drop args 2)
+ args)))
+
+ (meta-conclusion m)
+ Jp)))
+ (map
+ (lambda (judgment)
+ (cons (replace-judgment mapping judgment)
+ #f))
+ (meta-hypotheses m)))
+ (parse-error err4 name)))))))
+
+(defmacro define-derivation% (name kind maybe-assignment conclusion hypotheses rule . more)
+ (let ((derivation
+ (fold (lambda (step derivation)
+ (apply apply-rule derivation step))
+ (d conclusion)
+ (cons rule more))))
+ (ifn (lset= equal? hypotheses (list-hypotheses derivation))
+ (parse-error
+ "define-derivation: expected remaining hypotheses ~a, but got ~a."
+ hypotheses (list-hypotheses derivation))
+ (if maybe-assignment
+ (begin
+ (hash-set!
+ *rules*
+ name
+ (cons `(,@(judgment-context conclusion)
+ ⊢
+ ,(if (eq? kind 'type)
+ (list 'type (just maybe-assignment))
+ (list ':
+ (just maybe-assignment)
+ (third (judgment-content conclusion)))))
+ hypotheses))
+ (hash-set!
+ *definition-rules*
+ name
+ (cons `(,@(judgment-context conclusion)
+ ⊢
+ ,(if (eq? kind 'type)
+ (list '≐
+ (just maybe-assignment)
+ (second (judgment-content conclusion)))
+ (list '≐
+ (just maybe-assignment)
+ (second (judgment-content conclusion))
+ (third (judgment-content conclusion)))))
+ hypotheses))
+ (hash-set! (if (eq? kind 'type) *types* *constructors*)
+ (just (pre-destruct 'type (just maybe-assignment)))
+ (rule-ref name))
+ '(values)
+ )
+ (begin
+ (hash-set! *rules* name (cons conclusion hypotheses))
+ '(values))))))
+
+;; NOTE: A derivation must have at least one derivation rule (can't derive a
+;; statement out of nothing).
+(define-syntax define-derivation
+ (syntax-rules (:= ⊢ type :)
+ ((_ name ((Γ ⊢ (:= a (type expr)))
+ hypothesis ...)
+ (rule-1 arg-1 ...)
+ (rule-2 arg-2 ...)
+ ...)
+ (define-derivation% name type (just . a) (Γ ⊢ (type expr)) (hypothesis ...)
+ (rule-1 arg-1 ...)
+ (rule-2 arg-2 ...)
+ ...))
+ ((_ name ((Γ ⊢ (:= a (: b B)))
+ hypothesis ...)
+ (rule-1 arg-1 ...)
+ (rule-2 arg-2 ...)
+ ...)
+ (define-derivation% name element (just . a) (Γ ⊢ (: b B)) (hypothesis ...)
+ (rule-1 arg-1 ...)
+ (rule-2 arg-2 ...)
+ ...))
+ ((_ name (conclusion hypothesis ...)
+ (rule-1 arg-1 ...)
+ (rule-2 arg-2 ...)
+ ...)
+ (define-derivation% name #f #f conclusion (hypothesis ...)
+ (rule-1 arg-1 ...)
+ (rule-2 arg-2 ...)
+ ...))))
+
+(define (define-derivation-list name derivation)
+ (let ((tree (derivation-tree derivation)))
+ `(define-derivation ,name
+ (,(car tree) ,@(list-hypotheses derivation))
+ ,@(reverse (derivation-steps derivation)))))
projects / vouivre.git / commitdiff