Set hybrid-core to default; converted Δ to dict
* Hybrid core now used by default in this branch. * Converted Δ to a Racket dictionary, started converting Δ abstractions to use dictionary.
This commit is contained in:
William J. Bowman
parent
c99b44bc09
commit
b318617f0e
|
|
@ -5,7 +5,7 @@
|
|||
racket/syntax
|
||||
syntax/parse
|
||||
(for-template
|
||||
(only-in "curnel/redex-lang.rkt"
|
||||
(only-in "curnel/hybrid-lang.rkt"
|
||||
cur-expand)))
|
||||
|
||||
(provide cur-match)
|
||||
|
|
@ -17,7 +17,7 @@
|
|||
[pattern body] ...)])))
|
||||
|
||||
(require
|
||||
(rename-in "curnel/redex-lang.rkt" [provide -provide])
|
||||
(rename-in "curnel/hybrid-lang.rkt" [provide -provide])
|
||||
(only-in racket/base eof)
|
||||
(for-syntax 'extra)
|
||||
'extra)
|
||||
|
|
@ -27,5 +27,5 @@
|
|||
(except-out
|
||||
(all-from-out
|
||||
'extra
|
||||
"curnel/redex-lang.rkt")
|
||||
"curnel/hybrid-lang.rkt")
|
||||
-provide))
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
#lang racket/base
|
||||
|
||||
;; A mostly Redex core, with parts written in Racket for performance reasons
|
||||
;; TODO: Move tests into common place to use in both Redex cores.
|
||||
|
||||
(require
|
||||
racket/dict
|
||||
racket/function
|
||||
racket/list
|
||||
redex/reduction-semantics)
|
||||
|
||||
(provide
|
||||
|
|
@ -13,33 +13,21 @@
|
|||
|
||||
(set-cache-size! 10000)
|
||||
|
||||
;; Test suite setup.
|
||||
(module+ test
|
||||
(require
|
||||
rackunit
|
||||
(only-in racket/set set=?))
|
||||
(define-syntax-rule (check-holds (e ...))
|
||||
(check-true
|
||||
(judgment-holds (e ...))))
|
||||
(define-syntax-rule (check-not-holds (e ...))
|
||||
(check-false
|
||||
(judgment-holds (e ...))))
|
||||
(define-syntax-rule (check-equiv? e1 e2)
|
||||
(check (default-equiv) e1 e2))
|
||||
(define-syntax-rule (check-not-equiv? e1 e2)
|
||||
(check (compose not (default-equiv)) e1 e2)))
|
||||
(define-language base
|
||||
(dict ::= any))
|
||||
;; TODO: More abstractions for Redex dictionaries.
|
||||
|
||||
(define make-dict make-immutable-hash)
|
||||
|
||||
#| ttL is the core language of Cur. Very similar to TT (Idirs core) and Luo's UTT. Surface
|
||||
| langauge should provide short-hand, such as -> for non-dependent function types, and type
|
||||
| inference.
|
||||
|#
|
||||
(define-language ttL
|
||||
(define-extended-language ttL base
|
||||
(i j k ::= natural)
|
||||
(U ::= (Unv i))
|
||||
(t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e) (elim D U))
|
||||
;; Δ (signature). (inductive-name : type ((constructor : type) ...))
|
||||
;; NB: Δ is a map from a name x to a pair of it's type and a map of constructor names to their types
|
||||
(Δ ::= ∅ (Δ (D : t ((c : t) ...))))
|
||||
(Δ ::= dict)
|
||||
(D x c ::= variable-not-otherwise-mentioned)
|
||||
#:binding-forms
|
||||
(λ (x : t) e #:refers-to x)
|
||||
|
|
@ -49,7 +37,17 @@
|
|||
(define t? (redex-match? ttL t))
|
||||
(define e? (redex-match? ttL e))
|
||||
(define U? (redex-match? ttL U))
|
||||
(define Δ? (redex-match? ttL Δ))
|
||||
|
||||
;; TODO: Constracts
|
||||
;; An inductive-decl contains the type of the type being declared,
|
||||
;; a t?, and a dictionary of constructor names (x?) mapped to their
|
||||
;; types (t?)
|
||||
(define-struct inductive-decl (type constr-dict))
|
||||
|
||||
;; A Δ is a dict mapping names x? to inductive-decl?
|
||||
(define Δ? dict?)
|
||||
(define make-empty-Δ make-dict)
|
||||
(define empty-Δ? dict-empty?)
|
||||
|
||||
;;; ------------------------------------------------------------------------
|
||||
;;; Universe typing
|
||||
|
|
@ -94,61 +92,73 @@
|
|||
;;; ------------------------------------------------------------------------
|
||||
;;; Primitive Operations on signatures Δ (those operations that do not require contexts)
|
||||
|
||||
;;; TODO: Might be worth maintaining the above bijection between Δ and maps for performance reasons
|
||||
|
||||
;; TODO: This is doing too many things
|
||||
;; NB: Depends on clause order
|
||||
;; TODO: Maybe shouldn't fall back, but maintains redex-core interface.
|
||||
;; Get the type of x as declared in Δ, as either a constructor or an inductive type
|
||||
(define-metafunction ttL
|
||||
Δ-ref-type : Δ x -> t or #f
|
||||
[(Δ-ref-type ∅ x) #f]
|
||||
[(Δ-ref-type (Δ (x : t any)) x) t]
|
||||
[(Δ-ref-type (Δ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t]
|
||||
[(Δ-ref-type (Δ (x_0 : t_0 any)) x) (Δ-ref-type Δ x)])
|
||||
[(Δ-ref-type Δ x)
|
||||
,(cond
|
||||
[(dict-ref (term Δ) (term x) (thunk #f))
|
||||
=> inductive-decl-type]
|
||||
[else (term (Δ-ref-constructor-type Δ foo x))])])
|
||||
|
||||
;; Get the type of a constructor x in the inductive declaration Δ
|
||||
;; TODO: Doesn't need x_D anymore
|
||||
(define-metafunction ttL
|
||||
Δ-ref-constructor-type : Δ x x -> t or #f
|
||||
[(Δ-ref-constructor-type Δ x_D x)
|
||||
,(cond
|
||||
[(for/or ([(D idecl) (in-dict (term Δ))])
|
||||
(let ([constr-dict (inductive-decl-constr-dict idecl)])
|
||||
(and (dict-has-key? constr-dict (term x)) constr-dict)))
|
||||
=>
|
||||
(curryr dict-ref (term x))]
|
||||
[else #f])])
|
||||
|
||||
;; Add an inductive declaration to Δ
|
||||
(define-metafunction ttL
|
||||
Δ-set : Δ x t ((x : t) ...) -> Δ
|
||||
[(Δ-set Δ x t any) (Δ (x : t any))])
|
||||
[(Δ-set Δ x t any)
|
||||
,(dict-set
|
||||
(term Δ)
|
||||
(term x)
|
||||
(inductive-decl
|
||||
(term t)
|
||||
(for/fold ([d (make-dict)])
|
||||
([constr-decl (term any)])
|
||||
(dict-set d (first constr-decl) (third constr-decl)))))])
|
||||
|
||||
;; Merge two inductive declarations
|
||||
(define-metafunction ttL
|
||||
Δ-union : Δ Δ -> Δ
|
||||
[(Δ-union Δ ∅) Δ]
|
||||
[(Δ-union Δ_2 (Δ_1 (x : t any)))
|
||||
((Δ-union Δ_2 Δ_1) (x : t any))])
|
||||
[(Δ-union Δ_1 Δ_2)
|
||||
,(for/fold ([d (term Δ_1)])
|
||||
([(k v) (in-dict (term Δ_2))])
|
||||
(dict-set d k v (thunk (error 'curnel "~a is already declared in ~a" k d))))])
|
||||
|
||||
;; Returns the inductively defined type that x constructs
|
||||
;; NB: Depends on clause order
|
||||
(define-metafunction ttL
|
||||
Δ-key-by-constructor : Δ x -> x
|
||||
[(Δ-key-by-constructor (Δ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c)
|
||||
x]
|
||||
[(Δ-key-by-constructor (Δ (x_1 : t_1 any)) x)
|
||||
(Δ-key-by-constructor Δ x)])
|
||||
[(Δ-key-by-constructor Δ x_c)
|
||||
,(for/or ([(k v) (in-dict (term Δ))])
|
||||
(and (dict-has-key? (inductive-decl-constr-dict v)) k))])
|
||||
|
||||
;; Returns the constructor map for the inductively defined type x_D in the signature Δ
|
||||
(define-metafunction ttL
|
||||
Δ-ref-constructor-map : Δ x -> ((x : t) ...) or #f
|
||||
;; NB: Depends on clause order
|
||||
[(Δ-ref-constructor-map ∅ x_D) #f]
|
||||
[(Δ-ref-constructor-map (Δ (x_D : t_D any)) x_D)
|
||||
any]
|
||||
[(Δ-ref-constructor-map (Δ (x_1 : t_1 any)) x_D)
|
||||
(Δ-ref-constructor-map Δ x_D)])
|
||||
|
||||
;; TODO: Should not use Δ-ref-type
|
||||
(define-metafunction ttL
|
||||
Δ-ref-constructor-type : Δ x x -> t
|
||||
[(Δ-ref-constructor-type Δ x_D x_ci)
|
||||
(Δ-ref-type Δ x_ci)])
|
||||
[(Δ-ref-constructor-map Δ x_D)
|
||||
,(cond
|
||||
[(dict-ref (term Δ) (term x_D) (thunk #f)) =>
|
||||
(lambda (x)
|
||||
(for/list ([(k v) (inductive-decl-constr-dict x)])
|
||||
`(,k : ,v)))]
|
||||
[else #f])])
|
||||
|
||||
;; Get the list of constructors for the inducitvely defined type x_D
|
||||
;; NB: Depends on clause order
|
||||
(define-metafunction ttL
|
||||
Δ-ref-constructors : Δ x -> (x ...) or #f
|
||||
[(Δ-ref-constructors ∅ x_D) #f]
|
||||
[(Δ-ref-constructors (Δ (x_D : t_D ((x : t) ...))) x_D)
|
||||
(x ...)]
|
||||
[(Δ-ref-constructors (Δ (x_1 : t_1 any)) x_D)
|
||||
(Δ-ref-constructors Δ x_D)])
|
||||
[(Δ-ref-constructors Δ x_D)
|
||||
,(dict-keys (inductive-decl-constr-dict (dict-ref (term Δ) (term x_D))))])
|
||||
|
||||
;; NB: Depends on clause order
|
||||
(define-metafunction ttL
|
||||
|
|
@ -182,13 +192,11 @@
|
|||
;; TODO: Might be worth it to actually maintain the above bijections, for performance reasons.
|
||||
|
||||
;; Return the parameters of x_D as a telescope Ξ
|
||||
;; TODO: Define generic traversals of Δ and Γ ?
|
||||
(define-metafunction tt-ctxtL
|
||||
Δ-ref-parameter-Ξ : Δ x -> Ξ
|
||||
[(Δ-ref-parameter-Ξ (Δ (x_D : (in-hole Ξ U) any)) x_D)
|
||||
Ξ]
|
||||
[(Δ-ref-parameter-Ξ (Δ (x_1 : t_1 any)) x_D)
|
||||
(Δ-ref-parameter-Ξ Δ x_D)])
|
||||
[(Δ-ref-parameter-Ξ Δ x_D)
|
||||
Ξ
|
||||
(where (in-hole Ξ U) (Δ-ref-type Δ x_D))])
|
||||
|
||||
;; Applies the term t to the telescope Ξ.
|
||||
;; TODO: Test
|
||||
|
|
@ -390,7 +398,7 @@
|
|||
(define E? (redex-match? tt-redL E))
|
||||
(define v? (redex-match? tt-redL v))
|
||||
|
||||
(define current-Δ (make-parameter (term ∅)))
|
||||
(define current-Δ (make-parameter (make-empty-Δ)))
|
||||
(define tt-->
|
||||
(reduction-relation tt-redL
|
||||
(--> (in-hole E ((λ (x : t_0) t_1) t_2))
|
||||
|
|
@ -532,25 +540,29 @@
|
|||
#:mode (wf I I)
|
||||
#:contract (wf Δ Γ)
|
||||
|
||||
[----------------- "WF-Empty"
|
||||
(wf ∅ ∅)]
|
||||
[(side-condition ,(empty-Δ? (term Δ)))
|
||||
----------------- "WF-Empty"
|
||||
(wf Δ ∅)]
|
||||
|
||||
[(type-infer Δ Γ t t_0)
|
||||
(wf Δ Γ)
|
||||
----------------- "WF-Var"
|
||||
(wf Δ (Γ x : t))]
|
||||
|
||||
[(wf Δ ∅)
|
||||
[(where x_D ,(dict-iterate-first (term Δ_1)))
|
||||
(where t_D (Δ-ref-type Δ_1 x_D))
|
||||
(where (x_c ...) (Δ-ref-constructors Δ_1 x_D))
|
||||
(where ((name t_c (in-hole Ξ (in-hole Θ x_D*))) ...)
|
||||
((Δ-ref-type Δ_1 x_c) ...))
|
||||
(where Δ ,(dict-remove (term Δ_1) (term x_D)))
|
||||
(wf Δ ∅)
|
||||
(type-infer Δ ∅ t_D U_D)
|
||||
(type-infer Δ (∅ x_D : t_D) t_c U_c) ...
|
||||
;; NB: Ugh this should be possible with pattern matching alone ....
|
||||
(side-condition ,(map (curry equal? (term x_D)) (term (x_D* ...))))
|
||||
(side-condition (positive* x_D (t_c ...)))
|
||||
----------------- "WF-Inductive"
|
||||
(wf (Δ (x_D : t_D
|
||||
;; Checks that a constructor for x actually produces an x, i.e., that
|
||||
;; the constructor is well-formed.
|
||||
((x_c : (name t_c (in-hole Ξ (in-hole Θ x_D*)))) ...))) ∅)])
|
||||
(wf Δ_1 ∅)])
|
||||
|
||||
;; TODO: Bi-directional and inference?
|
||||
;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
|
||||
|
|
@ -605,3 +617,12 @@
|
|||
(equivalent Δ t t_0)
|
||||
----------------- "DTR-Check"
|
||||
(type-check Δ Γ e t)])
|
||||
|
||||
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
(define-term Δt (Δ-set ,(make-empty-Δ) True Type ((T : True))))
|
||||
(check-false
|
||||
(judgment-holds (type-check ,(make-empty-Δ) ∅ T True)))
|
||||
(check-true
|
||||
(judgment-holds (type-check Δt ∅ T True))))
|
||||
|
|
|
|||
493
cur-lib/cur/curnel/hybrid-lang.rkt
Normal file
493
cur-lib/cur/curnel/hybrid-lang.rkt
Normal file
|
|
@ -0,0 +1,493 @@
|
|||
#lang racket/base
|
||||
;; This module just provide module language sugar over the redex model.
|
||||
|
||||
(require
|
||||
"hybrid-core.rkt"
|
||||
redex/reduction-semantics
|
||||
racket/provide-syntax
|
||||
(for-syntax
|
||||
(except-in racket import)
|
||||
syntax/parse
|
||||
racket/syntax
|
||||
(except-in racket/provide-transform export)
|
||||
racket/require-transform
|
||||
"hybrid-core.rkt"
|
||||
redex/reduction-semantics))
|
||||
(provide
|
||||
;; Basic syntax
|
||||
for-syntax
|
||||
only-in
|
||||
except-in
|
||||
all-defined-out
|
||||
rename-in
|
||||
rename-out
|
||||
prefix-out
|
||||
prefix-in
|
||||
submod
|
||||
#%module-begin
|
||||
(rename-out
|
||||
[dep-module+ module+]
|
||||
[dep-provide provide]
|
||||
[dep-require require]
|
||||
|
||||
[dep-lambda lambda]
|
||||
[dep-lambda λ]
|
||||
[dep-app #%app]
|
||||
|
||||
[dep-forall forall]
|
||||
[dep-forall ∀]
|
||||
|
||||
[dep-inductive data]
|
||||
|
||||
[dep-elim elim]
|
||||
|
||||
[dep-top #%top]
|
||||
[dep-top-interaction #%top-interaction]
|
||||
|
||||
; [dep-datum #%datum]
|
||||
[dep-define define]
|
||||
[dep-void void])
|
||||
begin
|
||||
Type
|
||||
;; DYI syntax extension
|
||||
define-syntax
|
||||
begin-for-syntax
|
||||
define-for-syntax
|
||||
syntax-case
|
||||
syntax-rules
|
||||
define-syntax-rule
|
||||
(for-syntax
|
||||
(all-from-out syntax/parse)
|
||||
(all-from-out racket)
|
||||
(all-from-out racket/syntax)
|
||||
cur->datum
|
||||
cur-expand
|
||||
type-infer/syn
|
||||
type-check/syn?
|
||||
normalize/syn
|
||||
step/syn
|
||||
cur-equal?))
|
||||
|
||||
(begin-for-syntax
|
||||
;; TODO: Gamma and Delta seem to get reset inside a module+
|
||||
(define gamma
|
||||
(make-parameter
|
||||
(term ∅)
|
||||
(lambda (x)
|
||||
(unless (Γ? x)
|
||||
(error 'core-error "We built a bad term environment ~s" x))
|
||||
x)))
|
||||
|
||||
(define delta
|
||||
(make-parameter
|
||||
(make-empty-Δ)
|
||||
(lambda (x)
|
||||
(unless (Δ? x)
|
||||
(error 'core-error "We built a bad inductive declaration ~s" x))
|
||||
x)))
|
||||
|
||||
;; These should be provided by core, so details of envs can be hidden.
|
||||
(define (extend-Γ/term env x t)
|
||||
(term (Γ-set ,(env) ,x ,t)))
|
||||
|
||||
(define (extend-Γ/term! env x t) (env (extend-Γ/term env x t)))
|
||||
|
||||
(define (extend-Γ/syn env x t)
|
||||
(extend-Γ/term env (syntax->datum x) (cur->datum t)))
|
||||
|
||||
(define (extend-Γ/syn! env x t) (env (extend-Γ/syn env x t)))
|
||||
|
||||
(define (extend-Δ/term env x t c*)
|
||||
(term (Δ-set ,(env) ,x ,t (,@c*))))
|
||||
|
||||
(define (extend-Δ/term! env x t c*)
|
||||
(env (extend-Δ/term env x t c*)))
|
||||
|
||||
(define (extend-Δ/syn env x t c*)
|
||||
(extend-Δ/term env (syntax->datum x) (cur->datum t)
|
||||
(for/list ([c (syntax->list c*)])
|
||||
(syntax-case c ()
|
||||
[(c : ct)
|
||||
(parameterize ([gamma (extend-Γ/syn gamma x t)])
|
||||
(term (,(syntax->datum #'c) : ,(cur->datum #'ct))))]))))
|
||||
|
||||
(define (extend-Δ/syn! env x t c*)
|
||||
(env (extend-Δ/syn env x t c*)))
|
||||
|
||||
(define subst? (list/c (listof x?) (listof e?)))
|
||||
(define bind-subst
|
||||
(make-parameter
|
||||
(list null null)
|
||||
(lambda (x)
|
||||
(unless (subst? x)
|
||||
(error 'core-error "We build a bad subst ~s" x))
|
||||
x)))
|
||||
|
||||
(define (add-binding/term! x t)
|
||||
(let ([vars (first (bind-subst))]
|
||||
[exprs (second (bind-subst))])
|
||||
(bind-subst (list (cons x vars) (cons t exprs)))))
|
||||
|
||||
(define (subst-bindings t)
|
||||
(term (subst-all ,t ,(first (bind-subst)) ,(second (bind-subst)))))
|
||||
|
||||
(define (type-infer/term t)
|
||||
(let ([t (judgment-holds (type-infer ,(delta) ,(gamma) ,(subst-bindings t) t_0) t_0)])
|
||||
(and (pair? t) (car t))))
|
||||
|
||||
(define (type-check/term? e t)
|
||||
(and (judgment-holds (type-check ,(delta) ,(gamma) ,(subst-bindings e) ,(subst-bindings t))) #t))
|
||||
|
||||
;; TODO: Blanket disarming is probably a bad idea.
|
||||
(define orig-insp (variable-reference->module-declaration-inspector (#%variable-reference)))
|
||||
(define (disarm syn) (syntax-disarm syn orig-insp))
|
||||
|
||||
;; Locally expand everything down to core forms.
|
||||
(define (core-expand syn)
|
||||
(disarm
|
||||
(local-expand
|
||||
syn
|
||||
'expression
|
||||
(append (syntax-e #'(term reduce subst-all dep-top #%app λ Π elim Unv #%datum void))))))
|
||||
|
||||
;; Only type-check at the top-level, to prevent exponential
|
||||
;; type-checking. Redex is expensive enough.
|
||||
(define inner-expand? (make-parameter #f))
|
||||
|
||||
;; Reifiy cur syntax into curnel datum
|
||||
(define (cur->datum syn)
|
||||
;; Main loop; avoid type
|
||||
(define reified-term
|
||||
;; TODO: This results in less good error messages. Add an
|
||||
;; algorithm to find the smallest ill-typed term.
|
||||
(parameterize ([inner-expand? #t])
|
||||
(let cur->datum ([syn syn])
|
||||
(syntax-parse (core-expand syn)
|
||||
#:literals (term reduce #%app subst-all)
|
||||
#:datum-literals (elim Π λ : Unv)
|
||||
[x:id (syntax->datum #'x)]
|
||||
[(subst-all e _ _) (syntax->datum #'e)]
|
||||
[(reduce Δ e) (cur->datum #'e)]
|
||||
[(term e) (cur->datum #'e)]
|
||||
[(Unv i) (term (Unv ,(syntax->datum #'i)))]
|
||||
;; TODO: should really check that b is one of the binders
|
||||
;; Maybe make a syntax class for the binders, core forms,
|
||||
;; etc.
|
||||
[(b:id (x:id : t) e)
|
||||
(let* ([x (syntax->datum #'x)]
|
||||
[t (cur->datum #'t)]
|
||||
[e (parameterize ([gamma (extend-Γ/term gamma x t)])
|
||||
(cur->datum #'e))])
|
||||
(term (,(syntax->datum #'b) (,x : ,t) ,e)))]
|
||||
[(elim t1 t2)
|
||||
(let* ([t1 (cur->datum #'t1)]
|
||||
[t2 (cur->datum #'t2)])
|
||||
(term (elim ,t1 ,t2)))]
|
||||
[(#%app e1 e2)
|
||||
(term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
|
||||
(unless (or (inner-expand?) (type-infer/term reified-term))
|
||||
#;(printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma))
|
||||
(raise-syntax-error 'cur "term is ill-typed:" reified-term syn))
|
||||
reified-term)
|
||||
|
||||
(define (datum->cur syn t)
|
||||
(match t
|
||||
[(list (quote term) e)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(datum->cur syn e))]
|
||||
[(list (quote Unv) i)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(Type #,i))]
|
||||
[(list (quote Π) (list x (quote :) t) body)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(dep-forall (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
|
||||
[(list (quote λ) (list x (quote :) t) body)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(dep-lambda (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
|
||||
[(list (list (quote elim) t1) t2)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(dep-elim #,(datum->cur syn t1) #,(datum->cur syn t2)))]
|
||||
[(list e1 e2)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
(dep-app #,(datum->cur syn e1) #,(datum->cur syn e2)))]
|
||||
[_
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
#,(datum->syntax syn t))]))
|
||||
|
||||
(define (eval-cur syn)
|
||||
(term (reduce ,(delta) ,(subst-bindings (cur->datum syn)))))
|
||||
|
||||
(define (syntax->curnel-syntax syn)
|
||||
(quasisyntax/loc
|
||||
syn
|
||||
;; TODO: this subst-all should be #,(subst-bindings (cur->datum syn)), but doesn't work
|
||||
(term (reduce #,(delta) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst)))))))
|
||||
|
||||
;; Reflection tools
|
||||
|
||||
(define (normalize/syn syn)
|
||||
(datum->cur
|
||||
syn
|
||||
(eval-cur syn)))
|
||||
|
||||
(define (step/syn syn)
|
||||
(datum->cur
|
||||
syn
|
||||
(term (step ,(delta) ,(subst-bindings (cur->datum syn))))))
|
||||
|
||||
;; Are these two terms equivalent in type-systems internal equational reasoning?
|
||||
(define (cur-equal? e1 e2)
|
||||
(and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
|
||||
|
||||
;; TODO: Document local-env
|
||||
(define (type-infer/syn syn #:local-env [env '()])
|
||||
(parameterize ([gamma (for/fold ([gamma (gamma)])
|
||||
([(x t) (in-dict env)])
|
||||
(extend-Γ/syn (thunk gamma) x t))])
|
||||
(let ([t (type-infer/term (eval-cur syn))])
|
||||
(and t (datum->cur syn t)))))
|
||||
|
||||
(define (type-check/syn? syn type)
|
||||
(type-check/term? (eval-cur syn) (eval-cur type)))
|
||||
|
||||
;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
|
||||
;; expanded until expansion reaches a Curnel form, or one of the
|
||||
;; identifiers in ls.
|
||||
(define (cur-expand syn . ls)
|
||||
(disarm
|
||||
(local-expand
|
||||
syn
|
||||
'expression
|
||||
(append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-top))
|
||||
ls)))))
|
||||
|
||||
;; -----------------------------------------------------------------
|
||||
;; Require/provide macros
|
||||
|
||||
#| TODO NB XXX
|
||||
| This is code some of the most hacky awful code I've ever written. But it works. ish
|
||||
|#
|
||||
(begin-for-syntax
|
||||
(define envs (list #'(void)))
|
||||
|
||||
(define (cur-identifier-bound? id)
|
||||
(let ([x (syntax->datum id)])
|
||||
(and (x? x)
|
||||
(or (term (Γ-ref ,(gamma) ,x))
|
||||
(term (Δ-ref-type ,(delta) ,x))))))
|
||||
|
||||
(define (filter-cur-exports syn modes)
|
||||
(partition (compose cur-identifier-bound? export-local-id)
|
||||
(apply append (map (lambda (e) (expand-export e modes))
|
||||
(syntax->list syn))))))
|
||||
(define-syntax extend-env-and-provide
|
||||
(make-provide-transformer
|
||||
(lambda (syn modes)
|
||||
(syntax-case syn ()
|
||||
[(_ e ...)
|
||||
(let-values ([(cur ~cur) (filter-cur-exports #'(e ...) modes)])
|
||||
#| TODO: Ignoring the built envs for now
|
||||
(set! envs (for/list ([e cur])
|
||||
(let* ([x (syntax->datum (export-local-id e))]
|
||||
[t (type-infer/term x)]
|
||||
[env (if (term (lookup ,(gamma) ,x)) #'gamma #'delta)])
|
||||
#`(extend-env/term! #,env #,(export-out-sym e) #,t))))
|
||||
|#
|
||||
~cur)]))))
|
||||
|
||||
(define-syntax (export-envs syn)
|
||||
(syntax-case syn ()
|
||||
[(_ gamma-out delta-out bind-out)
|
||||
(begin
|
||||
#`(begin-for-syntax
|
||||
(define gamma-out (term #,(gamma)))
|
||||
(define delta-out (term #,(delta)))
|
||||
(define bind-out '#,(bind-subst))))]))
|
||||
|
||||
;; TODO: This can only handle a single provide form, otherwise generates multiple *-out
|
||||
(define-syntax (dep-provide syn)
|
||||
(syntax-case syn ()
|
||||
[(_ e ...)
|
||||
(begin
|
||||
#| TODO NB:
|
||||
| Ignoring the built envs above, for now. The local-lift export seems to get executed before
|
||||
| the filtered environment is built.
|
||||
|#
|
||||
;; TODO: rename out will need to rename variables in gamma and ; delta.
|
||||
(syntax-local-lift-module-end-declaration
|
||||
#`(export-envs gamma-out delta-out bind-out))
|
||||
#`(provide (extend-env-and-provide e ...)
|
||||
(for-syntax gamma-out delta-out bind-out)))]))
|
||||
(begin-for-syntax
|
||||
(define out-gammas #`())
|
||||
(define out-deltas #`())
|
||||
(define out-binds #`())
|
||||
(define gn 0)
|
||||
(define sn 0)
|
||||
(define bn 0)
|
||||
(define (filter-cur-imports syn)
|
||||
(for/fold ([imports '()]
|
||||
[sources '()])
|
||||
([req-spec (syntax->list syn)])
|
||||
(let-values ([(more-imports more-sources) (expand-import req-spec)])
|
||||
(values (for/fold ([imports imports])
|
||||
([imp more-imports])
|
||||
(cond
|
||||
[(equal? (import-src-sym imp) 'gamma-out)
|
||||
(let ([new-id (format-id (import-orig-stx imp)
|
||||
"gamma-out~a" gn)])
|
||||
;; TODO: Fewer set!s
|
||||
;; TODO: Do not DIY gensym
|
||||
(set! gn (add1 gn))
|
||||
(set! out-gammas
|
||||
#`(#,@out-gammas (gamma (term (Γ-union
|
||||
,(gamma)
|
||||
,#,new-id)))))
|
||||
(cons (struct-copy import imp [local-id new-id])
|
||||
imports))]
|
||||
;; TODO: Many shared code between these two clauses
|
||||
[(equal? (import-src-sym imp) 'delta-out)
|
||||
(let ([new-id (format-id (import-orig-stx imp)
|
||||
"delta-out~a" sn)])
|
||||
;; TODO: Fewer set!s
|
||||
;; TODO: Do not DIY gensym
|
||||
(set! sn (add1 sn))
|
||||
(set! out-deltas
|
||||
#`(#,@out-deltas (delta (term (Δ-union
|
||||
,(delta)
|
||||
,#,new-id)))))
|
||||
(cons (struct-copy import imp [local-id new-id])
|
||||
imports))]
|
||||
;; TODO: Many shared code between these two clauses
|
||||
[(equal? (import-src-sym imp) 'bind-out)
|
||||
(let ([new-id (format-id (import-orig-stx imp)
|
||||
"bind-out~a" bn)])
|
||||
;; TODO: Fewer set!s
|
||||
;; TODO: Do not DIY gensym
|
||||
(set! bn (add1 bn))
|
||||
(set! out-binds
|
||||
#`(#,@out-binds (bind-subst (list (append
|
||||
(first #,new-id)
|
||||
(first (bind-subst)))
|
||||
(append
|
||||
(second #,new-id)
|
||||
(second (bind-subst)))))))
|
||||
(cons (struct-copy import imp [local-id new-id])
|
||||
imports))]
|
||||
[else (cons imp imports)]))
|
||||
(append sources more-sources))))))
|
||||
|
||||
(define-syntax extend-env-and-require
|
||||
(make-require-transformer
|
||||
(lambda (syn)
|
||||
(syntax-case syn ()
|
||||
[(_ e ...) (filter-cur-imports #'(e ...))]))))
|
||||
|
||||
;; TODO: rename in will need to rename variables in gamma and delta.
|
||||
(define-syntax (import-envs syn)
|
||||
(syntax-case syn ()
|
||||
[(_) #`(begin-for-syntax #,@out-gammas #,@out-deltas
|
||||
#,@out-binds)]))
|
||||
|
||||
(define-syntax (dep-require syn)
|
||||
(syntax-case syn ()
|
||||
[(_ e ...)
|
||||
#`(begin
|
||||
(require (extend-env-and-require e ...))
|
||||
(import-envs))]))
|
||||
|
||||
(define-syntax (dep-module+ syn)
|
||||
(syntax-case syn ()
|
||||
[(_ name body ...)
|
||||
#`(module+ name
|
||||
(begin-for-syntax
|
||||
(gamma (term #,(gamma)))
|
||||
(delta (term #,(delta)))
|
||||
(bind-subst '#,(bind-subst)))
|
||||
body ...)]))
|
||||
|
||||
;; -----------------------------------------------------------------
|
||||
;; Core wrapper macros
|
||||
;;
|
||||
;; TODO: Can these be simplified further?
|
||||
(define-syntax (dep-lambda syn)
|
||||
(syntax-case syn (:)
|
||||
[(_ (x : t) e)
|
||||
(syntax->curnel-syntax
|
||||
(quasisyntax/loc syn (λ (x : t) e)))]))
|
||||
|
||||
(define-syntax (dep-app syn)
|
||||
(syntax-case syn ()
|
||||
[(_ e1 e2)
|
||||
(syntax->curnel-syntax
|
||||
(quasisyntax/loc syn (#%app e1 e2)))]))
|
||||
|
||||
(define-syntax (dep-forall syn)
|
||||
(syntax-case syn (:)
|
||||
[(_ (x : t) e)
|
||||
(syntax->curnel-syntax
|
||||
(quasisyntax/loc syn (Π (x : t) e)))]))
|
||||
|
||||
(define-syntax (Type syn)
|
||||
(syntax-case syn ()
|
||||
[(_ i)
|
||||
(syntax->curnel-syntax
|
||||
(quasisyntax/loc syn (Unv i)))]
|
||||
[_ (quasisyntax/loc syn (Type 0))]))
|
||||
|
||||
(define-syntax (dep-inductive syn)
|
||||
(syntax-case syn (:)
|
||||
[(_ i : ti (x1 : t1) ...)
|
||||
(begin
|
||||
(extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
|
||||
#'(void))]))
|
||||
|
||||
(define-syntax (dep-elim syn)
|
||||
(syntax-case syn ()
|
||||
[(_ D T)
|
||||
(syntax->curnel-syntax
|
||||
(quasisyntax/loc syn (elim D T)))]))
|
||||
|
||||
(define-syntax-rule (dep-void) (void))
|
||||
|
||||
;; TODO: Not sure if this is the correct behavior for #%top
|
||||
(define-syntax (dep-top syn)
|
||||
(syntax-case syn ()
|
||||
[(_ . id)
|
||||
;; TODO NB FIXME: HACKS HACKS HACKS
|
||||
(let ([t (core-expand #'id)])
|
||||
(if (equal? (syntax->datum t) '(void))
|
||||
#'(void)
|
||||
(syntax->curnel-syntax t)))]))
|
||||
|
||||
(define-syntax (dep-top-interaction syn)
|
||||
(syntax-case syn ()
|
||||
[(_ . form)
|
||||
(begin
|
||||
;; TODO NB FIXME: HACKS
|
||||
#`(begin
|
||||
(export-envs gamma-out delta-out bind-out)
|
||||
(begin-for-syntax
|
||||
(define nm (map (lambda (x) (namespace-variable-value x #f (lambda x #t))) (namespace-mapped-symbols)))
|
||||
(bind-subst (first (memf subst? nm)))
|
||||
(gamma (first (memf Γ? nm)))
|
||||
(delta (first (memf Δ? nm))))
|
||||
form))]))
|
||||
|
||||
(define-syntax (dep-define syn)
|
||||
(syntax-parse syn
|
||||
[(_ id:id e)
|
||||
(let ([e (cur->datum #'e)]
|
||||
[id (syntax->datum #'id)])
|
||||
;; NB: Have to roll our own namespace rather than use built-in define so id is resolved at
|
||||
;; compile time in redex, and at runtime in racket.
|
||||
(extend-Γ/term! gamma id (type-infer/term e))
|
||||
(add-binding/term! id e)
|
||||
#'(void))]))
|
||||
Loading…
Reference in New Issue
Block a user