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.

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(TypeAnalysis): remove duplicated brackets from printed solution #26

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

mzacho
Copy link

@mzacho mzacho commented Dec 25, 2022

When performing a type analysis and inspecting the log of the unclosed solution, it seems like the brackets ⟦⟧ for type variables belonging to expressions/ identifiers are duplicated on the left-side of the equation.

Example:

Typechecking the following program foo.tip

main() {
  var p;
  p = alloc null;
  *p = p;
  return 42;
}

with

"args": ["-types", "-verbose", "./examples/foo.tip"]

yields

[info] Processing foo.tip
[verbose] Parsing
[verbose] Declaration analysis
[verbose] Starting TypeAnalysis
[verbose] Visiting AProgram at 1:1
[verbose] Generating constraint ⟦42[5:10]⟧ = int
[verbose] Unifying ⟦42[5:10]⟧ and int
[verbose] Visiting AFunDeclaration at 1:1
[verbose] Generating constraint ⟦main(){...}:1:1⟧ = () -> ⟦42[5:10]⟧
[verbose] Unifying ⟦main(){...}:1:1⟧ and () -> ⟦42[5:10]⟧
[verbose] Visiting AFunBlockStmt at 1:8
[verbose] Visiting AVarStmt at 2:3
[verbose] Visiting AIdentifierDeclaration at 2:7
[verbose] Visiting AAssignStmt at 3:3
[verbose] Generating constraint ⟦p[2:7]⟧ = ⟦alloc null[3:7]⟧
[verbose] Unifying ⟦p[2:7]⟧ and ⟦alloc null[3:7]⟧
[verbose] Visiting AIdentifier at 3:3
[verbose] Visiting AAlloc at 3:7
[verbose] Generating constraint ⟦alloc null[3:7]⟧ = ⭡⟦null[3:13]⟧
[verbose] Unifying ⟦alloc null[3:7]⟧ and ⭡⟦null[3:13]⟧
[verbose] Visiting ANull at 3:13
[verbose] Generating constraint ⟦null[3:13]⟧ = ⭡x1
[verbose] Unifying ⟦null[3:13]⟧ and ⭡x1
[verbose] Visiting AAssignStmt at 4:3
[verbose] Generating constraint ⟦p[2:7]⟧ = ⭡⟦p[2:7]⟧
[verbose] Unifying ⟦p[2:7]⟧ and ⭡⟦p[2:7]⟧
[verbose] Unifying subterms ⟦null[3:13]⟧ and ⟦p[2:7]⟧
[verbose] Unifying ⟦null[3:13]⟧ and ⟦p[2:7]⟧
[verbose] Unifying subterms x1 and ⟦p[2:7]⟧
[verbose] Unifying x1 and ⟦p[2:7]⟧
[verbose] Visiting AIdentifier at 4:4
[verbose] Visiting AIdentifier at 4:8
[verbose] Visiting AReturnStmt at 5:3
[verbose] Visiting ANumber at 5:10
[verbose] Generating constraint ⟦42[5:10]⟧ = int
[verbose] Unifying ⟦42[5:10]⟧ and int
[info] Solution (not yet closed):
  ⟦x1⟧ = ⭡⟦p[2:7]⟧
  ⟦⟦p[2:7]⟧⟧ = ⭡⟦p[2:7]⟧
  ⟦⟦alloc null[3:7]⟧⟧ = ⭡⟦p[2:7]⟧
  ⟦⟦42[5:10]⟧⟧ = int
  ⟦⟦main(){...}:1:1⟧⟧ = () -> ⟦42[5:10]⟧
  ⟦⟦null[3:13]⟧⟧ = ⭡⟦p[2:7]⟧
[info] Inferred types:
  ⟦null[3:13]⟧ = ⭡μx2.⭡x2
  ⟦p[2:7]⟧ = μx2.⭡x2
  ⟦main(){...}:1:1⟧ = () -> int
  ⟦alloc null[3:7]⟧ = ⭡μx2.⭡x2
  ⟦42[5:10]⟧ = int
[info] Results of types analysis of ./examples/foo.tip written to ./out/foo.tip__types.ttip

before the fix and

...
[info] Solution (not yet closed):
  x1 = ⭡⟦p[2:7]⟧
  ⟦p[2:7]⟧ = ⭡⟦p[2:7]⟧
  ⟦alloc null[3:7]⟧ = ⭡⟦p[2:7]⟧
  ⟦42[5:10]⟧ = int
  ⟦main(){...}:1:1⟧ = () -> ⟦42[5:10]⟧
  ⟦null[3:13]⟧ = ⭡⟦p[2:7]⟧
...

after the fix.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant