From 4b1735d435b8e2c405efd2e7d3b73c989673512d Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Sat, 12 Jul 2014 21:00:04 +0200
Subject: [PATCH] First draft of redex core language.

---
 redex-core.rkt | 227 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 227 insertions(+)
 create mode 100644 redex-core.rkt

diff --git a/redex-core.rkt b/redex-core.rkt
new file mode 100644
index 0000000..6995886
--- /dev/null
+++ b/redex-core.rkt
@@ -0,0 +1,227 @@
+#lang racket/base
+
+(require
+  redex/reduction-semantics)
+
+#;(provide
+  define-inductive-type
+  match
+  define-fun
+  define-rec
+  lambda)
+
+
+;; References:
+;; http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
+;; https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf
+;; http://www.emn.fr/z-info/ntabareau/papers/universe_polymorphism.pdf
+
+;; Core language. Surface langauge should provide short-hand, such as
+;; -> for non-dependent function types, and type inference.
+(define-language dtracketL
+  (i ::= natural)
+  (U ::= Type (Unv i))
+  (x ::= variable-not-otherwise-mentioned)
+  ;; TODO: Having 2 binders is stupid.
+  (v ::= (Π (x : t) t) (λ (x : t) t) x U)
+  (t e ::= v (t t) (t : t)))
+
+(module+ test
+  (require (except-in rackunit check))
+  (check-true (redex-match? dtracketL U (term Type)))
+  (check-true (redex-match? dtracketL U (term (Unv 0))))
+  (check-true (redex-match? dtracketL e (term (λ (x_0 : (Unv 0)) x_0))))
+  (check-true (redex-match? dtracketL v (term (λ (x_0 : (Unv 0)) x_0))))
+  (check-true (redex-match? dtracketL t (term (λ (x_0 : (Unv 0)) x_0)))))
+
+;; 'A'
+;; Types of Universes
+;; Replace with sub-typing
+(define-judgment-form dtracketL
+  #:mode (unv-ok I O)
+  #:contract (unv-ok U U)
+
+  [-----------------
+   (unv-ok Type (Unv 0))]
+
+  [(where i_2 ,(sub1 (term i_0)))
+   (unv-ok (Unv i_2) (Unv i_3))
+   (where i_1 ,(add1 (term i_3)))
+   -----------------
+   (unv-ok (Unv i_0) (Unv i_1))])
+
+;; 'R'
+;; Kinding, I think
+(define-judgment-form dtracketL
+  #:mode (unv-kind I I O)
+  #:contract (unv-kind U U U)
+
+  [----------------
+   (unv-kind Type Type Type)]
+
+  [----------------
+   (unv-kind (Unv i) Type Type)]
+
+  [(where i_3 ,(max (term i_1) (term i_2)))
+   ----------------
+   (unv-kind (Unv i_1) (Unv i_2) (Unv i_3))])
+
+;; NB: Substitution is hard
+(define-metafunction dtracketL
+  subst : t x t -> t
+  [(subst x x t) t]
+  [(subst x_0 x t) x]
+  [(subst (Π (x : t_0) t_1) x t) (Π (x : t_0) t_1)]
+  [(subst (λ (x : t_0) t_1) x t) (λ (x : t_0) t_1)]
+  [(subst (Π (x_0 : t_0) t_1) x t) (Π (x_0 : t_0) (subst t_1 x t))]
+  [(subst (λ (x_0 : t_0) t_1) x t) (λ (x_0 : t_0) (subst t_1 x t))]
+  [(subst (e_0 e_1) x t) ((subst e_0 x t) (subst e_1 x t))])
+
+(define-extended-language dtracket-redL dtracketL
+  (E hole (E t) (E : t)))
+
+;; TODO: Congruence-closure instead of β
+(define ==β
+  (reduction-relation dtracket-redL
+    (==> ((Π (x : t_0) t_1) t_2)
+         (subst t_1 x t_2))
+    (==> ((λ (x : t) e_0) e_1)
+         (subst e_0 x e_1))
+    with
+    [(--> (in-hole E t_0) (in-hole E t_1))
+     (==> t_0 t_1)]))
+
+;; TODO: Bi-directional and inference?
+;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
+
+(define-extended-language dtracket-typingL dtracketL
+  (Γ ∅ (Γ x : t)))
+
+;; NB: Depends on clause order
+(define-metafunction dtracket-typingL
+  lookup : Γ x -> t or #f
+  [(lookup ∅ x) #f]
+  [(lookup (Γ x : t) x) t]
+  [(lookup (Γ x_0 : t_0) x_1) (lookup Γ x_1)])
+
+;; NB: Depends on clause order
+(define-metafunction dtracket-typingL
+  remove : Γ x -> Γ
+  [(remove ∅ x) ∅]
+  [(remove (Γ x : t) x) Γ]
+  [(remove (Γ x_0 : t_0) x_1) (remove Γ x_1)])
+
+;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
+#;(define-judgment-form dtracket-typingL
+  #:mode (synth I I O)
+  #:contract (synth Γ t t)
+
+  [(unv-ok U_0 U_1)
+   ----------------- ;; DTR-SAxiom
+   (synth ∅ U_0 U_1)]
+
+  [(synth (remove Γ x) t U)
+   ----------------- ;; DTR-SStart
+   (synth (Γ x : t) x t)]
+
+  [(synth Γ t t_1) (synth Γ t_0 U)
+   ----------------- ;; DTR-SWeakening
+   (synth (Γ x : t_0) t t_1)]
+
+  [(check Γ e t)
+   ----------------- ;; DTR-SSwitch
+   (synth Γ (e : t) t)]
+
+  [(synth Γ e_0 (Π (x : t_0) t_1))
+   (check Γ e_1 t_0)
+   ----------------- ;; DTR-Application
+   (synth Γ (e_0 e_1) (subst t_1 x e_1))])
+
+#;(define-judgment-form dtracket-typingL
+  #:mode (check I I I)
+  #:contract (check Γ t t)
+
+
+  [(check (Γ x : t_0) e t_1)
+   (synth Γ (Π (x : t_0) t_1) U)
+   ----------------- ;; DTR-CAbstraction
+   (check Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
+
+  [(synth Γ t_0 U_1)
+   (synth (Γ x : t_0) t U_2)
+   (unv-kind U_1 U_2 U)
+   ----------------- ;; DTR-CProduct
+   (check Γ (Π (x : t_0) t) U)]
+
+  [(check Γ t t_1) (synth Γ t_0 U)
+   ----------------- ;; DTR-CWeakening
+   (check (Γ x : t_0) t t_1)]
+
+  [(synth Γ e t_1)
+   (synth Γ t_0 U)
+   (side-condition ,(term (first (apply-reduction-relation* ==β (term t_0) (term t_1)))))
+   ----------------- ;; DTR-CConversion
+   (check Γ e t_0)]
+
+  [(synth Γ e t)
+   ----------------- ;; DTR-CSwitch
+   (check Γ e t)])
+
+(define-judgment-form dtracket-typingL
+  #:mode (types I I O)
+  #:contract (types Γ e t)
+
+  [(unv-ok U_0 U_1)
+   ----------------- ;; DTR-Axiom
+   (types ∅ U_0 U_1)]
+
+  [(where t (lookup Γ x))
+   (types (remove Γ x) t U)
+   ----------------- ;; DTR-SStart
+   (types Γ x t)]
+
+  [(types Γ t t_1) (types Γ t_0 U)
+   ----------------- ;; DTR-Weakening
+   (types (Γ x : t_0) t t_1)]
+
+  [(types Γ t_0 U_1)
+   (types (Γ x : t_0) t U_2)
+   (unv-kind U_1 U_2 U)
+   ----------------- ;; DTR-Product
+   (types Γ (Π (x : t_0) t) U)]
+
+  [(types Γ e_0 (Π (x : t_0) t_1))
+   (types Γ e_1 t_0)
+   ----------------- ;; DTR-Application
+   (types Γ (e_0 e_1) (subst t_1 x e_1))]
+
+  [(types (Γ x : t_0) e t_1)
+   (types Γ (Π (x : t_0) t_1) U)
+   ----------------- ;; DTR-Abstraction
+   (types Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
+
+  ;; This rule is no good for algorithmic checking; Redex infinitly
+  ;; searches it.
+  ;; Perhaps something closer to Zombies = type would be better.
+  #;[(types Γ e (in-hole E t))
+   (where t_0 (in-hole E t))
+   (where t_1 ,(car (apply-reduction-relation* ==β (term t_0))))
+   (types Γ t_1 U)
+   ----------------- ;; DTR-Conversion
+   (types Γ e t_1)])
+(module+ test
+  (check-true (judgment-holds (types ∅ Type (Unv 0))))
+  (check-true (judgment-holds (types (∅ x : Type) Type (Unv 0))))
+  (check-true (judgment-holds (types (∅ x : Type) x Type)))
+  (check-true (judgment-holds (types ((∅ x_0 : Type) x_1 : Type)
+                                     (Π (x_3 : x_0) x_1) Type)))
+
+  (check-true (judgment-holds (types ∅ (λ (x : Type) x) (Π (x : Type) Type)))))
+
+(define-judgment-form dtracket-typingL
+  #:mode (type-check I I I)
+  #:contract (type-check Γ e t)
+
+  [(types Γ e t)
+   ---------------
+   (type-check Γ e t)])