Simon Génier pushed to branch heap at Stefan / Typer
Commits: d74651cf by Simon Génier at 2020-11-25T10:59:52-05:00 Get rid of attributes on builtin.
- - - - - f73bc318 by Simon Génier at 2020-12-01T23:35:45-05:00 Merge branch 'remove-attributes' into HEAD
- - - - - c0df7b8b by Simon Génier at 2020-12-02T11:36:56-05:00 Cosmetic changes to utest_main.ml.
Some of these changes bring the style more in line with the GNU coding standard that is used for Typer. - Reindent file to 2 spaces. - Break lines before a operator. - Break lines before 80 columns.
Others are my attempts to improve readability. - Use functions specialized on refs in Arg. - Remove superfluous parenthesis. - Extract large fun expressions to local let bindings.
- - - - - 077b4494 by Simon Génier at 2020-12-02T12:05:43-05:00 Utest_main now also handle Windows paths.
- - - - - a4cc1ea7 by Simon Génier at 2020-12-03T12:13:32-05:00 Merge branch 'utests-main-windows'
- - - - - 1ce7599d by Simon Génier at 2020-12-04T09:56:45-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.
- - - - - 5a31e992 by Simon Génier at 2020-12-05T14:46:49-05:00 Merge branch 'datacons-label'
- - - - - b0050e45 by Simon Génier at 2020-12-05T16:52:07-05:00 Add primitives for separate allocation and initialization.
- - - - -
12 changed files:
- btl/builtins.typer - + btl/heap.typer - + samples/heap.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - + src/heap.ml - src/lexp.ml - src/opslexp.ml - src/option.ml - tests/utest_main.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -469,4 +469,29 @@ 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"; + +Heap_unsafe-alloc : Int -> ##Heap Int; +Heap_unsafe-alloc = Built-in "Heap.alloc"; + +Heap_unsafe-free : Int -> ##Heap Unit; +Heap_unsafe-free = Built-in "Heap.free"; + +Heap_unsafe-export : Int -> ##Heap ?t; +Heap_unsafe-export = Built-in "Heap.export"; + +Heap_unsafe_store_header : Int -> ##DataconsLabel -> ##Heap Unit; +Heap_unsafe_store_header = Built-in "Heap.store-header"; + +Heap_unsafe-store-cell : Int -> Int -> ?t -> ##Heap Unit; +Heap_unsafe-store-cell = Built-in "Heap.store-cell"; + +Heap_unsafe-load-cell : Int -> Int -> ##Heap ?t; +Heap_unsafe-load-cell = Built-in "Heap.load-cell"; + %%% 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))) +)
===================================== samples/heap.typer =====================================
===================================== src/builtin.ml ===================================== @@ -134,7 +134,7 @@ let add_builtin_cst (name : string) (e : lexp) lmap := SMap.add name (e, t) map
let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind, None) in + let t = mkBuiltin ((dloc, name), kind) in add_builtin_cst name t; t
@@ -153,16 +153,14 @@ let register_builtin_csts () = add_builtin_cst "Eq.refl" DB.eq_refl
let register_builtin_types () = + let type_arrow_0 = + mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) + in let _ = new_builtin_type "Sexp" DB.type0 in - let _ = new_builtin_type - "IO" (mkArrow (Anormal, (dloc, None), - DB.type0, dloc, DB.type0)) in - let _ = new_builtin_type - "Ref" (mkArrow (Anormal, (dloc, None), - DB.type0, dloc, DB.type0)) in - let _ = new_builtin_type - "Array" (mkArrow (Anormal, (dloc, None), - DB.type0, dloc, DB.type0)) in + let _ = new_builtin_type "IO" type_arrow_0 in + let _ = new_builtin_type "Heap" type_arrow_0 in + let _ = new_builtin_type "Ref" type_arrow_0 in + let _ = new_builtin_type "Array" type_arrow_0 in let _ = new_builtin_type "FileHandle" DB.type0 in ()
===================================== src/debruijn.ml ===================================== @@ -84,18 +84,18 @@ let fatal = Log.log_fatal ~section:"DEBRUIJN" let dloc = dummy_location let type_level_sort = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort, None) +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) -let type_int = mkBuiltin ((dloc, "Int"), type0, None) -let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) -let type_float = mkBuiltin ((dloc, "Float"), type0, None) -let type_string = mkBuiltin ((dloc, "String"), type0, None) -let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None) +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_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -108,7 +108,7 @@ let type_eq_type = mkArrow (Anormal, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (mkVar (lv, 3))))))) -let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type, None) +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let eq_refl = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -124,8 +124,7 @@ let eq_refl = [Aerasable, mkVar (lv, 2); Aerasable, mkVar (tv, 1); Anormal, mkVar (xv, 0); - Anormal, mkVar (xv, 0)])))), - None) + Anormal, mkVar (xv, 0)])))))
(* easier to debug with type annotations *)
===================================== src/elab.ml ===================================== @@ -106,7 +106,7 @@ let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0
let add_special_form (name, func) = - BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form, None)); + BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); special_forms := SMap.add name func (!special_forms)
let get_special_form name = @@ -584,7 +584,7 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype = and elab_special_form ctx f args ot = let loc = lexp_location f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with - | Builtin ((_, name), _, _) -> + | Builtin ((_, name), _) -> (* Special form. *) (get_special_form name) ctx loc args ot
@@ -593,40 +593,11 @@ and elab_special_form ctx f args ot =
(* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc oname t = - (* lookup default attribute of t. *) - (* FIXME: Don't lookup defaults/tactics here. Instead, just always - * generate a metavar at this point. The use of defaults/tactics should be - * postponed, probably to just before we do HM-style generalization. *) - match - try (* FIXME: We shouldn't hard code as popular a name as `default`. *) - let pidx, pname = (senv_lookup "default" ctx), "default" in - let default = mkVar ((dloc, Some pname), pidx) in - get_attribute ctx loc [default; t] - with e -> None with - | Some attr - -> (* FIXME: The `default` attribute table shouldn't contain elements of - * type `Macro` but elements of type `something -> Sexp`. - * The point of the `Macro` type is to be able to distinguish - * a macro call from a function call, but here, we have no need - * to distinguish two cases. - * Better yet: let's not do any table lookup here. Instead, - * call a `default-arg-filler` function, implemented in Typer, - * just like `Macro_expand` function. That one can then look - * things up in a table and/or do anything else it wants. *) - let v = lexp_expand_macro loc attr [] ctx (Some t) in - - (* get the sexp returned by the macro *) - let lsarg = match v with - | Vcommand cmd - -> (match cmd () with - | Vsexp (sexp) -> sexp - | _ -> value_fatal loc v "default attribute should return a IO Sexp" ) - | _ -> value_fatal loc v "default attribute should return an IO" in - - (* Elaborate the argument *) - check lsarg t ctx - | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (loc, oname) t + newMetavar + (ectx_to_lctx ctx) + (ectx_to_scope_level ctx) + (loc, oname) + t
(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = @@ -1388,92 +1359,23 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = * Special forms implementation * -------------------------------------------------------------------------- *)
-and sform_new_attribute ctx loc sargs ot = - match sargs with - | [t] -> let ltp = infer_type t ctx (loc, None) in - (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` - * is False, for example): Should be a type like `AttributeMap t` - * instead. *) - (mkBuiltin ((loc, "new-attribute"), - L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp), - Some AttributeMap.empty), - Lazy) - | _ -> fatal ~loc "new-attribute expects a single Type argument" - -and sform_add_attribute ctx loc (sargs : sexp list) ot = - let n = get_size ctx in - let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with - | [table; e; attr] when is_var e - -> table, (n - (get_var_db_index (get_var e)), U.get_vname_name (get_var_vname (get_var e))), attr - | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in - - let map, attr_type = - match OL.lexp'_whnf table (ectx_to_lctx ctx) with - | Builtin (_, attr_type, Some map) -> map, attr_type - | _ -> fatal ~loc "add-attribute expects a table as first argument" in - - (* FIXME: Type check (attr: type == attr_type) *) - let attr' = L.clean (OL.lexp_close (ectx_to_lctx ctx) attr) in - let table = AttributeMap.add var attr' map in - (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), - Lazy) - - - and get_attribute ctx loc largs = - let ctx_n = get_size ctx in - let table, var = match largs with - | [table; e] when is_var e - -> table, (ctx_n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in - - - let map = - match OL.lexp'_whnf table (ectx_to_lctx ctx) with - | Builtin (_, attr_type, Some map) -> map - | _ -> fatal ~loc "get-attribute expects a table as first argument" in - - try Some (AttributeMap.find var map) - with Not_found -> None - -and sform_get_attribute ctx loc (sargs : sexp list) ot = - match get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) with - | Some e -> (e, Lazy) - | None -> sexp_error loc "No attribute found"; sform_dummy_ret ctx loc - -and sform_has_attribute ctx loc (sargs : sexp list) ot = - let n = get_size ctx in - let table, var = match List.map (lexp_parse_sexp ctx) sargs with - | [table; e] when is_var e - -> table, (n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in - - - let map, attr_type = - let lp = OL.lexp_whnf table (ectx_to_lctx ctx) in - match lexp_lexp' lp with - | Builtin (_, attr_type, Some map) -> map, attr_type - | lxp -> lexp_fatal loc table - "get-attribute expects a table as first argument" in - - (BI.o2l_bool ctx (AttributeMap.mem var map), Lazy) - - and sform_declexpr ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [e] when is_var e - -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with - | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; +and sform_declexpr ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with + | Some lxp -> (lxp, Lazy) + | None -> error ~loc "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; - sform_dummy_ret ctx loc + | _ -> error ~loc "declexpr expects one argument"; + sform_dummy_ret ctx loc
- let sform_decltype ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [e] when is_var e - -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc "decltype expects one argument"; - sform_dummy_ret ctx loc +let sform_decltype ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) + | _ -> error ~loc "decltype expects one argument"; + sform_dummy_ret ctx loc
@@ -1489,7 +1391,7 @@ let sform_built_in ctx loc sargs ot = * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp', None) in + let bi = mkBuiltin ((loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; @@ -1926,10 +1828,6 @@ let register_special_forms () = ("Type_", sform_type); ("load", sform_load); (* FIXME: We should add here `let_in_`, `case_`, etc... *) - ("get-attribute", sform_get_attribute); - ("new-attribute", sform_new_attribute); - ("has-attribute", sform_has_attribute); - ("add-attribute", sform_add_attribute); (* FIXME: These should be functions! *) ("decltype", sform_decltype); ("declexpr", sform_declexpr); @@ -1973,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/eval.ml ===================================== @@ -56,13 +56,195 @@ let global_eval_trace = ref ([], []) let global_eval_ctx = ref make_runtime_ctx (* let eval_max_recursion_depth = ref 23000 *)
-let builtin_functions - = ref (SMap.empty : ((location -> eval_debug_info - -> value_type list -> value_type) - (* The primitive's arity. *) - * int) SMap.t) +(* eval error are always fatal *) +let error loc ?print_action msg = + Log.log_error ~section:"EVAL" ~loc:loc ?print_action msg; + Log.internal_error msg + +type builtin_function = + location -> eval_debug_info -> value_type list -> value_type + +module type CallInfo = sig + val name : string + module Ty : sig + val arity : int + end +end + +let wrong_number_of_arguments ~location (module Ci : CallInfo) actual = + let message = + "`" + ^ Ci.name + ^ "` expects " + ^ string_of_int Ci.Ty.arity + ^ " arguments, but got " + ^ string_of_int actual + in + error location message + +let dynamic_type_error ~location (module Ci : CallInfo) index expected actual = + let index_name = match index with + | 0 -> "first" + | 1 -> "second" + | 2 -> "third" + | _ -> string_of_int (index + 1) ^ "th" + in + let message = + "`" + ^ Ci.name + ^ "` expects a " + ^ expected + ^ " as it's " + ^ index_name + ^ " argument, but got " + ^ value_string actual + in + error location message + +(** A type that can be used as a built-in. It is a weaker contract than [Ty] + because while [Ty] can be returned by a built-in, a [BuiltinTy] can only + appear in the unevaluted form of a built-in and must dissapear when the + evaluation is done. *) +module type BuiltinTy = sig + type ocaml_ty + + val name : string + + val arity : int + + val invoke + : location + -> (module CallInfo) + -> int + -> ocaml_ty + -> value_type list + -> value_type +end + +(** A type that can be exported to and imported from Typer. *) +module type Ty = sig + include BuiltinTy + + val export : location -> ocaml_ty -> value_type + + val import : location -> value_type -> ocaml_ty option +end + +module ArrowTy (Domain : Ty) (Codomain : BuiltinTy) = struct + type ocaml_ty = Domain.ocaml_ty -> Codomain.ocaml_ty + + let name = "(" ^ Domain.name ^ " -> " ^ Codomain.name ^ ")" + + let arity = 1 + Codomain.arity + + let invoke location (module Ci : CallInfo) n f = function + | a_head :: a_tail + -> (match Domain.import location a_head with + | Some a + -> Codomain.invoke location (module Ci) (n + 1) (f a) a_tail + | None + -> dynamic_type_error ~location (module Ci) n Domain.name a_head) + | _ -> wrong_number_of_arguments ~location (module Ci) n +end + +let invoke_last export location (module Ci : CallInfo) n value = function + | [] -> export location value + | vs -> wrong_number_of_arguments ~location (module Ci) (n + List.length vs) + +module CommandTy + (Inner : Ty) + : Ty with type ocaml_ty = unit -> Inner.ocaml_ty + = struct + + type ocaml_ty = unit -> Inner.ocaml_ty + + let name = "command of " ^ Inner.name + + let arity = 0 + + let export location command = + Vcommand (fun () -> Inner.export location (command ())) + + let import location = function + | Vcommand command -> + (* TODO: better error message. *) + Some (fun () -> Option.get (Inner.import location (command ()))) + | _ -> None + + let invoke = invoke_last export +end + +module IntTy : Ty with type ocaml_ty = int = struct + type ocaml_ty = int + + let name = "int" + + let arity = 0 + + let export _ i = Vint i + + let import _ = function + | Vint i -> Some i + | _ -> None + + let invoke = invoke_last export +end
-let add_builtin_function name f arity = +module StringTy : Ty with type ocaml_ty = string = struct + type ocaml_ty = string + + let name = "string" + + let arity = 0 + + let export _ s = Vstring s + + let import _ = function + | Vstring s -> Some s + | _ -> None + + let invoke = invoke_last export +end + +module UnitTy : Ty with type ocaml_ty = unit = struct + type ocaml_ty = unit + + let name = "()" + + let arity = 0 + + (* TODO: find a way to return the real unit. *) + let export _ i = Vint 0 + + let import _ _ = Some () + + let invoke = invoke_last export +end + +module ValueTy : Ty with type ocaml_ty = value_type = struct + type ocaml_ty = value_type + + let name = "value" + + let arity = 0 + + let export _ value = value + + let import _ value = Some value + + let invoke = invoke_last export +end + +module type Builtin = sig + val name : string + module Ty : BuiltinTy + val impl : location -> Ty.ocaml_ty +end + +(** A map of the function name to its implementation and arity. *) +let builtin_functions : (builtin_function * int) SMap.t ref = ref SMap.empty + +let add_builtin_function name (f : builtin_function) arity = builtin_functions := SMap.add name (f, arity) (!builtin_functions)
let append_eval_trace trace (expr : elexp) = @@ -81,11 +263,6 @@ let rec_depth trace = let (a, b) = trace in List.length b
-(* eval error are always fatal *) -let error loc ?print_action msg = - Log.log_error ~section:"EVAL" ~loc ?print_action msg; - Log.internal_error msg - let fatal loc msg = Log.log_fatal ~section:"EVAL" ~loc msg let warning loc msg = Log.log_warning ~section:"EVAL" ~loc msg
@@ -1018,6 +1195,12 @@ 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 register_builtin (module B : Builtin) = + let run location _ = + B.Ty.invoke location (module B : CallInfo) 0 (B.impl location) + in + builtin_functions := SMap.add B.name (run, B.Ty.arity) !builtin_functions + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [
===================================== src/heap.ml ===================================== @@ -0,0 +1,150 @@ +(* 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/. *) + +(** A heap of Typer objects that can be partially initialized. *) + +open Env +open Eval +open Lexp + +module IMap = Util.IMap + +type location = Util.location +type symbol = Sexp.symbol +type value = Env.value_type + +type size = int +type addr = int + +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 next_free_address : addr ref = ref 1 + +type t = (symbol option ref * value option array) IMap.t ref + +let heap : t = ref IMap.empty + +let alloc (cells_count : size) : addr = + let address = !next_free_address in + next_free_address := address + 1; + heap := IMap.add address (ref None, Array.make cells_count None) !heap; + address + +let free (address : addr) : unit = + heap := IMap.remove address !heap + +(** If address points to a fully initialized object, returns it. *) +let export (address : addr) : value = + let rec export_cells cells n acc = + if n == 0 + then acc + else + let n = n - 1 in + export_cells cells n (Option.get cells.(n) :: acc) + in + let constructor, cells = IMap.find address !heap in + Env.Vcons (Option.get !constructor, export_cells cells (Array.length cells) []) + +(** Initializes the header of the object so it is valid for the given data + constructor. *) +let store_header + (location : location) + (address : addr) + (datacons : value) + : unit = + + match datacons with + | Env.Vcons (symbol, []) + -> let constructor, _ = IMap.find address !heap in + constructor := Some symbol + | _ -> error ~location ("not a data constructor: " ^ Env.value_string datacons) + +(** If [address] points to an object of at least [cell_index + 1] cells, mutates + the value at that index. *) +let store_cell (address : addr) (cell_index : int) (value : value) : unit = + let _, cells = IMap.find address !heap in + cells.(cell_index) <- Some value + +(** If [address] points to an object of at least [cell_index + 1] cells and the + cell at [cell_index] is initialized, returns the value at that index. *) +let load_cell (address : addr) (cell_index : int) : value = + let _, cells = IMap.find address !heap in + Option.get cells.(cell_index) + +module DataconsLabelOfString = struct + let name = "datacons-label<-string" + module Ty = ArrowTy (StringTy) (StringTy) + let impl _ name = name +end + +module HeapAlloc = struct + let name = "Heap.alloc" + module Ty = ArrowTy (IntTy) (CommandTy (IntTy)) + let impl location size () = alloc size +end + +module HeapFree = struct + let name = "Heap.free" + module Ty = ArrowTy (IntTy) (CommandTy (UnitTy)) + let impl _ address () = free address +end + +module HeapExport = struct + let name = "Heap.export" + module Ty = ArrowTy (IntTy) (CommandTy (ValueTy)) + let impl _ address () = export address +end + +module HeapStoreHeader = struct + let name = "Heap.store-header" + module Ty = ArrowTy (IntTy) (ArrowTy (ValueTy) (CommandTy (UnitTy))) + let impl location address datacons () = store_header location address datacons +end + +module HeapStoreCell = struct + let name = "Heap.store-cell" + module Ty = + ArrowTy (IntTy) + (ArrowTy (IntTy) + (ArrowTy (ValueTy) + (CommandTy (UnitTy)))) + let impl _ address cell_index value () = store_cell address cell_index value +end + +module HeapLoadCell = struct + let name = "Heap.load-cell" + module Ty = ArrowTy (IntTy) (ArrowTy (IntTy) (CommandTy (ValueTy))) + let impl _ address cell_index () = load_cell address cell_index +end + +let register_builtins () = + Builtin.add_builtin_cst "DataconsLabel" type_datacons_label; + Eval.register_builtin (module DataconsLabelOfString); + Eval.register_builtin (module HeapAlloc); + Eval.register_builtin (module HeapFree); + Eval.register_builtin (module HeapExport); + Eval.register_builtin (module HeapStoreHeader); + Eval.register_builtin (module HeapStoreCell); + Eval.register_builtin (module HeapLoadCell)
===================================== src/lexp.ml ===================================== @@ -40,9 +40,6 @@ type meta_id = int (* Identifier of a meta variable. *)
type label = symbol
-type attribute_key = (int * string) (* rev_dbi * Var name *) -module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) - (*************** Elaboration to Lexp *********************)
(* The scoping of `Let` is tricky: @@ -66,7 +63,7 @@ type ltype = lexp | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort - | Builtin of symbol * ltype * lexp AttributeMap.t option + | Builtin of symbol * ltype | Var of vref | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) @@ -196,12 +193,8 @@ let lexp'_hash (lp : lexp') = | Stype lp -> lexp_hash lp | StypeOmega -> Hashtbl.hash s | StypeLevel -> Hashtbl.hash s)) - | Builtin (v, t, m) - -> U.combine_hash 4 (U.combine_hash - (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) - (match m with - | Some m -> Hashtbl.hash m - | None -> 404)) + | Builtin (v, t) + -> U.combine_hash 4 (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) | Var v -> U.combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) @@ -264,7 +257,7 @@ let hc_eq e1 e2 = | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 - | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 | (Susp (e1, s1), Susp (e2, s2)) -> e1 == e2 && compare s1 s2 = 0 | (Let (_, defs1, e1), Let (_, defs2, e2)) @@ -310,7 +303,7 @@ let hc (l : lexp') : lexp = let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t, m) = hc (Builtin (v, t, m)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) let mkLet (l, ds, e) = hc (Let (l, ds, e)) let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) @@ -329,18 +322,18 @@ let impossible = mkImm Sexp.dummy_epsilon
let lexp_head e = match lexp_lexp' e with - | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s - | Var _ -> "Var" - | Let _ -> "let" - | Arrow _ -> "Arrow" - | Lambda _ -> "lambda" - | Call _ -> "Call" - | Cons _ -> "datacons" - | Case _ -> "case" + | Imm s -> + if e = impossible then "impossible" else "Imm" ^ sexp_string s + | Var _ -> "Var" + | Let _ -> "let" + | Arrow _ -> "Arrow" + | Lambda _ -> "lambda" + | Call _ -> "Call" + | Cons _ -> "datacons" + | Case _ -> "case" | Inductive _ -> "typecons" | Susp _ -> "Susp" - | Builtin (_, _, None) -> "Builtin" - | Builtin _ -> "AttributeTable" + | Builtin _ -> "Builtin" | Metavar _ -> "Metavar" | Sort _ -> "Sort" | SortLevel _ -> "SortLevel" @@ -512,7 +505,7 @@ let rec lexp_location e = | SortLevel SLz -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l - | Builtin ((l, _), _, _) -> l + | Builtin ((l, _), _) -> l | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l | Lambda (_,(l,_),_,_) -> l @@ -667,7 +660,7 @@ let rec lexp_unparse lxp = match lexp_lexp' lxp with | Susp _ -> lexp_unparse (nosusp lxp) | Imm (sexp) -> sexp - | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) + | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (loc, maybename name) | Cons (t, (l, name)) @@ -893,7 +886,7 @@ let rec get_precedence expr ctx = | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" | Call (exp, _) -> get_precedence exp ctx - | Builtin ((_, name), _, _) when is_binary_op name -> + | Builtin ((_, name), _) when is_binary_op name -> lkp (get_binary_op_name name) | Var ((_, Some name), _) when is_binary_op name -> lkp (get_binary_op_name name) @@ -955,11 +948,11 @@ and lexp_str ctx (exp : lexp) : string =
let get_name fname = match lexp_lexp' fname with - | Builtin ((_, name), _, _) -> name, 0 - | Var((_, Some name), idx) -> name, idx - | Lambda _ -> "__", 0 - | Cons _ -> "__", 0 - | _ -> "__", -1 in + | Builtin ((_, name), _) -> name, 0 + | Var((_, Some name), idx) -> name, idx + | Lambda _ -> "__", 0 + | Cons _ -> "__", 0 + | _ -> "__", -1 in
match lexp_lexp' exp with | Imm(value) -> (match value with @@ -1070,7 +1063,7 @@ and lexp_str ctx (exp : lexp) : string = | (_, Some name) -> name) ^ " => " ^ (lexp_stri 1 df))
- | Builtin ((_, name), _, _) -> "##" ^ name + | Builtin ((_, name), _) -> "##" ^ name
| Sort (_, StypeLevel) -> "##TypeLevel.Sort" | Sort (_, StypeOmega) -> "##Type_ω" @@ -1131,7 +1124,7 @@ let rec eq e1 e2 = | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2 - | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 | (Susp (e1, s1), _) -> eq (push_susp e1 s1) e2 | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2)
===================================== src/opslexp.ml ===================================== @@ -182,7 +182,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = args)) ctx | Call (f', xs1) -> mkCall (f', List.append xs1 xs) - | Builtin ((_, name), _, _) + | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> U.option_default e (f ctx args) | None -> e) @@ -342,7 +342,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = || (match (s1, s2) with | (Stype e1, Stype e2) -> conv_p e1 e2 | _ -> false) - | (Builtin ((_, s1), _, _), Builtin ((_, s2), _, _)) -> s1 = s2 + | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 | (Var (_, v1), Var (_, v2)) -> v1 = v2 | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, vd2, t21, _, t22)) -> ak1 == ak2 @@ -620,9 +620,8 @@ and check'' erased ctx e = -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) - | Builtin (_, t, _) + | Builtin (_, t) -> let _ = check_type DB.set_empty Myers.nil t in - (* FIXME: Check the attributemap as well! *) t (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) @@ -990,7 +989,7 @@ and get_type ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int - | Builtin (_, t, _) -> t + | Builtin (_, t) -> t | SortLevel _ -> DB.type_level | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega @@ -1101,10 +1100,10 @@ let erasure_dummy = DB.type0
let rec erase_type (lxp: lexp): E.elexp = match lexp_lexp' lxp with - | L.Imm(s) -> E.Imm(s) - | L.Builtin(v, _, _) -> E.Builtin(v) - | L.Var(v) -> E.Var(v) - | L.Cons(_, s) -> E.Cons(s) + | L.Imm(s) -> E.Imm(s) + | L.Builtin(v, _) -> E.Builtin(v) + | L.Var(v) -> E.Var(v) + | L.Cons(_, s) -> E.Cons(s) | L.Lambda (P.Aerasable, _, _, body) -> erase_type (L.push_susp body (S.substitute erasure_dummy)) | L.Lambda (_, vdef, _, body) ->
===================================== src/option.ml ===================================== @@ -25,3 +25,8 @@ let equal (inner_equal : 'a -> 'a -> bool) (l : 'a t) (r : 'a t) : bool = | Some l, Some r -> inner_equal l r | None, None -> true | _ -> false + +let get (o : 'a option) : 'a = + match o with + | Some v -> v + | None -> invalid_arg "expected Some"
===================================== tests/utest_main.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -30,32 +30,34 @@ * * --------------------------------------------------------------------------- *)
-open Fmt +(** Search *_test.byte executable and run them. + Usage: + ./utest_main tests_folder root_folder *)
-let cut_name str = - String.sub str 0 (String.length str - 12) +open Fmt
let global_verbose_lvl = ref 5 -let global_sample_dir = ref "./" -let global_tests_dir = ref "./_build/tests/" +let global_sample_dir = ref "." +let global_tests_dir = ref (Filename.concat "_build" "tests") let global_fsection = ref "" let global_ftitle = ref "" let global_filter = ref false
-let arg_defs = [ +let arg_defs = + [ ("--verbose", - Arg.Int (fun g -> global_verbose_lvl := g), " Set verbose level"); + Arg.Set_int global_verbose_lvl, " Set verbose level"); ("--samples", - Arg.String (fun g -> global_sample_dir := g), " Set sample directory"); + Arg.Set_string global_sample_dir, " Set sample directory"); ("--tests", - Arg.String (fun g -> global_tests_dir := g), " Set tests directory"); + Arg.Set_string global_tests_dir, " Set tests directory"); (* Allow users to select which test to run *) ("--fsection", Arg.String (fun g -> global_fsection := String.uppercase_ascii g; - global_filter := true), " Set test filter"); + global_filter := true), " Set test filter"); ("--ftitle", Arg.String (fun g -> global_ftitle := String.uppercase_ascii g; - global_filter := true), " Set test filter"); + global_filter := true), " Set test filter"); ]
@@ -69,99 +71,114 @@ let cut_byte str = String.sub str 0 ((String.length str) - 10) let cut_native str = String.sub str 0 ((String.length str) - 12)
let cut_name str = - if (Filename.check_suffix str "_test.byte") - then (cut_byte str) - else (cut_native str) + if Filename.check_suffix str "_test.byte" + then cut_byte str + else cut_native str
let print_file_name i n name pass = - let line_size = 80 - (String.length (cut_name name)) - 16 in - let name = cut_name name in - - (if pass then print_string green else print_string red); - print_string " ("; - ralign_print_int i 2; print_string "/"; - ralign_print_int n 2; print_string ") "; - print_string name; - print_string (make_line '.' line_size); - if pass then print_string "..OK\n" else print_string "FAIL\n"; - print_string reset + let line_size = 80 - (String.length (cut_name name)) - 16 in + let name = cut_name name in + + (if pass then print_string green else print_string red); + print_string " ("; + ralign_print_int i 2; print_string "/"; + ralign_print_int n 2; print_string ") "; + print_string name; + print_string (make_line '.' line_size); + if pass then print_string "..OK\n" else print_string "FAIL\n"; + print_string reset
let must_run str = - not (!global_filter) + not !global_filter || String.uppercase_ascii (cut_name str) = !global_fsection
-(* search *_test.byte executable en run them - Usage: - ./utest_main tests_folder root_folder *) let main () = - parse_args (); - - print_string "\n"; - calign_print_string " Running Unit Test " 80; - print_string "\n\n"; - - (*print_string ("[ ] Test folder: " ^ folder ^ "\n"); *) - - (* get tests files *) - let folder = !global_tests_dir in - let root_folder = !global_sample_dir in - - let files = try Sys.readdir folder - with e ->( - print_string ("The folder: " ^ (! global_tests_dir) ^ " does not exist.\n" ^ - "Have you tried "./utests --tests= ./tests" ?\n"); - raise e; - ) in - - let check name = - if (Filename.check_suffix name "_test.byte") || - (Filename.check_suffix name "_test.native") then true else false in - - (* select files that are executable tests *) - let files = Array.fold_left - (fun acc elem -> if check elem then elem::acc else acc) - [] files in - - let files_n = List.length files in - - (if files_n = 0 then ( - print_string "No tests were found. Did you compiled them? \n")); - - let exit_code = ref 0 in - let failed_test = ref 0 in - let tests_n = ref 0 in - let test_args = - ["--samples"; root_folder; - "--verbose"; (string_of_int !global_verbose_lvl)] @ - (if not (!global_ftitle = "") then - ["--ftitle"; !global_ftitle] else []) in - - List.iter (fun file -> - flush stdout; - - if must_run file then ( - tests_n := !tests_n + 1; - let command = String.concat " " (List.map Filename.quote - ((folder ^ file)::test_args)) in - exit_code := Sys.command command; - - (if !exit_code != 0 then( - (if verbose 1 then print_file_name (!tests_n) files_n file false); - failed_test := !failed_test + 1) - else - (if verbose 1 then print_file_name (!tests_n) files_n file true); - ); - - (if verbose 2 then print_newline ()); - - ); - - ) files; - - print_string "\n\n"; - print_string " Test Ran : "; print_int !tests_n; - print_string "\n Test Failed : "; print_int !failed_test; - print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); - print_endline "\n" + parse_args (); + + print_string "\n"; + calign_print_string " Running Unit Test " 80; + print_string "\n\n"; + + (*print_string ("[ ] Test folder: " ^ folder ^ "\n"); *) + + (* get tests files *) + let folder = !global_tests_dir in + let root_folder = !global_sample_dir in + + let files = + try Sys.readdir folder + with + | e + -> (print_string ("The folder: " ^ !global_tests_dir + ^ " does not exist.\n" + ^ "Have you tried "./utests --tests= ./tests" ?\n"); + raise e) + in + + let check name = + Filename.check_suffix name "_test.byte" + || Filename.check_suffix name "_test.native" + in + + (* select files that are executable tests *) + let files = Array.fold_left + (fun acc elem -> if check elem then elem::acc else acc) + [] files in + + let files_n = List.length files in + + (if files_n = 0 then + print_string "No tests were found. Did you compiled them? \n"); + + let exit_code = ref 0 in + let failed_test = ref 0 in + let tests_n = ref 0 in + let test_args = + ["--samples"; root_folder; + "--verbose"; string_of_int !global_verbose_lvl] + @ (if not (!global_ftitle = "") then + ["--ftitle"; !global_ftitle] else []) in + + let run_file test_path = + flush stdout; + + tests_n := !tests_n + 1; + let command_parts = Filename.concat folder test_path :: test_args in + let command_parts = + if Sys.os_type = "Win32" + then + (* I wish Filename.quote could be used on Windows. + + It would be appropriate if Ocaml spawned the process through the C + API, but Sys.command passes does it through the shell, which is + cmd.exe and has its own quoting rules. Ocaml has + Filename.quote_command, which does the right thing on every platform, + but it is only available since Ocaml 4.10. Until then, let's hope the + command does not need to be escaped. *) + command_parts + else List.map Filename.quote command_parts + in + + print_endline (String.concat " " command_parts); + exit_code := Sys.command (String.concat " " command_parts); + + (if !exit_code != 0 + then + ((if verbose 1 then print_file_name !tests_n files_n test_path false); + failed_test := !failed_test + 1) + else + (if verbose 1 then print_file_name !tests_n files_n test_path true); + ); + + (if verbose 2 then print_newline ()); + in + + List.iter run_file (List.filter must_run files); + + print_string "\n\n"; + print_string " Test Ran : "; print_int !tests_n; + print_string "\n Test Failed : "; print_int !failed_test; + print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); + print_endline "\n"
let _ = main ();
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/454e0f80017c25e2ce98bbe7c17105997...