diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 050c5e0e2..554e2c119 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -10,7 +10,7 @@ jobs: strategy: matrix: version: [4.08.1, 5.2.1] - os: [ubuntu-latest, macOS-latest] + os: [ubuntu-latest, macos-latest] exclude: - os: macos-latest version: 4.08.1 @@ -18,7 +18,7 @@ jobs: runs-on: ${{ matrix.os }} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: System dependencies (ubuntu) if: startsWith(matrix.os, 'ubuntu') @@ -26,13 +26,13 @@ jobs: sudo apt install build-essential libgmp-dev z3 cvc4 opam - name: System dependencies (macOS) - if: startsWith(matrix.os, 'macOS') + if: startsWith(matrix.os, 'macos') run: | brew install --force --overwrite gpatch gmp z3 pkgconf opam - name: Restore cached opam id: cache-opam-restore - uses: actions/cache/restore@v3 + uses: actions/cache/restore@v4 with: path: ~/.opam key: ${{ matrix.os }}-${{ matrix.version }} @@ -45,7 +45,7 @@ jobs: - name: Save cached opam if: steps.cache-opam-restore.outputs.cache-hit != 'true' id: cache-opam-save - uses: actions/cache/save@v3 + uses: actions/cache/save@v4 with: path: ~/.opam key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }} diff --git a/src/bin/dune b/src/bin/dune index 1eed938e3..38c3f278c 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -242,6 +242,6 @@ (%{workspace_root}/src/gen_lib/sail2_values.lem as src/gen_lib/sail2_values.lem) - (%{workspace_root}/src/sail_lean_backend/Sail/sail.lean + (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as - src/sail_lean_backend/Sail/sail.lean))) + src/sail_lean_backend/Sail/Sail.lean))) diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 07fec203b..dad0f27b6 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -149,7 +149,7 @@ let add_target_header plugin opts = let load_plugin opts plugin = try if is_bytecode then Dynlink.loadfile plugin else Dynlink.loadfile_private plugin; - let plugin_opts = Target.extract_options () |> fix_options |> target_align in + let plugin_opts = Target.extract_options () |> List.map Flag.to_arg |> fix_options |> target_align in opts := add_target_header plugin !opts @ plugin_opts with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg) diff --git a/src/lib/flag.ml b/src/lib/flag.ml new file mode 100644 index 000000000..ddfa2ed77 --- /dev/null +++ b/src/lib/flag.ml @@ -0,0 +1,64 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* SPDX-License-Identifier: BSD-2-Clause *) +(****************************************************************************) + +open Arg + +type t = { prefix : string list; hide_prefix : bool; debug : bool; hide : bool; arg : string option; key : string } + +let create ?(prefix = []) ?(hide_prefix = false) ?(debug = false) ?(hide = false) ?arg key = + { prefix; hide_prefix; debug; hide; arg; key } + +let underscore_sep = Util.string_of_list "_" (fun s -> s) + +let to_arg (flag, spec, doc) = + let apply_prefix key = + match flag.prefix with [] -> key | _ when flag.hide_prefix -> key | _ -> underscore_sep flag.prefix ^ "_" ^ key + in + let key = + "-" ^ if flag.key = "" then underscore_sep flag.prefix else (if flag.debug then "d" else "") ^ apply_prefix flag.key + in + let arg_prefix = match flag.arg with Some desc -> "<" ^ desc ^ "> " | None -> " " in + (key, spec, if flag.hide then "" else arg_prefix ^ (if flag.debug then "(debug) " else "") ^ doc) diff --git a/src/lib/flag.mli b/src/lib/flag.mli new file mode 100644 index 000000000..5d378814a --- /dev/null +++ b/src/lib/flag.mli @@ -0,0 +1,51 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* SPDX-License-Identifier: BSD-2-Clause *) +(****************************************************************************) + +type t + +val create : ?prefix:string list -> ?hide_prefix:bool -> ?debug:bool -> ?hide:bool -> ?arg:string -> string -> t + +val to_arg : t * Arg.spec * string -> Arg.key * Arg.spec * Arg.doc diff --git a/src/lib/target.ml b/src/lib/target.ml index b2c8a7e4a..16e4d179a 100644 --- a/src/lib/target.ml +++ b/src/lib/target.ml @@ -52,7 +52,7 @@ module StringMap = Map.Make (String) type target = { name : string; - options : (Arg.key * Arg.spec * Arg.doc) list; + options : (Flag.t * Arg.spec * string) list; pre_parse_hook : unit -> unit; pre_initial_check_hook : string list -> unit; pre_rewrites_hook : typed_ast -> Effects.side_effect_info -> Env.t -> unit; @@ -93,12 +93,12 @@ let register ~name ?flag ?description:desc ?(options = []) ?(pre_parse_hook = fu prerr_endline ("Cannot use multiple Sail targets simultaneously: " ^ tgt ^ " and " ^ name); exit 1 in - let desc = match desc with Some desc -> desc | None -> " invoke the Sail " ^ name ^ " target" in + let desc = match desc with Some desc -> desc | None -> "invoke the Sail " ^ name ^ " target" in let flag = match flag with Some flag -> flag | None -> name in let tgt = { name; - options = ("-" ^ flag, Arg.Unit set_target, desc) :: options; + options = (Flag.create ~prefix:[flag] "", Arg.Unit set_target, desc) :: options; pre_parse_hook; pre_initial_check_hook; pre_rewrites_hook; diff --git a/src/lib/target.mli b/src/lib/target.mli index 5ab1d8182..d360cd170 100644 --- a/src/lib/target.mli +++ b/src/lib/target.mli @@ -106,7 +106,7 @@ val register : name:string -> ?flag:string -> ?description:string -> - ?options:(Arg.key * Arg.spec * Arg.doc) list -> + ?options:(Flag.t * Arg.spec * string) list -> ?pre_parse_hook:(unit -> unit) -> ?pre_initial_check_hook:(string list -> unit) -> ?pre_rewrites_hook:(typed_ast -> Effects.side_effect_info -> Env.t -> unit) -> @@ -130,4 +130,4 @@ val get : name:string -> target option val extract_registered : unit -> string list (** Used internally to dynamically update the option list when loading plugins *) -val extract_options : unit -> (Arg.key * Arg.spec * Arg.doc) list +val extract_options : unit -> (Flag.t * Arg.spec * string) list diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 021d85de0..40eb0df86 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -4194,7 +4194,9 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, uannot)) as mpa | _ -> Reporting.unreachable l __POS__ "unifying mapping type, expanded synonyms to non-mapping type!" end | MP_app (other, mpats) when Env.is_mapping other env -> - bind_mpat allow_unknown other_env env (MP_aux (MP_app (other, [mk_mpat (MP_tuple mpats)]), (l, uannot))) typ + bind_mpat allow_unknown other_env env + (MP_aux (MP_app (other, [mk_mpat ~loc:l (MP_tuple mpats)]), (l, uannot))) + typ | MP_app (f, _) when not (Env.is_union_constructor f env || Env.is_mapping f env) -> typ_error l (string_of_id f ^ " is not a union constructor or mapping in mapping-pattern " ^ string_of_mpat mpat) | MP_as (mpat, id) -> diff --git a/src/sail_c_backend/sail_plugin_c.ml b/src/sail_c_backend/sail_plugin_c.ml index 37d1af537..13670e812 100644 --- a/src/sail_c_backend/sail_plugin_c.ml +++ b/src/sail_c_backend/sail_plugin_c.ml @@ -53,39 +53,42 @@ let opt_specialize_c = ref false let c_options = [ - ( "-c_include", + ( Flag.create ~prefix:["c"] ~arg:"filename" "include", Arg.String (fun i -> opt_includes_c := i :: !opt_includes_c), - " provide additional include for C output" + "provide additional include for C output" ); - ("-c_no_main", Arg.Set C_backend.opt_no_main, " do not generate the main() function"); - ("-c_no_rts", Arg.Set C_backend.opt_no_rts, " do not include the Sail runtime"); - ( "-c_no_lib", + (Flag.create ~prefix:["c"] "no_main", Arg.Set C_backend.opt_no_main, "do not generate the main() function"); + (Flag.create ~prefix:["c"] "no_rts", Arg.Set C_backend.opt_no_rts, "do not include the Sail runtime"); + ( Flag.create ~prefix:["c"] "no_lib", Arg.Tuple [Arg.Set C_backend.opt_no_lib; Arg.Set C_backend.opt_no_rts], - " do not include the Sail runtime or library" + "do not include the Sail runtime or library" ); - ("-c_prefix", Arg.String (fun prefix -> C_backend.opt_prefix := prefix), " prefix generated C functions"); - ( "-c_extra_params", + ( Flag.create ~prefix:["c"] ~arg:"prefix" "prefix", + Arg.String (fun prefix -> C_backend.opt_prefix := prefix), + "prefix generated C functions" + ); + ( Flag.create ~prefix:["c"] ~arg:"parameters" "extra_params", Arg.String (fun params -> C_backend.opt_extra_params := Some params), - " generate C functions with additional parameters" + "generate C functions with additional parameters" ); - ( "-c_extra_args", + ( Flag.create ~prefix:["c"] ~arg:"arguments" "extra_args", Arg.String (fun args -> C_backend.opt_extra_arguments := Some args), - " supply extra argument to every generated C function call" + "supply extra argument to every generated C function call" ); - ("-c_specialize", Arg.Set opt_specialize_c, " specialize integer arguments in C output"); - ( "-c_preserve", + (Flag.create ~prefix:["c"] "specialize", Arg.Set opt_specialize_c, "specialize integer arguments in C output"); + ( Flag.create ~prefix:["c"] "preserve", Arg.String (fun str -> Specialize.add_initial_calls (Ast_util.IdSet.singleton (Ast_util.mk_id str))), - " make sure the provided function identifier is preserved in C output" + "make sure the provided function identifier is preserved in C output" ); - ( "-c_fold_unit", + ( Flag.create ~prefix:["c"] "fold_unit", Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str), - " remove comma separated list of functions from C output, replacing them with unit" + "remove comma separated list of functions from C output, replacing them with unit" ); - ( "-c_coverage", + ( Flag.create ~prefix:["c"] ~arg:"file" "coverage", Arg.String (fun str -> C_backend.opt_branch_coverage := Some (open_out str)), - " Turn on coverage tracking and output information about all branches and functions to a file" + "Turn on coverage tracking and output information about all branches and functions to a file" ); - ( "-O", + ( Flag.create ~prefix:["c"] ~hide_prefix:true "O", Arg.Tuple [ Arg.Set C_backend.optimize_primops; @@ -94,17 +97,20 @@ let c_options = Arg.Set C_backend.optimize_struct_updates; Arg.Set C_backend.optimize_alias; ], - " turn on optimizations for C compilation" + "turn on optimizations for C compilation" ); - ( "-Ofixed_int", + ( Flag.create ~prefix:["c"] ~hide_prefix:true "Ofixed_int", Arg.Set C_backend.optimize_fixed_int, - " assume fixed size integers rather than GMP arbitrary precision integers" + "assume fixed size integers rather than GMP arbitrary precision integers" ); - ( "-Ofixed_bits", + ( Flag.create ~prefix:["c"] ~hide_prefix:true "Ofixed_bits", Arg.Set C_backend.optimize_fixed_bits, - " assume fixed size bitvectors rather than arbitrary precision bitvectors" + "assume fixed size bitvectors rather than arbitrary precision bitvectors" + ); + ( Flag.create ~prefix:["c"] ~hide_prefix:true "static", + Arg.Set C_backend.opt_static, + "make generated C functions static" ); - ("-static", Arg.Set C_backend.opt_static, " make generated C functions static"); ] let c_rewrites = diff --git a/src/sail_coq_backend/sail_plugin_coq.ml b/src/sail_coq_backend/sail_plugin_coq.ml index 41988d7be..a5afe5722 100644 --- a/src/sail_coq_backend/sail_plugin_coq.ml +++ b/src/sail_coq_backend/sail_plugin_coq.ml @@ -58,58 +58,57 @@ let opt_coq_lib_style : Pretty_print_coq.library_style option ref = ref None let coq_options = [ - ( "-coq_output_dir", + ( Flag.create ~prefix:["coq"] ~arg:"directory" "output_dir", Arg.String (fun dir -> opt_coq_output_dir := Some dir), - " set a custom directory to output generated Coq" + "set a custom directory to output generated Coq" ); - ( "-coq_lib", + ( Flag.create ~prefix:["coq"] ~arg:"filename" "lib", Arg.String (fun l -> opt_libs_coq := l :: !opt_libs_coq), - " provide additional library to open in Coq output" + "provide additional library to open in Coq output" ); - ( "-coq_alt_modules", + ( Flag.create ~prefix:["coq"] ~arg:"filename" "alt_modules", Arg.String (fun l -> opt_alt_modules_coq := l :: !opt_alt_modules_coq), - " provide alternative modules to open in Coq output" + "provide alternative modules to open in Coq output" ); - ( "-coq_alt_modules2", + ( Flag.create ~prefix:["coq"] ~arg:"filename" "alt_modules2", Arg.String (fun l -> opt_alt_modules2_coq := l :: !opt_alt_modules2_coq), - " provide additional alternative modules to open only in main (non-_types) Coq output, and suppress \ - default definitions of MR and M monads" + "provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default \ + definitions of MR and M monads" ); - ( "-coq_extern_type", + ( Flag.create ~prefix:["coq"] ~arg:"typename" "extern_type", Arg.String Pretty_print_coq.(fun ty -> opt_extern_types := ty :: !opt_extern_types), - " do not generate a definition for the type" + "do not generate a definition for the type" ); - ( "-coq_generate_extern_types", + ( Flag.create ~prefix:["coq"] "generate_extern_types", Arg.Set Pretty_print_coq.opt_generate_extern_types, - " generate only extern types rather than suppressing them" + "generate only extern types rather than suppressing them" ); - ( "-coq_isla", + ( Flag.create ~prefix:["coq"] ~arg:"filename" "isla", Arg.String (fun fname -> opt_coq_isla := Some fname), - " generate Coq code for decoding Isla trace values" + "generate Coq code for decoding Isla trace values" ); - ( "-coq_record_update", + ( Flag.create ~prefix:["coq"] "record_update", Arg.Set Pretty_print_coq.opt_coq_record_update, - " use coq-record-update package's syntax for record updates" + "use coq-record-update package's syntax for record updates" ); - ( "-coq_lib_style", + ( Flag.create ~prefix:["coq"] "lib_style", Arg.Symbol ( ["bbv"; "stdpp"], fun s -> opt_coq_lib_style := match s with "bbv" -> Some BBV | "stdpp" -> Some Stdpp | _ -> assert false ), - " select which style of Coq library to use (default: stdpp when the concurrency interfaces is used, bbv \ - otherwise)" + "select which style of Coq library to use (default: stdpp when the concurrency interfaces is used, bbv otherwise)" ); - ( "-dcoq_undef_axioms", + ( Flag.create ~prefix:["coq"] ~debug:true "undef_axioms", Arg.Set Pretty_print_coq.opt_undef_axioms, - " (debug) generate axioms for functions that are declared but not defined" + "generate axioms for functions that are declared but not defined" ); - ( "-dcoq_warn_nonex", + ( Flag.create ~prefix:["coq"] ~debug:true "warn_nonex", Arg.Set Rewrites.opt_coq_warn_nonexhaustive, - " (debug) generate warnings for non-exhaustive pattern matches in the Coq backend" + "generate warnings for non-exhaustive pattern matches in the Coq backend" ); - ( "-dcoq_debug_on", + ( Flag.create ~prefix:["coq"] ~arg:"function" ~debug:true "debug_on", Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f :: !Pretty_print_coq.opt_debug_on), - " (debug) produce debug messages for Coq output on given function" + "produce debug messages for Coq output on given function" ); ] diff --git a/src/sail_doc_backend/sail_plugin_doc.ml b/src/sail_doc_backend/sail_plugin_doc.ml index e9c77cb2f..f803b3dcf 100644 --- a/src/sail_doc_backend/sail_plugin_doc.ml +++ b/src/sail_doc_backend/sail_plugin_doc.ml @@ -69,24 +69,30 @@ let embedding_option () = let doc_options = [ - ( "-doc_format", + ( Flag.create ~prefix:["doc"] ~arg:"format" "format", Arg.String (fun format -> opt_doc_format := format), - " Output documentation in the chosen format, either latex or asciidoc (default asciidoc)" + "Output documentation in the chosen format, either latex or asciidoc (default asciidoc)" ); - ( "-doc_file", + ( Flag.create ~prefix:["doc"] ~arg:"file" "file", Arg.String (fun file -> opt_doc_files := file :: !opt_doc_files), - " Document only the provided files" + "Document only the provided files" ); - ( "-doc_embed", + ( Flag.create ~prefix:["doc"] ~arg:"plain|base64" "embed", Arg.String (fun format -> opt_doc_embed := Some format), - " Embed all documentation contents into the documentation bundle rather than referencing it" + "Embed all documentation contents into the documentation bundle rather than referencing it" ); - ( "-doc_embed_with_location", + ( Flag.create ~prefix:["doc"] "embed_with_location", Arg.Set opt_doc_embed_with_location, - " When used with --doc-embed, include both the contents and locations" + "When used with --doc-embed, include both the contents and locations" + ); + ( Flag.create ~prefix:["doc"] "compact", + Arg.Unit (fun _ -> opt_doc_compact := true), + "Use compact documentation format" + ); + ( Flag.create ~prefix:["doc"] ~arg:"file" "bundle", + Arg.String (fun file -> opt_doc_bundle := file), + "Name for documentation bundle file" ); - ("-doc_compact", Arg.Unit (fun _ -> opt_doc_compact := true), " Use compact documentation format"); - ("-doc_bundle", Arg.String (fun file -> opt_doc_bundle := file), " Name for documentation bundle file"); ] let output_docinfo doc_dir docinfo = @@ -136,10 +142,13 @@ let _ = let html_options = [ - ("-html_css", Arg.String (fun file -> opt_html_css := Some file), " CSS file for html output"); - ( "-html_link_prefix", + ( Flag.create ~prefix:["html"] ~arg:"file" "css", + Arg.String (fun file -> opt_html_css := Some file), + "CSS file for html output" + ); + ( Flag.create ~prefix:["html"] ~arg:"string" "link_prefix", Arg.String (fun prefix -> opt_html_link_prefix := prefix), - " Prefix links in HTML output with string" + "Prefix links in HTML output with string" ); ] diff --git a/src/sail_latex_backend/sail_plugin_latex.ml b/src/sail_latex_backend/sail_plugin_latex.ml index bbbfcc5d6..a66ee3b48 100644 --- a/src/sail_latex_backend/sail_plugin_latex.ml +++ b/src/sail_latex_backend/sail_plugin_latex.ml @@ -50,12 +50,15 @@ open Interactive.State let latex_options = [ - ( "-latex_prefix", + ( Flag.create ~prefix:["latex"] ~arg:"prefix" "prefix", Arg.String (fun prefix -> Latex.opt_prefix := prefix), - " set a custom prefix for generated LaTeX labels and macro commands (default sail)" + "set a custom prefix for generated LaTeX labels and macro commands (default sail)" ); - ("-latex_full_valspecs", Arg.Clear Latex.opt_simple_val, " print full valspecs in LaTeX output"); - ( "-latex_abbrevs", + ( Flag.create ~prefix:["latex"] "full_valspecs", + Arg.Clear Latex.opt_simple_val, + "print full valspecs in LaTeX output" + ); + ( Flag.create ~prefix:["latex"] "abbrevs", Arg.String (fun s -> let abbrevs = String.split_on_char ';' s in @@ -68,7 +71,7 @@ let latex_options = | None -> Latex.opt_abbrevs := filtered | Some abbrev -> raise (Arg.Bad (abbrev ^ " does not end in a '.'")) ), - " semicolon-separated list of abbreviations to fix spacing for in LaTeX output (default 'e.g.;i.e.')" + "semicolon-separated list of abbreviations to fix spacing for in LaTeX output (default 'e.g.;i.e.')" ); ] diff --git a/src/sail_lean_backend/Sail/sail.lean b/src/sail_lean_backend/Sail/Sail.lean similarity index 100% rename from src/sail_lean_backend/Sail/sail.lean rename to src/sail_lean_backend/Sail/Sail.lean diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 0277dc967..addfb7ec3 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -29,6 +29,7 @@ let add_single_kid_id_rename ctxt id kid = } let implicit_parens x = enclose (string "{") (string "}") x + let doc_id_ctor (Id_aux (i, _)) = match i with Id i -> string i | Operator x -> string (Util.zencode_string ("op " ^ x)) @@ -36,7 +37,6 @@ let doc_kid ctxt (Kid_aux (Var x, _) as ki) = match KBindings.find_opt ki ctxt.kid_id_renames with | Some (Some i) -> string (string_of_id i) | _ -> string ("k_" ^ String.sub x 1 (String.length x - 1)) - (* TODO do a proper renaming and keep track of it *) let is_enum env id = match Env.lookup_id id env with Enum _ -> true | _ -> false @@ -389,7 +389,6 @@ let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.en let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = let defs = remove_imports defs 0 in - let output : document = separate_map empty (doc_def empty_context) defs in - output_string o "import Sail.sail\n\n"; + let output : document = separate_map empty doc_def defs in print o output; () diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml index 5d4d2f1e8..882063b41 100644 --- a/src/sail_lean_backend/sail_plugin_lean.ml +++ b/src/sail_lean_backend/sail_plugin_lean.ml @@ -77,13 +77,13 @@ let lean_version : string = "lean4:nightly-2024-09-25" let lean_options = [ - ( "-lean_output_dir", + ( Flag.create ~prefix:["lean"] ~arg:"directory" "output_dir", Arg.String (fun dir -> opt_lean_output_dir := Some dir), - " set a custom directory to output generated Lean" + "set a custom directory to output generated Lean" ); - ( "-lean_force_output", + ( Flag.create ~prefix:["lean"] "force_output", Arg.Unit (fun () -> opt_lean_force_output := true), - " removes the content of the output directory if it is non-empty" + "removes the content of the output directory if it is non-empty" ); ] @@ -157,7 +157,7 @@ let create_lake_project (out_name : string) default_sail_dir = (* Change the base directory if the option '--lean-output-dir' is set *) let base_dir = match !opt_lean_output_dir with Some dir -> dir | None -> "." in let project_dir = Filename.concat base_dir out_name in - if !opt_lean_force_output && Sys.is_directory project_dir then ( + if !opt_lean_force_output && Sys.file_exists project_dir && Sys.is_directory project_dir then ( let _ = Unix.system ("rm -r " ^ Filename.quote project_dir ^ "/*") in () ) @@ -174,15 +174,19 @@ let create_lake_project (out_name : string) default_sail_dir = let out_name_camel = Libsail.Util.to_upper_camel_case out_name in let lakefile = open_out (Filename.concat project_dir "lakefile.toml") in output_string lakefile - ("name = \"" ^ out_name ^ "\"\ndefaultTargets = [\"" ^ out_name_camel - ^ "\"]\n\n[[lean_lib]]\nname = \"Sail\"\n\n[[lean_lib]]\nname = \"" ^ out_name_camel ^ "\"" + ("name = \"" ^ out_name ^ "\"\ndefaultTargets = [\"" ^ out_name_camel ^ "\"]\n\n[[lean_lib]]\nname = \"" + ^ out_name_camel ^ "\"" ); close_out lakefile; + let lean_src_dir = Filename.concat project_dir out_name_camel in + if not (Sys.file_exists lean_src_dir) then Unix.mkdir lean_src_dir 0o775; let sail_dir = Reporting.get_sail_dir default_sail_dir in let _ = - Unix.system ("cp -r " ^ Filename.quote (sail_dir ^ "/src/sail_lean_backend/Sail") ^ " " ^ Filename.quote project_dir) + Unix.system + ("cp -r " ^ Filename.quote (sail_dir ^ "/src/sail_lean_backend/Sail") ^ " " ^ Filename.quote lean_src_dir) in let project_main = open_out (Filename.concat project_dir (out_name_camel ^ ".lean")) in + output_string project_main ("import " ^ out_name_camel ^ ".Sail.Sail\n\n"); project_main let output (out_name : string) ast default_sail_dir = diff --git a/src/sail_lem_backend/sail_plugin_lem.ml b/src/sail_lem_backend/sail_plugin_lem.ml index 2fe2d41ef..3e022ec97 100644 --- a/src/sail_lem_backend/sail_plugin_lem.ml +++ b/src/sail_lem_backend/sail_plugin_lem.ml @@ -57,24 +57,33 @@ let opt_lem_split_files : bool ref = ref false let lem_options = [ - ( "-lem_output_dir", + ( Flag.create ~prefix:["lem"] ~arg:"directory" "output_dir", Arg.String (fun dir -> opt_lem_output_dir := Some dir), - " set a custom directory to output generated Lem" + "set a custom directory to output generated Lem" ); - ( "-isa_output_dir", + ( Flag.create ~prefix:["lem"] ~arg:"directory" ~hide_prefix:true "isa_output_dir", Arg.String (fun dir -> opt_isa_output_dir := Some dir), - " set a custom directory to output generated Isabelle auxiliary theories" + "set a custom directory to output generated Isabelle auxiliary theories" ); - ("-lem_split_files", Arg.Set opt_lem_split_files, " split output into multiple files, one per input file"); - ( "-lem_lib", + ( Flag.create ~prefix:["lem"] "split_files", + Arg.Set opt_lem_split_files, + "split output into multiple files, one per input file" + ); + ( Flag.create ~prefix:["lem"] ~arg:"filename" "lib", Arg.String (fun l -> opt_libs_lem := l :: !opt_libs_lem), - " provide additional library to open in Lem output" + "provide additional library to open in Lem output" + ); + ( Flag.create ~prefix:["lem"] "sequential", + Arg.Set Pretty_print_lem.opt_sequential, + "use sequential state monad for Lem output" + ); + ( Flag.create ~prefix:["lem"] "mwords", + Arg.Set Monomorphise.opt_mwords, + "use native machine word library for Lem output" ); - ("-lem_sequential", Arg.Set Pretty_print_lem.opt_sequential, " use sequential state monad for Lem output"); - ("-lem_mwords", Arg.Set Monomorphise.opt_mwords, " use native machine word library for Lem output"); - ( "-lem_extern_type", + ( Flag.create ~prefix:["lem"] ~arg:"typename" "extern_type", Arg.String Pretty_print_lem.(fun ty -> opt_extern_types := ty :: !opt_extern_types), - " do not generate a definition for the type" + "do not generate a definition for the type" ); ] diff --git a/src/sail_ocaml_backend/sail_plugin_ocaml.ml b/src/sail_ocaml_backend/sail_plugin_ocaml.ml index 9934dbf65..08bd2be5b 100644 --- a/src/sail_ocaml_backend/sail_plugin_ocaml.ml +++ b/src/sail_ocaml_backend/sail_plugin_ocaml.ml @@ -52,22 +52,22 @@ let opt_ocaml_generators = ref ([] : string list) let ocaml_options = [ - ("-ocaml_nobuild", Arg.Set Ocaml_backend.opt_ocaml_nobuild, " do not build generated OCaml"); - ( "-ocaml_trace", + (Flag.create ~prefix:["ocaml"] "nobuild", Arg.Set Ocaml_backend.opt_ocaml_nobuild, "do not build generated OCaml"); + ( Flag.create ~prefix:["ocaml"] "trace", Arg.Set Ocaml_backend.opt_trace_ocaml, - " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml" + "output an OCaml translated version of the input with tracing instrumentation, implies -ocaml" ); - ( "-ocaml_build_dir", + ( Flag.create ~prefix:["ocaml"] ~arg:"directory" "build_dir", Arg.String (fun dir -> Ocaml_backend.opt_ocaml_build_dir := dir), - " set a custom directory to build generated OCaml" + "set a custom directory to build generated OCaml" ); - ( "-ocaml_coverage", + ( Flag.create ~prefix:["ocaml"] "coverage", Arg.Set Ocaml_backend.opt_ocaml_coverage, - " build OCaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx)." + "build OCaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx)." ); - ( "-ocaml_generators", + ( Flag.create ~prefix:["ocaml"] ~arg:"types" "generators", Arg.String (fun s -> opt_ocaml_generators := s :: !opt_ocaml_generators), - " produce random generators for the given types" + "produce random generators for the given types" ); ] @@ -115,17 +115,17 @@ let opt_tofrominterp_output_dir : string option ref = ref None let tofrominterp_options = [ - ( "-tofrominterp_lem", + ( Flag.create ~prefix:["tofrominterp"] "lem", Arg.Set ToFromInterp_backend.lem_mode, - " output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp" + "output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp" ); - ( "-tofrominterp_mwords", + ( Flag.create ~prefix:["tofrominterp"] "mwords", Arg.Set ToFromInterp_backend.mword_mode, - " output embedding translation in machine-word mode rather than bit-list mode, implies -tofrominterp" + "output embedding translation in machine-word mode rather than bit-list mode, implies -tofrominterp" ); - ( "-tofrominterp_output_dir", + ( Flag.create ~prefix:["tofrominterp"] ~arg:"directory" "output_dir", Arg.String (fun dir -> opt_tofrominterp_output_dir := Some dir), - " set a custom directory to output embedding translation OCaml" + "set a custom directory to output embedding translation OCaml" ); ] @@ -149,7 +149,7 @@ let tofrominterp_target out_file { ast; _ } = let _ = Target.register ~name:"tofrominterp" - ~description:" output OCaml functions to translate between shallow embedding and interpreter" + ~description:"output OCaml functions to translate between shallow embedding and interpreter" ~options:tofrominterp_options ~rewrites:tofrominterp_rewrites tofrominterp_target let marshal_target out_file { ast; env; _ } = @@ -164,5 +164,5 @@ let marshal_target out_file { ast; env; _ } = close_out f let _ = - Target.register ~name:"marshal" ~description:" OCaml-marshal out the rewritten AST to a file" + Target.register ~name:"marshal" ~description:"OCaml-marshal out the rewritten AST to a file" ~rewrites:tofrominterp_rewrites marshal_target diff --git a/src/sail_output/sail_plugin_output.ml b/src/sail_output/sail_plugin_output.ml index b2e642293..415f8c66e 100644 --- a/src/sail_output/sail_plugin_output.ml +++ b/src/sail_output/sail_plugin_output.ml @@ -50,9 +50,9 @@ open Interactive.State let output_sail_options = [ - ( "-output_sail_dir", + ( Flag.create ~prefix:["output_sail"] ~arg:"directory" "dir", Arg.String (fun dir -> Frontend.opt_reformat := Some dir), - " set a directory to output pretty-printed Sail" + "set a directory to output pretty-printed Sail" ); ] @@ -63,4 +63,4 @@ let sail_target out_file { ast; _ } = let _ = Target.register ~name:"sail" ~flag:"output_sail" ~options:output_sail_options - ~description:" print Sail code after type checking and initial rewriting" sail_target + ~description:"print Sail code after type checking and initial rewriting" sail_target diff --git a/src/sail_smt_backend/sail_plugin_smt.ml b/src/sail_smt_backend/sail_plugin_smt.ml index 3b530a9c4..4ada592f9 100644 --- a/src/sail_smt_backend/sail_plugin_smt.ml +++ b/src/sail_smt_backend/sail_plugin_smt.ml @@ -64,30 +64,42 @@ let set_smt_auto_solver arg = let smt_options = [ - ("-smt_auto", Arg.Tuple [Arg.Set opt_smt_auto], " automatically call the smt solver on generated SMT"); - ( "-smt_auto_solver", + ( Flag.create ~prefix:["smt"] "auto", + Arg.Tuple [Arg.Set opt_smt_auto], + "automatically call the smt solver on generated SMT" + ); + ( Flag.create ~prefix:["smt"] ~arg:"cvc4/cvc5/z3" "auto_solver", Arg.Tuple [Arg.Set opt_smt_auto; Arg.String set_smt_auto_solver], - " set the solver to use for counterexample checks (default cvc5)" + "set the solver to use for counterexample checks (default cvc5)" + ); + ( Flag.create ~prefix:["smt"] "ignore_overflow", + Arg.Set opt_smt_ignore_overflow, + "ignore integer overflow in generated SMT" ); - ("-smt_ignore_overflow", Arg.Set opt_smt_ignore_overflow, " ignore integer overflow in generated SMT"); - ( "-smt_int_size", + ( Flag.create ~prefix:["smt"] ~arg:"n" "int_size", Arg.String (fun n -> opt_smt_unknown_integer_width := int_of_string n), - " set a bound of n on the maximum integer bitwidth for generated SMT (default 128)" + "set a bound of n on the maximum integer bitwidth for generated SMT (default 128)" ); - ("-smt_propagate_vars", Arg.Unit (fun () -> ()), " (deprecated) propgate variables through generated SMT"); - ( "-smt_bits_size", + ( Flag.create ~prefix:["smt"] "propagate_vars", + Arg.Unit (fun () -> ()), + "(deprecated) propgate variables through generated SMT" + ); + ( Flag.create ~prefix:["smt"] ~arg:"n" "bits_size", Arg.String (fun n -> opt_smt_unknown_bitvector_width := int_of_string n), - " set a size bound of n for unknown-length bitvectors in generated SMT (default 64)" + "set a size bound of n for unknown-length bitvectors in generated SMT (default 64)" ); - ( "-smt_vector_size", + ( Flag.create ~prefix:["smt"] ~arg:"n" "vector_size", Arg.String (fun n -> opt_smt_unknown_generic_vector_width := int_of_string n), - " set a bound of 2 ^ n for generic vectors in generated SMT (default 5)" + "set a bound of 2 ^ n for generic vectors in generated SMT (default 5)" ); - ( "-smt_include", + ( Flag.create ~prefix:["smt"] ~arg:"filename" "include", Arg.String (fun i -> opt_smt_includes := i :: !opt_smt_includes), - " insert additional file in SMT output" + "insert additional file in SMT output" + ); + ( Flag.create ~prefix:["smt"] "disable_specialization", + Arg.Clear opt_smt_specialize, + "Disable generic specialization when generating SMT" ); - ("-smt_disable_specialization", Arg.Clear opt_smt_specialize, " Disable generic specialization when generating SMT"); ] let smt_rewrites = diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index c73f9626a..6af55cc08 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -108,23 +108,23 @@ let opt_disable_optimizations = ref false let verilog_options = [ - ( "-sv_output_dir", + ( Flag.create ~prefix:["sv"] ~arg:"path" "output_dir", Arg.String (fun s -> opt_output_dir := Some s), - " set the output directory for generated SystemVerilog files" + "set the output directory for generated SystemVerilog files" ); - ( "-sv_include", + ( Flag.create ~prefix:["sv"] ~arg:"file" "include", Arg.String (fun s -> opt_includes := s :: !opt_includes), - " add include directive to generated SystemVerilog file" + "add include directive to generated SystemVerilog file" ); - ( "-sv_toplevel", + ( Flag.create ~prefix:["sv"] ~arg:"id" "toplevel", Arg.String (fun s -> Specialize.add_initial_calls (IdSet.singleton (mk_id s)); opt_toplevel := s ), - " Sail function to use as toplevel module" + "Sail function to use as toplevel module" ); - ( "-sv_verilate", + ( Flag.create ~prefix:["sv"] ~arg:"compile|run" "verilate", Arg.String (fun opt -> if opt = "run" then opt_verilate := Verilator_run @@ -135,59 +135,65 @@ let verilog_options = "Invalid argument for -sv_verilate option. Valid options are either 'run' or 'compile'." ) ), - " Invoke verilator on generated output" + "Invoke verilator on generated output" ); - ( "-sv_verilate_args", + ( Flag.create ~prefix:["sv"] ~arg:"string" "verilate_args", Arg.String (fun s -> append_flag opt_verilate_args s), - " Extra arguments to pass to verilator" + "Extra arguments to pass to verilator" ); - ( "-sv_verilate_cflags", + ( Flag.create ~prefix:["sv"] ~arg:"string" "verilate_cflags", Arg.String (fun s -> append_flag opt_verilate_cflags s), - " Verilator CFLAGS argument" + "Verilator CFLAGS argument" ); - ( "-sv_verilate_ldflags", + ( Flag.create ~prefix:["sv"] ~arg:"string" "verilate_ldflags", Arg.String (fun s -> append_flag opt_verilate_ldflags s), - " Verilator LDFLAGS argument" + "Verilator LDFLAGS argument" ); - ( "-sv_verilate_link_sail_runtime", + ( Flag.create ~prefix:["sv"] "verilate_link_sail_runtime", Arg.Set opt_verilate_link_sail_runtime, - " Link the Sail C runtime with the generated verilator C++" + "Link the Sail C runtime with the generated verilator C++" ); - ("-sv_verilate_jobs", Arg.Int (fun i -> opt_verilate_jobs := i), " Provide the -j option to verilator"); - ("-sv_lines", Arg.Set opt_line_directives, " output `line directives"); - ("-sv_comb", Arg.Set opt_comb, " output an always_comb block instead of initial block"); - ("-sv_inregs", Arg.Set opt_inregs, " take register values from inputs"); - ("-sv_outregs", Arg.Set opt_outregs, " output register values"); - ( "-sv_int_size", + ( Flag.create ~prefix:["sv"] ~arg:"n" "verilate_jobs", + Arg.Int (fun i -> opt_verilate_jobs := i), + "Provide the -j option to verilator" + ); + (Flag.create ~prefix:["sv"] "lines", Arg.Set opt_line_directives, "output `line directives"); + (Flag.create ~prefix:["sv"] "comb", Arg.Set opt_comb, "output an always_comb block instead of initial block"); + (Flag.create ~prefix:["sv"] "inregs", Arg.Set opt_inregs, "take register values from inputs"); + (Flag.create ~prefix:["sv"] "outregs", Arg.Set opt_outregs, "output register values"); + ( Flag.create ~prefix:["sv"] ~arg:"n" "int_size", Arg.Int (fun i -> opt_max_unknown_integer_width := i), - " set the maximum width for unknown integers" + "set the maximum width for unknown integers" ); - ( "-sv_bits_size", + ( Flag.create ~prefix:["sv"] ~arg:"n" "bits_size", Arg.Int (fun i -> opt_max_unknown_bitvector_width := i), - " set the maximum width for bitvectors with unknown width" + "set the maximum width for bitvectors with unknown width" ); - ("-sv_no_strings", Arg.Set opt_no_strings, " don't emit any strings, instead emit units"); - ("-sv_no_packed", Arg.Set opt_no_packed, " don't emit packed datastructures"); - ("-sv_no_assertions", Arg.Set opt_no_assertions, " ignore all Sail asserts"); - ("-sv_never_pack_unions", Arg.Set opt_never_pack_unions, " never emit a packed union"); - ("-sv_padding", Arg.Set opt_padding, " add padding on packed unions"); - ( "-sv_unreachable", + (Flag.create ~prefix:["sv"] "no_strings", Arg.Set opt_no_strings, "don't emit any strings, instead emit units"); + (Flag.create ~prefix:["sv"] "no_packed", Arg.Set opt_no_packed, "don't emit packed datastructures"); + (Flag.create ~prefix:["sv"] "no_assertions", Arg.Set opt_no_assertions, "ignore all Sail asserts"); + (Flag.create ~prefix:["sv"] "never_pack_unions", Arg.Set opt_never_pack_unions, "never emit a packed union"); + (Flag.create ~prefix:["sv"] "padding", Arg.Set opt_padding, "add padding on packed unions"); + ( Flag.create ~prefix:["sv"] ~arg:"functionname" "unreachable", Arg.String (fun fn -> opt_unreachable := fn :: !opt_unreachable), - " Mark function as unreachable." + "Mark function as unreachable." ); - ("-sv_nomem", Arg.Set opt_nomem, " don't emit a dynamic memory implementation"); - ( "-sv_fun2wires", + (Flag.create ~prefix:["sv"] "nomem", Arg.Set opt_nomem, "don't emit a dynamic memory implementation"); + ( Flag.create ~prefix:["sv"] ~arg:"functionname" "fun2wires", Arg.String (fun fn -> opt_fun2wires := fn :: !opt_fun2wires), - " Use input/output ports instead of emitting a function call" + "Use input/output ports instead of emitting a function call" ); - ( "-sv_specialize", + ( Flag.create ~prefix:["sv"] ~arg:"n" "specialize", Arg.Int (fun i -> opt_int_specialize := Some i), - " Run n specialization passes on Sail Int-kinded type variables" + "Run n specialization passes on Sail Int-kinded type variables" + ); + ( Flag.create ~prefix:["sv"] "disable_optimizations", + Arg.Set opt_disable_optimizations, + "disable SystemVerilog specific optimizations" ); - ("-sv_disable_optimizations", Arg.Set opt_disable_optimizations, " disable SystemVerilog specific optimizations"); - ( "-sv_dpi", + ( Flag.create ~prefix:["sv"] ~arg:"set" "dpi", Arg.String (fun s -> opt_dpi_sets := StringSet.add s !opt_dpi_sets), - " Use SystemVerilog DPI-C for a set of primitives (e.g. memory)" + "Use SystemVerilog DPI-C for a set of primitives (e.g. memory)" ); ] diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean index 3807b800a..4259a876e 100644 --- a/test/lean/bitvec_operation.expected.lean +++ b/test/lean/bitvec_operation.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail def bitvector_eq (x : BitVec 16) (y : BitVec 16) : Bool := (Eq x y) diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean index 2fad5dcfb..21299c2a4 100644 --- a/test/lean/enum.expected.lean +++ b/test/lean/enum.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail inductive E where | A | B | C deriving Inhabited diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean index cb4785ae3..274596012 100644 --- a/test/lean/extern.expected.lean +++ b/test/lean/extern.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail def extern_add : Int := (Int.add 5 4) diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean index 6691094c3..0bbfd363a 100644 --- a/test/lean/extern_bitvec.expected.lean +++ b/test/lean/extern_bitvec.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail def extern_const : BitVec 64 := (0xFFFF000012340000 : BitVec 64) diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean index b13e6ae83..75f318f27 100644 --- a/test/lean/let.expected.lean +++ b/test/lean/let.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail def foo : BitVec 16 := let z := (HOr.hOr (0xFFFF : BitVec 16) (0xABCD : BitVec 16)) diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index 37529f301..168e57e8d 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail structure My_struct where field1 : Int diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean index f7df77729..6a4db83d8 100644 --- a/test/lean/trivial.expected.lean +++ b/test/lean/trivial.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail def foo (y : Unit) : Unit := y diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean index 5ac53560d..7ac4b0aed 100644 --- a/test/lean/tuples.expected.lean +++ b/test/lean/tuples.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail def tuple1 : (Int × Int × (BitVec 2 × Unit)) := (3, 5, ((0b10 : BitVec 2), ())) diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean index bf45cdbd3..85eec97e7 100644 --- a/test/lean/typquant.expected.lean +++ b/test/lean/typquant.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import Out.Sail.Sail /-- Type quantifiers: n : Int -/ def foo (n : Int) : BitVec 4 := diff --git a/test/typecheck/fail/mp_tuple_loc.expect b/test/typecheck/fail/mp_tuple_loc.expect new file mode 100644 index 000000000..f944f3f91 --- /dev/null +++ b/test/typecheck/fail/mp_tuple_loc.expect @@ -0,0 +1,5 @@ +Type error: +fail/mp_tuple_loc.sail:9.9-24: +9 | () <-> foo((), (), ()), +  | ^-------------^ +  | Tuple mapping-pattern and tuple type have different length diff --git a/test/typecheck/fail/mp_tuple_loc.sail b/test/typecheck/fail/mp_tuple_loc.sail new file mode 100644 index 000000000..ebbf0f7f6 --- /dev/null +++ b/test/typecheck/fail/mp_tuple_loc.sail @@ -0,0 +1,16 @@ + +enum E = A + +mapping foo : (unit, unit) <-> E = { + ((), ()) <-> A, +} + +mapping bar : unit <-> E = { + () <-> foo((), (), ()), +} + +val main : unit -> unit + +function main() = { + let _ : E = bar(); +}