Skip to content

Commit

Permalink
Add ability to save a _simplified_ derivation as Latex. (Used in paper.)
Browse files Browse the repository at this point in the history
  • Loading branch information
justinpombrio committed Apr 11, 2018
1 parent a21bb14 commit 07c382a
Showing 1 changed file with 16 additions and 6 deletions.
22 changes: 16 additions & 6 deletions sweet-t.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -187,16 +187,26 @@
(map (λ (rule) (Resugared-simplified-derivation (resugar lang rule ⊢)))
rules)))

(define (save-derivation deriv filename)
(let [[port (open-output-file filename #:exists 'replace)]]
(fprintf port "\\begin{prooftree}~n")
(derivation/latex deriv port)
(fprintf port "\\end{prooftree}~n")
(close-output-port port)))

; for saving a type rule to a .ps file
(define-syntax-rule (save-sugar-type-rules lang ⊢ rules)
(map (λ (rule)
(let* [[deriv (Resugared-rule (resugar lang rule ⊢))]
[filename (string-append (DsRule-name rule) ".tex")]
[port (open-output-file filename #:exists 'replace)]]
(fprintf port "\\begin{prooftree}~n")
(derivation/latex deriv port)
(fprintf port "\\end{prooftree}~n")
(close-output-port port)))
[filename (string-append (DsRule-name rule) ".tex")]]
(save-derivation deriv filename)))
rules))

(define-syntax-rule (save-sugar-simplified-derivations lang ⊢ rules)
(map (λ (rule)
(let* [[deriv (Resugared-simplified-derivation (resugar lang rule ⊢))]
[filename (string-append (DsRule-name rule) ".tex")]]
(save-derivation deriv filename)))
rules))

; render a derivation as latex
Expand Down

0 comments on commit 07c382a

Please sign in to comment.