From 0b004d9ccbdd338e6ddf2cacb27e7f74a6093abc Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Sat, 12 Jul 2014 22:28:57 +0200
Subject: [PATCH] Added type reduction and infer-core
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
* Can't get β-equiv rule to work, so normalize types then check.
* Added infer-core, a closer to surface language on which to do
inference.
---
redex-core.rkt | 24 ++++++++++++++++++++++--
1 file changed, 22 insertions(+), 2 deletions(-)
diff --git a/redex-core.rkt b/redex-core.rkt
index 09511fb..00b1611 100644
--- a/redex-core.rkt
+++ b/redex-core.rkt
@@ -78,7 +78,7 @@
[(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)))
+ (E hole (E t) (λ (x : t) E) (Π (x : t) E)))
;; TODO: Congruence-closure instead of β
(define ==β
@@ -91,6 +91,18 @@
[(--> (in-hole E t_0) (in-hole E t_1))
(==> t_0 t_1)]))
+(define-metafunction dtracket-redL
+ reduce : e -> e
+ [(reduce e) ,(car (apply-reduction-relation* ==β (term e)))])
+(module+ test
+ (check-equal? (term (reduce Type)) (term Type))
+ (check-equal? (term (reduce ((λ (x : t) x) Type))) (term Type))
+ (check-equal? (term (reduce ((Π (x : t) x) Type))) (term Type))
+ (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) Type))))
+ (term (Π (x : t) Type)))
+ (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) x))))
+ (term (Π (x : t) x))))
+
;; TODO: Bi-directional and inference?
;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
@@ -200,9 +212,11 @@
----------------- ;; DTR-Abstraction
(types Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
+ ;; TODO: beta-equiv
;; This rule is no good for algorithmic checking; Redex infinitly
;; searches it.
;; Perhaps something closer to Zombies = type would be better.
+ ;; For now, reduce types
#;[(types Γ e (in-hole E t))
(where t_0 (in-hole E t))
(where t_1 ,(car (apply-reduction-relation* ==β (term t_0))))
@@ -224,4 +238,10 @@
[(types Γ e t)
---------------
- (type-check Γ e t)])
+ (type-check Γ e (reduce t))])
+
+;; Infer-core Language
+;; A relaxed core where annotation are optional.
+(define-extended-language dtracket-surfaceL dtracketL
+ (v ::= .... (λ x e) (Π x e))
+ (t e ::= .... (e : t)))