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

New redtt core #270

Closed
wants to merge 438 commits into from
Closed

New redtt core #270

wants to merge 438 commits into from

Conversation

jonsterling
Copy link
Collaborator

I'm sketching some ideas for how to formulate the new evaluator in a cleaner and more systematic way, which should also enable some optimizations to avoid unnecessary swapping, etc.

@jonsterling
Copy link
Collaborator Author

Ahh, I think I realized that the idea of naive / syntactic substitution is just wrong in this setting, even if followed by 're-evaluation'.

Consider x = y !!- loop[x] <0/y>; with the naive version, this remains loop[x], and does not become base.

I guess the meaning of substitution really has to be, add the equation to the theory and re-evaluate or something.

@favonia Do you have any clarifying Thoughts here?

@favonia
Copy link
Collaborator

favonia commented Aug 30, 2018

The substitution is done to both the term and the oracle. That's why we have the two-layer oracle to deal with hiding. The semantics in terms of stratified judgments is

dimension variables; equation theory; expression variables |- term : type

so any dimension substitution applies to the rest of the judgment.

In this case, you should have x=0 !!- loop[x] after substitution.

@jonsterling
Copy link
Collaborator Author

@favonia I see, now I think I remember.

@jonsterling
Copy link
Collaborator Author

@favonia Does the following rule make sense? In particular the third premise to calculate the substitution. (I'm checking whether I understood your comment.)

screen shot 2018-08-30 at 11 56 53 am

@favonia
Copy link
Collaborator

favonia commented Aug 30, 2018

Yes, it's okay, except that you should get the value right away from the second premise.

@favonia
Copy link
Collaborator

favonia commented Aug 30, 2018

I now implemented the subst and swap operations directly in #265 to save you some brain power.

@favonia
Copy link
Collaborator

favonia commented Aug 30, 2018

Oops I guess I also need to implement apartness. (It can be simulated by try union r r' h; false with _ -> true but this is so ugly.) Done in #265.

@favonia
Copy link
Collaborator

favonia commented Aug 30, 2018

@favonia Does the following rule make sense? In particular the third premise to calculate the substitution. (I'm checking whether I understood your comment.)

I fixed the rule in the LaTeX note.

@favonia
Copy link
Collaborator

favonia commented Sep 1, 2018

@jonsterling I think equate is a good name. How about me commiting something to #265 so that you can cherry-pick? Also, do you want a pretty printer? If so, is the following format readable?

x~0,y~0,z~#7,w~#6,s~#7,t~#7

The above line means x=y=0 and z=s=t. #6 and #7 have no meaning outside the oracle.

@jonsterling
Copy link
Collaborator Author

@favonia I already brought in the files, so technically there is no need to cherry-pick --- except the git history is not correct, since it does not indicate that you wrote those files. Please feel to make changes directly to this branch, so that we avoid needless merge conflicts.

Also feel free to make any renamings you like :)

@jonsterling
Copy link
Collaborator Author

And the pretty printing format you described sounds good!

@favonia
Copy link
Collaborator

favonia commented Sep 1, 2018

LOL I realized PersistentTable.merge is probably wrong. Actually, it is fine. I misread.

@favonia
Copy link
Collaborator

favonia commented Sep 1, 2018

And the pretty printing format you described sounds good!

Done (modulo bugs).

@favonia
Copy link
Collaborator

favonia commented Sep 1, 2018

I already brought in the files, so technically there is no need to cherry-pick

I think you can cherry-pick a commit out of the history, but oh well it is done now.

mutable parent : (int, cls) T.t}

let emp () =
let size = 100 in
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I might have picked the wrong initial size...

src/core/NewDomain.ml Outdated Show resolved Hide resolved
src/core/NewDomain.ml Outdated Show resolved Hide resolved
@jonsterling jonsterling closed this Jan 7, 2020
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.

2 participants