suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Added untested macro for defining inferrence rules

Browse Source
This commit is contained in:
William J. Bowman 2015-01-21 01:37:50 -05:00
parent b57f2d4a85
commit 9ec162b079
1 changed files with 43 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
example.rkt
View File

@ -380,16 +380,52 @@
(has-type g e2 t1) (has-type g e2 t1)
(has-type g (app e1 e2) t2))))) (has-type g (app e1 e2) t2)))))
(require (for-syntax syntax/parse racket))
(begin-for-syntax
(define-syntax-class dash
(pattern x:id
#:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
"Invalid dash"))
(define-syntax-class decl (pattern (x:id (~literal :) t:id)))
(define-syntax-class inferrence-rule
(pattern (d:decl ...
x*:expr ...
line:dash lab:id
(name:id y* ...))
#:with rule #'(lab : (forall* d ...
(->* x* ... (name y* ...)))))))
(define-syntax (define-relation syn)
(syntax-parse syn
[(_ (n:id types*:id ...) rules:inferrence-rule ...)
#:fail-unless (andmap (curry equal? (length (syntax->datum #'(types* ...))))
(map length (syntax->datum #'((rules.y* ...)
...))))
"Mismatch between relation declared and relation definition"
#:fail-unless (andmap (curry equal? (syntax->datum #'n))
(syntax->datum #'(rules.name ...)))
"Mismatch between relation declared name and result of inference rule"
#'(data n : (->* types* ... Type)
rules.rule ...)]))
#| #|
;; Gee, it would be great if I could write those rules more naturally. ;; Gee, it would be great if I could write those rules more naturally.
;; Suppose like: ;; Suppose like:
(define-type-system (has-type gamma term type) (define-relation (has-type gamma term type)
[------------------------ T-Unit [(g : gamma)
(has-type g unitv Unit)] ------------------------ T-Unit
[(== (maybe type) (lookup-gamma g x) (some type t)) (has-type g unitv Unit)]
------------------------ T-Var
(has-type g (tvar x) t)] [(g : gamma) (x : var) (t : type)
...) (== (maybe type) (lookup-gamma g x) (some type t))
------------------------ T-Var
(has-type g (tvar x) t)]
[]
)
And have each free-identifier automagically forall quantified And have each free-identifier automagically forall quantified
(might require some tricky type inference). (might require some tricky type inference).