diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..b953c9d5 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +interpreter/_build diff --git a/interpreter/default.nix b/interpreter/default.nix new file mode 100644 index 00000000..823756b4 --- /dev/null +++ b/interpreter/default.nix @@ -0,0 +1,9 @@ +{ nixpkgs ? import {} }: with nixpkgs; with ocaml-ng.ocamlPackages_4_14; +buildDunePackage rec { + pname = "wasm-components"; + version = "idk"; + useDune2 = true; + src = ./.; + nativeBuildInputs = [ menhir ]; + buildInputs = [ menhirLib (import ../../spec/interpreter { inherit nixpkgs; }) ]; +} diff --git a/interpreter/dune b/interpreter/dune new file mode 100644 index 00000000..ba4b6556 --- /dev/null +++ b/interpreter/dune @@ -0,0 +1,17 @@ +(env +; (_ (flags (:standard -w +a-4-27-42-44-45 -warn-error +a-3)))) + (dev (flags (:standard -g -w +a-4-27-42-44-45-70 -warn-error -A)))) +(include_subdirs unqualified) + + +(library + (name wasm_components) + (public_name wasm_components) + (modules ast desugar elaborate etypes etype_pp parse parser putil lexer flags script substitute subtype valid) + (libraries wasm menhirLib)) + +(executable + (name main) + (modules main run) + (modes byte exe) + (libraries bigarray wasm wasm_components)) diff --git a/interpreter/dune-project b/interpreter/dune-project new file mode 100644 index 00000000..f4850935 --- /dev/null +++ b/interpreter/dune-project @@ -0,0 +1,8 @@ +(lang dune 2.8) +(name wasm_components) + +(source (github dbp/components)) +(license Apache-2.0) +(authors "Daniel Patterson") +(maintainers "dbp@dbpmail.net") +(using menhir 2.1) diff --git a/interpreter/main/flags.ml b/interpreter/main/flags.ml new file mode 100644 index 00000000..e3fcc2ab --- /dev/null +++ b/interpreter/main/flags.ml @@ -0,0 +1,7 @@ +let interactive = ref false +let trace = ref false +let unchecked = ref false +let print_sig = ref false +let dry = ref false +let width = ref 80 +let harness = ref true diff --git a/interpreter/main/main.ml b/interpreter/main/main.ml new file mode 100644 index 00000000..bb7e4a00 --- /dev/null +++ b/interpreter/main/main.ml @@ -0,0 +1,57 @@ +open Wasm_components + +let name = "wasm" +let version = "1.1" + +let configure () = + Wasm.Import.register (Wasm.Utf8.decode "spectest") Wasm.Spectest.lookup; + Wasm.Import.register (Wasm.Utf8.decode "env") Wasm.Env.lookup + +let banner () = + print_endline (name ^ " " ^ version ^ " reference interpreter") + +let usage = "Usage: " ^ name ^ " [option] [file ...]" + +let args = ref [] +let add_arg source = args := !args @ [source] + +let quote s = "\"" ^ String.escaped s ^ "\"" + +let argspec = Arg.align +[ + "-", Arg.Set Wasm_components.Flags.interactive, + " run interactively (default if no files given)"; + "-e", Arg.String add_arg, " evaluate string"; + "-i", Arg.String (fun file -> add_arg ("(input " ^ quote file ^ ")")), + " read script from file"; + "-o", Arg.String (fun file -> add_arg ("(output " ^ quote file ^ ")")), + " write module to file"; + "-w", Arg.Int (fun n -> Wasm_components.Flags.width := n), + " configure output width (default is 80)"; + "-s", Arg.Set Flags.print_sig, " show module signatures"; + "-u", Arg.Set Flags.unchecked, " unchecked, do not perform validation"; + "-h", Arg.Clear Flags.harness, " exclude harness for JS conversion"; + "-d", Arg.Set Flags.dry, " dry, do not run program"; + "-t", Arg.Set Flags.trace, " trace execution"; + "-v", Arg.Unit banner, " show version" +] + +let () = + Printexc.record_backtrace true; + try + configure (); + Arg.parse argspec + (fun file -> add_arg ("(input " ^ quote file ^ ")")) usage; + List.iter (fun arg -> if not (Run.run_string arg) then exit 1) !args; + if !args = [] then Wasm_components.Flags.interactive := true; + if !Wasm_components.Flags.interactive then begin + Wasm_components.Flags.print_sig := true; + banner (); + Run.run_stdin () + end + with exn -> + flush_all (); + prerr_endline + (Sys.argv.(0) ^ ": uncaught exception " ^ Printexc.to_string exn); + Printexc.print_backtrace stderr; + exit 2 diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml new file mode 100644 index 00000000..a0ecf530 --- /dev/null +++ b/interpreter/script/run.ml @@ -0,0 +1,273 @@ +open Wasm_components +open Wasm_components.Script +open Wasm.Source + + +(* Errors & Tracing *) + +module Script = Wasm.Error.Make () +module Abort = Wasm.Error.Make () +module Assert = Wasm.Error.Make () +module IO = Wasm.Error.Make () + +exception Abort = Abort.Error +exception Assert = Assert.Error +exception IO = IO.Error + +let trace name = if !Flags.trace then print_endline ("-- " ^ name) + + +(* File types *) + +let binary_ext = "wasm" +let sexpr_ext = "wat" +let script_binary_ext = "bin.wast" +let script_ext = "wast" +let js_ext = "js" + +let dispatch_file_ext on_binary on_sexpr on_script_binary on_script on_js file = + if Filename.check_suffix file binary_ext then + on_binary file + else if Filename.check_suffix file sexpr_ext then + on_sexpr file + else if Filename.check_suffix file script_binary_ext then + on_script_binary file + else if Filename.check_suffix file script_ext then + on_script file + else if Filename.check_suffix file js_ext then + on_js file + else + raise (Sys_error (file ^ ": unrecognized file type")) + +(* Input *) + +let error at category msg = + trace ("Error: "); + prerr_endline (Wasm.Source.string_of_region at ^ ": " ^ category ^ ": " ^ msg); + false + +let input_from get_script run = + try + let script = get_script () in + trace "Running..."; + run script; + true + with + | Wasm.Decode.Code (at, msg) -> error at "decoding error" msg + | Wasm.Parse.Syntax (at, msg) -> error at "syntax error" msg + | Syntax (at, msg) -> error at "syntax error" msg + | Valid.Invalid (at, msg) -> + Printexc.print_backtrace stdout; + error at "invalid module" msg + | Wasm.Import.Unknown (at, msg) -> error at "link failure" msg + | Wasm.Eval.Link (at, msg) -> error at "link failure" msg + | Wasm.Eval.Trap (at, msg) -> error at "runtime trap" msg + | Wasm.Eval.Exhaustion (at, msg) -> error at "resource exhaustion" msg + | Wasm.Eval.Crash (at, msg) -> error at "runtime crash" msg + | Wasm.Encode.Code (at, msg) -> error at "encoding error" msg + | Script.Error (at, msg) -> error at "script error" msg + | IO (at, msg) -> error at "i/o error" msg + | Assert (at, msg) -> error at "assertion failure" msg + | Abort _ -> false + +let input_script start name lexbuf run = + input_from (fun _ -> Wasm_components.Parse.parse name lexbuf start) run + +let input_sexpr name lexbuf run = + input_from (fun _ -> + let x, c = Wasm_components.Parse.parse name lexbuf + Wasm_components.Parse.Component in + [Component (x, Textual c @@ no_region) @@ no_region]) run + +let input_binary name buf run = + input_from (fun _ -> + raise (Sys_error "i don't do this yet (2)")) run + +let input_sexpr_file input file run = + trace ("Loading (" ^ file ^ ")..."); + let ic = open_in file in + try + let lexbuf = Lexing.from_channel ic in + trace "Parsing..."; + let success = input file lexbuf run in + close_in ic; + success + with exn -> close_in ic; raise exn + +let input_binary_file file run = + trace ("Loading (" ^ file ^ ")..."); + let ic = open_in_bin file in + try + let len = in_channel_length ic in + let buf = Bytes.make len '\x00' in + really_input ic buf 0 len; + trace "Decoding..."; + let success = input_binary file (Bytes.to_string buf) run in + close_in ic; + success + with exn -> close_in ic; raise exn + +let input_js_file file run = + raise (Sys_error (file ^ ": unrecognized input file type")) + +let input_file file run = + trace ("Input file (\"" ^ String.escaped file ^ "\")..."); + dispatch_file_ext + input_binary_file + (input_sexpr_file input_sexpr) + (input_sexpr_file (input_script Wasm_components.Parse.Script)) + (input_sexpr_file (input_script Wasm_components.Parse.Script)) + input_js_file + file run + +let input_string string run = + trace ("Running (\"" ^ String.escaped string ^ "\")..."); + let lexbuf = Lexing.from_string string in + trace "Parsing..."; + input_script Wasm_components.Parse.Script "string" lexbuf run + + +(* Interactive *) + +let continuing = ref false + +let lexbuf_stdin buf len = + let prompt = if !continuing then " " else "> " in + print_string prompt; flush_all (); + continuing := true; + let rec loop i = + if i = len then i else + let ch = input_char stdin in + Bytes.set buf i ch; + if ch = '\n' then i + 1 else loop (i + 1) + in + let n = loop 0 in + if n = 1 then continuing := false else trace "Parsing..."; + n + +let input_stdin run = + let lexbuf = Lexing.from_function lexbuf_stdin in + let rec loop () = + let success = input_script Wasm_components.Parse.Script "stdin" lexbuf run in + if not success then Lexing.flush_input lexbuf; + if Lexing.(lexbuf.lex_curr_pos >= lexbuf.lex_buffer_len - 1) then + continuing := false; + loop () + in + try loop () with End_of_file -> + print_endline ""; + trace "Bye." + +(* Configuration *) + +let quote : script ref = ref [] +let desugar_ctx : Wasm_components.Desugar.definition_ctx + = Wasm_components.Desugar.empty_ctx () None +let valid_ctx : Wasm_components.Etypes.ctx ref + = ref (Wasm_components.Etypes.empty_ctx None false) + +(* Printing *) + +let print_component_type t = + Etype_pp.pp_line (fun () -> Etype_pp.emit_component_type !valid_ctx t) + +(* Running *) + +let rec run_definition def : Wasm_components.Ast.IntAst.component + = match def.it with + | Textual c -> + Wasm_components.Desugar._desugar_component (Desugar.SC desugar_ctx) c + | Encoded (name, bs) -> + raise (Sys_error "Binary modules not yet supported") + | Quoted (name, s) -> + trace "Parsing quote..."; + let x, c = + Wasm_components.Parse.parse name (Lexing.from_string s) + Wasm_components.Parse.Component in + run_definition (Textual c @@ no_region) + +let extract_msg s = + let rec strip_spaces s = if String.starts_with ~prefix:" " s + then strip_spaces (String.sub s 1 (String.length s - 1)) + else s in + strip_spaces (List.hd (List.rev (String.split_on_char '\n' s))) +let assert_message at name msg' re = + let msg = extract_msg msg' in + if + String.length msg < String.length re || + String.sub msg 0 (String.length re) <> re + then begin + print_endline ("Result: \"" ^ msg ^ "\""); + print_endline ("Expect: \"" ^ re ^ "\""); + Assert.error at ("wrong " ^ name ^ " error") + end + +let run_assertion ass = + match ass.it with + | AssertMalformed (def, re) -> + trace "Asserting malformed..."; + (match ignore (run_definition def) with + | exception Parse.Syntax (_, msg) -> assert_message ass.at "parsing" msg re + | _ -> Assert.error ass.at "expected decoding/parsing error" + ) + + | AssertInvalid (def, re) -> + trace "Asserting invalid..."; + (match + let m = run_definition def in + let _ = Valid.infer_component !valid_ctx m in + Assert.error ass.at "expected validation error" + with + | exception Wasm_components.Valid.Invalid (_, msg) -> + assert_message ass.at "validation" msg re + | _ -> Assert.error ass.at "expected validation error" + ) + +let rec run_command + (cmd : Wasm_components.Script.command) : unit = + match cmd.it with + | Component (x_opt, def) -> + let c = run_definition def in + if not !Flags.unchecked then begin + trace "Checking..."; + let t = Valid.infer_component !valid_ctx c in + if !Flags.print_sig then begin + trace "Signature:"; + print_component_type t + end; + Wasm_components.Desugar.bind desugar_ctx (Ast.Component @@ no_region) + x_opt; + valid_ctx := { !valid_ctx with + Etypes.components = !valid_ctx.Etypes.components + @ [ t ] } + end; + () (* TODO: actually run it *) + | Assertion ass -> + quote := cmd :: !quote; + if not !Flags.dry then begin + run_assertion ass + end + | Meta cmd -> + run_meta cmd +and run_meta cmd = + match cmd.it with + | Script (x_opt, script) -> + run_quote_script script; + + | Input (x_opt, file) -> + (try if not (input_file file run_quote_script) then + Abort.error cmd.at "aborting" + with Sys_error msg -> IO.error cmd.at msg) + +and run_script script = + List.iter run_command script + +and run_quote_script (script : Wasm_components.Script.script) = + let save_quote = !quote in + quote := []; + (try run_script script with exn -> quote := save_quote; raise exn); + quote := !quote @ save_quote + +let run_file file = input_file file run_script +let run_string string = input_string string run_script +let run_stdin () = input_stdin run_script diff --git a/interpreter/script/run.mli b/interpreter/script/run.mli new file mode 100644 index 00000000..d8b0f2b7 --- /dev/null +++ b/interpreter/script/run.mli @@ -0,0 +1,9 @@ +exception Abort of Wasm.Source.region * string +exception Assert of Wasm.Source.region * string +exception IO of Wasm.Source.region * string + +val trace : string -> unit + +val run_string : string -> bool +val run_file : string -> bool +val run_stdin : unit -> unit diff --git a/interpreter/script/script.ml b/interpreter/script/script.ml new file mode 100644 index 00000000..bc8272cf --- /dev/null +++ b/interpreter/script/script.ml @@ -0,0 +1,24 @@ +type var = string Wasm.Source.phrase + +type definition = definition' Wasm.Source.phrase +and definition' = + | Textual of Ast.VarAst.component + | Encoded of string * string + | Quoted of string * string +type assertion = assertion' Wasm.Source.phrase +and assertion' = + | AssertInvalid of definition * string + | AssertMalformed of definition * string +type command = command' Wasm.Source.phrase +and command' = + | Assertion of assertion + | Component of Ast.Var.binder * definition + | Meta of meta +and meta = meta' Wasm.Source.phrase +and meta' = + | Input of var option * string + (* | Output of var option * string option*) + | Script of var option * script +and script = command list + +exception Syntax of Wasm.Source.region * string diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml new file mode 100644 index 00000000..a57691e4 --- /dev/null +++ b/interpreter/syntax/ast.ml @@ -0,0 +1,486 @@ +module Source = Wasm.Source + +type name = string Source.phrase +type url = string Source.phrase +type externname = externname' Source.phrase +and externname' = + { + en_name : name; + en_url : url option; + } + +type core_sort = core_sort' Source.phrase +and core_sort' = + | Core_func + | Core_table + | Core_memory + | Core_global + | Core_type + | Core_module + | Core_instance +type sort = sort' Source.phrase +and sort' = + | CoreSort of core_sort + | Func + | Value + | Type + | Component + | Instance +type val_int_size = VI_8 | VI_16 | VI_32 | VI_64 +type val_float_size = VF_32 | VF_64 + +let show_core_sort' (s : core_sort') : string + = match s with + | Core_func -> "func" + | Core_table -> "table" + | Core_memory -> "memory" + | Core_global -> "global" + | Core_type -> "type" + | Core_module -> "module" + | Core_instance -> "instance" +let show_sort' (s : sort') : string + = match s with + | CoreSort s' -> "core_" ^ show_core_sort' s'.Source.it + | Func -> "func" + | Value -> "value" + | Type -> "type" + | Component -> "component" + | Instance -> "instance" + + +module type AstParams = sig + type ident + type 'a bound + type 'a core_externdesc_wrapper + type 'a typeuse +end +module type AstT = sig + type core_memory_id + type core_func_id + type core_module_id + type core_instance_id + type component_id + type instance_id + type value_id + type func_id + type outer_id + type core_sort_idx + type core_sort_idx' + type sort_idx + type sort_idx' + type core_export + type core_export' + type core_instantiate_arg + type core_instantiate_arg' + type core_instance_expr + type core_instance_expr' + type inline_export + type inline_export' + type export + type export' + type instantiate_arg + type instantiate_arg' + type instance_expr + type instance_expr' + type core_alias_target + type core_alias_target' + type core_alias + type core_alias' + type alias_target + type alias_target' + type alias + type alias' + type core_functype + type core_deftype + type core_deftype' + type core_typedecl + type core_typedecl' + type core_externdesc + type core_exportdecl + type core_exportdecl' + type core_moduledecl + type core_moduledecl' + type core_moduletype + type core_moduletype' + type core_deftype_ + type core_deftype_' + type record_field + type record_field' + type variant_case + type variant_case' + type def_val_type + type def_val_type' + type val_type + type func_ios + type func_ios' + type func_type + type func_type' + type type_bound + type type_bound' + type component_type + type component_type' + type instance_type + type instance_type' + type component_decl + type component_decl' + type instance_decl + type instance_decl' + type importdecl + type importdecl' + type exportdecl + type exportdecl' + type def_type + type def_type' + type canon_opt + type canon_opt' + type canon + type canon' + type start + type start' + type import + type import' + type core_definition + type definition + type definition' + type component + type component' +end +module Make (P : AstParams) = struct + + type core_memory_id = P.ident + type core_func_id = P.ident + type core_module_id = P.ident + type core_instance_id = P.ident + + type component_id = P.ident + type instance_id = P.ident + type value_id = P.ident + type func_id = P.ident + + type outer_id = P.ident + + type core_sort_idx = core_sort_idx' Source.phrase + and core_sort_idx' = + { + c_s_sort : core_sort; + c_s_idx : P.ident; + } + + type sort_idx = sort_idx' Source.phrase + and sort_idx' = + { + s_sort : sort; + s_idx : P.ident; + } + + (* # Core instantiate *) + + type core_export = core_export' Source.phrase + and core_export' = + { + c_e_name : name; + c_e_value : core_sort_idx; + } + type core_instantiate_arg = core_instantiate_arg' Source.phrase + and core_instantiate_arg' = + { + c_ia_name : name; + c_ia_value : core_sort_idx; + } + type core_instance_expr = core_instance_expr' Source.phrase + and core_instance_expr' = + | Core_instantiate_module of core_module_id * core_instantiate_arg list + | Core_instantiate_inline of core_export list + + (* # Instantiate *) + + type inline_export = inline_export' Source.phrase + and inline_export' = + { + ie_name : externname; + ie_value : sort_idx; + } + type instantiate_arg = instantiate_arg' Source.phrase + and instantiate_arg' = + { + ia_name : name; + ia_value : sort_idx; + } + type instance_expr = instance_expr' Source.phrase + and instance_expr' = + | Instantiate_component of component_id * instantiate_arg list + | Instantiate_inline of inline_export list + + (* # Core Alias *) + + type core_alias_target = core_alias_target' Source.phrase + and core_alias_target' = + | Core_alias_export of core_instance_id * name + | Core_alias_outer of outer_id * P.ident + + type core_alias = core_alias' Source.phrase + and core_alias' = + { + c_a_target : core_alias_target; + c_a_sort : core_sort + } + + (* # Alias *) + + type alias_target = alias_target' Source.phrase + and alias_target' = + | Alias_export of instance_id * name + | Alias_core_export of core_instance_id * name + | Alias_outer of outer_id * P.ident + type alias = alias' Source.phrase + and alias' = + { + a_target : alias_target; + a_sort : sort; + } + + (* # Core Type *) + + type core_functype = Wasm.Ast.type_ + + type core_deftype = core_deftype' Source.phrase + and core_deftype' = + | Core_deftype_functype of core_functype + (* With GC:modul + | Core_deftype_structtype of core_structtype + | Core_deftype_arraytype of core_arraytype + *) + + type core_typedecl = core_typedecl' Source.phrase + and core_typedecl' = + { + c_td_type : core_deftype + } + type core_externdesc = Wasm.Ast.import_desc P.core_externdesc_wrapper + type core_exportdecl = core_exportdecl' Source.phrase + and core_exportdecl' = + { + c_ed_name : name; + c_ed_ty : core_externdesc; + } + type core_importdecl = core_importdecl' Source.phrase + and core_importdecl' = + { + c_id_name1 : name; + c_id_name2 : name; + c_id_ty : core_externdesc; + } + type core_moduledecl = core_moduledecl' Source.phrase + and core_moduledecl' = + (* imports are conceptually bound, but the binding is inside of + P.core_externdesc_wrapper *) + | Core_md_importdecl of core_importdecl + | Core_md_typedecl of core_deftype P.bound + | Core_md_aliasdecl of core_alias P.bound + | Core_md_exportdecl of core_exportdecl + + type core_moduletype = core_moduletype' Source.phrase + and core_moduletype' = + { + decls : core_moduledecl list + } + + type core_deftype_ = core_deftype_' Source.phrase + and core_deftype_' = + | Core_deftype__deftype of core_deftype + | Core_deftype__moduletype of core_moduletype + + (* # Type *) + type record_field = record_field' Source.phrase + and record_field' = + { + rf_name : name; + rf_type : val_type; + } + and variant_case = variant_case' Source.phrase + and variant_case' = + { + vc_name : name; + vc_type : val_type option; + vc_default : P.ident option; + } + and def_val_type = def_val_type' Source.phrase + and def_val_type' = + | Record of record_field list + | Variant of (variant_case P.bound) list + | List of val_type + | Tuple of val_type list + | Flags of name list + | Enum of name list + | Union of val_type list + | Option of val_type + | Expected of val_type option * val_type option + | Own of P.ident + | Borrow of P.ident + | Bool + | Signed of val_int_size | Unsigned of val_int_size + | Float of val_float_size + | Char | String + and val_type = def_val_type P.typeuse + type func_ios = func_ios' Source.phrase + and func_ios' = + | Fio_one of val_type + | Fio_many of (name * val_type) list + type func_type = func_type' Source.phrase + and func_type' = + { + ft_params : func_ios; + ft_result : func_ios; + } + and component_type = component_type' Source.phrase + and component_type' = component_decl list + and instance_type = instance_type' Source.phrase + and instance_type' = instance_decl list + and component_decl = component_decl' Source.phrase + and component_decl' = + | Component_import of importdecl + | Component_instance of instance_decl + and instance_decl = instance_decl' Source.phrase + and instance_decl' = + | Instance_type of def_type P.bound + | Instance_alias of alias P.bound + | Instance_export of exportdecl + and importdecl = importdecl' Source.phrase + and importdecl' = { id_name : externname; id_type : importdesc } + and exportdecl = exportdecl' Source.phrase + and exportdecl' = { ed_name : externname; ed_type : importdesc } + and importdesc = exportdesc P.bound + and exportdesc = exportdesc' Source.phrase + and exportdesc' = + | Export_sort_id of sort * P.ident + | Export_core_mod of core_moduletype + | Export_func of func_type + | Export_comp of component_type + | Export_inst of instance_type + | Export_val of val_type + | Export_type of type_bound + and type_bound = type_bound' Source.phrase + and type_bound' = + | Tbound_subr + | Tbound_eq of def_type P.typeuse + and def_type = def_type' Source.phrase + and def_type' = + | Deftype_val of def_val_type + | Deftype_func of func_type + | Deftype_comp of component_type + | Deftype_inst of instance_type + | Deftype_rsrc of P.ident option (* destructor index *) + + (* # Canon *) + type canon_opt = canon_opt' Source.phrase + and canon_opt' = + | String_utf8 + | String_utf16 + | String_latin1_utf16 + | Memory of core_memory_id + | Realloc of core_func_id + | PostReturn of core_func_id + type canon_resource_builtin = canon_resource_builtin' Source.phrase + and canon_resource_builtin' = + | CRB_new of def_type P.typeuse + | CRB_drop of val_type + | CRB_rep of def_type P.typeuse + type canon = canon' Source.phrase + and canon' = + | Canon_lift of core_func_id * exportdesc * canon_opt list + | Canon_lower of func_id * canon_opt list + | Canon_resource_builtin of canon_resource_builtin + + (* # Start *) + type start = start' Source.phrase + and start' = + { + s_func : func_id; + s_params : value_id list; + s_result : unit P.bound list; + } + + type import = import' Source.phrase + and import' = { i_name : externname; i_type : importdesc; } + + type export = export' Source.phrase + and export' = + { + e_name : externname; + e_value : sort_idx; + e_type : exportdesc option + } + + type core_definition = + | CoreModuleDef of Wasm.Ast.module_ P.bound + | CoreInstanceDef of core_instance_expr P.bound + | CoreTypeDef of core_deftype_ P.bound + type definition = definition' Source.phrase + and definition' = + | CoreDef of core_definition + | ComponentDef of component + | InstanceDef of instance_expr P.bound + | AliasDef of alias P.bound + | TypeDef of def_type P.bound + | CanonDef of canon P.bound + | StartDef of start + | ImportDef of import (* the binder is inside the importdesc *) + | ExportDef of export P.bound + and component = component' P.bound Source.phrase + and component' = + { + defns : definition list + } +end + +module Int32_AstParams : (AstParams + with type ident = int32 + with type 'a bound = 'a + with type 'a core_externdesc_wrapper = + Wasm.ParseUtil.context * 'a + with type 'a typeuse = int32) = struct + type ident = int32 + type 'a bound = 'a + type 'a core_externdesc_wrapper = Wasm.ParseUtil.context * 'a + type 'a typeuse = int32 +end +module IntAst = Make(Int32_AstParams) + +type var = string Source.phrase +module VarQ (VarAst : AstT) = struct + type ident = + | Idx of int32 Source.phrase + | Var of var + | Export of sort * ident * name list (* inline export alias *) + | CoreInlineInstance of VarAst.core_export list + | InlineInstance of VarAst.inline_export list + type binder = + | No_binder + | Var_binder of var + (*| Export_binder of externname (* TODO TEMPORARY REMOVE REMOVE *)*) + | Export_binders of externname list + type 'a bound = { body : 'a; binder : binder } + let bind b a = { body = a; binder = b } + let string_of_binder x = + let open Source in + match x with + | No_binder -> "_" + | Var_binder v -> v.it + | Export_binders es -> "(" ^ String.concat " " (List.map (fun x -> x.it.en_name.it) es) ^ ")" + type 'a core_externdesc_wrapper = Wasm.ParseUtil.context -> unit -> 'a + type 'a typeuse = + | TVar of ident + | TInline of 'a +end +module rec VarD : + (AstParams + with type ident = VarQ(Make(VarD)).ident + with type 'a bound = 'a VarQ(Make(VarD)).bound + with type 'a core_externdesc_wrapper = + 'a VarQ(Make(VarD)).core_externdesc_wrapper + with type 'a typeuse = 'a VarQ(Make(VarD)).typeuse) = struct + include VarQ(Make(VarD)) +end + +module VarAst = Make(VarD) +module Var = VarQ(Make(VarD)) diff --git a/interpreter/test/resource/resource-simple.wast b/interpreter/test/resource/resource-simple.wast new file mode 100644 index 00000000..74f63186 --- /dev/null +++ b/interpreter/test/resource/resource-simple.wast @@ -0,0 +1,271 @@ +(assert_invalid + (component + (core module $cm + (func (export "one") (param i32) (result i32) (i32.const 1))) + (core instance $ci (instantiate $cm)) + (type $t (resource (rep i32))) + (export $et "t" (type $t))) + "Cannot export type containing bare resource type") + +(assert_invalid + (component + (core module $cm + (func (export "one") (param i32) (result i32) (i32.const 1))) + (core instance $ci (instantiate $cm)) + (type $t (resource (rep i32))) + (export $et "t" (type $t) (type (sub resource))) + (alias core export $ci "one" (core func $cf1)) + (canon lift $cf1 (func $f1 (param (own $t)) (result (own $t)))) + (export "one" (func $f1))) + "Cannot export type containing bare resource type") + +(assert_invalid + (component $C + (type $t (resource (rep i32))) + (component + (alias outer $C $t (type)))) + "Cannot export type containing bare resource type") + +(assert_invalid + (component $C + (type $t (resource (rep i32))) + (export $et "t" (type $t) (type (sub resource))) + (component + (alias outer $C $et (type)))) + "Cannot export type containing bare resource type") + +(assert_invalid + (component $C + (import "t" (type $it (sub resource))) + (component + (alias outer $C $it (type)))) + "Outer alias may not refer to type variable") + +(component $dt + (core module $cm + (func (export "one") (param i32) (result i32) (local.get 0))) + (core instance $ci (instantiate $cm)) + (type $t (resource (rep i32))) + (export $et "t" (type $t) (type (sub resource))) + (alias core export $ci "one" (core func $cf1)) + (canon lift $cf1 (func $f1 (param (own $t)) (result (own $t)))) + (export "one" (func $f1) (func (param (own $et)) (result (own $et))))) + +(component $use1 + (import "deftype" (instance $deftype + (export "t" (type $et (sub resource))) + (export "one" (func (param (own $et)) (result (own $et)))))) + (alias export $deftype "t" (type $det)) + (alias export $deftype "one" (func $f1)) + (canon lower $f1 (core func $cf1)) + (core module $cm + (import "dt" "one" (func $one (param i32) (result i32))) + (func (export "two") (param i32) (result i32) (local.get 0) (call $one))) + (core instance $ci (instantiate $cm + (with "dt" (instance (export "one" (func $cf1)))))) + (alias core export $ci "two" (core func $cf2)) + (canon lift $cf2 (func $f2 (param (own $det)) (result (own $det)))) + (export "two" (func $f2))) + +(component + (instance $deftype (instantiate $dt)) + (instance (instantiate $use1 (with "deftype" (instance $deftype))))) + +(component $use2i + (import "deftype" (instance $deftype + (export "t" (type $et (sub resource))) + (export "one" (func (param (own $et)) (result (own $et)))))) + (alias export $deftype "t" (type $det)) + (import "two" (instance $itwo + (alias outer $use2i $det (type $iet)) + (export "two" (func (param (own $iet)) (result (own $iet))))))) + +(component + (instance $deftype (instantiate $dt)) + (instance $itwo (instantiate $use1 (with "deftype" (instance $deftype)))) + (instance (instantiate $use2i + (with "deftype" (instance $deftype)) + (with "two" (instance $itwo))))) + +(component $use2c + (import "deftype" (instance $deftype + (export "t" (type $et (sub resource))) + (export "one" (func (param (own $et)) (result (own $et)))))) + (import "two" (component $ctwo + (import "deftype" (instance $deftype + (export "t" (type $et (sub resource))) + (export "one" (func (param (own $et)) (result (own $et)))))) + (alias export $deftype "t" (type $det)) + (export "two" (func (param (own $det)) (result (own $det)))))) + (alias export $deftype "t" (type $det)) + (alias export $deftype "one" (func $f1)) + (instance $itwo (instantiate $ctwo + (with "deftype" (instance $deftype)))) + (alias export $itwo "two" (func $f2)) + (export "one" (func $f1)) + (export "two" (func $f2)) + ) + +(component + (instance $deftype (instantiate $dt)) + (instance (instantiate $use2c + (with "deftype" (instance $deftype)) + (with "two" (component $use1))))) + +(component $dt2 + (type $t1 (resource (rep i32))) + (type $t2 (resource (rep i32))) + (export $et1 "t1" (type $t1) (type (sub resource))) + (export $et2 "t2" (type $t2) (type (sub resource))) + (core module $cm + (func (export "id") (param i32) (result i32) (local.get 0))) + (core instance $ci (instantiate $cm)) + (alias core export $ci "id" (core func $cfid)) + (canon lift $cfid (func $fid1 (param (own $et1)) (result (own $et1)))) + (canon lift $cfid (func $fid2 (param (own $et2)) (result (own $et2)))) + (export "one" (func $fid1)) + (export "two" (func $fid2))) + +(component $needs_dt2i + (import "deftype" (component + (export "t1" (type $t1 (sub resource))) + (export "t2" (type $t2 (sub resource))) + (export "one" (func (param (own $t1)) (result (own $t1)))) + (export "two" (func (param (own $t2)) (result (own $t2))))))) + +(component + (instance (instantiate $needs_dt2i + (with "deftype" (component $dt2))))) + +(component $needs_dt2i_backwards + (import "deftype" (component + (export "t1" (type $t1 (sub resource))) + (export "t2" (type $t2 (sub resource))) + (export "one" (func (param (own $t2)) (result (own $t2)))) + (export "two" (func (param (own $t1)) (result (own $t1))))))) + +(assert_invalid + (component + (instance (instantiate $needs_dt2i_backwards + (with "deftype" (component $dt2))))) + "Type variable u0.0 is not u0.1") + + +(component $needs_two_imports_same + (import "uses_types" (component + (import "t1" (type $t1 (sub resource))) + (import "t2" (type (eq $t1)))))) + +(component $needs_two_imports_different + (import "uses_types" (component + (import "t1" (type (sub resource))) + (import "t2" (type (sub resource)))))) + +(component $two_imports_same + (import "t1" (type $t1 (sub resource))) + (import "t2" (type (eq $t1)))) + +(component $two_imports_different + (import "t1" (type (sub resource))) + (import "t2" (type (sub resource)))) + +(component + (instance (instantiate $needs_two_imports_different + (with "uses_types" (component $two_imports_different))))) + +(assert_invalid + (component + (instance (instantiate $needs_two_imports_different + (with "uses_types" (component $two_imports_same))))) + "Type variable u0.0 is not u0.1") + +(component + (instance (instantiate $needs_two_imports_same + (with "uses_types" (component $two_imports_different))))) + +(component + (instance (instantiate $needs_two_imports_same + (with "uses_types" (component $two_imports_same))))) + +(component $needs_exports_shared + (import "deftype" (component + (export "t1" (type $t (sub resource))) + (export "t2" (type (eq $t)))))) + +(component $exports_shared + (type $t (resource (rep i32))) + (export $t1 "t1" (type $t) (type (sub resource))) + (export "t2" (type $t) (type (eq $t1)))) + +(component + (instance (instantiate $needs_exports_shared + (with "deftype" (component $exports_shared))))) + +(component $exports_shared_reverse + (type $t (resource (rep i32))) + (export $t2 "t2" (type $t) (type (sub resource))) + (export "t1" (type $t) (type (eq $t2)))) + +(component + (instance (instantiate $needs_exports_shared + (with "deftype" (component $exports_shared_reverse))))) + +(component $exports_not_shared + (type $t (resource (rep i32))) + (export "t1" (type $t) (type (sub resource))) + (export "t2" (type $t) (type (sub resource)))) + +(assert_invalid + (component + (instance (instantiate $needs_exports_shared + (with "deftype" (component $exports_not_shared))))) + "Type variable u0.0 is not u0.1") + +(component + (import "in" (component $in + (export "t" (type (sub resource))))) + (instance $ii (instantiate $in))) + +(assert_invalid + (component + (import "in" (component $in + (export "t" (type (sub resource))))) + (instance $ii (instantiate $in)) + (alias export $ii "t" (type $t)) + (export "t" (type $t))) + "Component type may not refer to non-imported uvar") + +(assert_invalid + (component + (import "in" (component $in + (export "t" (type $t (sub resource))) + (export "f" (func (param (own $t)) (result (own $t)))))) + (instance $ii (instantiate $in)) + (alias export $ii "f" (func $f)) + (export "f" (func $f))) + "Component type may not refer to non-imported uvar") + +(assert_invalid + (component + (import "in" (component $in + (export "i2" (instance + (export "t" (type (sub resource))))))) + (instance $ii (instantiate $in)) + (alias export $ii "i2" (instance $i2)) + (export "i2" (instance $i2))) + "Component type may not refer to non-imported uvar") + +(component + (type $t (resource (rep i32))) + (canon resource.new $t (core func $tnew)) + (canon resource.drop (own $t) (core func $tdrop)) + (canon resource.rep $t (core func $trep)) + (core module $cm + (import "t" "new" (func (param i32) (result i32))) + (import "t" "drop" (func (param i32))) + (import "t" "rep" (func (param i32) (result i32)))) + (core instance (instantiate $cm + (with "t" (instance + (export "new" (func $tnew)) + (export "drop" (func $tdrop)) + (export "rep" (func $trep))))))) diff --git a/interpreter/text/Putil.ml b/interpreter/text/Putil.ml new file mode 100644 index 00000000..b15ea8f8 --- /dev/null +++ b/interpreter/text/Putil.ml @@ -0,0 +1,41 @@ +open Wasm.Source + +type var = Ast.var +type 'a perhaps_named = Ast.Var.binder * 'a + +(* Error handling *) + +let error at msg = raise (Script.Syntax (at, msg)) + +(*let parse_error msg = + error Source.no_region + (if msg = "syntax error" then "unexpected token" else msg)*) + +(* Position handling *) + +let convert_pos pos = + { file = pos.Lexing.pos_fname; + line = pos.Lexing.pos_lnum; + column = pos.Lexing.pos_cnum - pos.Lexing.pos_bol + } + +let region lexbuf = + let left = convert_pos (Lexing.lexeme_start_p lexbuf) in + let right = convert_pos (Lexing.lexeme_end_p lexbuf) in + {left = left; right = right} + +let span_regions left right = + { left = left.left; right = right.right } + +let position_to_pos position = + { file = position.Lexing.pos_fname; + line = position.Lexing.pos_lnum; + column = position.Lexing.pos_cnum - position.Lexing.pos_bol + } + +let positions_to_region position1 position2 = + { left = position_to_pos position1; + right = position_to_pos position2 + } + +let ptr x y = positions_to_region x y diff --git a/interpreter/text/desugar.ml b/interpreter/text/desugar.ml new file mode 100644 index 00000000..5b68858e --- /dev/null +++ b/interpreter/text/desugar.ml @@ -0,0 +1,1040 @@ +open Ast +module Source = Wasm.Source +open Source +module V = struct + include Ast.VarAst + include Ast.Var +end +module I = struct + include Ast.IntAst + include Ast.Int32_AstParams +end + +module CoreCtx = Wasm.ParseUtil +module VarMap = CoreCtx.VarMap +type space = CoreCtx.space + = {mutable map : int32 VarMap.t; mutable count : int32} +let empty () = {map = VarMap.empty; count = 0l} +type core_types = {ct_space : space; mutable ct_list : I.core_deftype_ list} +let empty_core_types () = {ct_space = empty (); ct_list = []} + +let atmap' + (f : 'a -> Source.region -> 'b) + (x : 'a Source.phrase) + : 'b Source.phrase + = { Source.it = f x.Source.it x.Source.at; Source.at = x.Source.at; } +let atmap (f : 'a -> 'b) : 'a Source.phrase -> 'b Source.phrase + = atmap' (fun x r -> f x) + +let unimplemented err = raise (Sys_error ("Unimplemented " ^ err)) + +type core_ctx = + { core_types : core_types + ; core_funcs : space + ; core_modules : space + ; core_instances : space + ; core_tables : space + ; core_mems : space + ; core_globals : space + } +let empty_core_ctx () = + { core_types = empty_core_types () + ; core_funcs = empty () + ; core_modules = empty () + ; core_instances = empty () + ; core_tables = empty () + ; core_mems = empty () + ; core_globals = empty () + } + +type ctx_for_definition +type ctx_for_core_module_decl +type ctx_for_component_decl +type _ desugar_def = + | DD_def : I.definition -> ctx_for_definition desugar_def + | DD_cmd : I.core_moduledecl -> ctx_for_core_module_decl desugar_def + | DD_cd : I.instance_decl -> ctx_for_component_decl desugar_def +let from_def_dd (def : ctx_for_definition desugar_def) : I.definition + = match def with + | DD_def d -> d +let from_cmd_dd (def : ctx_for_core_module_decl desugar_def) : I.core_moduledecl + = match def with + | DD_cmd d -> d +let from_cd_dd_i (def : ctx_for_component_decl desugar_def) : I.instance_decl + = match def with + | DD_cd d -> d +let from_cd_dd (def : ctx_for_component_decl desugar_def) : I.component_decl + = let id = from_cd_dd_i def in + I.Component_instance id @@ id.at +type some_ctx = + | SC : 'a ctx -> some_ctx +and 'a ctx = + { parent : some_ctx option + ; name : var option + ; core_ctx : core_ctx + ; types : space + ; components : space + ; instances : space + ; funcs : space + ; values : space + ; mutable desugar_defs_pre : 'a desugar_def list + ; mutable desugar_defs_post : 'a desugar_def list + } +type definition_ctx = ctx_for_definition ctx +type core_module_decl_ctx = ctx_for_core_module_decl ctx +type component_decl_ctx = ctx_for_component_decl ctx + +let empty_ctx_ parent name = + { parent = parent + ; name = name + ; core_ctx = empty_core_ctx () + ; types = empty () + ; components = empty () + ; instances = empty () + ; funcs = empty () + ; values = empty () + ; desugar_defs_pre = [] + ; desugar_defs_post = [] + } +let empty_ctx () = empty_ctx_ None +let new_ctx parent = empty_ctx_ (Some parent) + +let name_of_core_sort core_sort = + "core " ^ + match core_sort.it with + | Core_func -> "function" + | Core_table -> "table" + | Core_memory -> "memory" + | Core_global -> "global" + | Core_type -> "type" + | Core_module -> "module" + | Core_instance -> "instance" +let space_of_core_sort core_ctx core_sort = + match core_sort.it with + | Core_func -> core_ctx.core_funcs + | Core_table -> core_ctx.core_tables + | Core_memory -> core_ctx.core_mems + | Core_global -> core_ctx.core_globals + | Core_type -> core_ctx.core_types.ct_space + | Core_module -> core_ctx.core_modules + | Core_instance -> core_ctx.core_instances +let name_of_sort sort = + match sort.it with + | CoreSort cs -> name_of_core_sort cs + | Func -> "func" + | Value -> "value" + | Type -> "type" + | Component -> "component" + | Instance -> "instance" +let space_of_sort ctx sort = + match sort.it with + | CoreSort cs -> space_of_core_sort ctx.core_ctx cs + | Func -> ctx.funcs + | Value -> ctx.values + | Type -> ctx.types + | Component -> ctx.components + | Instance -> ctx.instances + +(* TODO: 2^32 range checks in various places in both here and the written + version *) +let anon ctx sort n = + let space = space_of_sort ctx sort in + let i = space.count in + space.count <- Int32.add i n; + if Wasm.I32.lt_u space.count n then + Putil.error Source.no_region + ("too many " ^ name_of_sort sort ^ " bindings"); + i + + +let to_outer_name (b : V.binder) : var option + = match b with + | V.Var_binder v -> Some v + | _ -> None + +type 'c export_func = 'c ctx -> sort -> externname -> I.ident -> unit +let bind_ : 'c. 'c export_func -> 'c ctx -> sort -> V.binder -> unit + = fun export_func ctx sort x -> + let space = space_of_sort ctx sort in + let i = anon ctx sort 1l in + match x with + | V.No_binder -> () + | V.Var_binder v -> space.map <- VarMap.add v.it i space.map + | V.Export_binders ns -> ignore (List.map (fun n -> export_func ctx sort n i) ns) +let bind_export_def ctx sort n i + = ctx.desugar_defs_post <- + DD_def (I.ExportDef ({ I.e_name = n; + I.e_value = { I.s_sort = sort; I.s_idx = i; } + @@ no_region; + I.e_type = None } + @@ no_region) + @@ no_region) + ::ctx.desugar_defs_post +let bind = bind_ bind_export_def +let bind_export_no : 'c. 'c export_func + = fun ctx srt n i -> Putil.error no_region "export binding not allowed here" +let bind_NE + : 'c. 'c ctx -> sort -> V.binder -> unit + = fun ctx sort x -> bind_ bind_export_no ctx sort x +let bind_type_ export_func ctx x t + = bind_ export_func ctx (Type @@ t.at) x +let bind_type = bind_type_ bind_export_def +let bind_type_NE = bind_type_ bind_export_no +let bind_core_type_ export_func ctx x t + = bind_ export_func ctx (CoreSort (Core_type @@ t.at) @@ t.at) x; + ctx.core_ctx.core_types.ct_list <- + ctx.core_ctx.core_types.ct_list @ [t] +let bind_core_type = bind_core_type_ bind_export_def +let bind_core_type_NE = bind_core_type_ bind_export_no + +type 'a make_alias_type = + 'a ctx -> sort -> region -> int32 -> int32 -> I.ident +let lookup_here ctx sort x = + try + Some (VarMap.find x.it (space_of_sort ctx sort).map) + with Not_found -> None +let rec lookup_opt + : 'a 'b. 'a make_alias_type -> 'a ctx -> 'b ctx -> int + -> sort -> var -> I.ident option + = fun make_alias ctx_orig ctx n sort x -> + match lookup_here ctx sort x with + | Some id -> Some (make_alias ctx_orig sort x.at (Int32.of_int n) id) + | None -> match ctx.parent with + | None -> None + | Some (SC ctx') -> + lookup_opt make_alias ctx_orig ctx' (n+1) sort x +let lookup_ (make_alias : 'a make_alias_type) (ctx : 'a ctx) + (sort : sort) (x : var) = + match lookup_opt make_alias ctx ctx 0 sort x with + | Some id -> id + | None -> Putil.error x.at ("unknown " ^ name_of_sort sort ^ " " ^ x.it) +let make_alias_def ctx sort at oi id + = if oi = 0l then id + else (ctx.desugar_defs_pre <- + DD_def (I.AliasDef ({ I.a_target = I.Alias_outer (oi, id) @@ at + ; I.a_sort = sort } @@ at) @@ at) + ::ctx.desugar_defs_pre; + anon ctx sort 1l) +let lookup = lookup_ make_alias_def +let make_alias_cmd ctx sort at oi id + = match sort.it with + | CoreSort s' -> + if oi = 0l then id + else (ctx.desugar_defs_pre <- + DD_cmd (I.Core_md_aliasdecl + ({ I.c_a_target = I.Core_alias_outer (oi, id) @@ at + ; I.c_a_sort = s' } @@ at) @@ at) + ::ctx.desugar_defs_pre; + anon ctx sort 1l) + | _ -> Putil.error sort.at ("can't reference non-core sort " + ^ name_of_sort sort ^ " in core:moduledecl") +let lookup_cmd = lookup_ make_alias_cmd +let make_alias_cd ctx sort at oi id + = if oi = 0l then id + else (ctx.desugar_defs_pre <- + DD_cd (I.Instance_alias ({ I.a_target = I.Alias_outer (oi, id) @@ at + ; I.a_sort = sort } @@ at) @@ at) + ::ctx.desugar_defs_pre; + anon ctx sort 1l) +let lookup_cd = lookup_ make_alias_cd +(* for alias stuff *) +let rec raw_lookup_n : 'a. 'a ctx -> int -> sort -> var -> I.ident + = fun ctx n sort x -> + if n = 0 then + match lookup_here ctx sort x with + | None -> Putil.error x.at ("Nothing named exists in that context") + | Some idx -> idx + else match ctx.parent with + | None -> Putil.error x.at ("Fewer than " ^ string_of_int n + ^ " surrounding contexts") + | Some (SC ctx') -> raw_lookup_n ctx' (n-1) sort x +let rec find_parent_index : 'a. 'a ctx -> var -> int32 + = fun ctx var -> + if Some var.it = Option.map (fun x -> x.it) ctx.name then 0l + else match ctx.parent with + | None -> Putil.error var.at ("No parent context named " ^ var.it) + | Some (SC ctx') -> Int32.succ (find_parent_index ctx' var) + +let rec desugar_ident + (ctx : definition_ctx) + (s : sort) (i : V.ident) + : I.ident + = match i with + | V.Idx i -> i.it + | V.Var v -> lookup ctx s v + | V.Export (s', i, ns) -> + let sort_eq a b = match a.it, b.it with + | CoreSort aa, CoreSort bb -> aa.it = bb.it + | _, _ -> a.it = b.it in + if not (sort_eq s' s) then + Putil.error s'.at ("sort_idx: export: " ^ name_of_sort s' + ^ " != " ^ name_of_sort s); + let rgn = Putil.span_regions s'.at (List.hd (List.rev ns)).at in + let if_core core noncore = match s'.it with + | CoreSort _ -> core + | _ -> noncore + in + let i_sort = + if_core (CoreSort (Core_instance @@ rgn) @@ rgn) (Instance @@ rgn) in + let i' = desugar_ident ctx i_sort i in + let go i s'' n = + let target = + if_core (I.Alias_core_export (i, n)) (I.Alias_export (i, n)) in + ctx.desugar_defs_pre <- + DD_def (I.AliasDef ({ I.a_target = target @@ rgn + ; I.a_sort = s'' } @@ rgn) + @@ rgn)::ctx.desugar_defs_pre; + anon ctx s'' 1l + in + let rec go' i ns = match ns with + | [] -> Putil.error s.at "sort_idx: export: no names" + | [n] -> go i s' n + | n::ns -> let i' = go i i_sort n in go' i' ns + in go' i' ns + | _ -> Putil.error s.at "ident: unexpected inline instance" +let desugar_ident_cmd + (ctx : core_module_decl_ctx) (s : sort) (i : V.ident) + : I.ident + = match i with + | V.Idx i -> i.it + | V.Var v -> lookup_cmd ctx s v + | _ -> Putil.error s.at "ident: unexpected inline instance or export" +let rec desugar_ident_cd + (ctx : component_decl_ctx) (s : sort) (i : V.ident) + : I.ident + = match i with + | V.Idx i -> i.it + | V.Var v -> lookup_cd ctx s v + | V.Export (s', i, ns) -> + let sort_eq a b = match a.it, b.it with + | CoreSort aa, CoreSort bb -> aa.it = bb.it + | _, _ -> a.it = b.it in + if not (sort_eq s' s) then + Putil.error s'.at ("sort_idx: export: " ^ name_of_sort s' + ^ " != " ^ name_of_sort s); + let rgn = Putil.span_regions s'.at (List.hd (List.rev ns)).at in + let if_core core noncore = match s'.it with + | CoreSort _ -> core + | _ -> noncore + in + let i_sort = + if_core (CoreSort (Core_instance @@ rgn) @@ rgn) (Instance @@ rgn) in + let i' = desugar_ident_cd ctx i_sort i in + let go i s'' n = + let target = + if_core (I.Alias_core_export (i, n)) (I.Alias_export (i, n)) in + ctx.desugar_defs_pre <- + DD_cd (I.Instance_alias ({ I.a_target = target @@ rgn + ; I.a_sort = s'' } @@ rgn) + @@ rgn)::ctx.desugar_defs_pre; + anon ctx s'' 1l + in + let rec go' i ns = match ns with + | [] -> Putil.error s.at "sort_idx: export: no names" + | [n] -> go i s' n + | n::ns -> let i' = go i i_sort n in go' i' ns + in go' i' ns + | _ -> Putil.error s.at "ident: unexpected inline instance" + +let desugar_sort_idx' (ctx : definition_ctx) (sc : V.sort_idx') + : I.sort_idx' + = { I.s_sort = sc.V.s_sort + ; I.s_idx = desugar_ident ctx sc.V.s_sort sc.V.s_idx } +let desugar_sort_idx (ctx : definition_ctx) : V.sort_idx -> I.sort_idx + = atmap (desugar_sort_idx' ctx) +let desugar_core_sort_idx' (ctx : definition_ctx) (sc : V.core_sort_idx') + = { I.c_s_sort = sc.V.c_s_sort + ; I.c_s_idx = desugar_ident ctx + (CoreSort sc.V.c_s_sort @@ sc.V.c_s_sort.at) + sc.V.c_s_idx } +let desugar_core_sort_idx (ctx : definition_ctx) + : V.core_sort_idx -> I.core_sort_idx + = atmap (desugar_core_sort_idx' ctx) + +let desugar_core_export' (ctx : definition_ctx) (ce : V.core_export') + : I.core_export' + = { I.c_e_name = ce.V.c_e_name + ; I.c_e_value = desugar_core_sort_idx ctx ce.V.c_e_value } +let desugar_core_export (ctx : definition_ctx) + : V.core_export -> I.core_export + = atmap (desugar_core_export' ctx) + +let desugar_core_instantiate_arg_inline_instance + (ctx : definition_ctx) (es : V.core_export list) + : I.core_sort_idx + = let at = Putil.span_regions (List.hd es).at (List.hd (List.rev es)).at in + let es' = List.map (desugar_core_export ctx) es in + ctx.desugar_defs_pre <- + DD_def (I.CoreDef (I.CoreInstanceDef (I.Core_instantiate_inline es' @@ at)) + @@ at)::ctx.desugar_defs_pre; + let cs = Core_instance @@ at in + { I.c_s_sort = cs + ; I.c_s_idx = anon ctx (CoreSort cs @@ at) 1l } @@ at +let desugar_core_instantiate_arg' (ctx : definition_ctx) + (ia : V.core_instantiate_arg') + : I.core_instantiate_arg' + = { I.c_ia_name = ia.V.c_ia_name + ; I.c_ia_value = match ia.V.c_ia_value.it.V.c_s_idx with + | V.CoreInlineInstance es -> + desugar_core_instantiate_arg_inline_instance ctx es + | _ -> desugar_core_sort_idx ctx ia.V.c_ia_value } +let desugar_core_instantiate_arg (ctx : definition_ctx) + : V.core_instantiate_arg -> I.core_instantiate_arg + = atmap (desugar_core_instantiate_arg' ctx) +let desugar_core_instance_expr' + (ctx : definition_ctx) (ie : V.core_instance_expr') at + : I.core_instance_expr' + = match ie with + | V.Core_instantiate_module (mid, args) -> + I.Core_instantiate_module + ( desugar_ident ctx (CoreSort (Core_module @@ at) @@ at) mid + , List.map (desugar_core_instantiate_arg ctx) args) + | V.Core_instantiate_inline es -> + I.Core_instantiate_inline (List.map (desugar_core_export ctx) es) +let desugar_core_instance_expr (ctx : definition_ctx) + : V.core_instance_expr -> I.core_instance_expr + = atmap' (desugar_core_instance_expr' ctx) + +let collect_core_space_binders at (cspace : Wasm.ParseUtil.space) : var list + = List.map (fun (x, y) -> x @@ at) + (Wasm.ParseUtil.VarMap.bindings cspace.Wasm.ParseUtil.map) +let collect_core_binders at (cctx : Wasm.ParseUtil.context) : var list + = let open Wasm.ParseUtil in + List.concat_map (collect_core_space_binders at) + [cctx.types.space; cctx.tables; cctx.memories; + cctx.funcs; cctx.locals; cctx.globals; + cctx.datas; cctx.elems] +let core_ctx_for_ctx (ctx : core_module_decl_ctx) + : CoreCtx.context + = let index_functypes = fun i d -> + match d.it with + | I.Core_deftype__deftype cd -> + (match cd.it with + | I.Core_deftype_functype ft -> Some (i, ft)) + | _ -> None in + let indexed_functypes = + List.mapi (fun i' (i, d) -> (i, i', d)) + (List.filter_map (fun x -> x) + (List.mapi index_functypes ctx.core_ctx.core_types.ct_list)) in + let new_map = VarMap.filter_map + (fun n i -> + Option.map (fun (_, i', _) -> Int32.of_int i') + (List.find_opt (fun (i', _, _) -> Int32.to_int i == i') + indexed_functypes)) + ctx.core_ctx.core_types.ct_space.map in + let open CoreCtx in + { (empty_context ()) + with CoreCtx.types = + { space = { map = new_map + ; count = Int32.of_int (List.length indexed_functypes) + } + ; list = List.map (fun (_, _, d) -> d) indexed_functypes + } + } +let desugar_core_externdesc (ctx : core_module_decl_ctx) + (id : V.core_externdesc) at + : I.core_externdesc * V.binder + = let cctx = core_ctx_for_ctx ctx in + let id' = id cctx () in + let binder = match collect_core_binders at cctx with + | [] -> V.No_binder + | [v] -> V.Var_binder v + | _ -> Putil.error at "Too many core binders" in + ((cctx, id'), binder) +let desugar_core_importdecl' (ctx : core_module_decl_ctx) + (id : V.core_importdecl') at + : I.core_importdecl' * V.binder + = let x, b = desugar_core_externdesc ctx id.V.c_id_ty at in + { I.c_id_name1 = id.V.c_id_name1 + ; I.c_id_name2 = id.V.c_id_name2 + ; I.c_id_ty = x }, b +let desugar_core_importdecl (ctx : core_module_decl_ctx) + (id : V.core_importdecl) + : I.core_importdecl * V.binder + = let x, b = desugar_core_importdecl' ctx id.it id.at in + { it = x; at = id.at }, b +let desugar_core_deftype' (ctx : 'a ctx) (t : V.core_deftype') + : I.core_deftype' + = match t with + | V.Core_deftype_functype ft -> I.Core_deftype_functype ft +let desugar_core_deftype (ctx : 'a ctx) + : V.core_deftype -> I.core_deftype + = atmap (desugar_core_deftype' ctx) +let core_id_to_sort (cid : Wasm.Ast.import_desc) : sort + = let open Wasm.Ast in + CoreSort ((match cid.it with + | FuncImport _ -> Core_func + | TableImport _ -> Core_table + | MemoryImport _ -> Core_memory + | GlobalImport _ -> Core_global) @@ cid.at) @@ cid.at +let desugar_core_alias_target' (ctx : core_module_decl_ctx) sort + (t : V.core_alias_target') at : I.core_alias_target' + = match t with + | V.Core_alias_export (id, name) -> + I.Core_alias_export ( desugar_ident_cmd ctx + (CoreSort (Core_instance @@ at) @@ at) id + , name) + | V.Core_alias_outer (oi, ident) -> + let oin = match oi with + | V.Idx i -> i.it + | V.Var v -> find_parent_index ctx v + | _ -> Putil.error at "Inadmissible outer index" in + let idx = match ident with + | V.Idx i -> i.it + | V.Var v -> raw_lookup_n ctx (Int32.to_int oin) (CoreSort sort @@ at) v + | _ -> Putil.error at "Inadmissible index" in + I.Core_alias_outer (oin, idx) +let desugar_core_alias_target (ctx : core_module_decl_ctx) sort + : V.core_alias_target -> I.core_alias_target + = atmap' (desugar_core_alias_target' ctx sort) +let desugar_core_alias' (ctx : core_module_decl_ctx) (a : V.core_alias') + : I.core_alias' + = { I.c_a_target = desugar_core_alias_target ctx a.V.c_a_sort a.V.c_a_target + ; I.c_a_sort = a.V.c_a_sort } +let desugar_core_alias (ctx : core_module_decl_ctx) + : V.core_alias -> I.core_alias + = atmap (desugar_core_alias' ctx) +let desugar_core_exportdecl' (ctx : core_module_decl_ctx) + (d : V.core_exportdecl') at : I.core_exportdecl' + = { I.c_ed_name = d.V.c_ed_name + ; I.c_ed_ty = fst (desugar_core_externdesc ctx d.V.c_ed_ty at) } +let desugar_core_exportdecl (ctx : core_module_decl_ctx) + : V.core_exportdecl -> I.core_exportdecl + = atmap' (desugar_core_exportdecl' ctx) +let desugar_core_moduledecl' (ctx : core_module_decl_ctx) + (d : V.core_moduledecl') + : I.core_moduledecl' + = match d with + | V.Core_md_importdecl i -> + let id, b = desugar_core_importdecl ctx i in + bind_NE ctx (core_id_to_sort (snd id.it.I.c_id_ty)) b; + I.Core_md_importdecl id + | V.Core_md_typedecl bt -> + let dt = desugar_core_deftype ctx bt.V.body in + bind_core_type_NE ctx bt.V.binder (I.Core_deftype__deftype dt @@ dt.at); + I.Core_md_typedecl dt + | V.Core_md_aliasdecl ba -> + let a = desugar_core_alias ctx ba.V.body in + bind_NE ctx (CoreSort a.it.I.c_a_sort @@ a.at) ba.V.binder; + I.Core_md_aliasdecl a + | V.Core_md_exportdecl e -> + let e' = desugar_core_exportdecl ctx e in + I.Core_md_exportdecl e' +let desugar_core_moduledecl (ctx : core_module_decl_ctx) + : V.core_moduledecl -> I.core_moduledecl + = atmap (desugar_core_moduledecl' ctx) +let rec desugar_core_moduledecls (ctx : core_module_decl_ctx) + (ds : V.core_moduledecl list) + : I.core_moduledecl list + = match ds with + | [] -> [] + | d ::ds -> + let d' = desugar_core_moduledecl ctx d in + let dpres = List.map from_cmd_dd (List.rev ctx.desugar_defs_pre) in + let dposts = List.map from_cmd_dd ctx.desugar_defs_post in + ctx.desugar_defs_pre <- []; + ctx.desugar_defs_post <- []; + dpres @ (d' :: dposts @ desugar_core_moduledecls ctx ds) +let desugar_core_moduletype' (ctx : 'a ctx) (t : V.core_moduletype') + : I.core_moduletype' + = { I.decls = desugar_core_moduledecls (new_ctx (SC ctx) None) t.V.decls } +let desugar_core_moduletype (ctx : 'a ctx) + : V.core_moduletype -> I.core_moduletype + = atmap (desugar_core_moduletype' ctx) +let desugar_core_deftype_' (ctx : definition_ctx) (t : V.core_deftype_') + : I.core_deftype_' + = match t with + | V.Core_deftype__deftype t -> + I.Core_deftype__deftype (desugar_core_deftype ctx t) + | V.Core_deftype__moduletype t -> + I.Core_deftype__moduletype (desugar_core_moduletype ctx t) +let desugar_core_deftype_ (ctx : definition_ctx) + : V.core_deftype_ -> I.core_deftype_ + = atmap (desugar_core_deftype_' ctx) + +let desugar_core_definition + (ctx : definition_ctx) (def : V.core_definition) at + : I.core_definition + = match def with + | V.CoreModuleDef bm -> + bind ctx (CoreSort (Core_module @@ at) @@ at) bm.V.binder; + I.CoreModuleDef bm.V.body + | V.CoreInstanceDef bi -> + let ie = desugar_core_instance_expr ctx bi.V.body in + bind ctx (CoreSort (Core_instance @@ at) @@ at) bi.V.binder; + I.CoreInstanceDef ie + | V.CoreTypeDef bt -> + let dt = desugar_core_deftype_ ctx bt.V.body in + bind_core_type ctx bt.V.binder dt; + I.CoreTypeDef dt + +let desugar_inline_export' (ctx : definition_ctx) (e : V.inline_export') + : I.inline_export' + = { I.ie_name = e.V.ie_name + ; I.ie_value = desugar_sort_idx ctx e.V.ie_value } +let desugar_inline_export (ctx : definition_ctx) + : V.inline_export -> I.inline_export + = atmap (desugar_inline_export' ctx) + +let inline_export'_to_export' (e : I.inline_export') : I.export' + = { I.e_name = e.I.ie_name + ; I.e_value = e.I.ie_value + ; I.e_type = None } +let inline_export_to_export : I.inline_export -> I.export + = atmap inline_export'_to_export' + +let desugar_instantiate_arg_inline_instance + (ctx : definition_ctx) (es : V.inline_export list) + : I.sort_idx + = let at = Putil.span_regions (List.hd es).at (List.hd (List.rev es)).at in + let es' = List.map (desugar_inline_export ctx) es in + ctx.desugar_defs_pre <- + DD_def (I.InstanceDef (I.Instantiate_inline es' @@ at) @@ at) + ::ctx.desugar_defs_pre; + { I.s_sort = Instance @@ at + ; I.s_idx = anon ctx (Instance @@ at) 1l } @@ at +let desugar_instantiate_arg' (ctx : definition_ctx) (ia : V.instantiate_arg') + : I.instantiate_arg' + = { I.ia_name = ia.V.ia_name + ; I.ia_value = match ia.V.ia_value.it.V.s_idx with + | V.InlineInstance es -> + desugar_instantiate_arg_inline_instance ctx es + | _ -> desugar_sort_idx ctx ia.V.ia_value } +let desugar_instantiate_arg (ctx : definition_ctx) + : V.instantiate_arg -> I.instantiate_arg + = atmap (desugar_instantiate_arg' ctx) +let desugar_instance_expr' (ctx : definition_ctx) (ie : V.instance_expr') at + : I.instance_expr' + = match ie with + | V.Instantiate_component (cid, args) -> + I.Instantiate_component + ( desugar_ident ctx (Component @@ at) cid + , List.map (desugar_instantiate_arg ctx) args) + | V.Instantiate_inline es -> + I.Instantiate_inline (List.map (desugar_inline_export ctx) es) +let desugar_instance_expr (ctx : definition_ctx) + : V.instance_expr -> I.instance_expr + = atmap' (desugar_instance_expr' ctx) + +let desugar_alias_target' + (ctx : 'a ctx) (desugar_ident : 'a ctx -> sort -> V.ident -> I.ident) + sort (t : V.alias_target') at + : I.alias_target' + = match t with + | V.Alias_export (id, name) -> + I.Alias_export ( desugar_ident ctx (Instance @@ at) id + , name) + | V.Alias_core_export (id, name) -> + I.Alias_core_export ( desugar_ident ctx + (CoreSort (Core_instance @@ at) @@ at) id + , name) + | V.Alias_outer (oi, ident) -> + let oin = match oi with + | V.Idx i -> i.it + | V.Var v -> find_parent_index ctx v + | _ -> Putil.error at "Inadmissible outer index" in + let idx = match ident with + | V.Idx i -> i.it + | V.Var v -> raw_lookup_n ctx (Int32.to_int oin) sort v + | _ -> Putil.error at "Inadmissible index" in + I.Alias_outer (oin, idx) +let desugar_alias_target + (ctx : 'a ctx) (desugar_ident : 'a ctx -> sort -> V.ident -> I.ident) sort + : V.alias_target -> I.alias_target + = atmap' (desugar_alias_target' ctx desugar_ident sort) +let desugar_alias' ctx desugar_ident (a : V.alias') + : I.alias' + = { I.a_target = desugar_alias_target ctx desugar_ident + a.V.a_sort a.V.a_target + ; I.a_sort = a.V.a_sort } +let desugar_alias + (ctx : 'a ctx) (desugar_ident : 'a ctx -> sort -> V.ident -> I.ident) + : V.alias -> I.alias + = atmap (desugar_alias' ctx desugar_ident) + +type 'a desugar_type_params = + { _desugar_ident : 'a ctx -> sort -> V.ident -> I.ident + ; _deinline_type : 'a ctx -> I.def_type -> I.ident + } +let desugar_type_params_def : ctx_for_definition desugar_type_params + = { _desugar_ident = desugar_ident + ; _deinline_type = + fun ctx t -> + ctx.desugar_defs_pre <- + DD_def (I.TypeDef t @@ no_region)::ctx.desugar_defs_pre; + let type_idx = ctx.types.count in + bind_type_ bind_export_no ctx V.No_binder t; + (*print_endline ("debug: deinline_type: " ^ string_of_region t.at + ^ " = " ^ Int32.to_string type_idx);*) + type_idx (* hack *) + } +let desugar_type_params_decl : ctx_for_component_decl desugar_type_params + = { _desugar_ident = desugar_ident_cd + ; _deinline_type = + fun ctx t -> + ctx.desugar_defs_pre <- + DD_cd (I.Instance_type t @@ no_region)::ctx.desugar_defs_pre; + let type_idx = ctx.types.count in + bind_type_ bind_export_no ctx V.No_binder t; + type_idx (* hack *) + } + +let rec desugar_record_field' (ctx : 'a ctx) (params : 'a desugar_type_params) + (rf : V.record_field') at + : I.record_field' + = { I.rf_name = rf.V.rf_name + ; I.rf_type = desugar_val_type ctx params at rf.V.rf_type } +and desugar_record_field (ctx : 'a ctx) (params : 'a desugar_type_params) + : V.record_field -> I.record_field + = atmap' (desugar_record_field' ctx params) +and desugar_variant_case' (ctx : 'a ctx) (params : 'a desugar_type_params) + vcs (vc : V.variant_case') at + : I.variant_case' + = { I.vc_name = vc.V.vc_name + ; I.vc_type = Option.map (desugar_val_type ctx params at) vc.V.vc_type + ; I.vc_default = + match vc.V.vc_default with + | None -> None + | Some (V.Idx i) -> Some i.it + | Some (V.Var v) -> + let ivcs = List.mapi (fun i a -> (i, a)) vcs in + let (i, _) = List.find (fun (i, vc) -> + match vc.V.binder with + | V.Var_binder v' -> v'.it = v.it + | _ -> false) ivcs in + Some (Int32.of_int i) + | Some _ -> Putil.error at "Default must be index or var" + } +and desugar_variant_case (ctx : 'a ctx) (params : 'a desugar_type_params) vcs + : V.variant_case V.bound -> I.variant_case + = fun vc -> atmap' (desugar_variant_case' ctx params vcs) vc.V.body +and desugar_def_val_type' (ctx : 'a ctx) (params : 'a desugar_type_params) + (t : V.def_val_type') at + : I.def_val_type' + = match t with + | V.Record rfs -> I.Record (List.map (desugar_record_field ctx params) rfs) + | V.Variant vcs -> I.Variant (List.map (desugar_variant_case ctx params vcs) vcs) + | V.List vt -> I.List (desugar_val_type ctx params at vt) + | V.Tuple vts -> I.Tuple (List.map (desugar_val_type ctx params at) vts) + | V.Flags ns -> I.Flags ns + | V.Enum ns -> I.Enum ns + | V.Union vts -> I.Union (List.map (desugar_val_type ctx params at) vts) + | V.Option vt -> I.Option (desugar_val_type ctx params at vt) + | V.Expected (vt1, vt2) -> + I.Expected ( Option.map (desugar_val_type ctx params at) vt1 + , Option.map (desugar_val_type ctx params at) vt2) + | V.Own v -> (match v with + | V.Idx _ | V.Var _ -> + I.Own (params._desugar_ident ctx (Type @@ at) v) + | _ -> Putil.error at "Resource type must be var or index") + | V.Borrow v -> (match v with + | V.Idx _ | V.Var _ -> + I.Borrow (params._desugar_ident ctx (Type @@ at) v) + | _ -> Putil.error at "Resource type must be var or index") + | V.Bool -> I.Bool + | V.Signed i -> I.Signed i + | V.Unsigned i -> I.Unsigned i + | V.Float f -> I.Float f + | V.Char -> I.Char + | V.String -> I.String +and desugar_def_val_type ctx params + : V.def_val_type -> I.def_val_type + = atmap' (desugar_def_val_type' ctx params) +and desugar_val_type (ctx : 'a ctx) (params : 'a desugar_type_params) at + (vt : V.val_type) + : I.val_type + = match vt with + | V.TVar id -> params._desugar_ident ctx (Type @@ at) id + | V.TInline t -> let t' = desugar_def_val_type ctx params t in + params._deinline_type ctx (I.Deftype_val t' @@ t'.at) +let desugar_func_ios' (ctx : 'a ctx) (params : 'a desugar_type_params) + (io : V.func_ios') at : I.func_ios' + = match io with + | V.Fio_one vt -> I.Fio_one (desugar_val_type ctx params at vt) + | V.Fio_many nts -> + I.Fio_many (List.map (fun (n, vt) -> + (n, desugar_val_type ctx params at vt)) nts) +let desugar_func_ios (ctx : 'a ctx) (params : 'a desugar_type_params) + : V.func_ios -> I.func_ios + = atmap' (desugar_func_ios' ctx params) +let desugar_func_type' ctx params + (ft : V.func_type') : I.func_type' + = { I.ft_params = desugar_func_ios ctx params ft.V.ft_params + ; I.ft_result = desugar_func_ios ctx params ft.V.ft_result } +let desugar_func_type ctx params + : V.func_type -> I.func_type + = atmap (desugar_func_type' ctx params) +let rec desugar_type_decls + (ctx : 'c ctx) + (desugar_decl : 'c ctx -> 'a -> 'b) + (from_dd : 'c desugar_def -> 'b) + (decls : 'a list) + = match decls with + | [] -> [] + | d::ds -> + let d' = desugar_decl ctx d in + let dpres = List.map from_dd (List.rev ctx.desugar_defs_pre) in + let dposts = List.map from_dd ctx.desugar_defs_post in + ctx.desugar_defs_pre <- []; + ctx.desugar_defs_post <- []; + dpres @ (d' :: dposts @ desugar_type_decls ctx desugar_decl from_dd ds) +let exportdesc_to_sort ed + = match ed.it with + | I.Export_sort_id (s, _) -> s + | I.Export_core_mod _ -> CoreSort (Core_module @@ ed.at) @@ ed.at + | I.Export_func _ -> Func @@ ed.at + | I.Export_comp _ -> Component @@ ed.at + | I.Export_inst _ -> Instance @@ ed.at + | I.Export_val _-> Value @@ ed.at + | I.Export_type _ -> Type @@ ed.at +let rec desugar_def_type_typeuse ctx params at dt + = match dt with + | V.TVar id -> params._desugar_ident ctx (Type @@ at) id + | V.TInline t -> let t' = desugar_def_type ctx params None t in + params._deinline_type ctx t' +and desugar_type_bound' ctx params (tc : V.type_bound') at : I.type_bound' + = match tc with + | V.Tbound_subr -> I.Tbound_subr + | V.Tbound_eq dt -> I.Tbound_eq (desugar_def_type_typeuse ctx params at dt) +and desugar_type_bound ctx params (tb : V.type_bound) : I.type_bound + = atmap' (desugar_type_bound' ctx params) tb +and desugar_exportdesc' ctx params name (ed : V.exportdesc') at : I.exportdesc' + = match ed with + | V.Export_sort_id (s, id) -> + I.Export_sort_id (s, params._desugar_ident ctx (Type @@ at) id) + | V.Export_core_mod cmt -> + I.Export_core_mod (desugar_core_moduletype ctx cmt) + | V.Export_func ft -> + I.Export_func (desugar_func_type ctx params ft) + | V.Export_comp ct -> + I.Export_comp (desugar_component_type ctx params name ct) + | V.Export_inst it -> + I.Export_inst (desugar_instance_type ctx params name it) + | V.Export_val vt -> + I.Export_val (desugar_val_type ctx params at vt) + | V.Export_type tb -> + I.Export_type (desugar_type_bound ctx params tb) +and desugar_exportdesc + : 'c. 'c ctx -> 'c desugar_type_params -> var option + -> V.exportdesc -> I.exportdesc + = fun ctx params name -> atmap' (desugar_exportdesc' ctx params name) +and desugar_export_decl' ctx params (ed : V.exportdecl') + : I.exportdecl' * V.binder + = { I.ed_name = ed.V.ed_name + ; I.ed_type = desugar_exportdesc ctx params + (to_outer_name ed.V.ed_type.V.binder) ed.V.ed_type.V.body }, + ed.V.ed_type.V.binder +and desugar_export_decl ctx params (ed : V.exportdecl) + : I.exportdecl * V.binder + = let ed', x = desugar_export_decl' ctx params ed.it in + { at = ed.at; it = ed' }, x +and desugar_instance_decl' + = fun ctx params decl -> + match decl with + | V.Instance_type bdt -> + let t' = desugar_def_type ctx params + (to_outer_name bdt.V.binder) bdt.V.body in + bind_type_NE ctx bdt.V.binder t'; + I.Instance_type t' + | V.Instance_alias ba -> + let a = desugar_alias ctx params._desugar_ident ba.V.body in + bind_NE ctx ba.V.body.it.V.a_sort ba.V.binder; + I.Instance_alias a + | V.Instance_export ed -> + let ed', b = desugar_export_decl ctx params ed in + (match ed.it.V.ed_type.V.body.it, b with + | V.Export_type _, x -> bind_NE ctx (Type @@ ed.at) x + | _, V.No_binder -> () + | _, _ -> Putil.error ed.at "Binder not allowed on non-type export"); + I.Instance_export ed' +and desugar_instance_decl (ctx : component_decl_ctx) params + : V.instance_decl -> I.instance_decl + = atmap (desugar_instance_decl' ctx params) +and desugar_instance_type' ctx params name + : V.instance_decl list -> I.instance_decl list + = desugar_type_decls + (new_ctx (SC ctx) name) + (fun c d -> desugar_instance_decl c desugar_type_params_decl d) + from_cd_dd_i +and desugar_instance_type + : 'c. 'c ctx -> 'c desugar_type_params -> var option + -> V.instance_type -> I.instance_type + = fun ctx params name -> atmap (desugar_instance_type' ctx params name) +and desugar_import_decl' ctx params (id : V.importdecl') + : I.importdecl' * V.binder + = { I.id_name = id.V.id_name + ; I.id_type = desugar_exportdesc ctx params + (to_outer_name id.V.id_type.V.binder) id.V.id_type.V.body }, + id.V.id_type.V.binder +and desugar_import_decl ctx params (id : V.importdecl) + : I.importdecl * V.binder + = let id', x = desugar_import_decl' ctx params id.it in + { at = id.at; it = id' }, x +and desugar_component_decl' ctx params (decl : V.component_decl') + : I.component_decl' + = match decl with + | V.Component_import id -> + let id', b = desugar_import_decl ctx params id in + bind_NE ctx (exportdesc_to_sort id'.it.I.id_type) b; + I.Component_import id' + | V.Component_instance id -> + I.Component_instance (desugar_instance_decl ctx params id) +and desugar_component_decl ctx params + : V.component_decl -> I.component_decl + = atmap (desugar_component_decl' ctx params) +and desugar_component_type' ctx params name + : V.component_decl list -> I.component_decl list + = desugar_type_decls + (new_ctx (SC ctx) name) + (fun c d -> desugar_component_decl c desugar_type_params_decl d) + from_cd_dd +and desugar_component_type + : 'c. 'c ctx -> 'c desugar_type_params -> var option + -> V.component_type -> I.component_type + = fun ctx params name -> atmap (desugar_component_type' ctx params name) +and desugar_def_type' ctx params name (dt : V.def_type') at + : I.def_type' + = match dt with + | V.Deftype_val dvt -> + I.Deftype_val (desugar_def_val_type ctx params dvt) + | V.Deftype_func ft -> + I.Deftype_func (desugar_func_type ctx params ft) + | V.Deftype_comp ct -> + I.Deftype_comp (desugar_component_type ctx params name ct) + | V.Deftype_inst it -> + I.Deftype_inst (desugar_instance_type ctx params name it) + | V.Deftype_rsrc fi -> + I.Deftype_rsrc (Option.map (params._desugar_ident ctx (Func @@ at)) fi) +and desugar_def_type + : 'c. 'c ctx -> 'c desugar_type_params -> var option + -> V.def_type -> I.def_type + = fun ctx params name -> atmap' (desugar_def_type' ctx params name) + +let desugar_canon_opt' ctx (o : V.canon_opt') at : I.canon_opt' + = match o with + | V.String_utf8 -> I.String_utf8 + | V.String_utf16 -> I.String_utf16 + | V.String_latin1_utf16 -> I.String_latin1_utf16 + | V.Memory cmid -> + I.Memory (desugar_ident ctx (CoreSort (Core_memory @@ at) @@ at) cmid) + | V.Realloc cfid -> + I.Realloc (desugar_ident ctx (CoreSort (Core_func @@ at) @@ at) cfid) + | V.PostReturn cfid -> + I.PostReturn (desugar_ident ctx (CoreSort (Core_func @@ at) @@ at) cfid) +let desugar_canon_opt ctx : V.canon_opt -> I.canon_opt + = atmap' (desugar_canon_opt' ctx) +let desugar_canon' ctx (d : V.canon') at : I.canon' + = match d with + | V.Canon_lift (cfid, ed, opts) -> + let cfid' = desugar_ident ctx (CoreSort (Core_func @@ at) @@ at) cfid in + let ed' = desugar_exportdesc ctx desugar_type_params_def None ed in + let opts' = List.map (desugar_canon_opt ctx) opts in + I.Canon_lift (cfid', ed', opts') + | V.Canon_lower (fid, opts) -> + let fid' = desugar_ident ctx (Func @@ at) fid in + let opts' = List.map (desugar_canon_opt ctx) opts in + I.Canon_lower (fid', opts') + | V.Canon_resource_builtin { it = V.CRB_new dt; _ } -> + let dt' = desugar_def_type_typeuse ctx desugar_type_params_def at dt in + I.Canon_resource_builtin (I.CRB_new dt' @@ at) + | V.Canon_resource_builtin { it = V.CRB_drop vt; _ } -> + let vt' = desugar_val_type ctx desugar_type_params_def at vt in + I.Canon_resource_builtin (I.CRB_drop vt' @@at) + | V.Canon_resource_builtin { it = V.CRB_rep dt; _ } -> + let dt' = desugar_def_type_typeuse ctx desugar_type_params_def at dt in + I.Canon_resource_builtin (I.CRB_rep dt' @@ at) +let desugar_canon ctx : V.canon -> I.canon + = atmap' (desugar_canon' ctx) + +let desugar_start' ctx (s : V.start') at : I.start' * unit V.bound list + = { I.s_func = desugar_ident ctx (Func @@ at) s.V.s_func + ; I.s_params = List.map (desugar_ident ctx (Value @@ at)) s.V.s_params + ; I.s_result = List.map (fun v -> v.V.body) s.V.s_result }, s.V.s_result +let desugar_start ctx (s : V.start) : I.start * unit V.bound list + = let s', bs = desugar_start' ctx s.it s.at in + { it = s'; at = s.at }, bs + +let desugar_import' ctx (i : V.import') : I.import' * V.binder + = { I.i_name = i.V.i_name + ; I.i_type = desugar_exportdesc ctx desugar_type_params_def + (to_outer_name i.V.i_type.V.binder) i.V.i_type.V.body }, + i.V.i_type.V.binder +let desugar_import ctx (i : V.import) : I.import * V.binder + = let i', b = desugar_import' ctx i.it in + { it = i'; at = i.at }, b + +let desugar_export' ctx (e : V.export') : I.export' + = { I.e_name = e.V.e_name + ; I.e_value = desugar_sort_idx ctx e.V.e_value + ; I.e_type = Option.map (desugar_exportdesc ctx desugar_type_params_def None) e.V.e_type} +let desugar_export ctx : V.export -> I.export + = atmap (desugar_export' ctx) + +let rec desugar_definition' (ctx : definition_ctx) (def : V.definition') at + : I.definition' + = match def with + | V.CoreDef c -> I.CoreDef (desugar_core_definition ctx c at) + | V.ComponentDef c -> + let dc = _desugar_component (SC ctx) c in + bind ctx (Component @@ c.at) c.it.V.binder; + I.ComponentDef dc + | V.InstanceDef bi -> + let ie = desugar_instance_expr ctx bi.V.body in + bind ctx (Instance @@ at) bi.V.binder; + I.InstanceDef ie + | V.AliasDef ba -> + let a = desugar_alias ctx desugar_ident ba.V.body in + bind ctx ba.V.body.it.V.a_sort ba.V.binder; + I.AliasDef a + | V.TypeDef dt -> + let dt' = desugar_def_type ctx desugar_type_params_def + (to_outer_name dt.V.binder) dt.V.body in + bind_type ctx dt.V.binder dt'; + I.TypeDef dt' + | V.CanonDef bc -> + let c = desugar_canon ctx bc.V.body in + let sort = match c.it with + | I.Canon_lift _ -> Func @@ c.at + | I.Canon_lower _ -> CoreSort (Core_func @@ c.at) @@ c.at + | I.Canon_resource_builtin _ -> CoreSort (Core_func @@ c.at) @@ c.at in + bind ctx sort bc.V.binder; + I.CanonDef c + | V.StartDef s -> + let s', bs = desugar_start ctx s in + ignore (List.map (fun b -> bind ctx (Value @@ s'.at) b.V.binder) bs); + I.StartDef s' + | V.ImportDef i -> + let i', b = desugar_import ctx i in + bind ctx (exportdesc_to_sort i'.it.I.i_type) b; + I.ImportDef i' + | V.ExportDef be -> + let e' = desugar_export ctx be.V.body in + bind ctx (e'.it.I.e_value.it.I.s_sort) be.V.binder; + I.ExportDef e' +and desugar_definition (ctx : definition_ctx) : V.definition -> I.definition + = atmap' (desugar_definition' ctx) + +and desugar_definitions (ctx : definition_ctx) (defs : V.definition list) + : I.definition list + = match defs with + | [] -> [] + | d::ds -> + let d' = desugar_definition ctx d in + let dpres = List.map from_def_dd (List.rev ctx.desugar_defs_pre) in + let dposts = List.map from_def_dd ctx.desugar_defs_post in + ctx.desugar_defs_pre <- []; + ctx.desugar_defs_post <- []; + dpres @ (d' :: dposts @ desugar_definitions ctx ds) + +and _desugar_component' (ctx : some_ctx) (c : V.component' V.bound) at + : I.component' + = { I.defns = desugar_definitions + (new_ctx ctx (match c.V.binder with + | V.No_binder -> None + | V.Var_binder v -> Some v + | V.Export_binders _ -> Putil.error at "bad")) + c.V.body.V.defns; } +and _desugar_component (ctx : some_ctx) : V.component -> I.component + = atmap' (fun c -> _desugar_component' ctx c) + +let desugar_component c = _desugar_component (SC (empty_ctx () None)) c diff --git a/interpreter/text/dune b/interpreter/text/dune new file mode 100644 index 00000000..08ce0647 --- /dev/null +++ b/interpreter/text/dune @@ -0,0 +1,9 @@ +(menhir (modules parser) (flags --table --inspection --explain)) + +(rule + (target lexer.ml) + ; NOTE(dbp 2021-10-12): I don't know of a way to depend on a package... + ; (deps lexer.mll) + (deps lexer.mll) + (action (chdir %{workspace_root} + (run %{bin:ocamllex} -ml -q -o %{target} %{deps})))) diff --git a/interpreter/text/lexer.mli b/interpreter/text/lexer.mli new file mode 100644 index 00000000..93538f31 --- /dev/null +++ b/interpreter/text/lexer.mli @@ -0,0 +1 @@ +val token : Lexing.lexbuf -> Parser.token (* raises Source.Error *) diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll new file mode 100644 index 00000000..0dfe2861 --- /dev/null +++ b/interpreter/text/lexer.mll @@ -0,0 +1,197 @@ +{ +open Parser +open Putil + +let error lexbuf msg = raise (Script.Syntax (region lexbuf, msg)) +let error_nest start lexbuf msg = + lexbuf.Lexing.lex_start_p <- start; + error lexbuf msg + +let string s = + let b = Buffer.create (String.length s) in + let i = ref 1 in + while !i < String.length s - 1 do + let c = if s.[!i] <> '\\' then s.[!i] else + match (incr i; s.[!i]) with + | 'n' -> '\n' + | 'r' -> '\r' + | 't' -> '\t' + | '\\' -> '\\' + | '\'' -> '\'' + | '\"' -> '\"' + | 'u' -> + let j = !i + 2 in + i := String.index_from s j '}'; + let n = int_of_string ("0x" ^ String.sub s j (!i - j)) in + let bs = Wasm.Utf8.encode [n] in + Buffer.add_substring b bs 0 (String.length bs - 1); + bs.[String.length bs - 1] + | h -> + incr i; + Char.chr (int_of_string ("0x" ^ String.make 1 h ^ String.make 1 s.[!i])) + in Buffer.add_char b c; + incr i + done; + Buffer.contents b + +} + +let sign = '+' | '-' +let digit = ['0'-'9'] +let hexdigit = ['0'-'9''a'-'f''A'-'F'] +let num = digit ('_'? digit)* +let hexnum = hexdigit ('_'? hexdigit)* + +let letter = ['a'-'z''A'-'Z'] +let symbol = + ['+''-''*''/''\\''^''~''<''>''!''?''@''#''$''%''&''|'':''`''.''\''] + +let space = [' ''\t''\n''\r'] +let ascii = ['\x00'-'\x7f'] +let ascii_no_nl = ['\x00'-'\x09''\x0b'-'\x7f'] +let utf8cont = ['\x80'-'\xbf'] +let utf8enc = + ['\xc2'-'\xdf'] utf8cont + | ['\xe0'] ['\xa0'-'\xbf'] utf8cont + | ['\xed'] ['\x80'-'\x9f'] utf8cont + | ['\xe1'-'\xec''\xee'-'\xef'] utf8cont utf8cont + | ['\xf0'] ['\x90'-'\xbf'] utf8cont utf8cont + | ['\xf4'] ['\x80'-'\x8f'] utf8cont utf8cont + | ['\xf1'-'\xf3'] utf8cont utf8cont utf8cont +let utf8 = ascii | utf8enc +let utf8_no_nl = ascii_no_nl | utf8enc + +let escape = ['n''r''t''\\''\'''\"'] +let character = + [^'"''\\''\x00'-'\x1f''\x7f'-'\xff'] + | utf8enc + | '\\'escape + | '\\'hexdigit hexdigit + | "\\u{" hexnum '}' + +let nat = num | "0x" hexnum +let int = sign nat +let frac = num +let hexfrac = hexnum +let float = + sign? num '.' frac? + | sign? num ('.' frac?)? ('e' | 'E') sign? num + | sign? "0x" hexnum '.' hexfrac? + | sign? "0x" hexnum ('.' hexfrac?)? ('p' | 'P') sign? num + | sign? "inf" + | sign? "nan" + | sign? "nan:" "0x" hexnum +let string = '"' character* '"' +let reserved = (letter | digit | '_' | symbol )+ +let name = '$' reserved + +rule token = parse + | "(" { LPAR } + | ")" { RPAR } + + | nat as s { NAT s } + | string as s { STRING (string s) } + | '"'character*('\n'|eof) { error lexbuf "unclosed string literal" } + | '"'character*['\x00'-'\x09''\x0b'-'\x1f''\x7f'] + { error lexbuf "illegal control character in string literal" } + | '"'character*'\\'_ + { error_nest (Lexing.lexeme_end_p lexbuf) lexbuf "illegal escape" } + + | "component" { COMPONENT } + | "module" { MODULE } + | "instance" { INSTANCE } + + | "core" { CORE } + + | "func" { FUNC } + | "table" { TABLE } + | "memory" { MEMORY } + | "global" { GLOBAL } + | "value" { VALUE } + | "type" { TYPE } + | "with" { WITH } + | "instantiate" { INSTANTIATE } + | "alias" { ALIAS } + + | "import" { IMPORT } + | "export" { EXPORT } + | "outer" { OUTER } + + | "bool" {BOOL } + | "s8" { SIGNED(Ast.VI_8) } + | "s16" { SIGNED(Ast.VI_16) } + | "s32" { SIGNED(Ast.VI_32) } + | "s64" { SIGNED(Ast.VI_64) } + | "u8" { UNSIGNED(Ast.VI_8) } + | "u16" { UNSIGNED(Ast.VI_16) } + | "u32" { UNSIGNED(Ast.VI_32) } + | "u64" { UNSIGNED(Ast.VI_64) } + | "i32" { I32 } + | "float32" { FLOAT(Ast.VF_32) } + | "float64" { FLOAT(Ast.VF_64) } + | "char" { CHAR } + | "string" { TSTRING } + | "record" { RECORD } + | "variant" { VARIANT } + | "list" { LIST } + | "tuple" { TUPLE } + | "flags" { FLAGS } + | "enum" { ENUM } + | "union" { UNION } + | "option" { OPTION } + | "error" { ERROR } + | "field" { FIELD } + | "case" { CASE } + | "refines" { REFINES } + | "param" { PARAM } + | "result" { RESULT } + | "own" { OWN } + | "borrow" { BORROW } + | "eq" { EQ } + | "sub" { SUB } + | "resource" { RESOURCE } + | "resource.new" { RESOURCE_NEW } + | "resource.drop" { RESOURCE_DROP } + | "resource.rep" { RESOURCE_REP } + | "rep" { REP } + | "dtor" { DTOR } + | "canon" { CANON } + | "lift" { LIFT } + | "lower" { LOWER } + | "string-encoding" { STRINGENCODING } + | "=" { EQS } + | "utf8" { UTF8 } + | "utf16" { UTF16 } + | "latin1+utf16" { LATIN1UTF16 } + | "realloc" { REALLOC } + | "post-return" { POSTRETURN } + | "start" { START } + + (* scripts *) + | "input" { INPUT } + | "binary" { BIN } + | "quote" { QUOTE } + | "assert_invalid" { ASSERT_INVALID } + | "assert_malformed" { ASSERT_MALFORMED } + + | name as s { VAR s } + + | ";;"utf8_no_nl*eof { EOF } + | ";;"utf8_no_nl*'\n' { Lexing.new_line lexbuf; token lexbuf } + | ";;"utf8_no_nl* { token lexbuf (* causes error on following position *) } + | "(;" { comment (Lexing.lexeme_start_p lexbuf) lexbuf; token lexbuf } + | space#'\n' { token lexbuf } + | '\n' { Lexing.new_line lexbuf; token lexbuf } + | eof { EOF } + + | reserved as s { error lexbuf ("unknown operator: " ^ s) } + | utf8 { error lexbuf "malformed operator" } + | _ { error lexbuf "malformed UTF-8 encoding" } + +and comment start = parse + | ";)" { () } + | "(;" { comment (Lexing.lexeme_start_p lexbuf) lexbuf; comment start lexbuf } + | '\n' { Lexing.new_line lexbuf; comment start lexbuf } + | eof { error_nest start lexbuf "unclosed comment" } + | utf8 { comment start lexbuf } + | _ { error lexbuf "malformed UTF-8 encoding" } diff --git a/interpreter/text/parse.ml b/interpreter/text/parse.ml new file mode 100644 index 00000000..c3abfb89 --- /dev/null +++ b/interpreter/text/parse.ml @@ -0,0 +1,321 @@ +open Putil + +type 'a start = + | Component : (Ast.VarAst.component perhaps_named) start + | Script : Script.script start + +exception Syntax = Wasm.Script.Syntax + +(* + + A lexbuf structure has these members: + - refill: a function which can be called to get more valid bytes + - lex_buffer: a buffer with a bunch of bytes in it + - lex_buffer_len: the index into lex_buffer of the last valid byte of data + within it + - lex_abs_pos: the absolute position in the stream of index 0 of the + lex_buffer + - lex_start_pos: the index of the first valid byte of data in lex_buffer + - lex_curr_pos: ??? index between lex_start_pos and lex_buffer_len + - lex_last_pos: ??? index between lex_start_pos and lex_buffer_len + - lex_last_action: ??? + - lex_eof_reached: + - lex_mem: ??? indices between lex_start_pos and lex_buffer_len + - lex_start_p: + - lex_curr_p: + *) + +type backtracking_lexbuf = { + bt_lexbuf : Lexing.lexbuf; + mutable replay_ptr : int option; + mutable lookahead_buffers : Lexing.lexbuf list; + } +let dummy_refill lexbuf = error (Putil.region lexbuf) "Dummy lexbuf refill!" +let copy_lexbuf lexbuf = + let open Lexing in + let newbuf = Bytes.create (Bytes.length lexbuf.lex_buffer) in + Bytes.blit lexbuf.lex_buffer 0 newbuf 0 (Bytes.length lexbuf.lex_buffer); + { lexbuf with + refill_buff = dummy_refill; + lex_buffer = newbuf; + lex_mem = Array.copy lexbuf.lex_mem; + } +let bt_lexbuf_set_lexbuf bt_lexbuf lexbuf = + let open Lexing in + bt_lexbuf.bt_lexbuf.lex_buffer <- lexbuf.lex_buffer; + bt_lexbuf.bt_lexbuf.lex_buffer_len <- lexbuf.lex_buffer_len; + bt_lexbuf.bt_lexbuf.lex_abs_pos <- lexbuf.lex_abs_pos; + bt_lexbuf.bt_lexbuf.lex_start_pos <- lexbuf.lex_start_pos; + bt_lexbuf.bt_lexbuf.lex_curr_pos <- lexbuf.lex_curr_pos; + bt_lexbuf.bt_lexbuf.lex_last_pos <- lexbuf.lex_last_pos; + bt_lexbuf.bt_lexbuf.lex_last_action <- lexbuf.lex_last_action; + bt_lexbuf.bt_lexbuf.lex_eof_reached <- lexbuf.lex_eof_reached; + bt_lexbuf.bt_lexbuf.lex_mem <- lexbuf.lex_mem; + bt_lexbuf.bt_lexbuf.lex_start_p <- lexbuf.lex_start_p; + bt_lexbuf.bt_lexbuf.lex_curr_p <- lexbuf.lex_curr_p +let rec list_drop n list = + if n = 0 then list else + match list with + | [] -> [] + | x::xs -> list_drop (n-1) xs +let bt_lexbuf_commit bt_lexbuf = + match bt_lexbuf.replay_ptr with + | None -> bt_lexbuf.lookahead_buffers <- [] + | Some ptr -> + bt_lexbuf.lookahead_buffers <- list_drop ptr bt_lexbuf.lookahead_buffers; + bt_lexbuf.replay_ptr <- Some 0 +let bt_lexbuf_mark bt_lexbuf = + bt_lexbuf_commit bt_lexbuf; + bt_lexbuf.lookahead_buffers <- + copy_lexbuf bt_lexbuf.bt_lexbuf::bt_lexbuf.lookahead_buffers; + bt_lexbuf.replay_ptr <- match bt_lexbuf.replay_ptr with + | None -> None + | Some n -> Some (n+1) +let bt_lexbuf_abort bt_lexbuf = + bt_lexbuf_set_lexbuf bt_lexbuf + (copy_lexbuf (List.hd bt_lexbuf.lookahead_buffers)); + bt_lexbuf.replay_ptr <- + if List.length bt_lexbuf.lookahead_buffers > 1 + then Some 1 + else None +let bt_lexbuf_refill bt_lexbuf orig_refill lexbuf = + match bt_lexbuf.replay_ptr with + | Some ptr -> + bt_lexbuf_set_lexbuf bt_lexbuf + (copy_lexbuf (List.nth bt_lexbuf.lookahead_buffers ptr)); + let new_ptr = ptr + 1 in + bt_lexbuf.replay_ptr <- + if new_ptr >= List.length bt_lexbuf.lookahead_buffers + then None + else Some new_ptr + | None -> + orig_refill lexbuf; + bt_lexbuf.lookahead_buffers <- + bt_lexbuf.lookahead_buffers @ [copy_lexbuf lexbuf] +let bt_lexbuf_of_lexbuf lexbuf = + let rec ret = { + bt_lexbuf = {lexbuf with + Lexing.refill_buff = + fun lexbuf' -> + bt_lexbuf_refill ret lexbuf.Lexing.refill_buff + lexbuf'}; + replay_ptr = None; + lookahead_buffers = []; + } + in ret + +let lex_core_module (lexbuf : Lexing.lexbuf) + : Lexing.position * Wasm.Script.var option * Wasm.Ast.module_ + = let lcm_status : int ref = ref 0 + and paren_depth : int ref = ref 0 + and first_pos : Lexing.position option ref = ref None in + let token' lexbuf = let tok = Wasm.Lexer.token lexbuf in + match !first_pos with + | None -> first_pos := Some lexbuf.Lexing.lex_start_p; + tok + | Some _ -> tok in + let (x, d) = + Wasm.Parser.module1 (fun lexbuf -> + if !paren_depth = 0 + then match !lcm_status with + | 0 -> lcm_status := 1; Wasm.Parser.LPAR + | 1 -> lcm_status := 2; paren_depth := 1; Wasm.Parser.MODULE + | 2 -> Wasm.Parser.EOF + | _ -> error (Putil.region lexbuf) "Impossible: bad lcm state" + else match token' lexbuf with + | Wasm.Parser.LPAR -> paren_depth := !paren_depth + 1; + Wasm.Parser.LPAR + | Wasm.Parser.RPAR -> paren_depth := !paren_depth - 1; + Wasm.Parser.RPAR + | tok -> tok) lexbuf + in match !first_pos, d.Wasm.Source.it with + | Some p, Wasm.Script.Textual m -> (p, x, m) + | _, _ -> error (Putil.region lexbuf) + "Impossible: non-Textual module or no lex" + +let lex_core_deftype (lexbuf : Lexing.lexbuf) + : Lexing.position * Wasm.Ast.type_ + = let lcm_status : int ref = ref 0 + and paren_depth : int ref = ref 0 + and first_pos : Lexing.position option ref = ref None in + let token' lexbuf = let tok = Wasm.Lexer.token lexbuf in + match !first_pos with + | None -> first_pos := Some lexbuf.Lexing.lex_start_p; + tok + | Some _ -> tok in + let prim_lex () = + match token' lexbuf with + | Wasm.Parser.LPAR -> paren_depth := !paren_depth + 1; + Wasm.Parser.LPAR + | Wasm.Parser.RPAR -> paren_depth := !paren_depth - 1; + Wasm.Parser.RPAR + | tok -> tok in + let ty = + Wasm.Parser.type_ (fun lexbuf -> + if !paren_depth = 0 + then match !lcm_status with + | 0 -> lcm_status := 1; prim_lex () + | 1 -> Wasm.Parser.EOF + | _ -> error (Putil.region lexbuf) "Impossible: bad lcdt state" + else prim_lex ()) lexbuf + in match !first_pos with + | Some p -> p, ty + | _ -> error (Putil.region lexbuf) "Impossible: no lex" + +let lex_core_importdesc (lexbuf : Lexing.lexbuf) + : Lexing.position * Wasm.Ast.import_desc' Ast.Var.core_externdesc_wrapper + = let lcm_status : int ref = ref 0 + and paren_depth : int ref = ref 0 + and first_pos : Lexing.position option ref = ref None in + let token' lexbuf = let tok = Wasm.Lexer.token lexbuf in + match !first_pos with + | None -> first_pos := Some lexbuf.Lexing.lex_start_p; + tok + | Some _ -> tok in + let prim_lex () = + match token' lexbuf with + | Wasm.Parser.LPAR -> paren_depth := !paren_depth + 1; + Wasm.Parser.LPAR + | Wasm.Parser.RPAR -> paren_depth := !paren_depth - 1; + Wasm.Parser.RPAR + | tok -> tok in + let id = + Wasm.Parser.import_desc (fun lexbuf -> + if !paren_depth = 0 + then match !lcm_status with + | 0 -> lcm_status := 1; prim_lex () + | 1 -> Wasm.Parser.EOF + | _ -> error (Putil.region lexbuf) "Impossible: bad lcdt state" + else prim_lex ()) lexbuf + in match !first_pos with + | Some p -> p, id + | _ -> error (Putil.region lexbuf) "Impossible: no lex" + +type special_lookaheads = + | SL_none + | SL_module + | SL_type + | SL_string +type next_token_may_be = + | NT_none + | NT_core_module + | NT_core_deftype + | NT_core_importdesc + +let parse' name orig_lexbuf start = + let bt_lexbuf = bt_lexbuf_of_lexbuf orig_lexbuf in + let lexbuf = bt_lexbuf.bt_lexbuf in + let open MenhirLib.General in + let module Interp = Parser.MenhirInterpreter in + let input = Interp.lexer_lexbuf_to_supplier Lexer.token lexbuf in + let failure error_state = + let env = match[@warning "-4"] error_state with + | Interp.HandlingError env -> env + | _ -> assert false in + match Interp.stack env with + | lazy Nil -> assert false + | lazy (Cons (Interp.Element (state, _, start_pos, end_pos), _)) -> + print_endline (string_of_int (Interp.number state)); + raise (Syntax ({Wasm.Source.left = Putil.convert_pos start_pos; + Wasm.Source.right = Putil.convert_pos end_pos}, + "Parse error")) in + let is_sl = ref SL_none in + let is_nt = ref NT_none in + let rec token_supplier () = + is_sl := SL_none; + match !is_nt with + | NT_core_module -> + (is_nt := NT_none; + bt_lexbuf_mark bt_lexbuf; + try + let p, x, m = lex_core_module lexbuf in + bt_lexbuf_commit bt_lexbuf; + Parser.COREMOD (x, m), p, lexbuf.Lexing.lex_curr_p + with + e -> let msg = Printexc.to_string e + and stack = Printexc.get_backtrace () in + Printf.eprintf "there was an error: %s%s\n" msg stack; + + bt_lexbuf_abort bt_lexbuf; + bt_lexbuf_commit bt_lexbuf; (* there are no other options *) + token_supplier ()) + | NT_core_deftype -> + (is_nt := NT_none; + bt_lexbuf_mark bt_lexbuf; + try + let p, t = lex_core_deftype lexbuf in + bt_lexbuf_commit bt_lexbuf; + Parser.COREDEFTYPE t, p, lexbuf.Lexing.lex_curr_p + with + _ -> bt_lexbuf_abort bt_lexbuf; + bt_lexbuf_commit bt_lexbuf; (* there are no other options *) + let tok, p, q = token_supplier () in + (match tok with + | Parser.VAR _ -> is_nt := NT_core_deftype + | _ -> ()); + tok, p, q) + | NT_core_importdesc -> + (is_nt := NT_none; + bt_lexbuf_mark bt_lexbuf; + try + let p, id = lex_core_importdesc lexbuf in + bt_lexbuf_commit bt_lexbuf; + Parser.COREIMPORTDESC id, p, lexbuf.Lexing.lex_curr_p + with + _ -> bt_lexbuf_abort bt_lexbuf; + bt_lexbuf_commit bt_lexbuf; (* there are no other options *) + token_supplier ()) + | _ -> + let tok, p, q = input () in + (match tok with + | Parser.MODULE -> is_sl := SL_module + | Parser.TYPE -> is_sl := SL_type + | Parser.STRING _ -> is_sl := SL_string + | _ -> is_sl := SL_none); + tok, p, q in + let rec go checkpoint = + let open Interp in + match checkpoint with + | InputNeeded a -> go (offer checkpoint (token_supplier ())) + | Shifting _ -> go (resume checkpoint) + | AboutToReduce (_, production) -> + (match lhs production with + | X (N N_core_marker) -> + (match !is_sl with + | SL_module -> is_nt := NT_core_module + | SL_type -> is_nt := NT_core_deftype + | _ -> ()); + go (resume checkpoint) + | X (N N_core_type_marker) -> + (match !is_sl with + | SL_type -> is_nt := NT_core_deftype + | _ -> ()); + go (resume checkpoint) + | X (N N_core_importdecl_marker) -> + (match !is_sl with + | SL_string -> is_nt := NT_core_importdesc + | _ -> ()); + go (resume checkpoint) + | X (N N_core_exportdecl_marker) -> + (match !is_sl with + | SL_string -> is_nt := NT_core_importdesc + | _ -> ()); + go (resume checkpoint) + | _ -> go (resume checkpoint)) + | HandlingError _ -> failure checkpoint + | Accepted r -> r + (* We should always see HandlingError first *) + | Rejected -> assert false + in go (start lexbuf.Lexing.lex_curr_p) + + +let parse (type a) name lexbuf : a start -> a = function + | Component -> parse' name lexbuf Parser.Incremental.component_module + | Script -> parse' name lexbuf Parser.Incremental.component_script + +let string_to start s = + let lexbuf = Lexing.from_string s in + parse "string" lexbuf start + +let string_to_script s = string_to Script s +let string_to_component s = snd (string_to Component s) diff --git a/interpreter/text/parse.mli b/interpreter/text/parse.mli new file mode 100644 index 00000000..08d8f7cc --- /dev/null +++ b/interpreter/text/parse.mli @@ -0,0 +1,12 @@ +open Putil + +type 'a start = + | Component : (Ast.VarAst.component perhaps_named) start + | Script : Script.script start + +exception Syntax of Wasm.Source.region * string + +val parse : string -> Lexing.lexbuf -> 'a start -> 'a (* raises Syntax *) + +val string_to_script : string -> Script.script (* raises Syntax *) +val string_to_component : string -> Ast.VarAst.component (* raises Syntax *) diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly new file mode 100644 index 00000000..bcd4aba5 --- /dev/null +++ b/interpreter/text/parser.mly @@ -0,0 +1,619 @@ +%{ + +(* work around Menhir type inference bug *) +module Wasm_components = struct + (* for some reason, warning 60 (unused module) can't be disabled, but warning + 34, unused type, can be... *) + type this_module_is_not_unused +end +type workaround_menhir_bug = Wasm_components.this_module_is_not_unused + [@@warning "-34"] + +open Script +open Ast +open VarAst +open Wasm.Source + +open Putil +%} +%start component_module component_script +%type component_module +%type component_script + +%type perhaps_var +%type defs +%type def +%type def_type + +%token LPAR RPAR +%token CORE MODULE COMPONENT INSTANCE ALIAS +%token INSTANTIATE WITH +%token VAR STRING +%token COREMOD +%token COREDEFTYPE +%token unit -> Wasm.Ast.import_desc'> COREIMPORTDESC + +%token IMPORT EXPORT OUTER + +%token FUNC TABLE MEMORY GLOBAL +%token VALUE TYPE +%token NAT + +%token BOOL CHAR TSTRING RECORD VARIANT LIST TUPLE FLAGS ENUM UNION OWN BORROW +%token OPTION ERROR +%token SIGNED UNSIGNED +%token FLOAT +%token FIELD CASE REFINES +%token PARAM RESULT SUB EQ +%token CANON LIFT LOWER +%token STRINGENCODING EQS UTF8 UTF16 LATIN1UTF16 REALLOC POSTRETURN +%token START + +%token INPUT +%token QUOTE BIN + +%token ASSERT_INVALID ASSERT_MALFORMED + +%token RESOURCE RESOURCE_NEW RESOURCE_DROP RESOURCE_REP REP I32 DTOR + +%token EOF + +%% + +component_module : + | LPAR COMPONENT perhaps_var defs RPAR + { $3, (Var.bind $3 { defns = $4 } @@ ptr $symbolstartpos $endpos) } + +prim_var : + | VAR { Var.Var ($1 @@ ptr $symbolstartpos $endpos) } + | NAT { Var.Idx (Int32.of_string $1 @@ ptr $symbolstartpos $endpos) } +core_var : + | prim_var { $1 } + | LPAR core_sort core_var name+ RPAR + { Var.Export (CoreSort $2 @@ ptr $startpos($2) $endpos($2), $3, $4) } +var : + | prim_var { $1 } + | LPAR core_marker_shenanigan_sort var name+ RPAR + { Var.Export ($2, $3, $4) } + +name : + | STRING { $1 @@ ptr $symbolstartpos $endpos } +%inline perhaps_var : + | /* empty */ { Var.No_binder } + | VAR { Var.Var_binder ($1 @@ ptr $symbolstartpos $endpos) } +%inline perhaps_var_E : + | perhaps_var { $1 } + | export_binder { Var.Export_binders ($1::[]) } +%inline export_binder : + | LPAR EXPORT externname RPAR { $3 } + +%inline perhaps_var_E_ : + | perhaps_var { $1 } + | export_binder_ { Var.Export_binders ($1::[]) } +%inline export_binder_ : + | LPAR core_exportdecl_marker externname RPAR { $3 } + +url : + | STRING { $1 @@ ptr $symbolstartpos $endpos } +externname : + | name url? { { en_name = $1; en_url = $2; } @@ ptr $symbolstartpos $endpos } + + +defs : + | /* empty */ { [] } + | def defs + { $1::$2 } +def : + | component_module + { let (a, b) = $1 in ComponentDef b @@ ptr $symbolstartpos $endpos } + | core_def { CoreDef $1 @@ ptr $symbolstartpos $endpos } + | LPAR INSTANCE perhaps_var_E instance_expr RPAR + { InstanceDef (Var.bind $3 $4) @@ ptr $symbolstartpos $endpos } + | alias { AliasDef $1 @@ ptr $symbolstartpos $endpos } + | type_ { TypeDef $1 @@ ptr $symbolstartpos $endpos } + | canon { CanonDef $1 @@ ptr $symbolstartpos $endpos } + | start { StartDef $1 @@ ptr $symbolstartpos $endpos } + | import { ImportDef $1 @@ ptr $symbolstartpos $endpos } + | export_ { ExportDef $1 @@ ptr $symbolstartpos $endpos } + +(* Yes, this is structured a bit strangely. + * See note on nonterminal 'core' below. *) +core_def : + | LPAR core_marker core_def_right { $3 } +core_def_right : + | MODULE COREMOD + { let (b, m) = $2 in + let b' = match b with | None -> Var.No_binder + | Some v -> Var.Var_binder v in + CoreModuleDef (Var.bind b' m) } + | INSTANCE perhaps_var_E core_instance_expr RPAR + { CoreInstanceDef (Var.bind $2 $3) } + | TYPE perhaps_var_E core_deftype__right + { CoreTypeDef (Var.bind $2 $3) } + +core_alias : + | ALIAS core_alias_target LPAR core_sort perhaps_var_E RPAR RPAR + { Var.bind $5 ({ c_a_target = $2; c_a_sort = $4 } + @@ ptr $symbolstartpos $endpos) } + +(* This production looks totally useless, and in most grammars it would be. + * However, it is actually here to be used as a signal to the parser driving + * code in parse.ml (function parse'). Because this nonterminal is not used + * anywhere that the grammar needs to recognize a CORE token save for in + * core_def, the feeding code knows that any time this production is being + * reduced, if the lookahead token is MODULE, this might be a core module + * definition---and so next time the lexer is prompted for a token, it instead + * investigates whether this is the case (via some extra lookahead), and then, + * if it is, invokes the core lexer and parser over the next bit of the input + * stream, generating a synthetic COREMOD token which is used by the first + * production in the core_def_right rule above. *) +core_marker : + | CORE { () } + +core_instance_expr : + | LPAR INSTANTIATE core_var core_instantiate_arg* RPAR + { Core_instantiate_module ($3, $4) @@ ptr $symbolstartpos $endpos} + | core_export* + { Core_instantiate_inline $1 @@ ptr $symbolstartpos $endpos } +core_instantiate_arg : + | LPAR WITH name core_sort_idx RPAR + { { c_ia_name = $3; c_ia_value = $4 } @@ ptr $symbolstartpos $endpos } + | LPAR WITH name LPAR INSTANCE core_export* RPAR RPAR + { let herepos = ptr $symbolstartpos $endpos in + { c_ia_name = $3; + c_ia_value = { c_s_sort = Core_instance @@ no_region; + c_s_idx = Var.CoreInlineInstance $6; } @@ herepos } + @@ herepos } + +core_export : + | LPAR EXPORT name core_sort_idx RPAR + { { c_e_name = $3; c_e_value = $4 } @@ ptr $symbolstartpos $endpos } + +core_sort_idx : + | LPAR core_sort core_var RPAR + { { c_s_sort = $2; c_s_idx = $3 } @@ ptr $symbolstartpos $endpos } + | LPAR core_sort core_var name+ RPAR + { { c_s_sort = $2; + c_s_idx = Var.Export (CoreSort $2 @@ ptr $startpos($2) $endpos($2), + $3, $4); } + @@ ptr $symbolstartpos $endpos } +%inline core_sort_sans_module_type : + | FUNC { Core_func @@ ptr $symbolstartpos $endpos } + | TABLE { Core_table @@ ptr $symbolstartpos $endpos } + | MEMORY { Core_memory @@ ptr $symbolstartpos $endpos } + | GLOBAL { Core_global @@ ptr $symbolstartpos $endpos } + | INSTANCE { Core_instance @@ ptr $symbolstartpos $endpos } +%inline core_sort : + | core_sort_sans_module_type { $1 } + | MODULE { Core_module @@ ptr $symbolstartpos $endpos } + | TYPE { Core_type @@ ptr $symbolstartpos $endpos } + +core_alias_target : + | EXPORT core_var name + { Core_alias_export ($2, $3) @@ ptr $symbolstartpos $endpos } + | OUTER prim_var prim_var + { Core_alias_outer ($2, $3) @@ ptr $symbolstartpos $endpos } + +core_deftype__right : + | COREDEFTYPE RPAR + { Core_deftype__deftype (Core_deftype_functype $1 + @@ ptr $symbolstartpos $endpos) + @@ ptr $symbolstartpos $endpos } + | LPAR MODULE core_moduledecl* RPAR RPAR + { Core_deftype__moduletype ({ decls = $3; } @@ ptr $symbolstartpos $endpos) + @@ ptr $symbolstartpos $endpos } +core_moduledecl : + | core_importdecl { Core_md_importdecl $1 @@ ptr $symbolstartpos $endpos } + | core_type { Core_md_typedecl $1 @@ ptr $symbolstartpos $endpos } + | core_alias { Core_md_aliasdecl $1 @@ ptr $symbolstartpos $endpos } + | core_exportdecl { Core_md_exportdecl $1 @@ ptr $symbolstartpos $endpos } +core_importdecl : + | LPAR IMPORT core_importdecl_marker name COREIMPORTDESC RPAR + { { c_id_name1 = $3; c_id_name2 = $4; + c_id_ty = fun c u -> $5 c u @@ ptr $startpos($5) $endpos($5); } + @@ ptr $symbolstartpos $endpos } +core_importdecl_marker : + | name { $1 } +core_type : + | core_type_marker TYPE perhaps_var COREDEFTYPE RPAR + { Var.bind $3 (Core_deftype_functype $4 @@ ptr $symbolstartpos $endpos) } +core_type_marker : + | LPAR { () } +core_exportdecl : + | LPAR core_exportdecl_marker name COREIMPORTDESC RPAR + { { c_ed_name = $3; + c_ed_ty = fun c u -> $4 c u @@ ptr $startpos($4) $endpos($4); } + @@ ptr $symbolstartpos $endpos } +core_exportdecl_marker : + | EXPORT { () } + +instance_expr : + | LPAR INSTANTIATE var instantiate_arg* RPAR + { Instantiate_component ($3, $4) @@ ptr $symbolstartpos $endpos } + | export* + { Instantiate_inline $1 @@ ptr $symbolstartpos $endpos } +instantiate_arg : + | LPAR WITH name sort_idx RPAR + { { ia_name = $3; ia_value = $4; } @@ ptr $symbolstartpos $endpos } + | LPAR WITH name LPAR INSTANCE export* RPAR RPAR + { let herepos = ptr $symbolstartpos $endpos in + { ia_name = $3; + ia_value = { s_sort = Instance @@ no_region; + s_idx = Var.InlineInstance $6; } @@ herepos } + @@ herepos } + +export : + | LPAR EXPORT externname sort_idx RPAR + { { ie_name = $3; ie_value = $4 } @@ ptr $symbolstartpos $endpos } + +export_ : + | LPAR EXPORT perhaps_var externname sort_idx exportdesc? RPAR + { let t = match $6 with + | None -> None + | Some (Var.No_binder, t) -> Some t + | Some _ -> error (ptr $startpos($6) $endpos($6)) "Binder not allowed on export definition type ascription" + in + Var.bind $3 ({ e_name = $4; e_value = $5; e_type = t } + @@ ptr $symbolstartpos $endpos) } + +sort_idx : + | LPAR sort var RPAR + { { s_sort = $2; s_idx = $3 } @@ ptr $symbolstartpos $endpos } + | LPAR sort var name+ RPAR + { { s_sort = $2; + s_idx = Var.Export ($2, $3, $4); } + @@ ptr $symbolstartpos $endpos } +%inline core_marker_shenanigan_sort_sans_module_type : + | core_marker core_sort_sans_module_type { CoreSort $2 @@ ptr $symbolstartpos $endpos } + | comp_sort { $1 } +%inline core_marker_shenanigan_sort : + | core_marker core_sort { CoreSort $2 @@ ptr $symbolstartpos $endpos } + | comp_sort { $1 } +%inline sort : + | CORE core_sort { CoreSort $2 @@ ptr $symbolstartpos $endpos } + | comp_sort { $1 } +%inline comp_sort : + | FUNC { Func @@ ptr $symbolstartpos $endpos } + | VALUE { Value @@ ptr $symbolstartpos $endpos } + | TYPE { Type @@ ptr $symbolstartpos $endpos } + | INSTANCE { Instance @@ ptr $symbolstartpos $endpos } + | COMPONENT { Ast.Component @@ ptr $symbolstartpos $endpos } + +%inline alias : + | LPAR ALIAS alias_target LPAR sort perhaps_var_E RPAR RPAR + { Var.bind $6 ({ a_target = $3; a_sort = $5 } + @@ ptr $symbolstartpos $endpos) } + | LPAR core_marker_shenanigan_sort_sans_module_type perhaps_var_E LPAR ALIAS alias_target RPAR RPAR + { Var.bind $3 ({ a_target = $6; a_sort = $2 } + @@ ptr $symbolstartpos $endpos) } + | LPAR core_marker MODULE perhaps_var_E_ LPAR ALIAS alias_target RPAR RPAR + { Var.bind $4 ({ a_target = $7; a_sort = CoreSort (Core_module @@ ptr $startpos($3) $endpos($3)) @@ ptr $startpos($2) $endpos($2) } + @@ ptr $symbolstartpos $endpos) } + | LPAR core_marker TYPE perhaps_var_E LPAR ALIAS alias_target RPAR RPAR + { Var.bind $4 ({ a_target = $7; a_sort = CoreSort (Core_type @@ ptr $startpos($3) $endpos($3)) @@ ptr $startpos($2) $endpos($2) } + @@ ptr $symbolstartpos $endpos) } +alias_target : + | EXPORT var name + { Alias_export ($2, $3) @@ ptr $symbolstartpos $endpos } + | CORE EXPORT var name + { Alias_core_export ($3, $4) @@ ptr $symbolstartpos $endpos } + | OUTER prim_var prim_var + { Alias_outer ($2, $3) @@ ptr $symbolstartpos $endpos } + +type_ : + | LPAR TYPE perhaps_var_E def_type RPAR + { Var.bind $3 $4 } +def_type : + | def_val_type { Deftype_val $1 @@ ptr $symbolstartpos $endpos } + | func_type { let b, x = $1 in Deftype_func x @@ ptr $symbolstartpos $endpos } + | component_type { let b, x = $1 in Deftype_comp x @@ ptr $symbolstartpos $endpos } + | instance_type { let b, x = $1 in Deftype_inst x @@ ptr $symbolstartpos $endpos } + | resource_type { Deftype_rsrc $1 @@ ptr $symbolstartpos $endpos } +def_val_type : + | BOOL { Bool @@ ptr $symbolstartpos $endpos } + | SIGNED { Signed $1 @@ ptr $symbolstartpos $endpos } + | UNSIGNED { Unsigned $1 @@ ptr $symbolstartpos $endpos } + | FLOAT { Float $1 @@ ptr $symbolstartpos $endpos } + | CHAR { Char @@ ptr $symbolstartpos $endpos } + | TSTRING { String @@ ptr $symbolstartpos $endpos } + | LPAR RECORD recordfield* RPAR { Record $3 @@ ptr $symbolstartpos $endpos } + | LPAR VARIANT variantcase+ RPAR { Variant $3 @@ ptr $symbolstartpos $endpos } + | LPAR LIST val_type RPAR { List $3 @@ ptr $symbolstartpos $endpos } + | LPAR TUPLE val_type* RPAR { Tuple $3 @@ ptr $symbolstartpos $endpos} + | LPAR FLAGS name* RPAR { Flags $3 @@ ptr $symbolstartpos $endpos } + | LPAR ENUM name+ RPAR { Enum $3 @@ ptr $symbolstartpos $endpos } + | LPAR UNION val_type+ RPAR { Union $3 @@ ptr $symbolstartpos $endpos} + | LPAR OPTION val_type RPAR {Option $3 @@ ptr $symbolstartpos $endpos} + | LPAR RESULT ioption(val_type) ioption(result_error_clause) RPAR + { Expected ($3,$4) @@ ptr $symbolstartpos $endpos } + | LPAR OWN var RPAR { Own $3 @@ ptr $symbolstartpos $endpos } + | LPAR BORROW var RPAR { Borrow $3 @@ ptr $symbolstartpos $endpos } +%inline result_error_clause: + | LPAR ERROR val_type RPAR { $3 } +recordfield : + | LPAR FIELD name val_type RPAR + { { rf_name = $3; rf_type = $4; } @@ ptr $symbolstartpos $endpos } +caserefines : + | LPAR REFINES var RPAR { $3 } +variantcase : + | LPAR CASE perhaps_var name ioption(val_type) ioption(caserefines) RPAR + { Var.bind $3 ({ vc_name = $4; vc_type = $5; vc_default = $6 } + @@ ptr $symbolstartpos $endpos) } +resource_type : + | LPAR RESOURCE LPAR REP I32 RPAR rt_dtor? RPAR + { $7 } +rt_dtor : + | LPAR DTOR var RPAR { $3 } + +%inline typeuse(inner) : + | inner { Var.TInline $1 } + | var { Var.TVar $1 } +val_type : + | typeuse(def_val_type) { $1 } +func_type : + | func_type_IBFB(func_type_empty, func_type_empty) { let a, b, c = $1 in a, b } +%inline func_type_empty : + | { () } +func_type_IBFB(ib, fb) : + | LPAR FUNC perhaps_var_E ib functype_decls_FB(fb) RPAR + { let a, b = $5 in $3, a @@ ptr $symbolstartpos $endpos, ($4, b) } +functype_decls_FB(fb) : + | functype_result_decls(fb) + { let r, x = $1 in + { ft_params = Fio_many [] @@ ptr $startpos($1) $endpos($1) + ; ft_result = r }, x } + | LPAR PARAM val_type RPAR functype_result_decls(fb) + { let r, x = $5 in + { ft_params = Fio_one $3 @@ ptr $startpos($3) $endpos($3) + ; ft_result = r }, x } + | functype_param_decl functype_param_decls(fb) + { let p, (r, x) = $2 in + { ft_params = Fio_many ($1::p) @@ ptr $startpos($1) $endpos($2); + ft_result = r }, x } +functype_param_decls(fb) : + | functype_param_decl functype_param_decls(fb) + { let p, r = $2 in ($1::p), r } + | functype_result_decls(fb) { [], $1 } +%inline functype_result_decls(fb) : + | fb { Fio_many [] @@ ptr $startpos($1) $endpos($1), $1 } + | LPAR RESULT val_type RPAR fb { Fio_one $3 @@ ptr $startpos($3) $endpos($3), $5 } + | functype_result_decl functype_result_decll(fb) + { let r, x = $2 in Fio_many ($1::r) @@ ptr $startpos($1) $endpos($2), x } +functype_result_decll(fb) : + | fb { [], $1 } + | functype_result_decl functype_result_decll(fb) + { let r, x = $2 in ($1::r), x } +%inline functype_result_decl : + | LPAR RESULT name val_type RPAR { $3, $4 } +%inline functype_param_decl : + | LPAR PARAM name val_type RPAR + { $3, $4 } +component_type : + | component_type_IBFB(component_type_empty, component_type_empty) { let a, b, c = $1 in a, b } +%inline component_type_empty : + | { () } +component_type_IBFB(ib, fb) : + | LPAR COMPONENT perhaps_var ib component_decl* fb RPAR + { $3, $5 @@ ptr $symbolstartpos $endpos, ($4, $6) } +instance_type : + | instance_type_IBFB(instance_type_empty, instance_type_empty) { let a, b, c = $1 in a, b } +%inline instance_type_empty : + | { () } +instance_type_IBFB(ib, fb) : + | LPAR INSTANCE perhaps_var ib instance_decl* fb RPAR + { $3, $5 @@ ptr $symbolstartpos $endpos, ($4, $6) } +component_decl : + | import_decl { Component_import $1 @@ ptr $symbolstartpos $endpos } + | instance_decl { Component_instance $1 @@ ptr $symbolstartpos $endpos } +instance_decl : + | alias { Instance_alias $1 @@ ptr $symbolstartpos $endpos } + | type_decl { Instance_type $1 @@ ptr $symbolstartpos $endpos } + | export_decl { Instance_export $1 @@ ptr $symbolstartpos $endpos } +import_decl : + | LPAR IMPORT externname importdesc RPAR + { let b, x = $4 in + { id_name = $3; id_type = Var.bind b x; } @@ ptr $symbolstartpos $endpos } +importdesc : + | exportdesc { $1 } +type_decl : + | LPAR TYPE perhaps_var_E def_type RPAR + { Var.bind $3 $4 } +export_decl : + | LPAR EXPORT externname exportdesc RPAR + { let b, x = $4 in + { ed_name = $3; ed_type = Var.bind b x; } @@ ptr $symbolstartpos $endpos } +exportdesc : + | exportdesc_FB(exportdesc_empty) { let a, b, c = $1 in a, b } +%inline exportdesc_empty : + | { () } +%inline exportdesc_funconly_FB(fb) : + | exportdesc_funconly_IBFB(exportdesc_empty, fb) + { let a, b, (i, f) = $1 in a, b, f } +%inline exportdesc_funconly_IBFB(ib, fb) : + | LPAR comp_sort perhaps_var_E ib LPAR TYPE var RPAR fb RPAR + { $3, Export_sort_id ($2, $7) @@ ptr $symbolstartpos $endpos, ($4, $9) } + | func_type_IBFB(ib, fb) + { let b, x, y = $1 in b, Export_func x @@ ptr $symbolstartpos $endpos, y } +%inline exportdesc_FB(fb) : + | exportdesc_IBFB(CORE, exportdesc_empty, fb) + { let a, b, (i, f) = $1 in a, b, f } +exportdesc_IBFB(core_helper, ib, fb) : + | exportdesc_funconly_IBFB(ib, fb) + { $1 } + | LPAR core_helper MODULE perhaps_var_E_ ib core_type_marker TYPE core_var RPAR fb RPAR + { $4, + Export_sort_id (CoreSort (Core_module @@ ptr $startpos($3) $endpos($3)) + @@ ptr $startpos($2) $endpos($3) + ,$8) + @@ ptr $symbolstartpos $endpos, ($5, $10) } + | LPAR core_helper TYPE perhaps_var_E ib LPAR TYPE core_var RPAR fb RPAR + { $4, + Export_sort_id (CoreSort (Core_type @@ ptr $startpos($3) $endpos($3)) + @@ ptr $startpos($2) $endpos($3) + ,$8) + @@ ptr $symbolstartpos $endpos, ($5, $10) } + | LPAR core_marker core_sort_sans_module_type perhaps_var ib LPAR TYPE core_var RPAR fb RPAR + { $4, + Export_sort_id (CoreSort $3 @@ ptr $startpos($2) $endpos($3), $8) + @@ ptr $symbolstartpos $endpos, ($5, $10) } + | LPAR core_helper MODULE perhaps_var_E_ ib core_moduledecl* fb RPAR + { $4, Export_core_mod ({ decls = $6; } @@ ptr $startpos($6) $endpos($6)) + @@ ptr $symbolstartpos $endpos, ($5, $7) } + | component_type_IBFB(ib, fb) + { let b, x, y = $1 in b, Export_comp x @@ ptr $symbolstartpos $endpos, y } + | instance_type_IBFB(ib, fb) + { let b, x, y = $1 in b, Export_inst x @@ ptr $symbolstartpos $endpos, y } + | LPAR VALUE perhaps_var_E ib val_type fb RPAR + { $3, Export_val $5 @@ ptr $symbolstartpos $endpos, ($4, $6) } + | LPAR TYPE perhaps_var_E ib type_bound fb RPAR + { $3, Export_type $5 @@ ptr $symbolstartpos $endpos, ($4, $6) } +type_bound : + | type_cstr { $1 } +type_cstr : + | LPAR SUB RESOURCE RPAR + { Tbound_subr @@ ptr $symbolstartpos $endpos } + | LPAR EQ typeuse(def_type) RPAR + { Tbound_eq $3 @@ ptr $symbolstartpos $endpos } + +%inline canon : + | LPAR CANON LIFT canon_lift_args(canon_func_end) RPAR + { let x, b = $4 in Var.bind b (x @@ ptr $symbolstartpos $endpos) } + | LPAR CANON LOWER canon_lower_args(canon_core_func_end) RPAR + { let x, b = $4 in Var.bind b (x @@ ptr $symbolstartpos $endpos) } + + | LPAR CANON RESOURCE_NEW typeuse(def_type) canon_core_func_end RPAR + { Var.bind $5 (Canon_resource_builtin + (CRB_new $4 @@ ptr $symbolstartpos $endpos) + @@ ptr $symbolstartpos $endpos) } + | LPAR CANON RESOURCE_DROP val_type;; canon_core_func_end RPAR + { Var.bind $5 (Canon_resource_builtin + (CRB_drop $4 @@ ptr $symbolstartpos $endpos) + @@ ptr $symbolstartpos $endpos) } + | LPAR CANON RESOURCE_REP typeuse(def_type) canon_core_func_end RPAR + { Var.bind $5 (Canon_resource_builtin + (CRB_rep $4 @@ ptr $symbolstartpos $endpos) + @@ ptr $symbolstartpos $endpos) } + + | exportdesc_funconly_FB(invert_canon_lift_right) + { let v, e, (x, o) = $1 in + let oo, _ = o [] in + Var.bind v (Canon_lift (x, e, oo) @@ ptr $symbolstartpos $endpos) } + + | LPAR core_marker FUNC perhaps_var_E LPAR CANON LOWER canon_lower_args(canon_core_no_end) RPAR RPAR + { let x, _ = $8 in Var.bind $4 (x @@ ptr $symbolstartpos $endpos) } + + | LPAR core_marker FUNC perhaps_var_E LPAR CANON RESOURCE_NEW typeuse(def_type) RPAR RPAR + { Var.bind $4 (Canon_resource_builtin + (CRB_new $8 @@ ptr $symbolstartpos $endpos) + @@ ptr $symbolstartpos $endpos) } + | LPAR core_marker FUNC perhaps_var_E LPAR CANON RESOURCE_DROP val_type RPAR RPAR + { Var.bind $4 (Canon_resource_builtin + (CRB_drop $8 @@ ptr $symbolstartpos $endpos) + @@ ptr $symbolstartpos $endpos) } + | LPAR core_marker FUNC perhaps_var_E LPAR CANON RESOURCE_REP typeuse(def_type) RPAR RPAR + { Var.bind $4 (Canon_resource_builtin + (CRB_rep $8 @@ ptr $symbolstartpos $endpos) + @@ ptr $symbolstartpos $endpos) } +canon_lift_args(canon_end) : + | var canon_opts(canon_end) + { let o, (x, e) = $2 [] in (Canon_lift ($1, e, o), x) } +%inline invert_canon_lift_right : + | LPAR CANON LIFT var canon_opts(canon_no_end) RPAR + { ($4, $5) } +canon_lower_args(canon_end) : + | var canon_opts(canon_end) + { let o, e = $2 [] in Canon_lower ($1, o), e } +canon_opts(canon_end) : + | canon_end { fun o -> List.rev o, $1 } + | canon_opt canon_opts(canon_end) { fun o -> $2 ($1::o) } +canon_opt : + | STRINGENCODING EQS UTF8 { String_utf8 @@ ptr $symbolstartpos $endpos } + | STRINGENCODING EQS UTF16 { String_utf16 @@ ptr $symbolstartpos $endpos } + | STRINGENCODING EQS LATIN1UTF16 { String_utf16 @@ ptr $symbolstartpos $endpos } + | LPAR MEMORY core_var RPAR { Memory $3 @@ ptr $symbolstartpos $endpos } + | LPAR REALLOC core_var RPAR { Realloc $3 @@ ptr $symbolstartpos $endpos } + | LPAR POSTRETURN core_var RPAR { PostReturn $3 @@ ptr $symbolstartpos $endpos } +canon_func_end : + | exportdesc { $1 } +canon_no_end : + | { () } + +canon_core_func_end : + | LPAR CORE FUNC perhaps_var_E RPAR { $4 } +canon_core_no_end : + | { () } + +start : + | LPAR START var startbody RPAR + { let ps, rs = $4 [] in + { s_func = $3 + ; s_params = ps + ; s_result = List.map (fun r -> Var.bind r ()) rs; + } @@ ptr $symbolstartpos $endpos} +%inline +startresults : + | /* empty */ { fun rs vs -> List.rev vs, List.rev rs } + | LPAR RESULT LPAR VALUE perhaps_var RPAR RPAR startresults_ + { fun rs vs -> $8 ($5::rs) vs } +startresults_ : + | startresults { $1 } +startbody : + | startresults { $1 [] } + | LPAR VALUE var RPAR startbody { fun vs -> $5 ($3::vs) } + +%inline import : + | LPAR IMPORT externname importdesc RPAR + { let b, x = $4 in + ({ i_name = $3; i_type = Var.bind b x; } @@ ptr $symbolstartpos $endpos) } | exportdesc_IBFB(core_marker, import_right, exportdesc_empty) + { let b, x, (i, f) = $1 in + ({ i_name = i; i_type = Var.bind b x; } @@ ptr $symbolstartpos $endpos) } +%inline import_right : + | LPAR IMPORT externname RPAR { $3 } + + +(*** SCRIPTS ***) + +string_list : + | /* empty */ { "" } + | string_list STRING { $1 ^ $2 } + +script_component : + | component_module + { let x, c = $1 in x, Textual c @@ ptr $symbolstartpos $endpos } + | LPAR COMPONENT perhaps_var BIN string_list RPAR + { $3, Encoded ( "binary:" + ^ string_of_pos (position_to_pos $symbolstartpos) + , $5) + @@ ptr $symbolstartpos $endpos } + | LPAR COMPONENT perhaps_var QUOTE string_list RPAR + { $3, Quoted ( "quoted: " + ^ string_of_pos (position_to_pos $symbolstartpos) + , $5) + @@ ptr $symbolstartpos $endpos } + +script_var_opt : + | /* empty */ { None } + | VAR { Some ($1 @@ ptr $symbolstartpos $endpos) } /* Sugar */ + +meta : + | LPAR INPUT script_var_opt STRING RPAR { Input ($3, $4) @@ ptr $symbolstartpos $endpos } + +assertion : + | LPAR ASSERT_INVALID script_component STRING RPAR + { AssertInvalid (snd $3, $4) @@ ptr $symbolstartpos $endpos } + | LPAR ASSERT_MALFORMED script_component STRING RPAR + { AssertMalformed (snd $3, $4) @@ ptr $symbolstartpos $endpos } + +cmd : + | assertion { Assertion $1 @@ ptr $symbolstartpos $endpos } + | script_component + { let b, c = $1 in + Script.Component (b, c) @@ ptr $symbolstartpos $endpos } + | meta { Meta $1 @@ ptr $symbolstartpos $endpos } + +cmd_list : + | /* empty */ { [] } + | cmd cmd_list { $1 :: $2 } + +component_script : + | cmd_list EOF { $1 } diff --git a/interpreter/valid/elaborate.ml b/interpreter/valid/elaborate.ml new file mode 100644 index 00000000..77b4c173 --- /dev/null +++ b/interpreter/valid/elaborate.ml @@ -0,0 +1,662 @@ +open Ast +module I = IntAst +open Wasm.Source +open Subtype +open Etypes +open Etype_pp +open Substitute + +type vc_ctx = { vc_ctx_ctx : ctx; vc_ctx_cases : variant_case list } + +let resolve_type_use (ctx : ctx) (t : int32) : def_type + = let ti = Int32.to_int t in + try List.nth ctx.types ti + with Failure _ -> + raise (Invalid (no_region, "No such type to use: " ^ + string_of_int ti)) + +let resolve_val_type_use (ctx : ctx) at (t : int32) : val_type + = match resolve_type_use ctx t with + | DT_val_type vt -> vt + | _ -> raise (Invalid (at, "type use is not a value type")) + +(* why don't we have the I.prim_val_type vs I.def_val_type split again? *) +let rec elab_def_val_type (ctx : ctx) (t : I.def_val_type) : val_type + = match t.it with + | I.Bool -> Bool + | I.Signed s -> Signed s + | I.Unsigned s -> Unsigned s + | I.Float s -> Float s + | I.Char -> Char + | I.String -> List Char + | I.List t' -> List (resolve_val_type_use ctx t.at t') + | I.Record rfs -> Record (List.map (elab_record_field ctx) rfs) + | I.Variant vcs -> elab_variant_cases ctx vcs + | I.Tuple vts -> Record (List.mapi (elab_tuple_field ctx t.at) vts) + | I.Flags ns -> Record (List.map (elab_flags_case ctx) ns) + | I.Enum ns -> Variant (List.map (elab_enum_case ctx) ns) + | I.Option t' -> Variant + [ { vc_name = "none" @@ t.at + ; vc_type = None + ; vc_default = None } + ; { vc_name = "some" @@ t.at + ; vc_type = Some (resolve_val_type_use ctx t.at t') + ; vc_default = None } + ] + | I.Expected (t1, t2) -> + Variant + [ { vc_name = "ok" @@ t.at + ; vc_type = Option.map (resolve_val_type_use ctx t.at) t1 + ; vc_default = None + } + ; { vc_name = "error" @@ t.at + ; vc_type = Option.map (resolve_val_type_use ctx t.at) t2 + ; vc_default = None + } + ] + | I.Union ts -> Variant (List.mapi (elab_union_case ctx t.at) ts) + | I.Own t' -> + let et' = resolve_type_use ctx t' in + def_type_is_resource ctx et'; + Own et' + | I.Borrow t' -> + let et' = resolve_type_use ctx t' in + def_type_is_resource ctx et'; + Borrow et' +and elab_record_field (ctx : ctx) (f : I.record_field) : record_field + = { rf_name = f.it.I.rf_name + ; rf_type = resolve_val_type_use ctx f.at f.it.I.rf_type } +and elab_variant_cases ctx (vcs : I.variant_case list) + = let go cs c = + let vc_ctx = { vc_ctx_ctx = ctx; vc_ctx_cases = cs } in + let c' = elab_variant_case vc_ctx c in + List.append cs [c'] + in + Variant (List.fold_left go [] vcs) +and elab_variant_case (vc_ctx : vc_ctx) (c : I.variant_case) : variant_case + = let t' = Option.map (resolve_val_type_use vc_ctx.vc_ctx_ctx c.at) + c.it.I.vc_type in + { vc_name = c.it.I.vc_name; + vc_type = t'; + vc_default = Option.map (elab_variant_default vc_ctx t' c.at) + c.it.I.vc_default + } +and elab_variant_default (vc_ctx : vc_ctx) (t' : val_type option) at (def : int32) + : int32 + = match List.nth vc_ctx.vc_ctx_cases (Int32.to_int def) with + | exception Failure _ -> + raise (Invalid (at, "default case does not exist")) + | vc' -> subtype_val_type_option vc_ctx.vc_ctx_ctx t' vc'.vc_type; + def +and elab_tuple_field (ctx : ctx) at (i : int) (f : I.val_type) : record_field + = { rf_name = string_of_int i @@ at; rf_type = resolve_val_type_use ctx at f } +and elab_flags_case (ctx : ctx) (n : name) : record_field + = { rf_name = n; rf_type = Bool } +and elab_enum_case (ctx : ctx) (n : name) : variant_case + = { vc_name = n; vc_type = None; vc_default = None } +and elab_union_case (ctx : ctx) at (i : int) (f : I.val_type) : variant_case + = { vc_name = string_of_int i @@ at + ; vc_type = Some (resolve_val_type_use ctx at f) + ; vc_default = None + } + +type position = + { pos_param : bool (* borrows allowed *) + ; pos_export : bool (* no bare resource types allowed *) + } + +let rec wf_val_type (ctx : ctx) (p : position) (t : val_type) : unit + = match t with + | Bool -> () + | Signed _ -> () + | Unsigned _ -> () + | Float _ -> () + | Char -> () + | List t -> wf_val_type ctx p t + | Record rfs -> List.iter (wf_record_field ctx p rfs) rfs + | Variant vcs -> List.iter (wf_variant_case ctx p vcs) vcs + | Own (DT_resource_type rtidx) -> + wf_def_type ctx p (DT_resource_type rtidx) + | Own (DT_var a) -> + wf_def_type ctx p (DT_var a); + def_type_is_resource ctx (DT_var a) + | Own _ -> raise (Invalid (no_region, "non-resource type in own/borrow")) + | Borrow dt -> + if p.pos_param + then wf_val_type ctx p (Own dt) + else raise (Invalid (no_region, "borrow in non-parameter position")) +and wf_record_field (ctx : ctx) (p : position) (rfs : record_field list) (rf : record_field) : unit + = let rfs' = List.filter (fun rf' -> rf'.rf_name.it = rf.rf_name.it) rfs in + if List.length rfs' <> 1 + then raise (Invalid (rf.rf_name.at, "duplicate record field name")) + else wf_val_type ctx p rf.rf_type +and wf_variant_case (ctx : ctx) (p : position) (vcs : variant_case list) (vc : variant_case) : unit + = let vcs' = List.filter (fun vc' -> vc'.vc_name.it = vc.vc_name.it) vcs in + if List.length vcs' <> 1 + then raise (Invalid (vc.vc_name.at, "duplicate variant case name")) + else (); + (match vc.vc_default with + | None -> () + | Some i -> + match List.nth vcs (Int32.to_int i) with + | exception Failure _ -> + raise (Invalid (vc.vc_name.at, "default case does not exist")) + | vc' -> subtype_val_type_option ctx vc.vc_type vc'.vc_type); + (match vc.vc_type with + | None -> () + | Some t -> wf_val_type ctx p t) +and wf_func_io (ctx : ctx) (p : position) (io : func_ios) : unit + = match io with + | Fio_one vt -> wf_val_type ctx p vt + | Fio_many nvts -> List.iter (fun (n, vt) -> wf_val_type ctx p vt) nvts +and wf_func_type (ctx : ctx) (p : position) (ft : func_type) : unit + = wf_func_io ctx { p with pos_param = true; } ft.ft_params; + wf_func_io ctx { p with pos_param = false; } ft.ft_result; +and wf_extern_desc (ctx : ctx) (p : position) (ed : extern_desc) : unit + = match ed with + | ED_core_module cmt -> () + | ED_func ft -> wf_func_type ctx p ft + | ED_value vt -> wf_val_type ctx p vt + | ED_type dt -> wf_def_type ctx p dt + | ED_instance it -> wf_instance_type ctx p it + | ED_component ct -> wf_component_type ctx p ct +and wf_instance_type (ctx : ctx) (p : position) (it : instance_type) : unit + = let ctx', bsub = bound_to_evars ctx it.it_evars in + let eds = List.map + (fun ed -> subst_extern_desc (bsubst_subst bsub) ed.ed_desc) + it.it_exports in + List.iter (wf_extern_desc ctx' p) eds +and wf_component_type (ctx : ctx) (p : position) (ct : component_type) : unit + = let ctx', bsub = bound_to_uvars ctx false ct.ct_uvars in + let eds = List.map + (fun ed -> subst_extern_desc (bsubst_subst bsub) ed.ed_desc) + ct.ct_imports in + List.iter (wf_extern_desc ctx' p) eds; + let in' = subst_instance_type (bsubst_subst bsub) ct.ct_instance in + wf_instance_type ctx' p in' +and wf_def_type (ctx : ctx) (p : position) (dt : def_type) : unit + = match dt with + | DT_var tv -> () + | DT_resource_type rtidx -> + if p.pos_export + then raise (Invalid (no_region, + "Cannot export type containing bare resource type")) + else + if Int32.to_int rtidx >= List.length (ctx.rtypes) + then raise (Invalid (no_region, "resource type index does not exist")) + else () + | DT_val_type vt -> wf_val_type ctx p vt + | DT_func_type ft -> wf_func_type ctx p ft + | DT_instance_type it -> wf_instance_type ctx p it + | DT_component_type ct -> wf_component_type ctx p ct + +let elab_func_io (ctx : ctx) (p : position) (io : I.func_ios) : func_ios + = + let go t = let t' = resolve_val_type_use ctx no_region t in + wf_val_type ctx p t'; t' in + match io.it with + | I.Fio_one t -> Fio_one (go t) + | I.Fio_many ts -> Fio_many (List.map (fun (n, t) -> (n, go t)) ts) + +let elab_func_type (ctx : ctx) (ft : I.func_type) : func_type + = { ft_params = elab_func_io ctx { pos_param = true; pos_export = false; } + ft.it.I.ft_params + ; ft_result = elab_func_io ctx { pos_param = false; pos_export = false; } + ft.it.I.ft_result + } + +let core_type_of_core_externdesc (ed : core_extern_desc) : core_type + = let open Wasm.Types in + match ed with + | ExternFuncType ft -> CT_func ft + | ExternTableType t -> CT_table t + | ExternMemoryType t -> CT_memory t + | ExternGlobalType t -> CT_global t + +let resolve_core_alias_export + (ctx : ctx) (i : core_instance_type) at (s : core_sort') (n : name) + : core_type + = let ed = + try List.find (fun x -> x.ced_name.it = n.it) i.cit_exports + with Not_found -> + raise (Invalid (at, "No such export: " ^ n.it)) + in + let open Wasm.Types in + match s, ed.ced_desc with + | Core_func, ExternFuncType _ + | Core_table, ExternTableType _ + | Core_memory, ExternMemoryType _ + | Core_global, ExternGlobalType _ -> + core_type_of_core_externdesc ed.ced_desc + | _, _ -> raise (Invalid (at, "Export of wrong sort: " ^ n.it)) + +let rec resolve_core_alias_outer + (ctx : ctx) at (o : int) (i : int) (s : core_sort') : core_type + = match o with + | 0 -> + (try + match s with + (*| Core_func -> CT_func (List.nth ctx.core_ctx.core_funcs i)*) + (*| Core_table -> CT_table (List.nth ctx.core_ctx.core_tables i)*) + (*| Core_memory -> CT_table (List.nth ctx.core_ctx.core_mems i)*) + (*| Core_global -> CT_global (List.nth ctx.core_ctx.core_globals i)*) + | Core_type -> List.nth ctx.core_ctx.core_types i + | _ -> raise (Invalid (at, "Stateful outer aliases not allowed")) + with | Not_found -> + raise (Invalid (at, "No such index " ^ string_of_int i + ^ " for sort " ^ show_core_sort' s))) + | _ -> match ctx.parent_ctx with + | Some ctx' -> + resolve_core_alias_outer ctx' at (o - 1) i s + | None -> + raise (Invalid (at, "No such enclosing component")) + +let resolve_core_alias (ctx : ctx) (a : I.core_alias) : core_type + = match a.it.I.c_a_target.it with + | I.Core_alias_export (i, n) -> + resolve_core_alias_export + ctx (List.nth ctx.core_ctx.core_instances (Int32.to_int i)) + a.it.I.c_a_target.at a.it.I.c_a_sort.it n + | I.Core_alias_outer (o, i) -> + resolve_core_alias_outer + ctx a.it.I.c_a_target.at + (Int32.to_int o) (Int32.to_int i) + a.it.I.c_a_sort.it + +let mark_dead_ed at ed = + match ed.ad_contents.ed_desc with + | ED_instance _ | ED_value _ -> + if not ed.ad_live + then raise (Invalid (at, "Cannot reuse dead value/instance")) + else { ed with ad_live = false } + | _ -> ed + +let resolve_alias_export + (ctx : ctx) (i : int32) at (s : sort') (n : name) + : ctx * (core_type, def_type) Either.t + = let i = Int32.to_int i in + let ii = (List.nth ctx.instances i).itad_exports in + let ed = + try List.find (fun x -> x.ad_contents.ed_name.it.en_name.it = n.it) ii + with | Not_found -> + raise (Invalid (at, "No such export: " ^ n.it)) + in + let ed' = mark_dead_ed at ed in + let eds' = List.map (fun x -> if x.ad_contents.ed_name.it.en_name.it = n.it + then ed' else x) ii in + let ii' = { itad_exports = eds' } in + let is' = List.mapi (fun i' x -> if i' = i then ii' else x) + ctx.instances in + let ctx' = { ctx with instances = is' } in + (ctx', match s, ed.ad_contents.ed_desc with + | CoreSort { it = Core_module; _ }, ED_core_module cmt -> + Either.Left (CT_module cmt) + | Func, ED_func ft -> Either.Right (DT_func_type ft) + | Value, ED_value v -> Either.Right (DT_val_type v) + | Type, ED_type t -> Either.Right t + | Instance, ED_instance it -> Either.Right (DT_instance_type it) + | Component, ED_component ct -> Either.Right (DT_component_type ct) + | _ -> raise (Invalid (at, + pp_string (fun () -> + emit "Bad export alias:"; + emit_newline " expected sort "; + emit (show_sort' s); + emit_newline " got descriptor "; + emit_extern_desc ctx ed.ad_contents.ed_desc)))) + +let innerize_type (ctx : ctx) (ob : bool) (t : (core_type, def_type) Either.t) + : (core_type, def_type) Either.t + = + match t with + | Either.Left ct -> Either.Left ct + | Either.Right t -> + let innerize_fv (fv : free_tyvar) : def_type + = if ob + then + match resolve_tyvar ctx (TV_free fv) with + | RTV_definite dt -> dt + | _ -> raise (Invalid (no_region, + "Outer alias may not refer to type variable")) + else + match fv with + | FTV_uvar (o, i) -> DT_var (TV_free (FTV_uvar (o + 1, i))) + | FTV_evar (o, i) -> DT_var (TV_free (FTV_evar (o + 1, i))) + in + Either.Right (subst_def_type (fsubst_subst innerize_fv) t) + +let rec resolve_alias_outer + (ctx : ctx) at (o : int) (i : int) (s : sort') + : (core_type, def_type) Either.t + = match o with + | 0 -> + (try + match s with + | CoreSort s' -> Either.Left (resolve_core_alias_outer ctx at 0 i s'.it) + (* | Func -> Either.Right (DT_func_type (List.nth ctx.funcs i))*) + (* | Value -> Either.Right (DT_val_type (List.nth ctx.values i))*) + | Type -> Either.Right (List.nth ctx.types i) + | Component -> + Either.Right (DT_component_type (List.nth ctx.components i)) + (* | Instance -> + Either.Right (DT_instance_type (List.nth ctx.instances i))*) + | _ -> raise (Invalid (at, "Stateful outer aliases not allowed")) + with | Failure _ -> + raise (Invalid (at, "No such index " ^ string_of_int i + ^ " for sort " ^ show_sort' s))) + | _ -> match ctx.parent_ctx with + | Some ctx' -> + innerize_type ctx' ctx.outer_boundary + (resolve_alias_outer ctx' at (o - 1) i s) + | None -> + raise (Invalid (at, "No such enclosing component")) + +let resolve_alias (ctx : ctx) (a : I.alias) : + ctx * (core_type, def_type) Either.t + = match a.it.I.a_target.it with + | I.Alias_export (i, n) -> + resolve_alias_export + ctx i a.at a.it.I.a_sort.it n + | I.Alias_core_export (i, ns) -> + (match a.it.I.a_sort.it with + | CoreSort s' -> + (ctx, Either.Left + (resolve_core_alias_export + ctx (List.nth ctx.core_ctx.core_instances (Int32.to_int i)) + a.it.I.a_target.at + s'.it + ns)) + | _ -> + raise (Invalid (a.at, + "Cannot look for non-core export of core instance"))) + | I.Alias_outer (o, i) -> + let t = resolve_alias_outer + ctx a.it.I.a_target.at + (Int32.to_int o) (Int32.to_int i) + a.it.I.a_sort.it in + (match t with + | Either.Right dt -> + wf_def_type ctx { pos_param = false; pos_export = true } dt + | _ -> ()); + (ctx, t) + +let elab_core_deftype (ctx : ctx) (ct : I.core_deftype) : core_type + = match ct.it with + | I.Core_deftype_functype cft -> CT_func cft.it + +let empty_core_module_type : core_module_type + = { cmt_imports = [] ; cmt_instance = { cit_exports = [] } } + +let elab_core_extern_desc (ced : I.core_externdesc) + = let open Wasm.Types in + let open Wasm.Ast in + let open Wasm.ParseUtil in + match (snd ced).it with + | FuncImport i -> + ExternFuncType (List.nth (fst ced).types.list (Int32.to_int i.it)).it + | TableImport tt -> + ExternTableType tt + | MemoryImport mt -> + ExternMemoryType mt + | GlobalImport gt -> + ExternGlobalType gt + +let elab_core_moduledecl (ctx : ctx) (cmd : I.core_moduledecl) + : ctx * core_module_type + = match cmd.it with + | I.Core_md_importdecl ci -> + (ctx, { cmt_imports = [ { cid_name1 = ci.it.I.c_id_name1 + ; cid_name2 = ci.it.I.c_id_name2 + ; cid_desc = elab_core_extern_desc + ci.it.I.c_id_ty } ] + ; cmt_instance = { cit_exports = [] } }) + | I.Core_md_typedecl cdt -> + let cdt' = elab_core_deftype ctx cdt in + ({ ctx with core_ctx = { ctx.core_ctx with + core_types = ctx.core_ctx.core_types @ [cdt'] } }, + empty_core_module_type) + | I.Core_md_aliasdecl ad -> + (match ad.it.I.c_a_sort.it, ad.it.I.c_a_target.it with + | Core_type, I.Core_alias_outer _ -> + let ct = resolve_core_alias ctx ad in + ({ ctx with + core_ctx = { ctx.core_ctx with + core_types = ctx.core_ctx.core_types @ [ct] } }, + empty_core_module_type) + | _, _ -> raise (Invalid (cmd.at, "Only outer type aliases allowed in core module types"))) + | I.Core_md_exportdecl ed -> + (ctx, { cmt_imports = [] + ; cmt_instance = { + cit_exports = [ { ced_name = ed.it.I.c_ed_name + ; ced_desc = elab_core_extern_desc + ed.it.I.c_ed_ty } ] } }) + +let elab_core_moduletype (ctx : ctx) (cmt : I.core_moduletype) + : core_module_type + = let rec go ctx' cmt' decls = + match decls with + | [] -> cmt' + | d::ds -> + let ctx'', cmt'' = elab_core_moduledecl ctx' d in + let cmt''' = + { cmt_imports = cmt'.cmt_imports @ cmt''.cmt_imports + ; cmt_instance = + { cit_exports = cmt'.cmt_instance.cit_exports + @ cmt''.cmt_instance.cit_exports } } in + go ctx'' cmt''' ds + in go (empty_ctx (Some ctx) false) empty_core_module_type (cmt.it.I.decls) + +let elab_core_deftype_ (ctx : ctx) (cdt : I.core_deftype_) + : core_type + = match cdt.it with + | I.Core_deftype__deftype cdt -> elab_core_deftype ctx cdt + | I.Core_deftype__moduletype cmt -> CT_module (elab_core_moduletype ctx cmt) + +let unvar_instance_type (it : instance_type) + : boundedtyvar list * instance_type + = (it.it_evars, { it_evars = [] ; it_exports = it.it_exports }) + +let rec elab_extern_desc (ctx : ctx) (ed : I.exportdesc) + : boundedtyvar list * extern_desc + = + let go_it it = let v, it' = unvar_instance_type it in (v, ED_instance it') in + match ed.it with + | I.Export_sort_id (s, id) -> + let dt = List.nth ctx.types (Int32.to_int id) in + (match s.it, dt with + | Func, DT_func_type ft -> ([], ED_func ft) + | Component, DT_component_type ct -> ([], ED_component ct) + | Instance, DT_instance_type it -> go_it it + | Value, DT_val_type vt -> ([], ED_value vt) + | Type, _ -> ([], ED_type dt) + | _, _ -> raise (Invalid (ed.at, "Export type doesn't match sort"))) + | I.Export_core_mod cmt -> + ([], ED_core_module (elab_core_moduletype ctx cmt)) + | I.Export_func ft -> + ([], ED_func (elab_func_type ctx ft)) + | I.Export_comp ct -> + ([], ED_component (elab_component_type ctx ct)) + | I.Export_inst it -> + go_it (elab_instance_type ctx it) + | I.Export_val vt -> + ([], ED_value (resolve_val_type_use ctx ed.at vt)) + | I.Export_type { it = I.Tbound_eq dt ; _ } -> + ([], ED_type (resolve_type_use ctx dt)) + | I.Export_type { it = I.Tbound_subr ; _ } -> + ([Tbound_subr], ED_type (DT_var (TV_bound 0))) + +and elab_instance_decl (ctx : ctx) (id : I.instance_decl) + : ctx * extern_decl option + = match id.it with + | I.Instance_type t -> + let t' = elab_def_type ctx t in + (match t' with + | DT_resource_type _ -> raise (Invalid (id.at, "Resource type can not appear in instance declarator")) + | _ -> + let ctx' = { ctx with types = ctx.types @ [t'] } in + (ctx', None)) + | I.Instance_alias a -> + (match a.it.I.a_sort.it with + | CoreSort { it = Core_type; _ } -> + let ctx', t = resolve_alias ctx a in + (match t with + | Either.Left ct -> + let ctx'' = { ctx' with + core_ctx = { ctx'.core_ctx with + core_types = ctx'.core_ctx.core_types + @ [ct] } } in + (ctx'', None) + | _ -> raise (Invalid (no_region, + "core type alias produced non-core-type"))) + | Type -> + let ctx', t = resolve_alias ctx a in + (match t with + | Either.Right t -> + let ctx'' = { ctx' with types = ctx'.types @ [t] } in + (ctx'', None) + | _ -> raise (Invalid (no_region, + "type alias produced non-type"))) + | _ -> + raise + (Invalid + (no_region, + "non-(core) type alias not allowed in instance type declarator" + ))) + | I.Instance_export ed -> + let v, ed' = elab_extern_desc ctx ed.it.I.ed_type in + let ctx', bsub = bound_to_evars ctx v in + let ed'' = subst_extern_desc (bsubst_subst bsub) ed' in + let ctx'' = match ed'' with + | ED_type dt -> + { ctx' with types = ctx'.types @ [ dt ] } + | _ -> ctx' in + (ctx'', Some { ed_name = ed.it.I.ed_name ; ed_desc = ed'' }) + +and raise_fvs (fv : free_tyvar) : def_type + = let raise_o o = if o > 0 then o - 1 else + raise (Invalid (no_region, + "Component type may not refer to non-" + ^ "imported uvar")) + in + DT_var (TV_free (match fv with + | FTV_uvar (o, i) -> FTV_uvar (raise_o o, i) + | FTV_evar (o, i) -> FTV_evar (raise_o o, i))) + +(* todo: check for uniqueness of names *) +and finish_instance_type_ (ctx : ctx) (decls : extern_decl list) : instance_type + = let esubst = List.init (List.length ctx.evars) (fun i -> Some (DT_var (TV_bound i))) in + let subst = esubst_subst [esubst] in + { it_evars = List.map (fun (t, _) -> t) (List.rev ctx.evars) + ; it_exports = List.map (subst_extern_decl subst) decls + } + +and finish_instance_type (ctx : ctx) (decls : extern_decl list) : instance_type + = let it = finish_instance_type_ ctx decls in + let subst = fsubst_subst raise_fvs in + { it_evars = it.it_evars + ; it_exports = List.map (subst_extern_decl subst) it.it_exports + } + +and elab_instance_type (ctx : ctx) (it : I.instance_type) : instance_type + = let rec go ctx ds = match ds with + | [] -> (ctx, []) + | d::ds -> + let ctx', d' = elab_instance_decl ctx d in + let ctx'', ds' = go ctx' ds in + match d' with + | None -> ctx'', ds' + | Some d' -> ctx'', d'::ds' in + let ctx', ds' = go (empty_ctx (Some ctx) false) it.it in + finish_instance_type ctx' ds' + +and instance_to_context (ctx : ctx) (live : bool) (imported : bool) + (it : instance_type) : ctx + = let ctx', bsubst = bound_to_uvars ctx imported it.it_evars in + let ct_exports = + List.map (fun x -> make_live_ live + (subst_extern_decl (bsubst_subst bsubst) x)) + it.it_exports in + ({ ctx' with + instances = ctx'.instances @ [ { itad_exports = ct_exports } ] }) + +and make_live_ : 'a. bool -> 'a -> 'a alive_dead + = fun l a -> { ad_contents = a; ad_live = l } + +and make_live : 'a. 'a -> 'a alive_dead + = fun a -> make_live_ true a + +and add_extern_desc_to_ctx (ctx : ctx) (live : bool) (imported : bool) (ed : extern_desc) : ctx + = match ed with + | ED_core_module cmt -> + { ctx with + core_ctx = { ctx.core_ctx with + core_modules = ctx.core_ctx.core_modules @ [ cmt ] } } + | ED_func ft -> + { ctx with funcs = ctx.funcs @ [ ft ] } + | ED_value vt -> + { ctx with values = ctx.values @ [ make_live_ live vt ] } + | ED_type dt -> + { ctx with types = ctx.types @ [ dt ] } + | ED_instance it -> + instance_to_context ctx live imported it + | ED_component ct -> + { ctx with components = ctx.components @ [ ct ] } + +and elab_component_decl (ctx : ctx) (cd : I.component_decl) + : ctx * extern_decl option * extern_decl option + = match cd.it with + | I.Component_import id -> + let v, ed' = elab_extern_desc ctx id.it.I.id_type in + let ctx', bsub = bound_to_uvars ctx true v in + let ed'' = subst_extern_desc (bsubst_subst bsub) ed' in + (add_extern_desc_to_ctx ctx' true true ed'' + ,Some { ed_name = id.it.I.id_name ; ed_desc = ed'' }, None) + | I.Component_instance id -> + let ctx', export = elab_instance_decl ctx id in + (ctx', None, export) + +and finish_component_type (ctx : ctx) (is : extern_decl list) (es : extern_decl list) : component_type + = let it = finish_instance_type_ ctx es in + let rec mk_usubst_uvars bidx uvars = match uvars with + | [] -> ([], []) + | (x, true)::xs -> + let us, uv = mk_usubst_uvars (bidx + 1) xs in + (Some (DT_var (TV_bound bidx))::us, x::uv) + | (_, false)::xs -> mk_usubst_uvars bidx xs in + let usubst, uvars = mk_usubst_uvars 0 ctx.uvars in + let subst = { (usubst_subst [usubst]) with fvar_sub = raise_fvs } in + { ct_uvars = List.rev uvars + ; ct_imports = List.map (subst_extern_decl subst) is + ; ct_instance = subst_instance_type subst it + } + +and elab_def_type (ctx : ctx) (dt : I.def_type) : def_type + = match dt.it with + | I.Deftype_val dvt -> DT_val_type (elab_def_val_type ctx dvt) + | I.Deftype_func ft -> DT_func_type (elab_func_type ctx ft) + | I.Deftype_inst it -> DT_instance_type (elab_instance_type ctx it) + | I.Deftype_comp ct -> DT_component_type (elab_component_type ctx ct) + | I.Deftype_rsrc _ -> + raise (Invalid (dt.at, + "Resource type declaration can't appear here")) + +and build_component_type : 'a. (ctx -> 'a -> ctx * extern_decl option * extern_decl option) -> (ctx -> unit) -> ctx -> bool -> 'a list -> component_type + = fun f ff ctx ob ds -> + let rec go ctx ds = match ds with + | [] -> (ctx, [], []) + | d::ds -> + let ctx', id, ed = f ctx d in + let ctx'', is, es = go ctx' ds in + let is' = match id with + | None -> is + | Some i -> i::is in + let es' = match ed with + | None -> es + | Some e -> e::es in + ctx'', is', es' in + let ctx', is, es = go (empty_ctx (Some ctx) ob) ds in + ff ctx'; + finish_component_type ctx' is es + + +and elab_component_type (ctx : ctx) (ct : I.component_type) : component_type + = build_component_type elab_component_decl (fun _ -> ()) ctx false ct.it diff --git a/interpreter/valid/etype_pp.ml b/interpreter/valid/etype_pp.ml new file mode 100644 index 00000000..79f1aab4 --- /dev/null +++ b/interpreter/valid/etype_pp.ml @@ -0,0 +1,290 @@ +open Wasm.Source + +open Etypes +open Ast + +let pp_indent : int ref = ref 0 +let pp_wrap : int ref = ref 80 +let pp_pos : int ref = ref 0 +let pp_linum : int ref = ref 0 +type pp_var_ctx = + { pvc_parent : pp_var_ctx option + ; pvc_uvars : string list + ; pvc_evars : string list + ; pvc_bvars : string list + } +let empty_pp_var_ctx : pp_var_ctx + = { pvc_parent = None + ; pvc_uvars = [] + ; pvc_evars = [] + ; pvc_bvars = [] + } +let pp_vars : pp_var_ctx ref + = ref empty_pp_var_ctx +let pp_var_idx : int ref = ref 0 +let pp_output : string list ref = ref [] + +let _output s = pp_output := s::!pp_output + +let rec nr_codepoints n i s = + (* wrong, but good enough & doesn't require an external unicode library *) + if i >= String.length s + then n + else + let ud = String.get_utf_8_uchar s 0 in + nr_codepoints (n+1) (i+Uchar.utf_decode_length ud) s + +let emit_newline s = + pp_pos := !pp_indent + nr_codepoints 0 0 s; + pp_linum := !pp_linum + 1; + _output "\n"; + _output (String.make !pp_indent ' '); + _output s + +let emit_ s = + let orig_pos = !pp_pos in + let new_pos = orig_pos + nr_codepoints 0 0 s in + if new_pos >= !pp_wrap + then (emit_newline s; !pp_indent) + else (pp_pos := new_pos; _output s; orig_pos) + +let emit s = + let _ = emit_ s in () + +let emit_indent_begin s f = + let orig_indent = !pp_indent in + let orig_pos = emit_ s in + pp_indent := orig_pos; + f (); + pp_indent := orig_indent + +let with_indent_here f = + let orig_indent = !pp_indent in + pp_indent := !pp_pos; + f (); + pp_indent := orig_indent + +let emit_indent_end s f = + emit s; + with_indent_here f + +let rec emit_list sep f xs = + match xs with + | [] -> () + | x::xs -> + let orig_linum = !pp_linum in + with_indent_here (fun () -> f x); + if !pp_linum <> orig_linum + then emit_newline sep + else emit sep; + emit_list sep f xs + +let emit_bracketed_list start stop sep f xs = + let old_line = !pp_linum in + emit_indent_begin start + (fun () -> + emit_list sep f xs; + if !pp_linum <> old_line + then emit_newline stop + else emit stop) + + +let pp_begin () = + pp_linum := 0; + pp_pos := 0; + pp_wrap := 60; + pp_indent := 2; + pp_vars := empty_pp_var_ctx; + pp_var_idx := 0; + pp_output := [] +let pp_end () = + let out = String.concat "" (List.rev !pp_output) in + pp_output := []; out +let pp_string f = + pp_begin (); + f (); + pp_end () + +let pp_line f = + print_endline (pp_string f) + +let pp_debug prefix f = + pp_line (fun () -> emit prefix; emit ": "; f ()) + +let emit_core_extern_desc (ctx : ctx) (ced : core_extern_desc) : unit + = emit (Wasm.Types.string_of_extern_type ced) + +let emit_core_export_decl (ctx : ctx) (ced : core_export_decl) : unit + = emit ced.ced_name.it; emit " "; + emit_indent_end ": " (fun () -> + emit_core_extern_desc ctx ced.ced_desc) + +let emit_core_export_decls (ctx : ctx) (ceds : core_export_decl list) : unit + = emit_bracketed_list "{ " "} " "; " (emit_core_export_decl ctx) ceds + +let emit_core_import_decls (ctx : ctx) (ceds : core_import_decl list) : unit + = () + +let emit_core_instance_type (ctx : ctx) (cit : core_instance_type) : unit + = emit_core_export_decls ctx cit.cit_exports + +let emit_core_module_type (ctx : ctx) (cmt : core_module_type) : unit + = () + +let emit_val_int_size (ctx : ctx) (vis : val_int_size) : unit + = match vis with + | VI_8 -> emit "8 " + | VI_16 -> emit "16 " + | VI_32 -> emit "32 " + | VI_64 -> emit "64 " +let emit_val_float_size (ctx : ctx) (vis : val_float_size) : unit + = match vis with + | VF_32 -> emit "32 " + | VF_64 -> emit "64 " + + +let rec emit_val_type (ctx : ctx) (vt : val_type) : unit + = match vt with + | Bool -> emit "bool " + | Signed i -> emit "s"; emit_val_int_size ctx i + | Unsigned i -> emit "u"; emit_val_int_size ctx i + | Float f -> emit "f"; emit_val_float_size ctx f + | Char -> emit "char " + | List vt -> + emit_indent_end "list(" (fun () -> emit_val_type ctx vt; emit ") ") + | Record rfs -> + emit_bracketed_list "{ " "} " "; " (emit_record_field ctx) rfs + | Variant vcs -> + emit_bracketed_list "< " "> " "| " (emit_variant_case ctx) vcs + | Own dt -> + emit_indent_end "own(" (fun () -> emit_def_type ctx dt; emit ") ") + | Borrow dt -> + emit_indent_end "borrow(" (fun () -> emit_def_type ctx dt; emit ") ") +and emit_record_field (ctx : ctx) (rf : record_field) : unit + = emit rf.rf_name.it; emit " "; + emit_indent_end ": " (fun () -> emit_val_type ctx rf.rf_type) +and emit_variant_case (ctx : ctx) (vc : variant_case) : unit + = emit vc.vc_name.it; + (match vc.vc_default with + | None -> emit " " + | Some d -> emit "("; emit (Int32.to_string d); emit ") "); + (match vc.vc_type with + | None -> () + | Some vt -> emit_indent_end ": " (fun () -> emit_val_type ctx vt)); + +and emit_func_io (ctx : ctx) (fio : func_ios) : unit + = match fio with + | Fio_one vt -> emit_val_type ctx vt + | Fio_many nvts -> + emit_bracketed_list "[ " "] " "; " + (fun (n, vt) -> emit n.it; emit " "; + emit_indent_end ": " (fun () -> + emit_val_type ctx vt)) + nvts + +and emit_func_type (ctx : ctx) (ft : func_type) : unit + = emit_func_io ctx ft.ft_params; emit "-> "; emit_func_io ctx ft.ft_result + +and emit_def_type (ctx : ctx) (dt : def_type) : unit + = match dt with + | DT_var (TV_bound i) -> emit (List.nth !pp_vars.pvc_bvars i) + | DT_var (TV_free (FTV_evar (o, i))) -> + emit_indent_end "evar(" (fun () -> + emit (string_of_int o); emit ", "; emit (string_of_int i); emit ")") + | DT_var (TV_free (FTV_uvar (o, i))) -> + emit_indent_end "uvar(" (fun () -> + emit (string_of_int o); emit ", "; emit (string_of_int i); emit ")") + | DT_resource_type idx -> + emit_indent_end "resource " (fun () -> emit (Int32.to_string idx)) + | DT_val_type vt -> emit_val_type ctx vt + | DT_func_type ft -> emit_func_type ctx ft + | DT_instance_type it -> emit_instance_type ctx it + | DT_component_type ct -> emit_component_type ctx ct + +and emit_extern_desc (ctx : ctx) (ed : extern_desc) : unit + = match ed with + | ED_core_module cmt -> emit_core_module_type ctx cmt + | ED_func ft -> emit_func_type ctx ft + | ED_value vt -> emit_val_type ctx vt + | ED_type dt -> emit_def_type ctx dt + | ED_instance it -> emit_instance_type ctx it + | ED_component ct -> emit_component_type ctx ct + +and emit_extern_decl (ctx : ctx) (ed : extern_decl) : unit + = emit ed.ed_name.it.en_name.it; emit " "; + emit_indent_end ": " (fun () -> emit_extern_desc ctx ed.ed_desc) + +and emit_extern_decls (ctx : ctx) (eds : extern_decl list) : unit + = emit_bracketed_list "{ " "} " "; " (emit_extern_decl ctx) eds + +and next_var_name () : string + = let next_idx = !pp_var_idx + 1 in + pp_var_idx := next_idx; + "α" ^ string_of_int next_idx + +and emit_type_bound (ctx : ctx) (tb : type_bound) : unit + = match tb with + | Tbound_eq dt -> + emit_indent_end "eq " (fun () -> emit_def_type ctx dt) + | Tbound_subr -> emit "sub resource" + +and emit_bound_var (ctx : ctx) (v : boundedtyvar) : unit + = let var = next_var_name () in + pp_vars := { !pp_vars with pvc_bvars = var::!pp_vars.pvc_bvars }; + emit_indent_begin "(" (fun () -> + with_indent_here (fun () -> emit var); + emit_indent_end ": " (fun () -> emit_type_bound ctx v); + emit ")") + +and emit_bound_vars (ctx : ctx) (vs : boundedtyvar list) : unit + = emit_list " " (emit_bound_var ctx) vs + +and emit_instance_type (ctx : ctx) (it : instance_type) : unit + = emit_indent_begin "∃ " (fun () -> + let old_vars = !pp_vars in + with_indent_here (fun () -> emit_bound_vars ctx it.it_evars); + emit ". "; + with_indent_here (fun () -> emit_extern_decls ctx it.it_exports); + pp_vars := old_vars) + +and emit_component_type (ctx : ctx) (ct : component_type) : unit + = emit_indent_begin "∀ " (fun () -> + let old_vars = !pp_vars in + with_indent_here (fun () -> emit_bound_vars ctx ct.ct_uvars); + emit ". "; + with_indent_here (fun () -> emit_extern_decls ctx ct.ct_imports); + emit "→ "; + emit_instance_type ctx ct.ct_instance; + pp_vars := old_vars) + +let pp_core_extern_desc ctx x = + pp_string (fun () -> emit_core_extern_desc ctx x) + +let pp_core_export_decl ctx x = + pp_string (fun () -> emit_core_export_decl ctx x) + +let pp_core_export_decls ctx x = + pp_string (fun () -> emit_core_export_decls ctx x) + +let pp_core_import_decls ctx x = + pp_string (fun () -> emit_core_import_decls ctx x) + +let pp_core_instance_type ctx x = + pp_string (fun () -> emit_core_instance_type ctx x) + +let pp_val_type ctx x = + pp_string (fun () -> emit_val_type ctx x) + +let pp_def_type ctx x = + pp_string (fun () -> emit_def_type ctx x) + +let pp_extern_desc ctx x = + pp_string (fun () -> emit_extern_desc ctx x) + +let pp_extern_decls ctx x = + pp_string (fun () -> emit_extern_decls ctx x) + +let pp_instance_type ctx x = + pp_string (fun () -> emit_instance_type ctx x) + +let pp_component_type ctx x = pp_string (fun () -> emit_component_type ctx x) diff --git a/interpreter/valid/etypes.ml b/interpreter/valid/etypes.ml new file mode 100644 index 00000000..2a883cf3 --- /dev/null +++ b/interpreter/valid/etypes.ml @@ -0,0 +1,145 @@ +open Ast + +exception Invalid of Source.region * string + +type bound_tyvar = int (* de bruijn index *) +type free_tyvar = + | FTV_uvar of int * int + | FTV_evar of int * int +type tyvar = + | TV_bound of bound_tyvar + | TV_free of free_tyvar + +type 'a alive_dead = { ad_contents : 'a ; ad_live : bool } + +type val_type = + | Bool + | Signed of val_int_size | Unsigned of val_int_size + | Float of val_float_size + | Char + | List of val_type + | Record of record_field list + | Variant of variant_case list + | Own of def_type + | Borrow of def_type +and record_field = + { + rf_name : name; + rf_type : val_type; + } +and variant_case = + { + vc_name : name; + vc_type : val_type option; + vc_default : int32 option; + } +and val_type_ad = val_type alive_dead + +and func_ios = + | Fio_one of val_type + | Fio_many of (name * val_type) list +and func_type = { ft_params : func_ios; ft_result : func_ios } + +and type_bound = + | Tbound_eq of def_type + | Tbound_subr +and boundedtyvar = type_bound + +and instance_type = + { it_evars : boundedtyvar list ; it_exports : extern_decl list } +and instance_type_ad = + { itad_exports : extern_decl_ad list } +and extern_decl = + { ed_name : externname ; ed_desc : extern_desc } +and extern_decl_ad = extern_decl alive_dead +and extern_desc = + | ED_core_module of core_module_type + | ED_func of func_type + | ED_value of val_type + | ED_type of def_type + | ED_instance of instance_type + | ED_component of component_type +and component_type = + { ct_uvars : boundedtyvar list + ; ct_imports : extern_decl list + ; ct_instance : instance_type } +and resource_type = + { rt_dtor : int32 option } + +and def_type = + | DT_var of tyvar + | DT_resource_type of int32 + | DT_val_type of val_type + | DT_func_type of func_type + | DT_instance_type of instance_type + | DT_component_type of component_type + +and core_func_type = Wasm.Types.func_type +and core_extern_desc = Wasm.Types.extern_type +and core_export_decl = + { ced_name : name ; ced_desc : core_extern_desc } +and core_instance_type = + { cit_exports : core_export_decl list } +and core_import_decl = + { cid_name1 : name ; cid_name2 : name ; cid_desc : core_extern_desc } +and core_module_type = + { cmt_imports : core_import_decl list ; cmt_instance : core_instance_type } +and core_table_type = Wasm.Types.table_type +and core_mem_type = Wasm.Types.memory_type +and core_global_type = Wasm.Types.global_type + +type core_type = + | CT_func of core_func_type + | CT_module of core_module_type + | CT_instance of core_instance_type + | CT_table of core_table_type + | CT_memory of core_mem_type + | CT_global of core_global_type + +type core_ctx = + { core_types : core_type list + ; core_funcs : core_func_type list + ; core_modules : core_module_type list + ; core_instances : core_instance_type list + ; core_tables : core_table_type list + ; core_mems : core_mem_type list + ; core_globals : core_global_type list + } + +type ctx = + { parent_ctx : ctx option + ; outer_boundary : bool (* should type variables from the parent be blocked? *) + ; core_ctx : core_ctx + ; uvars : (boundedtyvar * bool) list + ; evars : (boundedtyvar * def_type option) list + ; rtypes : resource_type list + ; types : def_type list + ; components : component_type list + ; instances : instance_type_ad list + ; funcs : func_type list + ; values : val_type_ad list + } + +let empty_core_ctx () = + { core_types = [] + ; core_funcs = [] + ; core_modules = [] + ; core_instances = [] + ; core_tables = [] + ; core_mems = [] + ; core_globals = [] + } + +let empty_ctx parent ob = + { parent_ctx = parent + ; outer_boundary = ob + ; core_ctx = empty_core_ctx () + ; uvars = [] + ; evars = [] + ; rtypes = [] + ; types = [] + ; components = [] + ; instances = [] + ; funcs = [] + ; values = [] + } diff --git a/interpreter/valid/substitute.ml b/interpreter/valid/substitute.ml new file mode 100644 index 00000000..30ec74de --- /dev/null +++ b/interpreter/valid/substitute.ml @@ -0,0 +1,131 @@ +open Etypes + +type bsubst = def_type option list +type esubst = (def_type option list) list +type usubst = (def_type option list) list +type fsubst = free_tyvar -> def_type (* called on fvars not caught by esubst/usubst *) +type subst = + { bvar_sub : bsubst + ; evar_sub : esubst + ; uvar_sub : usubst + ; fvar_sub : fsubst + } + +let empty_fvar_sub (fv : free_tyvar) : def_type + = DT_var (TV_free fv) + +let bsubst_subst (bs : bsubst) : subst + = { bvar_sub = bs ; evar_sub = [] ; uvar_sub = []; fvar_sub = empty_fvar_sub } +let esubst_subst (es : esubst) : subst + = { bvar_sub = [] ; evar_sub = es ; uvar_sub = []; fvar_sub = empty_fvar_sub } +let usubst_subst (us : usubst) : subst + = { bvar_sub = [] ; evar_sub = [] ; uvar_sub = us; fvar_sub = empty_fvar_sub } +let fsubst_subst (fs : fsubst) : subst + = { bvar_sub = [] ; evar_sub = [] ; uvar_sub = []; fvar_sub = fs } + + +(* so if i do bound_to_evars ctx [bound1 bound2] + * then i want to end up with either + * ctx ++ { evars bound1 bound2 }, 0 -> ctx.evars.length + 1, 1 -> ctx.evars.length + * or + * ctx ++ { evars bound2 bound1 }, 0 -> ctx.evars.length, 1 -> ctx.evars.length + 1 + *) + +let rec bound_to_evars (ctx : ctx) (vs : boundedtyvar list) : ctx * bsubst + = match vs with + | [] -> (ctx, []) + | v::vs' -> + let ctx', sub = bound_to_evars { ctx with evars = ctx.evars @ [(v, None)] } vs' in + (ctx', sub @ [Some (DT_var (TV_free (FTV_evar (0, List.length ctx.evars))))]) + +let rec bound_to_uvars (ctx : ctx) (imported : bool) + (vs : boundedtyvar list) : ctx * bsubst + = match vs with + | [] -> (ctx, []) + | v::vs' -> + let ctx', sub = bound_to_uvars { ctx with + uvars = ctx.uvars @ [(v, imported)] } imported vs' in + (ctx', sub @ [Some (DT_var (TV_free (FTV_uvar (0, List.length ctx.uvars))))]) + +let rec subst_val_type (s : subst) (vt : val_type) : val_type + = match vt with + | Bool -> Bool + | Signed s -> Signed s + | Unsigned u -> Unsigned u + | Float f -> Float f + | Char -> Char + | List vt -> List (subst_val_type s vt) + | Record rfs -> Record (List.map (subst_record_field s) rfs) + | Variant vcs -> Variant (List.map (subst_variant_case s) vcs) + | Own dt -> Own (subst_def_type s dt) + | Borrow dt -> Borrow (subst_def_type s dt) + +and subst_record_field (s : subst) (rf : record_field) : record_field + = { rf_name = rf.rf_name ; rf_type = subst_val_type s rf.rf_type } + +and subst_variant_case (s : subst) (vc : variant_case) : variant_case + = { vc_name = vc.vc_name + ; vc_type = Option.map (subst_val_type s) vc.vc_type + ; vc_default = vc.vc_default } + +and subst_func_ios (s : subst) (fio : func_ios) : func_ios + = match fio with + | Fio_one vt -> Fio_one (subst_val_type s vt) + | Fio_many nvts -> + Fio_many (List.map (fun (n, vt) -> (n, subst_val_type s vt)) nvts) + +and subst_func_type (s : subst) (ft : func_type) : func_type + = { ft_params = subst_func_ios s ft.ft_params + ; ft_result = subst_func_ios s ft.ft_result } + +and subst_def_type (s : subst) (dt : def_type) : def_type + = match dt with + | DT_var (TV_bound n) -> + (try match List.nth s.bvar_sub n with + | None -> dt + | Some dt' -> dt' + with Failure _ -> dt) + | DT_var (TV_free fv) -> + let not_explicit () = s.fvar_sub fv in + (try match fv with + | FTV_uvar (o, i) -> + (match List.nth (List.nth s.uvar_sub o) i with + | None -> not_explicit () + | Some dt' -> dt') + | FTV_evar (o, i) -> + (match List.nth (List.nth s.evar_sub o) i with + | None -> not_explicit () + | Some dt' -> dt') + with Failure _ -> not_explicit ()) + | DT_resource_type i -> DT_resource_type i + | DT_val_type vt -> DT_val_type (subst_val_type s vt) + | DT_func_type ft -> DT_func_type (subst_func_type s ft) + | DT_instance_type it -> DT_instance_type (subst_instance_type s it) + | DT_component_type ct -> DT_component_type (subst_component_type s ct) + +and subst_instance_type (s : subst) (it : instance_type) : instance_type + = let bs' = List.init (List.length it.it_evars) (fun _ -> None) in + let s' = { s with bvar_sub = bs' @ s.bvar_sub } in + { it_evars = it.it_evars + ; it_exports = List.map (subst_extern_decl s') it.it_exports + } + +and subst_component_type (s : subst) (ct : component_type) : component_type + = let bs' = List.init (List.length ct.ct_uvars) (fun _ -> None) in + let s' = { s with bvar_sub = bs' @ s.bvar_sub } in + { ct_uvars = ct.ct_uvars + ; ct_imports = List.map (subst_extern_decl s') ct.ct_imports + ; ct_instance = subst_instance_type s' ct.ct_instance + } + +and subst_extern_desc (s : subst) (ed : extern_desc) : extern_desc + = match ed with + | ED_core_module cmt -> ED_core_module cmt + | ED_func ft -> ED_func (subst_func_type s ft) + | ED_value vt -> ED_value (subst_val_type s vt) + | ED_type tt -> ED_type (subst_def_type s tt) + | ED_instance it -> ED_instance (subst_instance_type s it) + | ED_component ct -> ED_component (subst_component_type s ct) + +and subst_extern_decl (s : subst) (ed : extern_decl) : extern_decl + = { ed_name = ed.ed_name ; ed_desc = subst_extern_desc s ed.ed_desc } diff --git a/interpreter/valid/subtype.ml b/interpreter/valid/subtype.ml new file mode 100644 index 00000000..174cac4b --- /dev/null +++ b/interpreter/valid/subtype.ml @@ -0,0 +1,391 @@ +open Ast +open Wasm.Source +open Etypes +open Etype_pp +open Substitute + +let subtype_trace = true + +let subtype_err k s1 s2 + = raise (Invalid (no_region, "Could not show that " ^ k ^ " " ^ s1 ^ + + " is a subtype of " ^ s2)) + +let subtype_core_extern_desc (ctx : ctx) + (ed1 : core_extern_desc) (ed2 : core_extern_desc) : unit + = if Wasm.Types.match_extern_type ed1 ed2 + then () + else subtype_err "core type" + (Wasm.Types.string_of_extern_type ed1) + (Wasm.Types.string_of_extern_type ed2) + +let subtype_core_export_decls' (ctx : ctx) + (ceds1 : core_export_decl list) (ced2 : core_export_decl) : unit + = try + let ced1 = List.find (fun x -> x.ced_name.it = ced2.ced_name.it) ceds1 in + subtype_core_extern_desc ctx ced1.ced_desc ced2.ced_desc + with Not_found -> + raise (Invalid (no_region, + pp_string (fun () -> + emit "No extern desc named "; + emit ced2.ced_name.it; + emit " in "; + emit_core_export_decls ctx ceds1))) + +let subtype_core_export_decls (ctx : ctx) + (ceds1 : core_export_decl list) (ceds2 : core_export_decl list) : unit + = List.iter (subtype_core_export_decls' ctx ceds1) ceds2 + +let subtype_core_instance_type (ctx : ctx) + (cit1 : core_instance_type) (cit2 : core_instance_type) : unit + = subtype_core_export_decls ctx cit1.cit_exports cit2.cit_exports + +let subtype_core_import_decls' (ctx : ctx) + (cids1 : core_import_decl list) (cid2 : core_import_decl) : unit + = try + let cid1 = List.find (fun x -> x.cid_name1.it = cid2.cid_name1.it + && x.cid_name2.it = cid2.cid_name2.it) + cids1 in + subtype_core_extern_desc ctx cid1.cid_desc cid2.cid_desc + with Not_found -> + raise (Invalid (no_region, + pp_string (fun () -> + emit "No extern desc named "; + emit cid2.cid_name1.it; + emit "."; + emit cid2.cid_name2.it; + emit " in "; + emit_core_import_decls ctx cids1))) + +let subtype_core_import_decls (ctx : ctx) + (cids1 : core_import_decl list) (cids2 : core_import_decl list) : unit + = List.iter (subtype_core_import_decls' ctx cids1) cids2 + +let subtype_core_module_type (ctx : ctx) + (cmt1 : core_module_type) (cmt2 : core_module_type) : unit + = subtype_core_import_decls ctx cmt2.cmt_imports cmt1.cmt_imports; + subtype_core_instance_type ctx cmt1.cmt_instance cmt2.cmt_instance + +type resolved_tyvar = + | RTV_definite of def_type + | RTV_bound of int + | RTV_evar of int * int * type_bound + | RTV_uvar of int * int * type_bound + +let rec resolve_tyvar (ctx : ctx) (tv : tyvar) : resolved_tyvar + = let rec lookup_uvar ctx o i = + match o with + | 0 -> (match List.nth ctx.uvars i with + | (Tbound_eq dt, _) -> Either.Left dt + | (tb, _) -> Either.Right tb) + | _ -> (match ctx.parent_ctx with + | Some ctx' -> lookup_uvar ctx' (o - 1) i + | None -> raise (Invalid (no_region, "Uvar refers to non-existent outer component"))) + in + let rec lookup_evar ctx o i = + match o with + | 0 -> (match List.nth ctx.evars i with + | (_, Some dt) -> Either.Left dt + | (Tbound_eq dt, None) -> Either.Left dt + | (tb, None) -> Either.Right tb) + | _ -> (match ctx.parent_ctx with + | Some ctx' -> lookup_evar ctx' (o - 1) i + | None -> raise (Invalid (no_region, "Evar refers to non-existent outer component"))) + in + let resolve_deftype_tyvar d = + match d with + | DT_var tv -> resolve_tyvar ctx tv + | _ -> RTV_definite d + in + match tv with + | TV_bound b -> RTV_bound b + | TV_free (FTV_evar (o, i)) -> + (match lookup_evar ctx o i with + | Either.Left d -> resolve_deftype_tyvar d + | Either.Right tb -> RTV_evar (o, i, tb)) + | TV_free (FTV_uvar (o, i)) -> + (match lookup_uvar ctx o i with + | Either.Left d -> resolve_deftype_tyvar d + | Either.Right tb -> RTV_uvar (o, i, tb)) + +let rec subtype_val_type (ctx : ctx) + (vt1 : val_type) (vt2 : val_type) : unit + = match vt1, vt2 with + | Bool, Bool -> () + | Signed s1, Signed s2 + | Unsigned s1, Unsigned s2 -> + if s1 = s2 then () + else subtype_err "val type" (pp_val_type ctx vt1) (pp_val_type ctx vt2) + | Float f1, Float f2 -> + if f1 = f2 then () + else subtype_err "val type" (pp_val_type ctx vt1) (pp_val_type ctx vt2) + | Char, Char -> () + | List vt1', List vt2' -> + subtype_val_type ctx vt1' vt2' + | Record rfs1, Record rfs2 -> + List.iter (fun rf2 -> + try + let rf1 = + List.find (fun rf1 -> rf1.rf_name.it = rf2.rf_name.it) rfs1 + in subtype_val_type ctx rf1.rf_type rf2.rf_type + with | Not_found -> + raise (Invalid (no_region, + "Could not find record field " + ^ rf2.rf_name.it ^ " in record type " + ^ pp_val_type ctx vt1))) rfs2 + | Variant vcs1, Variant vcs2 -> + List.iter (fun vc1 -> + try + let vc2 = + List.find (fun vc2 -> vc1.vc_name.it = vc2.vc_name.it) vcs2 + in subtype_val_type_option ctx vc1.vc_type vc2.vc_type + with | Not_found -> + raise (Invalid (no_region, + "Could not find variant case " + ^ vc1.vc_name.it ^ " in variant type " + ^ pp_val_type ctx vt2))) vcs1 + | Own dt1, Own dt2 -> + def_type_is_resource ctx dt1; + def_type_is_resource ctx dt2; + subtype_def_type ctx dt1 dt2 + | Borrow dt1, Borrow dt2 -> + def_type_is_resource ctx dt1; + def_type_is_resource ctx dt2; + subtype_def_type ctx dt1 dt2 + | _, _ -> subtype_err "val type" (pp_val_type ctx vt1) (pp_val_type ctx vt2) + +and subtype_val_type_option (ctx : ctx) + (vt1 : val_type option) (vt2 : val_type option) : unit + = match vt1, vt2 with + | None, None -> () + | None, Some vt -> raise (Invalid (no_region, + "Expected " ^ pp_val_type ctx vt + ^ ", got nothing.")) + | Some _, None -> () + | Some vt1, Some vt2 -> subtype_val_type ctx vt1 vt2 + +and subtype_func_ios (ctx : ctx) (fi1 : func_ios) (fi2 : func_ios) : unit + = match fi1, fi2 with + | Fio_one vt1, Fio_one vt2 -> subtype_val_type ctx vt1 vt2 + | Fio_many vts1, Fio_many vts2 -> + List.iter (fun (vn2, vt2) -> + try let (_, vt1) = List.find (fun (vn1, _) -> vn1.it = vn2.it) vts1 + in subtype_val_type ctx vt1 vt2 + with | Not_found -> + raise (Invalid (no_region, + "Could not find function argument " ^ vn2.it))) + vts2 + | _, _ -> + raise (Invalid (no_region, "Cannot match Fio_one against Fio_many")) + +and subtype_func_type (ctx : ctx) (ft1 : func_type) (ft2 : func_type) : unit + = subtype_func_ios ctx ft2.ft_params ft1.ft_params; + subtype_func_ios ctx ft1.ft_result ft2.ft_result + +and iibb_search_inst + (ctx : ctx) (exps : extern_decl list) (i : int) (ed : extern_decl) + = + let find_ed' () = + List.find (fun x -> x.ed_name.it.en_name.it = ed.ed_name.it.en_name.it) + exps in + match ed.ed_desc with + | ED_type (DT_var (TV_bound i')) when i = i' -> (* jackpot! *) + let ed' = find_ed' () in + (match ed'.ed_desc with + | ED_type dt -> Some dt + | _ -> raise (Invalid (ed'.ed_name.at, + "Cannot instantiate type import " + ^ ed.ed_name.it.en_name.it ^ "with non-type"))) + | ED_instance it -> + let ed' = find_ed' () in + (match ed'.ed_desc with + | ED_instance it' -> + List.find_map (iibb_search_inst ctx it'.it_exports (i + List.length it.it_evars)) + it.it_exports + | _ -> raise (Invalid (ed'.ed_name.at, + "Cannot instantiate instance import " + ^ ed.ed_name.it.en_name.it ^ "with non-instance"))) + | _ -> None + +and matchit_bvar_binding (ctx : ctx) + (es : extern_decl list) (is : extern_decl list) + (i : int) (v : boundedtyvar) + : def_type + = match v with + | Tbound_eq dt -> dt + | Tbound_subr -> + match List.find_map (iibb_search_inst ctx es i) is with + | None -> raise (Invalid (no_region, "!! Impossible: un-exported evar")) + | Some dt -> dt + +and matchit_bvar_bindings (ctx : ctx) + (es : extern_decl list) (it : instance_type) + : bsubst + = List.mapi (fun i v -> Some (matchit_bvar_binding ctx es it.it_exports i v)) + (List.rev it.it_evars) + +and match_instance_type (ctx : ctx) + (es : extern_decl list) (it : instance_type) + : bsubst + = if subtype_trace + then (emit_extern_decls ctx es; + emit_newline " <: "; + with_indent_here (fun () -> emit_instance_type ctx it); + emit_newline ""); + let evar_insts = matchit_bvar_bindings ctx es it in + let es' = List.map (subst_extern_decl (bsubst_subst evar_insts)) + it.it_exports in + subtype_extern_decls ctx es es'; + evar_insts + +and subtype_instance_type (ctx : ctx) + (it1 : instance_type) (it2 : instance_type) + : unit + = if subtype_trace + then (emit_instance_type ctx it1; + emit_newline " <: "; + with_indent_here (fun () -> emit_instance_type ctx it2); + emit_newline ""); + let ctx', bsubst = bound_to_uvars ctx false it1.it_evars in + let it1es + = List.map (subst_extern_decl (bsubst_subst bsubst)) it1.it_exports in + let _ = match_instance_type ctx' it1es it2 in + () + +and subtype_component_type (ctx : ctx) + (ct1 : component_type) (ct2 : component_type) + : unit + = if subtype_trace + then (emit_component_type ctx ct1; + emit_newline " <: "; + with_indent_here (fun () -> emit_component_type ctx ct2); + emit_newline ""); + let ctx', bsubst = bound_to_uvars ctx false ct2.ct_uvars in + let ct2imes = + List.map (subst_extern_decl (bsubst_subst bsubst)) ct2.ct_imports in + let ct2in' = + subst_instance_type (bsubst_subst bsubst) ct2.ct_instance in + let ct1im' = { it_evars = ct1.ct_uvars; it_exports = ct1.ct_imports } in + let ct1subst = match_instance_type ctx' ct2imes ct1im' in + let ct1in' = subst_instance_type (bsubst_subst ct1subst) ct1.ct_instance in + subtype_instance_type ctx' ct1in' ct2in' + +and subtype_var_var (ctx : ctx) (v1 : tyvar) (v2 : tyvar) : unit + = match resolve_tyvar ctx v1, resolve_tyvar ctx v2 with + | RTV_definite dt1, RTV_definite dt2 -> + subtype_def_type ctx dt1 dt2 + | RTV_uvar (o1, i1, _), RTV_uvar (o2, i2, _) -> + if o1 = o2 && i1 = i2 + then () + else raise (Invalid (no_region, + pp_string (fun () -> + emit "Type variable "; + emit ("u" ^ string_of_int o1 ^ "." + ^ string_of_int i1); + emit " is not "; + emit ("u" ^ string_of_int o2 ^ "." + ^ string_of_int i2)))) + | RTV_evar (o1, i1, _), RTV_evar (o2, i2, _) -> + if o1 = o2 && i1 = i2 + then () + else raise (Invalid (no_region, + pp_string (fun () -> + emit "Type variable "; + emit ("e" ^ string_of_int o1 ^ "." + ^ string_of_int i1); + emit " is not "; + emit ("e" ^ string_of_int o2 ^ "." + ^ string_of_int i2)))) + | RTV_bound _, _ + | _, RTV_bound _ -> + raise (Invalid (no_region, "!! Impossible: extra bvar in subtype_var")) + | _, _ -> + raise (Invalid (no_region, "Variable is not subtype")) + +and subtype_var_def_type (ctx : ctx) (tv : tyvar) (dt : def_type) : unit + = match resolve_tyvar ctx tv with + | RTV_definite dt' -> subtype_def_type ctx dt' dt + | _ -> raise (Invalid (no_region, "Variable cannot match def_type")) +and subtype_def_type_var (ctx : ctx) (dt : def_type) (tv : tyvar) : unit + = match resolve_tyvar ctx tv with + | RTV_definite dt' -> subtype_def_type ctx dt dt' + | _ -> raise (Invalid (no_region, "Variable cannot match def_type")) + +and subtype_def_type (ctx : ctx) (dt1 : def_type) (dt2 : def_type) : unit + = match dt1, dt2 with + | DT_var tv1, DT_var tv2 -> subtype_var_var ctx tv1 tv2 + | DT_var tv, _ -> subtype_var_def_type ctx tv dt2 + | _, DT_var tv -> subtype_def_type_var ctx dt1 tv + | DT_resource_type i1, DT_resource_type i2 -> + if i1 = i2 then () + else raise (Invalid (no_region, "Resource type " ^ Int32.to_string i1 + ^ " is not " ^ Int32.to_string i2)) + | DT_val_type vt1, DT_val_type vt2 -> subtype_val_type ctx vt1 vt2 + | DT_func_type ft1, DT_func_type ft2 -> subtype_func_type ctx ft1 ft2 + | DT_instance_type it1, DT_instance_type it2 -> + subtype_instance_type ctx it1 it2 + | DT_component_type ct1, DT_component_type ct2 -> + subtype_component_type ctx ct1 ct2 + | _, _ -> raise (Invalid (no_region, "Def type " ^ pp_def_type ctx dt1 + ^ " is not of the same sort as " + ^ pp_def_type ctx dt2)) + +and subtype_extern_desc (ctx : ctx) + (ed1 : extern_desc) (ed2 : extern_desc) + : unit + = match ed1, ed2 with + | ED_core_module cmt1, ED_core_module cmt2 -> + subtype_core_module_type ctx cmt1 cmt2 + | ED_func ft1, ED_func ft2 -> + subtype_func_type ctx ft1 ft2 + | ED_value vt1, ED_value vt2 -> + subtype_val_type ctx vt1 vt2 + | ED_type dt1, ED_type dt2 -> + subtype_def_type ctx dt1 dt2 (* TODO CHECK - this should be right + though, I think *) + | ED_instance it1, ED_instance it2 -> + subtype_instance_type ctx it1 it2 + | ED_component ct1, ED_component ct2 -> + subtype_component_type ctx ct1 ct2 + | _, _ -> raise (Invalid (no_region, "Extern desc " + ^ pp_extern_desc ctx ed1 + ^ " is not of the same sort as " + ^ pp_extern_desc ctx ed2)) + +and subtype_extern_decls' (ctx : ctx) + (eds1 : extern_decl list) (ed2 : extern_decl) + : unit + = try + let ed1 = List.find (fun x -> x.ed_name.it.en_name.it = ed2.ed_name.it.en_name.it) eds1 in + subtype_extern_desc ctx ed1.ed_desc ed2.ed_desc + with Not_found -> + raise (Invalid (no_region, + pp_string (fun () -> + emit "No extern desc named "; + emit ed2.ed_name.it.en_name.it; + emit " in "; + emit_extern_decls ctx eds1))) +and subtype_extern_decls (ctx : ctx) + (eds1 : extern_decl list) (eds2 : extern_decl list) + : unit + = if subtype_trace + then (emit_extern_decls ctx eds1; + emit_newline " <: "; + with_indent_here (fun () -> emit_extern_decls ctx eds2); + emit_newline ""); + List.iter (subtype_extern_decls' ctx eds1) eds2 + +and def_type_is_resource (ctx : ctx) (dt : def_type) : unit + = match dt with + | DT_var tv -> + (match resolve_tyvar ctx tv with + | RTV_definite dt' -> def_type_is_resource ctx dt' + | RTV_bound _ -> + raise (Invalid (no_region, "!! Impossible: extra bvar in dtir")) + | RTV_uvar (_, _, Tbound_subr) -> () + | RTV_evar (_, _, Tbound_subr) -> () + | _ -> raise (Invalid (no_region, + "Tyvar does not resolve to resource type"))) + | DT_resource_type i -> () + | _ -> raise (Invalid (no_region, "Def type " ^ pp_def_type ctx dt + ^ "is not resource type")) diff --git a/interpreter/valid/subtype.mli b/interpreter/valid/subtype.mli new file mode 100644 index 00000000..65a83272 --- /dev/null +++ b/interpreter/valid/subtype.mli @@ -0,0 +1,18 @@ +open Etypes + +val iibb_search_inst : ctx -> extern_decl list -> int -> extern_decl -> def_type option + +type resolved_tyvar = + | RTV_definite of def_type + | RTV_bound of int + | RTV_evar of int * int * type_bound + | RTV_uvar of int * int * type_bound + +val resolve_tyvar : ctx -> tyvar -> resolved_tyvar + +val subtype_core_extern_desc : ctx -> core_extern_desc -> core_extern_desc -> unit + +val subtype_val_type : ctx -> val_type -> val_type -> unit +val subtype_val_type_option : ctx -> val_type option -> val_type option -> unit +val subtype_extern_desc : ctx -> extern_desc -> extern_desc -> unit +val def_type_is_resource : ctx -> def_type -> unit diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml new file mode 100644 index 00000000..cca3eb7b --- /dev/null +++ b/interpreter/valid/valid.ml @@ -0,0 +1,542 @@ +module Source = Wasm.Source +open Source +open Ast +open Etypes +open Etype_pp +open Elaborate +open Substitute +open Subtype +module I = Ast.IntAst + +exception Invalid = Etypes.Invalid + +module CA = Wasm.Ast + +let infer_core_import (ctx : ctx) (cmd : CA.module_) (i : CA.import) + : core_import_decl + = { cid_name1 = Wasm.Utf8.encode i.it.CA.module_name @@ i.at + ; cid_name2 = Wasm.Utf8.encode i.it.CA.item_name @@ i.at + ; cid_desc = Wasm.Ast.import_type cmd i + } +let infer_core_export (ctx : ctx) (cmd : CA.module_) (e : CA.export) + : core_export_decl + = { ced_name = Wasm.Utf8.encode e.it.CA.name @@ e.at + ; ced_desc = Wasm.Ast.export_type cmd e + } +let infer_core_module (ctx : ctx) (cmd : Wasm.Ast.module_) : core_module_type + = + { cmt_imports = List.map (infer_core_import ctx cmd) cmd.it.CA.imports + ; cmt_instance = { + cit_exports = List.map (infer_core_export ctx cmd) cmd.it.CA.exports + } + } + +let check_uniqueness_ : 'a. string -> ('a -> string) -> 'a phrase list -> 'a phrase -> unit + = fun err project all this -> + if (List.length + (List.filter (fun this' -> project this'.it = project this.it) all) + <> 1) + then raise (Invalid (this.at, err ^ project this.it)) + else () +let check_uniqueness : 'a. string -> ('a -> string) -> 'a phrase list -> unit + = fun err project all -> + List.iter (check_uniqueness_ err project all) all + +let find_core_instantiate_arg_named ctx cias name = + try List.find (fun cia -> cia.it.I.c_ia_name.it = name.it) cias + with Not_found -> + raise (Invalid (name.at, "Expected to find instantiate arg " ^ name.it)) +let find_core_export_named ctx cit name + = try List.find (fun ced -> ced.ced_name.it = name.it) cit.cit_exports + with Not_found -> + raise (Invalid (name.at, "Expected to find export " ^ name.it)) +let check_core_instantiate_import ctx cias cid + = let cia = find_core_instantiate_arg_named ctx cias cid.cid_name1 in + if (cia.it.I.c_ia_value.it.I.c_s_sort.it <> Ast.Core_instance) + then raise (Invalid (cia.at, "Only two-level imports are suported")) + else (); + let cit = List.nth ctx.core_ctx.core_instances + (Int32.to_int cia.it.I.c_ia_value.it.I.c_s_idx) in + let ced = find_core_export_named ctx cit cid.cid_name2 in + subtype_core_extern_desc ctx ced.ced_desc cid.cid_desc +let infer_core_export (ctx : ctx) (e : I.core_export) : core_export_decl + = { ced_name = e.it.I.c_e_name + ; ced_desc = + let i = Int32.to_int e.it.I.c_e_value.it.I.c_s_idx in + let open Wasm.Types in + match e.it.I.c_e_value.it.I.c_s_sort.it with + | Core_func -> ExternFuncType (List.nth ctx.core_ctx.core_funcs i) + | Core_table -> ExternTableType (List.nth ctx.core_ctx.core_tables i) + | Core_memory -> ExternMemoryType (List.nth ctx.core_ctx.core_mems i) + | Core_global -> ExternGlobalType (List.nth ctx.core_ctx.core_globals i) + | s -> raise (Invalid (e.at, "Cannot inline-export core sort " + ^ show_core_sort' s)) + } +let infer_core_instance (ctx : ctx) (es : I.core_export list) + : core_instance_type + = { cit_exports = List.map (infer_core_export ctx) es } +let infer_core_defn (ctx : ctx) (d : I.core_definition) + : ctx + = match d with + | I.CoreModuleDef cmd -> + let cmt = infer_core_module ctx cmd in + { ctx with + core_ctx = { ctx.core_ctx with + core_modules = ctx.core_ctx.core_modules @ [cmt] } } + | I.CoreInstanceDef { it = I.Core_instantiate_module (cmid, cias); + at = at } -> + let cmt = List.nth ctx.core_ctx.core_modules (Int32.to_int cmid) in + List.iter (check_core_instantiate_import ctx cias) cmt.cmt_imports; + check_uniqueness "Duplicate instantiate arg name " + (fun x -> x.I.c_ia_name.it) cias; + { ctx with + core_ctx = { ctx.core_ctx with + core_instances = ctx.core_ctx.core_instances + @ [cmt.cmt_instance]}} + | I.CoreInstanceDef { it = I.Core_instantiate_inline es ; _ } -> + check_uniqueness "Duplicate core export name " + (fun x -> x.I.c_e_name.it) es; + let i = infer_core_instance ctx es in + { ctx with + core_ctx = { ctx.core_ctx with + core_instances = ctx.core_ctx.core_instances @ [i] } } + | I.CoreTypeDef cdt -> + let t = elab_core_deftype_ ctx cdt in + { ctx with + core_ctx = { ctx.core_ctx with + core_types = ctx.core_ctx.core_types @ [t] } } + +let rec mark_dead_sort_idxs (ctx : ctx) (sis : I.sort_idx list) : ctx + = match sis with + | [] -> ctx + | si::sis' -> + let ii = Int32.to_int si.it.I.s_idx in + let ctx' = match si.it.I.s_sort.it with + | Value -> + { ctx with + values = + List.mapi (fun i vad -> + if i = ii + then (if not vad.ad_live + then raise (Invalid (si.at, "Cannot reuse dead value")) + else { vad with ad_live = false }) + else vad) ctx.values } + | Instance -> + { ctx with + instances = + List.mapi (fun i iad -> + if i = ii + then + { itad_exports = + List.map (mark_dead_ed si.at) iad.itad_exports } + else iad) ctx.instances } + | _ -> ctx + in mark_dead_sort_idxs ctx' sis' +let mark_dead_ias (ctx : ctx) (ias : I.instantiate_arg list) : ctx + = mark_dead_sort_idxs ctx (List.map (fun ia -> ia.it.I.ia_value) ias) +let mark_dead_ies (ctx : ctx) (ies : I.inline_export list) : ctx + = mark_dead_sort_idxs ctx (List.map (fun ie -> ie.it.I.ie_value) ies) + +let find_instantiate_arg_named (n : name) (ias : I.instantiate_arg list) + : I.instantiate_arg + = try List.find (fun ia -> ia.it.I.ia_name.it = n.it) ias + with Not_found -> + let at = match ias with | [] -> n.at | ia::_ -> ia.at in + raise (Invalid (at, "Must provide import " ^ n.it)) + +let rec iibb_search_inst + (ctx : ctx) (exps : extern_decl list) (i : int) (ed : extern_decl) + = + let find_ed' () = + List.find (fun x -> x.ed_name.it.en_name.it = ed.ed_name.it.en_name.it) + exps in + match ed.ed_desc with + | ED_type (DT_var (TV_bound i)) -> (* jackpot! *) + let ed' = find_ed' () in + (match ed'.ed_desc with + | ED_type dt -> Some dt + | _ -> raise (Invalid (ed'.ed_name.at, + "Cannot instantiate type import " + ^ ed.ed_name.it.en_name.it ^ "with non-type"))) + | ED_instance it -> + let ed' = find_ed' () in + (match ed'.ed_desc with + | ED_instance it' -> + List.find_map (iibb_search_inst ctx it'.it_exports (i + List.length it.it_evars)) + it.it_exports + | _ -> raise (Invalid (ed'.ed_name.at, + "Cannot instantiate instance import " + ^ ed.ed_name.it.en_name.it ^ "with non-instance"))) + | _ -> None +let iibb_search_ed + (ctx : ctx) (ias : I.instantiate_arg list) (i : int) (ed : extern_decl) + : def_type option + = + let find_ia () = find_instantiate_arg_named ed.ed_name.it.en_name ias in + match ed.ed_desc with + | ED_type (DT_var (TV_bound i)) -> (* jackpot! *) + (match (find_ia ()).it.I.ia_value.it with + | { I.s_sort = { it = Type ; _ } ; I.s_idx = ti } -> + Some (List.nth ctx.types (Int32.to_int ti)) + | _ -> raise (Invalid ((find_ia ()).at, + "Cannot instantiate type import " + ^ ed.ed_name.it.en_name.it ^ "with non-type"))) + | ED_instance it -> + (match (find_ia ()).it.I.ia_value.it with + | { I.s_sort = { it = Instance ; _ } ; I.s_idx = ii } -> + let inst = (List.nth ctx.instances (Int32.to_int ii)) in + let exps = List.map (fun x -> x.ad_contents) inst.itad_exports in + List.find_map (iibb_search_inst ctx exps (i + List.length it.it_evars)) + it.it_exports + | _ -> raise (Invalid ((find_ia ()).at, + "Cannot instantiate instance import " + ^ ed.ed_name.it.en_name.it ^ "with non-instance"))) + | _ -> None +let infer_instantiate_bvar_binding + (ctx : ctx) (is : extern_decl list) (ias : I.instantiate_arg list) (i : int) (v : boundedtyvar) + : def_type + = match v with + | Tbound_eq dt -> dt + | Tbound_subr -> + match List.find_map (iibb_search_ed ctx ias i) is with + | None -> raise (Invalid (no_region, "!! Impossible: un-imported uvar")) + | Some dt -> dt +let infer_instantiate_bvar_bindings + (ctx : ctx) (ct : component_type) (ias : I.instantiate_arg list) : bsubst + = List.mapi (fun i v -> Some (infer_instantiate_bvar_binding ctx ct.ct_imports ias i v)) + (List.rev ct.ct_uvars) + +let infer_sort_idx_ed (ctx : ctx) (si : I.sort_idx) : extern_desc + = + let i = Int32.to_int si.it.I.s_idx in + match si.it.I.s_sort.it with + | CoreSort { it = Core_module ; _ } -> + ED_core_module (List.nth ctx.core_ctx.core_modules i) + | Func -> ED_func (List.nth ctx.funcs i) + | Value -> ED_value (List.nth ctx.values i).ad_contents + | Type -> ED_type (List.nth ctx.types i) + | Instance -> + ED_instance + { it_evars = []; it_exports = List.map (fun x -> x.ad_contents) + (List.nth ctx.instances i).itad_exports } + | Component -> ED_component (List.nth ctx.components i) + | _ -> raise (Invalid (si.at, "Cannot instantiate an import with sort " + ^ show_sort' si.it.I.s_sort.it)) + +let check_instantiate_import (ctx : ctx) (ias : I.instantiate_arg list) (im : extern_decl) : unit + = let ia = find_instantiate_arg_named im.ed_name.it.en_name ias in + let ed = infer_sort_idx_ed ctx ia.it.I.ia_value in + pp_begin (); + subtype_extern_desc ctx ed im.ed_desc; + let _ = pp_end () in () + +let max_flat_params : int = 16 +let max_flat_results : int = 1 + +let rec flatten_val_type (vt : val_type) : Wasm.Types.result_type + = let open Wasm.Types in + match vt with + | Bool -> [NumType I32Type] + | Unsigned VI_8 | Unsigned VI_16 | Unsigned VI_32 + | Signed VI_8 | Signed VI_16 | Signed VI_32 -> + [NumType I32Type] + | Unsigned VI_64 | Signed VI_64 -> + [NumType I64Type] + | Float VF_32 -> [NumType F32Type] + | Float VF_64 -> [NumType F64Type] + | Char -> [NumType I32Type] + | List _ -> [NumType I32Type; NumType I32Type] + | Record rfs -> List.concat_map flatten_record_field rfs + | Variant vcs -> flatten_variant vcs + | Own _ | Borrow _ -> [NumType I32Type] +and flatten_record_field (rf : record_field) : Wasm.Types.result_type + = flatten_val_type rf.rf_type +and flatten_variant (vcs : variant_case list) : Wasm.Types.result_type + = flatten_variant_discriminant (List.length vcs) + @ flatten_variant_merge (List.map flatten_variant_case vcs) +and variant_discriminant (n : int) : val_type + = Unsigned + (if n <= 256 + then VI_8 + else if n <= 65536 + then VI_16 + else if n <= 4294967296 + then VI_32 + else raise (Invalid (no_region, "Cannot have " ^ string_of_int n))) +and flatten_variant_discriminant (n : int) : Wasm.Types.result_type + = flatten_val_type (variant_discriminant n) +and flatten_variant_case (vc : variant_case) : Wasm.Types.result_type + = match vc.vc_type with + | None -> [] + | Some vt -> flatten_val_type vt +and flatten_variant_merge (ts : Wasm.Types.result_type list) + : Wasm.Types.result_type + = match ts with + | [] -> [] + | ts1::ts2s -> + let ts2 = flatten_variant_merge ts2s in + flatten_variant_merge_rts ts1 ts2 +and flatten_variant_merge_rts + (ts1 : Wasm.Types.result_type) (ts2 : Wasm.Types.result_type) + : Wasm.Types.result_type + = match ts1, ts2 with + | [], _ -> ts2 + | _, [] -> ts1 + | t1::t1s, t2::t2s -> + (flatten_variant_merge_ts t1 t2)::(flatten_variant_merge_rts t1s t2s) +and flatten_variant_merge_ts + (t1 : Wasm.Types.value_type) (t2 : Wasm.Types.value_type) + : Wasm.Types.value_type + = let open Wasm.Types in + if t1 = t2 then t1 + else if (t1 = NumType I32Type && t2 = NumType F32Type) + || (t1 = NumType F32Type && t2 = NumType I32Type) + then NumType I32Type + else NumType I64Type + +let flatten_func_ios (fio : func_ios) : Wasm.Types.result_type + = match fio with + | Fio_one vt -> flatten_val_type vt + | Fio_many nvts -> + List.concat_map (fun (n, vt) -> flatten_val_type vt) nvts + +let flatten_func_type (is_lower : bool) (ft : func_type) + : core_func_type + = let open Wasm.Types in + let ps = flatten_func_ios ft.ft_params in + let ps' = if List.length ps > max_flat_params + then [NumType I32Type] else ps in + let rs = flatten_func_ios ft.ft_result in + let (ps'', rs') = + if List.length rs > max_flat_results + then if is_lower + then (ps' @ [NumType I32Type], []) + else (ps', [NumType I32Type]) + else (ps', rs) in + FuncType (ps'', rs') + +let check_canon_opts (ctx : ctx) (os : I.canon_opt list) : unit + = () + +let fio_vts fio + = match fio with + | Fio_one vt -> [vt] + | Fio_many vts -> List.map (fun (n, vt) -> vt) vts + +let check_exportable (ctx : ctx) (ed : extern_desc) : unit + = wf_extern_desc ctx { pos_param = false; pos_export = true; } ed + +let rec infer_component_defn (ctx : ctx) (d : I.definition) + : ctx * extern_decl option * extern_decl option + = match d.it with + | I.CoreDef cd -> (infer_core_defn ctx cd, None, None) + | I.ComponentDef c -> + let ct = infer_component ctx c in + ({ ctx with components = ctx.components @ [ct] }, None, None) + | I.InstanceDef ({ it = I.Instantiate_component (cid, ias) ; _ }) -> + let ct = List.nth ctx.components (Int32.to_int cid) in + check_uniqueness "Duplicate instantiate arg name " + (fun x -> x.I.ia_name.it) ias; + let uvar_insts = infer_instantiate_bvar_bindings ctx ct ias in + let ct_imports = List.map (subst_extern_decl (bsubst_subst uvar_insts)) + ct.ct_imports in + let ct_instance = subst_instance_type (bsubst_subst uvar_insts) + ct.ct_instance in + List.iter (check_instantiate_import ctx ias) ct_imports; + let ctx' = instance_to_context ctx true false ct_instance in + let ctx'' = mark_dead_ias ctx' ias in + (ctx'', None, None) + | I.InstanceDef ({ it = I.Instantiate_inline ies; _ }) -> + check_uniqueness "Duplicate inline export name " + (fun x -> x.I.ie_name.it.en_name.it) ies; + let ctx' = mark_dead_ies ctx ies in + ({ ctx' with + instances = + ctx'.instances @ + [ { itad_exports = + List.map (fun ie -> + make_live { ed_name = ie.it.I.ie_name + ; ed_desc = infer_sort_idx_ed ctx + ie.it.I.ie_value + }) ies } ] }, None, None) + | I.AliasDef a -> + let ctx', at = resolve_alias ctx a in + (match a.it.I.a_sort.it, at with + | CoreSort { it = Core_module; _ }, Either.Left (CT_module cmt) -> + ({ ctx' with + core_ctx = { ctx'.core_ctx with + core_modules = ctx'.core_ctx.core_modules + @ [ cmt ] } }, None, None) + | CoreSort { it = Core_type; _ }, Either.Left ct -> + ({ ctx' with + core_ctx = { ctx'.core_ctx with + core_types = ctx'.core_ctx.core_types + @ [ ct ] } }, None, None) + | CoreSort { it = Core_table; _}, Either.Left (CT_table tt) -> + ({ ctx' with + core_ctx = { ctx'.core_ctx with + core_tables = ctx'.core_ctx.core_tables + @ [ tt ] } }, None, None) + | CoreSort { it = Core_memory; _}, Either.Left (CT_memory mt) -> + ({ ctx' with + core_ctx = { ctx'.core_ctx with + core_mems = ctx'.core_ctx.core_mems + @ [ mt ] } }, None, None) + | CoreSort { it = Core_global; _}, Either.Left (CT_global gt) -> + ({ ctx' with + core_ctx = { ctx'.core_ctx with + core_globals = ctx'.core_ctx.core_globals + @ [ gt ] } }, None, None) + | CoreSort { it = Core_func; _}, Either.Left (CT_func ft) -> + ({ ctx' with + core_ctx = { ctx'.core_ctx with + core_funcs = ctx'.core_ctx.core_funcs + @ [ ft ] } }, None, None) + | Func, Either.Right (DT_func_type ft) -> + ({ ctx' with funcs = ctx'.funcs @ [ ft ] }, None, None) + | Value, Either.Right (DT_val_type vt) -> + ({ ctx' with values = ctx'.values @ [ make_live vt ] + }, None, None) + | Type, Either.Right dt -> ({ ctx' with types = ctx'.types @ [ dt ] } + ,None, None) + | Instance, Either.Right (DT_instance_type it) -> + (instance_to_context ctx' true false it, None, None) + | Component, Either.Right (DT_component_type ct) -> + ({ ctx' with components = ctx'.components @ [ ct ] }, None, None) + | _, _ -> raise (Invalid (a.at, "!! Impossible: resolve_alias bad sort"))) + | I.TypeDef { it = I.Deftype_rsrc dtor; _ } -> + (* This is the only place that resource types are valid, + and they are generative here *) + let i = Int32.of_int (List.length ctx.rtypes) in + ({ ctx with + rtypes = ctx.rtypes @ [ { rt_dtor = dtor } ]; + types = ctx.types @ [ DT_resource_type i ] } + ,None, None) + | I.TypeDef dt -> + let dt' = elab_def_type ctx dt in + ({ ctx with types = ctx.types @ [ dt' ] }, None, None) + | I.CanonDef { it = I.Canon_lift (cfid, ed, cos); _ } -> + let cfit = List.nth ctx.core_ctx.core_funcs (Int32.to_int cfid) in + (match elab_extern_desc ctx ed with + | ([], ED_func fit) -> + subtype_core_extern_desc ctx (Wasm.Types.ExternFuncType cfit) + (Wasm.Types.ExternFuncType (flatten_func_type false fit)); + check_canon_opts ctx cos; + ({ ctx with funcs = ctx.funcs @ [ fit ] }, None, None) + | _ -> raise (Invalid (d.at, "Canon lift externdesc must be func"))) + | I.CanonDef { it = I.Canon_lower (fid, cos); _ } -> + let ft = List.nth ctx.funcs (Int32.to_int fid) in + let cft = flatten_func_type true ft in + check_canon_opts ctx cos; + ({ ctx with + core_ctx = { ctx.core_ctx with + core_funcs = ctx.core_ctx.core_funcs @ [ cft ] } } + ,None, None) + | I.CanonDef { it = I.Canon_resource_builtin { it = I.CRB_new dt; _ }; _ } -> + let dt' = resolve_type_use ctx dt in + (match dt' with + | DT_resource_type i -> () + | _ -> raise (Invalid (d.at, "Canon resource.new requires a resource " + ^ "type defined in this component"))); + let open Wasm.Types in + let cft = FuncType ([NumType I32Type], [NumType I32Type]) in + ({ ctx with + core_ctx = { ctx.core_ctx with + core_funcs = ctx.core_ctx.core_funcs @ [ cft ] } } + ,None, None) + | I.CanonDef { it = I.Canon_resource_builtin { it = I.CRB_drop vt; _ }; _ } -> + let vt' = resolve_val_type_use ctx d.at vt in + (match vt' with + | Own _ | Borrow _ -> () + | _ -> raise (Invalid (d.at, "Canon resource.drop requuires a resource " + ^ "handle type"))); + let open Wasm.Types in + let cft = FuncType ([NumType I32Type], []) in + ({ ctx with + core_ctx = { ctx.core_ctx with + core_funcs = ctx.core_ctx.core_funcs @ [ cft ] } } + ,None, None) + | I.CanonDef { it = I.Canon_resource_builtin { it = I.CRB_rep dt; _ }; _ } -> + let dt' = resolve_type_use ctx dt in + (match dt' with + | DT_resource_type i -> () + | _ -> raise (Invalid (d.at, "Canon resource.rep requires a resource " + ^ "type defined in this component"))); + let open Wasm.Types in + let cft = FuncType ([NumType I32Type], [NumType I32Type]) in + ({ ctx with + core_ctx = { ctx.core_ctx with + core_funcs = ctx.core_ctx.core_funcs @ [ cft ] } } + ,None, None) + | I.StartDef { it = sd; _ } -> + let ft = List.nth ctx.funcs (Int32.to_int sd.I.s_func) in + let vts = fio_vts ft.ft_params in + let vts' = List.map (fun i -> + (List.nth ctx.values (Int32.to_int i)).ad_contents) + sd.I.s_params in + List.iter2 (subtype_val_type ctx) vts' vts; + let ctx' = mark_dead_sort_idxs ctx + (List.map (fun i -> { I.s_sort = Value @@ no_region + ; I.s_idx = i } @@ no_region) + sd.I.s_params) in + let rvts = fio_vts ft.ft_result in + let nftr = List.length rvts in + let nftr' = List.length sd.I.s_result in + (if nftr <> nftr' + then raise (Invalid (d.at, "Start definition calls function returning " + ^ string_of_int nftr ^ " results, but " + ^ " expects to have " + ^ string_of_int nftr' ^ " results")) + else ()); + ({ ctx' with values = ctx'.values @ List.map make_live rvts } + ,None, None) + | I.ImportDef { it = { I.i_name = ni; I.i_type = it; }; _ } -> + let v, ed' = elab_extern_desc ctx it in + let ctx', bsub = bound_to_uvars ctx true v in + let ed'' = subst_extern_desc (bsubst_subst bsub) ed' in + (add_extern_desc_to_ctx ctx' true true ed'' + ,Some { ed_name = ni ; ed_desc = ed'' }, None) + | I.ExportDef { it = { I.e_name = en; I.e_value = si; I.e_type = et }; _ } -> + let ed = infer_sort_idx_ed ctx si in + let vs, ed' = match et with + | None -> ([], ed) + | Some ed' -> elab_extern_desc ctx ed' in + let ctx', ed'' = match vs, ed', ed with + | [v], ED_type (DT_var (TV_bound 0)), ED_type dt -> + ({ ctx with + evars = ctx.evars @ [ (v, Some dt) ] } + ,ED_type (DT_var (TV_free (FTV_evar (0, List.length ctx.evars))))) + | _, ED_instance it, _ -> + (ctx, ED_instance { it_evars = vs; it_exports = it.it_exports }) + | [], _, _ -> (ctx, ed') + | _, _, _ -> + raise (Invalid (d.at, "Exported type should not have evars" + ^ " unless it is a `type` or `instance`")) in + subtype_extern_desc ctx' ed ed''; + check_exportable ctx' ed''; + let ctx'' = mark_dead_sort_idxs ctx' [si] in + let ctx''' = add_extern_desc_to_ctx ctx'' false false ed'' in + (ctx''', None, Some { ed_name = en; ed_desc = ed'' }) + +and ctx_no_live_vals (ctx : ctx) : unit + = + let check_this : 'a. ('a alive_dead) -> unit + = fun ad -> + if ad.ad_live + then raise (Invalid (no_region, + "All values must be dead at end of component!")) + else () in + let check_export_decl (ed : extern_decl_ad) : unit + = match ed.ad_contents.ed_desc with + | ED_value _ -> check_this ed + | ED_instance _ -> check_this ed + | _ -> () in + let check_itad (itad : instance_type_ad) : unit + = let _ = List.map check_export_decl itad.itad_exports in () in + let _ = List.map check_this ctx.values in + let _ = List.map check_itad ctx.instances in + () + +and infer_component (ctx : ctx) (c : I.component) : component_type + = build_component_type infer_component_defn ctx_no_live_vals ctx true + c.it.I.defns diff --git a/interpreter/valid/valid.mli b/interpreter/valid/valid.mli new file mode 100644 index 00000000..5dfc4fca --- /dev/null +++ b/interpreter/valid/valid.mli @@ -0,0 +1,5 @@ +exception Invalid of Wasm.Source.region * string + +val infer_component + : Etypes.ctx -> Ast.IntAst.component + -> Etypes.component_type (* raises Invalid *) diff --git a/interpreter/wasm_components.opam b/interpreter/wasm_components.opam new file mode 100644 index 00000000..39ffa2ab --- /dev/null +++ b/interpreter/wasm_components.opam @@ -0,0 +1,20 @@ +opam-version: "2.0" +maintainer: "Lucy Menon " +authors: "Lucy Menon " +homepage: "https://github.com/WebAssembly/component-model" +bug-reports: "https://github.com/WebAssembly/component-model/issues" +license: "Apache-2.0" +dev-repo: "git+https://github.com/WebAssembly/component-model.git" +build: [ + ["dune" "build" "-p" name "-j" jobs + "@install" + "@doc" {with-doc} + "@runtest" {with-test} ] +] +depends: [ + "ocaml" {>= "4.08.0" & < "4.13"} + "dune" {>= "2.9.1"} + "wasm" {>= "1.1.1"} +] +synopsis: + "Library to read and write WebAssembly (Wasm) files and manipulate their AST"