Simon Génier pushed to branch datacons-label at Stefan / Typer

Commits: efae3f75 by Simon Génier at 2020-12-03T12:38:05-05:00 Add a new primitive: datacons-label.

This patch add a new primitive type, ##DataconsLabel, which uniquely identifies a data constructor within a type. This will be consumed by Low Level Typer to write the header of 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.

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.

- - - - -

4 changed files:

- src/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml

Changes:

===================================== 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,14 @@ 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 datacons_label_of_string = + mkBuiltin ((dloc, "datacons-label<-string"), + mkArrow (Anormal, + (dloc, None), + type_string, + dloc, + type_datacons_label)) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in

===================================== src/elab.ml ===================================== @@ -1416,6 +1416,30 @@ let sform_datacons ctx loc sargs ot = | _ -> sexp_error loc "##constr requires two arguments"; sform_dummy_ret ctx loc

+let datacons_label = + mkBuiltin ((dloc, "##datacons-label'"), + mkArrow (Anormal, + (dloc, None), + DB.type_string, + dloc, + DB.type_datacons_label)) + +let sform_datacons_label + (ctx : elab_context) + (loc : location) + (sargs : sexp list) + (_ : ltype option) + : lexp * sform_type = + + match sargs with + | [Symbol (symbol_location, symbol_name)] + -> let symbol = mkImm (String (symbol_location, symbol_name)) in + let e = mkCall (DB.datacons_label_of_string, [Anormal, symbol]) in + e, Lazy + | _ + -> sexp_error loc "##datacons-label must have a single symbolic argument"; + sform_dummy_ret ctx loc + let elab_colon_to_ak k = match k with | "_:::_" -> Aerasable | "_::_" -> Aimplicit @@ -1810,27 +1834,28 @@ let sform_load usr_elctx loc sargs ot = let register_special_forms () = List.iter add_special_form [ - ("Built-in", sform_built_in); - ("DeBruijn", sform_debruijn); + ("Built-in", sform_built_in); + ("DeBruijn", sform_debruijn); ("typer-identifier", sform_identifier); - ("typer-immediate", sform_immediate); - ("datacons", sform_datacons); - ("typecons", sform_typecons); - ("_:_", sform_hastype); - ("lambda_->_", sform_lambda Anormal); - ("lambda_=>_", sform_lambda Aimplicit); - ("lambda_≡>_", sform_lambda Aerasable); - ("_->_", sform_arrow Anormal); - ("_=>_", sform_arrow Aimplicit); - ("_≡>_", sform_arrow Aerasable); - ("case_", sform_case); - ("let_in_", sform_letin); - ("Type_", sform_type); - ("load", sform_load); + ("typer-immediate", sform_immediate); + ("datacons", sform_datacons); + ("datacons-label", sform_datacons_label); + ("typecons", sform_typecons); + ("_:_", sform_hastype); + ("lambda_->_", sform_lambda Anormal); + ("lambda_=>_", sform_lambda Aimplicit); + ("lambda_≡>_", sform_lambda Aerasable); + ("_->_", sform_arrow Anormal); + ("_=>_", sform_arrow Aimplicit); + ("_≡>_", sform_arrow Aerasable); + ("case_", sform_case); + ("let_in_", sform_letin); + ("Type_", sform_type); + ("load", sform_load); (* FIXME: We should add here `let_in_`, `case_`, etc... *) (* FIXME: These should be functions! *) - ("decltype", sform_decltype); - ("declexpr", sform_declexpr); + ("decltype", sform_decltype); + ("declexpr", sform_declexpr); ]

(* Default context with builtin types

===================================== 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/efae3f75561f9b0af693287dc37b397980...