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

Fixed up inferrence rules

Browse Source
This commit is contained in:
William J. Bowman 2016-01-18 15:13:09 -05:00
parent 0e46da74ab
commit 22404dfe98
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 10 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
cur-lib/cur/olly.rkt
View File

@ -151,13 +151,11 @@
x:id x:id
#:when (regexp-match? #rx"-+" (symbol->string (syntax-e #'x))))) #:when (regexp-match? #rx"-+" (symbol->string (syntax-e #'x)))))
(define-syntax-class declaration
(pattern (x:id (~datum :) t)))
;; Alias syntax-classes with names for better error messages
(define-syntax-class hypothesis (define-syntax-class hypothesis
(pattern (x:id (~datum :) t))
(pattern (~not e:horizontal-line))) (pattern (~not e:horizontal-line)))
;; Alias syntax-classes with names for better error messages
(define-syntax-class rule-name (define-syntax-class rule-name
(pattern x:id)) (pattern x:id))
@ -186,26 +184,25 @@
(attribute rule-arg-count) (attribute rule-arg-count)
(attribute relation-arg-count)))) (attribute relation-arg-count))))
;; TODO: Automatically infer decl ... by binding all free identifiers? ;; TODO: Automatically infer hypotheses that are merely declarations by binding all free identifiers?
;; TODO: Automatically infer decl ... for meta-variables that are the ;; TODO: Automatically infer hypotheses as above for meta-variables that are the
;; same as bnf grammar. ;; same as bnf grammar, as a simple first case
(define-syntax-class (inferrence-rule name indices) (define-syntax-class (inferrence-rule name indices)
(pattern (d:declaration ... (pattern (h:hypothesis ...
(~peek (~not declaration)) #;line:horizontal-line
(~optional line:horizontal-line)
~! ~!
h:hypothesis ...
line:horizontal-line
#;(~optional line:horizontal-line)
lab:rule-name lab:rule-name
(~var t (conclusion name indices (attribute lab)))) (~var t (conclusion name indices (attribute lab))))
#:with constr-decl #:with constr-decl
#'(lab : (-> d ... h ... (t.name t.arg ...))) #'(lab : (-> h ... (t.name t.arg ...)))
;; TODO: convert meta-vars such as e1 to e_1 ;; TODO: convert meta-vars such as e1 to e_1
#:attr latex #:attr latex
(format (format
"\\inferrule~n{~a}~n{~a}" "\\inferrule~n{~a}~n{~a}"
(string-trim (string-trim
(for/fold ([str ""]) (for/fold ([str ""])
;; TODO: Perhaps omit hypotheses that are merely delcarations of free variables
([hyp (syntax->datum #'(h ...))]) ([hyp (syntax->datum #'(h ...))])
(format "~a~a \\+" str hyp)) (format "~a~a \\+" str hyp))
" \\+" " \\+"