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

add MonadTypedStore #105

Merged
merged 82 commits into from
Jul 25, 2023
Merged

add MonadTypedStore #105

merged 82 commits into from
Jul 25, 2023

Commits on Jul 24, 2023

  1. add MonadTypedStore

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    c6af4e5 View commit details
    Browse the repository at this point in the history

  2. add axioms for new and get

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    acea7fe View commit details
    Browse the repository at this point in the history

  3. sync with impredicative_set

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    4b12c3f View commit details
    Browse the repository at this point in the history

  4. add cnew and cchk laws

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    7334c27 View commit details
    Browse the repository at this point in the history

  5. more laws

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    9db04d1 View commit details
    Browse the repository at this point in the history

  6. add crun and example_typed_store.v (fact_ref)

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    edde048 View commit details
    Browse the repository at this point in the history

  7. add fibonacci example with two refs

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    1a23435 View commit details
    Browse the repository at this point in the history

  8. adjust laws and finish proofs

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    183f368 View commit details
    Browse the repository at this point in the history

  9. test: cnew_get_def

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    c3725c8 View commit details
    Browse the repository at this point in the history

  10. build model using Unset Universe Checking

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    7163057 View commit details
    Browse the repository at this point in the history

  11. move recursive TypedStoreModel to typed_store_model.v and replace it … 

    …by weaker version in monad_model.v
    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    67afd95 View commit details
    Browse the repository at this point in the history

  12. make definition closer to expected

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    1049c4a View commit details
    Browse the repository at this point in the history

  13. remove hint incompatible disabling universe checking

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    17e836f View commit details
    Browse the repository at this point in the history

  14. use specialized version of funext

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    3d4ad81 View commit details
    Browse the repository at this point in the history

  15. add cchknew to infer reference inequalities

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    2e71b3d View commit details
    Browse the repository at this point in the history

  16. compress

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    bc89acd View commit details
    Browse the repository at this point in the history

  17. add cchknew again...

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    035a394 View commit details
    Browse the repository at this point in the history

  18. small improvements

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    4c2f68b View commit details
    Browse the repository at this point in the history

  19. use eq_bind in example

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    d0eabbb View commit details
    Browse the repository at this point in the history

  20. make loc abstract

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    7942e13 View commit details
    Browse the repository at this point in the history

  21. make cchk a derived operation

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    65d9c2c View commit details
    Browse the repository at this point in the history

  22. wip : for loop example

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    af3ca62 View commit details
    Browse the repository at this point in the history

  23. prove fact_for_ok

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    b686852 View commit details
    Browse the repository at this point in the history

  24. prove equations for forloop

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    844eff0 View commit details
    Browse the repository at this point in the history

  25. simplify and update impredicative_set

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    fb5df79 View commit details
    Browse the repository at this point in the history

  26. change definition forloop63

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    8d91c9b View commit details
    Browse the repository at this point in the history

  27. prove 63-bit version (with many admits)

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    4b2a928 View commit details
    Browse the repository at this point in the history

  28. use forloop630

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    efd60c4 View commit details
    Browse the repository at this point in the history

  29. use conversion names from refproof

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    e398a03 View commit details
    Browse the repository at this point in the history

  30. reorder script for clarity

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    376a3b0 View commit details
    Browse the repository at this point in the history

  31. fix 63-bit proof

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    0e04c6f View commit details
    Browse the repository at this point in the history

  32. down to one admit

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    a91b865 View commit details
    Browse the repository at this point in the history

  33. finish proof of uint2N_sub_succ

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    079ce44 View commit details
    Browse the repository at this point in the history

  34. extract lemmas

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    9beb5e4 View commit details
    Browse the repository at this point in the history

  35. separate int63-related lemmas

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    4a290fd View commit details
    Browse the repository at this point in the history

  36. factorize

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    0817a4f View commit details
    Browse the repository at this point in the history

  37. HB.pack test

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    9cd54ec View commit details
    Browse the repository at this point in the history

  38. fix

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    7339390 View commit details
    Browse the repository at this point in the history

  39. wip

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    e8f1633 View commit details
    Browse the repository at this point in the history

  40. faster actm_bind

    @t6s @affeldt-aist
    t6s authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    45f5e59 View commit details
    Browse the repository at this point in the history

  41. try exception

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    e4df44b View commit details
    Browse the repository at this point in the history

  42. shorten join'_naturality

    @t6s @affeldt-aist
    t6s authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    9600b39 View commit details
    Browse the repository at this point in the history

  43. simplify typed_store_model

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    d55e539 View commit details
    Browse the repository at this point in the history

  44. turn option_monad into an alias

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    acb8c22 View commit details
    Browse the repository at this point in the history

  45. wip

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    a1ef81f View commit details
    Browse the repository at this point in the history

  46. fix

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    22b9a70 View commit details
    Browse the repository at this point in the history

  47. wip

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    df5fe68 View commit details
    Browse the repository at this point in the history

  48. wip

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    24c9096 View commit details
    Browse the repository at this point in the history

  49. wip

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    9cf240a View commit details
    Browse the repository at this point in the history

  50. wip

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    2ea483e View commit details
    Browse the repository at this point in the history

  51. wip

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    d566907 View commit details
    Browse the repository at this point in the history

  52. shorten cnewput

    @t6s @affeldt-aist
    t6s authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    5a825c0 View commit details
    Browse the repository at this point in the history

  53. wip

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    cde55dc View commit details
    Browse the repository at this point in the history

  54. mv

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    3716922 View commit details
    Browse the repository at this point in the history

  55. cputput

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    6e26977 View commit details
    Browse the repository at this point in the history

  56. cgetC

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    eb7fad0 View commit details
    Browse the repository at this point in the history

  57. introduce spec lemmas for nth_error

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    f38ce64 View commit details
    Browse the repository at this point in the history

  58. cnewgetD

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    522cbe9 View commit details
    Browse the repository at this point in the history

  59. generalize bind_cnew' so that bind_cnew is not useful anymore

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    08160fd View commit details
    Browse the repository at this point in the history

  60. implicits

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    d0a6c9a View commit details
    Browse the repository at this point in the history

  61. more implicit

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    85d5b0b View commit details
    Browse the repository at this point in the history

  62. simplify bind_cnew

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    992569b View commit details
    Browse the repository at this point in the history

  63. add axioms allowing cycles in store, and example with cycle

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    556d4bc View commit details
    Browse the repository at this point in the history

  64. dbindA -> ret_uncurry?

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    cc16f23 View commit details
    Browse the repository at this point in the history

  65. check instance of typed_store_model

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    e94438d View commit details
    Browse the repository at this point in the history

  66. typo

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    5be4413 View commit details
    Browse the repository at this point in the history

  67. bindA_uncurry

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    263fecf View commit details
    Browse the repository at this point in the history

  68. build actual model in example_typed_store

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    f3e9f14 View commit details
    Browse the repository at this point in the history

  69. can define outside typed_store_model, but HB.instance still fails

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    a4a1cfe View commit details
    Browse the repository at this point in the history

  70. cgetnewE

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    d92b5df View commit details
    Browse the repository at this point in the history

  71. check examples with both models

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    536b108 View commit details
    Browse the repository at this point in the history

  72. rename MLtypes in a more coherent way

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    96fb1a7 View commit details
    Browse the repository at this point in the history

  73. make loc contents abstract in hierarchy.v

    @garrigue @affeldt-aist
    garrigue authored and affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    c3c900f View commit details
    Browse the repository at this point in the history

  74. cgetputC (wip) + wip (#109)

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    81f9c77 View commit details
    Browse the repository at this point in the history

  75. Typed store monad wip (#111) 

    * cputC (wip)

* refactoring

* factorize coerce, uniformize monad_model/typed_store_model
    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    f913819 View commit details
    Browse the repository at this point in the history

  76. fix

    @affeldt-aist
    affeldt-aist committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    5fd0198 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2023

  1. doc

    @affeldt-aist
    affeldt-aist committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    cdda5da View commit details
    Browse the repository at this point in the history

  2. shared ml_type_eq_mixin

    @garrigue
    garrigue committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    848dbeb View commit details
    Browse the repository at this point in the history

  3. rm do notation

    @affeldt-aist
    affeldt-aist committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    393ab5e View commit details
    Browse the repository at this point in the history

  4. nitpick

    @affeldt-aist
    affeldt-aist committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    5662802 View commit details
    Browse the repository at this point in the history

  5. nitpick

    @affeldt-aist
    affeldt-aist committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    2aa98a9 View commit details
    Browse the repository at this point in the history

  6. improve notations and

    @t6s
    t6s committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    a2cd43e View commit details
    Browse the repository at this point in the history