Simon Génier pushed to branch datacons-label at Stefan / Typer
Commits: 90dfe882 by Simon Génier at 2020-12-04T09:56:09-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.
- - - - -
4 changed files:
- btl/builtins.typer - + btl/heap.typer - src/elab.ml - + src/heap.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -469,4 +469,11 @@ 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/heap.typer ===================================== @@ -0,0 +1,34 @@ +%%% heap --- Manipulate partially initialized objects on the heap + +%% Copyright (C) 2011-2020 Free Software Foundation, Inc. +%% +%% Author: Simon Génier simon.genier@umontreal.ca +%% Keywords: languages, lisp, dependent types. +%% +%% This file is part of Typer. +%% +%% Typer is free software; you can redistribute it and/or modify it under the +%% terms of the GNU General Public License as published by the Free Software +%% Foundation, either version 3 of the License, or (at your option) any +%% later version. +%% +%% Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%% WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%% FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%% more details. +%% +%% You should have received a copy of the GNU General Public License along +%% with this program. If not, see http://www.gnu.org/licenses/. + +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))) +)
===================================== src/elab.ml ===================================== @@ -1871,6 +1871,7 @@ let default_ectx else ctx_define ctx (dloc, Some key) e t) (!BI.lmap) lctx in
+ Heap.register_builtins (); (* read base file *) let lctx = dynamic_bind parsing_internals true (fun ()
===================================== src/heap.ml ===================================== @@ -0,0 +1,40 @@ +(* Copyright (C) 2020 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +open Env +open Lexp +open Pexp + +type location = Util.location + +let error ~(location : location) (message : string) : 'a = + Log.log_fatal ~section:"HEAP" ~loc:location message + +let dloc = Util.dummy_location +let type0 = Debruijn.type0 +let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) + +let datacons_label_of_string location depth = function + | [Vstring _ as label] -> label + | _ -> error ~location "`##datacons-label<-string` expects 1 string argument" + +let register_builtins () = + Builtin.add_builtin_cst "DataconsLabel" type_datacons_label; + Eval.add_builtin_function "datacons-label<-string" datacons_label_of_string 1
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/90dfe88279df30b2820bd9bd66418b38e8...