From 57a31020c30b4ab807aff66b246e4a59a57ce6fb Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Sat, 2 Mar 2024 11:47:15 -0500 Subject: [PATCH 01/27] forge_error test modality, multiple tests, improve messages from AST --- forge/lang/alloy-syntax/lexer.rkt | 3 +- forge/lang/alloy-syntax/parser.rkt | 3 +- forge/lang/ast.rkt | 120 ++++++++++++++----------- forge/lang/expander.rkt | 4 +- forge/run-tests.sh | 8 +- forge/sigs.rkt | 44 ++++++--- forge/tests/forge/other/ast-errors.frg | 20 +++++ 7 files changed, 134 insertions(+), 68 deletions(-) create mode 100644 forge/tests/forge/other/ast-errors.frg diff --git a/forge/lang/alloy-syntax/lexer.rkt b/forge/lang/alloy-syntax/lexer.rkt index bad95ce2..24253869 100644 --- a/forge/lang/alloy-syntax/lexer.rkt +++ b/forge/lang/alloy-syntax/lexer.rkt @@ -108,7 +108,8 @@ ["some" (token+ `SOME-TOK "" lexeme "" lexeme-start lexeme-end)] ["sum" (token+ `SUM-TOK "" lexeme "" lexeme-start lexeme-end #f #t)] ["test" (token+ `TEST-TOK "" lexeme "" lexeme-start lexeme-end)] - ["theorem" (token+ `THEOREM-TOK "" lexeme "" lexeme-start lexeme-end)] + ["theorem" (token+ `THEOREM-TOK "" lexeme "" lexeme-start lexeme-end)] + ["forge_error" (token+ `FORGE_ERROR-TOK "" lexeme "" lexeme-start lexeme-end)] ["two" (token+ `TWO-TOK "" lexeme "" lexeme-start lexeme-end)] ["univ" (token+ `UNIV-TOK "" lexeme "" lexeme-start lexeme-end)] ["unsat" (token+ `UNSAT-TOK "" lexeme "" lexeme-start lexeme-end)] diff --git a/forge/lang/alloy-syntax/parser.rkt b/forge/lang/alloy-syntax/parser.rkt index 4e90e6f4..982d85e8 100644 --- a/forge/lang/alloy-syntax/parser.rkt +++ b/forge/lang/alloy-syntax/parser.rkt @@ -85,7 +85,8 @@ ParaDecls : /LEFT-PAREN-TOK @ParaDeclList? /RIGHT-PAREN-TOK AssertDecl : /ASSERT-TOK Name? Block CmdDecl : (Name /COLON-TOK)? (RUN-TOK | CHECK-TOK) (QualName | Block)? Scope? (/FOR-TOK Bounds)? -TestDecl : (Name /COLON-TOK)? (QualName | Block)? Scope? (/FOR-TOK Bounds)? /IS-TOK (SAT-TOK | UNSAT-TOK | THEOREM-TOK) +TestDecl : (Name /COLON-TOK)? (QualName | Block)? Scope? (/FOR-TOK Bounds)? /IS-TOK + (SAT-TOK | UNSAT-TOK | THEOREM-TOK | FORGE_ERROR-TOK) TestExpectDecl : TEST-TOK? EXPECT-TOK Name? TestBlock TestBlock : /LEFT-CURLY-TOK TestDecl* /RIGHT-CURLY-TOK Scope : /FOR-TOK Number (/BUT-TOK @TypescopeList)? diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index a1afa0f2..f60e3da8 100644 --- a/forge/lang/ast.rkt +++ b/forge/lang/ast.rkt @@ -103,67 +103,87 @@ [(integer? a-node) (intexpr->expr/maybe (int a-node) #:op functionname #:info info)] [(node/expr? a-node) a-node] [else - (define loc (nodeinfo-loc info)) - (define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc))) - (raise-syntax-error functionname - (format "~a operator expected to be given an expression, but instead got ~a at loc: ~a" functionname (node-type a-node) locstr) - (datum->syntax #f (deparse a-node) (build-source-location-syntax loc)))])) + (raise-forge-error + #:msg (format "~a operator expected to be given an expression, but instead got ~a, which was ~a." + functionname (deparse a-node) (node-type a-node)) + #:context a-node)])) (define/contract (expr->intexpr/maybe a-node #:op functionname #:info info) (@-> node? #:op symbol? #:info nodeinfo? node/int?) - (cond [(node/expr? a-node) (node/int/op/sum (node-info a-node) (list a-node))] + (cond [(and (node/expr? a-node) + (equal? (node/expr-arity a-node) 1)) + ; If arity 1, this node/expr can be converted automatically to a node/int + (node/int/op/sum (node-info a-node) (list a-node))] + [(node/expr? a-node) + ; Otherwise, this node/expr has the wrong arity for auto-conversion to a node/int + (raise-forge-error + #:msg (format "Could not treat ~a as an integer expression. Expected arity 1, got arity ~a" + (deparse a-node) (node/expr-arity a-node)) + #:context a-node)] [(node/int? a-node) a-node] [(integer? a-node) (int a-node)] [else - (define loc (nodeinfo-loc info)) - (define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc))) - (raise-syntax-error functionname - (format "~a operator expected an expression, but instead got ~a at loc: ~a" functionname (node-type a-node) locstr) - (datum->syntax #f (deparse a-node) (build-source-location-syntax loc)))])) + (raise-forge-error + #:msg (format "~a operator expected an expression, but instead got ~a, which was ~a" + functionname (deparse a-node) (node-type a-node)) + #:context a-node)])) +; Check arguments to an operator declared with define-node-op (define (check-args info op args type? #:same-arity? [same-arity? #f] #:arity [arity #f] #:min-length [min-length 2] #:max-length [max-length #f] #:join? [join? #f] #:domain? [domain? #f] #:range? [range? #f]) (define loc (nodeinfo-loc info)) - (define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc))) - + + ; check: correct number of arguments (when (< (length args) min-length) - (raise-syntax-error op (format "building ~a; not enough arguments: required ~a got ~a at loc: ~a" - op min-length args locstr) - (datum->syntax #f (map deparse args) (build-source-location-syntax loc)))) + (raise-forge-error + #:msg (format "building ~a; not enough arguments: required ~a got ~a." + op min-length args) + #:context loc)) (unless (false? max-length) (when (> (length args) max-length) - (raise-syntax-error op (format "too many arguments to ~a; maximum ~a, got ~a at loc: ~a" op max-length args locstr) - (datum->syntax #f (map deparse args) (build-source-location-syntax loc))))) + (raise-forge-error + #:msg (format "too many arguments to ~a; maximum ~a, got ~a." op max-length args) + #:context loc))) + (for ([a (in-list args)]) + ; check: type of argument (unless (type? a) - (raise-syntax-error op (format "argument to ~a had unexpected type. expected ~a, got ~a. loc: ~a" op type? a locstr) - (datum->syntax #f (map deparse args) (build-source-location-syntax loc)))) + (raise-forge-error + #:msg (format "argument to ~a had unexpected type. expected ~a, got ~a." op type? a) + #:context loc)) + ; check: arity of argument (unless (false? arity) (unless (equal? (node/expr-arity a) arity) - (raise-syntax-error op (format "argument to ~a was not expression with arity ~v (got: ~a) at loc: ~a" op arity a locstr) - (datum->syntax #f (map deparse args) (build-source-location-syntax loc)))))) + (raise-forge-error + #:msg (format "argument to ~a was not expression with arity ~v (got: ~a)" op arity a) + #:context loc)))) + (when same-arity? (let ([arity (node/expr-arity (car args))]) (for ([a (in-list args)]) (unless (equal? (node/expr-arity a) arity) - (raise-syntax-error op (format "arguments to ~a must have same arity. got ~a and ~a at loc: ~a" - op arity (node/expr-arity a) locstr) - (datum->syntax #f (map deparse args) (build-source-location-syntax loc))))))) + (raise-forge-error + #:msg (format "arguments to ~a must have same arity. got ~a and ~a" + op arity (node/expr-arity a)) + #:context loc))))) (when join? (when (<= (apply join-arity (for/list ([a (in-list args)]) (node/expr-arity a))) 0) - (raise-syntax-error op (format "join would create a relation of arity 0 at loc: ~a" locstr) - (datum->syntax #f (map deparse args) (build-source-location-syntax loc))))) + (raise-forge-error + #:msg (format "join would create a relation of arity 0") + #:context loc))) (when range? (unless (equal? (node/expr-arity (cadr args)) 1) - (raise-syntax-error op (format "second argument to ~a must have arity 1 at loc: ~a" op locstr) - (datum->syntax #f (map deparse args) (build-source-location-syntax loc))))) + (raise-forge-error + #:msg (format "second argument to ~a must have arity 1" op) + #:context loc))) (when domain? (unless (equal? (node/expr-arity (car args)) 1) - (raise-syntax-error op (format "first argument to ~a must have arity 1 at loc: ~a" op locstr) - (datum->syntax #f (map deparse args) (build-source-location-syntax loc)))))) + (raise-forge-error + #:msg (format "first argument to ~a must have arity 1" op) + #:context loc)))) ;; EXPRESSIONS ----------------------------------------------------------------- @@ -244,17 +264,17 @@ (define c (intexpr->expr/maybe orig-c #:op 'if-then-else #:info info)) (unless (node/formula? a) - (raise-syntax-error #f (format "If-then-else expression requires first argument to be a formula") - (datum->syntax #f (deparse a) (build-source-location-syntax (nodeinfo-loc info))))) + (raise-forge-error #:msg (format "If-then-else expression requires first argument to be a formula") + #:context (nodeinfo-loc info))) (unless (node/expr? b) - (raise-syntax-error #f (format "If-then-else expression requires second argument to be an expression") - (datum->syntax #f (deparse b) (build-source-location-syntax (nodeinfo-loc info))))) + (raise-forge-error #:msg (format "If-then-else expression requires second argument to be an expression") + #:context (nodeinfo-loc info))) (unless (node/expr? c) - (raise-syntax-error #f (format "If-then-else expression requires third argument to be an expression") - (datum->syntax #f (deparse c) (build-source-location-syntax (nodeinfo-loc info))))) + (raise-forge-error #:msg (format "If-then-else expression requires third argument to be an expression") + #:context (nodeinfo-loc info))) (unless (equal? (node/expr-arity b) (node/expr-arity c)) - (raise-syntax-error #f (format "If-then-else expression requires expression arguments to have same arity") - (datum->syntax #f (deparse c) (build-source-location-syntax (nodeinfo-loc info))))) + (raise-forge-error #:msg (format "If-then-else expression requires expression arguments to have same arity") + #:context (nodeinfo-loc info))) (node/expr/ite info (node/expr-arity b) a b c)) (define-syntax (ite/info stx) @@ -605,11 +625,8 @@ [val (identifier? (syntax val)) (quasisyntax/loc stx (node/expr/constant (nodeinfo #,(build-source-location stx) 'checklangplaceholder) 1 'univ))]))) (define-syntax iden (lambda (stx) (syntax-case stx () [val (identifier? (syntax val)) (quasisyntax/loc stx (node/expr/constant (nodeinfo #,(build-source-location stx) 'checklangplaceholder) 2 'iden))]))) -; relations, not constants -; (define-syntax Int (lambda (stx) (syntax-case stx () -; [val (identifier? (syntax val)) (quasisyntax/loc stx (node/expr/relation (nodeinfo #,(build-source-location stx)) 1 "Int" '(Int) "univ" #f))]))) -; (define-syntax succ (lambda (stx) (syntax-case stx () -; [val (identifier? (syntax val)) (quasisyntax/loc stx (node/expr/relation (nodeinfo #,(build-source-location stx)) 2 "succ" '(Int Int) "Int" #f))]))) + +; Int and succ are built-in relations, not constant expressions ;; INTS ------------------------------------------------------------------------ @@ -625,15 +642,16 @@ (define-node-op divide node/int/op #f #:min-length 2 #:type node/int?) ; id, parent, arity, checks -; card and sum both accept a single node/expr as their argument +; card and sum both accept a single node/expr as their argument. (define-node-op card node/int/op #f #:min-length 1 #:max-length 1 #:type node/expr?) -(define-node-op sum node/int/op #f #:min-length 1 #:max-length 1 #:type node/expr?) +; sum must have an argument *of arity 1*; it is used to convert node/expr to node/int. +(define-node-op sum node/int/op #f #:min-length 1 #:max-length 1 #:arity 1 #:type node/expr?) (define-node-op remainder node/int/op #f #:min-length 2 #:max-length 2 #:type node/int?) (define-node-op abs node/int/op #f #:min-length 1 #:max-length 1 #:type node/int?) (define-node-op sign node/int/op #f #:min-length 1 #:max-length 1 #:type node/int?) -; min and max are now *defined*, not declared, and in sigs-structs.rkt: +; min and max are now *defined*, not declared, in sigs-structs.rkt. ;; -- constants ---------------------------------------------------------------- @@ -821,8 +839,10 @@ (unless (node/expr? expr) (define loc (nodeinfo-loc info)) (define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc))) - (raise-syntax-error mult (format "~a operator expected to be given an expression, but instead got ~a at loc: ~a" mult (node-type expr) locstr) - (datum->syntax #f (deparse expr) (build-source-location-syntax loc)))) + (raise-forge-error + #:msg (format "~a operator expected to be given an expression, but instead got ~a" + mult (node-type expr)) + #:context loc)) (node/formula/multiplicity info mult expr)) (define (no-pairwise-intersect vars #:context [context #f]) @@ -1173,7 +1193,7 @@ (define (pretty-loc loc) (format "~a:~a:~a (span ~a)" (srcloc-source loc) (srcloc-line loc) (srcloc-column loc) (srcloc-span loc))) -(define (raise-forge-error #:msg [msg "error"] #:context [context #f] #:raise? [raise? #t]) +(define (raise-forge-error #:msg [msg "error"] #:context [context #f] #:raise? [raise? #t]) (define loc (cond [(nodeinfo? context) (pretty-loc (nodeinfo-loc context))] ; Wheats/chaffs have their inner formula in the info field diff --git a/forge/lang/expander.rkt b/forge/lang/expander.rkt index 2ff4aa00..d91c7d30 100644 --- a/forge/lang/expander.rkt +++ b/forge/lang/expander.rkt @@ -333,7 +333,7 @@ pred-block:BlockClass)) (~optional scope:ScopeClass) (~optional bounds:BoundsClass) - (~or "sat" "unsat" "theorem")))) + (~or "sat" "unsat" "theorem" "forge_error")))) ; TestBlock : /LEFT-CURLY-TOK TestDecl* /RIGHT-CURLY-TOK (define-syntax-class TestBlockClass @@ -963,7 +963,7 @@ preds:BlockClass)) (~optional scope:ScopeClass) (~optional bounds:BoundsClass) - (~and expected (~or "sat" "unsat" "theorem"))) + (~and expected (~or "sat" "unsat" "theorem" "forge_error"))) (with-syntax ([name #`(~? name.name #,(make-temporary-name stx))] [preds #'(~? pred.name preds)] [expected (datum->syntax #'expected diff --git a/forge/run-tests.sh b/forge/run-tests.sh index 748b7e32..32a5d653 100755 --- a/forge/run-tests.sh +++ b/forge/run-tests.sh @@ -13,10 +13,12 @@ fi echo "Re-running Forge setup for test efficiency." raco setup forge - # Get test files testDir=$1 -doNotTestPattern="[error|srcloc]/[^/]*\\.frg" +# In "basic" regular expressions, use the backslashed versions of "(", ")", and "|" +# Also, apply the pattern deeper than just one directory level (handle error/loc/*.frg) +#doNotTestPattern="\(error\|srclocs\)/[^/]*\\.frg" +doNotTestPattern="\(error\|srclocs\)/.*\\.frg" # ^ these tests get checked by tests/error/main.rkt testFiles="$( find $testDir -type f \( -name "*.rkt" -o -name "*.frg" \) | grep --invert-match ${doNotTestPattern} )" numTestFiles="$(echo "$testFiles" | wc -l)" @@ -28,7 +30,7 @@ exitCode=0 # Print header of test files found echo -e "Found the following $numTestFiles test files:\n$breakLine$testFiles\n$breakLine" -# Run tests and report progress +Run tests and report progress for testFile in $testFiles; do current=`date "+%X"` echo -e "\nRunning $testFile ($current)" diff --git a/forge/sigs.rkt b/forge/sigs.rkt index d1b375e4..2c8557d7 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -638,7 +638,27 @@ (add-to-execs (with-syntax ([loc (build-source-location stx)]) (quasisyntax/loc stx - (cond + (cond + + [(equal? 'expected 'forge_error) + ; Expecting an error. If we receive one, do nothing. + ; Otherwise, continue to report the error and then close the run. + ; (N.B., this assumes the run isn't actually created or sent to the solver.) + (define run-reference #f) + (with-handlers ([exn:fail:user? void]) + #,(syntax/loc stx (run name args ...)) + ; Cannot throw the Forge error here, or it will be caught and ignored + (set! run-reference name) + (close-run name)) + ; Instead, wait and throw it here + (when run-reference + (report-test-failure + #:name 'name + #:msg (format "Failed test ~a. No Forge error was produced." 'name) + #:context loc + #:run run-reference + #:sterling #f))] + [(member 'expected '(sat unsat)) #,(syntax/loc stx (run name args ...)) (define first-instance (tree:get-value (Run-result name))) @@ -1036,7 +1056,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Struct to hold test-failure information for eventual reporting -(struct test-failure (name msg context instance run)) +(struct test-failure (name msg context instance run sterling)) ; Mutable value to store list of test-failure structs (define delayed-test-failures null) ; Called to clear the mutable list @@ -1044,7 +1064,8 @@ ; Record (or report, depending on the value of the delay-test-failure-reporting? ; parameter) a test failure. -(define (report-test-failure #:name name #:msg msg #:context context #:instance [instance #f] #:run run) +(define (report-test-failure #:name name #:msg msg #:context context + #:instance [instance #f] #:run run #:sterling [sterling #t]) ; Default is to not delay, but options may affect this. (cond [(not (equal? (get-option run 'test_keep) 'first)) (unless (equal? (get-verbosity) 0) @@ -1053,14 +1074,15 @@ (unless (empty? delayed-test-failures) (close-run (test-failure-run (first delayed-test-failures)))) ; then add this failure to the queue - (set! delayed-test-failures (cons (test-failure name msg context instance run) + (set! delayed-test-failures (cons (test-failure name msg context instance run sterling) delayed-test-failures))] [else ; Raise a Forge error and stop execution; show Sterling if enabled. (when (>= (get-verbosity) 1) - (printf "Test ~a failed. Opening Sterling (if able) and stopping.~n" name)) - (true-display run) + (printf "Test ~a failed. Stopping execution.~n" name)) + (when sterling + (true-display run)) (raise-forge-error #:msg msg #:context context)])) ; To be run at the very end of the Forge execution; reports test failures and opens @@ -1074,14 +1096,14 @@ (define last-failure (if (empty? failures) #f (last failures))) (for ([failure failures]) - (define-values (name msg context instance run) + (define-values (name msg context instance run sterling) (values (test-failure-name failure) (test-failure-msg failure) (test-failure-context failure) (test-failure-instance failure) - (test-failure-run failure))) + (test-failure-run failure) (test-failure-sterling failure))) ; Print the error (don't raise an actual exception) - (define sterling-or-instance (if (equal? (get-option run 'run_sterling) 'off) - (format "Sterling disabled, so reporting raw instance data:~n~a" instance) + (define sterling-or-instance (if (or (not sterling) (equal? (get-option run 'run_sterling) 'off)) + (format "Sterling disabled for this test. Reporting raw instance data:~n~a" instance) (format "Running Sterling to show instance generated, if any.~n~a" (if (equal? failure last-failure) "Solver is active; evaluator and next are available." @@ -1090,7 +1112,7 @@ #:context context #:raise? #f) ; Display in Sterling (if run_sterling is enabled) - (when (equal? failure last-failure) + (when (and sterling (equal? failure last-failure)) (true-display run))) ; Return to empty-failure-list state. diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg new file mode 100644 index 00000000..36ccd173 --- /dev/null +++ b/forge/tests/forge/other/ast-errors.frg @@ -0,0 +1,20 @@ +#lang forge + +-- Tests for some errors of last resort in the AST; some of these +-- will be regression tests. + +one sig Person { + age: one Int +} + +test expect { + -- Regression test for lack of arity-checking in implicit node/expr->node/int + implicit_expr_to_intexpr_arity_add_1: {add[age, 1] = 1} is forge_error + implicit_expr_to_intexpr_arity_add_2: {add[1, age] = 1} is forge_error + -- Test for lack of arity-checking in direct use of sum + sum_arity: {sum[age] = 1} is forge_error + -- test for bad decl arity in sum aggregator + foo: {(sum x : age | x.age) = 1} is forge_error + -- test for bad decl arity in quantification + bar: {some x : age | some x} is sat //forge_error +} \ No newline at end of file From 1268d936cd8de4151e4964b99cfb3899173cfed0 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Sat, 2 Mar 2024 12:09:49 -0500 Subject: [PATCH 02/27] more error fixes, tests --- forge/lang/ast.rkt | 38 ++++++++++++++++++-------- forge/tests/forge/other/ast-errors.frg | 8 ++++-- 2 files changed, 33 insertions(+), 13 deletions(-) diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index f60e3da8..f312ff54 100644 --- a/forge/lang/ast.rkt +++ b/forge/lang/ast.rkt @@ -690,15 +690,20 @@ (define (sum-quant/func decls raw-int-expr #:info [node-info empty-nodeinfo]) (for ([e (map cdr decls)]) (unless (node/expr? e) - (raise-argument-error 'set "expr?" e)) + (raise-forge-error + #:msg (format "sum aggregator expected an expression in its declaration, given ~a" e) + #:context e)) (unless (equal? (node/expr-arity e) 1) - (raise-argument-error 'set "decl of arity 1" e))) + (raise-forge-error + #:msg (format "sum aggregator expected its declaration expression to have arity 1, given ~a" e) + #:context e))) (define int-expr (cond [(node/expr? raw-int-expr) (expr->intexpr/maybe raw-int-expr #:op 'sum #:info node-info)] [else raw-int-expr])) (unless (node/int? int-expr) - (raise-argument-error 'set "int-expr?" int-expr)) + (raise-forge-error #:msg "sum aggregator body expected an integer expression, got ~a" int-expr + #:context int-expr)) (node/int/sum-quant node-info decls int-expr)) (define (sum-quant-expr info decls int-expr) @@ -808,11 +813,14 @@ (define (quantified-formula info quantifier decls formula) (for ([e (in-list (map cdr decls))]) (unless (node/expr? e) - (raise-argument-error quantifier "expr?" e)) - #'(unless (equal? (node/expr-arity e) 1) - (raise-argument-error quantifier "decl of arity 1" e))) + (raise-forge-error #:msg (format "~a quantifier expected an expression for domain, got ~a" quantifier e) + #:context e)) + (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))) (unless (or (node/formula? formula) (equal? #t formula)) - (raise-argument-error quantifier "formula?" formula)) + (raise-forge-error #:msg (format "~a quantifier body expected a formula, got ~a" quantifier formula) + #:context formula)) (node/formula/quantified info quantifier decls formula)) ;(struct node/formula/higher-quantified node/formula (quantifier decls formula)) @@ -877,7 +885,9 @@ (=> (no-pairwise-intersect (list v0 ...) #:context #,(build-source-location stx)) pred))))] [(_ info ([v0 e0 m0:opt-mult-class] ...) pred) (quasisyntax/loc stx - (let* ([v0 (node/expr/quantifier-var info (node/expr-arity e0) (gensym (format "~a_all" 'v0)) 'v0)] ...) + (let* ([v0 (node/expr/quantifier-var info + (if (node/expr? e0) (node/expr-arity e0) 1) + (gensym (format "~a_all" 'v0)) 'v0)] ...) (quantified-formula info 'all (list (cons v0 e0) ...) pred)))])) ;;; SOME ;;; @@ -903,7 +913,9 @@ ; TODO: currently discarding the multiplicity info, unchecked (in this and the following cases) [(_ info ([v0 e0 m0:opt-mult-class] ...) pred) (quasisyntax/loc stx - (let* ([v0 (node/expr/quantifier-var info (node/expr-arity e0) (gensym (format "~a_some" 'v0)) 'v0)] ...) + (let* ([v0 (node/expr/quantifier-var info + (if (node/expr? e0) (node/expr-arity e0) 1) + (gensym (format "~a_some" 'v0)) 'v0)] ...) (quantified-formula info 'some (list (cons v0 e0) ...) pred)))] ; quantifier case with disjointness flag; embed and repeat [(_ info #:disj ([v0 e0 m0:opt-mult-class] ...) pred) @@ -942,7 +954,9 @@ ; quantifier without disj: rewrite as !some [(_ info ([v0 e0 m0:opt-mult-class] ...) pred) (quasisyntax/loc stx - (let* ([v0 (node/expr/quantifier-var info (node/expr-arity e0) (gensym (format "~a_no" 'v0)) 'v0)] ...) + (let* ([v0 (node/expr/quantifier-var info + (if (node/expr? e0) (node/expr-arity e0) 1) + (gensym (format "~a_no" 'v0)) 'v0)] ...) (! (quantified-formula info 'some (list (cons v0 e0) ...) pred))))] [(_ info expr) (quasisyntax/loc stx @@ -1027,7 +1041,9 @@ (syntax-parse stx [(_ (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck])) ([x1 r1 m0:opt-mult-class] ...) int-expr) (quasisyntax/loc stx - (let* ([x1 (node/expr/quantifier-var (nodeinfo #,(build-source-location stx) check-lang) (node/expr-arity r1) (gensym (format "~a_sum" 'x1)) 'x1)] ...) + (let* ([x1 (node/expr/quantifier-var (nodeinfo #,(build-source-location stx) check-lang) + (if (node/expr? r1) (node/expr-arity r1) 1) + (gensym (format "~a_sum" 'x1)) 'x1)] ...) (sum-quant-expr (nodeinfo #,(build-source-location stx) check-lang) (list (cons x1 r1) ...) int-expr)))])) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 36ccd173..50b0c9af 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -14,7 +14,11 @@ test expect { -- Test for lack of arity-checking in direct use of sum sum_arity: {sum[age] = 1} is forge_error -- test for bad decl arity in sum aggregator - foo: {(sum x : age | x.age) = 1} is forge_error + sum_aggregator_decl_arity: {(sum x : age | x.age) = 1} is forge_error + -- test for bad type in sum aggregator decl + sum_aggregator_decl_fmla: {(sum x : (Person = Person) | x.age) = 1} is forge_error -- test for bad decl arity in quantification - bar: {some x : age | some x} is sat //forge_error + quantifier_decl_arity: {some x : age | some x} is forge_error + -- test for bad type in quantifier decl + quantifier_decl_arity: {some x : (Person = Person) | some x} is forge_error } \ No newline at end of file From 3bd96f78eb7b50a94a733df22d36fb0c41521777 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Mon, 4 Mar 2024 16:56:23 -0500 Subject: [PATCH 03/27] add more AST last-resort tests --- forge/tests/forge/other/ast-errors.frg | 38 ++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 50b0c9af..010c0834 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -8,17 +8,51 @@ one sig Person { } test expect { + ----- sum aggregator and ints ----- + -- Regression test for lack of arity-checking in implicit node/expr->node/int implicit_expr_to_intexpr_arity_add_1: {add[age, 1] = 1} is forge_error implicit_expr_to_intexpr_arity_add_2: {add[1, age] = 1} is forge_error + -- (There is no comparable arity check for node/int -> node/expr) + -- Test for lack of arity-checking in direct use of sum sum_arity: {sum[age] = 1} is forge_error -- test for bad decl arity in sum aggregator sum_aggregator_decl_arity: {(sum x : age | x.age) = 1} is forge_error -- test for bad type in sum aggregator decl sum_aggregator_decl_fmla: {(sum x : (Person = Person) | x.age) = 1} is forge_error + + + ----- quantification ----- + -- Should be similar structure for each quantifier. Labeling the "some" cases for reference. + + -- SOME -- test for bad decl arity in quantification - quantifier_decl_arity: {some x : age | some x} is forge_error + quantifier_some_decl_arity: {some x : age | some x} is forge_error -- test for bad type in quantifier decl - quantifier_decl_arity: {some x : (Person = Person) | some x} is forge_error + quantifier_some_decl_arity: {some x : (Person = Person) | some x} is forge_error + -- test for bad type in quantified-formula subformula + quantifier_some_subformula_type: {some x : Person | x} is forge_error + + -- ALL + quantifier_all_decl_arity: {all x : age | some x} is forge_error + quantifier_all_decl_arity: {all x : (Person = Person) | some x} is forge_error + quantifier_all_subformula_type: {all x : Person | x} is forge_error + + -- LONE + quantifier_lone_decl_arity: {lone x : age | some x} is forge_error + quantifier_lone_decl_arity: {lone x : (Person = Person) | some x} is forge_error + quantifier_lone_subformula_type: {lone x : Person | x} is forge_error + + -- ONE + quantifier_one_decl_arity: {one x : age | some x} is forge_error + quantifier_one_decl_arity: {one x : (Person = Person) | some x} is forge_error + quantifier_one_subformula_type: {one x : Person | x} is forge_error + + -- NO + quantifier_no_decl_arity: {no x : age | some x} is forge_error + quantifier_no_decl_arity: {no x : (Person = Person) | some x} is forge_error + quantifier_no_subformula_type: {no x : Person | x} is forge_error + + } \ No newline at end of file From 607c43d55746b63c9a6e42abf50d4efd82c7917a Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Mon, 4 Mar 2024 17:41:35 -0500 Subject: [PATCH 04/27] working --- forge/tests/forge/other/ast-errors.frg | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 010c0834..36be6edf 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -29,30 +29,39 @@ test expect { -- SOME -- test for bad decl arity in quantification quantifier_some_decl_arity: {some x : age | some x} is forge_error - -- test for bad type in quantifier decl - quantifier_some_decl_arity: {some x : (Person = Person) | some x} is forge_error + -- test for bad syntax-type in quantifier decl + quantifier_some_decl_syntax_type: {some x : (Person = Person) | some x} is forge_error -- test for bad type in quantified-formula subformula quantifier_some_subformula_type: {some x : Person | x} is forge_error + -- test for non-variable in quantifier variable position + -- TODO: copy to other quantifier types + --quantifier_some_decl_arity: {some Person : Person | some Person} is forge_error -- ALL quantifier_all_decl_arity: {all x : age | some x} is forge_error - quantifier_all_decl_arity: {all x : (Person = Person) | some x} is forge_error + quantifier_all_decl_syntax_type: {all x : (Person = Person) | some x} is forge_error quantifier_all_subformula_type: {all x : Person | x} is forge_error -- LONE quantifier_lone_decl_arity: {lone x : age | some x} is forge_error - quantifier_lone_decl_arity: {lone x : (Person = Person) | some x} is forge_error + quantifier_lone_decl_syntax_type: {lone x : (Person = Person) | some x} is forge_error quantifier_lone_subformula_type: {lone x : Person | x} is forge_error -- ONE quantifier_one_decl_arity: {one x : age | some x} is forge_error - quantifier_one_decl_arity: {one x : (Person = Person) | some x} is forge_error + quantifier_one_decl_syntax_type: {one x : (Person = Person) | some x} is forge_error quantifier_one_subformula_type: {one x : Person | x} is forge_error -- NO quantifier_no_decl_arity: {no x : age | some x} is forge_error - quantifier_no_decl_arity: {no x : (Person = Person) | some x} is forge_error + quantifier_no_decl_syntax_type: {no x : (Person = Person) | some x} is forge_error quantifier_no_subformula_type: {no x : Person | x} is forge_error + + + -- Relational operators + + + } \ No newline at end of file From f087e335c693a0b5f56378037740dd0ea78e4f82 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Mon, 4 Mar 2024 18:35:14 -0500 Subject: [PATCH 05/27] fix another bad error message --- forge/last-checker.rkt | 20 ++++++++++++-------- forge/tests/forge/other/ast-errors.frg | 10 +++++++--- 2 files changed, 19 insertions(+), 11 deletions(-) diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index 9596867d..3a394e17 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -89,14 +89,14 @@ [domain (cdr decl)]) ; CHECK: shadowed variables (when (assoc var quantvars) - (raise-syntax-error #f - (format "Shadowing of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) - (datum->syntax #f var (build-source-location-syntax (nodeinfo-loc info))))) + (raise-forge-error + #:msg (format "Shadowing of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) + #:context info)) ; CHECK: recur into domain(s) (checkExpression run-or-state domain quantvars checker-hash))) decls) ; Extend domain environment - (let ([new-quantvars (append (map assocify decls) quantvars)]) + (let ([new-quantvars (append (map assocify decls) quantvars)]) ; CHECK: recur into subformula (checkFormula run-or-state subform new-quantvars checker-hash))))] [(node/formula/sealed info) @@ -371,10 +371,14 @@ checker-hash ; Look up in quantvars association list, type is type of domain (cons (if (assoc expr quantvars) ; expr, not sym (decls are over var nodes) - (checkExpression run-or-state (second (assoc expr quantvars)) quantvars checker-hash) - (raise-syntax-error #f (format "Variable ~a used but was unbound in overall formula being checked. Bound variables: ~a" sym (map car quantvars) ) - (datum->syntax #f name (build-source-location-syntax (nodeinfo-loc info))))) - #t))] + (checkExpression run-or-state (second (assoc expr quantvars)) quantvars checker-hash) + (raise-forge-error + #:msg (format "Variable ~a used, but it was unbound at this point.\ + Often, this means that a sig, field, or helper name is being used as a quantifier variable.\ + It might also mean that the variable domain references the variable itself.\ + For help debugging, the bound variables at this point were: ~a" sym (map car quantvars) ) + #:context info)) + #t))] ; set comprehension e.g. {n : Node | some n.edges} [(node/expr/comprehension info arity decls subform) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 36be6edf..0c0c6c51 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -1,4 +1,6 @@ #lang forge +option verbose 0 +option run_sterling off -- Tests for some errors of last resort in the AST; some of these -- will be regression tests. @@ -34,29 +36,31 @@ test expect { -- test for bad type in quantified-formula subformula quantifier_some_subformula_type: {some x : Person | x} is forge_error -- test for non-variable in quantifier variable position - -- TODO: copy to other quantifier types - --quantifier_some_decl_arity: {some Person : Person | some Person} is forge_error + quantifier_some_decl_arity: {some Person : Person | some Person} is forge_error -- ALL quantifier_all_decl_arity: {all x : age | some x} is forge_error quantifier_all_decl_syntax_type: {all x : (Person = Person) | some x} is forge_error quantifier_all_subformula_type: {all x : Person | x} is forge_error + quantifier_all_decl_arity: {all Person : Person | some Person} is forge_error -- LONE quantifier_lone_decl_arity: {lone x : age | some x} is forge_error quantifier_lone_decl_syntax_type: {lone x : (Person = Person) | some x} is forge_error quantifier_lone_subformula_type: {lone x : Person | x} is forge_error + quantifier_lone_decl_arity: {lone Person : Person | some Person} is forge_error -- ONE quantifier_one_decl_arity: {one x : age | some x} is forge_error quantifier_one_decl_syntax_type: {one x : (Person = Person) | some x} is forge_error quantifier_one_subformula_type: {one x : Person | x} is forge_error + quantifier_one_decl_arity: {one Person : Person | some Person} is forge_error -- NO quantifier_no_decl_arity: {no x : age | some x} is forge_error quantifier_no_decl_syntax_type: {no x : (Person = Person) | some x} is forge_error quantifier_no_subformula_type: {no x : Person | x} is forge_error - + quantifier_no_decl_arity: {no Person : Person | some Person} is forge_error From 81905de7be8f22c0d1f80d34b4bbc22c18984430 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Mon, 4 Mar 2024 18:40:06 -0500 Subject: [PATCH 06/27] add missing test --- forge/tests/forge/other/ast-errors.frg | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 0c0c6c51..ab7b6a09 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -23,6 +23,8 @@ test expect { sum_aggregator_decl_arity: {(sum x : age | x.age) = 1} is forge_error -- test for bad type in sum aggregator decl sum_aggregator_decl_fmla: {(sum x : (Person = Person) | x.age) = 1} is forge_error + -- test for bad arity in sum-aggregator sub-expression + sum_aggregator_decl_fmla: {(sum x : Person | age) = 1} is forge_error ----- quantification ----- @@ -63,9 +65,4 @@ test expect { quantifier_no_decl_arity: {no Person : Person | some Person} is forge_error - - -- Relational operators - - - } \ No newline at end of file From 161f38859681959e2d5e57b224fd8e46969e70bc Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 09:16:15 -0500 Subject: [PATCH 07/27] error improvements, more tests --- forge/lang/ast.rkt | 39 ++++++++++++-------- forge/tests/forge/other/ast-errors.frg | 50 ++++++++++++++++++++++---- 2 files changed, 67 insertions(+), 22 deletions(-) diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index f312ff54..6b2e4071 100644 --- a/forge/lang/ast.rkt +++ b/forge/lang/ast.rkt @@ -5,7 +5,7 @@ racket/contract racket/match forge/shared ; for verbosity level - (only-in racket false? empty? first second rest drop const thunk) + (only-in racket false? empty? first second rest drop const thunk range) (prefix-in @ (only-in racket + - * < > or <=))) (provide deparse @@ -104,8 +104,8 @@ [(node/expr? a-node) a-node] [else (raise-forge-error - #:msg (format "~a operator expected to be given an expression, but instead got ~a, which was ~a." - functionname (deparse a-node) (node-type a-node)) + #:msg (format "~a operator expected to be given an atom- or set-valued expression, but instead got ~a, which was ~a." + functionname (deparse a-node) (pretty-type-of a-node)) #:context a-node)])) (define/contract (expr->intexpr/maybe a-node #:op functionname #:info info) @@ -125,9 +125,21 @@ [else (raise-forge-error #:msg (format "~a operator expected an expression, but instead got ~a, which was ~a" - functionname (deparse a-node) (node-type a-node)) + functionname (deparse a-node) (pretty-type-of a-node)) #:context a-node)])) +(define (pretty-name-predicate p) + (cond [(equal? p node/expr?) "atom- or set-valued expression"] + [(equal? p node/formula?) "boolean-valued formula"] + [(equal? p node/int?) "integer-valued expression"] + [else p])) +(define (pretty-type-of x) + (cond [(node/formula? x) "boolean-valued formula"] + [(node/expr? x) "atom- or set-valued expression"] + [(node/int? x) "integer-valued expression"] + [(number? x) "number"] + [else "unknown expression type"])) + ; Check arguments to an operator declared with define-node-op (define (check-args info op args type? #:same-arity? [same-arity? #f] #:arity [arity #f] @@ -147,17 +159,20 @@ #:msg (format "too many arguments to ~a; maximum ~a, got ~a." op max-length args) #:context loc))) - (for ([a (in-list args)]) + (for ([a (in-list args)] + [idx (map add1 (range (length args)))]) ; check: type of argument (unless (type? a) (raise-forge-error - #:msg (format "argument to ~a had unexpected type. expected ~a, got ~a." op type? a) + #:msg (format "argument ~a of ~a to ~a had unexpected type. Expected ~a, got ~a, which was ~a." + idx (length args) op (pretty-name-predicate type?) (deparse a) (pretty-type-of a)) #:context loc)) ; check: arity of argument (unless (false? arity) (unless (equal? (node/expr-arity a) arity) (raise-forge-error - #:msg (format "argument to ~a was not expression with arity ~v (got: ~a)" op arity a) + #:msg (format "argument ~a of ~a to ~a was not expression with arity ~v (got: ~a)" + idx (length args) op arity (deparse a)) #:context loc)))) (when same-arity? @@ -837,19 +852,13 @@ (define hash-proc (make-robust-node-hash-syntax node/formula/multiplicity 0)) (define hash2-proc (make-robust-node-hash-syntax node/formula/multiplicity 3))]) -(define (node-type n) - (cond [(node/expr? n) "expression"] - [(node/int? n) "integer expression"] - [(node/formula? n) "formula"] - [else "unknown type"])) - (define (multiplicity-formula info mult expr) (unless (node/expr? expr) (define loc (nodeinfo-loc info)) (define locstr (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc))) (raise-forge-error - #:msg (format "~a operator expected to be given an expression, but instead got ~a" - mult (node-type expr)) + #:msg (format "~a operator expected to be given an atom- or set-valued expression, but instead got ~a" + mult (pretty-type-of expr)) #:context loc)) (node/formula/multiplicity info mult expr)) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index ab7b6a09..e1b9c9f9 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -5,9 +5,10 @@ option run_sterling off -- Tests for some errors of last resort in the AST; some of these -- will be regression tests. -one sig Person { +sig Person { age: one Int } +one sig Nim extends Person {} test expect { ----- sum aggregator and ints ----- @@ -22,7 +23,7 @@ test expect { -- test for bad decl arity in sum aggregator sum_aggregator_decl_arity: {(sum x : age | x.age) = 1} is forge_error -- test for bad type in sum aggregator decl - sum_aggregator_decl_fmla: {(sum x : (Person = Person) | x.age) = 1} is forge_error + sum_aggregator_decl_domain: {(sum x : (Person = Person) | x.age) = 1} is forge_error -- test for bad arity in sum-aggregator sub-expression sum_aggregator_decl_fmla: {(sum x : Person | age) = 1} is forge_error @@ -38,31 +39,66 @@ test expect { -- test for bad type in quantified-formula subformula quantifier_some_subformula_type: {some x : Person | x} is forge_error -- test for non-variable in quantifier variable position - quantifier_some_decl_arity: {some Person : Person | some Person} is forge_error + quantifier_some_decl_var: {some Person : Person | some Person} is forge_error -- ALL quantifier_all_decl_arity: {all x : age | some x} is forge_error quantifier_all_decl_syntax_type: {all x : (Person = Person) | some x} is forge_error quantifier_all_subformula_type: {all x : Person | x} is forge_error - quantifier_all_decl_arity: {all Person : Person | some Person} is forge_error + quantifier_all_decl_var: {all Person : Person | some Person} is forge_error -- LONE quantifier_lone_decl_arity: {lone x : age | some x} is forge_error quantifier_lone_decl_syntax_type: {lone x : (Person = Person) | some x} is forge_error quantifier_lone_subformula_type: {lone x : Person | x} is forge_error - quantifier_lone_decl_arity: {lone Person : Person | some Person} is forge_error + quantifier_lone_decl_var: {lone Person : Person | some Person} is forge_error -- ONE quantifier_one_decl_arity: {one x : age | some x} is forge_error quantifier_one_decl_syntax_type: {one x : (Person = Person) | some x} is forge_error quantifier_one_subformula_type: {one x : Person | x} is forge_error - quantifier_one_decl_arity: {one Person : Person | some Person} is forge_error + quantifier_one_decl_var: {one Person : Person | some Person} is forge_error -- NO quantifier_no_decl_arity: {no x : age | some x} is forge_error quantifier_no_decl_syntax_type: {no x : (Person = Person) | some x} is forge_error quantifier_no_subformula_type: {no x : Person | x} is forge_error - quantifier_no_decl_arity: {no Person : Person | some Person} is forge_error + quantifier_no_decl_var: {no Person : Person | some Person} is forge_error + -- Formula operators mis-used + and_given_expr_1: {some Person and Person} is forge_error + or_given_expr_1: {some Person or Person} is forge_error + not_given_expr: {not Person} is forge_error + implies_given_expr_1: {some Person implies Person} is forge_error + iff_given_expr_1: {some Person iff Person} is forge_error + -- other direction for binary operators + and_given_expr_2: {Person and some Person} is forge_error + or_given_expr_2: {Person or some Person} is forge_error + implies_given_expr_2: {Person implies some Person} is forge_error + iff_given_expr_2: {Person iff some Person} is forge_error + -- Relational operators mis-used + join_given_formula_1: {some (some Nim).Nim} is forge_error + join_given_formula_2: {some Nim.(some Nim)} is forge_error + union_given_formula_1: {some (some Nim) + Nim} is forge_error + union_given_formula_2: {some Nim + (some Nim)} is forge_error + intersect_given_formula_1: {some (some Nim) & Nim} is forge_error + intersect_given_formula_2: {some Nim & (some Nim)} is forge_error + subtract_given_formula_1: {some (some Nim) - Nim} is forge_error + subtract_given_formula_2: {some Nim - (some Nim)} is forge_error + + -- Set comprehension mis-used + comprehension_used_quantifier: { some {all x: Person | some x.age}} is forge_error + comprehension_bad_decl_arity: { some {x: age | some x.age}} is forge_error + comprehension_bad_decl_var: { some {Person: Person | some Person.age}} is forge_error + comprehension_bad_decl_type: { some {x: (Person = Person) | some x.age}} is forge_error + + + + -- Temporal formula operators mis-used + eventually_given_expr: {eventually Person} is forge_error + always_given_expr: {always Person} is forge_error + next_state_given_expr: {next_state Person} is forge_error + until_given_expr_1: {Person until some Person} is forge_error + until_given_expr_2: {some Person until Person} is forge_error } \ No newline at end of file From 0a8210a169a34d1f8bb5d9ae6fda5d9e712f58ba Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 09:21:34 -0500 Subject: [PATCH 08/27] fix typo in tests script --- forge/run-tests.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/forge/run-tests.sh b/forge/run-tests.sh index 32a5d653..57bb8e95 100755 --- a/forge/run-tests.sh +++ b/forge/run-tests.sh @@ -30,7 +30,7 @@ exitCode=0 # Print header of test files found echo -e "Found the following $numTestFiles test files:\n$breakLine$testFiles\n$breakLine" -Run tests and report progress +# Run tests and report progress for testFile in $testFiles; do current=`date "+%X"` echo -e "\nRunning $testFile ($current)" From 6ffd7c7f46ea77055143b729fb155f322a4cae7b Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 09:27:14 -0500 Subject: [PATCH 09/27] more testS --- forge/tests/forge/other/ast-errors.frg | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index e1b9c9f9..b65b5ae4 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -93,7 +93,8 @@ test expect { comprehension_bad_decl_var: { some {Person: Person | some Person.age}} is forge_error comprehension_bad_decl_type: { some {x: (Person = Person) | some x.age}} is forge_error - + -- Cardinality mis-used + card_given_fmla: { #(Person = Person) = 1 } is forge_error -- Temporal formula operators mis-used eventually_given_expr: {eventually Person} is forge_error @@ -101,4 +102,16 @@ test expect { next_state_given_expr: {next_state Person} is forge_error until_given_expr_1: {Person until some Person} is forge_error until_given_expr_2: {some Person until Person} is forge_error + releases_given_expr_1: {Person releases some Person} is forge_error + releases_given_expr_2: {some Person releases Person} is forge_error + historically_given_expr: {historically Person} is forge_error + once_given_expr: {once Person} is forge_error + prev_state_given_expr: {prev_state Person} is forge_error + since_given_expr_1: {Person since some Person} is forge_error + since_given_expr_2: {some Person since Person} is forge_error + triggered_given_expr_1: {Person triggered some Person} is forge_error + triggered_given_expr_2: {some Person triggered Person} is forge_error + + + } \ No newline at end of file From 0da83846e973218251f1816ef25bcf770ebf307e Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 09:46:54 -0500 Subject: [PATCH 10/27] more tests, slight error improvement --- forge/lang/ast.rkt | 2 +- forge/tests/forge/other/ast-errors.frg | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index 6b2e4071..0e4888e9 100644 --- a/forge/lang/ast.rkt +++ b/forge/lang/ast.rkt @@ -91,7 +91,7 @@ #:context f)] [else (raise-forge-error - #:msg (format "Could not use formula as a function: ~a." (deparse f)) + #:msg (format "Could not use a boolean-valued formula as a predicate, function, or field name: ~a." (deparse f)) #:context f)]))) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index b65b5ae4..c650fbac 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -80,12 +80,20 @@ test expect { -- Relational operators mis-used join_given_formula_1: {some (some Nim).Nim} is forge_error join_given_formula_2: {some Nim.(some Nim)} is forge_error + boxjoin_given_formula_1: {some (some Nim)[Nim]} is forge_error + boxjoin_given_formula_2: {some Nim[(some Nim)]} is forge_error union_given_formula_1: {some (some Nim) + Nim} is forge_error union_given_formula_2: {some Nim + (some Nim)} is forge_error intersect_given_formula_1: {some (some Nim) & Nim} is forge_error intersect_given_formula_2: {some Nim & (some Nim)} is forge_error subtract_given_formula_1: {some (some Nim) - Nim} is forge_error subtract_given_formula_2: {some Nim - (some Nim)} is forge_error + product_given_formula_1: {some (some Nim) -> Nim} is forge_error + product_given_formula_2: {some Nim -> (some Nim)} is forge_error + tc_given_formula: {some ^(some Person)} is forge_error + rtc_given_formula: {some *(some Person)} is forge_error + transpose_given_formula: {some ~(some Person)} is forge_error + -- Set comprehension mis-used comprehension_used_quantifier: { some {all x: Person | some x.age}} is forge_error From 594eebaf9747acf34b4db7508be1b8cff7eb701d Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 09:52:26 -0500 Subject: [PATCH 11/27] renaming test files rkt to frg --- forge/tests/forge/electrum/{after-tests.rkt => after-tests.frg} | 0 forge/tests/forge/electrum/{always-tests.rkt => always-tests.frg} | 0 forge/tests/forge/electrum/{always-true.rkt => always-true.frg} | 0 .../{basic-temporal-example.rkt => basic-temporal-example.frg} | 0 forge/tests/forge/electrum/{cities.rkt => cities.frg} | 0 .../forge/electrum/{eventually-tests.rkt => eventually-tests.frg} | 0 .../{example-light-puzzle.rkt => example-light-puzzle.frg} | 0 ...-can-stop-var-changes.rkt => non-var-can-stop-var-changes.frg} | 0 forge/tests/forge/electrum/{past-time.rkt => past-time.frg} | 0 .../forge/electrum/{social-network.rkt => social-network.frg} | 0 .../tests/forge/electrum/{traffic-light.rkt => traffic-light.frg} | 0 ...ar-can-force-var-changes.rkt => var-can-force-var-changes.frg} | 0 .../electrum/{var-vs-non-var-rels.rkt => var-vs-non-var-rels.frg} | 0 .../electrum/{var-vs-non-var-sigs.rkt => var-vs-non-var-sigs.frg} | 0 forge/tests/forge/examples/{booleanLogic.rkt => booleanLogic.frg} | 0 forge/tests/forge/examples/{sudoku.rkt => sudoku.frg} | 0 .../{expressionOperators.rkt => expressionOperators.frg} | 0 .../expressions/{orderOfOpsExprs.rkt => orderOfOpsExprs.frg} | 0 .../expressions/{orderOfOpsLogical.rkt => orderOfOpsLogical.frg} | 0 .../{orderOfOpsLogical2.rkt => orderOfOpsLogical2.frg} | 0 .../expressions/{setComprehensions.rkt => setComprehensions.frg} | 0 .../{booleanFormulaOperators.rkt => booleanFormulaOperators.frg} | 0 .../{multiplicityFormulas.rkt => multiplicityFormulas.frg} | 0 .../formulas/{quantifiedFormulas.rkt => quantifiedFormulas.frg} | 0 .../formulas/{setFormulaOperators.rkt => setFormulaOperators.frg} | 0 forge/tests/forge/ints/{intComparators.rkt => intComparators.frg} | 0 forge/tests/forge/ints/{intConverters.rkt => intConverters.frg} | 0 forge/tests/forge/ints/{intOperators.rkt => intOperators.frg} | 0 forge/tests/forge/ints/{intStructure.rkt => intStructure.frg} | 0 forge/tests/forge/relations/{breakers.rkt => breakers.frg} | 0 forge/tests/forge/relations/{lone.rkt => lone.frg} | 0 forge/tests/forge/relations/{one.rkt => ont.frg} | 0 forge/tests/forge/relations/{set.rkt => set.frg} | 0 forge/tests/forge/sigs/{abstractSigs.rkt => abstractSigs.frg} | 0 forge/tests/forge/sigs/{basicSigs.rkt => basicSigs.frg} | 0 forge/tests/forge/sigs/{extendingSigs.rkt => extendingSigs.frg} | 0 forge/tests/forge/sigs/{givenBounds.rkt => givenBounds.frg} | 0 forge/tests/forge/sigs/{loneSigs.rkt => loneSigs.frg} | 0 forge/tests/forge/sigs/{oneSigs.rkt => oneSigs.frg} | 0 forge/tests/forge/target/{close_fixed.rkt => close_fixed.frg} | 0 .../forge/target/{close_retargeting.rkt => close_retargeting.frg} | 0 forge/tests/forge/target/{far_fixed.rkt => far_fixed.frg} | 0 .../forge/target/{far_retargeting.rkt => far_retargeting.frg} | 0 forge/tests/forge/target/{hamming_runs.rkt => hamming_runs.frg} | 0 44 files changed, 0 insertions(+), 0 deletions(-) rename forge/tests/forge/electrum/{after-tests.rkt => after-tests.frg} (100%) rename forge/tests/forge/electrum/{always-tests.rkt => always-tests.frg} (100%) rename forge/tests/forge/electrum/{always-true.rkt => always-true.frg} (100%) rename forge/tests/forge/electrum/{basic-temporal-example.rkt => basic-temporal-example.frg} (100%) rename forge/tests/forge/electrum/{cities.rkt => cities.frg} (100%) rename forge/tests/forge/electrum/{eventually-tests.rkt => eventually-tests.frg} (100%) rename forge/tests/forge/electrum/{example-light-puzzle.rkt => example-light-puzzle.frg} (100%) rename forge/tests/forge/electrum/{non-var-can-stop-var-changes.rkt => non-var-can-stop-var-changes.frg} (100%) rename forge/tests/forge/electrum/{past-time.rkt => past-time.frg} (100%) rename forge/tests/forge/electrum/{social-network.rkt => social-network.frg} (100%) rename forge/tests/forge/electrum/{traffic-light.rkt => traffic-light.frg} (100%) rename forge/tests/forge/electrum/{var-can-force-var-changes.rkt => var-can-force-var-changes.frg} (100%) rename forge/tests/forge/electrum/{var-vs-non-var-rels.rkt => var-vs-non-var-rels.frg} (100%) rename forge/tests/forge/electrum/{var-vs-non-var-sigs.rkt => var-vs-non-var-sigs.frg} (100%) rename forge/tests/forge/examples/{booleanLogic.rkt => booleanLogic.frg} (100%) rename forge/tests/forge/examples/{sudoku.rkt => sudoku.frg} (100%) rename forge/tests/forge/expressions/{expressionOperators.rkt => expressionOperators.frg} (100%) rename forge/tests/forge/expressions/{orderOfOpsExprs.rkt => orderOfOpsExprs.frg} (100%) rename forge/tests/forge/expressions/{orderOfOpsLogical.rkt => orderOfOpsLogical.frg} (100%) rename forge/tests/forge/expressions/{orderOfOpsLogical2.rkt => orderOfOpsLogical2.frg} (100%) rename forge/tests/forge/expressions/{setComprehensions.rkt => setComprehensions.frg} (100%) rename forge/tests/forge/formulas/{booleanFormulaOperators.rkt => booleanFormulaOperators.frg} (100%) rename forge/tests/forge/formulas/{multiplicityFormulas.rkt => multiplicityFormulas.frg} (100%) rename forge/tests/forge/formulas/{quantifiedFormulas.rkt => quantifiedFormulas.frg} (100%) rename forge/tests/forge/formulas/{setFormulaOperators.rkt => setFormulaOperators.frg} (100%) rename forge/tests/forge/ints/{intComparators.rkt => intComparators.frg} (100%) rename forge/tests/forge/ints/{intConverters.rkt => intConverters.frg} (100%) rename forge/tests/forge/ints/{intOperators.rkt => intOperators.frg} (100%) rename forge/tests/forge/ints/{intStructure.rkt => intStructure.frg} (100%) rename forge/tests/forge/relations/{breakers.rkt => breakers.frg} (100%) rename forge/tests/forge/relations/{lone.rkt => lone.frg} (100%) rename forge/tests/forge/relations/{one.rkt => ont.frg} (100%) rename forge/tests/forge/relations/{set.rkt => set.frg} (100%) rename forge/tests/forge/sigs/{abstractSigs.rkt => abstractSigs.frg} (100%) rename forge/tests/forge/sigs/{basicSigs.rkt => basicSigs.frg} (100%) rename forge/tests/forge/sigs/{extendingSigs.rkt => extendingSigs.frg} (100%) rename forge/tests/forge/sigs/{givenBounds.rkt => givenBounds.frg} (100%) rename forge/tests/forge/sigs/{loneSigs.rkt => loneSigs.frg} (100%) rename forge/tests/forge/sigs/{oneSigs.rkt => oneSigs.frg} (100%) rename forge/tests/forge/target/{close_fixed.rkt => close_fixed.frg} (100%) rename forge/tests/forge/target/{close_retargeting.rkt => close_retargeting.frg} (100%) rename forge/tests/forge/target/{far_fixed.rkt => far_fixed.frg} (100%) rename forge/tests/forge/target/{far_retargeting.rkt => far_retargeting.frg} (100%) rename forge/tests/forge/target/{hamming_runs.rkt => hamming_runs.frg} (100%) diff --git a/forge/tests/forge/electrum/after-tests.rkt b/forge/tests/forge/electrum/after-tests.frg similarity index 100% rename from forge/tests/forge/electrum/after-tests.rkt rename to forge/tests/forge/electrum/after-tests.frg diff --git a/forge/tests/forge/electrum/always-tests.rkt b/forge/tests/forge/electrum/always-tests.frg similarity index 100% rename from forge/tests/forge/electrum/always-tests.rkt rename to forge/tests/forge/electrum/always-tests.frg diff --git a/forge/tests/forge/electrum/always-true.rkt b/forge/tests/forge/electrum/always-true.frg similarity index 100% rename from forge/tests/forge/electrum/always-true.rkt rename to forge/tests/forge/electrum/always-true.frg diff --git a/forge/tests/forge/electrum/basic-temporal-example.rkt b/forge/tests/forge/electrum/basic-temporal-example.frg similarity index 100% rename from forge/tests/forge/electrum/basic-temporal-example.rkt rename to forge/tests/forge/electrum/basic-temporal-example.frg diff --git a/forge/tests/forge/electrum/cities.rkt b/forge/tests/forge/electrum/cities.frg similarity index 100% rename from forge/tests/forge/electrum/cities.rkt rename to forge/tests/forge/electrum/cities.frg diff --git a/forge/tests/forge/electrum/eventually-tests.rkt b/forge/tests/forge/electrum/eventually-tests.frg similarity index 100% rename from forge/tests/forge/electrum/eventually-tests.rkt rename to forge/tests/forge/electrum/eventually-tests.frg diff --git a/forge/tests/forge/electrum/example-light-puzzle.rkt b/forge/tests/forge/electrum/example-light-puzzle.frg similarity index 100% rename from forge/tests/forge/electrum/example-light-puzzle.rkt rename to forge/tests/forge/electrum/example-light-puzzle.frg diff --git a/forge/tests/forge/electrum/non-var-can-stop-var-changes.rkt b/forge/tests/forge/electrum/non-var-can-stop-var-changes.frg similarity index 100% rename from forge/tests/forge/electrum/non-var-can-stop-var-changes.rkt rename to forge/tests/forge/electrum/non-var-can-stop-var-changes.frg diff --git a/forge/tests/forge/electrum/past-time.rkt b/forge/tests/forge/electrum/past-time.frg similarity index 100% rename from forge/tests/forge/electrum/past-time.rkt rename to forge/tests/forge/electrum/past-time.frg diff --git a/forge/tests/forge/electrum/social-network.rkt b/forge/tests/forge/electrum/social-network.frg similarity index 100% rename from forge/tests/forge/electrum/social-network.rkt rename to forge/tests/forge/electrum/social-network.frg diff --git a/forge/tests/forge/electrum/traffic-light.rkt b/forge/tests/forge/electrum/traffic-light.frg similarity index 100% rename from forge/tests/forge/electrum/traffic-light.rkt rename to forge/tests/forge/electrum/traffic-light.frg diff --git a/forge/tests/forge/electrum/var-can-force-var-changes.rkt b/forge/tests/forge/electrum/var-can-force-var-changes.frg similarity index 100% rename from forge/tests/forge/electrum/var-can-force-var-changes.rkt rename to forge/tests/forge/electrum/var-can-force-var-changes.frg diff --git a/forge/tests/forge/electrum/var-vs-non-var-rels.rkt b/forge/tests/forge/electrum/var-vs-non-var-rels.frg similarity index 100% rename from forge/tests/forge/electrum/var-vs-non-var-rels.rkt rename to forge/tests/forge/electrum/var-vs-non-var-rels.frg diff --git a/forge/tests/forge/electrum/var-vs-non-var-sigs.rkt b/forge/tests/forge/electrum/var-vs-non-var-sigs.frg similarity index 100% rename from forge/tests/forge/electrum/var-vs-non-var-sigs.rkt rename to forge/tests/forge/electrum/var-vs-non-var-sigs.frg diff --git a/forge/tests/forge/examples/booleanLogic.rkt b/forge/tests/forge/examples/booleanLogic.frg similarity index 100% rename from forge/tests/forge/examples/booleanLogic.rkt rename to forge/tests/forge/examples/booleanLogic.frg diff --git a/forge/tests/forge/examples/sudoku.rkt b/forge/tests/forge/examples/sudoku.frg similarity index 100% rename from forge/tests/forge/examples/sudoku.rkt rename to forge/tests/forge/examples/sudoku.frg diff --git a/forge/tests/forge/expressions/expressionOperators.rkt b/forge/tests/forge/expressions/expressionOperators.frg similarity index 100% rename from forge/tests/forge/expressions/expressionOperators.rkt rename to forge/tests/forge/expressions/expressionOperators.frg diff --git a/forge/tests/forge/expressions/orderOfOpsExprs.rkt b/forge/tests/forge/expressions/orderOfOpsExprs.frg similarity index 100% rename from forge/tests/forge/expressions/orderOfOpsExprs.rkt rename to forge/tests/forge/expressions/orderOfOpsExprs.frg diff --git a/forge/tests/forge/expressions/orderOfOpsLogical.rkt b/forge/tests/forge/expressions/orderOfOpsLogical.frg similarity index 100% rename from forge/tests/forge/expressions/orderOfOpsLogical.rkt rename to forge/tests/forge/expressions/orderOfOpsLogical.frg diff --git a/forge/tests/forge/expressions/orderOfOpsLogical2.rkt b/forge/tests/forge/expressions/orderOfOpsLogical2.frg similarity index 100% rename from forge/tests/forge/expressions/orderOfOpsLogical2.rkt rename to forge/tests/forge/expressions/orderOfOpsLogical2.frg diff --git a/forge/tests/forge/expressions/setComprehensions.rkt b/forge/tests/forge/expressions/setComprehensions.frg similarity index 100% rename from forge/tests/forge/expressions/setComprehensions.rkt rename to forge/tests/forge/expressions/setComprehensions.frg diff --git a/forge/tests/forge/formulas/booleanFormulaOperators.rkt b/forge/tests/forge/formulas/booleanFormulaOperators.frg similarity index 100% rename from forge/tests/forge/formulas/booleanFormulaOperators.rkt rename to forge/tests/forge/formulas/booleanFormulaOperators.frg diff --git a/forge/tests/forge/formulas/multiplicityFormulas.rkt b/forge/tests/forge/formulas/multiplicityFormulas.frg similarity index 100% rename from forge/tests/forge/formulas/multiplicityFormulas.rkt rename to forge/tests/forge/formulas/multiplicityFormulas.frg diff --git a/forge/tests/forge/formulas/quantifiedFormulas.rkt b/forge/tests/forge/formulas/quantifiedFormulas.frg similarity index 100% rename from forge/tests/forge/formulas/quantifiedFormulas.rkt rename to forge/tests/forge/formulas/quantifiedFormulas.frg diff --git a/forge/tests/forge/formulas/setFormulaOperators.rkt b/forge/tests/forge/formulas/setFormulaOperators.frg similarity index 100% rename from forge/tests/forge/formulas/setFormulaOperators.rkt rename to forge/tests/forge/formulas/setFormulaOperators.frg diff --git a/forge/tests/forge/ints/intComparators.rkt b/forge/tests/forge/ints/intComparators.frg similarity index 100% rename from forge/tests/forge/ints/intComparators.rkt rename to forge/tests/forge/ints/intComparators.frg diff --git a/forge/tests/forge/ints/intConverters.rkt b/forge/tests/forge/ints/intConverters.frg similarity index 100% rename from forge/tests/forge/ints/intConverters.rkt rename to forge/tests/forge/ints/intConverters.frg diff --git a/forge/tests/forge/ints/intOperators.rkt b/forge/tests/forge/ints/intOperators.frg similarity index 100% rename from forge/tests/forge/ints/intOperators.rkt rename to forge/tests/forge/ints/intOperators.frg diff --git a/forge/tests/forge/ints/intStructure.rkt b/forge/tests/forge/ints/intStructure.frg similarity index 100% rename from forge/tests/forge/ints/intStructure.rkt rename to forge/tests/forge/ints/intStructure.frg diff --git a/forge/tests/forge/relations/breakers.rkt b/forge/tests/forge/relations/breakers.frg similarity index 100% rename from forge/tests/forge/relations/breakers.rkt rename to forge/tests/forge/relations/breakers.frg diff --git a/forge/tests/forge/relations/lone.rkt b/forge/tests/forge/relations/lone.frg similarity index 100% rename from forge/tests/forge/relations/lone.rkt rename to forge/tests/forge/relations/lone.frg diff --git a/forge/tests/forge/relations/one.rkt b/forge/tests/forge/relations/ont.frg similarity index 100% rename from forge/tests/forge/relations/one.rkt rename to forge/tests/forge/relations/ont.frg diff --git a/forge/tests/forge/relations/set.rkt b/forge/tests/forge/relations/set.frg similarity index 100% rename from forge/tests/forge/relations/set.rkt rename to forge/tests/forge/relations/set.frg diff --git a/forge/tests/forge/sigs/abstractSigs.rkt b/forge/tests/forge/sigs/abstractSigs.frg similarity index 100% rename from forge/tests/forge/sigs/abstractSigs.rkt rename to forge/tests/forge/sigs/abstractSigs.frg diff --git a/forge/tests/forge/sigs/basicSigs.rkt b/forge/tests/forge/sigs/basicSigs.frg similarity index 100% rename from forge/tests/forge/sigs/basicSigs.rkt rename to forge/tests/forge/sigs/basicSigs.frg diff --git a/forge/tests/forge/sigs/extendingSigs.rkt b/forge/tests/forge/sigs/extendingSigs.frg similarity index 100% rename from forge/tests/forge/sigs/extendingSigs.rkt rename to forge/tests/forge/sigs/extendingSigs.frg diff --git a/forge/tests/forge/sigs/givenBounds.rkt b/forge/tests/forge/sigs/givenBounds.frg similarity index 100% rename from forge/tests/forge/sigs/givenBounds.rkt rename to forge/tests/forge/sigs/givenBounds.frg diff --git a/forge/tests/forge/sigs/loneSigs.rkt b/forge/tests/forge/sigs/loneSigs.frg similarity index 100% rename from forge/tests/forge/sigs/loneSigs.rkt rename to forge/tests/forge/sigs/loneSigs.frg diff --git a/forge/tests/forge/sigs/oneSigs.rkt b/forge/tests/forge/sigs/oneSigs.frg similarity index 100% rename from forge/tests/forge/sigs/oneSigs.rkt rename to forge/tests/forge/sigs/oneSigs.frg diff --git a/forge/tests/forge/target/close_fixed.rkt b/forge/tests/forge/target/close_fixed.frg similarity index 100% rename from forge/tests/forge/target/close_fixed.rkt rename to forge/tests/forge/target/close_fixed.frg diff --git a/forge/tests/forge/target/close_retargeting.rkt b/forge/tests/forge/target/close_retargeting.frg similarity index 100% rename from forge/tests/forge/target/close_retargeting.rkt rename to forge/tests/forge/target/close_retargeting.frg diff --git a/forge/tests/forge/target/far_fixed.rkt b/forge/tests/forge/target/far_fixed.frg similarity index 100% rename from forge/tests/forge/target/far_fixed.rkt rename to forge/tests/forge/target/far_fixed.frg diff --git a/forge/tests/forge/target/far_retargeting.rkt b/forge/tests/forge/target/far_retargeting.frg similarity index 100% rename from forge/tests/forge/target/far_retargeting.rkt rename to forge/tests/forge/target/far_retargeting.frg diff --git a/forge/tests/forge/target/hamming_runs.rkt b/forge/tests/forge/target/hamming_runs.frg similarity index 100% rename from forge/tests/forge/target/hamming_runs.rkt rename to forge/tests/forge/target/hamming_runs.frg From aac03f5d6ad8ae39faa9e07b483d806e76f31efb Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 09:59:09 -0500 Subject: [PATCH 12/27] fix: filename extension --- forge/tests/srclocs/main.rkt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/forge/tests/srclocs/main.rkt b/forge/tests/srclocs/main.rkt index 2245ab39..e89d2776 100644 --- a/forge/tests/srclocs/main.rkt +++ b/forge/tests/srclocs/main.rkt @@ -109,8 +109,8 @@ ;(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) +(require (only-in "../forge/examples/sudoku.frg" generatePuzzle)) +(check-full-ast-srclocs generatePuzzle "sudoku.frg" #:ignore-outer 2) ;; TODO: check run parameters as well (catch instances...) ;; TODO: other examples From d46997f467f751f9fd4b812d1383012048d400ca Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 12:19:22 -0500 Subject: [PATCH 13/27] working -- more tests, use raise-forge-error more, identify 3 to-dos --- forge/last-checker.rkt | 22 ++++++++++++---------- forge/sigs.rkt | 5 +++-- forge/tests/forge/other/ast-errors.frg | 24 ++++++++++++++++++++---- 3 files changed, 35 insertions(+), 16 deletions(-) diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index 3a394e17..2a723bd1 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -391,8 +391,9 @@ [domain (cdr decl)]) ; CHECK: shadowed variables (when (assoc var quantvars) - (raise-syntax-error #f (format "Shadowing of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) - (datum->syntax #f var (build-source-location-syntax (nodeinfo-loc info))))) + (raise-forge-error + #:msg (format "Shadowing of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) + #:context info)) ; CHECK: recur into domain(s) (checkExpression run-or-state domain quantvars checker-hash))) decls)] @@ -484,14 +485,15 @@ (when (empty? join-result) (if (eq? (nodeinfo-lang (node-info expr)) 'bsl) ((hash-ref checker-hash 'empty-join) expr) - (raise-syntax-error #f - (format "~n join always results in an empty relation: ~n Left argument of join \"~a\" is in ~a~n Right argument of join \"~a\" is in ~a~n There is no possible join result " - (deparse (first (node/expr/op-children expr))) - (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (car (first child-values))) - (deparse (second (node/expr/op-children expr))) - (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (car (second child-values))) - ) - (datum->syntax #f (deparse expr) (build-source-location-syntax (nodeinfo-loc (node-info expr)))))))) + (raise-forge-error + #:msg (format "Join always results in an empty relation:\ + Left argument of join \"~a\" is in ~a.\ + Right argument of join \"~a\" is in ~a" + (deparse (first (node/expr/op-children expr))) + (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (car (first child-values))) + (deparse (second (node/expr/op-children expr))) + (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (car (second child-values)))) + #:context expr)))) (when (and (not (cdr (first child-values))) (eq? (nodeinfo-lang (node-info expr)) 'bsl)) ((hash-ref checker-hash 'relation-join) expr args)) (cons join-result diff --git a/forge/sigs.rkt b/forge/sigs.rkt index 2c8557d7..d6e224a0 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -647,10 +647,11 @@ (define run-reference #f) (with-handlers ([exn:fail:user? void]) #,(syntax/loc stx (run name args ...)) - ; Cannot throw the Forge error here, or it will be caught and ignored + ; Cannot throw the new "failed test" Forge error here, or it will be caught and ignored (set! run-reference name) (close-run name)) - ; Instead, wait and throw it here + ; Instead, wait and throw it here (note this will only happen if _NO_ user-error was + ; produced by the run, and thus a run-reference is present. (when run-reference (report-test-failure #:name 'name diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index c650fbac..5130b6d9 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -1,5 +1,7 @@ -#lang forge -option verbose 0 +#lang forge + +-- Do not decrease the verbosity. This ensures certain checks are run. +option verbose 1 option run_sterling off -- Tests for some errors of last resort in the AST; some of these @@ -119,7 +121,21 @@ test expect { since_given_expr_2: {some Person since Person} is forge_error triggered_given_expr_1: {Person triggered some Person} is forge_error triggered_given_expr_2: {some Person triggered Person} is forge_error - - + ----- Errors possibly from outside the AST ----- + + -- Join type mismatch + empty_join_result: {some age.Nim} is forge_error + -- 0-ary join result + zero_arity_join_result: {some Nim.Nim} is forge_error + + -- TODO -- + + -- Variable-name shadowing across quantification + -- variable_name_shadowing: { some x: Person | all x: Person | some x } is sat + + -- Variable-name shadowing between quantification and comprehension + --comp_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is sat + -- Variable-name shadowing within a comprehension + --internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat } \ No newline at end of file From c7b9bcd8a30a6cedfe22a395c80be7003da67de3 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 12:34:00 -0500 Subject: [PATCH 14/27] checker descends into RHS of a minus; add test; add another to-do --- forge/last-checker.rkt | 18 ++++++++++++------ forge/tests/forge/other/ast-errors.frg | 16 +++++++++++++--- 2 files changed, 25 insertions(+), 9 deletions(-) diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index 2a723bd1..cefc3e48 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -389,6 +389,7 @@ (map (lambda (decl) (let ([var (car decl)] [domain (cdr decl)]) + (printf "!!!!! comprehension case; var: ~a; domain: ~a; quantvars: ~a~n" var domain quantvars) ; CHECK: shadowed variables (when (assoc var quantvars) (raise-forge-error @@ -445,12 +446,17 @@ ; SETMINUS [(? node/expr/op/-?) - (check-and-output expr - node/expr/op/- - checker-hash - ; A-B should have only 2 children. B may be empty. - (cons (checkExpression run-or-state (first args) quantvars checker-hash) - #t))] + (begin + ; A-B should have only 2 children. B may not exist; use A as the bound returned regardless. + ; However, if B is present, we must /check/ it anyway (and discard non-error results). + (when (@> (length args) 1) + (checkExpression run-or-state (second args) quantvars checker-hash)) + (check-and-output expr + node/expr/op/- + checker-hash + ; A-B should have only 2 children. B may be empty. + (cons (checkExpression run-or-state (first args) quantvars checker-hash) + #t)))] ; INTERSECTION [(? node/expr/op/&?) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 5130b6d9..a05bd940 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -132,10 +132,20 @@ test expect { -- TODO -- -- Variable-name shadowing across quantification - -- variable_name_shadowing: { some x: Person | all x: Person | some x } is sat + -- variable_name_shadowing: { some x: Person | all x: Person | some x } is sat -- s/b error -- Variable-name shadowing between quantification and comprehension - --comp_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is sat + --comp_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is sat -- s/b error -- Variable-name shadowing within a comprehension - --internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat + -- internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b error + -- Variable-name shadowing between nested comprehensions + -- nested_comp_variable_shadowing: {some {x: Person | some {x: Person | some x.age} }} is sat -- s/b error + + -- Minus operator: check RHS for validity, allow chaining + -- set_minus_rhs: {all x: Person, y: Person - x | x != y} is theorem -- should be OK + +-- Regression test: checker must descend into RHS of a minus, even if the RHS has no impact + -- on the inferred type of the expression. + set_minus_rhs_empty_join: { some Person - (age.Nim) } is forge_error + } \ No newline at end of file From 8d2a98393d4a99ca97c591be91e8a64d9139481d Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 5 Mar 2024 15:47:03 -0500 Subject: [PATCH 15/27] check for variable shadowing within quantifiers, more tests --- forge/last-checker.rkt | 12 +++++++++--- ...ected_tree_underconstraint_multiple_errors.frg | 2 +- forge/tests/forge/other/ast-errors.frg | 15 +++++++++------ 3 files changed, 19 insertions(+), 10 deletions(-) diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index cefc3e48..37af6786 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -87,11 +87,17 @@ (lambda (decl) (let ([var (car decl)] [domain (cdr decl)]) + (printf "!!!!! quantifier case: ~a ~a ~a ~n" var domain quantvars) ; CHECK: shadowed variables - (when (assoc var quantvars) + ; It does NOT suffice to do: (assoc var quantvars), since we now give variables + ; distinct gensym suffixes to help with disambiguation. + (when (ormap (lambda (qvd) + (equal? + (node/expr/quantifier-var-name var) + (node/expr/quantifier-var-name (first qvd)))) quantvars) (raise-forge-error - #:msg (format "Shadowing of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) - #:context info)) + #:msg (format "Nested re-use of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) + #:context var)) ; CHECK: recur into domain(s) (checkExpression run-or-state domain quantvars checker-hash))) decls) diff --git a/forge/tests/error/properties_undirected_tree_underconstraint_multiple_errors.frg b/forge/tests/error/properties_undirected_tree_underconstraint_multiple_errors.frg index 240dddaf..a67e6471 100644 --- a/forge/tests/error/properties_undirected_tree_underconstraint_multiple_errors.frg +++ b/forge/tests/error/properties_undirected_tree_underconstraint_multiple_errors.frg @@ -33,5 +33,5 @@ pred TreeWithEdges } assert TreeWithEdges is necessary for isUndirectedTree -assert all n : Node | TreeWithEdges is necessary for isUndirectedTree +assert all x : Node | TreeWithEdges is necessary for isUndirectedTree diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index a05bd940..24d57bed 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -129,14 +129,17 @@ test expect { -- 0-ary join result zero_arity_join_result: {some Nim.Nim} is forge_error - -- TODO -- - -- Variable-name shadowing across quantification - -- variable_name_shadowing: { some x: Person | all x: Person | some x } is sat -- s/b error - + variable_name_shadowing: { some x: Person | all x: Person | some x } is forge_error -- Variable-name shadowing between quantification and comprehension - --comp_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is sat -- s/b error - -- Variable-name shadowing within a comprehension + quant_comp_variable_shadowing: {some {x : Person | some x: Person | some x.age}} is forge_error + + -- TODO -- + + -- Same as above, but in the other direction + --comp_quant_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is sat -- s/b error + + -- Variable-name shadowing within a single comprehension -- internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b error -- Variable-name shadowing between nested comprehensions -- nested_comp_variable_shadowing: {some {x: Person | some {x: Person | some x.age} }} is sat -- s/b error From c5173bff49808030127d060e2a052b3046d7d18c Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Thu, 7 Mar 2024 11:18:21 -0500 Subject: [PATCH 16/27] working --- forge/breaks.rkt | 45 +++++++++++++++++--------- forge/lang/ast.rkt | 2 +- forge/lang/expander.rkt | 31 +++++++++--------- forge/last-checker.rkt | 10 ++++-- forge/tests/forge/other/ast-errors.frg | 32 ++++++++++++++---- forge/tests/froglet/froglet-pi.frg | 2 +- 6 files changed, 80 insertions(+), 42 deletions(-) diff --git a/forge/breaks.rkt b/forge/breaks.rkt index 137efdca..b48abac2 100644 --- a/forge/breaks.rkt +++ b/forge/breaks.rkt @@ -716,22 +716,37 @@ (λ () (break bound formulas))) )) -(add-strategy 'pfunc (λ (pri rel bound atom-lists rel-list [loc #f]) - - (define (pfuncformulajoin quantvarlst) - (cond - [(empty? (rest quantvarlst)) (@join (first quantvarlst) rel)] - [else (@join (first quantvarlst) (pfuncformulajoin (rest quantvarlst)))])) - (define (pfuncformula rllst quantvarlst) - (cond - [(empty? (rest (rest rllst))) - (let ([a (gensym)]) - (@all/info (@just-location-info loc) ([a (first rllst)]) (@lone (pfuncformulajoin (cons a quantvarlst)))))] - [else (let ([a (gensym)]) - (@all/info (@just-location-info loc) ([a (first rllst)]) (pfuncformula (rest rllst) (cons a quantvarlst))))])) - - (define formulas (set (pfuncformula rel-list (list)))) +(add-strategy 'pfunc + (λ (pri rel bound atom-lists rel-list [loc #f]) + (define (pfuncformulajoin quantvarlst) + (cond + ; x_n.rel + [(empty? (rest quantvarlst)) (@join (first quantvarlst) rel)] + ; ... x_n-1.x_n.rel + [else (@join (first quantvarlst) (pfuncformulajoin (rest quantvarlst)))])) + (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))))])) + (define pf-fmla (pfuncformula rel-list (list))) + (printf "pfunc breaker: ~a~n" pf-fmla) + (define formulas (set pf-fmla)) + ; OLD CODE ; (if (equal? A B) ; (formula-breaker pri ; TODO: can improve, but need better symmetry-breaking predicates diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index 0e4888e9..119bc397 100644 --- a/forge/lang/ast.rkt +++ b/forge/lang/ast.rkt @@ -892,7 +892,7 @@ (all/info info ([v0 e0 m0] ...) #,(quasisyntax/loc stx (=> (no-pairwise-intersect (list v0 ...) #:context #,(build-source-location stx)) pred))))] - [(_ info ([v0 e0 m0:opt-mult-class] ...) pred) + [(_ info ([v0 e0 m0:opt-mult-class] ...) pred) (quasisyntax/loc stx (let* ([v0 (node/expr/quantifier-var info (if (node/expr? e0) (node/expr-arity e0) 1) diff --git a/forge/lang/expander.rkt b/forge/lang/expander.rkt index d91c7d30..a745bfae 100644 --- a/forge/lang/expander.rkt +++ b/forge/lang/expander.rkt @@ -170,27 +170,28 @@ ; Mult : LONE-TOK | SOME-TOK | ONE-TOK | TWO-TOK (define-syntax-class MultClass - (pattern ((~datum Mult) "lone") #:attr symbol #'#:lone) - (pattern ((~datum Mult) "some") #:attr symbol #'#:some) - (pattern ((~datum Mult) "one") #:attr symbol #'#:one) - (pattern ((~datum Mult) "two") #:attr symbol #'#:two)) + (pattern ((~datum Mult) "lone") #:attr symbol (syntax/loc this-syntax #:lone)) + (pattern ((~datum Mult) "some") #:attr symbol (syntax/loc this-syntax #:some)) + (pattern ((~datum Mult) "one") #:attr symbol (syntax/loc this-syntax #:one)) + (pattern ((~datum Mult) "two") #:attr symbol (syntax/loc this-syntax #:two))) ; ArrowMult : used for field etc. declarations; the symbol attribute references a breaker (define-syntax-class ArrowMultClass - (pattern ((~datum ArrowMult) "lone") #:attr symbol #'pfunc) - (pattern ((~datum ArrowMult) "set") #:attr symbol #'default) - (pattern ((~datum ArrowMult) "one") #:attr symbol #'func) - (pattern ((~datum ArrowMult) "func") #:attr symbol #'func) - (pattern ((~datum ArrowMult) "pfunc") #:attr symbol #'pfunc) - (pattern ((~datum ArrowMult) "two") #:attr symbol #'(raise "relation arity two not implemented"))) + (pattern ((~datum ArrowMult) "lone") #:attr symbol (syntax/loc this-syntax pfunc)) + (pattern ((~datum ArrowMult) "set") #:attr symbol (syntax/loc this-syntax default)) + (pattern ((~datum ArrowMult) "one") #:attr symbol (syntax/loc this-syntax func)) + (pattern ((~datum ArrowMult) "func") #:attr symbol (syntax/loc this-syntax func)) + (pattern ((~datum ArrowMult) "pfunc") #:attr symbol (syntax/loc this-syntax pfunc)) + (pattern ((~datum ArrowMult) "two") #:attr symbol (syntax/loc this-syntax + (raise "relation arity two not implemented")))) ; HelperMult : used for helper fun/pred definitions; the symbol attribute references a symbol (define-syntax-class HelperMultClass - (pattern ((~datum HelperMult) "lone") #:attr symbol #'(quote lone)) - (pattern ((~datum HelperMult) "set") #:attr symbol #'(quote set)) - (pattern ((~datum HelperMult) "one") #:attr symbol #'(quote one)) - (pattern ((~datum HelperMult) "func") #:attr symbol #'(quote func)) - (pattern ((~datum HelperMult) "pfunc") #:attr symbol #'(quote pfunc))) + (pattern ((~datum HelperMult) "lone") #:attr symbol (syntax/loc this-syntax (quote lone))) + (pattern ((~datum HelperMult) "set") #:attr symbol (syntax/loc this-syntax (quote set))) + (pattern ((~datum HelperMult) "one") #:attr symbol (syntax/loc this-syntax (quote one))) + (pattern ((~datum HelperMult) "func") #:attr symbol (syntax/loc this-syntax (quote func))) + (pattern ((~datum HelperMult) "pfunc") #:attr symbol (syntax/loc this-syntax (quote pfunc)))) ; Declaration of variables with shared expr, shared optional multiplicity diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index 37af6786..769dab14 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -87,7 +87,6 @@ (lambda (decl) (let ([var (car decl)] [domain (cdr decl)]) - (printf "!!!!! quantifier case: ~a ~a ~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. @@ -397,9 +396,14 @@ [domain (cdr decl)]) (printf "!!!!! comprehension case; var: ~a; domain: ~a; quantvars: ~a~n" var domain quantvars) ; CHECK: shadowed variables - (when (assoc var quantvars) + ; It does NOT suffice to do: (assoc var quantvars), since we now give variables + ; distinct gensym suffixes to help with disambiguation. + (when (ormap (lambda (qvd) + (equal? + (node/expr/quantifier-var-name var) + (node/expr/quantifier-var-name (first qvd)))) quantvars) (raise-forge-error - #:msg (format "Shadowing of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) + #:msg (format "Nested re-use of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) #:context info)) ; CHECK: recur into domain(s) (checkExpression run-or-state domain quantvars checker-hash))) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 24d57bed..4de2c47e 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -133,16 +133,15 @@ test expect { variable_name_shadowing: { some x: Person | all x: Person | some x } is forge_error -- Variable-name shadowing between quantification and comprehension quant_comp_variable_shadowing: {some {x : Person | some x: Person | some x.age}} is forge_error + -- Same as above, but in the other direction + comp_quant_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is forge_error + -- Variable-name shadowing between nested comprehensions + nested_comp_variable_shadowing: {some {x: Person | some {x: Person | some x.age} }} is forge_error -- TODO -- - -- Same as above, but in the other direction - --comp_quant_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is sat -- s/b error - -- Variable-name shadowing within a single comprehension - -- internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b error - -- Variable-name shadowing between nested comprehensions - -- nested_comp_variable_shadowing: {some {x: Person | some {x: Person | some x.age} }} is sat -- s/b error + -- internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b FORGE error -- Minus operator: check RHS for validity, allow chaining -- set_minus_rhs: {all x: Person, y: Person - x | x != y} is theorem -- should be OK @@ -151,4 +150,23 @@ test expect { -- on the inferred type of the expression. set_minus_rhs_empty_join: { some Person - (age.Nim) } is forge_error -} \ No newline at end of file +} + + +-- To be integrated with next phase of last-checker improvements +/* + +-- Parse error +--fun primeAfterBoxNoGroup[x: Thread]: set Location {World.loc[x]'} + +fun baseline[x: Thread]: set Location {World.loc'[x]} +test expect { + non_equiv1: {some x: Thread | baseline[x] != World'.loc[x]} is sat + non_equiv2: {some x: Thread | baseline[x] != World.loc[x']} is sat + non_equiv3: {some x: Thread | baseline[x] != (World.loc)'[x]} is unsat + -- Nothing to do with priming; this one should give an empty-join error + -- non_equiv4: {some x: Thread | baseline[x] != World.(loc[x])} is forge_error + non_equiv5: {some x: Thread | baseline[x] != (World.loc[x])'} is unsat +} + +*/ \ No newline at end of file diff --git a/forge/tests/froglet/froglet-pi.frg b/forge/tests/froglet/froglet-pi.frg index a4120b04..5f7e22c7 100644 --- a/forge/tests/froglet/froglet-pi.frg +++ b/forge/tests/froglet/froglet-pi.frg @@ -1,5 +1,5 @@ #lang forge/bsl -option verbose 0 +option verbose 1 ------------------------------------------------- -- Tests for the Froglet partial-instance syntax. From 4db3f8e9c8cadfeeda9941473a322e3110c7387d Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Wed, 13 Mar 2024 15:44:21 -0400 Subject: [PATCH 17/27] add: better error for ifte mismatch of args --- forge/lang/expander.rkt | 2 +- forge/sigs-structs.rkt | 50 +++++++++++++++++----------- forge/tests/error/loc/ifte-error.frg | 13 ++++++++ forge/tests/error/main.rkt | 1 + 4 files changed, 46 insertions(+), 20 deletions(-) create mode 100644 forge/tests/error/loc/ifte-error.frg diff --git a/forge/lang/expander.rkt b/forge/lang/expander.rkt index a745bfae..7b4f638c 100644 --- a/forge/lang/expander.rkt +++ b/forge/lang/expander.rkt @@ -1126,7 +1126,7 @@ (first xs)] [else (raise-forge-error - #:msg (format "Ill-formed block: expected either one expression or any number of formulas") + #:msg (format "Ill-formed block: expected either one expression or any number of formulas; got ~a" xs) #:context stx)])) ; Block : /LEFT-CURLY-TOK Expr* /RIGHT-CURLY-TOK diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index a6d34bd7..df431976 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -652,11 +652,25 @@ Returns whether the given run resulted in sat or unsat, respectively. ; or expression form (which has its own AST node). Avoid exponential ; blowup from chained IFTEs by expanding to a chain of function calls. (define (ifte-disambiguator info a b c) - (if (node/formula? b) - (&&/info info - (=>/info info a b) - (=>/info info (!/info info a) c)) - (ite/info info a b c))) + (unless (node/formula? a) + (raise-forge-error + #:msg ("If-then-else needed a boolean-valued formula for its first argument; got ~a." (pretty-type-of a)) + #:context a)) + (cond + ; It's a formula if-then-else + [(and (node/formula? b) (node/formula? c)) + (&&/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)) + (ite/info info a b c)] + ; It's an error + [else + (raise-forge-error #:msg (format "If-then-else needed consistent types (either both formulas or both expressions) for its true and false branches, but got (~a) and (~a)." + (pretty-type-of b) (pretty-type-of c)) + #:context info)])) + (define-syntax (ifte stx) (syntax-parse stx [(_ (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck])) a b c) (quasisyntax/loc stx @@ -722,19 +736,17 @@ Returns whether the given run resulted in sat or unsat, respectively. (->/info info univ b))) (define (domain-check<: a b loc) - (let ([src-line (source-location-line loc)] - [src-col (source-location-column loc)] - [src-span (source-location-span loc)]) - (unless (equal? (node/expr-arity b) - (@+ 1 (node/expr-arity a))) - (raise-user-error (format "<: argument has incorrect arity (~a vs. ~a) in ~a <: ~a on line ~a, column ~a, span ~a" - (node/expr-arity a) (node/expr-arity b) (deparse a) (deparse b) src-line src-col src-span))))) + (unless (equal? (node/expr-arity b) + (@+ 1 (node/expr-arity a))) + (raise-forge-error + #:msg (format "<: argument has incorrect arity (~a vs. ~a) in ~a <: ~a" + (node/expr-arity a) (node/expr-arity b) (deparse a) (deparse b)) + #:context loc))) (define (domain-check:> a b loc) - (let ([src-line (source-location-line loc)] - [src-col (source-location-column loc)] - [src-span (source-location-span loc)]) - (unless (equal? (node/expr-arity a) - (@+ 1 (node/expr-arity b))) - (raise-user-error (format ":> argument has incorrect arity (~a vs. ~a) in ~a :> ~a on line ~a, column ~a, span ~a" - (node/expr-arity a) (node/expr-arity b) (deparse a) (deparse b) src-line src-col src-span))))) + (unless (equal? (node/expr-arity a) + (@+ 1 (node/expr-arity b))) + (raise-forge-error + #:msg (format ":> argument has incorrect arity (~a vs. ~a) in ~a :> ~a" + (node/expr-arity a) (node/expr-arity b) (deparse a) (deparse b)) + #:context loc))) diff --git a/forge/tests/error/loc/ifte-error.frg b/forge/tests/error/loc/ifte-error.frg new file mode 100644 index 00000000..bf770e63 --- /dev/null +++ b/forge/tests/error/loc/ifte-error.frg @@ -0,0 +1,13 @@ +#lang forge/temporal + +-- Test for srcloc preservation in if-then-else case + +sig Node {edges: set Node} +one sig A, B, C extends Node {} + +pred if_example { + {some A.edges.edges} + => {some B.edges.edges} + else {C.edges.edges} +} +test expect { {if_example} is sat} \ No newline at end of file diff --git a/forge/tests/error/main.rkt b/forge/tests/error/main.rkt index 8b740dfc..0c054bfe 100644 --- a/forge/tests/error/main.rkt +++ b/forge/tests/error/main.rkt @@ -39,6 +39,7 @@ ;;;;;;; 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 + (list "./loc/ifte-error.frg" #rx"ifte-error.frg:9:5.*If-then-else needed consistent types") (list "piecewise-bind-repeat.frg" #rx"rebinding detected") (list "piecewise-bind-combine.frg" #rx"may not be combined with complete bounds") From 162c711d0fd1e16d253afe720ac2fe97b29446c1 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Thu, 14 Mar 2024 08:34:34 -0400 Subject: [PATCH 18/27] prototype fix for pfunc breaker variable names --- forge/breaks.rkt | 29 ++++++++++++++--------------- forge/lang/ast.rkt | 6 +++--- 2 files changed, 17 insertions(+), 18 deletions(-) diff --git a/forge/breaks.rkt b/forge/breaks.rkt index b48abac2..2b8954fd 100644 --- 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 index 119bc397..50349998 100644 --- 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)) From 70df030948690749896323da9360120158f5776b Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Thu, 14 Mar 2024 09:36:22 -0400 Subject: [PATCH 19/27] further progress, repair missing stxloc. todo: error in breakers.frg test --- forge/breaks.rkt | 22 +++++----- forge/lang/expander.rkt | 52 +++++++++++++++--------- forge/last-checker.rkt | 2 +- forge/sigs-structs.rkt | 5 ++- forge/tests/forge/relations/breakers.frg | 5 +-- 5 files changed, 49 insertions(+), 37 deletions(-) diff --git a/forge/breaks.rkt b/forge/breaks.rkt index 2b8954fd..9a666ec8 100644 --- a/forge/breaks.rkt +++ b/forge/breaks.rkt @@ -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 @@ -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 diff --git a/forge/lang/expander.rkt b/forge/lang/expander.rkt index 7b4f638c..b43d4501 100644 --- a/forge/lang/expander.rkt +++ b/forge/lang/expander.rkt @@ -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 @@ -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 @@ -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 @@ -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" @@ -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) @@ -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))) @@ -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))))))))])) @@ -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))) @@ -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.) @@ -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 @@ -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)) @@ -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) @@ -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) @@ -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 ...)) diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index 769dab14..c4de5b39 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -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. diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index df431976..5a1cd738 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -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 diff --git a/forge/tests/forge/relations/breakers.frg b/forge/tests/forge/relations/breakers.frg index 28a75d74..29214a70 100644 --- a/forge/tests/forge/relations/breakers.frg +++ b/forge/tests/forge/relations/breakers.frg @@ -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" ----- From 5e45b2103e49301f2a4ab697a3bcca53c414a9d2 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Thu, 14 Mar 2024 10:30:00 -0400 Subject: [PATCH 20/27] resolve old error --- forge/lang/alloy-syntax/parser.rkt | 2 +- forge/tests/error/main.rkt | 2 ++ forge/tests/error/malformed-test-double.frg | 5 +++++ forge/tests/forge/relations/breakers.frg | 3 --- 4 files changed, 8 insertions(+), 4 deletions(-) create mode 100644 forge/tests/error/malformed-test-double.frg diff --git a/forge/lang/alloy-syntax/parser.rkt b/forge/lang/alloy-syntax/parser.rkt index 982d85e8..6485e5cb 100644 --- a/forge/lang/alloy-syntax/parser.rkt +++ b/forge/lang/alloy-syntax/parser.rkt @@ -85,7 +85,7 @@ ParaDecls : /LEFT-PAREN-TOK @ParaDeclList? /RIGHT-PAREN-TOK AssertDecl : /ASSERT-TOK Name? Block CmdDecl : (Name /COLON-TOK)? (RUN-TOK | CHECK-TOK) (QualName | Block)? Scope? (/FOR-TOK Bounds)? -TestDecl : (Name /COLON-TOK)? (QualName | Block)? Scope? (/FOR-TOK Bounds)? /IS-TOK +TestDecl : (Name /COLON-TOK)? (QualName | Block) Scope? (/FOR-TOK Bounds)? /IS-TOK (SAT-TOK | UNSAT-TOK | THEOREM-TOK | FORGE_ERROR-TOK) TestExpectDecl : TEST-TOK? EXPECT-TOK Name? TestBlock TestBlock : /LEFT-CURLY-TOK TestDecl* /RIGHT-CURLY-TOK diff --git a/forge/tests/error/main.rkt b/forge/tests/error/main.rkt index 0c054bfe..92c4ee03 100644 --- a/forge/tests/error/main.rkt +++ b/forge/tests/error/main.rkt @@ -35,6 +35,8 @@ ;(list "expect-fun-no-args.frg" #rx"TODO") ;;;;;;;;;;;;;;;;;;;;;;;; + + (list "./malformed-test-double.frg" #rx"FOR-TOK") ;; regression ;;;;;;; Source locations ;;;;;;; (list "./loc/sig_use_loc_error.frg" #rx"sig_use_loc_error.frg:7:39") ; vs. reachable diff --git a/forge/tests/error/malformed-test-double.frg b/forge/tests/error/malformed-test-double.frg new file mode 100644 index 00000000..d334f228 --- /dev/null +++ b/forge/tests/error/malformed-test-double.frg @@ -0,0 +1,5 @@ +#lang forge + +test expect { + {} is sat for {} is sat +} \ No newline at end of file diff --git a/forge/tests/forge/relations/breakers.frg b/forge/tests/forge/relations/breakers.frg index 29214a70..988eea1b 100644 --- a/forge/tests/forge/relations/breakers.frg +++ b/forge/tests/forge/relations/breakers.frg @@ -44,9 +44,6 @@ 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 - -- expander.rkt:701:40: preds: attribute contains non-syntax value - -- BAD_ERROR_2: {no l} is sat for {A = `A0 + `A1} is sat - ----- test "linear" ----- linearPossible: {} for {next is linear} is sat From 5b33114581d53c551d47af502ce0584c9d02cc8b Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Sat, 16 Mar 2024 11:57:52 -0400 Subject: [PATCH 21/27] revise tests after merge --- forge/tests/forge/other/ast-errors.frg | 34 ++++++++++++++++---------- 1 file changed, 21 insertions(+), 13 deletions(-) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 4de2c47e..71e85f81 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -129,26 +129,34 @@ test expect { -- 0-ary join result zero_arity_join_result: {some Nim.Nim} is forge_error - -- Variable-name shadowing across quantification - variable_name_shadowing: { some x: Person | all x: Person | some x } is forge_error + -- Variable-name shadowing: this is an ergonomic issue. In basic examples, the need for + -- an error is "obvious". But even the Forge developers re-use variable names in helper + -- predicates, and so a very strict shadowing check would be annoying at best. We're + -- sticking with shadowing checks on *identity*, rather than *user-facing name*. + -- Thus, these tests won't be run: + + -- Shadowing across quantification + --variable_name_shadowing: { some x: Person | all x: Person | some x } is forge_error -- Variable-name shadowing between quantification and comprehension - quant_comp_variable_shadowing: {some {x : Person | some x: Person | some x.age}} is forge_error + --quant_comp_variable_shadowing: {some {x : Person | some x: Person | some x.age}} is forge_error -- Same as above, but in the other direction - comp_quant_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is forge_error + --comp_quant_variable_shadowing: {some x: Person | some {x : Person | some x.age}} is forge_error -- Variable-name shadowing between nested comprehensions - nested_comp_variable_shadowing: {some {x: Person | some {x: Person | some x.age} }} is forge_error + --nested_comp_variable_shadowing: {some {x: Person | some {x: Person | some x.age} }} is forge_error + + -- Regression test: checker must descend into RHS of a minus, even if the RHS has no impact + -- on the inferred type of the expression. + set_minus_rhs_empty_join: { some Person - (age.Nim) } is forge_error - -- TODO -- - - -- Variable-name shadowing within a single comprehension - -- internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b FORGE error + -- TODO -- -- Minus operator: check RHS for validity, allow chaining - -- set_minus_rhs: {all x: Person, y: Person - x | x != y} is theorem -- should be OK + set_minus_rhs: {all x: Person, y: Person - x | x != y} is theorem -- should be OK + + -- TODO -- + -- Regression test: shadowing within a single comprehension will (without a check) cause Pardinus to crash. + internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b FORGE error --- Regression test: checker must descend into RHS of a minus, even if the RHS has no impact - -- on the inferred type of the expression. - set_minus_rhs_empty_join: { some Person - (age.Nim) } is forge_error } From 2ca5bf5788f718764e9aa5f3495cd43f24bf6c75 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Sat, 16 Mar 2024 13:00:22 -0400 Subject: [PATCH 22/27] working simultaneously on: shadowing (todo: comp. case, use identity not name); inferring atom types for evaluator --- forge/last-checker.rkt | 53 ++++++++++--------- forge/server/forgeserver.rkt | 7 ++- forge/sigs-functional.rkt | 2 +- forge/sigs-structs.rkt | 6 ++- .../tests/forge-core/other/multiple-runs.rkt | 23 +++++++- forge/tests/forge/other/ast-errors.frg | 11 ++-- 6 files changed, 67 insertions(+), 35 deletions(-) diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index 28d10f0f..50220eec 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -92,27 +92,33 @@ (check-and-output formula node/formula/quantified checker-hash - (begin (for-each - (lambda (decl) - (let ([var (car decl)] - [domain (cdr decl)]) - ; CHECK: shadowed variables - ; It does NOT suffice to do: (assoc var quantvars), since we now give variables - ; distinct gensym suffixes to help with disambiguation. - (when (ormap (lambda (qvd) - (equal? - (node/expr/quantifier-var-name var) - (node/expr/quantifier-var-name (first qvd)))) quantvars) - (raise-forge-error - #:msg (format "Nested re-use of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) - #:context var)) - ; CHECK: recur into domain(s) - (checkExpression run-or-state domain quantvars checker-hash))) - decls) - ; Extend domain environment - (let ([new-quantvars (append (map assocify decls) quantvars)]) - ; CHECK: recur into subformula - (checkFormula run-or-state subform new-quantvars checker-hash))))] + (begin + ; The new set of quantified variables will be extended by the variables declared here. + ; When checking the domains of each, need to make the _prior_ decls available. + + (let ([new-quantvars + (foldl + (lambda (decl sofar) + (let ([var (car decl)] + [domain (cdr decl)]) + ; CHECK: shadowed variables + ; It does NOT suffice to do: (assoc var quantvars), since we now give variables + ; distinct gensym suffixes to help with disambiguation. + (when (ormap (lambda (qvd) + (equal? + (node/expr/quantifier-var-name var) + (node/expr/quantifier-var-name (first qvd)))) quantvars) + (raise-forge-error + #:msg (format "Nested re-use of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var) + #:context var)) + ; CHECK: recur into domain(s), carrying decls from prior quantifiers + ; (but not this one!) + (checkExpression run-or-state domain sofar checker-hash) + ; Add to _end_ of the list, to maintain ordering + (reverse (cons (assocify decl) (reverse sofar))))) + quantvars decls)]) + ; CHECK: recur into subformula (with extended variable environment) + (checkFormula run-or-state subform new-quantvars checker-hash))))] [(node/formula/sealed info) (checkFormula run-or-state info quantvars)] [else (error (format "no matching case in checkFormula for ~a" (deparse formula)))])) @@ -453,14 +459,13 @@ (check-and-output expr node/expr/comprehension checker-hash + ; For rationale here, see the quantified-formula case. This differs slightly + ; because a comprehension is an expression, and thus needs to report its type. (cons (let ([child-values (map (lambda (decl) (let ([var (car decl)] [domain (cdr decl)]) - ;(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. (when (ormap (lambda (qvd) (equal? (node/expr/quantifier-var-name var) diff --git a/forge/server/forgeserver.rkt b/forge/server/forgeserver.rkt index c72d267d..c86a3857 100644 --- a/forge/server/forgeserver.rkt +++ b/forge/server/forgeserver.rkt @@ -50,11 +50,14 @@ (define id-to-instance-map (make-hash)) ; mutable hash (define (get-current-instance) - (tree:get-value current-tree)) + (define returned-instance (tree:get-value current-tree)) + (set-box! (Run-last-sterling-instance the-run) returned-instance) + returned-instance) (define (get-next-instance [next-mode 'P]) (set! current-tree (tree:get-child current-tree next-mode)) (set! curr-datum-id (+ curr-datum-id 1)) - (hash-set! id-to-instance-map curr-datum-id (get-current-instance)) + ; get-current-instance updates the Run's last sterling instance cursor when called + (hash-set! id-to-instance-map curr-datum-id (get-current-instance)) (values curr-datum-id (get-current-instance))) (define command-string (format "~a" (syntax->datum command))) diff --git a/forge/sigs-functional.rkt b/forge/sigs-functional.rkt index 39e3b187..7e4aab7a 100644 --- a/forge/sigs-functional.rkt +++ b/forge/sigs-functional.rkt @@ -632,7 +632,7 @@ (define-values (result atoms server-ports kodkod-currents kodkod-bounds) (send-to-kodkod spec command #:run-name name)) - (Run name command spec result server-ports atoms kodkod-currents kodkod-bounds)) + (Run name command spec result server-ports atoms kodkod-currents kodkod-bounds (box #f))) ;; NOTE WELL: make sure not to re-use run names; this will cause an diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index 5a1cd738..79f25888 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -210,11 +210,15 @@ [name symbol?] [command syntax?] [run-spec Run-spec?] + ; This is the *start* of the exploration tree [result tree:node?] [server-ports Server-ports?] [atoms (listof (or/c symbol? number?))] [kodkod-currents Kodkod-current?] - [kodkod-bounds (listof any/c)] ; TODO: specify + [kodkod-bounds (listof any/c)] + ; This is Sterling's current cursor into the exploration tree. + ; It is mutated whenever Sterling asks for a new instance. + [last-sterling-instance (box/c (or/c false/c tree:node?))] ) #:transparent) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/forge/tests/forge-core/other/multiple-runs.rkt b/forge/tests/forge-core/other/multiple-runs.rkt index 34ac5e27..1b9d89f0 100644 --- a/forge/tests/forge-core/other/multiple-runs.rkt +++ b/forge/tests/forge-core/other/multiple-runs.rkt @@ -61,12 +61,31 @@ (check-eq? (length (evaluate sat-run-B 'unused B)) 2) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Check that we can close a run without closing others +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; Check that we can close a run (forge:close-run sat-run-A) -; and still get (new) results from other runs +; still get (new) results from other runs (define b3 (sat-B-gen)) (check-eq? (Sat? b3) #t) (check-not-eq? (first (Sat-instances b3)) (first (Sat-instances b2))) (check-not-eq? (first (Sat-instances b3)) (first (Sat-instances b1))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Check behavior if we get a 2nd generator for the same run +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; Different generators re-start the model enumeration from the beginning, assuming +; the sequence of generator-arguments (e.g., 'next) is the same. +(define sat-B-gen-2 (forge:make-model-generator (forge:get-result sat-run-B) 'next)) +(define b1-2 (sat-B-gen-2)) +(define b2-2 (sat-B-gen-2)) +(define b3-2 (sat-B-gen-2)) +(define b4-2 (sat-B-gen-2)) +(define b4 (sat-B-gen)) + +(check-eq? (first (Sat-instances b1)) (first (Sat-instances b1-2))) +(check-eq? (first (Sat-instances b2)) (first (Sat-instances b2-2))) +(check-eq? (first (Sat-instances b3)) (first (Sat-instances b3-2))) +(check-eq? (first (Sat-instances b4)) (first (Sat-instances b4-2))) diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg index 71e85f81..8bd22b6b 100644 --- a/forge/tests/forge/other/ast-errors.frg +++ b/forge/tests/forge/other/ast-errors.frg @@ -148,14 +148,15 @@ test expect { -- on the inferred type of the expression. set_minus_rhs_empty_join: { some Person - (age.Nim) } is forge_error - - -- TODO -- -- Minus operator: check RHS for validity, allow chaining - set_minus_rhs: {all x: Person, y: Person - x | x != y} is theorem -- should be OK + set_minus_rhs_quant: {all x: Person, y: Person - x | x != y} is theorem -- should be OK + set_minus_rhs_comp: {some {x: Person, y: Person - x | x != y}} is theorem -- should be OK + -- TODO -- - -- Regression test: shadowing within a single comprehension will (without a check) cause Pardinus to crash. - internal_comp_variable_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b FORGE error + -- Regression test: shadowing within a single comprehension or quantifier would cause Pardinus to crash. + internal_comp_variable_name_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b FORGE error + internal_quant_variable_name_shadowing: {some x: Person, x: Person | x.age = x.age} is sat } From 2790b492206b6b46e5e22911b0d15693672c682c Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Sun, 17 Mar 2024 08:37:51 -0400 Subject: [PATCH 23/27] add: sterling PR 16: target/source index --- forge/sigs-structs.rkt | 2 +- forge/sterling/README.md | 4 +++- forge/sterling/build/6007.bundle.js | 2 -- forge/sterling/build/6563.bundle.js | 2 ++ ...{6007.bundle.js.LICENSE.txt => 6563.bundle.js.LICENSE.txt} | 0 forge/sterling/build/index.html | 2 +- forge/sterling/build/main.bundle.js | 2 +- 7 files changed, 8 insertions(+), 6 deletions(-) delete mode 100644 forge/sterling/build/6007.bundle.js create mode 100644 forge/sterling/build/6563.bundle.js rename forge/sterling/build/{6007.bundle.js.LICENSE.txt => 6563.bundle.js.LICENSE.txt} (100%) diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index 79f25888..cc2fc948 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -218,7 +218,7 @@ [kodkod-bounds (listof any/c)] ; This is Sterling's current cursor into the exploration tree. ; It is mutated whenever Sterling asks for a new instance. - [last-sterling-instance (box/c (or/c false/c tree:node?))] + [last-sterling-instance (box/c (or/c Sat? Unsat? false/c))] ) #:transparent) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/forge/sterling/README.md b/forge/sterling/README.md index d3089f14..cafa2cc0 100644 --- a/forge/sterling/README.md +++ b/forge/sterling/README.md @@ -1 +1,3 @@ -This folder contains a build of the current version of Sterling. +This folder contains a build of the current version of Sterling for Forge. To update, build Sterling and recursively copy the contents of the `dist` folder in that repo to the `build` sub-folder here. Remember to build with `yarn run build:forge`; the Forge version is slightly different from the Alloy version. + + diff --git a/forge/sterling/build/6007.bundle.js b/forge/sterling/build/6007.bundle.js deleted file mode 100644 index 885780ea..00000000 --- a/forge/sterling/build/6007.bundle.js +++ /dev/null @@ -1,2 +0,0 @@ -/*! For license information please see 6007.bundle.js.LICENSE.txt */ -(self.webpackChunksterling_ts=self.webpackChunksterling_ts||[]).push([[6007],{68921:(e,t,n)=>{"use strict";n.d(t,{zx:()=>E,hE:()=>C,hU:()=>T});var i=n(97375),o=n(105),r=n(44592),s=n(38554),a=n.n(s),l=n(67294),c=n(26450),d=n(70917),u=n(1358);function h(){return h=Object.assign||function(e){for(var t=1;t=0||(o[n]=e[n]);return o}(i,g),w=(0,r.cx)("chakra-spinner",b),C=h({display:"inline-block",borderColor:"currentColor",borderStyle:"solid",borderRadius:"99999px",borderWidth:d,borderBottomColor:_,borderLeftColor:_,animation:p+" "+m+" linear infinite"},n);return l.createElement(o.m$.div,h({ref:t,__css:C,className:w},y),a&&l.createElement(u.TX,null,a))}));function m(e,t){if(null==e)return{};var n,i,o={},r=Object.keys(e);for(i=0;i=0||(o[n]=e[n]);return o}function v(){return v=Object.assign||function(e){for(var t=1;t *:first-of-type:not(:last-of-type)":{borderEndRadius:0},"> *:not(:first-of-type):not(:last-of-type)":{borderRadius:0},"> *:not(:first-of-type):last-of-type":{borderStartRadius:0}}:{"& > *:not(style) ~ *:not(style)":{marginStart:d}}),l.createElement(y,{value:f},l.createElement(o.m$.div,v({ref:t,role:"group",__css:b,className:p},g)))}));r.Ts&&(C.displayName="ButtonGroup");var S=["label","placement","spacing","children","className","__css"],x=function(e){var t=e.label,n=e.placement;e.spacing;var i=e.children,s=void 0===i?l.createElement(f,{color:"currentColor",width:"1em",height:"1em"}):i,a=e.className,c=e.__css,d=m(e,S),u=(0,r.cx)("chakra-button__spinner",a),h="start"===n?"marginEnd":"marginStart",g=l.useMemo((function(){var e;return v(((e={display:"flex",alignItems:"center",position:t?"relative":"absolute"})[h]=t?"0.5rem":0,e.fontSize="1em",e.lineHeight="normal",e),c)}),[c,t,h]);return l.createElement(o.m$.div,v({className:u},d,{__css:g}),s)};r.Ts&&(x.displayName="ButtonSpinner");var k=["children","className"],L=function(e){var t=e.children,n=e.className,i=m(e,k),s=l.isValidElement(t)?l.cloneElement(t,{"aria-hidden":!0,focusable:!1}):t,a=(0,r.cx)("chakra-button__icon",n);return l.createElement(o.m$.span,v({display:"inline-flex",alignSelf:"center",flexShrink:0},i,{className:a}),s)};r.Ts&&(L.displayName="ButtonIcon");var N=["isDisabled","isLoading","isActive","isFullWidth","children","leftIcon","rightIcon","loadingText","iconSpacing","type","spinner","spinnerPlacement","className","as"],E=(0,o.Gp)((function(e,t){var n,s,c,d,u=w(),h=(0,o.mq)("Button",v({},u,e)),g=(0,o.Lr)(e),p=g.isDisabled,f=void 0===p?null==u?void 0:u.isDisabled:p,_=g.isLoading,b=g.isActive,y=g.isFullWidth,C=g.children,S=g.leftIcon,k=g.rightIcon,L=g.loadingText,E=g.iconSpacing,I=void 0===E?"0.5rem":E,T=g.type,M=g.spinner,A=g.spinnerPlacement,O=void 0===A?"start":A,R=g.className,P=g.as,F=m(g,N),B=l.useMemo((function(){var e,t=a()({},null!=(e=null==h?void 0:h._focus)?e:{},{zIndex:1});return v({display:"inline-flex",appearance:"none",alignItems:"center",justifyContent:"center",userSelect:"none",position:"relative",whiteSpace:"nowrap",verticalAlign:"middle",outline:"none",width:y?"100%":"auto"},h,!!u&&{_focus:t})}),[h,u,y]),W=(n=P,c=(s=l.useState(!n))[0],d=s[1],{ref:l.useCallback((function(e){e&&d("BUTTON"===e.tagName)}),[]),type:c?"button":void 0}),V=W.ref,z=W.type,H={rightIcon:k,leftIcon:S,iconSpacing:I,children:C};return l.createElement(o.m$.button,v({disabled:f||_,ref:(0,i.qq)(t,V),as:P,type:null!=T?T:z,"data-active":(0,r.PB)(b),"data-loading":(0,r.PB)(_),__css:B,className:(0,r.cx)("chakra-button",R)},F),_&&"start"===O&&l.createElement(x,{className:"chakra-button__spinner--start",label:L,placement:"start"},M),_?L||l.createElement(o.m$.span,{opacity:0},l.createElement(D,H)):l.createElement(D,H),_&&"end"===O&&l.createElement(x,{className:"chakra-button__spinner--end",label:L,placement:"end"},M))}));function D(e){var t=e.leftIcon,n=e.rightIcon,i=e.children,o=e.iconSpacing;return l.createElement(l.Fragment,null,t&&l.createElement(L,{marginEnd:o},t),i,n&&l.createElement(L,{marginStart:o},n))}r.Ts&&(E.displayName="Button");var I=["icon","children","isRound","aria-label"],T=(0,o.Gp)((function(e,t){var n=e.icon,i=e.children,o=e.isRound,r=e["aria-label"],s=m(e,I),a=n||i,c=l.isValidElement(a)?l.cloneElement(a,{"aria-hidden":!0,focusable:!1}):null;return l.createElement(E,v({padding:"0",borderRadius:o?"full":void 0,ref:t,"aria-label":r},s),c)}));r.Ts&&(T.displayName="IconButton")},68133:(e,t,n)=>{"use strict";n.d(t,{XZ:()=>L});var i=n(44592),o=n(26450),r=n(67294),s=n(97375),a=n(105),l=n(99860),c=n(53869),d=n(1358);function u(){return u=Object.assign||function(e){for(var t=1;t=0||(o[n]=e[n]);return o}i.Ts;var f=["isIndeterminate","isChecked"],m="custom"in l.E?l.E.custom(a.m$.svg):(0,l.E)(a.m$.svg),v=function(e){return r.createElement(m,u({width:"1.2em",viewBox:"0 0 12 10",variants:{unchecked:{opacity:0,strokeDashoffset:16},checked:{opacity:1,strokeDashoffset:0,transition:{duration:.2}}},style:{fill:"none",strokeWidth:2,stroke:"currentColor",strokeDasharray:16}},e),r.createElement("polyline",{points:"1.5 6 4.5 9 10.5 1"}))},_=function(e){return r.createElement(m,u({width:"1.2em",viewBox:"0 0 24 24",variants:{unchecked:{scaleX:.65,opacity:0},checked:{scaleX:1,opacity:1,transition:{scaleX:{duration:0},opacity:{duration:.02}}}},style:{stroke:"currentColor",strokeWidth:4}},e),r.createElement("line",{x1:"21",x2:"3",y1:"12",y2:"12"}))},b=function(e){var t=e.open,n=e.children;return r.createElement(c.M,{initial:!1},t&&r.createElement(l.E.div,{variants:{unchecked:{scale:.5},checked:{scale:1}},initial:"unchecked",animate:"checked",exit:"unchecked",style:{display:"flex",alignItems:"center",justifyContent:"center",height:"100%"}},n))},y=function(e){var t=e.isIndeterminate,n=e.isChecked,i=p(e,f),o=t?_:v;return r.createElement(b,{open:n||t},r.createElement(o,i))},w=["defaultIsChecked","defaultChecked","isChecked","isFocusable","isDisabled","isReadOnly","isRequired","onChange","isIndeterminate","isInvalid","name","value","id","onBlur","onFocus","tabIndex","aria-label","aria-labelledby","aria-invalid","aria-describedby"];function C(e){e.preventDefault(),e.stopPropagation()}var S=["spacing","className","children","iconColor","iconSize","icon","isChecked","isDisabled","onChange"],x=(0,a.m$)("span",{baseStyle:{display:"inline-flex",alignItems:"center",justifyContent:"center",verticalAlign:"top",userSelect:"none",flexShrink:0}}),k=(0,a.m$)("label",{baseStyle:{cursor:"pointer",display:"inline-flex",alignItems:"center",verticalAlign:"top",position:"relative",_disabled:{cursor:"not-allowed"}}}),L=(0,a.Gp)((function(e,t){var n=g(),l=u({},n,e),c=(0,a.jC)("Checkbox",l),h=(0,a.Lr)(e),f=h.spacing,m=void 0===f?"0.5rem":f,v=h.className,_=h.children,b=h.iconColor,L=h.iconSize,N=h.icon,E=void 0===N?r.createElement(y,null):N,D=h.isChecked,I=h.isDisabled,T=void 0===I?null==n?void 0:n.isDisabled:I,M=h.onChange,A=p(h,S),O=D;null!=n&&n.value&&h.value&&(O=n.value.includes(h.value));var R=M;null!=n&&n.onChange&&h.value&&(R=(0,i.PP)(n.onChange,M));var P=function(e){void 0===e&&(e={});var t=e,n=t.defaultIsChecked,a=t.defaultChecked,l=void 0===a?n:a,c=t.isChecked,h=t.isFocusable,g=t.isDisabled,f=t.isReadOnly,m=t.isRequired,v=t.onChange,_=t.isIndeterminate,b=t.isInvalid,y=t.name,S=t.value,x=t.id,k=t.onBlur,L=t.onFocus,N=t.tabIndex,E=void 0===N?void 0:N,D=t["aria-label"],I=t["aria-labelledby"],T=t["aria-invalid"],M=t["aria-describedby"],A=p(t,w),O=(0,s.W6)(v),R=(0,s.W6)(k),P=(0,s.W6)(L),F=(0,s.kt)(),B=F[0],W=F[1],V=(0,s.kt)(),z=V[0],H=V[1],j=(0,s.kt)(),U=j[0],K=j[1],$=(0,r.useRef)(null),q=(0,r.useState)(!0),Z=q[0],G=q[1],Y=(0,r.useState)(!!l),Q=Y[0],X=Y[1],J=(0,s.pY)(c,Q),ee=J[0],te=J[1];(0,i.ZK)({condition:!!n,message:'The "defaultIsChecked" prop has been deprecated and will be removed in a future version. Please use the "defaultChecked" prop instead, which mirrors default React checkbox behavior.'});var ne=(0,r.useCallback)((function(e){f||g?e.preventDefault():(ee||X(te?e.target.checked:!!_||e.target.checked),null==O||O(e))}),[f,g,te,ee,_,O]);(0,s.Gw)((function(){$.current&&($.current.indeterminate=Boolean(_))}),[_]);var ie=g&&!h,oe=(0,r.useCallback)((function(e){" "===e.key&&K.on()}),[K]),re=(0,r.useCallback)((function(e){" "===e.key&&K.off()}),[K]);(0,s.Gw)((function(){$.current&&$.current.checked!==te&&X($.current.checked)}),[$.current]);var se=(0,r.useCallback)((function(e,t){return void 0===e&&(e={}),void 0===t&&(t=null),u({},e,{ref:t,"data-active":(0,i.PB)(U),"data-hover":(0,i.PB)(z),"data-checked":(0,i.PB)(te),"data-focus":(0,i.PB)(B),"data-indeterminate":(0,i.PB)(_),"data-disabled":(0,i.PB)(g),"data-invalid":(0,i.PB)(b),"data-readonly":(0,i.PB)(f),"aria-hidden":!0,onMouseDown:(0,i.v0)(e.onMouseDown,(function(e){e.preventDefault(),K.on()})),onMouseUp:(0,i.v0)(e.onMouseUp,K.off),onMouseEnter:(0,i.v0)(e.onMouseEnter,H.on),onMouseLeave:(0,i.v0)(e.onMouseLeave,H.off)})}),[U,te,g,B,z,_,b,f,K,H.off,H.on]),ae=(0,r.useCallback)((function(e,t){return void 0===e&&(e={}),void 0===t&&(t=null),u({},A,e,{ref:(0,o.lq)(t,(function(e){e&&G("LABEL"===e.tagName)})),onClick:(0,i.v0)(e.onClick,(function(){var e;Z||(null==(e=$.current)||e.click(),(0,i.T_)($.current,{nextTick:!0}))})),"data-disabled":(0,i.PB)(g),"data-checked":(0,i.PB)(te),"data-invalid":(0,i.PB)(b)})}),[A,g,te,b,Z]),le=(0,r.useCallback)((function(e,t){return void 0===e&&(e={}),void 0===t&&(t=null),u({},e,{ref:(0,o.lq)($,t),type:"checkbox",name:y,value:S,id:x,tabIndex:E,onChange:(0,i.v0)(e.onChange,ne),onBlur:(0,i.v0)(e.onBlur,R,W.off),onFocus:(0,i.v0)(e.onFocus,P,W.on),onKeyDown:(0,i.v0)(e.onKeyDown,oe),onKeyUp:(0,i.v0)(e.onKeyUp,re),required:m,checked:te,disabled:ie,readOnly:f,"aria-label":D,"aria-labelledby":I,"aria-invalid":T?Boolean(T):b,"aria-describedby":M,"aria-disabled":g,style:d.NL})}),[y,S,x,ne,W.off,W.on,R,P,oe,re,m,te,ie,f,D,I,T,b,M,g,E]),ce=(0,r.useCallback)((function(e,t){return void 0===e&&(e={}),void 0===t&&(t=null),u({},e,{ref:t,onMouseDown:(0,i.v0)(e.onMouseDown,C),onTouchStart:(0,i.v0)(e.onTouchStart,C),"data-disabled":(0,i.PB)(g),"data-checked":(0,i.PB)(te),"data-invalid":(0,i.PB)(b)})}),[te,g,b]);return{state:{isInvalid:b,isFocused:B,isChecked:te,isActive:U,isHovered:z,isIndeterminate:_,isDisabled:g,isReadOnly:f,isRequired:m},getRootProps:ae,getCheckboxProps:se,getInputProps:le,getLabelProps:ce,htmlProps:A}}(u({},A,{isDisabled:T,isChecked:O,onChange:R})),F=P.state,B=P.getInputProps,W=P.getCheckboxProps,V=P.getLabelProps,z=P.getRootProps,H=r.useMemo((function(){return u({opacity:F.isChecked||F.isIndeterminate?1:0,transform:F.isChecked||F.isIndeterminate?"scale(1)":"scale(0.95)",fontSize:L,color:b},c.icon)}),[b,L,F.isChecked,F.isIndeterminate,c.icon]),j=r.cloneElement(E,{__css:H,isIndeterminate:F.isIndeterminate,isChecked:F.isChecked});return r.createElement(k,u({__css:c.container,className:(0,i.cx)("chakra-checkbox",v)},z()),r.createElement("input",u({className:"chakra-checkbox__input"},B({},t))),r.createElement(x,u({__css:c.control,className:"chakra-checkbox__control"},W()),j),_&&r.createElement(a.m$.span,u({className:"chakra-checkbox__label"},V(),{__css:u({marginStart:m},c.label)}),_))}));i.Ts&&(L.displayName="Checkbox")},84746:(e,t,n)=>{"use strict";n.d(t,{P:()=>d});var i=n(10894),o=n(105),r=n(44592),s=n(67294);function a(){return a=Object.assign||function(e){for(var t=1;t=0||(o[n]=e[n]);return o}(i,l);return s.createElement(o.m$.button,a({type:"button","aria-label":"Close",ref:t,disabled:d,__css:a({},{outline:0,display:"flex",alignItems:"center",justifyContent:"center",flexShrink:0},n,u)},h),r||s.createElement(c,{width:"1em",height:"1em"}))}));r.Ts&&(d.displayName="CloseButton")},20949:(e,t,n)=>{"use strict";n.d(t,{kc:()=>f,SG:()=>v,If:()=>m});var i=n(85393),o=n(44592),r=n(67294),s="chakra-ui-light",a="chakra-ui-dark",l={classList:{add:o.ZT,remove:o.ZT}};var c="(prefers-color-scheme: dark)";var d=function(){return document.documentElement.style.getPropertyValue("--chakra-ui-color-mode")},u=function(e){o.jU&&document.documentElement.style.setProperty("--chakra-ui-color-mode",e)},h=function(){return"undefined"!=typeof Storage},g="chakra-ui-color-mode",p={get:function(e){if(!h())return e;try{var t=localStorage.getItem(g);return null!=t?t:e}catch(t){return o.Ts&&console.log(t),e}},set:function(e){if(h())try{localStorage.setItem(g,e)}catch(e){o.Ts&&console.log(e)}},type:"localStorage"},f=r.createContext({});o.Ts&&(f.displayName="ColorModeContext");var m=function(){var e=r.useContext(f);if(void 0===e)throw new Error("useColorMode must be used within a ColorModeProvider");return e};function v(e){var t=e.value,n=e.children,h=e.options,g=h.useSystemColorMode,m=h.initialColorMode,v=e.colorModeManager,_=void 0===v?p:v,b="dark"===m?"dark":"light",y=r.useState("cookie"===_.type?_.get(b):b),w=y[0],C=y[1],S=(0,i.O)().document;r.useEffect((function(){if(o.jU&&"localStorage"===_.type){var e=(i=b,(null!=(r=function(e){var t=null==window.matchMedia?void 0:window.matchMedia("(prefers-color-scheme: dark)");if(t)return!!t.media===t.matches}())?r:"dark"===i)?"dark":"light");if(g)return C(e);var t=d(),n=_.get();return C(t||(n||("system"===m?e:b)))}var i,r}),[_,g,b,m]),r.useEffect((function(){var e="dark"===w;(function(e,t){var n=function(e){return o.jU?e.body:l}(t);n.classList.add(e?a:s),n.classList.remove(e?s:a)})(e,S),u(e?"dark":"light")}),[w,S]);var x=r.useCallback((function(e,t){if(void 0===t&&(t=!1),t){if(_.get()&&!g)return}else _.set(e);C(e)}),[_,g]),k=r.useCallback((function(){x("light"===w?"dark":"light")}),[w,x]);r.useEffect((function(){var e,t=g||"system"===m;return t&&(e=function(e){if(!("matchMedia"in window))return o.ZT;var t=window.matchMedia(c),n=function(){e(t.matches?"dark":"light",!0)};return t.addEventListener("change",n),function(){t.removeEventListener("change",n)}}(x)),function(){e&&t&&e()}}),[x,g,m]);var L=r.useMemo((function(){return{colorMode:null!=t?t:w,toggleColorMode:t?o.ZT:k,setColorMode:t?o.ZT:x}}),[w,x,k,t]);return r.createElement(f.Provider,{value:L},n)}o.Ts&&(v.displayName="ColorModeProvider"),o.Ts,o.Ts},79762:(e,t,n)=>{"use strict";n.d(t,{NI:()=>m,lX:()=>x,Yp:()=>y});var i=n(97375),o=n(105),r=n(44592),s=n(26450),a=n(67294),l=n(10894);function c(){return c=Object.assign||function(e){for(var t=1;t=0||(o[n]=e[n]);return o}var u=["id","isRequired","isInvalid","isDisabled","isReadOnly"],h=["getRootProps","htmlProps"],g=(0,s.kr)({strict:!1,name:"FormControlContext"}),p=g[0],f=g[1],m=(0,o.Gp)((function(e,t){var n=(0,o.jC)("Form",e),l=function(e){var t=e.id,n=e.isRequired,o=e.isInvalid,l=e.isDisabled,h=e.isReadOnly,g=d(e,u),p=(0,i.Me)(),f=t||"field-"+p,m=f+"-label",v=f+"-feedback",_=f+"-helptext",b=a.useState(!1),y=b[0],w=b[1],C=a.useState(!1),S=C[0],x=C[1],k=(0,i.kt)(),L=k[0],N=k[1],E=a.useCallback((function(e,t){return void 0===e&&(e={}),void 0===t&&(t=null),c({id:_},e,{ref:(0,s.lq)(t,(function(e){e&&x(!0)}))})}),[_]),D=a.useCallback((function(e,t){var n,i;return void 0===e&&(e={}),void 0===t&&(t=null),c({},e,{ref:t,"data-focus":(0,r.PB)(L),"data-disabled":(0,r.PB)(l),"data-invalid":(0,r.PB)(o),"data-readonly":(0,r.PB)(h),id:null!=(n=e.id)?n:m,htmlFor:null!=(i=e.htmlFor)?i:f})}),[f,l,L,o,h,m]),I=a.useCallback((function(e,t){return void 0===e&&(e={}),void 0===t&&(t=null),c({id:v},e,{ref:(0,s.lq)(t,(function(e){e&&w(!0)})),"aria-live":"polite"})}),[v]),T=a.useCallback((function(e,t){return void 0===e&&(e={}),void 0===t&&(t=null),c({},e,g,{ref:t,role:"group"})}),[g]),M=a.useCallback((function(e,t){return void 0===e&&(e={}),void 0===t&&(t=null),c({},e,{ref:t,role:"presentation","aria-hidden":!0,children:e.children||"*"})}),[]);return{isRequired:!!n,isInvalid:!!o,isReadOnly:!!h,isDisabled:!!l,isFocused:!!L,onFocus:N.on,onBlur:N.off,hasFeedbackText:y,setHasFeedbackText:w,hasHelpText:S,setHasHelpText:x,id:f,labelId:m,feedbackId:v,helpTextId:_,htmlProps:g,getHelpTextProps:E,getErrorMessageProps:I,getRootProps:T,getLabelProps:D,getRequiredIndicatorProps:M}}((0,o.Lr)(e)),g=l.getRootProps;l.htmlProps;var f=d(l,h),m=(0,r.cx)("chakra-form-control",e.className),v=a.useMemo((function(){return f}),[f]);return a.createElement(p,{value:v},a.createElement(o.Fo,{value:n},a.createElement(o.m$.div,c({},g({},t),{className:m,__css:n.container}))))}));r.Ts&&(m.displayName="FormControl");var v=(0,o.Gp)((function(e,t){var n=f(),i=(0,o.yK)(),s=(0,r.cx)("chakra-form__helper-text",e.className);return a.createElement(o.m$.div,c({},null==n?void 0:n.getHelpTextProps(e,t),{__css:i.helperText,className:s}))}));r.Ts&&(v.displayName="FormHelperText");var _=["isDisabled","isInvalid","isReadOnly","isRequired"],b=["id","disabled","readOnly","required","isRequired","isInvalid","isReadOnly","isDisabled","onFocus","onBlur"];function y(e){var t=function(e){var t,n,i,o=f(),s=e.id,a=e.disabled,l=e.readOnly,u=e.required,h=e.isRequired,g=e.isInvalid,p=e.isReadOnly,m=e.isDisabled,v=e.onFocus,_=e.onBlur,y=d(e,b),w=e["aria-describedby"]?[e["aria-describedby"]]:[];return null!=o&&o.hasFeedbackText&&null!=o&&o.isInvalid&&w.push(o.feedbackId),null!=o&&o.hasHelpText&&w.push(o.helpTextId),c({},y,{"aria-describedby":w.join(" ")||void 0,id:null!=s?s:null==o?void 0:o.id,isDisabled:null!=(t=null!=a?a:m)?t:null==o?void 0:o.isDisabled,isReadOnly:null!=(n=null!=l?l:p)?n:null==o?void 0:o.isReadOnly,isRequired:null!=(i=null!=u?u:h)?i:null==o?void 0:o.isRequired,isInvalid:null!=g?g:null==o?void 0:o.isInvalid,onFocus:(0,r.v0)(null==o?void 0:o.onFocus,v),onBlur:(0,r.v0)(null==o?void 0:o.onBlur,_)})}(e),n=t.isDisabled,i=t.isInvalid,o=t.isReadOnly,s=t.isRequired;return c({},d(t,_),{disabled:n,readOnly:o,required:s,"aria-invalid":(0,r.Qm)(i),"aria-required":(0,r.Qm)(s),"aria-readonly":(0,r.Qm)(o)})}var w=(0,o.Gp)((function(e,t){var n=(0,o.jC)("FormError",e),i=(0,o.Lr)(e),s=f();return null!=s&&s.isInvalid?a.createElement(o.Fo,{value:n},a.createElement(o.m$.div,c({},null==s?void 0:s.getErrorMessageProps(i,t),{className:(0,r.cx)("chakra-form__error-message",e.className),__css:c({display:"flex",alignItems:"center"},n.text)}))):null}));r.Ts&&(w.displayName="FormErrorMessage");var C=(0,o.Gp)((function(e,t){var n=(0,o.yK)(),i=f();if(null==i||!i.isInvalid)return null;var s=(0,r.cx)("chakra-form__error-icon",e.className);return a.createElement(l.ZP,c({ref:t,"aria-hidden":!0},e,{__css:n.icon,className:s}),a.createElement("path",{fill:"currentColor",d:"M11.983,0a12.206,12.206,0,0,0-8.51,3.653A11.8,11.8,0,0,0,0,12.207,11.779,11.779,0,0,0,11.8,24h.214A12.111,12.111,0,0,0,24,11.791h0A11.766,11.766,0,0,0,11.983,0ZM10.5,16.542a1.476,1.476,0,0,1,1.449-1.53h.027a1.527,1.527,0,0,1,1.523,1.47,1.475,1.475,0,0,1-1.449,1.53h-.027A1.529,1.529,0,0,1,10.5,16.542ZM11,12.5v-6a1,1,0,0,1,2,0v6a1,1,0,1,1-2,0Z"}))}));r.Ts&&(C.displayName="FormErrorIcon");var S=["className","children","requiredIndicator"],x=(0,o.Gp)((function(e,t){var n,i=(0,o.mq)("FormLabel",e),s=(0,o.Lr)(e);s.className;var l=s.children,u=s.requiredIndicator,h=void 0===u?a.createElement(k,null):u,g=d(s,S),p=f(),m=null!=(n=null==p?void 0:p.getLabelProps(g,t))?n:c({ref:t},g);return a.createElement(o.m$.label,c({},m,{className:(0,r.cx)("chakra-form__label",s.className),__css:c({display:"block",textAlign:"start"},i)}),l,null!=p&&p.isRequired?h:null)}));r.Ts&&(x.displayName="FormLabel");var k=(0,o.Gp)((function(e,t){var n=f(),i=(0,o.yK)();if(null==n||!n.isRequired)return null;var s=(0,r.cx)("chakra-form__required-indicator",e.className);return a.createElement(o.m$.span,c({},null==n?void 0:n.getRequiredIndicatorProps(e,t),{__css:i.requiredIndicator,className:s}))}));r.Ts&&(k.displayName="RequiredIndicator")},97375:(e,t,n)=>{"use strict";n.d(t,{vc:()=>g,kt:()=>r,W6:()=>a,pY:()=>l,Tx:()=>c,qY:()=>m,OR:()=>v,Ck:()=>b,NW:()=>w,Me:()=>p,ZS:()=>f,qq:()=>S,O3:()=>x,Gw:()=>s,bx:()=>L,KS:()=>N,zq:()=>y,rf:()=>_});var i=n(67294),o=n(44592);function r(e){void 0===e&&(e=!1);var t=(0,i.useState)(e),n=t[0],o=t[1];return[n,{on:(0,i.useCallback)((function(){o(!0)}),[]),off:(0,i.useCallback)((function(){o(!1)}),[]),toggle:(0,i.useCallback)((function(){o((function(e){return!e}))}),[])}]}n(20640);var s=o.jU?i.useLayoutEffect:i.useEffect;function a(e,t){void 0===t&&(t=[]);var n=i.useRef(e);return s((function(){n.current=e})),i.useCallback((function(){for(var e=arguments.length,t=new Array(e),i=0;i1?t-1:0),o=1;o0)&&(!(i&&!(0,o.lZ)(i).body.contains(i))&&!(null!=(n=t.current)&&n.contains(i)))}function L(e){void 0===e&&(e={});var t=e,n=t.timeout,o=void 0===n?300:n,r=t.preventDefault,s=void 0===r?function(){return!0}:r,a=i.useState([]),l=a[0],c=a[1],d=i.useRef(),u=function(){d.current&&(clearTimeout(d.current),d.current=null)};return i.useEffect((function(){return u}),[]),function(e){return function(t){if("Backspace"===t.key){var n=[].concat(l);return n.pop(),void c(n)}if(function(e){var t=e.key;return 1===t.length||t.length>1&&/[^a-zA-Z0-9]/.test(t)}(t)){var i=l.concat(t.key);s(t)&&(t.preventDefault(),t.stopPropagation()),c(i),e(i.join("")),u(),d.current=setTimeout((function(){c([]),d.current=null}),o)}}}}function N(e,t){var n=a(e);i.useEffect((function(){var e;if(null!=t)return e=window.setTimeout((function(){n()}),t),function(){e&&window.clearTimeout(e)}}),[t,n])}},10894:(e,t,n)=>{"use strict";n.d(t,{JO:()=>c,IU:()=>u,ZP:()=>d});var i=n(105),o=n(44592),r=n(67294);function s(){return s=Object.assign||function(e){for(var t=1;t=0||(o[n]=e[n]);return o}(e,a),_={ref:t,focusable:g,className:(0,o.cx)("chakra-icon",f),__css:s({w:"1em",h:"1em",display:"inline-block",lineHeight:"1em",flexShrink:0,color:u},m)},b=null!=c?c:l.viewBox;if(n&&"string"!=typeof n)return r.createElement(i.m$.svg,s({as:n},_,v));var y=null!=p?p:l.path;return r.createElement(i.m$.svg,s({verticalAlign:"middle",viewBox:b},_,v),y)}));o.Ts&&(c.displayName="Icon");var d=c;function u(e){var t=e.viewBox,n=void 0===t?"0 0 24 24":t,a=e.d,l=e.path,d=e.displayName,u=e.defaultProps,h=void 0===u?{}:u,g=(0,i.Gp)((function(e,t){return r.createElement(c,s({ref:t,viewBox:n},h,e),null!=l?l:r.createElement("path",{fill:"currentColor",d:a}))}));return o.Ts&&(g.displayName=d),g}},59876:(e,t,n)=>{"use strict";n.d(t,{XC:()=>r});var i=n(10894),o=n(67294),r=((0,i.IU)({d:"M16 1H4c-1.1 0-2 .9-2 2v14h2V3h12V1zm3 4H8c-1.1 0-2 .9-2 2v14c0 1.1.9 2 2 2h11c1.1 0 2-.9 2-2V7c0-1.1-.9-2-2-2zm0 16H8V7h11v14z",displayName:"CopyIcon"}),(0,i.IU)({d:"M23.384,21.619,16.855,15.09a9.284,9.284,0,1,0-1.768,1.768l6.529,6.529a1.266,1.266,0,0,0,1.768,0A1.251,1.251,0,0,0,23.384,21.619ZM2.75,9.5a6.75,6.75,0,1,1,6.75,6.75A6.758,6.758,0,0,1,2.75,9.5Z",displayName:"SearchIcon"}),(0,i.IU)({d:"M23.414,20.591l-4.645-4.645a10.256,10.256,0,1,0-2.828,2.829l4.645,4.644a2.025,2.025,0,0,0,2.828,0A2,2,0,0,0,23.414,20.591ZM10.25,3.005A7.25,7.25,0,1,1,3,10.255,7.258,7.258,0,0,1,10.25,3.005Z",displayName:"Search2Icon"}),(0,i.IU)({d:"M21.4,13.7C20.6,13.9,19.8,14,19,14c-5,0-9-4-9-9c0-0.8,0.1-1.6,0.3-2.4c0.1-0.3,0-0.7-0.3-1 c-0.3-0.3-0.6-0.4-1-0.3C4.3,2.7,1,7.1,1,12c0,6.1,4.9,11,11,11c4.9,0,9.3-3.3,10.6-8.1c0.1-0.3,0-0.7-0.3-1 C22.1,13.7,21.7,13.6,21.4,13.7z",displayName:"MoonIcon"}),(0,i.IU)({displayName:"SunIcon",path:o.createElement("g",{strokeLinejoin:"round",strokeLinecap:"round",strokeWidth:"2",fill:"none",stroke:"currentColor"},o.createElement("circle",{cx:"12",cy:"12",r:"5"}),o.createElement("path",{d:"M12 1v2"}),o.createElement("path",{d:"M12 21v2"}),o.createElement("path",{d:"M4.22 4.22l1.42 1.42"}),o.createElement("path",{d:"M18.36 18.36l1.42 1.42"}),o.createElement("path",{d:"M1 12h2"}),o.createElement("path",{d:"M21 12h2"}),o.createElement("path",{d:"M4.22 19.78l1.42-1.42"}),o.createElement("path",{d:"M18.36 5.64l1.42-1.42"}))}),(0,i.IU)({d:"M0,12a1.5,1.5,0,0,0,1.5,1.5h8.75a.25.25,0,0,1,.25.25V22.5a1.5,1.5,0,0,0,3,0V13.75a.25.25,0,0,1,.25-.25H22.5a1.5,1.5,0,0,0,0-3H13.75a.25.25,0,0,1-.25-.25V1.5a1.5,1.5,0,0,0-3,0v8.75a.25.25,0,0,1-.25.25H1.5A1.5,1.5,0,0,0,0,12Z",displayName:"AddIcon"}),(0,i.IU)({displayName:"SmallAddIcon",viewBox:"0 0 20 20",path:o.createElement("path",{fill:"currentColor",d:"M14 9h-3V6c0-.55-.45-1-1-1s-1 .45-1 1v3H6c-.55 0-1 .45-1 1s.45 1 1 1h3v3c0 .55.45 1 1 1s1-.45 1-1v-3h3c.55 0 1-.45 1-1s-.45-1-1-1z",fillRule:"evenodd"})}),(0,i.IU)({viewBox:"0 0 14 14",d:"M14,7.77 L14,6.17 L12.06,5.53 L11.61,4.44 L12.49,2.6 L11.36,1.47 L9.55,2.38 L8.46,1.93 L7.77,0.01 L6.17,0.01 L5.54,1.95 L4.43,2.4 L2.59,1.52 L1.46,2.65 L2.37,4.46 L1.92,5.55 L0,6.23 L0,7.82 L1.94,8.46 L2.39,9.55 L1.51,11.39 L2.64,12.52 L4.45,11.61 L5.54,12.06 L6.23,13.98 L7.82,13.98 L8.45,12.04 L9.56,11.59 L11.4,12.47 L12.53,11.34 L11.61,9.53 L12.08,8.44 L14,7.75 L14,7.77 Z M7,10 C5.34,10 4,8.66 4,7 C4,5.34 5.34,4 7,4 C8.66,4 10,5.34 10,7 C10,8.66 8.66,10 7,10 Z",displayName:"SettingsIcon"}),(0,i.IU)({displayName:"CheckCircleIcon",d:"M12,0A12,12,0,1,0,24,12,12.014,12.014,0,0,0,12,0Zm6.927,8.2-6.845,9.289a1.011,1.011,0,0,1-1.43.188L5.764,13.769a1,1,0,1,1,1.25-1.562l4.076,3.261,6.227-8.451A1,1,0,1,1,18.927,8.2Z"}),(0,i.IU)({d:"M19.5,9.5h-.75V6.75a6.75,6.75,0,0,0-13.5,0V9.5H4.5a2,2,0,0,0-2,2V22a2,2,0,0,0,2,2h15a2,2,0,0,0,2-2V11.5A2,2,0,0,0,19.5,9.5Zm-9.5,6a2,2,0,1,1,3,1.723V19.5a1,1,0,0,1-2,0V17.223A1.994,1.994,0,0,1,10,15.5ZM7.75,6.75a4.25,4.25,0,0,1,8.5,0V9a.5.5,0,0,1-.5.5H8.25a.5.5,0,0,1-.5-.5Z",displayName:"LockIcon"}),(0,i.IU)({d:"M19.5,9.5h-.75V6.75A6.751,6.751,0,0,0,5.533,4.811a1.25,1.25,0,1,0,2.395.717A4.251,4.251,0,0,1,16.25,6.75V9a.5.5,0,0,1-.5.5H4.5a2,2,0,0,0-2,2V22a2,2,0,0,0,2,2h15a2,2,0,0,0,2-2V11.5A2,2,0,0,0,19.5,9.5Zm-9.5,6a2,2,0,1,1,3,1.723V19.5a1,1,0,0,1-2,0V17.223A1.994,1.994,0,0,1,10,15.5Z",displayName:"UnlockIcon"}),(0,i.IU)({displayName:"ViewIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M23.432,10.524C20.787,7.614,16.4,4.538,12,4.6,7.6,4.537,3.213,7.615.568,10.524a2.211,2.211,0,0,0,0,2.948C3.182,16.351,7.507,19.4,11.839,19.4h.308c4.347,0,8.671-3.049,11.288-5.929A2.21,2.21,0,0,0,23.432,10.524ZM7.4,12A4.6,4.6,0,1,1,12,16.6,4.6,4.6,0,0,1,7.4,12Z"}),o.createElement("circle",{cx:"12",cy:"12",r:"2"}))}),(0,i.IU)({displayName:"ViewOffIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M23.2,10.549a20.954,20.954,0,0,0-4.3-3.6l4-3.995a1,1,0,1,0-1.414-1.414l-.018.018a.737.737,0,0,1-.173.291l-19.5,19.5c-.008.007-.018.009-.026.017a1,1,0,0,0,1.631,1.088l4.146-4.146a11.26,11.26,0,0,0,4.31.939h.3c4.256,0,8.489-2.984,11.051-5.8A2.171,2.171,0,0,0,23.2,10.549ZM16.313,13.27a4.581,4.581,0,0,1-3,3.028,4.3,4.3,0,0,1-3.1-.19.253.253,0,0,1-.068-.407l5.56-5.559a.252.252,0,0,1,.407.067A4.3,4.3,0,0,1,16.313,13.27Z"}),o.createElement("path",{d:"M7.615,13.4a.244.244,0,0,0,.061-.24A4.315,4.315,0,0,1,7.5,12,4.5,4.5,0,0,1,12,7.5a4.276,4.276,0,0,1,1.16.173.244.244,0,0,0,.24-.062l1.941-1.942a.254.254,0,0,0-.1-.421A10.413,10.413,0,0,0,12,4.75C7.7,4.692,3.4,7.7.813,10.549a2.15,2.15,0,0,0-.007,2.9,21.209,21.209,0,0,0,3.438,3.03.256.256,0,0,0,.326-.029Z"}))}),(0,i.IU)({d:"M11.2857,6.05714 L10.08571,4.85714 L7.85714,7.14786 L7.85714,1 L6.14286,1 L6.14286,7.14786 L3.91429,4.85714 L2.71429,6.05714 L7,10.42857 L11.2857,6.05714 Z M1,11.2857 L1,13 L13,13 L13,11.2857 L1,11.2857 Z",displayName:"DownloadIcon",viewBox:"0 0 14 14"}),(0,i.IU)({displayName:"DeleteIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M19.452 7.5H4.547a.5.5 0 00-.5.545l1.287 14.136A2 2 0 007.326 24h9.347a2 2 0 001.992-1.819L19.95 8.045a.5.5 0 00-.129-.382.5.5 0 00-.369-.163zm-9.2 13a.75.75 0 01-1.5 0v-9a.75.75 0 011.5 0zm5 0a.75.75 0 01-1.5 0v-9a.75.75 0 011.5 0zM22 4h-4.75a.25.25 0 01-.25-.25V2.5A2.5 2.5 0 0014.5 0h-5A2.5 2.5 0 007 2.5v1.25a.25.25 0 01-.25.25H2a1 1 0 000 2h20a1 1 0 000-2zM9 3.75V2.5a.5.5 0 01.5-.5h5a.5.5 0 01.5.5v1.25a.25.25 0 01-.25.25h-5.5A.25.25 0 019 3.75z"}))}),(0,i.IU)({displayName:"RepeatIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M10.319,4.936a7.239,7.239,0,0,1,7.1,2.252,1.25,1.25,0,1,0,1.872-1.657A9.737,9.737,0,0,0,9.743,2.5,10.269,10.269,0,0,0,2.378,9.61a.249.249,0,0,1-.271.178l-1.033-.13A.491.491,0,0,0,.6,9.877a.5.5,0,0,0-.019.526l2.476,4.342a.5.5,0,0,0,.373.248.43.43,0,0,0,.062,0,.5.5,0,0,0,.359-.152l3.477-3.593a.5.5,0,0,0-.3-.844L5.15,10.172a.25.25,0,0,1-.2-.333A7.7,7.7,0,0,1,10.319,4.936Z"}),o.createElement("path",{d:"M23.406,14.1a.5.5,0,0,0,.015-.526l-2.5-4.329A.5.5,0,0,0,20.546,9a.489.489,0,0,0-.421.151l-3.456,3.614a.5.5,0,0,0,.3.842l1.848.221a.249.249,0,0,1,.183.117.253.253,0,0,1,.023.216,7.688,7.688,0,0,1-5.369,4.9,7.243,7.243,0,0,1-7.1-2.253,1.25,1.25,0,1,0-1.872,1.656,9.74,9.74,0,0,0,9.549,3.03,10.261,10.261,0,0,0,7.369-7.12.251.251,0,0,1,.27-.179l1.058.127a.422.422,0,0,0,.06,0A.5.5,0,0,0,23.406,14.1Z"}))}),(0,i.IU)({displayName:"RepeatClockIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M12.965,6a1,1,0,0,0-1,1v5.5a1,1,0,0,0,1,1h5a1,1,0,0,0,0-2h-3.75a.25.25,0,0,1-.25-.25V7A1,1,0,0,0,12.965,6Z"}),o.createElement("path",{d:"M12.567,1.258A10.822,10.822,0,0,0,2.818,8.4a.25.25,0,0,1-.271.163L.858,8.309a.514.514,0,0,0-.485.213.5.5,0,0,0-.021.53l2.679,4.7a.5.5,0,0,0,.786.107l3.77-3.746a.5.5,0,0,0-.279-.85L5.593,9.007a.25.25,0,0,1-.192-.35,8.259,8.259,0,1,1,7.866,11.59,1.25,1.25,0,0,0,.045,2.5h.047a10.751,10.751,0,1,0-.792-21.487Z"}))}),(0,i.IU)({displayName:"EditIcon",path:o.createElement("g",{fill:"none",stroke:"currentColor",strokeLinecap:"round",strokeWidth:"2"},o.createElement("path",{d:"M11 4H4a2 2 0 0 0-2 2v14a2 2 0 0 0 2 2h14a2 2 0 0 0 2-2v-7"}),o.createElement("path",{d:"M18.5 2.5a2.121 2.121 0 0 1 3 3L12 15l-4 1 1-4 9.5-9.5z"}))}),(0,i.IU)({d:"M15.41 7.41L14 6l-6 6 6 6 1.41-1.41L10.83 12z",displayName:"ChevronLeftIcon"}),(0,i.IU)({d:"M10 6L8.59 7.41 13.17 12l-4.58 4.59L10 18l6-6z",displayName:"ChevronRightIcon"}));(0,i.IU)({displayName:"ChevronDownIcon",d:"M16.59 8.59L12 13.17 7.41 8.59 6 10l6 6 6-6z"}),(0,i.IU)({d:"M12 8l-6 6 1.41 1.41L12 10.83l4.59 4.58L18 14z",displayName:"ChevronUpIcon"}),(0,i.IU)({d:"M20 11H7.83l5.59-5.59L12 4l-8 8 8 8 1.41-1.41L7.83 13H20v-2z",displayName:"ArrowBackIcon"}),(0,i.IU)({d:"M12 4l-1.41 1.41L16.17 11H4v2h12.17l-5.58 5.59L12 20l8-8z",displayName:"ArrowForwardIcon"}),(0,i.IU)({d:"M4 12l1.41 1.41L11 7.83V20h2V7.83l5.58 5.59L20 12l-8-8-8 8z",displayName:"ArrowUpIcon"}),(0,i.IU)({viewBox:"0 0 16 16",d:"M11.891 9.992a1 1 0 1 1 1.416 1.415l-4.3 4.3a1 1 0 0 1-1.414 0l-4.3-4.3A1 1 0 0 1 4.71 9.992l3.59 3.591 3.591-3.591zm0-3.984L8.3 2.417 4.709 6.008a1 1 0 0 1-1.416-1.415l4.3-4.3a1 1 0 0 1 1.414 0l4.3 4.3a1 1 0 1 1-1.416 1.415z",displayName:"ArrowUpDownIcon"}),(0,i.IU)({d:"M20 12l-1.41-1.41L13 16.17V4h-2v12.17l-5.58-5.59L4 12l8 8 8-8z",displayName:"ArrowDownIcon"}),(0,i.IU)({displayName:"ExternalLinkIcon",path:o.createElement("g",{fill:"none",stroke:"currentColor",strokeLinecap:"round",strokeWidth:"2"},o.createElement("path",{d:"M18 13v6a2 2 0 0 1-2 2H5a2 2 0 0 1-2-2V8a2 2 0 0 1 2-2h6"}),o.createElement("path",{d:"M15 3h6v6"}),o.createElement("path",{d:"M10 14L21 3"}))}),(0,i.IU)({displayName:"LinkIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M10.458,18.374,7.721,21.11a2.853,2.853,0,0,1-3.942,0l-.892-.891a2.787,2.787,0,0,1,0-3.941l5.8-5.8a2.789,2.789,0,0,1,3.942,0l.893.892A1,1,0,0,0,14.94,9.952l-.893-.892a4.791,4.791,0,0,0-6.771,0l-5.8,5.8a4.787,4.787,0,0,0,0,6.77l.892.891a4.785,4.785,0,0,0,6.771,0l2.736-2.735a1,1,0,1,0-1.414-1.415Z"}),o.createElement("path",{d:"M22.526,2.363l-.892-.892a4.8,4.8,0,0,0-6.77,0l-2.905,2.9a1,1,0,0,0,1.414,1.414l2.9-2.9a2.79,2.79,0,0,1,3.941,0l.893.893a2.786,2.786,0,0,1,0,3.942l-5.8,5.8a2.769,2.769,0,0,1-1.971.817h0a2.766,2.766,0,0,1-1.969-.816,1,1,0,1,0-1.415,1.412,4.751,4.751,0,0,0,3.384,1.4h0a4.752,4.752,0,0,0,3.385-1.4l5.8-5.8a4.786,4.786,0,0,0,0-6.771Z"}))}),(0,i.IU)({displayName:"PlusSquareIcon",path:o.createElement("g",{fill:"none",stroke:"currentColor",strokeLinecap:"round",strokeWidth:"2"},o.createElement("rect",{height:"18",width:"18",rx:"2",ry:"2",x:"3",y:"3"}),o.createElement("path",{d:"M12 8v8"}),o.createElement("path",{d:"M8 12h8"}))}),(0,i.IU)({displayName:"CalendarIcon",viewBox:"0 0 14 14",d:"M10.8889,5.5 L3.11111,5.5 L3.11111,7.05556 L10.8889,7.05556 L10.8889,5.5 Z M12.4444,1.05556 L11.6667,1.05556 L11.6667,0 L10.1111,0 L10.1111,1.05556 L3.88889,1.05556 L3.88889,0 L2.33333,0 L2.33333,1.05556 L1.55556,1.05556 C0.692222,1.05556 0.00777777,1.75556 0.00777777,2.61111 L0,12.5 C0,13.3556 0.692222,14 1.55556,14 L12.4444,14 C13.3,14 14,13.3556 14,12.5 L14,2.61111 C14,1.75556 13.3,1.05556 12.4444,1.05556 Z M12.4444,12.5 L1.55556,12.5 L1.55556,3.94444 L12.4444,3.94444 L12.4444,12.5 Z M8.55556,8.61111 L3.11111,8.61111 L3.11111,10.1667 L8.55556,10.1667 L8.55556,8.61111 Z"}),(0,i.IU)({d:"M0.913134,0.920639 C1.49851,0.331726 2.29348,0 3.12342,0 L10.8766,0 C11.7065,0 12.5015,0.331725 13.0869,0.920639 C13.6721,1.50939 14,2.30689 14,3.13746 L14,8.12943 C13.9962,8.51443 13.9059,8.97125 13.7629,9.32852 C13.6128,9.683 13.3552,10.0709 13.0869,10.3462 C12.813,10.6163 12.4265,10.8761 12.0734,11.0274 C11.7172,11.1716 11.2607,11.263 10.8766,11.2669 L10.1234,11.2669 L10.1234,12.5676 L10.1209,12.5676 C10.1204,12.793 10.0633,13.0791 9.97807,13.262 C9.8627,13.466 9.61158,13.7198 9.40818,13.8382 L9.40824,13.8383 C9.4077,13.8386 9.40716,13.8388 9.40661,13.8391 C9.40621,13.8393 9.4058,13.8396 9.40539,13.8398 L9.40535,13.8397 C9.22958,13.9254 8.94505,13.9951 8.75059,14 L8.74789,14 C8.35724,13.9963 7.98473,13.8383 7.71035,13.5617 L5.39553,11.2669 L3.12342,11.2669 C2.29348,11.2669 1.49851,10.9352 0.913134,10.3462 C0.644826,10.0709 0.387187,9.683 0.23711,9.32852 C0.0941235,8.97125 0.00379528,8.51443 0,8.12943 L0,3.13746 C0,2.30689 0.327915,1.50939 0.913134,0.920639 Z M3.12342,1.59494 C2.71959,1.59494 2.33133,1.75628 2.04431,2.04503 C1.75713,2.33395 1.59494,2.72681 1.59494,3.13746 L1.59494,8.12943 C1.59114,8.35901 1.62114,8.51076 1.71193,8.72129 C1.79563,8.9346 1.88065,9.06264 2.04431,9.22185 C2.33133,9.5106 2.71959,9.67195 3.12342,9.67195 L5.72383,9.67195 C5.93413,9.67195 6.13592,9.75502 6.28527,9.90308 L8.52848,12.1269 L8.52848,10.4694 C8.52848,10.029 8.88552,9.67195 9.32595,9.67195 L10.8766,9.67195 C11.1034,9.67583 11.2517,9.64614 11.4599,9.55518 C11.6712,9.47132 11.7976,9.38635 11.9557,9.22185 C12.1193,9.06264 12.2044,8.9346 12.2881,8.72129 C12.3789,8.51076 12.4089,8.35901 12.4051,8.12943 L12.4051,3.13746 C12.4051,2.72681 12.2429,2.33394 11.9557,2.04503 C11.6687,1.75628 11.2804,1.59494 10.8766,1.59494 L3.12342,1.59494 Z",displayName:"ChatIcon",viewBox:"0 0 14 14"}),(0,i.IU)({displayName:"TimeIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M12,0A12,12,0,1,0,24,12,12.014,12.014,0,0,0,12,0Zm0,22A10,10,0,1,1,22,12,10.011,10.011,0,0,1,12,22Z"}),o.createElement("path",{d:"M17.134,15.81,12.5,11.561V6.5a1,1,0,0,0-2,0V12a1,1,0,0,0,.324.738l4.959,4.545a1.01,1.01,0,0,0,1.413-.061A1,1,0,0,0,17.134,15.81Z"}))}),(0,i.IU)({displayName:"ArrowRightIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M13.584,12a2.643,2.643,0,0,1-.775,1.875L3.268,23.416a1.768,1.768,0,0,1-2.5-2.5l8.739-8.739a.25.25,0,0,0,0-.354L.768,3.084a1.768,1.768,0,0,1,2.5-2.5l9.541,9.541A2.643,2.643,0,0,1,13.584,12Z"}),o.createElement("path",{d:"M23.75,12a2.643,2.643,0,0,1-.775,1.875l-9.541,9.541a1.768,1.768,0,0,1-2.5-2.5l8.739-8.739a.25.25,0,0,0,0-.354L10.934,3.084a1.768,1.768,0,0,1,2.5-2.5l9.541,9.541A2.643,2.643,0,0,1,23.75,12Z"}))}),(0,i.IU)({displayName:"ArrowLeftIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M10.416,12a2.643,2.643,0,0,1,.775-1.875L20.732.584a1.768,1.768,0,0,1,2.5,2.5l-8.739,8.739a.25.25,0,0,0,0,.354l8.739,8.739a1.768,1.768,0,0,1-2.5,2.5l-9.541-9.541A2.643,2.643,0,0,1,10.416,12Z"}),o.createElement("path",{d:"M.25,12a2.643,2.643,0,0,1,.775-1.875L10.566.584a1.768,1.768,0,0,1,2.5,2.5L4.327,11.823a.25.25,0,0,0,0,.354l8.739,8.739a1.768,1.768,0,0,1-2.5,2.5L1.025,13.875A2.643,2.643,0,0,1,.25,12Z"}))}),(0,i.IU)({displayName:"AtSignIcon",d:"M12,.5A11.634,11.634,0,0,0,.262,12,11.634,11.634,0,0,0,12,23.5a11.836,11.836,0,0,0,6.624-2,1.25,1.25,0,1,0-1.393-2.076A9.34,9.34,0,0,1,12,21a9.132,9.132,0,0,1-9.238-9A9.132,9.132,0,0,1,12,3a9.132,9.132,0,0,1,9.238,9v.891a1.943,1.943,0,0,1-3.884,0V12A5.355,5.355,0,1,0,12,17.261a5.376,5.376,0,0,0,3.861-1.634,4.438,4.438,0,0,0,7.877-2.736V12A11.634,11.634,0,0,0,12,.5Zm0,14.261A2.763,2.763,0,1,1,14.854,12,2.812,2.812,0,0,1,12,14.761Z"}),(0,i.IU)({displayName:"AttachmentIcon",d:"M21.843,3.455a6.961,6.961,0,0,0-9.846,0L1.619,13.832a5.128,5.128,0,0,0,7.252,7.252L17.3,12.653A3.293,3.293,0,1,0,12.646,8L7.457,13.184A1,1,0,1,0,8.871,14.6L14.06,9.409a1.294,1.294,0,0,1,1.829,1.83L7.457,19.67a3.128,3.128,0,0,1-4.424-4.424L13.411,4.869a4.962,4.962,0,1,1,7.018,7.018L12.646,19.67a1,1,0,1,0,1.414,1.414L21.843,13.3a6.96,6.96,0,0,0,0-9.846Z"}),(0,i.IU)({displayName:"UpDownIcon",viewBox:"-1 -1 9 11",d:"M 3.5 0L 3.98809 -0.569442L 3.5 -0.987808L 3.01191 -0.569442L 3.5 0ZM 3.5 9L 3.01191 9.56944L 3.5 9.98781L 3.98809 9.56944L 3.5 9ZM 0.488094 3.56944L 3.98809 0.569442L 3.01191 -0.569442L -0.488094 2.43056L 0.488094 3.56944ZM 3.01191 0.569442L 6.51191 3.56944L 7.48809 2.43056L 3.98809 -0.569442L 3.01191 0.569442ZM -0.488094 6.56944L 3.01191 9.56944L 3.98809 8.43056L 0.488094 5.43056L -0.488094 6.56944ZM 3.98809 9.56944L 7.48809 6.56944L 6.51191 5.43056L 3.01191 8.43056L 3.98809 9.56944Z"}),(0,i.IU)({d:"M23.555,8.729a1.505,1.505,0,0,0-1.406-.98H16.062a.5.5,0,0,1-.472-.334L13.405,1.222a1.5,1.5,0,0,0-2.81,0l-.005.016L8.41,7.415a.5.5,0,0,1-.471.334H1.85A1.5,1.5,0,0,0,.887,10.4l5.184,4.3a.5.5,0,0,1,.155.543L4.048,21.774a1.5,1.5,0,0,0,2.31,1.684l5.346-3.92a.5.5,0,0,1,.591,0l5.344,3.919a1.5,1.5,0,0,0,2.312-1.683l-2.178-6.535a.5.5,0,0,1,.155-.543l5.194-4.306A1.5,1.5,0,0,0,23.555,8.729Z",displayName:"StarIcon"}),(0,i.IU)({displayName:"EmailIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("path",{d:"M11.114,14.556a1.252,1.252,0,0,0,1.768,0L22.568,4.87a.5.5,0,0,0-.281-.849A1.966,1.966,0,0,0,22,4H2a1.966,1.966,0,0,0-.289.021.5.5,0,0,0-.281.849Z"}),o.createElement("path",{d:"M23.888,5.832a.182.182,0,0,0-.2.039l-6.2,6.2a.251.251,0,0,0,0,.354l5.043,5.043a.75.75,0,1,1-1.06,1.061l-5.043-5.043a.25.25,0,0,0-.354,0l-2.129,2.129a2.75,2.75,0,0,1-3.888,0L7.926,13.488a.251.251,0,0,0-.354,0L2.529,18.531a.75.75,0,0,1-1.06-1.061l5.043-5.043a.251.251,0,0,0,0-.354l-6.2-6.2a.18.18,0,0,0-.2-.039A.182.182,0,0,0,0,6V18a2,2,0,0,0,2,2H22a2,2,0,0,0,2-2V6A.181.181,0,0,0,23.888,5.832Z"}))}),(0,i.IU)({d:"M2.20731,0.0127209 C2.1105,-0.0066419 1.99432,-0.00664663 1.91687,0.032079 C0.871279,0.438698 0.212942,1.92964 0.0580392,2.95587 C-0.426031,6.28627 2.20731,9.17133 4.62766,11.0689 C6.77694,12.7534 10.9012,15.5223 13.3409,12.8503 C13.6507,12.5211 14.0186,12.037 13.9993,11.553 C13.9412,10.7397 13.186,10.1588 12.6051,9.71349 C12.1598,9.38432 11.2304,8.47427 10.6495,8.49363 C10.1267,8.51299 9.79754,9.05515 9.46837,9.38432 L8.88748,9.96521 C8.79067,10.062 7.55145,9.24878 7.41591,9.15197 C6.91248,8.8228 6.4284,8.45491 6.00242,8.04829 C5.57644,7.64167 5.18919,7.19632 4.86002,6.73161 C4.7632,6.59607 3.96933,5.41495 4.04678,5.31813 C4.04678,5.31813 4.72448,4.58234 4.91811,4.2919 C5.32473,3.67229 5.63453,3.18822 5.16982,2.45243 C4.99556,2.18135 4.78257,1.96836 4.55021,1.73601 C4.14359,1.34875 3.73698,0.942131 3.27227,0.612963 C3.02055,0.419335 2.59457,0.0708094 2.20731,0.0127209 Z",displayName:"PhoneIcon",viewBox:"0 0 14 14"}),(0,i.IU)({viewBox:"0 0 10 10",d:"M3,2 C2.44771525,2 2,1.55228475 2,1 C2,0.44771525 2.44771525,0 3,0 C3.55228475,0 4,0.44771525 4,1 C4,1.55228475 3.55228475,2 3,2 Z M3,6 C2.44771525,6 2,5.55228475 2,5 C2,4.44771525 2.44771525,4 3,4 C3.55228475,4 4,4.44771525 4,5 C4,5.55228475 3.55228475,6 3,6 Z M3,10 C2.44771525,10 2,9.55228475 2,9 C2,8.44771525 2.44771525,8 3,8 C3.55228475,8 4,8.44771525 4,9 C4,9.55228475 3.55228475,10 3,10 Z M7,2 C6.44771525,2 6,1.55228475 6,1 C6,0.44771525 6.44771525,0 7,0 C7.55228475,0 8,0.44771525 8,1 C8,1.55228475 7.55228475,2 7,2 Z M7,6 C6.44771525,6 6,5.55228475 6,5 C6,4.44771525 6.44771525,4 7,4 C7.55228475,4 8,4.44771525 8,5 C8,5.55228475 7.55228475,6 7,6 Z M7,10 C6.44771525,10 6,9.55228475 6,9 C6,8.44771525 6.44771525,8 7,8 C7.55228475,8 8,8.44771525 8,9 C8,9.55228475 7.55228475,10 7,10 Z",displayName:"DragHandleIcon"}),(0,i.IU)({displayName:"SpinnerIcon",path:o.createElement(o.Fragment,null,o.createElement("defs",null,o.createElement("linearGradient",{x1:"28.154%",y1:"63.74%",x2:"74.629%",y2:"17.783%",id:"a"},o.createElement("stop",{stopColor:"currentColor",offset:"0%"}),o.createElement("stop",{stopColor:"#fff",stopOpacity:"0",offset:"100%"}))),o.createElement("g",{transform:"translate(2)",fill:"none"},o.createElement("circle",{stroke:"url(#a)",strokeWidth:"4",cx:"10",cy:"12",r:"10"}),o.createElement("path",{d:"M10 2C4.477 2 0 6.477 0 12",stroke:"currentColor",strokeWidth:"4"}),o.createElement("rect",{fill:"currentColor",x:"8",width:"4",height:"4",rx:"8"})))}),(0,i.IU)({displayName:"CloseIcon",d:"M.439,21.44a1.5,1.5,0,0,0,2.122,2.121L11.823,14.3a.25.25,0,0,1,.354,0l9.262,9.263a1.5,1.5,0,1,0,2.122-2.121L14.3,12.177a.25.25,0,0,1,0-.354l9.263-9.262A1.5,1.5,0,0,0,21.439.44L12.177,9.7a.25.25,0,0,1-.354,0L2.561.44A1.5,1.5,0,0,0,.439,2.561L9.7,11.823a.25.25,0,0,1,0,.354Z"}),(0,i.IU)({displayName:"SmallCloseIcon",viewBox:"0 0 16 16",path:o.createElement("path",{d:"M9.41 8l2.29-2.29c.19-.18.3-.43.3-.71a1.003 1.003 0 0 0-1.71-.71L8 6.59l-2.29-2.3a1.003 1.003 0 0 0-1.42 1.42L6.59 8 4.3 10.29c-.19.18-.3.43-.3.71a1.003 1.003 0 0 0 1.71.71L8 9.41l2.29 2.29c.18.19.43.3.71.3a1.003 1.003 0 0 0 .71-1.71L9.41 8z",fillRule:"evenodd",fill:"currentColor"})}),(0,i.IU)({d:"M12 2C6.48 2 2 6.48 2 12s4.48 10 10 10 10-4.48 10-10S17.52 2 12 2zm0 18c-4.42 0-8-3.58-8-8 0-1.85.63-3.55 1.69-4.9L16.9 18.31C15.55 19.37 13.85 20 12 20zm6.31-3.1L7.1 5.69C8.45 4.63 10.15 4 12 4c4.42 0 8 3.58 8 8 0 1.85-.63 3.55-1.69 4.9z",displayName:"NotAllowedIcon"}),(0,i.IU)({d:"M21,5H3C2.621,5,2.275,5.214,2.105,5.553C1.937,5.892,1.973,6.297,2.2,6.6l9,12 c0.188,0.252,0.485,0.4,0.8,0.4s0.611-0.148,0.8-0.4l9-12c0.228-0.303,0.264-0.708,0.095-1.047C21.725,5.214,21.379,5,21,5z",displayName:"TriangleDownIcon"}),(0,i.IU)({d:"M12.8,5.4c-0.377-0.504-1.223-0.504-1.6,0l-9,12c-0.228,0.303-0.264,0.708-0.095,1.047 C2.275,18.786,2.621,19,3,19h18c0.379,0,0.725-0.214,0.895-0.553c0.169-0.339,0.133-0.744-0.095-1.047L12.8,5.4z",displayName:"TriangleUpIcon"}),(0,i.IU)({displayName:"InfoOutlineIcon",path:o.createElement("g",{fill:"currentColor",stroke:"currentColor",strokeLinecap:"square",strokeWidth:"2"},o.createElement("circle",{cx:"12",cy:"12",fill:"none",r:"11",stroke:"currentColor"}),o.createElement("line",{fill:"none",x1:"11.959",x2:"11.959",y1:"11",y2:"17"}),o.createElement("circle",{cx:"11.959",cy:"7",r:"1",stroke:"none"}))}),(0,i.IU)({displayName:"BellIcon",d:"M12 22c1.1 0 2-.9 2-2h-4c0 1.1.89 2 2 2zm6-6v-5c0-3.07-1.64-5.64-4.5-6.32V4c0-.83-.67-1.5-1.5-1.5s-1.5.67-1.5 1.5v.68C7.63 5.36 6 7.92 6 11v5l-2 2v1h16v-1l-2-2z"}),(0,i.IU)({d:"M12,0A12,12,0,1,0,24,12,12.013,12.013,0,0,0,12,0Zm.25,5a1.5,1.5,0,1,1-1.5,1.5A1.5,1.5,0,0,1,12.25,5ZM14.5,18.5h-4a1,1,0,0,1,0-2h.75a.25.25,0,0,0,.25-.25v-4.5a.25.25,0,0,0-.25-.25H10.5a1,1,0,0,1,0-2h1a2,2,0,0,1,2,2v4.75a.25.25,0,0,0,.25.25h.75a1,1,0,1,1,0,2Z"}),(0,i.IU)({d:"M12,0A12,12,0,1,0,24,12,12.013,12.013,0,0,0,12,0Zm0,19a1.5,1.5,0,1,1,1.5-1.5A1.5,1.5,0,0,1,12,19Zm1.6-6.08a1,1,0,0,0-.6.917,1,1,0,1,1-2,0,3,3,0,0,1,1.8-2.75A2,2,0,1,0,10,9.255a1,1,0,1,1-2,0,4,4,0,1,1,5.6,3.666Z",displayName:"QuestionIcon"}),(0,i.IU)({displayName:"QuestionOutlineIcon",path:o.createElement("g",{stroke:"currentColor",strokeWidth:"1.5"},o.createElement("path",{strokeLinecap:"round",fill:"none",d:"M9,9a3,3,0,1,1,4,2.829,1.5,1.5,0,0,0-1,1.415V14.25"}),o.createElement("path",{fill:"none",strokeLinecap:"round",d:"M12,17.25a.375.375,0,1,0,.375.375A.375.375,0,0,0,12,17.25h0"}),o.createElement("circle",{fill:"none",strokeMiterlimit:"10",cx:"12",cy:"12",r:"11.25"}))}),(0,i.IU)({d:"M11.983,0a12.206,12.206,0,0,0-8.51,3.653A11.8,11.8,0,0,0,0,12.207,11.779,11.779,0,0,0,11.8,24h.214A12.111,12.111,0,0,0,24,11.791h0A11.766,11.766,0,0,0,11.983,0ZM10.5,16.542a1.476,1.476,0,0,1,1.449-1.53h.027a1.527,1.527,0,0,1,1.523,1.47,1.475,1.475,0,0,1-1.449,1.53h-.027A1.529,1.529,0,0,1,10.5,16.542ZM11,12.5v-6a1,1,0,0,1,2,0v6a1,1,0,1,1-2,0Z",displayName:"WarningIcon"}),(0,i.IU)({displayName:"WarningTwoIcon",d:"M23.119,20,13.772,2.15h0a2,2,0,0,0-3.543,0L.881,20a2,2,0,0,0,1.772,2.928H21.347A2,2,0,0,0,23.119,20ZM11,8.423a1,1,0,0,1,2,0v6a1,1,0,1,1-2,0Zm1.05,11.51h-.028a1.528,1.528,0,0,1-1.522-1.47,1.476,1.476,0,0,1,1.448-1.53h.028A1.527,1.527,0,0,1,13.5,18.4,1.475,1.475,0,0,1,12.05,19.933Z"}),(0,i.IU)({viewBox:"0 0 14 14",path:o.createElement("g",{fill:"currentColor"},o.createElement("polygon",{points:"5.5 11.9993304 14 3.49933039 12.5 2 5.5 8.99933039 1.5 4.9968652 0 6.49933039"}))}),(0,i.IU)({displayName:"MinusIcon",path:o.createElement("g",{fill:"currentColor"},o.createElement("rect",{height:"4",width:"20",x:"2",y:"10"}))}),(0,i.IU)({displayName:"HamburgerIcon",viewBox:"0 0 24 24",d:"M 3 5 A 1.0001 1.0001 0 1 0 3 7 L 21 7 A 1.0001 1.0001 0 1 0 21 5 L 3 5 z M 3 11 A 1.0001 1.0001 0 1 0 3 13 L 21 13 A 1.0001 1.0001 0 1 0 21 11 L 3 11 z M 3 17 A 1.0001 1.0001 0 1 0 3 19 L 21 19 A 1.0001 1.0001 0 1 0 21 17 L 3 17 z"})},4612:(e,t,n)=>{"use strict";n.d(t,{II:()=>c});var i=n(79762),o=n(105),r=n(44592),s=n(67294),a=n(26450);function l(){return l=Object.assign||function(e){for(var t=1;t=0||(o[n]=e[n]);return o}r.Ts&&(c.displayName="Input"),c.id="Input";var u=["placement"],h={left:{marginEnd:"-1px",borderEndRadius:0,borderEndColor:"transparent"},right:{marginStart:"-1px",borderStartRadius:0,borderStartColor:"transparent"}},g=(0,o.m$)("div",{baseStyle:{flex:"0 0 auto",width:"auto",display:"flex",alignItems:"center",whiteSpace:"nowrap"}}),p=(0,o.Gp)((function(e,t){var n,i=e.placement,r=void 0===i?"left":i,a=d(e,u),c=null!=(n=h[r])?n:{},p=(0,o.yK)();return s.createElement(g,l({ref:t},a,{__css:l({},p.addon,c)}))}));r.Ts&&(p.displayName="InputAddon");var f=(0,o.Gp)((function(e,t){return s.createElement(p,l({ref:t,placement:"left"},e,{className:(0,r.cx)("chakra-input__left-addon",e.className)}))}));r.Ts&&(f.displayName="InputLeftAddon"),f.id="InputLeftAddon";var m=(0,o.Gp)((function(e,t){return s.createElement(p,l({ref:t,placement:"right"},e,{className:(0,r.cx)("chakra-input__right-addon",e.className)}))}));r.Ts&&(m.displayName="InputRightAddon"),m.id="InputRightAddon";var v=["children","className"],_=(0,o.Gp)((function(e,t){var n=(0,o.jC)("Input",e),i=(0,o.Lr)(e),c=i.children,u=i.className,h=d(i,v),g=(0,r.cx)("chakra-input__group",u),p={},f=(0,a.WR)(c),m=n.field;f.forEach((function(e){var t,i;n&&(m&&"InputLeftElement"===e.type.id&&(p.paddingStart=null!=(t=m.height)?t:m.h),m&&"InputRightElement"===e.type.id&&(p.paddingEnd=null!=(i=m.height)?i:m.h),"InputRightAddon"===e.type.id&&(p.borderEndRadius=0),"InputLeftAddon"===e.type.id&&(p.borderStartRadius=0))}));var _=f.map((function(t){var n,i,o={size:(null==(n=t.props)?void 0:n.size)||e.size,variant:(null==(i=t.props)?void 0:i.variant)||e.variant};return"Input"!==t.type.id?s.cloneElement(t,o):s.cloneElement(t,Object.assign(o,p,t.props))}));return s.createElement(o.m$.div,l({className:g,ref:t,__css:{width:"100%",display:"flex",position:"relative"}},h),s.createElement(o.Fo,{value:n},_))}));r.Ts&&(_.displayName="InputGroup");var b=["placement"],y=["className"],w=["className"],C=(0,o.m$)("div",{baseStyle:{display:"flex",alignItems:"center",justifyContent:"center",position:"absolute",top:"0",zIndex:2}}),S=(0,o.Gp)((function(e,t){var n,i,r,a=e.placement,c=void 0===a?"left":a,u=d(e,b),h=(0,o.yK)().field,g=((r={})["left"===c?"insetStart":"insetEnd"]="0",r.width=null!=(n=null==h?void 0:h.height)?n:null==h?void 0:h.h,r.height=null!=(i=null==h?void 0:h.height)?i:null==h?void 0:h.h,r.fontSize=null==h?void 0:h.fontSize,r);return s.createElement(C,l({ref:t,__css:g},u))}));S.id="InputElement",r.Ts&&(S.displayName="InputElement");var x=(0,o.Gp)((function(e,t){var n=e.className,i=d(e,y),o=(0,r.cx)("chakra-input__left-element",n);return s.createElement(S,l({ref:t,placement:"left",className:o},i))}));x.id="InputLeftElement",r.Ts&&(x.displayName="InputLeftElement");var k=(0,o.Gp)((function(e,t){var n=e.className,i=d(e,w),o=(0,r.cx)("chakra-input__right-element",n);return s.createElement(S,l({ref:t,placement:"right",className:o},i))}));k.id="InputRightElement",r.Ts&&(k.displayName="InputRightElement")},68527:(e,t,n)=>{"use strict";n.d(t,{xu:()=>v,M5:()=>y,iz:()=>N,kC:()=>D,rj:()=>T,LZ:()=>Z,xv:()=>ne});var i=n(105),o=n(94244),r=n(44592),s=n(67294),a=n(10894),l=n(26450);function c(){return c=Object.assign||function(e){for(var t=1;t=0||(o[n]=e[n]);return o}var u=["ratio","children","className"],h=(0,i.Gp)((function(e,t){var n=e.ratio,o=void 0===n?4/3:n,a=e.children,l=e.className,h=d(e,u),g=s.Children.only(a),p=(0,r.cx)("chakra-aspect-ratio",l);return s.createElement(i.m$.div,c({ref:t,position:"relative",className:p,_before:{height:0,content:'""',display:"block",paddingBottom:(0,r.XQ)(o,(function(e){return 1/e*100+"%"}))},__css:{"& > *:not(style)":{overflow:"hidden",position:"absolute",top:"0",right:"0",bottom:"0",left:"0",display:"flex",justifyContent:"center",alignItems:"center",width:"100%",height:"100%"},"& > img, & > video":{objectFit:"cover"}}},h),g)}));r.Ts&&(h.displayName="AspectRatio");var g=["className"],p=(0,i.Gp)((function(e,t){var n=(0,i.mq)("Badge",e),o=(0,i.Lr)(e);o.className;var a=d(o,g);return s.createElement(i.m$.span,c({ref:t,className:(0,r.cx)("chakra-badge",e.className)},a,{__css:c({display:"inline-block",whiteSpace:"nowrap",verticalAlign:"middle"},n)}))}));r.Ts&&(p.displayName="Badge");var f=["size","centerContent"],m=["size"],v=(0,i.m$)("div");r.Ts&&(v.displayName="Box");var _=(0,i.Gp)((function(e,t){var n=e.size,i=e.centerContent,o=void 0===i||i,r=d(e,f),a=o?{display:"flex",alignItems:"center",justifyContent:"center"}:{};return s.createElement(v,c({ref:t,boxSize:n,__css:c({},a,{flexShrink:0,flexGrow:0})},r))}));r.Ts&&(_.displayName="Square");var b=(0,i.Gp)((function(e,t){var n=e.size,i=d(e,m);return s.createElement(_,c({size:n,ref:t,borderRadius:"9999px"},i))}));r.Ts&&(b.displayName="Circle");var y=(0,i.m$)("div",{baseStyle:{display:"flex",alignItems:"center",justifyContent:"center"}});r.Ts&&(y.displayName="Center");var w=["className"],C=(0,i.Gp)((function(e,t){var n=(0,i.mq)("Code",e),o=(0,i.Lr)(e);o.className;var a=d(o,w);return s.createElement(i.m$.code,c({ref:t,className:(0,r.cx)("chakra-code",e.className)},a,{__css:c({display:"inline-block"},n)}))}));r.Ts&&(C.displayName="Code");var S=["className","centerContent"],x=(0,i.Gp)((function(e,t){var n=(0,i.Lr)(e),o=n.className,a=n.centerContent,l=d(n,S),u=(0,i.mq)("Container",e);return s.createElement(i.m$.div,c({ref:t,className:(0,r.cx)("chakra-container",o)},l,{__css:c({},u,a&&{display:"flex",flexDirection:"column",alignItems:"center"})}))}));r.Ts&&(x.displayName="Container");var k=["borderLeftWidth","borderBottomWidth","borderTopWidth","borderRightWidth","borderWidth","borderStyle","borderColor"],L=["className","orientation","__css"],N=(0,i.Gp)((function(e,t){var n=(0,i.mq)("Divider",e),o=n.borderLeftWidth,a=n.borderBottomWidth,l=n.borderTopWidth,u=n.borderRightWidth,h=n.borderWidth,g=n.borderStyle,p=n.borderColor,f=d(n,k),m=(0,i.Lr)(e),v=m.className,_=m.orientation,b=void 0===_?"horizontal":_,y=m.__css,w=d(m,L),C={vertical:{borderLeftWidth:o||u||h||"1px",height:"100%"},horizontal:{borderBottomWidth:a||l||h||"1px",width:"100%"}};return s.createElement(i.m$.hr,c({ref:t,"aria-orientation":b},w,{__css:c({},f,{border:"0",borderColor:p,borderStyle:g},C[b],y),className:(0,r.cx)("chakra-divider",v)}))}));r.Ts&&(N.displayName="Divider");var E=["direction","align","justify","wrap","basis","grow","shrink"],D=(0,i.Gp)((function(e,t){var n=e.direction,o=e.align,r=e.justify,a=e.wrap,l=e.basis,u=e.grow,h=e.shrink,g=d(e,E),p={display:"flex",flexDirection:n,alignItems:o,justifyContent:r,flexWrap:a,flexBasis:l,flexGrow:u,flexShrink:h};return s.createElement(i.m$.div,c({ref:t,__css:p},g))}));r.Ts&&(D.displayName="Flex");var I=["area","templateAreas","gap","rowGap","columnGap","column","row","autoFlow","autoRows","templateRows","autoColumns","templateColumns"],T=(0,i.Gp)((function(e,t){var n=e.area,o=e.templateAreas,r=e.gap,a=e.rowGap,l=e.columnGap,u=e.column,h=e.row,g=e.autoFlow,p=e.autoRows,f=e.templateRows,m=e.autoColumns,v=e.templateColumns,_=d(e,I),b={display:"grid",gridArea:n,gridTemplateAreas:o,gridGap:r,gridRowGap:a,gridColumnGap:l,gridAutoColumns:m,gridColumn:u,gridRow:h,gridAutoFlow:g,gridAutoRows:p,gridTemplateRows:f,gridTemplateColumns:v};return s.createElement(i.m$.div,c({ref:t,__css:b},_))}));r.Ts&&(T.displayName="Grid");var M=["className"],A=(0,i.Gp)((function(e,t){var n=(0,i.mq)("Heading",e),o=(0,i.Lr)(e);o.className;var a=d(o,M);return s.createElement(i.m$.h2,c({ref:t,className:(0,r.cx)("chakra-heading",e.className)},a,{__css:n}))}));r.Ts&&(A.displayName="Heading");var O=["className"],R=(0,i.Gp)((function(e,t){var n=(0,i.mq)("Kbd",e),o=(0,i.Lr)(e),a=o.className,l=d(o,O);return s.createElement(i.m$.kbd,c({ref:t,className:(0,r.cx)("chakra-kbd",a)},l,{__css:c({fontFamily:"mono"},n)}))}));r.Ts&&(R.displayName="Kbd");var P=["className","isExternal"],F=(0,i.Gp)((function(e,t){var n=(0,i.mq)("Link",e),o=(0,i.Lr)(e),a=o.className,l=o.isExternal,u=d(o,P);return s.createElement(i.m$.a,c({target:l?"_blank":void 0,rel:l?"noopener noreferrer":void 0,ref:t,className:(0,r.cx)("chakra-link",a)},u,{__css:n}))}));r.Ts&&(F.displayName="Link");var B=["children","styleType","stylePosition","spacing"],W=["as"],V=["as"],z=(0,i.Gp)((function(e,t){var n,o=(0,i.jC)("List",e),r=(0,i.Lr)(e),a=r.children,u=r.styleType,h=void 0===u?"none":u,g=r.stylePosition,p=r.spacing,f=d(r,B),m=(0,l.WR)(a),v=p?((n={})["& > *:not(style) ~ *:not(style)"]={mt:p},n):{};return s.createElement(i.Fo,{value:o},s.createElement(i.m$.ul,c({ref:t,listStyleType:h,listStylePosition:g,role:"list",__css:c({},o.container,v)},f),m))}));r.Ts&&(z.displayName="List");var H=(0,i.Gp)((function(e,t){e.as;var n=d(e,W);return s.createElement(z,c({ref:t,as:"ol",styleType:"decimal",marginStart:"1em"},n))}));r.Ts&&(H.displayName="OrderedList");var j=(0,i.Gp)((function(e,t){e.as;var n=d(e,V);return s.createElement(z,c({ref:t,as:"ul",styleType:"initial",marginStart:"1em"},n))}));r.Ts&&(j.displayName="UnorderedList");var U=(0,i.Gp)((function(e,t){var n=(0,i.yK)();return s.createElement(i.m$.li,c({ref:t},e,{__css:n.item}))}));r.Ts&&(U.displayName="ListItem");var K=(0,i.Gp)((function(e,t){var n=(0,i.yK)();return s.createElement(a.JO,c({ref:t,role:"presentation"},e,{__css:n.icon}))}));r.Ts&&(K.displayName="ListIcon");var $=["columns","spacingX","spacingY","spacing","minChildWidth"],q=(0,i.Gp)((function(e,t){var n,i,o=e.columns,a=e.spacingX,l=e.spacingY,u=e.spacing,h=e.minChildWidth,g=d(e,$),p=h?(i=h,(0,r.XQ)(i,(function(e){return(0,r.Ft)(e)?null:"repeat(auto-fit, minmax("+(t=e,((0,r.hj)(t)?t+"px":t)+", 1fr))");var t}))):(n=o,(0,r.XQ)(n,(function(e){return(0,r.Ft)(e)?null:"repeat("+e+", minmax(0, 1fr))"})));return s.createElement(T,c({ref:t,gap:u,columnGap:a,rowGap:l,templateColumns:p},g))}));r.Ts&&(q.displayName="SimpleGrid");var Z=(0,i.m$)("div",{baseStyle:{flex:1,justifySelf:"stretch",alignSelf:"stretch"}});r.Ts&&(Z.displayName="Spacer");var G="& > *:not(style) ~ *:not(style)",Y=["isInline","direction","align","justify","spacing","wrap","children","divider","className","shouldWrapChildren"],Q=function(e){return s.createElement(i.m$.div,c({className:"chakra-stack__item"},e,{__css:c({display:"inline-block",flex:"0 0 auto",minWidth:0},e.__css)}))},X=(0,i.Gp)((function(e,t){var n,o=e.isInline,a=e.direction,u=e.align,h=e.justify,g=e.spacing,p=void 0===g?"0.5rem":g,f=e.wrap,m=e.children,v=e.divider,_=e.className,b=e.shouldWrapChildren,y=d(e,Y),w=o?"row":null!=a?a:"column",C=s.useMemo((function(){return function(e){var t,n=e.spacing,i=e.direction,o={column:{marginTop:n,marginEnd:0,marginBottom:0,marginStart:0},row:{marginTop:0,marginEnd:0,marginBottom:0,marginStart:n},"column-reverse":{marginTop:0,marginEnd:0,marginBottom:n,marginStart:0},"row-reverse":{marginTop:0,marginEnd:n,marginBottom:0,marginStart:0}};return(t={flexDirection:i})[G]=(0,r.XQ)(i,(function(e){return o[e]})),t}({direction:w,spacing:p})}),[w,p]),S=s.useMemo((function(){return function(e){var t=e.spacing,n=e.direction,i={column:{my:t,mx:0,borderLeftWidth:0,borderBottomWidth:"1px"},"column-reverse":{my:t,mx:0,borderLeftWidth:0,borderBottomWidth:"1px"},row:{mx:t,my:0,borderLeftWidth:"1px",borderBottomWidth:0},"row-reverse":{mx:t,my:0,borderLeftWidth:"1px",borderBottomWidth:0}};return{"&":(0,r.XQ)(n,(function(e){return i[e]}))}}({spacing:p,direction:w})}),[p,w]),x=!!v,k=!b&&!x,L=(0,l.WR)(m),N=k?L:L.map((function(e,t){var n=void 0!==e.key?e.key:t,i=t+1===L.length,o=b?s.createElement(Q,{key:n},e):e;if(!x)return o;var r=i?null:s.cloneElement(v,{__css:S});return s.createElement(s.Fragment,{key:n},o,r)})),E=(0,r.cx)("chakra-stack",_);return s.createElement(i.m$.div,c({ref:t,display:"flex",alignItems:u,justifyContent:h,flexDirection:C.flexDirection,flexWrap:f,className:E,__css:x?{}:(n={},n[G]=C[G],n)},y),N)}));r.Ts&&(X.displayName="Stack");var J=(0,i.Gp)((function(e,t){return s.createElement(X,c({align:"center"},e,{direction:"row",ref:t}))}));r.Ts&&(J.displayName="HStack");var ee=(0,i.Gp)((function(e,t){return s.createElement(X,c({align:"center"},e,{direction:"column",ref:t}))}));r.Ts&&(ee.displayName="VStack");var te=["className","align","decoration","casing"],ne=(0,i.Gp)((function(e,t){var n=(0,i.mq)("Text",e),o=(0,i.Lr)(e);o.className,o.align,o.decoration,o.casing;var a=d(o,te),l=(0,r.YU)({textAlign:e.align,textDecoration:e.decoration,textTransform:e.casing});return s.createElement(i.m$.p,c({ref:t,className:(0,r.cx)("chakra-text",e.className)},l,a,{__css:n}))}));r.Ts&&(ne.displayName="Text");var ie=["spacing","children","justify","direction","align","className","shouldWrapChildren"],oe=["className"],re=(0,i.Gp)((function(e,t){var n=e.spacing,a=void 0===n?"0.5rem":n,l=e.children,u=e.justify,h=e.direction,g=e.align,p=e.className,f=e.shouldWrapChildren,m=d(e,ie),v=s.useMemo((function(){return{"--chakra-wrap-spacing":function(e){return(0,r.XQ)(a,(function(t){return(0,o.fr)("space",t)(e)}))},"--wrap-spacing":"calc(var(--chakra-wrap-spacing) / 2)",display:"flex",flexWrap:"wrap",justifyContent:u,alignItems:g,flexDirection:h,listStyleType:"none",padding:"0",margin:"calc(var(--wrap-spacing) * -1)","& > *:not(style)":{margin:"var(--wrap-spacing)"}}}),[a,u,g,h]),_=f?s.Children.map(l,(function(e,t){return s.createElement(se,{key:t},e)})):l;return s.createElement(i.m$.div,c({ref:t,className:(0,r.cx)("chakra-wrap",p)},m),s.createElement(i.m$.ul,{className:"chakra-wrap__list",__css:v},_))}));r.Ts&&(re.displayName="Wrap");var se=(0,i.Gp)((function(e,t){var n=e.className,o=d(e,oe);return s.createElement(i.m$.li,c({ref:t,__css:{display:"flex",alignItems:"flex-start"},className:(0,r.cx)("chakra-wrap__listitem",n)},o))}));r.Ts&&(se.displayName="WrapItem")},47016:(e,t,n)=>{"use strict";n.d(t,{v2:()=>K,j2:()=>q,sN:()=>X,qy:()=>Y});var i=n(105),o=n(44592),r=n(99860),s=n(67294),a=n(26450);function l(){return l=Object.assign||function(e){for(var t=1;t=t&&(i=0),i}function p(e,t,n){var i=e-1;return n&&i<0&&(i=t),i}var f="undefined"!=typeof window?s.useLayoutEffect:s.useEffect,m=function(){var e=this;this.descendants=new Map,this.register=function(t){var n;if(null!=t)return"object"==typeof(n=t)&&"nodeType"in n&&n.nodeType===Node.ELEMENT_NODE?e.registerNode(t):function(n){e.registerNode(n,t)}},this.unregister=function(t){e.descendants.delete(t);var n=h(Array.from(e.descendants.keys()));e.assignIndex(n)},this.destroy=function(){e.descendants.clear()},this.assignIndex=function(t){e.descendants.forEach((function(e){var n=t.indexOf(e.node);e.index=n,e.node.dataset.index=e.index.toString()}))},this.count=function(){return e.descendants.size},this.enabledCount=function(){return e.enabledValues().length},this.values=function(){return Array.from(e.descendants.values()).sort((function(e,t){return e.index-t.index}))},this.enabledValues=function(){return e.values().filter((function(e){return!e.disabled}))},this.item=function(t){if(0!==e.count())return e.values()[t]},this.enabledItem=function(t){if(0!==e.enabledCount())return e.enabledValues()[t]},this.first=function(){return e.item(0)},this.firstEnabled=function(){return e.enabledItem(0)},this.last=function(){return e.item(e.descendants.size-1)},this.lastEnabled=function(){var t=e.enabledValues().length-1;return e.enabledItem(t)},this.indexOf=function(t){var n,i;return t&&null!=(n=null==(i=e.descendants.get(t))?void 0:i.index)?n:-1},this.enabledIndexOf=function(t){return null==t?-1:e.enabledValues().findIndex((function(e){return e.node.isSameNode(t)}))},this.next=function(t,n){void 0===n&&(n=!0);var i=g(t,e.count(),n);return e.item(i)},this.nextEnabled=function(t,n){void 0===n&&(n=!0);var i=e.item(t);if(i){var o=g(e.enabledIndexOf(i.node),e.enabledCount(),n);return e.enabledItem(o)}},this.prev=function(t,n){void 0===n&&(n=!0);var i=p(t,e.count()-1,n);return e.item(i)},this.prevEnabled=function(t,n){void 0===n&&(n=!0);var i=e.item(t);if(i){var o=p(e.enabledIndexOf(i.node),e.enabledCount()-1,n);return e.enabledItem(o)}},this.registerNode=function(t,n){if(t&&!e.descendants.has(t)){var i=h(Array.from(e.descendants.keys()).concat(t));null!=n&&n.disabled&&(n.disabled=!!n.disabled);var o=u({node:t,index:-1},n);e.descendants.set(t,o),e.assignIndex(i)}}},v=(0,a.kr)({name:"DescendantsProvider",errorMessage:"useDescendantsContext must be used within DescendantsProvider"}),_=v[0],b=v[1],y=n(97375),w=n(66197);function C(){return C=Object.assign||function(e){for(var t=1;t=0||(o[n]=e[n]);return o}var x=["id","closeOnSelect","closeOnBlur","autoSelect","isLazy","isOpen","defaultIsOpen","onClose","onOpen","placement","lazyBehavior","direction","computePositionOnMount"],k=["onMouseEnter","onMouseMove","onMouseLeave","onClick","isDisabled","isFocusable","closeOnSelect"],L=["type","isChecked"],N=[_,function(){return b()},function(){return e=(0,s.useRef)(new m),f((function(){return function(){return e.current.destroy()}})),e.current;var e},function(e){return function(e){var t=b(),n=(0,s.useState)(-1),i=n[0],o=n[1],r=(0,s.useRef)(null);f((function(){return function(){r.current&&t.unregister(r.current)}}),[]),f((function(){if(r.current){var e=Number(r.current.dataset.index);i==e||Number.isNaN(e)||o(e)}}));var l=e?t.register(e):t.register;return{descendants:t,index:i,enabledIndex:t.enabledIndexOf(r.current),register:(0,a.lq)(l,r)}}(e)}],E=N[0],D=N[1],I=N[2],T=N[3],M=(0,a.kr)({strict:!1,name:"MenuContext"}),A=M[0],O=M[1];function R(e){var t;return(0,o.Re)(e)&&!(null==(t=e.getAttribute("role"))||!t.startsWith("menuitem"))}function P(e,t){void 0===e&&(e={}),void 0===t&&(t=null);var n=e,i=n.onMouseEnter,r=n.onMouseMove,u=n.onMouseLeave,h=n.onClick,g=n.isDisabled,p=n.isFocusable,f=n.closeOnSelect,m=S(n,k),v=O(),_=v.setFocusedIndex,b=v.focusedIndex,w=v.closeOnSelect,x=v.onClose,L=v.menuRef,N=v.isOpen,E=v.menuId,D=s.useRef(null),I=E+"-menuitem-"+(0,y.Me)(),M=T({disabled:g&&!p}),A=M.index,P=M.register,F=s.useCallback((function(e){null==i||i(e),g||_(A)}),[_,A,g,i]),B=s.useCallback((function(e){null==r||r(e),D.current&&!(0,o.H9)(D.current)&&F(e)}),[F,r]),W=s.useCallback((function(e){null==u||u(e),g||_(-1)}),[_,g,u]),V=s.useCallback((function(e){null==h||h(e),R(e.currentTarget)&&(null!=f?f:w)&&x()}),[x,h,w,f]),z=A===b,H=g&&!p;return(0,y.rf)((function(){N&&(z&&!H&&D.current?(0,o.T_)(D.current,{nextTick:!0,selectTextIfInput:!1,preventScroll:!1}):L.current&&!(0,o.H9)(L.current)&&(0,o.T_)(L.current,{preventScroll:!1}))}),[z,H,L,N]),C({},m,function(e){void 0===e&&(e={});var t=e,n=t.ref,i=t.isDisabled,r=t.isFocusable,u=t.clickOnEnter,h=void 0===u||u,g=t.clickOnSpace,p=void 0===g||g,f=t.onMouseDown,m=t.onMouseUp,v=t.onClick,_=t.onKeyDown,b=t.onKeyUp,y=t.tabIndex,w=t.onMouseOver,C=t.onMouseLeave,S=function(e,t){if(null==e)return{};var n,i,o={},r=Object.keys(e);for(i=0;i=0||(o[n]=e[n]);return o}(t,c),x=s.useState(!0),k=x[0],L=x[1],N=s.useState(!1),E=N[0],D=N[1],I=function(){var e=s.useRef(new Map),t=e.current,n=s.useCallback((function(t,n,i,o){e.current.set(i,{type:n,el:t,options:o}),t.addEventListener(n,i,o)}),[]),i=s.useCallback((function(t,n,i,o){t.removeEventListener(n,i,o),e.current.delete(i)}),[]);return s.useEffect((function(){return function(){t.forEach((function(e,t){i(e.el,e.type,t,e.options)}))}}),[i,t]),{add:n,remove:i}}(),T=k?y:y||0,M=i&&!r,A=s.useCallback((function(e){if(i)return e.stopPropagation(),void e.preventDefault();e.currentTarget.focus(),null==v||v(e)}),[i,v]),O=s.useCallback((function(e){E&&d(e)&&(e.preventDefault(),e.stopPropagation(),D(!1),I.remove(document,"keyup",O,!1))}),[E,I]),R=s.useCallback((function(e){if(null==_||_(e),!(i||e.defaultPrevented||e.metaKey)&&d(e.nativeEvent)&&!k){var t=h&&"Enter"===e.key;p&&" "===e.key&&(e.preventDefault(),D(!0)),t&&(e.preventDefault(),e.currentTarget.click()),I.add(document,"keyup",O,!1)}}),[i,k,_,h,p,I,O]),P=s.useCallback((function(e){null==b||b(e),i||e.defaultPrevented||e.metaKey||d(e.nativeEvent)&&!k&&p&&" "===e.key&&(e.preventDefault(),D(!1),e.currentTarget.click())}),[p,k,i,b]),F=s.useCallback((function(e){0===e.button&&(D(!1),I.remove(document,"mouseup",F,!1))}),[I]),B=s.useCallback((function(e){if(!(0,o.n_)(e)){if(i)return e.stopPropagation(),void e.preventDefault();k||D(!0),e.currentTarget.focus({preventScroll:!0}),I.add(document,"mouseup",F,!1),null==f||f(e)}}),[i,k,f,I,F]),W=s.useCallback((function(e){(0,o.n_)(e)||(k||D(!1),null==m||m(e))}),[m,k]),V=s.useCallback((function(e){i?e.preventDefault():null==w||w(e)}),[i,w]),z=s.useCallback((function(e){E&&(e.preventDefault(),D(!1)),null==C||C(e)}),[E,C]),H=(0,a.lq)(n,(function(e){e&&"BUTTON"!==e.tagName&&L(!1)}));return l({},S,k?{ref:H,type:"button","aria-disabled":M?void 0:i,disabled:M,onClick:A,onMouseDown:f,onMouseUp:m,onKeyUp:b,onKeyDown:_,onMouseOver:w,onMouseLeave:C}:{ref:H,role:"button","data-active":(0,o.PB)(E),"aria-disabled":i?"true":void 0,tabIndex:M?void 0:T,onClick:A,onMouseDown:B,onMouseUp:W,onKeyUp:P,onKeyDown:R,onMouseOver:V,onMouseLeave:z})}({onClick:V,onMouseEnter:F,onMouseMove:B,onMouseLeave:W,ref:(0,a.lq)(P,D,t),isDisabled:g,isFocusable:p}),{id:I,role:"menuitem",tabIndex:z?0:-1})}var F=["descendants"],B=["children","as"],W=["rootProps"],V=["type"],z=["icon","iconSpacing","command","commandSpacing","children"],H=["icon","iconSpacing"],j=["title","children","className"],U=["className","children"],K=function(e){var t=e.children,n=(0,i.jC)("Menu",e),r=function(e){void 0===e&&(e={});var t=e,n=t.id,i=t.closeOnSelect,r=void 0===i||i,a=t.closeOnBlur,l=void 0===a||a,c=t.autoSelect,d=void 0===c||c,u=t.isLazy,h=t.isOpen,g=t.defaultIsOpen,p=t.onClose,f=t.onOpen,m=t.placement,v=void 0===m?"bottom-start":m,_=t.lazyBehavior,b=void 0===_?"unmount":_,k=t.direction,L=t.computePositionOnMount,N=void 0!==L&&L,E=S(t,x),D=s.useRef(null),T=s.useRef(null),M=I(),A=s.useCallback((function(){(0,o.T_)(D.current,{nextTick:!0,selectTextIfInput:!1})}),[]),O=s.useCallback((function(){var e=setTimeout((function(){var e=M.firstEnabled();e&&K(e.index)}));Y.current.add(e)}),[M]),R=s.useCallback((function(){var e=setTimeout((function(){var e=M.lastEnabled();e&&K(e.index)}));Y.current.add(e)}),[M]),P=s.useCallback((function(){null==f||f(),d?O():A()}),[d,O,A,f]),F=(0,y.qY)({isOpen:h,defaultIsOpen:g,onClose:p,onOpen:P}),B=F.isOpen,W=F.onOpen,V=F.onClose,z=F.onToggle;(0,y.O3)({enabled:B&&l,ref:D,handler:function(e){var t;null!=(t=T.current)&&t.contains(e.target)||V()}});var H=(0,w.D)(C({},E,{enabled:B||N,placement:v,direction:k})),j=s.useState(-1),U=j[0],K=j[1];(0,y.rf)((function(){B||K(-1)}),[B]),(0,y.Ck)(D,{focusRef:T,visible:B,shouldFocus:!0});var $=(0,y.ZS)(n,"menu-button","menu-list"),q=$[0],Z=$[1],G=s.useCallback((function(){W(),A()}),[W,A]),Y=s.useRef(new Set([]));return(0,y.zq)((function(){Y.current.forEach((function(e){return clearTimeout(e)})),Y.current.clear()})),{openAndFocusMenu:G,openAndFocusFirstItem:s.useCallback((function(){W(),O()}),[O,W]),openAndFocusLastItem:s.useCallback((function(){W(),R()}),[W,R]),onTransitionEnd:s.useCallback((function(){var e,t,n=(0,o.lZ)(D.current),i=null==(e=D.current)?void 0:e.contains(n.activeElement);if(B&&!i){var r=null==(t=M.item(U))?void 0:t.node;r&&(0,o.T_)(r,{selectTextIfInput:!1,preventScroll:!1})}}),[B,U,M]),descendants:M,popper:H,buttonId:q,menuId:Z,forceUpdate:H.forceUpdate,orientation:"vertical",isOpen:B,onToggle:z,onOpen:W,onClose:V,menuRef:D,buttonRef:T,focusedIndex:U,closeOnSelect:r,closeOnBlur:l,autoSelect:d,setFocusedIndex:K,isLazy:u,lazyBehavior:b}}(C({},(0,i.Lr)(e),{direction:(0,i.Fg)().direction})),a=r.descendants,l=S(r,F),c=s.useMemo((function(){return l}),[l]),d=c.isOpen,u=c.onClose,h=c.forceUpdate;return s.createElement(E,{value:a},s.createElement(A,{value:c},s.createElement(i.Fo,{value:n},(0,o.Pu)(t,{isOpen:d,onClose:u,forceUpdate:h}))))};o.Ts&&(K.displayName="Menu");var $=(0,i.Gp)((function(e,t){var n=(0,i.yK)();return s.createElement(i.m$.button,C({ref:t},e,{__css:C({display:"inline-flex",appearance:"none",alignItems:"center",outline:0},n.button)}))})),q=(0,i.Gp)((function(e,t){e.children;var n=e.as,r=function(e,t){void 0===e&&(e={}),void 0===t&&(t=null);var n=O(),i=n.onToggle,r=n.popper,l=n.openAndFocusFirstItem,c=n.openAndFocusLastItem,d=s.useCallback((function(e){var t=(0,o.uh)(e),n={Enter:l,ArrowDown:l,ArrowUp:c}[t];n&&(e.preventDefault(),e.stopPropagation(),n(e))}),[l,c]);return C({},e,{ref:(0,a.lq)(n.buttonRef,t,r.referenceRef),id:n.buttonId,"data-active":(0,o.PB)(n.isOpen),"aria-expanded":n.isOpen,"aria-haspopup":"menu","aria-controls":n.menuId,onClick:(0,o.v0)(e.onClick,i),onKeyDown:(0,o.v0)(e.onKeyDown,d)})}(S(e,B),t),l=n||$;return s.createElement(l,C({},r,{className:(0,o.cx)("chakra-menu__menu-button",e.className)}),s.createElement(i.m$.span,{__css:{pointerEvents:"none",flex:"1 1 auto",minW:0}},e.children))}));o.Ts&&(q.displayName="MenuButton");var Z={enter:{visibility:"visible",opacity:1,scale:1,transition:{duration:.2,ease:[.4,0,.2,1]}},exit:{transitionEnd:{visibility:"hidden"},opacity:0,scale:.8,transition:{duration:.1,easings:"easeOut"}}},G="custom"in r.E?r.E.custom(i.m$.div):(0,r.E)(i.m$.div),Y=(0,i.Gp)((function(e,t){var n,r,l=e.rootProps,c=S(e,W),d=O(),u=d.isOpen,h=d.onTransitionEnd,g=function(e,t){void 0===e&&(e={}),void 0===t&&(t=null);var n=O();if(!n)throw new Error("useMenuContext: context is undefined. Seems you forgot to wrap component within ");var i=n.focusedIndex,r=n.setFocusedIndex,l=n.menuRef,c=n.isOpen,d=n.onClose,u=n.menuId,h=n.isLazy,g=n.lazyBehavior,p=D(),f=(0,y.bx)({preventDefault:function(e){return" "!==e.key&&R(e.target)}}),m=s.useCallback((function(e){var t=(0,o.uh)(e),n={Tab:function(e){return e.preventDefault()},Escape:d,ArrowDown:function(){var e=p.nextEnabled(i);e&&r(e.index)},ArrowUp:function(){var e=p.prevEnabled(i);e&&r(e.index)}},s=n[t];if(s)return e.preventDefault(),void s(e);var a=f((function(e){var t=(0,o.LP)(p.values(),e,(function(e){var t,n;return null!=(t=null==e||null==(n=e.node)?void 0:n.textContent)?t:""}),p.item(i));if(t){var n=p.indexOf(t.node);r(n)}}));R(e.target)&&a(e)}),[p,i,f,d,r]),v=s.useRef(!1);c&&(v.current=!0);var _=(0,o.VI)({hasBeenSelected:v.current,isLazy:h,lazyBehavior:g,isSelected:c});return C({},e,{ref:(0,a.lq)(l,t),children:_?e.children:null,tabIndex:-1,role:"menu",id:u,style:C({},e.style,{transformOrigin:"var(--popper-transform-origin)"}),"aria-orientation":"vertical",onKeyDown:(0,o.v0)(e.onKeyDown,m)})}(c,t),p=function(e){void 0===e&&(e={});var t=O(),n=t.popper,i=t.isOpen;return n.getPopperProps(C({},e,{style:C({visibility:i?"visible":"hidden"},e.style)}))}(l),f=(0,i.yK)();return s.createElement(i.m$.div,C({},p,{__css:{zIndex:null!=(n=e.zIndex)?n:null==(r=f.list)?void 0:r.zIndex}}),s.createElement(G,C({},g,{onUpdate:h,className:(0,o.cx)("chakra-menu__menu-list",g.className),variants:Z,initial:!1,animate:u?"enter":"exit",__css:C({outline:0},f.list)})))}));o.Ts&&(Y.displayName="MenuList");var Q=(0,i.Gp)((function(e,t){var n=e.type,o=S(e,V),r=(0,i.yK)(),a=o.as?null!=n?n:void 0:"button",l=C({textDecoration:"none",color:"inherit",userSelect:"none",display:"flex",width:"100%",alignItems:"center",textAlign:"start",flex:"0 0 auto",outline:0},r.item);return s.createElement(i.m$.button,C({ref:t,type:a},o,{__css:l}))})),X=(0,i.Gp)((function(e,t){var n=e.icon,i=e.iconSpacing,r=void 0===i?"0.75rem":i,a=e.command,l=e.commandSpacing,c=void 0===l?"0.75rem":l,d=e.children,u=P(S(e,z),t),h=n||a?s.createElement("span",{style:{pointerEvents:"none",flex:1}},d):d;return s.createElement(Q,C({},u,{className:(0,o.cx)("chakra-menu__menuitem",u.className)}),n&&s.createElement(ie,{fontSize:"0.8em",marginEnd:r},n),h,a&&s.createElement(ne,{marginStart:c},a))}));o.Ts&&(X.displayName="MenuItem");var J=function(e){return s.createElement("svg",C({viewBox:"0 0 14 14",width:"1em",height:"1em"},e),s.createElement("polygon",{fill:"currentColor",points:"5.5 11.9993304 14 3.49933039 12.5 2 5.5 8.99933039 1.5 4.9968652 0 6.49933039"}))},ee=(0,i.Gp)((function(e,t){var n=e.icon,i=e.iconSpacing,r=void 0===i?"0.75rem":i,a=S(e,H),l=function(e,t){void 0===e&&(e={}),void 0===t&&(t=null);var n=e,i=n.type,o=void 0===i?"radio":i,r=n.isChecked;return C({},P(S(n,L),t),{role:"menuitem"+o,"aria-checked":r})}(a,t);return s.createElement(Q,C({},l,{className:(0,o.cx)("chakra-menu__menuitem-option",a.className)}),s.createElement(ie,{fontSize:"0.8em",marginEnd:r,opacity:e.isChecked?1:0},n||s.createElement(J,null)),s.createElement("span",{style:{flex:1}},l.children))}));ee.id="MenuItemOption",o.Ts&&(ee.displayName="MenuItemOption"),o.Ts;var te=(0,i.Gp)((function(e,t){var n=e.title,r=e.children,a=e.className,l=S(e,j),c=(0,o.cx)("chakra-menu__group__title",a),d=(0,i.yK)();return s.createElement("div",{ref:t,className:"chakra-menu__group",role:"group"},n&&s.createElement(i.m$.p,C({className:c},l,{__css:d.groupTitle}),n),r)}));o.Ts&&(te.displayName="MenuGroup");var ne=(0,i.Gp)((function(e,t){var n=(0,i.yK)();return s.createElement(i.m$.span,C({ref:t},e,{__css:n.command,className:"chakra-menu__command"}))}));o.Ts&&(ne.displayName="MenuCommand");var ie=function(e){var t=e.className,n=e.children,r=S(e,U),a=s.Children.only(n),l=s.isValidElement(a)?s.cloneElement(a,{focusable:"false","aria-hidden":!0,className:(0,o.cx)("chakra-menu__icon",a.props.className)}):null,c=(0,o.cx)("chakra-menu__icon-wrapper",t);return s.createElement(i.m$.span,C({className:c},r,{__css:{flexShrink:0}}),l)};o.Ts&&(ie.displayName="MenuIcon"),o.Ts},68016:(e,t,n)=>{"use strict";n.d(t,{u_:()=>rn,fe:()=>un,ol:()=>gn,hz:()=>an,mz:()=>hn,xB:()=>dn,ZA:()=>cn});var i=n(84746),o=n(67294),r=n(87462),s=(n(45697),"data-focus-lock"),a="data-focus-lock-disabled";function l(e,t){return n=t,i=function(t){return e.forEach((function(e){return function(e,t){return"function"==typeof e?e(t):e&&(e.current=t),e}(e,t)}))},(r=(0,o.useState)((function(){return{value:n,callback:i,facade:{get current(){return r.value},set current(e){var t=r.value;t!==e&&(r.value=e,r.callback(e,t))}}}}))[0]).callback=i,r.facade;var n,i,r}var c={width:"1px",height:"0px",padding:0,overflow:"hidden",position:"fixed",top:"1px",left:"1px"},d=function(e){var t=e.children;return o.createElement(o.Fragment,null,o.createElement("div",{key:"guard-first","data-focus-guard":!0,"data-focus-auto-guard":!0,style:c}),t,t&&o.createElement("div",{key:"guard-last","data-focus-guard":!0,"data-focus-auto-guard":!0,style:c}))};d.propTypes={},d.defaultProps={children:null};var u=function(){return u=Object.assign||function(e){for(var t,n=1,i=arguments.length;n1?L(e[0],e):e[0]},E=function(e,t){return e.length>1?e.indexOf(L(e[t],e)):t},D=function(e,t){var n=e.get(t);if(void 0!==n)return n;var i=function(e,t){return!e||e===document||e&&e.nodeType===Node.DOCUMENT_NODE||!function(e){if(e.nodeType!==Node.ELEMENT_NODE)return!1;var t=window.getComputedStyle(e,null);return!(!t||!t.getPropertyValue||"none"!==t.getPropertyValue("display")&&"hidden"!==t.getPropertyValue("visibility"))}(e)&&t(e.parentNode&&e.parentNode.nodeType===Node.DOCUMENT_FRAGMENT_NODE?e.parentNode.host:e.parentNode)}(t,D.bind(void 0,e));return e.set(t,i),i},I=function(e){return Boolean(e&&e.dataset&&e.dataset.focusGuard)},T=function(e){return!I(e)},M=function(e){return Boolean(e)},A="NEW_FOCUS",O=function(e){for(var t=Array(e.length),n=0;n0&&t.add(o),(r&Node.DOCUMENT_POSITION_CONTAINS)>0&&t.add(i)}return e.filter((function(e,n){return!t.has(n)}))}(O(P(t).querySelectorAll('[data-focus-lock="'+n+'"]:not(['+a+'="disabled"])'))):[t]),e}),[])},B=function(e,t){var n=e.tabIndex-t.tabIndex,i=e.index-t.index;if(n){if(!e.tabIndex)return 1;if(!t.tabIndex)return-1}return n||i},W=function(e,t,n){return O(e).map((function(e,t){return{node:e,index:t,tabIndex:n&&-1===e.tabIndex?(e.dataset||{}).focusGuard?0:-1:e.tabIndex}})).filter((function(e){return!t||e.tabIndex>=0})).sort(B)},V=["button:enabled","select:enabled","textarea:enabled","input:enabled","a[href]","area[href]","summary","iframe","object","embed","audio[controls]","video[controls]","[tabindex]","[contenteditable]","[autofocus]"].join(","),z=V+", [data-focus-guard]",H=function(e,t){return e.reduce((function(e,n){return e.concat(O(n.querySelectorAll(t?z:V)),n.parentNode?O(n.parentNode.querySelectorAll(V)).filter((function(e){return e===n})):[])}),[])},j=function(e,t){return O(e).filter((function(e){return D(t,e)})).filter((function(e){return function(e){return!(("INPUT"===e.tagName||"BUTTON"===e.tagName)&&("hidden"===e.type||e.disabled))}(e)}))},U=function(e,t,n){return W(j(H(e,n),t),!0,n)},K=function(e,t){return W(j(H(e),t),!1)},$=function(e,t){return void 0===t&&(t=[]),t.push(e),e.parentNode&&$(e.parentNode,t),t},q=function(e,t){for(var n=$(e),i=$(t),o=0;o=0)return r}return!1},Z=function(e,t,n){var i=R(e),o=R(t),r=i[0],s=!1;return o.filter(Boolean).forEach((function(e){s=q(s||e,e)||s,n.filter(Boolean).forEach((function(e){var t=q(r,e);t&&(s=!s||t.contains(s)?t:q(t,s))}))})),s},G=function(e,t){var n=document&&document.activeElement,i=F(e).filter(T),o=Z(n||e,e,i),r=new Map,s=K(i,r),a=U(i,r).filter((function(e){var t=e.node;return T(t)}));if(a[0]||(a=s)[0]){var l,c,d,u,h=K([o],r).map((function(e){return e.node})),g=(l=h,c=a,d=new Map,c.forEach((function(e){return d.set(e.node,e)})),l.map((function(e){return d.get(e)})).filter(M)),p=g.map((function(e){return e.node})),f=function(e,t,n,i){var o=e.length,r=e[0],s=e[o-1],a=I(n);if(!(e.indexOf(n)>=0)){var l,c,d=t.indexOf(n),u=i?t.indexOf(i):d,h=i?e.indexOf(i):-1,g=d-u,p=t.indexOf(r),f=t.indexOf(s),m=(l=t,c=new Set,l.forEach((function(e){return c.add(L(e,l))})),l.filter((function(e){return c.has(e)}))),v=m.indexOf(n)-(i?m.indexOf(i):d),_=E(e,0),b=E(e,o-1);return-1===d||-1===h?A:!g&&h>=0?h:d<=p&&a&&Math.abs(g)>1?b:d>=f&&a&&Math.abs(g)>1?_:g&&Math.abs(v)>1?h:d<=p?b:d>f?_:g?Math.abs(g)>1?h:(o+h+g)%o:void 0}}(p,h,n,t);if(f===A){var m=s.map((function(e){return e.node})).filter((u=function(e,t){return e.reduce((function(e,n){return e.concat(function(e,t){return j((n=e.querySelectorAll("[data-autofocus-inside]"),O(n).map((function(e){return H([e])})).reduce((function(e,t){return e.concat(t)}),[])),t);var n}(n,t))}),[])}(i,r),function(e){return e.autofocus||e.dataset&&!!e.dataset.autofocus||u.indexOf(e)>=0}));return{node:m&&m.length?N(m):N(p)}}return void 0===f?f:g[f]}},Y=0,Q=!1;const X=function(e,t){var n,i=G(e,t);if(!Q&&i){if(Y>2)return console.error("FocusLock: focus-fighting detected. Only one focus management system could be active. See https://github.com/theKashey/focus-lock/#focus-fighting"),Q=!0,void setTimeout((function(){Q=!1}),1);Y++,(n=i.node).focus(),"contentWindow"in n&&n.contentWindow&&n.contentWindow.focus(),Y--}};var J=function(e){var t=document&&document.activeElement;return!(!t||t.dataset&&t.dataset.focusGuard)&&F(e).reduce((function(e,n){return e||n.contains(t)||function(e){return Boolean(O(e.querySelectorAll("iframe")).some((function(e){return e===document.activeElement})))}(n)}),!1)};function ee(e){var t=window.setImmediate;void 0!==t?t(e):setTimeout(e,1)}var te=null,ne=null,ie=null,oe=!1,re=function(){return!0};function se(e,t,n,i){var o=null,r=e;do{var s=i[r];if(s.guard)s.node.dataset.focusAutoGuard&&(o=s);else{if(!s.lockItem)break;if(r!==e)return;o=null}}while((r+=n)!==t);o&&(o.node.tabIndex=0)}var ae=function(e){return e&&"current"in e?e.current:e},le=function(){var e,t,n,i,o,r,s,a=!1;if(te){var l=te,c=l.observed,d=l.persistentFocus,u=l.autoFocus,h=l.shards,g=l.crossFrame,p=c||ie&&ie.portaledElement,f=document&&document.activeElement;if(p){var m=[p].concat(h.map(ae).filter(Boolean));if(f&&!function(e){return(te.whiteList||re)(e)}(f)||(d||(g?Boolean(oe):"meanwhile"===oe)||!(document&&document.activeElement===document.body||document&&O(document.querySelectorAll("[data-no-focus-lock]")).some((function(e){return e.contains(document.activeElement)})))||!ne&&u)&&(!p||J(m)||(s=f,ie&&ie.portaledElement===s)||(document&&!ne&&f&&!u?(f.blur&&f.blur(),document.body.focus()):(a=X(m,ne),ie={})),oe=!1,ne=document&&document.activeElement),document){var v=document&&document.activeElement,_=(t=F(e=m).filter(T),n=Z(e,e,t),i=new Map,o=U([n],i,!0),r=U(t,i).filter((function(e){var t=e.node;return T(t)})).map((function(e){return e.node})),o.map((function(e){var t=e.node;return{node:t,index:e.index,lockItem:r.indexOf(t)>=0,guard:I(t)}}))),b=_.map((function(e){return e.node})).indexOf(v);b>-1&&(_.filter((function(e){var t=e.guard,n=e.node;return t&&n.dataset.focusAutoGuard})).forEach((function(e){return e.node.removeAttribute("tabIndex")})),se(b,_.length,1,_),se(b,-1,-1,_))}}}return a},ce=function(e){le()&&e&&(e.stopPropagation(),e.preventDefault())},de=function(){return ee(le)},ue=function(){oe="just",setTimeout((function(){oe="meanwhile"}),0)};m.assignSyncMedium((function(e){var t=e.target,n=e.currentTarget;n.contains(t)||(ie={observerNode:n,portaledElement:t})})),v.assignMedium(de),_.assignMedium((function(e){return e({moveFocusInside:X,focusInside:J})}));const he=(ge=function(e){return e.filter((function(e){return!e.disabled}))},pe=function(e){var t=e.slice(-1)[0];t&&!te&&(document.addEventListener("focusin",ce,!0),document.addEventListener("focusout",de),window.addEventListener("blur",ue));var n=te,i=n&&t&&t.id===n.id;te=t,n&&!i&&(n.onDeactivation(),e.filter((function(e){return e.id===n.id})).length||n.returnFocus(!t)),t?(ne=null,i&&n.observed===t.observed||t.onActivation(),le(),ee(le)):(document.removeEventListener("focusin",ce,!0),document.removeEventListener("focusout",de),window.removeEventListener("blur",ue),ne=null)},function(e){var t,n=[];function i(){t=ge(n.map((function(e){return e.props}))),pe(t)}var r=function(r){var s,a;function l(){return r.apply(this,arguments)||this}a=r,(s=l).prototype=Object.create(a.prototype),s.prototype.constructor=s,S(s,a),l.peek=function(){return t};var c=l.prototype;return c.componentDidMount=function(){n.push(this),i()},c.componentDidUpdate=function(){i()},c.componentWillUnmount=function(){var e=n.indexOf(this);n.splice(e,1),i()},c.render=function(){return o.createElement(e,this.props)},l}(o.PureComponent);return(0,x.Z)(r,"displayName","SideEffect("+function(e){return e.displayName||e.name||"Component"}(e)+")"),r})((function(){return null}));var ge,pe,fe=o.forwardRef((function(e,t){return o.createElement(C,(0,r.Z)({sideCar:he,ref:t},e))})),me=C.propTypes||{};me.sideCar,function(e,t){if(null==e)return{};var n,i,o={},r=Object.keys(e);for(i=0;i=0||(o[n]=e[n])}(me,["sideCar"]),fe.propTypes={};const ve=fe;var _e=n(44592),be=function(e){var t=e.initialFocusRef,n=e.finalFocusRef,i=e.contentRef,r=e.restoreFocus,s=e.children,a=e.isDisabled,l=e.autoFocus,c=e.persistentFocus,d=e.lockFocusAcrossFrames,u=o.useCallback((function(){null!=t&&t.current?t.current.focus():null!=i&&i.current&&0===(0,_e.t5)(i.current).length&&(0,_e.T_)(i.current,{nextTick:!0})}),[t,i]),h=o.useCallback((function(){var e;null==n||null==(e=n.current)||e.focus()}),[n]),g=r&&!n;return o.createElement(ve,{crossFrame:d,persistentFocus:c,autoFocus:l,disabled:a,onActivation:u,onDeactivation:h,returnFocus:g},s)};_e.Ts&&(be.displayName="FocusLock");var ye=n(46871),we=n(105),Ce=n(38554),Se=n.n(Ce),xe=n(53869),ke=n(99860);function Le(e,t){if(null==e)return{};var n,i,o={},r=Object.keys(e);for(i=0;i=0||(o[n]=e[n]);return o}function Ne(){return Ne=Object.assign||function(e){for(var t=1;t0?1:0)},{overflow:"hidden",height:o,transitionEnd:null==s?void 0:s.exit,transition:null!=(t=null==r?void 0:r.exit)?t:Pe(Be.exit,a)})},enter:function(e){var t,n=e.animateOpacity,i=e.endingHeight,o=e.transition,r=e.transitionEnd,s=e.delay;return Ne({},n&&{opacity:1},{height:i,transitionEnd:null==r?void 0:r.enter,transition:null!=(t=null==o?void 0:o.enter)?t:Re(Be.enter,s)})}},Ve=o.forwardRef((function(e,t){var n=e.in,i=e.unmountOnExit,r=e.animateOpacity,s=void 0===r||r,a=e.startingHeight,l=void 0===a?0:a,c=e.endingHeight,d=void 0===c?"auto":c,u=e.style,h=e.className,g=e.transition,p=e.transitionEnd,f=Le(e,Fe),m=o.useState(!1),v=m[0],_=m[1];o.useEffect((function(){var e=setTimeout((function(){_(!0)}));return function(){return clearTimeout(e)}}),[]),(0,_e.ZK)({condition:Boolean(l>0&&i),message:"startingHeight and unmountOnExit are mutually exclusive. You can't use them together"});var b=parseFloat(l.toString())>0,y={startingHeight:l,endingHeight:d,animateOpacity:s,transition:v?g:{enter:{duration:0}},transitionEnd:Se()(p,{enter:{overflow:"initial"},exit:i?void 0:{display:b?"block":"none"}})},w=!i||n,C=n||i?"enter":"exit";return o.createElement(xe.M,{initial:!1,custom:y},w&&o.createElement(ke.E.div,Ne({ref:t},f,{className:(0,_e.cx)("chakra-collapse",h),style:Ne({overflow:"hidden",display:"block"},u),custom:y,variants:We,initial:!!i&&"exit",animate:C,exit:"exit"})))}));_e.Ts&&(Ve.displayName="Collapse");var ze=["unmountOnExit","in","className","transition","transitionEnd","delay"],He={enter:function(e){var t,n=void 0===e?{}:e,i=n.transition,o=n.transitionEnd,r=n.delay;return{opacity:1,transition:null!=(t=null==i?void 0:i.enter)?t:Re(Oe.enter,r),transitionEnd:null==o?void 0:o.enter}},exit:function(e){var t,n=void 0===e?{}:e,i=n.transition,o=n.transitionEnd,r=n.delay;return{opacity:0,transition:null!=(t=null==i?void 0:i.exit)?t:Pe(Oe.exit,r),transitionEnd:null==o?void 0:o.exit}}},je={initial:"exit",animate:"enter",exit:"exit",variants:He},Ue=o.forwardRef((function(e,t){var n=e.unmountOnExit,i=e.in,r=e.className,s=e.transition,a=e.transitionEnd,l=e.delay,c=Le(e,ze),d=i||n?"enter":"exit",u=!n||i&&n,h={transition:s,transitionEnd:a,delay:l};return o.createElement(xe.M,{custom:h},u&&o.createElement(ke.E.div,Ne({ref:t,className:(0,_e.cx)("chakra-fade",r),custom:h},je,{animate:d},c)))}));_e.Ts&&(Ue.displayName="Fade");var Ke=["unmountOnExit","in","reverse","initialScale","className","transition","transitionEnd","delay"],$e={exit:function(e){var t,n=e.reverse,i=e.initialScale,o=e.transition,r=e.transitionEnd,s=e.delay;return Ne({opacity:0},n?{scale:i,transitionEnd:null==r?void 0:r.exit}:{transitionEnd:Ne({scale:i},null==r?void 0:r.exit)},{transition:null!=(t=null==o?void 0:o.exit)?t:Pe(Oe.exit,s)})},enter:function(e){var t,n=e.transitionEnd,i=e.transition,o=e.delay;return{opacity:1,scale:1,transition:null!=(t=null==i?void 0:i.enter)?t:Re(Oe.enter,o),transitionEnd:null==n?void 0:n.enter}}},qe={initial:"exit",animate:"enter",exit:"exit",variants:$e},Ze=o.forwardRef((function(e,t){var n=e.unmountOnExit,i=e.in,r=e.reverse,s=void 0===r||r,a=e.initialScale,l=void 0===a?.95:a,c=e.className,d=e.transition,u=e.transitionEnd,h=e.delay,g=Le(e,Ke),p=!n||i&&n,f=i||n?"enter":"exit",m={initialScale:l,reverse:s,transition:d,transitionEnd:u,delay:h};return o.createElement(xe.M,{custom:m},p&&o.createElement(ke.E.div,Ne({ref:t,className:(0,_e.cx)("chakra-offset-slide",c)},qe,{animate:f,custom:m},g)))}));_e.Ts&&(Ze.displayName="ScaleFade");var Ge=["direction","style","unmountOnExit","in","className","transition","transitionEnd","delay"],Ye={exit:{duration:.15,ease:Ee.easeInOut},enter:{type:"spring",damping:25,stiffness:180}},Qe={exit:function(e){var t,n=e.direction,i=e.transition,o=e.transitionEnd,r=e.delay;return Ne({},Ae({direction:n}).exit,{transition:null!=(t=null==i?void 0:i.exit)?t:Pe(Ye.exit,r),transitionEnd:null==o?void 0:o.exit})},enter:function(e){var t,n=e.direction,i=e.transitionEnd,o=e.transition,r=e.delay;return Ne({},Ae({direction:n}).enter,{transition:null!=(t=null==o?void 0:o.enter)?t:Re(Ye.enter,r),transitionEnd:null==i?void 0:i.enter})}},Xe=o.forwardRef((function(e,t){var n=e.direction,i=void 0===n?"right":n,r=e.style,s=e.unmountOnExit,a=e.in,l=e.className,c=e.transition,d=e.transitionEnd,u=e.delay,h=Le(e,Ge),g=Ae({direction:i}),p=Object.assign({position:"fixed"},g.position,r),f=!s||a&&s,m=a||s?"enter":"exit",v={transitionEnd:d,transition:c,direction:i,delay:u};return o.createElement(xe.M,{custom:v},f&&o.createElement(ke.E.div,Ne({ref:t,initial:"exit",className:(0,_e.cx)("chakra-slide",l),animate:m,exit:"exit",custom:v,variants:Qe,style:p},h)))}));_e.Ts&&(Xe.displayName="Slide");var Je=["unmountOnExit","in","reverse","className","offsetX","offsetY","transition","transitionEnd","delay"],et={initial:function(e){var t,n=e.offsetX,i=e.offsetY,o=e.transition,r=e.transitionEnd,s=e.delay;return{opacity:0,x:n,y:i,transition:null!=(t=null==o?void 0:o.exit)?t:Pe(Oe.exit,s),transitionEnd:null==r?void 0:r.exit}},enter:function(e){var t,n=e.transition,i=e.transitionEnd,o=e.delay;return{opacity:1,x:0,y:0,transition:null!=(t=null==n?void 0:n.enter)?t:Re(Oe.enter,o),transitionEnd:null==i?void 0:i.enter}},exit:function(e){var t,n=e.offsetY,i=e.offsetX,o=e.transition,r=e.transitionEnd,s=e.reverse,a=e.delay,l={x:i,y:n};return Ne({opacity:0,transition:null!=(t=null==o?void 0:o.exit)?t:Pe(Oe.exit,a)},s?Ne({},l,{transitionEnd:null==r?void 0:r.exit}):{transitionEnd:Ne({},l,null==r?void 0:r.exit)})}},tt={initial:"initial",animate:"enter",exit:"exit",variants:et},nt=o.forwardRef((function(e,t){var n=e.unmountOnExit,i=e.in,r=e.reverse,s=void 0===r||r,a=e.className,l=e.offsetX,c=void 0===l?0:l,d=e.offsetY,u=void 0===d?8:d,h=e.transition,g=e.transitionEnd,p=e.delay,f=Le(e,Je),m=!n||i&&n,v=i||n?"enter":"exit",_={offsetX:c,offsetY:u,reverse:s,transition:h,transitionEnd:g,delay:p};return o.createElement(xe.M,{custom:_},m&&o.createElement(ke.E.div,Ne({ref:t,className:(0,_e.cx)("chakra-offset-slide",a),custom:_},tt,{animate:v},f)))}));_e.Ts&&(nt.displayName="SlideFade");var it=n(26450),ot=n(69283),rt=function(){return rt=Object.assign||function(e){for(var t,n=1,i=arguments.length;n