From bca0236687f01efb3a8dd037491abf77af07a6b4 Mon Sep 17 00:00:00 2001 From: Brant-Skywalker Date: Mon, 9 Sep 2024 20:01:24 -0500 Subject: [PATCH] precondition parsing --- export.rkt | 36 ++++++++++++++++++++++++++++++++---- 1 file changed, 32 insertions(+), 4 deletions(-) diff --git a/export.rkt b/export.rkt index 2ee23c0..e2b2e84 100644 --- a/export.rkt +++ b/export.rkt @@ -55,13 +55,41 @@ (define pre ((compose canonicalize remove-let) (dict-ref properties ':pre 'TRUE))) (define range-table (condition->range-table pre)) - (format "/* Preconditions: ~s */" range-table))] + (match range-table + [(hash-table (varname (list (interval lower upper lower_inc upper_inc))) ...) + (string-join + (map (lambda (varname lower upper lower_inc upper_inc) + (format "// ## PRE ~a: ~a, ~a, ~a, ~a\n" + varname lower upper lower_inc upper_inc)) + varname lower upper lower_inc upper_inc) + "")] + [(list (list varname (list (interval lower upper lower_inc upper_inc))) ...) + (string-join + (map (lambda (varname lower upper lower_inc upper_inc) + (format "// ## PRE ~a: ~a, ~a, ~a, ~a\n" + varname lower upper lower_inc upper_inc)) + varname lower upper lower_inc upper_inc) + "")]))] [(list 'FPCore name (list args ...) props ... body) (let-values ([(_ properties) (parse-properties props)]) (define pre ((compose canonicalize remove-let) (dict-ref properties ':pre 'TRUE))) (define range-table (condition->range-table pre)) - (format "/* Preconditions: ~s */" range-table))])) + (match range-table + [(hash-table (varname (list (interval lower upper lower_inc upper_inc))) ...) + (string-join + (map (lambda (varname lower upper lower_inc upper_inc) + (format "// ## PRE ~a: ~a, ~a, ~a, ~a\n" + varname lower upper lower_inc upper_inc)) + varname lower upper lower_inc upper_inc) + "")] + [(list (list varname (list (interval lower upper lower_inc upper_inc))) ...) + (string-join + (map (lambda (varname lower upper lower_inc upper_inc) + (format "// ## PRE ~a: ~a, ~a, ~a, ~a\n" + varname lower upper lower_inc upper_inc)) + varname lower upper lower_inc upper_inc) + "")]))])) (define (export-main argv stdin-port stdout-port) (define *lang* (make-parameter #f)) @@ -151,8 +179,8 @@ (unless (set-empty? unsupported) (raise-user-error (format "Sorry, the *.~a exporter does not support ~a" extension (string-join (map ~a unsupported) ", "))))) - (fprintf output-port "~a\n" (export core (format "ex~a" n))) - (when (equal? extension "c") (fprintf output-port "~a\n\n" c-pre))) + (when (equal? extension "c") (fprintf output-port "~a" c-pre)) + (fprintf output-port "~a\n" (export core (format "ex~a" n)))) (unless (export-ctx-bare ctx) (fprintf output-port (footer)))) (module+ main