Simon Génier pushed to branch datacons-label at Stefan / Typer
Commits: 767a1824 by Simon Génier at 2020-12-03T14:18:51-05:00 Add opaque values for identifying data constructors.
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.
- - - - -
5 changed files:
- btl/builtins.typer - btl/pervasive.typer - src/builtin.ml - src/debruijn.ml - src/eval.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -469,4 +469,9 @@ Test_eq = Built-in "Test.eq"; Test_neq : String -> ?a -> ?a -> IO Bool; Test_neq = Built-in "Test.neq";
+@ Given a string, return an opaque DataconsLabel that identifies a data +@ constructor. +datacons-label<-string : String -> DataconsLabel; +datacons-label<-string = Built-in "datacons-label<-string"; + %%% builtins.typer ends here.
===================================== btl/pervasive.typer ===================================== @@ -687,4 +687,17 @@ in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) (lambda _ -> ret)) );
+datacons-label = macro (lambda args -> + let + label = Sexp_dispatch (List_nth 0 args Sexp_error) + (lambda _ _ -> Sexp_error) + (lambda label-name -> Sexp_string label-name) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + in + IO_return (quote (datacons-label<-string (uquote label))) +) + %%% pervasive.typer ends here.
===================================== src/builtin.ml ===================================== @@ -148,6 +148,7 @@ let register_builtin_csts () = add_builtin_cst "Integer" DB.type_integer; add_builtin_cst "Float" DB.type_float; add_builtin_cst "String" DB.type_string; + add_builtin_cst "DataconsLabel" DB.type_datacons_label; add_builtin_cst "Elab_Context" DB.type_elabctx; add_builtin_cst "Eq" DB.type_eq; add_builtin_cst "Eq.refl" DB.eq_refl
===================================== src/debruijn.ml ===================================== @@ -36,7 +36,7 @@ module Str = Str
open Util
- +open Pexp open Lexp
module M = Myers @@ -95,6 +95,7 @@ let type_int = mkBuiltin ((dloc, "Int"), type0) let type_integer = mkBuiltin ((dloc, "Integer"), type0) let type_float = mkBuiltin ((dloc, "Float"), type0) let type_string = mkBuiltin ((dloc, "String"), type0) +let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in
===================================== src/eval.ml ===================================== @@ -1018,6 +1018,10 @@ let typelevel_lub loc (depth : eval_debug_info) (args_val: value_type list) = | [Vint v1; Vint v2] -> Vint(max v1 v2) | _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2")
+let datacons_label_of_string location depth = function + | [Vstring _ as label] -> label + | _ -> error location "`##datacons-label<-string expects 1 string argument" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -1075,6 +1079,7 @@ let register_builtin_functions () = ("Test.false" , test_false,2); ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3); + ("datacons-label<-string", datacons_label_of_string, 1); ] let _ = register_builtin_functions ()
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/767a1824fe4a8616807c67a191fd9d2bcf...