PositivityChecker for Haskell - #21
Conversation
add: PositivityChecker
updating
bring testing up to date
error handling, with ParseError
Add newest commits to my fork
eleanoremeyer
left a comment
eleanoremeyer
left a comment
There was a problem hiding this comment.
We should discuss this in person. @faiso-k
There was a problem hiding this comment.
Where are these imports used?
| JUST_NEG, | ||
| JUST_POS, | ||
| STRICT_POS, | ||
| // GUARD_POS, //not quite sure (think it is for records) |
There was a problem hiding this comment.
We should discuss this
| UNUSED; // does not occur | ||
|
|
||
| /** | ||
| * Simulates behavior of additive of the Occurrence semiring (a+b): |
There was a problem hiding this comment.
additive behavior (state what it is used for)
| } | ||
|
|
||
| /** | ||
| * Simulates behavior of multiplicative of the Occurrence semiring (a*b): |
There was a problem hiding this comment.
multiplicative behavior (state what it is used for)
| import java.io.*; | ||
| import java.util.*; | ||
|
|
||
| import aprove.input.Programs.haskell.StrictPositivityException; |
There was a problem hiding this comment.
Where is this import used?
| final List<HaskellDecl> decls = new ArrayList<>(List.of()); | ||
|
|
||
| for (var module : modMap.values()) { | ||
| decls.addAll(module.getDecls()); |
There was a problem hiding this comment.
What if two modules contain declarations with same name?
| // } | ||
| // } | ||
|
|
||
| final List<DataDecl> dataDecl = decls.stream() |
There was a problem hiding this comment.
Explicit for-each loop so you save redundancy and traverse only once.
| // OccurrenceGraph graph = builder.buildFromDataDecl(dataDecl, synTypeDecls, preludeTyCons); | ||
|
|
||
| List<Violation> violations = new ArrayList<>(); | ||
| Map<String, Occurrence> selfLoops = new LinkedHashMap<>(); |
There was a problem hiding this comment.
What is this used for?
| } | ||
|
|
||
| public void check(Modules mods) throws StrictPositivityException { | ||
| // debug(mods); |
| throw new StrictPositivityException(sb.toString()); | ||
| } | ||
| } | ||
|
|
There was a problem hiding this comment.
Add explanation to this function and checkForIOResult
| //check if arrow function | ||
| if (name.equals("->")) { | ||
| // System.out.println("WalkArrow called"); | ||
| walkArrow(apply, pol, target); |
There was a problem hiding this comment.
Isn't this the same as
walkType(args[0], flip(pol), target)
walkType(args[1], pol, target)
3 participants
Pull Request
Pre-Submission Checklist
Before submitting this PR, please confirm:
Summary
Type of Change
Select all that apply:
Testing
Tested on TPDB and own test cases
✅ Final Checklist
Additional Notes
New Exception StrictPositivityException added