prototype fix for pfunc breaker variable names

tnelson · Mar 14, 2024 · 162c711 · 162c711
1 parent 4db3f8e
commit 162c711
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 18 deletions.
diff --git a/forge/breaks.rkt b/forge/breaks.rkt
@@ -728,21 +728,20 @@
                 (define (pfuncformula rllst quantvarlst)
                   (cond
                     [(empty? (rest (rest rllst)))
-                     ; Note: the value of "a" defined here will not actually be reflected in what the
-                     ; macro below produces. (TODO: why?)
-                     ;; all/info macro uses 'v0 with QUOTING?
-                     (define foo (let ([a (gensym)])
-                       (printf "gs case 1: ~a~n" a)
-                       (@all/info (@just-location-info loc) ([a (first rllst)])
-                                  (@lone (pfuncformulajoin (cons a quantvarlst)))))
-                       )
-                     (printf "foo: ~a~n" foo)
-                     foo
-                     ]
-                    [else (let ([a (gensym)])
-                            (printf "gs case 2: ~a~n" a)
-                            (@all/info (@just-location-info loc) ([a (first rllst)])
-                                       (pfuncformula (rest rllst) (cons a quantvarlst))))]))
+                     (let* ([var-id (gensym 'pfunc)]
+                            [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+                       (@quantified-formula (@just-location-info loc) 'all
+                                            (list (cons a (first rllst)))
+                                            (@lone (pfuncformulajoin (cons a quantvarlst)))))]
+                    ;(@all/info (@just-location-info loc) ([a (first rllst)])
+                    ;           (@lone (pfuncformulajoin (cons a quantvarlst)))))]
+                    [else (let* ([var-id (gensym 'pfunc)]
+                                 [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+                            ;(@all/info (@just-location-info loc) ([a (first rllst)])
+                            ;           (pfuncformula (rest rllst) (cons a quantvarlst))
+                            (@quantified-formula (@just-location-info loc) 'all
+                                                 (list (cons a (first rllst)))
+                                                 (pfuncformula (rest rllst) (cons a quantvarlst))))]))
                 (define pf-fmla (pfuncformula rel-list (list)))
                 (printf "pfunc breaker: ~a~n" pf-fmla)
                 (define formulas (set pf-fmla))

diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt
@@ -829,13 +829,13 @@
   (for ([e (in-list (map cdr decls))])
     (unless (node/expr? e)
       (raise-forge-error #:msg (format "~a quantifier expected an expression for domain, got ~a" quantifier e)
-                         #:context e))
+                         #:context (if (node? e) e info)))
     (unless (equal? (node/expr-arity e) 1)
       (raise-forge-error #:msg (format "~a quantifier expected an arity-1 expression for domain, got ~a" quantifier e)
-                         #:context e)))
+                         #:context (if (node? e) e info))))
   (unless (or (node/formula? formula) (equal? #t formula))
     (raise-forge-error #:msg (format "~a quantifier body expected a formula, got ~a" quantifier formula)
-                       #:context formula))
+                       #:context (if (node? formula) formula info)))
   (node/formula/quantified info quantifier decls formula))
 
 ;(struct node/formula/higher-quantified node/formula (quantifier decls formula))