Skip to content

Commit

Permalink
further progress, repair missing stxloc. todo: error in breakers.frg …
Browse files Browse the repository at this point in the history
…test
  • Loading branch information
tnelson committed Mar 14, 2024
1 parent 162c711 commit 70df030
Show file tree
Hide file tree
Showing 5 changed files with 49 additions and 37 deletions.
22 changes: 12 additions & 10 deletions forge/breaks.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -652,11 +652,18 @@

(define (funcformula rllst quantvarlst)
(cond
[(empty? (rest (rest rllst)))
(let ([a (gensym)])
(@all/info (@just-location-info loc) ([a (first rllst)]) (@one (funcformulajoin (cons a quantvarlst)))))]
[else (let ([a (gensym)])
(@all/info (@just-location-info loc) ([a (first rllst)]) (funcformula (rest rllst) (cons a quantvarlst))))]))
[(empty? (rest (rest rllst)))
(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)))
(@one (funcformulajoin (cons a quantvarlst)))))]
[else
(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)))
(funcformula (rest rllst) (cons a quantvarlst))))]))
(define formulas (set (funcformula rel-list (list))))

; OLD CODE
Expand Down Expand Up @@ -733,17 +740,12 @@
(@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))

; OLD CODE
Expand Down
52 changes: 32 additions & 20 deletions forge/lang/expander.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@

(define-for-syntax (my-expand stx)
(define core-funcs-and-macros
(map (curry datum->syntax stx)
(map (lambda (s) (datum->syntax stx s stx))
'(^ * ~ + - & join
-> => implies ! not and or && || ifte iff <=>
= in ni != !in !ni is
Expand Down Expand Up @@ -159,14 +159,14 @@
(pattern ((~datum SigExt)
"extends"
name:QualNameClass)
#:attr symbol #'#:extends
#:attr value #'name.name)
#:attr symbol (syntax/loc this-syntax #:extends)
#:attr value (syntax/loc this-syntax name.name))
(pattern ((~datum SigExt)
"in"
name:QualNameClass
(~seq (~seq "+" names:QualNameClass) ...))
#:attr symbol #'#:in
#:attr value #'(raise "Extending with in not yet implemented.")))
#:attr symbol (syntax/loc this-syntax #:in)
#:attr value (syntax/loc this-syntax (raise "Extending with in not yet implemented."))))

; Mult : LONE-TOK | SOME-TOK | ONE-TOK | TWO-TOK
(define-syntax-class MultClass
Expand Down Expand Up @@ -209,8 +209,8 @@
#'(if (> (node/expr-arity expr) 1)
'set
'one))])
#'((names-c.names expr mult) ...))
#:attr names #'(names-c.names ...)))
(syntax/loc this-syntax ((names-c.names expr mult) ...)))
#:attr names (syntax/loc this-syntax (names-c.names ...))))

; Declaration of a comma-delimited list of variable declarations with expr and optional multiplicity
; DeclList : Decl
Expand Down Expand Up @@ -531,7 +531,8 @@
(~optional "exactly")
name:QualNameClass)
#:attr translate (begin (datum->syntax #'name
(list #'name.name)))))
(list #'name.name)
#'name))))

(define-syntax-class QualNameOrAtomOrAtomizedNumberClass
#:description "name, atom name, or number"
Expand Down Expand Up @@ -685,7 +686,9 @@
(~and op
(~or "in" "=" "<" ">" "<=" ">="
"is" "ni")))
#:attr symbol (datum->syntax #'op (op-symbol-to-operator (string->symbol (syntax->datum #'op))))))
#:attr symbol (datum->syntax #'op
(op-symbol-to-operator (string->symbol (syntax->datum #'op)))
#'op)))

; We don't overload (e.g.) <, but we don't want users to need to write (e.g.) "int<".
(define (op-symbol-to-operator sym)
Expand Down Expand Up @@ -723,7 +726,8 @@
(pattern ((~datum Quant) (~and q (~or "all" "no" "lone"
"some" "one" "two")))
#:attr symbol (datum->syntax #'q
(string->symbol (syntax->datum #'q))))
(string->symbol (syntax->datum #'q))
#'q))
(pattern ((~datum Quant) (~literal sum))
#:attr symbol (syntax/loc #'q sum-quant)))

Expand Down Expand Up @@ -832,7 +836,8 @@
(with-syntax ([relation-name relation-name-p1]
[relation-types (datum->syntax relation-types
(cons sig-name ;(syntax->datum sig-name)
(syntax->list relation-types)))]
(syntax->list relation-types))
relation-types)]
[relation-mult relation-mult]
[is-var relation-is-var])
(syntax/loc relation-name-p1 (relation (#:lang (get-check-lang)) relation-name relation-types #:is relation-mult #:is-var is-var))))))))]))
Expand Down Expand Up @@ -870,8 +875,10 @@
name:NameClass
decls:ParaDeclsClass
block:BlockClass)
(with-syntax ([decl (datum->syntax #'name (cons (syntax->datum #'name.name)
(syntax->list #'decls.pairs)))]
(with-syntax ([decl (datum->syntax #'name
(cons (syntax->datum #'name.name)
(syntax->list #'decls.pairs))
#'name)]
[block #'block])
(quasisyntax/loc stx (begin
(~? (raise (format "Prefixes not allowed: ~a" 'prefix)))
Expand Down Expand Up @@ -899,7 +906,8 @@
output-expr:ExprClass
body:ExprClass)
(with-syntax ([decl (datum->syntax #'name (cons (syntax->datum #'name.name)
(syntax->list #'decls.pairs)))]
(syntax->list #'decls.pairs))
#'name)]
; Parser "Expr" includes both expressions and formulas. Thus, disambiguate
; (e.g.) the "Expr" `one univ` into true expr and multiplicity in the expander;
; It's not the job of the `fun` macro to handle this. (Same for `pred`, etc.)
Expand Down Expand Up @@ -943,7 +951,8 @@
(~optional scope:ScopeClass)
(~optional bounds:BoundsClass))
(with-syntax ([cmd-type (datum->syntax #'cmd-type
(string->symbol (syntax->datum #'cmd-type)))]
(string->symbol (syntax->datum #'cmd-type))
#'cmd-type)]
[name #`(~? name.name #,(make-temporary-name stx))]
[preds #'(~? pred.name preds)])
#`(begin
Expand All @@ -968,7 +977,8 @@
(with-syntax ([name #`(~? name.name #,(make-temporary-name stx))]
[preds #'(~? pred.name preds)]
[expected (datum->syntax #'expected
(string->symbol (syntax->datum #'expected)))])
(string->symbol (syntax->datum #'expected))
#'expected)])
(syntax/loc stx
(test name (~? (~@ #:preds [preds]))
(~? (~@ #:scope scope.translate))
Expand Down Expand Up @@ -1009,8 +1019,8 @@
[qpd:QuantifiedPropertyDeclClass
;;;#:do [(printf "QuantifiedPropertyDeclClass.PropExprs: ~a~n" (syntax->datum #'qpd.prop-exprs))]
(with-syntax*
( [(exp-pred-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.pred-name) (syntax->datum #'qpd.pred-exprs)))]
[(exp-prop-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.prop-name) (syntax->datum #'qpd.prop-exprs)))]
( [(exp-pred-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.pred-name) (syntax->datum #'qpd.pred-exprs)) stx)]
[(exp-prop-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.prop-name) (syntax->datum #'qpd.prop-exprs)) stx)]

[prop-consolidated (if (equal? (syntax->datum #'qpd.prop-exprs) '())
(syntax/loc stx qpd.prop-name)
Expand Down Expand Up @@ -1245,7 +1255,7 @@
op)
expr1:ExprClass)
(with-syntax ([expr1 (my-expand #'expr1)]
[op (datum->syntax #'op (string->symbol (syntax->datum #'op)))])
[op (datum->syntax #'op (string->symbol (syntax->datum #'op)) #'op)])
(syntax/loc stx (op (#:lang (get-check-lang)) expr1)))]

[((~datum Expr) "#" expr1:ExprClass)
Expand Down Expand Up @@ -1439,11 +1449,13 @@
(with-syntax ([ellip '...])
(syntax/loc stx-outer
(define-syntax (macro-id stx)
; Uncomment this if debugging loss of syntax location. Look through the spam for
; syntax that doesn't carry a location or that has unexpected location.
;(printf "in macro-id ~a: ~a~n" 'macro-id stx)
(syntax-parse stx
#:track-literals
[((~var macro-id id) . pattern) pattern-directive ... (syntax/loc stx template)]))))]))


(dsm-keep (Expr1 stx ...) (Expr stx ...))
(dsm-keep (Expr2 stx ...) (Expr stx ...))
(dsm-keep (Expr3 stx ...) (Expr stx ...))
Expand Down
2 changes: 1 addition & 1 deletion forge/last-checker.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -394,7 +394,7 @@
(map (lambda (decl)
(let ([var (car decl)]
[domain (cdr decl)])
(printf "!!!!! comprehension case; var: ~a; domain: ~a; quantvars: ~a~n" var domain quantvars)
;(printf "!!!!! comprehension case; var: ~a; domain: ~a; quantvars: ~a~n" var domain quantvars)
; CHECK: shadowed variables
; It does NOT suffice to do: (assoc var quantvars), since we now give variables
; distinct gensym suffixes to help with disambiguation.
Expand Down
5 changes: 3 additions & 2 deletions forge/sigs-structs.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -662,8 +662,9 @@ Returns whether the given run resulted in sat or unsat, respectively.
(&&/info info
(=>/info info a b)
(=>/info info (!/info info a) c))]
; It's an expression if-then-else
[(and (node/expr? b) (node/expr? c))
; It's an expression if-then-else (note: mixing int-expr and rel-expr is OK)
[(and (or (node/expr? b) (node/int? b) (integer? b))
(or (node/expr? c) (node/int? c) (integer? c)))
(ite/info info a b c)]
; It's an error
[else
Expand Down
5 changes: 1 addition & 4 deletions forge/tests/forge/relations/breakers.frg
Original file line number Diff line number Diff line change
Expand Up @@ -44,11 +44,8 @@ test expect {
-- Overlap with a previous test, but keep since it checks a valuable syntax foible
cardinalityCheckSyntax: { {#{a: A | some FrontDesk.p[a]}} > 1} is sat

-- TODO BAD ERRORS: recording here for discussion
-- Run-spec: contract violation expected: node/formula? given: (Relation l)
--BAD_ERROR_1: {l} is sat
-- expander.rkt:701:40: preds: attribute contains non-syntax value
--BAD_ERROR_2: {no l} is sat for {A = `A0 + `A1} is sat
-- BAD_ERROR_2: {no l} is sat for {A = `A0 + `A1} is sat

----- test "linear" -----

Expand Down

0 comments on commit 70df030

Please sign in to comment.