1. 09 Feb, 2021 1 commit
  2. 04 Jan, 2021 4 commits
  3. 22 Dec, 2020 2 commits
  4. 12 Dec, 2020 1 commit
  5. 07 Dec, 2020 1 commit
  6. 05 Dec, 2020 1 commit
  7. 04 Dec, 2020 1 commit
    • Simon Génier's avatar
      Add opaque values for identifying data constructors. · 1ce7599d
      Simon Génier authored
      This patch add a new primitive type, ##DataconsLabel, which uniquely identifies
      a data constructor within a type. Its inhabitants will be consumed by Low Level
      Typer to write the correct header for objects. The goal is to give an abstract
      type that is as useful on Typer on OCaml where the labels are strings than on a
      future backend which will be better for Low Level Typer and where labels will
      likely be integers.
      
      Values are created through the primitive ##datacons-label<-string and there is
      also a macro datacons-label which allows us to write a symbol directly. I
      choosed to use a right pointing arrow its name, against the Lisp convention. I
      think it makes more sense in languages with an ML syntax because function
      composition is made like this
      
          c<-b . b<-a
      
      and it also goes in the same direction as the b_of_a convention in OCaml. I also
      though it was OK because there where no other primitives with arrows in their
      names so that convention does not clash with others.
      
      Finally, I decided to go against the name ##Discriminent because it suggests it
      only applies to sum types, but ##DataconsLabel is also needed for product types.
      1ce7599d
  8. 03 Dec, 2020 1 commit
  9. 02 Dec, 2020 3 commits
  10. 25 Nov, 2020 1 commit
  11. 05 Nov, 2020 9 commits
  12. 26 Sep, 2020 6 commits
  13. 16 Sep, 2020 4 commits
  14. 14 Sep, 2020 3 commits
  15. 13 Sep, 2020 2 commits
    • Jean-Alexandre Barszcz's avatar
      Make the case elaboration code more consistent · efe2032d
      Jean-Alexandre Barszcz authored
      This commit doesn't substantially change the behavior of the case
      elaboration, but makes the code a bit more consistent and might save
      some unnecessary metavariables in some cases.
      efe2032d
    • Jean-Alexandre Barszcz's avatar
      Make Eq.refl available to the ocaml code · b4d53239
      Jean-Alexandre Barszcz authored
      * src/debruijn.ml : Add a definition of the lexp for Eq.refl
      
      * src/builtin.ml : Register the constant Eq.refl
      
      * btl/builtins.typer (Eq_refl) : Use the builtin variable ##Eq.refl
      instead of registering the builtin with the `Built-in` form. This
      ensures that we have the right variable and type, and might help to
      keep things in sync between the ocaml and typer code.
      b4d53239