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

Commits: c31a3765 by Simon Génier at 2020-12-05T16:57:32-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,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 ===================================== @@ -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,114 @@ 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 = + + 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

-let datacons_label_of_string location depth = function - | [Vstring _ as label] -> label - | _ -> error ~location "`##datacons-label<-string` expects 1 string argument" +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.add_builtin_function "datacons-label<-string" datacons_label_of_string 1 + add_builtin_cst "DataconsLabel" type_datacons_label; + add_builtin_cst "Heap" type_heap; + register_builtin (module DataconsLabelOfString); + register_builtin (module HeapAlloc); + register_builtin (module HeapFree); + register_builtin (module HeapExport); + register_builtin (module HeapStoreHeader); + register_builtin (module HeapStoreCell); + register_builtin (module HeapLoadCell)

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