diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index 6f828327d..a1afa0f26 100644 --- a/forge/lang/ast.rkt +++ b/forge/lang/ast.rkt @@ -44,11 +44,11 @@ ; * node/formula/sealed ; * wheat ; * node/int -- integer expression +; * node/int/sum-quant -- sum "quantified" form ; * node/int/op (children) ; * node/int/op/add ; * ... ; * node/int/constant (value) -- int constant -; * node/unknown -- delayed binding of identifiers for predicates and functions ;; ----------------------------------------------------------------------------- ; Struct to hold metadata about an AST node (like source location) diff --git a/forge/lang/deparse.rkt b/forge/lang/deparse.rkt index a4f23b553..f2c737d3c 100644 --- a/forge/lang/deparse.rkt +++ b/forge/lang/deparse.rkt @@ -60,6 +60,8 @@ (deparse-expr arg 20)] [(? node/int?) (deparse-int arg 20)] + [(? procedure?) + (format "(Racket procedure, which is likely an unexpected predicate or function definition: ~a)" arg)] [else (format "(COULD-NOT-DEPARSE: ~a)" arg)])) diff --git a/forge/lang/expander.rkt b/forge/lang/expander.rkt index 3bcb9bdd3..2ff4aa00d 100644 --- a/forge/lang/expander.rkt +++ b/forge/lang/expander.rkt @@ -44,6 +44,14 @@ (make-token abstract-tok "abstract" #:abstract)) +; Used because we sometimes need to evaluate "inside-out" while expanding +; macros "outside-in". The list of symbols are the "stop locations". +; This, if we ever add more macros, they need to be added here (unless +; they can be safely expanded as just themselves?) + +; TODO: why is lack of "prime" not breaking something? Is this only ops meant +; to be used with [] or that have >1 argument? + (define-for-syntax (my-expand stx) (define core-funcs-and-macros (map (curry datum->syntax stx) @@ -54,7 +62,7 @@ int< int> int= int>= int<= add subtract multiply divide sign abs remainder card sum sing succ max min sum-quant - node/int/constant + node/int/constant let))) (define result (local-expand stx 'expression core-funcs-and-macros)) @@ -1302,10 +1310,11 @@ [(exprs ...) (datum->syntax #f (map my-expand (syntax->list #'(exprs.exprs ...))))]) (syntax/loc stx (name exprs ...)))] + [((~datum Expr) expr1:ExprClass "[" exprs:ExprListClass "]") - (with-syntax ([expr1 (my-expand #'expr1)] - [(exprs ...) (datum->syntax #f (map my-expand (syntax->list #'(exprs.exprs ...))))]) - (syntax/loc stx (expr1 exprs ...)))] + (with-syntax ([expr1 (my-expand #'expr1)] + [(exprs ...) (datum->syntax #f (map my-expand (syntax->list #'(exprs.exprs ...))))]) + (syntax/loc stx (expr1 exprs ...)))] [((~datum Expr) "~" expr1:ExprClass) (with-syntax ([expr1 (my-expand #'expr1)]) @@ -1332,7 +1341,9 @@ (if local-value ; if we have a local-value, it's likely a Forge macro or Forge-defined helper procedure (syntax/loc stx name.name) - ; otherwise, it's likely an AST node (to be functionally updated with proper syntax location) + ; otherwise, it's likely an AST node (to be functionally updated with proper syntax + ; location at runtime). Note this is a QualName at compile time, but may be substituted + ; to something more complex at runtime via pred/fun application. (with-syntax ([loc (build-source-location (syntax/loc this-syntax #'1))]) (syntax/loc stx (correct-id-loc name.name #:loc loc))))] @@ -1355,25 +1366,67 @@ ; struct-copy would not retain the sub-struct identity and fields, producing just a node ; ditto the struct-update-lib library ; struct-set requires using a special form to create the struct. -; Fortunately, all we need to deal with here _at this time_ is Sig and Relation structs... +; We need to handle Sig and Relation cases, but at runtime the expression might be more +; complex (via substitution from fun/pred application). + ; *New* instance of the structure, with the same values but a (possibly) new source loc (define (correct-id-loc astnode #:loc [loc #f]) - ;(printf "correct-id-loc: ~a; ~a~n" astnode loc) + ;(printf "correct-id-loc: ~a; ~a; ~a~n" astnode (node? astnode) loc) + + (define new-info (if (node? astnode) + (nodeinfo loc (nodeinfo-lang (node-info astnode))) + #f)) (cond [(forge:Sig? astnode) - (define new-info (nodeinfo loc (nodeinfo-lang (node-info astnode)))) (forge:Sig new-info (node/expr-arity astnode) (node/expr/relation-name astnode) (node/expr/relation-typelist-thunk astnode) (node/expr/relation-parent astnode) (node/expr/relation-is-variable astnode) (node/expr/relation-name astnode) (forge:Sig-one astnode) (forge:Sig-lone astnode) (forge:Sig-abstract astnode) (forge:Sig-extends astnode))] [(forge:Relation? astnode) - (define new-info (nodeinfo loc (nodeinfo-lang (node-info astnode)))) (forge:Relation new-info (node/expr-arity astnode) (node/expr/relation-name astnode) (node/expr/relation-typelist-thunk astnode) (node/expr/relation-parent astnode) (node/expr/relation-is-variable astnode) (node/expr/relation-name astnode) ;(forge:Relation-name astnode) (forge:Relation-sigs-thunks astnode) (forge:Relation-breaker astnode))] + [(node/expr/quantifier-var? astnode) + (node/expr/quantifier-var + new-info + (node/expr-arity astnode) (node/expr/quantifier-var-sym astnode) (node/expr/quantifier-var-name astnode))] + ; Annoyingly, structs aren't polymorphic in the way we need. This is not elegant, but: + + ; join, transpose, +, -, &, ^, *, ->, sing, ', ++ + [(node/expr/op/join? astnode) (rebuild-expr-op node/expr/op/join astnode new-info)] + [(node/expr/op/~? astnode) (rebuild-expr-op node/expr/op/~ astnode new-info)] + [(node/expr/op/+? astnode) (rebuild-expr-op node/expr/op/+ astnode new-info)] + [(node/expr/op/-? astnode) (rebuild-expr-op node/expr/op/- astnode new-info)] + [(node/expr/op/&? astnode) (rebuild-expr-op node/expr/op/& astnode new-info)] + [(node/expr/op/^? astnode) (rebuild-expr-op node/expr/op/^ astnode new-info)] + [(node/expr/op/*? astnode) (rebuild-expr-op node/expr/op/* astnode new-info)] + [(node/expr/op/->? astnode) (rebuild-expr-op node/expr/op/-> astnode new-info)] + [(node/expr/op/sing? astnode) (rebuild-expr-op node/expr/op/sing astnode new-info)] + [(node/expr/op/prime? astnode) (rebuild-expr-op node/expr/op/prime astnode new-info)] + [(node/expr/op/++? astnode) (rebuild-expr-op node/expr/op/++ astnode new-info)] + + [(node/expr/ite? astnode) + (node/expr/ite new-info (node/expr-arity astnode) + (node/expr/ite-condition astnode) + (node/expr/ite-thene astnode) + (node/expr/ite-elsee astnode))] + [(node/expr/fun-spacer? astnode) + (node/expr/fun-spacer new-info (node/expr-arity astnode) + (node/expr/fun-spacer-name astnode) + (node/expr/fun-spacer-args astnode) + (node/expr/fun-spacer-codomain astnode) + (node/expr/fun-spacer-expanded astnode))] + [(node/expr/comprehension? astnode) + (node/expr/comprehension new-info (node/expr-arity astnode) + (node/expr/comprehension-decls astnode) + (node/expr/comprehension-formula astnode))] + [(node/expr/constant? astnode) + (node/expr/constant new-info (node/expr-arity astnode) (node/expr/constant-type astnode))] [else astnode])) +(define (rebuild-expr-op constructor astnode new-info) + (constructor new-info (node/expr-arity astnode) (node/expr/op-children astnode))) ; -------------------------- ; these used to be define-simple-macro, but define-simple-macro doesn't diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index aeaad7975..9596867df 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -54,7 +54,18 @@ (check-and-output formula node/formula/constant checker-hash #f)] [(node/fmla/pred-spacer info name args expanded) - (checkFormula run-or-state expanded quantvars checker-hash)] + (define domain-types (for/list ([arg args]) + (checkExpression run-or-state (mexpr-expr (apply-record-domain arg)) quantvars checker-hash))) + (define arg-types (for/list ([arg args] [acc (range 0 (length args))]) + (list (checkExpression run-or-state (apply-record-arg arg) quantvars checker-hash) acc))) + (for-each + (lambda (type) (if (not (member (car (car type)) (list-ref domain-types (cadr type)))) + (raise-forge-error + #:msg (format "The sig(s) given as an argument to predicate ~a are of incorrect type" name) + #:context (apply-record-arg (list-ref args (cadr type)))) + (void))) + arg-types) + (checkFormula run-or-state expanded quantvars checker-hash)] [(node/formula/op info args) (check-and-output formula @@ -260,8 +271,12 @@ ; wrap around checkExpression-mult to provide check for multiplicity, ; while throwing the multiplicity away in output; DO NOT CALL THIS AS PASSTHROUGH! (define (checkExpression run-or-state expr quantvars checker-hash) - (let ([output (checkExpression-mult run-or-state expr quantvars checker-hash)]) - (car output))) +;(printf "expr: ~a~n" expr) + (match expr + [(? node/int?) (list (list 'Int))] + [(? integer?) (list (list 'Int))] + [_ (let ([output (checkExpression-mult run-or-state expr quantvars checker-hash)]) + (car output))])) ; similar except that this is called from a formula, so in bsl ; it should check that the multiplicity of the overall expr is 1 diff --git a/forge/send-to-kodkod.rkt b/forge/send-to-kodkod.rkt index afcd9f632..42316d9e4 100644 --- a/forge/send-to-kodkod.rkt +++ b/forge/send-to-kodkod.rkt @@ -635,6 +635,14 @@ Please declare a sufficient scope for ~a." (define all-atoms (append int-atoms sig-atoms)) + ; for ease of understanding, just sort by first atom + (define (tuple (define bounds-hash (for/hash ([sig (get-sigs run-spec)]) @@ -649,7 +657,9 @@ Please declare a sufficient scope for ~a." (unless (subset? (list->set lower) (list->set upper)) (raise-run-error (format "Bounds inconsistency detected for sig ~a: lower bound was ~a, which is not a subset of upper bound ~a." (Sig-name sig) lower upper) (get-blame-node run-spec sig))) - (values name (bound rel lower upper))))) + (values name (bound rel + (sort (remove-duplicates lower) tuple Predicate ; Gets a predicate by name from a given state +; Note that this will return the procedure, not the macro (no stx loc capture) (define (get-pred run-or-state name) (define state (get-state run-or-state)) (hash-ref (State-pred-map state) name)) ; get-fun :: Run-or-State, Symbol -> Function ; Gets a function by name from a given state +; Note that this will return the procedure, not the macro (no stx loc capture) (define (get-fun run-or-state name) (define state (get-state run-or-state)) (hash-ref (State-fun-map state) name)) diff --git a/forge/sigs.rkt b/forge/sigs.rkt index f7d73312e..d1b375e42 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -434,31 +434,65 @@ [(pred pt:pred-type (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck])) name:id conds:expr ...+) - (with-syntax ([the-info #`(nodeinfo #,(build-source-location stx) check-lang)]) + (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) check-lang)] + [inner-unsyntax #'unsyntax]) (quasisyntax/loc stx (begin - ; use srcloc of actual predicate, not this location in sigs - ; "pred spacer" still present, even if no arguments, to consistently record use of a predicate - (define name - (pt.seal (node/fmla/pred-spacer the-info 'name '() (&&/info the-info conds ...)))) - (update-state! (state-add-pred curr-state 'name name)))))] + ; - Use a macro in order to capture the location of the _use_. + ; For 0-arg predicates, produce the AST node immediately + (define-syntax (name stx2) + (syntax-parse stx2 + [name + (quasisyntax/loc stx2 + ; - "pred spacer" still present, even if no arguments, to consistently record use of a predicate + (let* ([the-info (nodeinfo (inner-unsyntax (build-source-location stx2)) check-lang)] + [ast-node (pt.seal (node/fmla/pred-spacer the-info 'name '() (&&/info the-info conds ...)))]) + (update-state! (state-add-pred curr-state 'name ast-node)) + ast-node))])) )))] ; some decls: predicate must be called to evaluate it [(pred pt:pred-type (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck])) (name:id decls:param-decl-class ...+) conds:expr ...+) - (with-syntax ([the-info #`(nodeinfo #,(build-source-location stx) check-lang)]) - (quasisyntax/loc stx - (begin - ; "pred spacer" added to record use of predicate along with original argument declarations etc. - (define (name decls.name ...) - (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name)) - (error (format "Argument '~a' to pred ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead." - 'decls.name 'name decls.name))) - ... - (pt.seal (node/fmla/pred-spacer the-info 'name (list (apply-record 'decls.name decls.mexpr decls.name) ...) - (&&/info the-info conds ...)))) - (update-state! (state-add-pred curr-state 'name name)))))])) + (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) check-lang)] + [inner-unsyntax #'unsyntax]) + (define result-stx + (with-syntax ([functionname (format-id #'name "~a/func" #'name)]) + (quasisyntax/loc stx + (begin + ; - Use a macro in order to capture the location of the _use_. + + (define-syntax (name stx2) + ;(printf "in macro: ~a~n" stx2) + (syntax-parse stx2 + ; If it's the macro name and all the args, expand to an invocation of the procedure + [(name args (... ...)) + (quasisyntax/loc stx2 + (functionname args (... ...) #:info (nodeinfo + (inner-unsyntax (build-source-location stx2)) check-lang)))] + ; If it's just the macro name, expand to a lambda that can take the same arguments when available + [name:id + (quasisyntax/loc stx2 + (lambda (decls.name ...) + (functionname decls.name ... + #:info (nodeinfo + (inner-unsyntax (build-source-location stx2)) check-lang))))] + )) + + ; - "pred spacer" added to record use of predicate along with original argument declarations etc. + (define (functionname decls.name ... #:info [the-info #f]) + (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name)) + (error (format "Argument '~a' to pred ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead." + 'decls.name 'name decls.name))) + ... + (pt.seal (node/fmla/pred-spacer the-info 'name (list (apply-record 'decls.name decls.mexpr decls.name) ...) + (&&/info the-info conds ...)))) + + + + + (update-state! (state-add-pred curr-state 'name functionname)))))) + result-stx)])) (define/contract (repeat-product expr count) [@-> node/expr? number? node/expr?] @@ -477,11 +511,28 @@ (~optional (~seq #:codomain codomain:codomain-class) #:defaults ([codomain.mexpr #'(mexpr (repeat-product univ (node/expr-arity result)) (if (> (node/expr-arity result) 1) 'set 'one))]))) + ; TODO: there is no check-lang in this macro; does that mean that language-level details are lost within a helper fun? - (with-syntax ([the-info #`(nodeinfo #,(build-source-location stx) 'checklangNoCheck)]) - #'(begin - ; "fun spacer" added to record use of function along with original argument declarations etc. - (define (name decls.name ...) + + (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) 'checklangNoCheck)] + [functionname (format-id #'name "~a/func" #'name)] + [inner-unsyntax #'unsyntax]) + (quasisyntax/loc stx + (begin + ; - create a macro that captures the syntax location of the _use_ + (define-syntax (name stx2) + (syntax-parse stx2 + [(name args (... ...)) + (quasisyntax/loc stx2 + (functionname args (... ...) #:info (nodeinfo + (inner-unsyntax (build-source-location stx2)) 'checklangNoCheck)))] + [name:id + (quasisyntax/loc stx2 + (lambda (decls.name ...) + (functionname decls.name ... #:info (nodeinfo (inner-unsyntax (build-source-location stx2)) 'checklangNoCheck))))])) + + ; - "fun spacer" added to record use of function along with original argument declarations etc. + (define (functionname decls.name ... #:info [the-info #f]) (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name)) (error (format "Argument '~a' to fun ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead." 'decls.name 'name decls.name))) @@ -498,7 +549,7 @@ (list (apply-record 'decls.name decls.mexpr decls.name) ...) codomain.mexpr safe-result)) - (update-state! (state-add-fun curr-state 'name name))))])) + (update-state! (state-add-fun curr-state 'name name)))))])) ; Declare a new constant ; (const name value) diff --git a/forge/tests/error/expect-fun-args.frg b/forge/tests/error/expect-fun-args.frg new file mode 100644 index 000000000..05d6df570 --- /dev/null +++ b/forge/tests/error/expect-fun-args.frg @@ -0,0 +1,12 @@ +#lang forge/bsl +option verbose 0 +option run_sterling off +abstract sig Player {} +one sig X, O extends Player {} +sig Board {board: pfunc Int -> Int -> Player} + +fun playerAt[b: Board, row, col: Int]: lone Player { + b.board[row][col] } + +test expect { should_error: { some playerAt } is sat } + diff --git a/forge/tests/error/expect-fun-no-args.frg b/forge/tests/error/expect-fun-no-args.frg new file mode 100644 index 000000000..84a568000 --- /dev/null +++ b/forge/tests/error/expect-fun-no-args.frg @@ -0,0 +1,11 @@ +#lang forge/bsl +option verbose 0 +option run_sterling off +abstract sig Player {} +one sig X, O extends Player {} +sig Board {board: pfunc Int -> Int -> Player} + +fun xplayer: lone Player { X } + +test expect { should_error: { xplayer[O] = X } is sat } + diff --git a/forge/tests/error/formula_comprehension_cardinality.frg b/forge/tests/error/formula_comprehension_cardinality.frg index 7f3a4c47f..d6a89b9dd 100644 --- a/forge/tests/error/formula_comprehension_cardinality.frg +++ b/forge/tests/error/formula_comprehension_cardinality.frg @@ -10,4 +10,8 @@ pred problem { -- The parser thinks this looks like a constraint block! Expander needs -- to prevent this from making it to AST-creation. #{all a: A | a.i > 0} > 1 +} + +test expect { + should_error: {problem} is sat } \ No newline at end of file diff --git a/forge/tests/error/formula_comprehension_multiplicity.frg b/forge/tests/error/formula_comprehension_multiplicity.frg index 00239ae23..1911e0855 100644 --- a/forge/tests/error/formula_comprehension_multiplicity.frg +++ b/forge/tests/error/formula_comprehension_multiplicity.frg @@ -10,4 +10,8 @@ pred problem { -- The parser thinks this looks like a constraint block! Expander needs -- to prevent this from making it to AST-creation. some {all a: A | a.i > 0} +} + +test expect { + should_error: {problem} is sat } \ No newline at end of file diff --git a/forge/tests/error/main.rkt b/forge/tests/error/main.rkt index bd12e7fe2..8b740dfce 100644 --- a/forge/tests/error/main.rkt +++ b/forge/tests/error/main.rkt @@ -22,6 +22,20 @@ (define REGISTRY (list + ;;;;;;;;;;;;;;;;;;;;;;;; + ; Some error tests look at the specific source-location blamed + + ; misuse of predicates and helper functions with arguments/no-arguments + (list "expect-predicate-args.frg" #rx"Ill-formed block") + (list "expect-predicate-no-args.frg" #rx"expect-predicate-no-args.frg:13:45.*Tried to give arguments to a predicate, but it takes none") + + ; TODO: needs switch to raise-forge-error so the proper location is in the message + ; (list "expect-fun-args.frg" #rx"Racket procedure, which is likely.*expect-fun-args.frg:11") + ; TODO: needs to confirm that equality is irrespective of source location (it should be) + ;(list "expect-fun-no-args.frg" #rx"TODO") + + ;;;;;;;;;;;;;;;;;;;;;;;; + ;;;;;;; Source locations ;;;;;;; (list "./loc/sig_use_loc_error.frg" #rx"sig_use_loc_error.frg:7:39") ; vs. reachable (list "./loc/field_use_loc_error.frg" #rx"field_use_loc_error.frg:7:29") ; vs. reachable @@ -126,8 +140,6 @@ (list "expr-in-comprehension-condition.frg" #rx"expected a formula") (list "non-expr-in-comprehension-domain.frg" #rx"expected a singleton or relational expression") (list "arity-in-comprehension-domain.frg" #rx"variable domain needs arity = 1") - (list "expect-predicate-args.frg" #rx"Ill-formed block") - (list "expect-predicate-no-args.frg" #rx"Tried to give arguments to a predicate, but it takes none") (list "override-wrong-arity.frg" #rx"must have same arity") (list "override-no-overlap.frg" #rx"will never override anything") @@ -137,6 +149,15 @@ (list "int_literal_too_big.frg" #rx"could not be represented in the current bitwidth") (list "parsing_less_dash.frg" #rx"Negative numbers must not have blank space between the minus") + + ;;; Mismatched type tests + (list "mismatched-arg-type-basic.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type") + (list "mismatched-arg-type-basic-univ.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type") + (list "mismatched-arg-type-arity.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type") + (list "mismatched-arg-type-no-quant.frg" #rx"The sig\\(s\\) given as an argument to predicate p1 are of incorrect type") + (list "mismatched-arg-type-no-quant2.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type") + (list "mismatched-arg-type-non-primsig.frg" #rx"The sig\\(s\\) given as an argument to predicate p2 are of incorrect type") + (list "mismatched-arg-type-non-primsig2.frg" #rx"The sig\\(s\\) given as an argument to predicate p are of incorrect type") )) diff --git a/forge/tests/error/mismatched-arg-type-arity.frg b/forge/tests/error/mismatched-arg-type-arity.frg new file mode 100644 index 000000000..8bad55557 --- /dev/null +++ b/forge/tests/error/mismatched-arg-type-arity.frg @@ -0,0 +1,14 @@ +#lang forge/bsl + +sig A { f1: lone B } +sig B { f2: lone A } +pred p1[a: A] { + p2[a.f1, a] +} +pred p2[b1: B, b2: B] { + some b2.f2 +} + +test expect { + should_error: {some x: A | p1[x]} is sat +} diff --git a/forge/tests/error/mismatched-arg-type-basic-univ.frg b/forge/tests/error/mismatched-arg-type-basic-univ.frg new file mode 100644 index 000000000..8b49d42cd --- /dev/null +++ b/forge/tests/error/mismatched-arg-type-basic-univ.frg @@ -0,0 +1,14 @@ +#lang forge + +sig A { f1: lone B } +sig B { f2: lone A } +pred p1[a: univ] { + p2[a] +} +pred p2[b: B] { + some b.f2 +} + +test expect { + should_error: {some x: univ | p1[x]} is sat +} diff --git a/forge/tests/error/mismatched-arg-type-basic.frg b/forge/tests/error/mismatched-arg-type-basic.frg new file mode 100644 index 000000000..6f832cc0e --- /dev/null +++ b/forge/tests/error/mismatched-arg-type-basic.frg @@ -0,0 +1,14 @@ +#lang forge/bsl + +sig A { f1: lone B } +sig B { f2: lone A } +pred p1[a: A] { + p2[a] +} +pred p2[b: B] { + some b.f2 +} + +test expect { + should_error: {some x: A | p1[x]} is sat +} diff --git a/forge/tests/error/mismatched-arg-type-int.frg b/forge/tests/error/mismatched-arg-type-int.frg new file mode 100644 index 000000000..6f9ddcaeb --- /dev/null +++ b/forge/tests/error/mismatched-arg-type-int.frg @@ -0,0 +1,14 @@ +#lang forge/bsl + +sig A { f1: lone B } +sig B { f2: lone A } +pred p1[a: A] { + p2[a] +} +pred p2[b: Int] { + b > 0 +} + +test expect { + should_error: {some x: A | p1[x]} is sat +} diff --git a/forge/tests/error/mismatched-arg-type-no-quant.frg b/forge/tests/error/mismatched-arg-type-no-quant.frg new file mode 100644 index 000000000..b7a74edc9 --- /dev/null +++ b/forge/tests/error/mismatched-arg-type-no-quant.frg @@ -0,0 +1,16 @@ +#lang forge/bsl + +sig A { f1: lone B } +sig B { f2: lone A } +one sig C { f3: lone A } + +pred p1[a: A] { + p2[a.f1, a] +} +pred p2[b1: B, b2: B] { + some b2.f2 +} + +test expect { + should_error: {p1[C]} is sat +} diff --git a/forge/tests/error/mismatched-arg-type-no-quant2.frg b/forge/tests/error/mismatched-arg-type-no-quant2.frg new file mode 100644 index 000000000..d449e824b --- /dev/null +++ b/forge/tests/error/mismatched-arg-type-no-quant2.frg @@ -0,0 +1,16 @@ +#lang forge/bsl + +sig A { f1: lone B } +sig B { f2: lone A } +one sig C { f3: lone A } + +pred p1[a: A] { + p2[a.f1, a] +} +pred p2[b1: B, b2: B] { + some b2.f2 +} + +test expect { + should_error: {p1[C.f3]} is sat +} diff --git a/forge/tests/error/mismatched-arg-type-non-primsig.frg b/forge/tests/error/mismatched-arg-type-non-primsig.frg new file mode 100644 index 000000000..770074a2b --- /dev/null +++ b/forge/tests/error/mismatched-arg-type-non-primsig.frg @@ -0,0 +1,18 @@ +#lang forge/bsl + +sig A { + f2: lone B +} +one sig B extends A {} +one sig C extends A {} + +pred p1[a: A] { + p2[a] +} +pred p2[b: B] { + some b.f2 +} + +test expect { + should_error: {some x: A | p1[x]} is sat +} diff --git a/forge/tests/error/mismatched-arg-type-non-primsig2.frg b/forge/tests/error/mismatched-arg-type-non-primsig2.frg new file mode 100644 index 000000000..097583d13 --- /dev/null +++ b/forge/tests/error/mismatched-arg-type-non-primsig2.frg @@ -0,0 +1,15 @@ +#lang forge/bsl + +sig A { + f2: lone B +} +one sig B extends A {} +one sig C extends A {} + +pred p[c: C] { + some c.f2 +} + +test expect { + should_error: {some x: B | p[x]} is sat +} diff --git a/forge/tests/forge-core/ints/intStructure.rkt b/forge/tests/forge-core/ints/intStructure.rkt index 8ebdfbc77..1d5f8a7eb 100644 --- a/forge/tests/forge-core/ints/intStructure.rkt +++ b/forge/tests/forge-core/ints/intStructure.rkt @@ -36,12 +36,11 @@ #:scope ([Int 5]) #:expect theorem) - (define (make-n n) - (cond - [(@= n 0) (sing (int 0))] - [(@< n 0) (join succ (make-n (add1 n)))] - [(@> n 0) (join (make-n (sub1 n)) succ)])) + (cond + [(@= n 0) (sing (int 0))] + [(@< n 0) (join succ (make-n (add1 n)))] + [(@> n 0) (join (make-n (sub1 n)) succ)])) (pred (Size lower upper) ; lower @@ -52,6 +51,9 @@ (some (make-n upper)) ; some 0 (no (make-n (add1 upper)))) ; no 1) + + + (test size1 #:preds [(Size -1 0)] #:scope ([Int 1]) diff --git a/forge/tests/forge-functional/other/ast-nodes.rkt b/forge/tests/forge-functional/other/ast-nodes.rkt index 73908e17f..1888af51e 100644 --- a/forge/tests/forge-functional/other/ast-nodes.rkt +++ b/forge/tests/forge-functional/other/ast-nodes.rkt @@ -5,12 +5,21 @@ (require (prefix-in @ rackunit)) ; Tests for AST node equality, etc. +; Equality should apply irrespective of source location information. + +; Note there is some test-duplication between here and the forge-core version. +; DO NOT DELETE ONE IN FAVOR OF THE OTHER (especially without confirming that they are +; in fact identical!) (@check-equal? univ univ) (@check-equal? true true) (@check-equal? (join iden iden) (join iden iden)) (@check-equal? (in (join iden iden) (join iden iden)) (in (join iden iden) (join iden iden))) + +; Quantifier variables (node/expr/quantifier-var) have a "sym" field that should be +; distinct, even if the variable name is the same. This helps to detect shadowing, etc. +; But as a result, it is not safe to consider "x" = "x" here. (@check-not-equal? (some ([x univ]) (in x x)) (some ([x univ]) (in x x))) (@check-equal? (some univ) @@ -47,5 +56,8 @@ (@check-not-equal? (equal-hash-code univ) (equal-hash-code iden)) - - +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Not testing equality for sig/relation nodes across aliasing here, +; since that's only done in the Forge expander at the moment. +; In forge/core, syntax location must be modified manually. +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; \ No newline at end of file diff --git a/forge/tests/forge/expressions/expressionOperators.rkt b/forge/tests/forge/expressions/expressionOperators.rkt index a5609dd90..73ebd4487 100644 --- a/forge/tests/forge/expressions/expressionOperators.rkt +++ b/forge/tests/forge/expressions/expressionOperators.rkt @@ -118,7 +118,7 @@ test expect ExpressionOperators { autoConvertIntFun : {canConvertIntExprNullary <= #Node} is theorem autoConvertIntFun_args : {canConvertIntExprUnary[Node] <= #Node} is theorem - -- Regression test for last-checker/join/spacer issue; Jan 05 2023 + -- Regression test for last-checker/join/spacer issue; Jan 05 2024 regression_join_on_spacer : { some n: Node | { some forceSpacerAroundNode[n].edges diff --git a/forge/tests/srclocs/main.rkt b/forge/tests/srclocs/main.rkt index 8fc65b928..2245ab390 100644 --- a/forge/tests/srclocs/main.rkt +++ b/forge/tests/srclocs/main.rkt @@ -2,38 +2,70 @@ ; Confirm that source locations are indeed preserved in case they are needed for errors. -(require (rename-in rackunit [check rackunit-check])) -(require (only-in racket flatten first string-contains?)) +(require (rename-in rackunit [check rackunit-check]) + (only-in rackunit check-true check-equal? check-not-eq?)) +(require (only-in racket flatten first second string-contains?) + (prefix-in @ (only-in racket -))) ; Returns a list of all AST nodes in this tree -(define (gather-tree n #:leafs-only leafs-only) +(define (gather-tree n #:leafs-only leafs-only #:ignore-outer ignore-outer) + (define ignore (if (< 1 ignore-outer) 0 (@- ignore-outer 1))) + + ;; Helper for AST nodes that have a quantified structure + (define (gather-quant-helper e) + (define decls (cond [(node/formula/quantified? e) + (node/formula/quantified-decls e)] + [(node/expr/comprehension? e) + (node/expr/comprehension-decls e)] + [else + (node/int/sum-quant-decls e)])) + (define fmla (cond [(node/formula/quantified? e) + (node/formula/quantified-formula e)] + [(node/expr/comprehension? e) + (node/expr/comprehension-formula e)] + [else + (node/int/sum-quant-int-expr e)])) + (append + ; Gather both decl variables and decl expressions (and their subexpressions) + (flatten (map (lambda (decl) + (list (gather-tree (car decl) #:leafs-only leafs-only #:ignore-outer ignore) + (gather-tree (cdr decl) #:leafs-only leafs-only #:ignore-outer ignore))) + decls)) + (gather-tree fmla #:leafs-only leafs-only #:ignore-outer ignore))) + (define descendents (cond [(node/expr/op? n) - (flatten (map (lambda (ch) (gather-tree ch #:leafs-only leafs-only)) + (flatten (map (lambda (ch) (gather-tree ch #:leafs-only leafs-only #:ignore-outer ignore)) (node/expr/op-children n)))] [(node/formula/op? n) - (flatten (map (lambda (ch) (gather-tree ch #:leafs-only leafs-only)) + (flatten (map (lambda (ch) (gather-tree ch #:leafs-only leafs-only #:ignore-outer ignore)) (node/formula/op-children n)))] [(node/int/op? n) - (flatten (map (lambda (ch) (gather-tree ch #:leafs-only leafs-only)) + (flatten (map (lambda (ch) (gather-tree ch #:leafs-only leafs-only #:ignore-outer ignore)) (node/int/op-children n)))] [(node/fmla/pred-spacer? n) - (gather-tree (node/fmla/pred-spacer-expanded n) #:leafs-only leafs-only)] + (gather-tree (node/fmla/pred-spacer-expanded n) #:leafs-only leafs-only #:ignore-outer ignore)] [(node/expr/fun-spacer? n) - (gather-tree (node/expr/fun-spacer-expanded n) #:leafs-only leafs-only)] + (gather-tree (node/expr/fun-spacer-expanded n) #:leafs-only leafs-only #:ignore-outer ignore)] + [(node/formula/multiplicity? n) + (gather-tree (node/formula/multiplicity-expr n) #:leafs-only leafs-only #:ignore-outer ignore)] + [(node/formula/sealed? n) + ; for sealed AST nodes, the inner formula is contained in the info field + (gather-tree (node-info n) #:leafs-only leafs-only #:ignore-outer ignore)] [(node/formula/multiplicity? n) - (gather-tree (node/formula/multiplicity-expr n) #:leafs-only leafs-only)] - [(node/formula/quantified? n) - ; TODO: decls - (gather-tree (node/formula/quantified-formula n) #:leafs-only leafs-only)] + (gather-tree (node/formula/multiplicity-expr n) #:leafs-only leafs-only #:ignore-outer ignore)] + [(or (node/formula/quantified? n) + (node/expr/comprehension? n) + (node/int/sum-quant? n)) + (gather-quant-helper n)] ;; TODO: other cases [else (list n)])) - (if leafs-only - descendents - (cons n descendents))) + (cond [leafs-only descendents] + [ignore-outer descendents] + [else (cons n descendents)])) (define (print-one-per-line l) (cond [(not (list l)) (printf " ~a~n" l)] @@ -42,15 +74,19 @@ ; Confirm that the syntax location information for all nodes refers to the proper module -(define (check-full-ast-srclocs root-ast sub-path-str) - (for ([n (gather-tree root-ast #:leafs-only #f)]) +; The `ignore-outer` parameter allows the caller to ignore the source location of outermost +; expressions, since that will be captured in _this_ module. Look instead at subexpressions. +; (Recommended for direct pred invocations: *2* layers to ignore (spacer and outer conjunction). +(define (check-full-ast-srclocs root-ast sub-path-str #:ignore-outer [ignore-outer 0]) + (for ([n (gather-tree root-ast #:leafs-only #f #:ignore-outer ignore-outer)]) (define loc (nodeinfo-loc (node-info n))) + ;(printf "~a~n" loc) (define source-path-correct (string-contains? (path->string (srcloc-source loc)) sub-path-str)) (unless source-path-correct - (printf " ~a: ~a~n" n loc)) + (printf " Source path unexpected for:~n ~a~n~a~n" n loc)) ; Comment out for now, avoid unpleasant flickering spam ;(check-true source-path-correct) )) @@ -67,13 +103,63 @@ ;(require (only-in "../forge/library/reachable.frg" reach6)) ;(check-full-ast-srclocs reach6 "/forge/library/reachable.frg") -(require (only-in "../forge/formulas/booleanFormulaOperators.rkt" Implies And Or Not)) -(check-full-ast-srclocs Implies "/forge/formulas/booleanFormulaOperators.rkt") -(check-full-ast-srclocs And "/forge/formulas/booleanFormulaOperators.rkt") -(check-full-ast-srclocs Or "/forge/formulas/booleanFormulaOperators.rkt") -(check-full-ast-srclocs Not "/forge/formulas/booleanFormulaOperators.rkt") - +;(require (only-in "../forge/formulas/booleanFormulaOperators.rkt" Implies And Or Not)) +;(check-full-ast-srclocs Implies "/forge/formulas/booleanFormulaOperators.rkt" #:ignore-outer 2) +;(check-full-ast-srclocs And "/forge/formulas/booleanFormulaOperators.rkt" #:ignore-outer 2) +;(check-full-ast-srclocs Or "/forge/formulas/booleanFormulaOperators.rkt" #:ignore-outer 2) +;(check-full-ast-srclocs Not "/forge/formulas/booleanFormulaOperators.rkt" #:ignore-outer 2) +(require (only-in "../forge/examples/sudoku.rkt" generatePuzzle)) +(check-full-ast-srclocs generatePuzzle "sudoku.rkt" #:ignore-outer 2) ;; TODO: check run parameters as well (catch instances...) -;; TODO: other examples \ No newline at end of file +;; TODO: other examples + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Check source locations for a specific example +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(require "sigs_fields_preds_funs.frg") +(check-true (node? Providence)) +(check-true (node? reachableFromProvidence)) ; Providence.^(edges1+edges2) + +(define usePvd (first (node/expr/op-children reachableFromProvidence))) +(check-true (node? usePvd)) +(define useEdges1 (first (node/expr/op-children + (first (node/expr/op-children + (second (node/expr/op-children reachableFromProvidence))))))) +(check-true (node? useEdges1)) + + +;; SIG ;; +; Use and declaration considered equal +(check-equal? Providence usePvd) +; but not referentially equal +(check-not-eq? Providence usePvd) +; and have different source locations +(check-not-equal? (nodeinfo-loc (node-info Providence)) + (nodeinfo-loc (node-info usePvd))) +;; FIELD ;; +; Use and declaration considered equal +(check-equal? edges1 useEdges1) +; but not referentially equal +(check-not-eq? edges1 useEdges1) +; and have different source locations +(check-not-equal? (nodeinfo-loc (node-info edges1)) + (nodeinfo-loc (node-info useEdges1))) + +;; PRED ;; +(define pvdReachesEverything (reachesEverything Providence)) +(check-true (node? pvdReachesEverything)) +;(printf "~npvdReachesEverything: ~a~n" (nodeinfo-loc (node-info pvdReachesEverything))) +(check-equal? 153 + (srcloc-line (nodeinfo-loc (node-info pvdReachesEverything)))) + + +;; FUN ;; +(define twoHopsFromProvidence (twoHopsAway Providence)) +(check-true (node? twoHopsFromProvidence)) +;(printf "~ntopHopsFromProvidence: ~a~n" (nodeinfo-loc (node-info twoHopsFromProvidence))) +(check-equal? 161 + (srcloc-line (nodeinfo-loc (node-info twoHopsFromProvidence)))) diff --git a/forge/tests/srclocs/sigs_fields_preds_funs.frg b/forge/tests/srclocs/sigs_fields_preds_funs.frg new file mode 100644 index 000000000..f9a6c6536 --- /dev/null +++ b/forge/tests/srclocs/sigs_fields_preds_funs.frg @@ -0,0 +1,30 @@ +#lang forge + +-- For importing into forge/core and inspecting syntax locations of individual nodes. + +sig Node { + edges1: set Node, + edges2: set Node +} +sig Providence extends Node {} + +pred reachesEverything[city: Node] { + Node in city.^(edges1 + edges2) +} +pred allRoadsLeadToProvidence { + all n: Node | Providence in n.^(edges1 + edges2) +} + +fun twoHopsAway[city: Node]: set Node { + city.(edges1+edges2).(edges1+edges2) +} +fun reachableFromProvidence: set Node { + Providence.^(edges1+edges2) +} + + + + + + +