Cleaned up eliminator reduction and typing

Reorganized eliminator typing
Typing of eliminators is now entirely in metafunctions. It is easier to understand, and should lead to more efficient typing. Some of these functions should be exposed via reflection.
2015-10-02 17:02:48 -04:00 · 2015-10-01 17:45:37 -04:00 · 2015-10-01 16:54:21 -04:00 · 2015-10-01 14:42:30 -04:00 · 2015-10-01 13:09:28 -04:00 · 2015-10-01 10:41:56 -04:00
2 changed files with 590 additions and 517 deletions
--- a/curnel/redex-core.rkt
+++ b/curnel/redex-core.rkt
--- a/curnel/redex-lang.rkt
+++ b/curnel/redex-lang.rkt
@ -11,7 +11,7 @@
    racket/syntax
    (except-in racket/provide-transform export)
    racket/require-transform
-    (except-in "redex-core.rkt" remove)
+    "redex-core.rkt"
    redex/reduction-semantics))
 (provide
  ;; Basic syntax
@ -86,6 +86,7 @@
          (error 'core-error "We built a bad sigma ~s" x))
        x)))

+  ;; These should be provided by core, so details of envs can be hidden.
  (define (extend-Γ/term env x t)
    (term (,(env) ,x : ,t)))

@ -269,8 +270,8 @@
  (define (cur-identifier-bound? id)
    (let ([x (syntax->datum id)])
      (and (x? x)
-        (or (term (lookup-Γ ,(gamma) ,x))
-          (term (lookup-Σ ,(sigma) ,x))))))
+        (or (term (Γ-ref ,(gamma) ,x))
+          (term (Σ-ref-type ,(sigma) ,x))))))

  (define (filter-cur-exports syn modes)
    (partition (compose cur-identifier-bound? export-local-id)
@ -336,7 +337,7 @@
                       ;; TODO: Do not DIY gensym
                       (set! gn (add1 gn))
                       (set! out-gammas
-                             #`(#,@out-gammas (gamma (term (append-Γ
+                             #`(#,@out-gammas (gamma (term (Γ-union
                                                             ,(gamma)
                                                             ,#,new-id)))))
                       (cons (struct-copy import imp [local-id new-id])
@ -349,7 +350,7 @@
                       ;; TODO: Do not DIY gensym
                       (set! sn (add1 sn))
                       (set! out-sigmas
-                             #`(#,@out-sigmas (sigma (term (append-Σ
+                             #`(#,@out-sigmas (sigma (term (Σ-union
                                                             ,(sigma)
                                                             ,#,new-id)))))
                       (cons (struct-copy import imp [local-id new-id])
Author	SHA1	Message	Date
William J. Bowman	0d110dffaf	Cleaned up eliminator reduction and typing	2015-10-02 17:02:48 -04:00
William J. Bowman	fd455b7a07	Reorganized eliminator typing Typing of eliminators is now entirely in metafunctions. It is easier to understand, and should lead to more efficient typing. Some of these functions should be exposed via reflection.	2015-10-01 17:45:37 -04:00
William J. Bowman	bd2e06acce	Removed unused judgment	2015-10-01 16:54:21 -04:00
William J. Bowman	26e5e40ec6	Removed methods-for Finish reorganization of method type metafunctions	2015-10-01 14:42:30 -04:00
William J. Bowman	47460cf916	More work on organizing method types	2015-10-01 13:09:28 -04:00
William J. Bowman	e69920907d	Reorganizing eliminating typing	2015-10-01 10:41:56 -04:00
William J. Bowman	0ea4c0447b	Removed some Racket code; want this core Redexy	2015-10-01 10:30:52 -04:00
William J. Bowman	5d5ec00052	Comments on more reorg	2015-10-01 00:05:21 -04:00
William J. Bowman	bb86e4fabc	Replaced unnecessary patterns with any This simplifies reading, and should improve performance	2015-09-30 23:31:34 -04:00
William J. Bowman	1182c477dc	Reorganized context functions; style fixes * Reorganized, reimplemented, and renamed many functions related to contexts (telescopes Ξ and apply context Θ) * Moved some test suite stuff to the top * Various style fixes in comments, indentation and such	2015-09-30 23:19:45 -04:00
William J. Bowman	993e51eab9	Reorganizing code, removing explicit reductions * Reorganizing sections of code to be easier to read. Grouping by similar requirements in meta-functions, and trying to reduce dependencies between meta-functions. * Removed explicit reductions from various meta-functions. That should be handled by equivalence rules in type-checking.	2015-09-30 22:09:09 -04:00
William J. Bowman	0ff4474bcc	More check-equiv? tests * check-equiv? now uses default-equiv, for more extensibility * more tests now uses check-equiv?	2015-09-30 21:38:39 -04:00
William J. Bowman	9eca5d6222	Reindent and renaming * Renaming Σ and Γ methods to be named more like dictionary functions, since Σ and Γ are essentially maps. * Reindent various bits of code	2015-09-30 17:58:36 -04:00
William J. Bowman	e49cf0c425	fresh-x was broken, and wasn't helping	2015-09-30 17:37:52 -04:00
William J. Bowman	0647b19ee6	fresh-x when generating names; α-equiv testing * This commit breaks something, not sure why * Changed all uses of (where .... ,(variable-not-in )) to use (fresh-x) instead. * Defined check-equiv for testing modulo α-equivalence * Changed many check-equal? to check-equiv?. Remaining require splitting into separate tests, e.g., checking that judgment-form returns exactly 1 argument that is check-equiv? ...	2015-09-30 16:39:28 -04:00
William J. Bowman	e08d006aba	Moved Σ to core language, since elim is there.	2015-09-30 16:21:03 -04:00
William J. Bowman	2398bd1603	Renamed languages to reflect facts: cic to tt	2015-09-30 16:16:03 -04:00