pretty-print-horn.rkt
#lang racket
(define tabsize (make-parameter 2))
(define (indent depth)
(make-string (* depth (tabsize)) #\space))
(define (add-newlines lines)
(add-between lines "\n"))
(define (surround start end body)
(append (list start) body (list end)))
(define (parens body)
(surround "(" ")" body))
;; formula, depth -> list string
(define (pretty-print-depth formula depth)
(list* (indent depth)
(match formula
[(list 'and conjuncts ...)
(parens
(list* "and"
"\n"
(flatten
(add-newlines
(map (lambda (x) (pretty-print-depth x (+ depth 1)))
conjuncts)))))]
[(list 'forall head body)
(parens
(list* "forall"
" "
(~a head)
"\n"
(pretty-print-depth body (+ depth 1))))]
[(list 'exists head body)
(parens
(list* "exists"
" "
(~a head)
"\n"
(pretty-print-depth body (+ depth 1))))]
[formula
(list (~a formula))])))
(define (pretty-print formula)
(apply string-append (pretty-print-depth formula 0)))
(define (cubify constraints pruning)
;; EHC -> (LinearEHC -> LinearEHC) -> List LinearEHC
(define (cubify-help formula path-builder)
(match formula
[(list 'and conjuncts ...)
(apply append (map (lambda (conjunct) (cubify-help conjunct path-builder)) conjuncts))]
[(list 'forall head body)
(cubify-help body (lambda (x) (path-builder (list 'forall head x))))]
[(list 'exists head body)
(cubify-help body (lambda (x) (path-builder (list 'exists head x))))]
['((true)) (if pruning '() '((true)))]
[formula (list (path-builder formula))]))
(cubify-help constraints identity))
(define input-file (make-parameter #f))
(define hypercube (make-parameter #f))
(define prune-true (make-parameter #f))
(command-line
#:program "pretty-print"
#:once-each
[("-i" "--input") file-name
"read input from file"
(input-file file-name)]
[("--hypercube") "print the constraints as a hyper cube"
(hypercube #t)]
[("--prune-true") "remove the constraints with head true"
(prune-true #t)])
(current-input-port (if (input-file)
(open-input-file (input-file))
(current-input-port)))
(define constraints (read))
(if (hypercube)
(for-each displayln (cubify constraints (prune-true)))
(displayln (pretty-print constraints)))