Simon Génier pushed to branch heap at Stefan / Typer

Commits: 8740561e by Simon Génier at 2020-12-06T21:14:41-05:00 Add primitives for separate allocation and initialization.

- - - - -

6 changed files:

- btl/builtins.typer - + samples/heap.typer - src/builtin.ml - src/eval.ml - src/heap.ml - src/option.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -476,4 +476,22 @@ Test_neq = Built-in "Test.neq"; 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.

===================================== samples/heap.typer =====================================

===================================== src/builtin.ml ===================================== @@ -152,17 +152,14 @@ let register_builtin_csts () = add_builtin_cst "Eq" DB.type_eq; add_builtin_cst "Eq.refl" DB.eq_refl

+let type_arrow_0 = + mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) + let register_builtin_types () = 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 "Ref" type_arrow_0 in + let _ = new_builtin_type "Array" type_arrow_0 in let _ = new_builtin_type "FileHandle" DB.type0 in ()

===================================== src/eval.ml ===================================== @@ -56,13 +56,18 @@ 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 + +(** 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 arity = +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 +86,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

===================================== src/heap.ml ===================================== @@ -18,11 +18,21 @@ * 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 Builtin open Env +open Eval open Lexp -open Pexp + +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 @@ -30,11 +40,113 @@ let error ~(location : location) (message : string) : 'a = let dloc = Util.dummy_location let type0 = Debruijn.type0 let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) +let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) + +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 =

-let datacons_label_of_string location depth = function + 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) + +let datacons_label_of_string : builtin_function = + fun location _ + -> function | [Vstring _ as label] -> label - | _ -> error ~location "`##datacons-label<-string` expects 1 string argument" + | _ -> error ~location "`datacons-label<-string` expects [##DataconsLabel]." + +let heap_alloc : builtin_function = + fun location _ + -> function + | [Vint size] -> Vcommand (fun () -> Vint (alloc size)) + | _ -> error ~location "`Heap.alloc` expects [Int]." + +let heap_free : builtin_function = + fun location _ + -> function + | [Vint address] -> Vcommand (fun () -> free address; Vint 0) + | _ -> error ~location "`Heap.free` expects [Int]." + +let heap_export : builtin_function = + fun location _ + -> function + | [Vint address] -> export address + | _ -> error ~location "`Heap.export` expects [Int]." + +let heap_store_header : builtin_function = + fun location _ + -> function + | [Vint address; datacons] + -> Vcommand (fun () -> store_header location address datacons; Vint 0) + | _ -> error ~location "`Heap.store-header` expects [Int; 'a]" + +let heap_store_cell : builtin_function = + fun location _ + -> function + | [Vint address; Vint cell_index; value] + -> Vcommand (fun () -> store_cell address cell_index value; Vint 0) + | _ -> error ~location "`Heap.store-header` expects [Int; Int; 'a]" + +let heap_load_cell : builtin_function = + fun location _ + -> function + | [Vint address; Vint cell_index; value] + -> Vcommand (fun () -> load_cell address cell_index) + | _ -> error ~location "`Heap.store-cell` expects [Int; Int]"

let register_builtins () = - Builtin.add_builtin_cst "DataconsLabel" type_datacons_label; - Eval.add_builtin_function "datacons-label<-string" datacons_label_of_string 1 + add_builtin_cst "DataconsLabel" type_datacons_label; + add_builtin_cst "Heap" type_heap; + add_builtin_function "datacons-label<-string" datacons_label_of_string 1; + add_builtin_function "Heap.alloc" heap_alloc 1; + add_builtin_function "Heap.free" heap_alloc 1; + add_builtin_function "Heap.export" heap_alloc 1; + add_builtin_function "Heap.store-header" heap_store_header 2; + add_builtin_function "Heap.store-cell" heap_store_cell 3; + add_builtin_function "Heap.load-cell" heap_load_cell 2;

===================================== 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"

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8740561e4bce390d333ffc8b9809aad050...