add MonadTypedStore

[garrigue]

A monad for OCaml programs

[garrigue]

I have added many more laws, and proved all of them. There are 4 operations:

  cnew : coq_type T -> M (loc T) ;
  cget : loc T -> M (coq_type T) ;
  cput : loc T -> coq_type T -> M unit ;
  cchk : loc T -> M unit ;

The idea is that cchk is a noop that just makes sure that a reference is available in the store. It works like a particle propagating the information at a distance, as it can commute with pretty much everything.

[garrigue]

Is there really no way to check that the laws I prove in monad_model.v are really those from hierarchy.v ? There are many laws, and keeping track of the changes is not so easy.

[garrigue]

This starts to look like something usable. See the examples in example_typed_store.v.

There may be too many laws, but we need more examples to decide. Also, there is probably a better way to rewrite under binders using functional extensionality. Write a more restricted lemma?

[garrigue]

I suppose the closure was an error...

[affeldt-aist]

Is there really no way to check that the laws I prove in monad_model.v are really those from hierarchy.v ? There are many laws, and keeping track of the changes is not so easy.

What about using shared definitions as in https://github.com/affeldt-aist/monae/pull/105/commits/a14f868533a79557669fd247f0d06fe2eb2b56e3 ?

[affeldt-aist]

I suppose the closure was an error...

My bad.

[garrigue]

The approach in https://github.com/affeldt-aist/monae/commit/a14f868533a79557669fd247f0d06fe2eb2b56e3 seems very verbose.

After some efforts, I could eventually redefine a monad by hand in monad_model.ModelTypedStore. There is a major caveat: it requires disabling universe checking in some places, which is inconsistent with automation (everything becomes equal!) Also, this seems to cause a universe inconsistency in altprob_model. Very strange. I should probaly move the code to a separated file to avoid this kind of side-effect.

[garrigue]

I moved TypedStoreModel to a separate file, and replaced it by a weaker version that does not require disabling checks in monad_model.v There is still some problem:

HB.instance Definition _ :=
  isMonadTypedStore.Build M cnewget cnewgetC cnewput cnewputC cputput
    cputget cgetputchk cgetget cgetC cputC cputgetC cnewchk cchknewC
    cchkgetC cchkget cgetchk cchkputC cchkput cputchk cchkC cchkdup
    crunret crunskip crunnew.

still fails with an undocumented error. This is all the stranger as this time I can easily build the required structure manually (using some unnamed mixins...)