Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix missing error check in AST for expr->intexpr conversion; add new test modality #247

Merged
merged 28 commits into from
Mar 17, 2024
Merged

Fix missing error check in AST for expr->intexpr conversion; add new test modality #247

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
57a3102
forge_error test modality, multiple tests, improve messages from AST
tnelson Mar 2, 2024
1268d93
more error fixes, tests
tnelson Mar 2, 2024
3bd96f7
add more AST last-resort tests
tnelson Mar 4, 2024
607c43d
working
tnelson Mar 4, 2024
f087e33
fix another bad error message
tnelson Mar 4, 2024
81905de
add missing test
tnelson Mar 4, 2024
161f388
error improvements, more tests
tnelson Mar 5, 2024
0a8210a
fix typo in tests script
tnelson Mar 5, 2024
6ffd7c7
more testS
tnelson Mar 5, 2024
0da8384
more tests, slight error improvement
tnelson Mar 5, 2024
594eeba
renaming test files rkt to frg
tnelson Mar 5, 2024
aac03f5
fix: filename extension
tnelson Mar 5, 2024
d46997f
working -- more tests, use raise-forge-error more, identify 3 to-dos
tnelson Mar 5, 2024
c7b9bcd
checker descends into RHS of a minus; add test; add another to-do
tnelson Mar 5, 2024
8d2a983
check for variable shadowing within quantifiers, more tests
tnelson Mar 5, 2024
c5173bf
working
tnelson Mar 7, 2024
4db3f8e
add: better error for ifte mismatch of args
tnelson Mar 13, 2024
162c711
prototype fix for pfunc breaker variable names
tnelson Mar 14, 2024
70df030
further progress, repair missing stxloc. todo: error in breakers.frg …
tnelson Mar 14, 2024
5e45b21
resolve old error
tnelson Mar 14, 2024
0e51f65
Merge branch 'dev' into fix_ast_errorcheck
tnelson Mar 16, 2024
5b33114
revise tests after merge
tnelson Mar 16, 2024
2ca5bf5
working simultaneously on: shadowing (todo: comp. case, use identity …
tnelson Mar 16, 2024
2790b49
add: sterling PR 16: target/source index
tnelson Mar 17, 2024
da233ff
working
tnelson Mar 17, 2024
bf04043
walk back shadowing by name rather than by id
tnelson Mar 17, 2024
5289198
resolve intra-quantifier/comp shadowing issue
tnelson Mar 17, 2024
d192302
fix typo, old error test
tnelson Mar 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 36 additions & 20 deletions forge/breaks.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -652,11 +652,18 @@

(define (funcformula rllst quantvarlst)
(cond
[(empty? (rest (rest rllst)))
(let ([a (gensym)])
(@all/info (@just-location-info loc) ([a (first rllst)]) (@one (funcformulajoin (cons a quantvarlst)))))]
[else (let ([a (gensym)])
(@all/info (@just-location-info loc) ([a (first rllst)]) (funcformula (rest rllst) (cons a quantvarlst))))]))
[(empty? (rest (rest rllst)))
(let* ([var-id (gensym 'pfunc)]
[a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
(@quantified-formula (@just-location-info loc) 'all
(list (cons a (first rllst)))
(@one (funcformulajoin (cons a quantvarlst)))))]
[else
(let* ([var-id (gensym 'pfunc)]
[a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
(@quantified-formula (@just-location-info loc) 'all
(list (cons a (first rllst)))
(funcformula (rest rllst) (cons a quantvarlst))))]))
(define formulas (set (funcformula rel-list (list))))

; OLD CODE
Expand Down Expand Up @@ -716,22 +723,31 @@
(λ () (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)))
(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)))))]
[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)))
(pfuncformula (rest rllst) (cons a quantvarlst))))]))
(define pf-fmla (pfuncformula rel-list (list)))
(define formulas (set pf-fmla))

; OLD CODE
; (if (equal? A B)
; (formula-breaker pri ; TODO: can improve, but need better symmetry-breaking predicates
Expand Down
3 changes: 2 additions & 1 deletion forge/lang/alloy-syntax/lexer.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
3 changes: 2 additions & 1 deletion forge/lang/alloy-syntax/parser.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)?
Expand Down
Loading
Loading