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

Jump to bottom

Work on inference, unification and subject-reduction #328

Merged
merged 71 commits into from
Apr 10, 2020
Merged

Work on inference, unification and subject-reduction #328

merged 71 commits into from
Apr 10, 2020

Conversation

fblanqui
Copy link
Member

@fblanqui fblanqui commented Apr 2, 2020 •
edited
Loading

fix type inference, unification, handling of implicit arguments in rules, subject-reduction
fix issues #303 #330 #334

gabrielhdt
gabrielhdt reviewed Apr 2, 2020
View reviewed changes
src/core/extra.ml Outdated Show resolved Hide resolved
rlepigre
rlepigre reviewed Apr 2, 2020
View reviewed changes
src/core/terms.ml Outdated Show resolved Hide resolved
@fblanqui
Copy link
Member Author

fblanqui commented Apr 2, 2020

There is a bug I need to fix. I am working on it.

@fblanqui fblanqui mentioned this pull request Apr 2, 2020
Closed
fblanqui added 22 commits April 2, 2020 19:18
@fblanqui
fix typo in comment
a8b9916
@fblanqui
prepare fix
50069df
@fblanqui
fix typos in comments
17a6a50
@fblanqui
fix typo in comment
465215c
@fblanqui
fix typo in comment
9865cc8
@fblanqui
indentation
ce199bc
@fblanqui
comment optim: reserve space for all LHS variables and not only those…
d82b019 
… that are non-linear or appears in the RHS as it may change after SR
@fblanqui
remove subst_from_constrs as it is useless
db583e2
@fblanqui
basics: add fresh_vars
e91ee90
@fblanqui
infer: change in log message
588eddc
@fblanqui
Terms.set_meta: do not erase the type!
d369293
@fblanqui
unif: log instantiations
2706e78
@fblanqui
scope: replace wildcard pattern variables by fresh named pattern vari…
212e1cc 
…ables
@fblanqui
fix sr by replacing LHS metas by fresh function symbols before solvin…
7790644 
…g RHS typing constraints
@fblanqui
details in tests
b2b7d03
@fblanqui
new test
28e84a0
@fblanqui
infer: change in log message
05996f8
@fblanqui
add basics.add_metas
0b8037a
@fblanqui
sr: details
e7b7bc7
@fblanqui
terms: add MetaMap
e285838
@fblanqui
improve sr
e0d283d
@fblanqui
Merge remote-tracking branch 'lp/master' into rhs_metas
05710a7
@fblanqui
Copy link
Member Author

fblanqui commented Apr 9, 2020 •
edited
Loading

I have a question: do we assume somewhere in the code that a meta of arity n has a type of the form \forall x1:A1,..,\forall xn:An,B?

@rlepigre
Copy link
Contributor

rlepigre commented Apr 9, 2020

I have a question: do we assume somewhere in he code that a meta of arity n has a type of the form \forall x1:A1,..,\forall xn:An,B?

I'm not sure, but most probably.

rlepigre
rlepigre previously approved these changes Apr 10, 2020
View reviewed changes
Copy link
Contributor

@rlepigre rlepigre left a comment

Choose a reason for hiding this comment

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

There are still changes in there that I think are a mistake, but I guess I can live with them.

@rlepigre
Copy link
Contributor

So can I merge @fblanqui? (I want to do it myself because I want to fix the commit message.)

rlepigre
rlepigre previously approved these changes Apr 10, 2020
View reviewed changes
@rlepigre rlepigre changed the title fix type inference, unification, handling of implicit arguments in rules, subject-reduction Work on inference, unification and subject-reduction Apr 10, 2020
@fblanqui
Copy link
Member Author

I have a question: do you keep the LHS unchanged after scoping?

@rlepigre
Copy link
Contributor

I have a question: do you keep the LHS unchanged after scoping?

For now yes, but it will have to change once I implement the optimisation.

@fblanqui
Copy link
Member Author

Ok. The optimisation does not change the matching behavior. It is important to not change this indeed. Only the RHS metavariables should be instantiated by something.

@fblanqui
Copy link
Member Author

Thanks to merge @rlepigre . And thanks for your improvements on this PR!

@rlepigre
Copy link
Contributor

Ok. The optimisation does not change the matching behavior. It is important to not change this indeed. Only the RHS metavariables should be instantiated by something.

Yeah, the only thing that the optimisation will do is just not record the term matching a pattern variable in the case where it is not useful in the RHS (and does not appear non-linearly). This means that we will have wildcards again (i.e., terms of the form Patt(None,...,...)) when reducing. For now these do not appear anymore I think. This wastes space since we allocate arrays that are bigger than they need to be.

@rlepigre rlepigre merged commit 1dd8385 into Deducteam:master Apr 10, 2020
@fblanqui fblanqui deleted the rhs_metas branch April 10, 2020 16:03
@fblanqui fblanqui mentioned this pull request Apr 10, 2020
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@gabrielhdt gabrielhdt gabrielhdt left review comments

@rlepigre rlepigre rlepigre approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Bug in rule RHS type inference.
3 participants
@fblanqui @rlepigre @gabrielhdt