diff options
Diffstat (limited to 'src')
42 files changed, 332 insertions, 446 deletions
diff --git a/src/ast_defs.ml b/src/ast_defs.ml index 0ce71618..f6b83c2c 100644 --- a/src/ast_defs.ml +++ b/src/ast_defs.ml @@ -50,4 +50,10 @@ open Ast -type 'a ast = Defs of 'a def list +type 'a ast = { + defs : 'a def list + } + +let empty_ast = { + defs = [] + } diff --git a/src/ast_util.ml b/src/ast_util.ml index b0137880..40cb7d98 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -713,8 +713,7 @@ and map_def_annot f = function | DEF_reg_dec ds -> DEF_reg_dec (map_decspec_annot f ds) | DEF_internal_mutrec fds -> DEF_internal_mutrec (List.map (map_fundef_annot f) fds) | DEF_pragma (name, arg, l) -> DEF_pragma (name, arg, l) -and map_ast_annot f = function - | Defs defs -> Defs (List.map (map_def_annot f) defs) +and map_ast_annot f ast = { ast with defs = List.map (map_def_annot f) ast.defs } and map_loop_measure_annot f = function | Loop (loop, exp) -> Loop (loop, map_exp_annot f exp) @@ -1086,10 +1085,11 @@ let ids_of_def = function | DEF_spec vs -> IdSet.singleton (id_of_val_spec vs) | DEF_internal_mutrec fds -> IdSet.of_list (List.map id_of_fundef fds) | _ -> IdSet.empty -let ids_of_ast (Defs defs) = +let ids_of_defs defs = List.fold_left IdSet.union IdSet.empty (List.map ids_of_def defs) +let ids_of_ast ast = ids_of_defs ast.defs -let val_spec_ids (Defs defs) = +let val_spec_ids defs = let val_spec_id (VS_aux (vs_aux, _)) = match vs_aux with | VS_val_spec (_, id, _, _) -> id @@ -1540,14 +1540,15 @@ let rec split_defs' f defs acc = | def :: defs when f def -> Some (acc, def, defs) | def :: defs -> split_defs' f defs (def :: acc) -let split_ast f (Defs defs) = +let split_defs f defs = match split_defs' f defs [] with | None -> None | Some (pre_defs, def, post_defs) -> - Some (Defs (List.rev pre_defs), def, Defs post_defs) + Some (List.rev pre_defs, def, post_defs) -let append_ast (Defs ast1) (Defs ast2) = Defs (ast1 @ ast2) -let concat_ast asts = List.fold_right append_ast asts (Defs []) +let append_ast ast1 ast2 = { defs = ast1.defs @ ast2.defs } +let append_ast_defs ast defs = { ast with defs = ast.defs @ defs } +let concat_ast asts = List.fold_right append_ast asts empty_ast let type_union_id (Tu_aux (Tu_ty_id (_, id), _)) = id @@ -2217,7 +2218,7 @@ let rec find_annot_defs sl = function find_annot_defs sl defs | [] -> None -let rec find_annot_ast sl (Defs defs) = find_annot_defs sl defs +let rec find_annot_ast sl { defs; _ } = find_annot_defs sl defs let string_of_lx lx = let open Lexing in diff --git a/src/ast_util.mli b/src/ast_util.mli index d9f80778..21a546ee 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -455,17 +455,19 @@ val rename_valspec : id -> 'a val_spec -> 'a val_spec val rename_fundef : id -> 'a fundef -> 'a fundef -val split_ast : ('a def -> bool) -> 'a ast -> ('a ast * 'a def * 'a ast) option +val split_defs : ('a def -> bool) -> 'a def list -> ('a def list * 'a def * 'a def list) option val append_ast : 'a ast -> 'a ast -> 'a ast +val append_ast_defs : 'a ast -> 'a def list -> 'a ast val concat_ast : 'a ast list -> 'a ast val type_union_id : type_union -> id val ids_of_def : 'a def -> IdSet.t +val ids_of_defs : 'a def list -> IdSet.t val ids_of_ast : 'a ast -> IdSet.t -val val_spec_ids : 'a ast -> IdSet.t +val val_spec_ids : 'a def list -> IdSet.t val pat_ids : 'a pat -> IdSet.t diff --git a/src/bitfield.ml b/src/bitfield.ml index e4813e44..46c18735 100644 --- a/src/bitfield.ml +++ b/src/bitfield.ml @@ -58,12 +58,6 @@ open Ast_util let bitvec size order = Printf.sprintf "bitvector(%i, %s)" size (string_of_order order) -let rec combine = function - | [] -> Defs [] - | (Defs defs) :: ast -> - let (Defs defs') = combine ast in - Defs (defs @ defs') - let newtype name size order = let chunks_64 = Util.list_init (size / 64) (fun i -> Printf.sprintf "%s_chunk_%i : bitvector(64, %s)" name i (string_of_order order)) @@ -76,7 +70,7 @@ let newtype name size order = chunk_rem :: List.rev chunks_64 in let nt = Printf.sprintf "struct %s = {\n %s }" name (Util.string_of_list ",\n " (fun x -> x) chunks) in - ast_of_def_string nt + defs_of_string nt let rec translate_indices hi lo = if hi / 64 = lo / 64 then @@ -98,7 +92,7 @@ let constructor name order start stop = "}" ] in - combine [ast_of_def_string constructor_val; ast_of_def_string constructor_function] + List.concat [defs_of_string constructor_val; defs_of_string constructor_function] (* For every index range, create a getter and setter *) let index_range_getter name field order start stop = @@ -109,7 +103,7 @@ let index_range_getter name field order start stop = Printf.sprintf "v.%s_chunk_%i[%i .. %i]" name chunk start stop in let irg_function = Printf.sprintf "function _get_%s_%s v = %s" name field (Util.string_of_list " @ " body indices) in - combine [ast_of_def_string irg_val; ast_of_def_string irg_function] + List.concat [defs_of_string irg_val; defs_of_string irg_function] let index_range_setter name field order start stop = let indices = translate_indices start stop in @@ -128,7 +122,7 @@ let index_range_setter name field order start stop = "}" ] in - combine [ast_of_def_string irs_val; ast_of_def_string irs_function] + List.concat [defs_of_string irs_val; defs_of_string irs_function] let index_range_update name field order start stop = let indices = translate_indices start stop in @@ -146,10 +140,10 @@ let index_range_update name field order start stop = ] in let iru_overload = Printf.sprintf "overload update_%s = {_update_%s_%s}" field name field in - combine [ast_of_def_string iru_val; ast_of_def_string iru_function; ast_of_def_string iru_overload] + List.concat [defs_of_string iru_val; defs_of_string iru_function; defs_of_string iru_overload] let index_range_overload name field order = - ast_of_def_string (Printf.sprintf "overload _mod_%s = {_get_%s_%s, _set_%s_%s}" field name field name field) + defs_of_string (Printf.sprintf "overload _mod_%s = {_get_%s_%s, _set_%s_%s}" field name field name field) let index_range_accessor (eval, typ_error) name field order (BF_aux (bf_aux, l)) = let getter n m = index_range_getter name field order (Big_int.to_int n) (Big_int.to_int m) in @@ -162,10 +156,10 @@ let index_range_accessor (eval, typ_error) name field order (BF_aux (bf_aux, l)) match bf_aux with | BF_single n -> let n = const_fold n in - combine [getter n n; setter n n; update n n; overload] + List.concat [getter n n; setter n n; update n n; overload] | BF_range (n, m) -> let n, m = const_fold n, const_fold m in - combine [getter n m; setter n m; update n m; overload] + List.concat [getter n m; setter n m; update n m; overload] | BF_concat _ -> failwith "Unimplemented" let field_accessor (eval, typ_error) name order (id, ir) = @@ -176,5 +170,5 @@ let macro (eval, typ_error) id size order ranges = let ranges = (mk_id "bits", BF_aux (BF_range (nconstant (Big_int.of_int (size - 1)), nconstant (Big_int.of_int 0)), Parse_ast.Unknown)) :: ranges in - combine ([newtype name size order; constructor name order (size - 1) 0] - @ List.map (field_accessor (eval, typ_error) name order) ranges) + List.concat ([newtype name size order; constructor name order (size - 1) 0] + @ List.map (field_accessor (eval, typ_error) name order) ranges) diff --git a/src/cgen_backend.ml b/src/cgen_backend.ml deleted file mode 100644 index 3bca3fa1..00000000 --- a/src/cgen_backend.ml +++ /dev/null @@ -1,78 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* 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 *) -(* *) -(* All rights reserved. *) -(* *) -(* This software was developed by the University of Cambridge Computer *) -(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) -(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in *) -(* the documentation and/or other materials provided with the *) -(* distribution. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) -(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) -(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) -(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) -(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) -(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) -(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) -(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) -(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) -(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) -(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) -(* SUCH DAMAGE. *) -(**************************************************************************) - -open Ast -open Ast_defs -open Ast_util -open PPrint - -let to_string doc = - let b = Buffer.create 120 in - ToBuffer.pretty 1. 120 b doc; - Buffer.contents b - -let do_mapdef_thing (MD_aux (MD_mapping (_, _, clauses), _)) = - print_endline ("Mapping has " ^ string_of_int (List.length clauses) ^ " clauses") - -let rec list_registers = function - | [] -> () - | (DEF_reg_dec reg) :: defs -> - print_endline (to_string (Pretty_print_sail.doc_dec reg)); - list_registers defs - | (DEF_mapdef mapdef) :: defs -> - do_mapdef_thing mapdef; - list_registers defs - | def :: defs -> - list_registers defs - -let output env (Defs defs) = - let xlenbits = mk_typ (Typ_id (mk_id "xlenbits")) in - print_endline (string_of_typ (Type_check.Env.expand_synonyms env xlenbits)); - list_registers defs diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index b7bc0a69..cea1fe93 100644 --- a/src/constant_propagation.ml +++ b/src/constant_propagation.ml @@ -301,16 +301,16 @@ let is_env_inconsistent env ksubsts = module StringSet = Set.Make(String) module StringMap = Map.Make(String) -let const_props target defs ref_vars = +let const_props target ast ref_vars = let const_fold exp = (* Constant-fold function applications with constant arguments *) let interpreter_istate = (* Do not interpret undefined_X functions *) let open Interpreter in - let undefined_builtin_ids = ids_of_ast (Defs Initial_check.undefined_builtin_val_specs) in + let undefined_builtin_ids = ids_of_defs Initial_check.undefined_builtin_val_specs in let remove_primop id = StringMap.remove (string_of_id id) in let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in - let (lstate, gstate) = Constant_fold.initial_state defs Type_check.initial_env in + let (lstate, gstate) = Constant_fold.initial_state ast Type_check.initial_env in (lstate, { gstate with primops = remove_undefined_primops gstate.primops }) in try @@ -328,9 +328,7 @@ let const_props target defs ref_vars = Bindings.add id exp m | _ -> m in - match defs with - | Defs defs -> - List.fold_left add Bindings.empty defs + List.fold_left add Bindings.empty ast.defs in let replace_constant (E_aux (e,annot) as exp) = match e with diff --git a/src/constant_propagation_mutrec.ml b/src/constant_propagation_mutrec.ml index 67d218dd..421964f4 100644 --- a/src/constant_propagation_mutrec.ml +++ b/src/constant_propagation_mutrec.ml @@ -159,7 +159,7 @@ let const_prop target defs substs ksubsts exp = in Constant_propagation.const_prop target - (Defs defs) + defs (Constant_propagation.referenced_vars exp) (substs, nexp_substs) Bindings.empty @@ -167,7 +167,7 @@ let const_prop target defs substs ksubsts exp = |> fst (* Propagate constant arguments into function clause pexp *) -let prop_args_pexp target defs ksubsts args pexp = +let prop_args_pexp target ast ksubsts args pexp = let pat, guard, exp, annot = destruct_pexp pexp in let pats = match pat with | P_aux (P_tup pats, _) -> pats @@ -184,14 +184,14 @@ let prop_args_pexp target defs ksubsts args pexp = else (pat :: pats, substs) in let pats, substs = List.fold_right2 match_arg args pats ([], Bindings.empty) in - let exp' = const_prop target defs substs ksubsts exp in + let exp' = const_prop target ast substs ksubsts exp in let pat' = match pats with | [pat] -> pat | _ -> P_aux (P_tup pats, (Parse_ast.Unknown, empty_tannot)) in construct_pexp (pat', guard, exp', annot) -let rewrite_ast target env (Defs defs) = +let rewrite_ast target env ({ defs; _ } as ast) = let rec rewrite = function | [] -> [] | DEF_internal_mutrec mutrecs :: ds -> @@ -206,7 +206,7 @@ let rewrite_ast target env (Defs defs) = | [] -> [infer_exp env (mk_lit_exp L_unit)] | args' -> args' in - if not (IdSet.mem id' (ids_of_ast (Defs !valspecs))) then begin + if not (IdSet.mem id' (ids_of_defs !valspecs)) then begin (* Generate copy of function with constant arguments propagated in *) let (FD_aux (FD_function (_, _, _, fcls), _)) = List.find (fun fd -> Id.compare id (id_of_fundef fd) = 0) mutrecs @@ -214,7 +214,7 @@ let rewrite_ast target env (Defs defs) = let valspec, ksubsts = generate_val_spec env id args l annot in let const_prop_funcl (FCL_aux (FCL_Funcl (_, pexp), (l, _))) = let pexp' = - prop_args_pexp target defs ksubsts args pexp + prop_args_pexp target ast ksubsts args pexp |> rewrite_pexp |> strip_pexp in @@ -235,7 +235,7 @@ let rewrite_ast target env (Defs defs) = let pexp' = if List.exists (fun id' -> Id.compare id id' = 0) !targets then let pat, guard, body, annot = destruct_pexp pexp in - let body' = const_prop target defs Bindings.empty KBindings.empty body in + let body' = const_prop target ast Bindings.empty KBindings.empty body in rewrite_pexp (construct_pexp (pat, guard, recheck_exp body', annot)) else pexp in FCL_aux (FCL_Funcl (id, pexp'), a) @@ -244,9 +244,9 @@ let rewrite_ast target env (Defs defs) = FD_aux (FD_function (ropt, topt, eopt, fcls'), a) in let mutrecs' = List.map (fun fd -> DEF_fundef (rewrite_fundef fd)) mutrecs in - let (Defs fdefs) = fst (check env (Defs (!valspecs @ !fundefs))) in + let fdefs = fst (check_defs env (!valspecs @ !fundefs)) in mutrecs' @ fdefs @ rewrite ds | d :: ds -> d :: rewrite ds in - Spec_analysis.top_sort_defs (Defs (rewrite defs)) + Spec_analysis.top_sort_defs { ast with defs = rewrite defs } diff --git a/src/initial_check.ml b/src/initial_check.ml index c0d956c4..a958dced 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -847,7 +847,7 @@ let to_ast ctx (P.Defs files) = let defs', ctx = to_ast_defs ctx file in (defs @ wrap_file (fst file) defs', ctx) ) ([], ctx) files in - Defs defs, ctx + { defs = defs }, ctx let initial_ctx = { type_constructors = @@ -931,7 +931,7 @@ let undefined_builtin_val_specs = extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> bitvector('n, dec) effect {undef}"; extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"] -let generate_undefineds vs_ids (Defs defs) = +let generate_undefineds vs_ids defs = let undefined_builtins = if !have_undefined_builtins then [] @@ -1026,14 +1026,14 @@ let generate_undefineds vs_ids (Defs defs) = def :: undefined_defs defs | [] -> [] in - Defs (undefined_builtins @ undefined_defs defs) + undefined_builtins @ undefined_defs defs let rec get_registers = function | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) :: defs -> (typ, id) :: get_registers defs | _ :: defs -> get_registers defs | [] -> [] -let generate_initialize_registers vs_ids (Defs defs) = +let generate_initialize_registers vs_ids defs = let regs = get_registers defs in let initialize_registers = if IdSet.mem (mk_id "initialize_registers") vs_ids || regs = [] then [] @@ -1043,9 +1043,9 @@ let generate_initialize_registers vs_ids (Defs defs) = (mk_pat (P_lit (mk_lit L_unit))) (mk_exp (E_block (List.map (fun (typ, id) -> mk_exp (E_assign (mk_lexp (LEXP_cast (typ, id)), mk_lit_exp L_undef))) regs)))]] in - Defs (defs @ initialize_registers) + defs @ initialize_registers -let generate_enum_functions vs_ids (Defs defs) = +let generate_enum_functions vs_ids defs = let rec gen_enums = function | DEF_type (TD_aux (TD_enum (id, elems, _), _)) as enum :: defs -> let enum_val_spec name quants typ = @@ -1101,21 +1101,23 @@ let generate_enum_functions vs_ids (Defs defs) = | def :: defs -> def :: gen_enums defs | [] -> [] in - Defs (gen_enums defs) + gen_enums defs let incremental_ctx = ref initial_ctx -let process_ast ?generate:(generate=true) defs = - let ast, ctx = to_ast !incremental_ctx defs in +let process_ast ?generate:(generate=true) ast = + let ast, ctx = to_ast !incremental_ctx ast in incremental_ctx := ctx; - let vs_ids = val_spec_ids ast in + let vs_ids = val_spec_ids ast.defs in if not !opt_undefined_gen && generate then - generate_enum_functions vs_ids ast + { ast with defs = generate_enum_functions vs_ids ast.defs } else if generate then - ast - |> generate_undefineds vs_ids - |> generate_enum_functions vs_ids - |> generate_initialize_registers vs_ids + { ast with + defs = ast.defs + |> generate_undefineds vs_ids + |> generate_enum_functions vs_ids + |> generate_initialize_registers vs_ids + } else ast @@ -1123,6 +1125,11 @@ let ast_of_def_string_with f str = let def = Parser.def_eof Lexer.token (Lexing.from_string str) in process_ast (P.Defs [("", f [def])]) + let ast_of_def_string str = let def = Parser.def_eof Lexer.token (Lexing.from_string str) in process_ast (P.Defs [("", [def])]) + +let defs_of_string str = + let def = Parser.def_eof Lexer.token (Lexing.from_string str) in + (process_ast (P.Defs [("", [def])])).defs diff --git a/src/initial_check.mli b/src/initial_check.mli index 0a5db7c2..6ca8ac80 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -103,6 +103,7 @@ val process_ast : ?generate:bool -> Parse_ast.defs -> unit ast val extern_of_string : id -> string -> unit def val val_spec_of_string : id -> string -> unit def +val defs_of_string : string -> unit def list val ast_of_def_string : string -> unit ast val ast_of_def_string_with : (Parse_ast.def list -> Parse_ast.def list) -> string -> unit ast val exp_of_string : string -> unit exp diff --git a/src/interactive.ml b/src/interactive.ml index d5d0fca4..20f16c6f 100644 --- a/src/interactive.ml +++ b/src/interactive.ml @@ -60,7 +60,7 @@ let opt_auto_interpreter_rewrites = ref false let env = ref Type_check.initial_env -let ast = ref (Defs []) +let ast = ref empty_ast let arg str = ("<" ^ str ^ ">") |> Util.yellow |> Util.clear diff --git a/src/interpreter.ml b/src/interpreter.ml index 29598993..b0faabce 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -977,10 +977,10 @@ let rec initialize_registers allow_registers gstate = initialize_registers allow_registers (process_def def) defs | [] -> gstate -let initial_state ?(registers=true) (Defs defs) env primops = - let gstate = initial_gstate primops defs env in +let initial_state ?(registers=true) ast env primops = + let gstate = initial_gstate primops ast.defs env in let gstate = - { (initialize_registers registers gstate defs) + { (initialize_registers registers gstate ast.defs) with allow_registers = registers } in initial_lstate, gstate diff --git a/src/isail.ml b/src/isail.ml index 7fcca62a..33de1d9c 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -111,7 +111,7 @@ let sail_logo = let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear -let vs_ids = ref (val_spec_ids !Interactive.ast) +let vs_ids = ref (val_spec_ids !Interactive.ast.defs) let interactive_state = ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops) @@ -150,8 +150,8 @@ let setup_sail_scripting () = let typschm = mk_typschm (mk_typquant []) (reflect_typ action) in mk_val_spec (VS_val_spec (typschm, mk_id name, [("_", name)], false)) ) !commands in - let val_specs, env' = Type_check.check !env (Defs val_specs) in - ast := append_ast !ast val_specs; + let val_specs, env' = Type_check.check_defs !env val_specs in + ast := append_ast_defs !ast val_specs; env := env'; if !sail_scripting_primops_once then ( @@ -538,7 +538,7 @@ let handle_input' input = print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast)) | ":ast" -> let chan = open_out arg in - Pretty_print_sail.pp_defs chan !Interactive.ast; + Pretty_print_sail.pp_ast chan !Interactive.ast; close_out chan | ":output" -> let chan = open_out arg in @@ -567,12 +567,12 @@ let handle_input' input = Interactive.ast := append_ast !Interactive.ast ast; Interactive.env := env; interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; - vs_ids := val_spec_ids !Interactive.ast + vs_ids := val_spec_ids !Interactive.ast.defs | ":u" | ":unload" -> - Interactive.ast := Ast_defs.Defs []; + Interactive.ast := Ast_defs.empty_ast; Interactive.env := Type_check.initial_env; interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; - vs_ids := val_spec_ids !Interactive.ast; + vs_ids := val_spec_ids !Interactive.ast.defs; (* See initial_check.mli for an explanation of why we need this. *) Initial_check.have_undefined_builtins := false; Process_file.clear_symbols () @@ -590,8 +590,8 @@ let handle_input' input = begin match args with | v :: "=" :: args -> let exp = Initial_check.exp_of_string (String.concat " " args) in - let ast, env = Type_check.check !Interactive.env (Defs [DEF_val (mk_letbind (mk_pat (P_id (mk_id v))) exp)]) in - Interactive.ast := append_ast !Interactive.ast ast; + let defs, env = Type_check.check_defs !Interactive.env [DEF_val (mk_letbind (mk_pat (P_id (mk_id v))) exp)] in + Interactive.ast := append_ast_defs !Interactive.ast defs; Interactive.env := env; interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; | _ -> print_endline "Invalid arguments for :let" @@ -648,12 +648,12 @@ let handle_input' input = Interactive.env := env; Interactive.ast := ast; interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; - vs_ids := val_spec_ids !Interactive.ast + vs_ids := val_spec_ids !Interactive.ast.defs | ":recheck_types" -> let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in Interactive.env := env; Interactive.ast := ast; - vs_ids := val_spec_ids !Interactive.ast + vs_ids := val_spec_ids !Interactive.ast.defs | ":compile" -> let out_name = match !Process_file.opt_file_out with | None -> "out.sail" @@ -686,17 +686,17 @@ let handle_input' input = Interactive.ast := append_ast !Interactive.ast ast; interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; Interactive.env := env; - vs_ids := val_spec_ids !Interactive.ast; + vs_ids := val_spec_ids !Interactive.ast.defs; print_endline ("(message \"Checked " ^ arg ^ " done\")\n"); with | Reporting.Fatal_error (Err_type (l, msg)) -> print_endline (emacs_error l (String.escaped msg)) end | ":unload" -> - Interactive.ast := Ast_defs.Defs []; + Interactive.ast := Ast_defs.empty_ast; Interactive.env := Type_check.initial_env; interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; - vs_ids := val_spec_ids !Interactive.ast; + vs_ids := val_spec_ids !Interactive.ast.defs; Initial_check.have_undefined_builtins := false; Process_file.clear_symbols () | ":typeat" -> diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index a7e64fe4..2fe21d93 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2196,10 +2196,10 @@ let sgen_finish = function Printf.sprintf " finish_%s();" (sgen_id id) | _ -> assert false -let rec get_recursive_functions (Defs defs) = +let rec get_recursive_functions defs = match defs with | DEF_internal_mutrec fundefs :: defs -> - IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions defs) | (DEF_fundef fdef as def) :: defs -> let open Rewriter in @@ -2216,11 +2216,11 @@ let rec get_recursive_functions (Defs defs) = let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in let _ = rewrite_def map_defs def in if IdSet.mem (id_of_fundef fdef) !ids then - IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs)) + IdSet.add (id_of_fundef fdef) (get_recursive_functions defs) else - get_recursive_functions (Defs defs) + get_recursive_functions defs - | _ :: defs -> get_recursive_functions (Defs defs) + | _ :: defs -> get_recursive_functions defs | [] -> IdSet.empty let jib_of_ast env ast = @@ -2230,7 +2230,7 @@ let jib_of_ast env ast = let compile_ast env output_chan c_includes ast = try - let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in + let recursive_functions = (Spec_analysis.top_sort_defs ast).defs |> get_recursive_functions in let cdefs, ctx = jib_of_ast env ast in let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml index ea4afd00..b92713ff 100644 --- a/src/jib/c_codegen.ml +++ b/src/jib/c_codegen.ml @@ -1666,10 +1666,10 @@ let sgen_finish = function Printf.sprintf " finish_%s();" (sgen_id id) | _ -> assert false -let rec get_recursive_functions (Defs defs) = +let rec get_recursive_functions defs = match defs with | DEF_internal_mutrec fundefs :: defs -> - IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions defs) | (DEF_fundef fdef as def) :: defs -> let open Rewriter in @@ -1686,11 +1686,11 @@ let rec get_recursive_functions (Defs defs) = let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in let _ = rewrite_def map_defs def in if IdSet.mem (id_of_fundef fdef) !ids then - IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs)) + IdSet.add (id_of_fundef fdef) (get_recursive_functions defs) else - get_recursive_functions (Defs defs) + get_recursive_functions defs - | _ :: defs -> get_recursive_functions (Defs defs) + | _ :: defs -> get_recursive_functions defs | [] -> IdSet.empty let codegen_output file_name docs = diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 4fd61a7d..cd4edd12 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -1642,7 +1642,7 @@ let sort_ctype_defs cdefs = ctype_defs @ cdefs -let compile_ast ctx (Defs defs) = +let compile_ast ctx ast = if !opt_memo_cache then (try if Sys.is_directory "_sbuild" then @@ -1653,9 +1653,9 @@ let compile_ast ctx (Defs defs) = | Sys_error _ -> Unix.mkdir "_sbuild" 0o775) else (); - let total = List.length defs in + let total = List.length ast.defs in let _, chunks, ctx = - List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs + List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) ast.defs in let cdefs = List.concat (List.rev chunks) in let cdefs, ctx = specialize_variants ctx [] cdefs in @@ -1669,4 +1669,4 @@ let add_special_functions env = let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in - snd (Type_error.check env (Defs [assert_vs; exit_vs; cons_vs])) + snd (Type_error.check_defs env [assert_vs; exit_vs; cons_vs]) diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index b03c1134..434ca8a9 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -118,7 +118,7 @@ let initial_ctx () = { tc_env = Type_check.initial_env; pragma_l = Parse_ast.Unknown; arg_stack = Stack.create (); - ast = Defs []; + ast = empty_ast; shared = Bindings.empty; preserved = IdSet.empty; events = ref EventMap.empty; diff --git a/src/latex.ml b/src/latex.ml index 7f9b1317..c2c61078 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -438,7 +438,7 @@ let tdef_id = function | TD_enum (id, _, _) -> id | TD_bitfield (id, _, _) -> id -let defs (Defs defs) = +let defs { defs; _ } = reset_state state; let preamble = string "\\providecommand\\saildoclabelled[2]{\\phantomsection\\label{#1}#2}" ^^ twice hardline in diff --git a/src/lexer.mll b/src/lexer.mll index 153467c1..fd320250 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -164,7 +164,6 @@ let kw_table = ("do", (fun _ -> Do)); ("mutual", (fun _ -> Mutual)); ("bitfield", (fun _ -> Bitfield)); - ("barr", (fun x -> Barr)); ("depend", (fun x -> Depend)); ("rreg", (fun x -> Rreg)); diff --git a/src/libsail.mllib b/src/libsail.mllib index 0651c59a..ff8ea23b 100644 --- a/src/libsail.mllib +++ b/src/libsail.mllib @@ -3,7 +3,6 @@ Ast Ast_util Bitfield C_backend -Cgen_backend Constant_fold Constant_propagation Constant_propagation_mutrec diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 968b1172..d86db99d 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -658,10 +658,10 @@ let apply_pat_choices choices = e_assert = rewrite_assert; e_case = rewrite_case } -let split_defs target all_errors splits env defs = +let split_defs target all_errors splits env ast = let no_errors_happened = ref true in let error_opt = if all_errors then Some no_errors_happened else None in - let split_constructors (Defs defs) = + let split_constructors defs = let sc_type_union q (Tu_aux (Tu_ty_id (ty, id), l)) = match split_src_type error_opt env id ty q with | None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)]) @@ -682,14 +682,14 @@ let split_defs target all_errors splits env defs = | _ -> ([], d) in let (refinements, defs') = List.split (List.map sc_def defs) - in (List.concat refinements, Defs defs') + in (List.concat refinements, defs') in - let (refinements, defs') = split_constructors defs in + let (refinements, defs') = split_constructors ast.defs in let subst_exp ref_vars substs ksubsts exp = let substs = bindings_from_list substs, ksubsts in - fst (Constant_propagation.const_prop target defs ref_vars substs Bindings.empty exp) + fst (Constant_propagation.const_prop target ast ref_vars substs Bindings.empty exp) in (* Split a variable pattern into every possible value *) @@ -773,7 +773,7 @@ let split_defs target all_errors splits env defs = (* Split variable patterns at the given locations *) - let map_locs ls (Defs defs) = + let map_locs ls defs = let rec match_l = function | Unknown -> [] | Unique (_, l) -> match_l l @@ -1171,11 +1171,11 @@ let split_defs target all_errors splits env defs = Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should have been rewritten before now" in - Defs (List.concat (List.mapi map_def defs)) + List.concat (List.mapi map_def defs) in - let (Defs defs'') = map_locs splits defs' in + let defs'' = map_locs splits defs' in Util.progress "Monomorphising " "done" (List.length defs'') (List.length defs''); - !no_errors_happened, (Defs defs'') + !no_errors_happened, { ast with defs = defs'' } @@ -1338,7 +1338,7 @@ let replace_type env typ = ("replace_type: Unsupported type " ^ string_of_typ typ)) -let rewrite_size_parameters target type_env (Defs defs) = +let rewrite_size_parameters target type_env ast = let open Rewriter in let open Util in @@ -1346,7 +1346,7 @@ let rewrite_size_parameters target type_env (Defs defs) = let ref_vars = Constant_propagation.referenced_vars exp in let substs = (Bindings.empty, KBindings.empty) in let assigns = Bindings.empty in - fst (Constant_propagation.const_prop target (Defs defs) ref_vars substs assigns exp) + fst (Constant_propagation.const_prop target ast ref_vars substs assigns exp) in let const_prop_pexp pexp = let (pat, guard, exp, a) = destruct_pexp pexp in @@ -1455,7 +1455,7 @@ in *) List.fold_left sizes_funcl fsizes funcls | _ -> fsizes in - let fn_sizes = List.fold_left sizes_def Bindings.empty defs in + let fn_sizes = List.fold_left sizes_def Bindings.empty ast.defs in let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),(l,annot))) = let pat,guard,body,(pl,_) = destruct_pexp pexp in @@ -1586,7 +1586,7 @@ in *) print_endline (string_of_id id ^ " needs " ^ String.concat ", " (List.map string_of_int args))) fn_sizes *) - Defs (List.map rewrite_def defs) + { ast with defs = List.map rewrite_def ast.defs } end @@ -2761,18 +2761,19 @@ let argset_to_list splits = in List.map argelt l -let analyse_defs debug env (Defs defs) = +let analyse_defs debug env ast = + let total_defs = List.length ast.defs in let def (idx,globals,r) d = begin match d with | DEF_fundef fd -> - Util.progress "Analysing " (string_of_id (id_of_fundef fd)) idx (List.length defs) + Util.progress "Analysing " (string_of_id (id_of_fundef fd)) idx total_defs | _ -> () end; let globals,r' = analyse_def debug env globals d in idx + 1, globals, merge r r' in - let _,_,r = List.fold_left def (0,Bindings.empty,empty) defs in - let _ = Util.progress "Analysing " "done" (List.length defs) (List.length defs) in + let _,_,r = List.fold_left def (0,Bindings.empty,empty) ast.defs in + let _ = Util.progress "Analysing " "done" total_defs total_defs in (* Resolve the interprocedural dependencies *) @@ -2829,7 +2830,7 @@ let fresh_sz_var = let () = counter := n+1 in mk_id ("sz#" ^ string_of_int n) -let add_extra_splits extras (Defs defs) = +let add_extra_splits extras defs = let success = ref true in let add_to_body extras (E_aux (_,(l,annot)) as e) = let l' = Generated l in @@ -2866,7 +2867,7 @@ let add_extra_splits extras (Defs defs) = | d -> d, [] in let defs, splits = List.split (List.map add_to_def defs) in - !success, Defs defs, List.concat splits + !success, defs, List.concat splits module MonoRewrites = struct @@ -3683,7 +3684,7 @@ let rec extract (E_aux (e,_)) = provide some way for the Lem pretty printer to know what to use; currently we just use two names for the cast, bitvector_cast_in and bitvector_cast_out, to let the pretty printer know whether to use the top-level environment. *) -let add_bitvector_casts global_env (Defs defs) = +let add_bitvector_casts global_env ({ defs; _ } as ast) = let rewrite_body id quant_kids top_env ret_typ exp = let rewrite_aux (e,ann) = match e with @@ -3834,7 +3835,7 @@ let add_bitvector_casts global_env (Defs defs) = let defs = List.mapi rewrite_def defs in let _ = Util.progress "Adding casts " "done" (List.length defs) (List.length defs) in let l = Generated Unknown in - let Defs cast_specs,_ = + let cast_specs, _ = (* TODO: use default/relevant order *) let kid = mk_kid "n" in let bitsn = bitvector_typ (nvar kid) dec_ord in @@ -3844,8 +3845,8 @@ let add_bitvector_casts global_env (Defs defs) = mk_val_spec (VS_val_spec (ts,name,[("_", "zeroExtend")],false)) in let defs = List.map mkfn (IdSet.elements !specs_required) in - check initial_env (Defs defs) - in Defs (cast_specs @ defs) + check_defs initial_env defs + in { ast with defs = cast_specs @ defs } end let replace_nexp_in_typ env typ orig new_nexp = @@ -3908,7 +3909,7 @@ let fresh_nexp_kid nexp = types, which these are explicitly supposed to be. *) mk_kid (mangle_nexp nexp (*^ "#"*)) -let rewrite_toplevel_nexps (Defs defs) = +let rewrite_toplevel_nexps ({ defs; _ } as ast) = let find_nexp env nexp_map nexp = let is_equal (kid,nexp') = prove __POS__ env (nc_eq nexp nexp') in List.find is_equal nexp_map @@ -4076,7 +4077,7 @@ let rewrite_toplevel_nexps (Defs defs) = (* Allow use of div and mod in nexp rewriting during later typechecking passes to help prove equivalences such as (8 * 'n) = 'p8_times_n# *) Type_check.opt_smt_div := true; - Defs (List.rev defs) + { ast with defs = List.rev defs } type options = { auto : bool; @@ -4094,28 +4095,29 @@ let recheck defs = let mono_rewrites = MonoRewrites.mono_rewrite -let monomorphise target opts splits defs = - let defs, env = Type_check.check Type_check.initial_env defs in +let monomorphise target opts splits ast = + let ast, env = Type_check.check Type_check.initial_env ast in let ok_analysis, new_splits, extra_splits = if opts.auto then - let f,r,ex = Analysis.analyse_defs opts.debug_analysis env defs in + let f,r,ex = Analysis.analyse_defs opts.debug_analysis env ast in if f || opts.all_split_errors || opts.continue_anyway then f, r, ex else raise (Reporting.err_general Unknown "Unable to monomorphise program") else true, [], Analysis.ExtraSplits.empty in let splits = new_splits @ (List.map (fun (loc,id) -> (loc,id,None)) splits) in - let ok_extras, defs, extra_splits = add_extra_splits extra_splits defs in + let ok_extras, defs, extra_splits = add_extra_splits extra_splits ast.defs in + let ast = { ast with defs = defs } in let splits = splits @ extra_splits in let () = if ok_extras || opts.all_split_errors || opts.continue_anyway then () else raise (Reporting.err_general Unknown "Unable to monomorphise program") in - let ok_split, defs = split_defs target opts.all_split_errors splits env defs in + let ok_split, ast = split_defs target opts.all_split_errors splits env ast in let () = if (ok_analysis && ok_extras && ok_split) || opts.continue_anyway then () else raise (Reporting.err_general Unknown "Unable to monomorphise program") - in defs + in ast let add_bitvector_casts = BitvectorSizeCasts.add_bitvector_casts let rewrite_atoms_to_singletons target defs = diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 2f262ec3..fed28b99 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -635,7 +635,7 @@ let ocaml_typedef ctx (TD_aux (td_aux, (l, _))) = | TD_bitfield _ -> Reporting.unreachable l __POS__ "Bitfield should be re-written" -let get_externs (Defs defs) = +let get_externs defs = let extern_id (VS_aux (VS_val_spec (typschm, id, exts, _), _)) = match Ast_util.extern_assoc "ocaml" exts with | None -> [] @@ -661,7 +661,7 @@ let ocaml_def ctx def = match def with | DEF_val lb -> nf_group (string "let" ^^ space ^^ ocaml_letbind ctx lb) ^^ ocaml_def_end | _ -> empty -let val_spec_typs (Defs defs) = +let val_spec_typs defs = let typs = ref (Bindings.empty) in let val_spec_typ (VS_aux (vs_aux, _)) = match vs_aux with @@ -683,7 +683,7 @@ let val_spec_typs (Defs defs) = size of the vector is. *) -let orig_types_for_ocaml_generator (Defs defs) = +let orig_types_for_ocaml_generator defs = Util.map_filter (function | DEF_type td -> Some td | _ -> None) defs @@ -926,10 +926,10 @@ let ocaml_pp_generators ctx defs orig_types required = separate_map hardline make_rand_gen (IdSet.elements required) ^^ hardline ^^ rand_record_pp -let ocaml_defs (Defs defs) generator_info = - let ctx = { register_inits = get_initialize_registers defs; - externs = get_externs (Defs defs); - val_specs = val_spec_typs (Defs defs) +let ocaml_ast ast generator_info = + let ctx = { register_inits = get_initialize_registers ast.defs; + externs = get_externs ast.defs; + val_specs = val_spec_typs ast.defs } in let empty_reg_init = @@ -942,11 +942,11 @@ let ocaml_defs (Defs defs) generator_info = let gen_pp = match generator_info with | None -> empty - | Some (types, req) -> ocaml_pp_generators ctx defs types (List.map mk_id req) + | Some (types, req) -> ocaml_pp_generators ctx ast.defs types (List.map mk_id req) in (string "open Sail_lib;;" ^^ hardline) ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end) - ^^ concat (List.map (ocaml_def ctx) defs) + ^^ concat (List.map (ocaml_def ctx) ast.defs) ^^ empty_reg_init ^^ gen_pp @@ -969,8 +969,8 @@ let ocaml_main spec sail_dir = " try zmain () with exn -> (prerr_endline(\"Exiting due to uncaught exception:\\n\" ^ Printexc.to_string exn); exit 1)\n";]) |> String.concat "\n" -let ocaml_pp_defs f defs generator_types = - ToChannel.pretty 1. 80 f (ocaml_defs defs generator_types) +let ocaml_pp_ast f ast generator_types = + ToChannel.pretty 1. 80 f (ocaml_ast ast generator_types) let system_checked str = @@ -986,7 +986,7 @@ let system_checked str = prerr_endline (str ^ " was stopped by a signal"); exit 1 -let ocaml_compile spec defs generator_types = +let ocaml_compile spec ast generator_types = let sail_dir = try Sys.getenv "SAIL_DIR" with | Not_found -> @@ -1007,9 +1007,9 @@ let ocaml_compile spec defs generator_types = let out_chan = open_out (spec ^ ".ml") in if !opt_ocaml_coverage then ignore(Unix.system ("cp -r " ^ sail_dir ^ "/lib/myocamlbuild_coverage.ml myocamlbuild.ml")); - ocaml_pp_defs out_chan defs generator_types; + ocaml_pp_ast out_chan ast generator_types; close_out out_chan; - if IdSet.mem (mk_id "main") (val_spec_ids defs) + if IdSet.mem (mk_id "main") (val_spec_ids ast.defs) then begin print_endline "Generating main"; diff --git a/src/optimize.ml b/src/optimize.ml index 8c456a1b..fccf0f3a 100644 --- a/src/optimize.ml +++ b/src/optimize.ml @@ -65,7 +65,7 @@ let split_at_function id defs = | Some (pre_defs, def, post_defs) -> Some (List.rev pre_defs, def, post_defs) -let recheck (Defs defs) = +let recheck ({ defs; _} as ast) = let defs = Type_check.check_with_envs Type_check.initial_env defs in let rec find_optimizations = function @@ -112,4 +112,4 @@ let recheck (Defs defs) = | [] -> [] in - Defs (find_optimizations defs) + { ast with defs = find_optimizations defs } diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index cc5cd4da..7f28fac8 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -3232,7 +3232,6 @@ let doc_val pat exp = group (separate space [string "Hint Unfold"; idpp; colon; string "sail."]) ^^ hardline let rec doc_def unimplemented generic_eq_types def = - (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with | DEF_spec v_spec -> doc_val_spec unimplemented v_spec | DEF_fixity _ -> empty @@ -3281,7 +3280,7 @@ let find_unimplemented defs = in List.fold_left adjust_def IdSet.empty defs -let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line suppress_MR_M = +let pp_ast_coq (types_file,types_modules) (defs_file,defs_modules) { defs; _ } top_line suppress_MR_M = try (* let regtypes = find_regtypes d in *) let state_ids = diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index dff937a7..e40de7aa 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1535,7 +1535,6 @@ let doc_regtype_fields (tname, (n1, n2, fields)) = separate_map hardline doc_field fields let rec doc_def_lem type_env def = - (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with | DEF_spec v_spec -> doc_spec_lem type_env v_spec | DEF_fixity _ -> empty @@ -1561,7 +1560,7 @@ let find_exc_typ defs = | _ -> false in if List.exists is_exc_typ_def defs then "exception" else "unit" -let pp_ast_lem (types_file,types_modules) (defs_file,defs_modules) type_env (Defs defs) top_line = +let pp_ast_lem (types_file,types_modules) (defs_file,defs_modules) type_env { defs; _ } top_line = (* let regtypes = find_regtypes d in *) let state_ids = State.generate_regstate_defs !opt_mwords defs diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index c306d0b6..ad4d5a75 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -769,10 +769,10 @@ let rec doc_def def = group (match def with separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] ) ^^ hardline -let doc_defs (Defs(defs)) = +let doc_ast { defs } = separate_map hardline doc_def (List.filter doc_filter defs) -let reformat dir (Defs defs) = +let reformat dir { defs } = let file_stack = ref [] in let pop () = match !file_stack with @@ -824,7 +824,7 @@ let reformat dir (Defs defs) = List.iter format_def defs; opt_insert_braces := false -let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d) +let pp_ast f d = ToChannel.pretty 1. 80 f (doc_ast d) let pretty_sail f doc = ToChannel.pretty 1. 120 f doc diff --git a/src/process_file.ml b/src/process_file.ml index 63ea49cc..b121c87c 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -267,7 +267,7 @@ let opt_dno_cast = ref false let check_ast (env : Type_check.Env.t) (ast : unit ast) : Type_check.tannot ast * Type_check.Env.t = let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in let ast, env = Type_error.check env ast in - let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in + let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_ast stdout ast else () in let () = if !opt_just_check then exit 0 else () in (ast, env) @@ -277,7 +277,7 @@ let load_files ?check:(check=false) options type_envs files = let t = Profile.start () in let ast = Parse_ast.Defs (List.map (fun f -> (f, parse_file f |> snd |> preprocess options)) files) in let ast = Initial_check.process_ast ~generate:(not check) ast in - let () = if !opt_ddump_initial_ast then Pretty_print_sail.pp_defs stdout ast else () in + let () = if !opt_ddump_initial_ast then Pretty_print_sail.pp_ast stdout ast else () in begin match !opt_reformat with | Some dir -> @@ -330,7 +330,7 @@ let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f -let output_lem filename libs type_env defs = +let output_lem filename libs type_env ast = let generated_line = generated_line filename in (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = (filename ^ "_types") in @@ -358,7 +358,7 @@ let output_lem filename libs type_env defs = string (" " ^ String.capitalize_ascii filename); string "begin"; string ""; - State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs; + State.generate_isa_lemmas !Pretty_print_lem.opt_mwords ast.defs; string ""; string "end" ] ^^ hardline @@ -370,7 +370,7 @@ let output_lem filename libs type_env defs = (Pretty_print.pp_ast_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) - type_env defs generated_line); + type_env ast generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; let ((ol,_,_,_) as ext_ol) = @@ -378,7 +378,7 @@ let output_lem filename libs type_env defs = print ol isa_lemmas; close_output_with_check ext_ol -let output_coq opt_dir filename alt_modules alt_modules2 libs defs = +let output_coq opt_dir filename alt_modules alt_modules2 libs ast = let generated_line = generated_line filename in let types_module = (filename ^ "_types") in let base_imports_default = ["Sail.Base"; "Sail.Real"] in @@ -396,10 +396,10 @@ let output_coq opt_dir filename alt_modules alt_modules2 libs defs = open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in let ((o,_,_,_) as ext_o) = open_output_with_check_unformatted opt_dir (filename ^ ".v") in - (Pretty_print_coq.pp_defs_coq + (Pretty_print_coq.pp_ast_coq (ot, base_imports) (o, base_imports @ (types_module :: libs) @ alt_modules2) - defs generated_line) + ast generated_line) (alt_modules2 <> []); (* suppress MR and M defns if alt_modules2 present*) close_output_with_check ext_ot; close_output_with_check ext_o @@ -408,45 +408,44 @@ let rec iterate (f : int -> unit) (n : int) : unit = if n = 0 then () else (f n; iterate f (n - 1)) -let output1 libpath out_arg filename type_env defs = +let output1 libpath out_arg filename type_env ast = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem f' libs type_env defs + output_lem f' libs type_env ast | Coq_out libs -> - output_coq !opt_coq_output_dir f' !opt_alt_modules_coq !opt_alt_modules2_coq libs defs + output_coq !opt_coq_output_dir f' !opt_alt_modules_coq !opt_alt_modules2_coq libs ast let output libpath out_arg files = List.iter - (fun (f, type_env, defs) -> - output1 libpath out_arg f type_env defs) + (fun (f, type_env, ast) -> + output1 libpath out_arg f type_env ast) files -let rewrite_step n total (defs, env) (name, rewriter) = +let rewrite_step n total (ast, env) (name, rewriter) = let t = Profile.start () in - let defs, env = rewriter env defs in + let ast, env = rewriter env ast in Profile.finish ("rewrite " ^ name) t; let _ = match !(opt_ddump_rewrite_ast) with | Some (f, i) -> begin let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in - (* output "" Lem_ast_out [filename, defs]; *) let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted None filename in - Pretty_print_sail.pp_defs ot defs; + Pretty_print_sail.pp_ast ot ast; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) end | _ -> () in Util.progress "Rewrite " name n total; - defs, env + ast, env -let rewrite env rewriters defs = +let rewrite env rewriters ast = let total = List.length rewriters in - try snd (List.fold_left (fun (n, defsenv) rw -> n + 1, rewrite_step n total defsenv rw) (1, (defs, env)) rewriters) with + try snd (List.fold_left (fun (n, astenv) rw -> n + 1, rewrite_step n total astenv rw) (1, (ast, env)) rewriters) with | Type_check.Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) -let rewrite_ast_initial env = rewrite env [("initial", fun env defs -> Rewriter.rewrite_ast defs, env)] +let rewrite_ast_initial env = rewrite env [("initial", fun env ast -> Rewriter.rewrite_ast ast, env)] let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_ast_target tgt) diff --git a/src/property.ml b/src/property.ml index 854677c8..6a648bd8 100644 --- a/src/property.ml +++ b/src/property.ml @@ -53,7 +53,7 @@ open Ast_defs open Ast_util open Parser_combinators -let find_properties (Defs defs) = +let find_properties { defs; _ } = let rec find_prop acc = function | DEF_pragma (("property" | "counterexample") as prop_type, command, l) :: defs -> begin match Util.find_next (function DEF_spec _ -> true | _ -> false) defs with @@ -69,7 +69,7 @@ let find_properties (Defs defs) = |> List.map (fun ((_, _, _, vs) as prop) -> (id_of_val_spec vs, prop)) |> List.fold_left (fun m (id, prop) -> Bindings.add id prop m) Bindings.empty -let add_property_guards props (Defs defs) = +let add_property_guards props ast = let open Type_check in let rec add_property_guards' acc = function | (DEF_fundef (FD_aux (FD_function (r_opt, t_opt, e_opt, funcls), fd_aux) as fdef) as def) :: defs -> @@ -118,7 +118,7 @@ let add_property_guards props (Defs defs) = | def :: defs -> add_property_guards' (def :: acc) defs | [] -> List.rev acc in - Defs (add_property_guards' [] defs) + { ast with defs = add_property_guards' [] ast.defs } let rewrite defs = add_property_guards (find_properties defs) defs diff --git a/src/rewriter.ml b/src/rewriter.ml index 49689b96..c5d829f6 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -386,14 +386,14 @@ let rewrite_def rewriters d = match d with | DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp) | DEF_loop_measures (id,_) -> raise (Reporting.err_unreachable (id_loc id) __POS__ "DEF_loop_measures survived to rewriter") -let rewrite_ast_base rewriters (Defs defs) = +let rewrite_ast_base rewriters ast = let rec rewrite ds = match ds with | [] -> [] | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in - Defs (rewrite defs) + { ast with defs = rewrite ast.defs } -let rewrite_ast_base_progress prefix rewriters (Defs defs) = - let total = List.length defs in +let rewrite_ast_base_progress prefix rewriters ast = + let total = List.length ast.defs in let rec rewrite n = function | [] -> [] | d :: ds -> @@ -401,7 +401,7 @@ let rewrite_ast_base_progress prefix rewriters (Defs defs) = let d = rewriters.rewrite_def rewriters d in d :: rewrite (n + 1) ds in - Defs (rewrite 1 defs) + { ast with defs = rewrite 1 ast.defs } let rec takedrop n xs = match n, xs with @@ -411,56 +411,6 @@ let rec takedrop n xs = let ys, xs = takedrop (n - 1) xs in x :: ys, xs -let rewrite_ast_base_parallel j rewriters (Defs defs) = - let module IntMap = Map.Make(struct type t = int let compare = compare end) in - let total = List.length defs in - let defs = ref defs in - - (* We have a list of child processes in pids, and a mapping from pid - to result location in results. *) - let pids = ref [] in - let results = ref IntMap.empty in - for i = 1 to j do - let work = if i = 1 then total / j + total mod j else total / j in - let work, rest = takedrop work !defs in - (* Create a temporary file where the child process will return it's result *) - let result = Filename.temp_file "sail" ".rewrite" in - let pid = Unix.fork () in - begin - if pid = 0 then - let Defs work = rewrite_ast_base rewriters (Defs work) in - let out_chan = open_out result in - Marshal.to_channel out_chan work [Marshal.Closures]; - close_out out_chan; - exit 0 - else - (pids := pid :: !pids; results := IntMap.add pid result !results) - end; - defs := rest - done; - (* Make sure we haven't left any definitions behind! *) - assert(List.length !defs = 0); - - let rewritten = ref [] in - - (* Now we wait for all our child processes *) - while List.compare_length_with !pids 0 > 0 do - let child = List.hd !pids in - pids := List.tl !pids; - let _, status = Unix.waitpid [] child in - match status with - | WEXITED 0 -> - let result = IntMap.find child !results in - let in_chan = open_in result in - rewritten := Marshal.from_channel in_chan :: !rewritten; - close_in in_chan; - Sys.remove result - | _ -> - prerr_endline "Child process exited abnormally in parallel rewrite"; - exit 1 - done; - Defs (List.concat !rewritten) - let rewriters_base = {rewrite_exp = rewrite_exp; rewrite_pat = rewrite_pat; @@ -470,7 +420,7 @@ let rewriters_base = rewrite_def = rewrite_def; rewrite_ast = rewrite_ast_base} -let rewrite_ast (Defs defs) = rewrite_ast_base rewriters_base (Defs defs) +let rewrite_ast ast = rewrite_ast_base rewriters_base ast type ('a,'pat,'pat_aux) pat_alg = { p_lit : lit -> 'pat_aux diff --git a/src/rewriter.mli b/src/rewriter.mli index fd874ba0..ab071318 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -73,8 +73,6 @@ val rewrite_ast : tannot ast -> tannot ast val rewrite_ast_base : tannot rewriters -> tannot ast -> tannot ast -val rewrite_ast_base_parallel : int -> tannot rewriters -> tannot ast -> tannot ast - (** Same as rewrite_defs_base but display a progress bar when verbosity >= 1 *) val rewrite_ast_base_progress : string -> tannot rewriters -> tannot ast -> tannot ast diff --git a/src/rewrites.ml b/src/rewrites.ml index ff909a35..57b71ec7 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -595,7 +595,7 @@ let rewrite_fun_remove_vector_concat_pat (FCL_aux (FCL_Funcl (id,pexp'),(l,annot))) in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) -let rewrite_ast_remove_vector_concat env (Defs defs) = +let rewrite_ast_remove_vector_concat env ast = let rewriters = {rewrite_exp = rewrite_exp_remove_vector_concat_pat; rewrite_pat = rewrite_pat; @@ -612,7 +612,7 @@ let rewrite_ast_remove_vector_concat env (Defs defs) = let defvals = List.map (fun lb -> DEF_val lb) letbinds in [DEF_val (LB_aux (LB_val (pat,exp),a))] @ defvals | d -> [d] in - Defs (List.flatten (List.map rewrite_def defs)) + { ast with defs = List.flatten (List.map rewrite_def ast.defs) } (* A few helper functions for rewriting guarded pattern clauses. Used both by the rewriting of P_when and separately by the rewriting of @@ -1188,7 +1188,7 @@ let rewrite_fun_remove_bitvector_pat | _ -> funcls in FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot)) -let rewrite_ast_remove_bitvector_pats env (Defs defs) = +let rewrite_ast_remove_bitvector_pats env ast = let rewriters = {rewrite_exp = rewrite_exp_remove_bitvector_pat; rewrite_pat = rewrite_pat; @@ -1207,8 +1207,8 @@ let rewrite_ast_remove_bitvector_pats env (Defs defs) = | d -> [d] in (* FIXME See above in rewrite_sizeof *) (* fst (check initial_env ( *) - Defs (List.flatten (List.map rewrite_def defs)) - (* )) *) + { ast with defs = List.flatten (List.map rewrite_def ast.defs) } + (* )) *) (* Rewrite literal number patterns to guarded patterns Those numeral patterns are not handled very well by Lem (or Isabelle) @@ -1447,9 +1447,9 @@ let rewrite_ast_exp_lift_assign env defs = rewrite_ast_base becomes write_reg_ref (vector_access (GPR, i)) exp *) -let rewrite_register_ref_writes (Defs defs) = - let (Defs write_reg_spec) = fst (Type_error.check initial_env (Defs (List.map gen_vs - [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")]))) in +let rewrite_register_ref_writes ast = + let write_reg_spec = fst (Type_error.check_defs initial_env (List.map gen_vs + [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")])) in let lexp_ref_exp (LEXP_aux (_, annot) as lexp) = try let exp = infer_exp (env_of_annot annot) (strip_exp (lexp_to_exp lexp)) in @@ -1468,7 +1468,7 @@ let rewrite_register_ref_writes (Defs defs) = let rec rewrite ds = match ds with | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) | [] -> [] in - Defs (rewrite (write_reg_spec @ defs)) + { ast with defs = rewrite (write_reg_spec @ ast.defs) } (* Remove redundant return statements, and translate remaining ones into an @@ -1478,7 +1478,7 @@ let rewrite_register_ref_writes (Defs defs) = TODO: Maybe separate generic removal of redundant returns, and Lem-specific rewriting of early returns *) -let rewrite_ast_early_return env (Defs defs) = +let rewrite_ast_early_return env ast = let is_unit (E_aux (exp, _)) = match exp with | E_lit (L_aux (L_unit, _)) -> true | _ -> false in @@ -1646,12 +1646,12 @@ let rewrite_ast_early_return env (Defs defs) = FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, List.map (rewrite_funcl_early_return rewriters) funcls), a) in - let (Defs early_ret_spec) = fst (Type_error.check initial_env (Defs [gen_vs - ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in + let early_ret_spec = fst (Type_error.check_defs initial_env [gen_vs + ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")]) in rewrite_ast_base { rewriters_base with rewrite_fun = rewrite_fun_early_return } - (Defs (early_ret_spec @ defs)) + { ast with defs = early_ret_spec @ ast.defs } let swaptyp typ (l,tannot) = match destruct_tannot tannot with | Some (env, typ', eff) -> (l, mk_tannot env typ eff) @@ -1702,7 +1702,7 @@ let pat_var (P_aux (paux, a)) = Instr : {'r, 'r in {32, 64}. (int('x), bits('r))} } *) -let rewrite_split_fun_ctor_pats fun_name env (Defs defs) = +let rewrite_split_fun_ctor_pats fun_name env ast = let rewrite_fundef typquant (FD_aux (FD_function (r_o, t_o, e_o, clauses), ((l, _) as fdannot))) = let rec_clauses, clauses = List.partition is_funcl_rec clauses in let clauses, aux_funs = @@ -1800,18 +1800,18 @@ let rewrite_split_fun_ctor_pats fun_name env (Defs defs) = let typquant = List.fold_left (fun tq def -> match def with | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tq, _), _), id, _, _), _)) when string_of_id id = fun_name -> tq - | _ -> tq) (mk_typquant []) defs + | _ -> tq) (mk_typquant []) ast.defs in let defs = List.fold_right (fun def defs -> match def with | DEF_fundef fundef when string_of_id (id_of_fundef fundef) = fun_name -> rewrite_fundef typquant fundef @ defs - | _ -> def :: defs) defs [] + | _ -> def :: defs) ast.defs [] in - Defs defs + { ast with defs = defs } (* Propagate effects of functions, if effect checking and propagation have not been performed already by the type checker. *) -let rewrite_fix_val_specs env (Defs defs) = +let rewrite_fix_val_specs env ast = let find_vs env val_specs id = try Bindings.find id val_specs with | Not_found -> @@ -1940,13 +1940,10 @@ let rewrite_fix_val_specs env (Defs defs) = | def -> def in - let (val_specs, defs) = List.fold_left rewrite_def (Bindings.empty, []) defs in + let (val_specs, defs) = List.fold_left rewrite_def (Bindings.empty, []) ast.defs in let defs = List.map (rewrite_val_specs val_specs) defs in - (* if !Type_check.opt_no_effects - then *) - Defs defs - (* else Defs defs *) + { ast with defs = defs } let rewrite_type_union_typs rw_typ (Tu_aux (Tu_ty_id (typ, id), annot)) = Tu_aux (Tu_ty_id (rw_typ typ, id), annot) @@ -1973,7 +1970,7 @@ let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) = (* Remove overload definitions and cast val specs from the specification because the interpreter doesn't know about them.*) -let rewrite_overload_cast env (Defs defs) = +let rewrite_overload_cast env ast = let remove_cast_vs (VS_aux (vs_aux, annot)) = match vs_aux with | VS_val_spec (typschm, id, ext, _) -> VS_aux (VS_val_spec (typschm, id, ext, false), annot) @@ -1986,8 +1983,8 @@ let rewrite_overload_cast env (Defs defs) = | DEF_overload _ -> true | _ -> false in - let defs = List.map simple_def defs in - Defs (List.filter (fun def -> not (is_overload def)) defs) + let defs = List.map simple_def ast.defs in + { ast with defs = List.filter (fun def -> not (is_overload def)) defs } let rewrite_undefined mwords env = @@ -2029,7 +2026,7 @@ and simple_typ_arg (A_aux (typ_arg_aux, l)) = | _ -> [] (* This pass aims to remove all the Num quantifiers from the specification. *) -let rewrite_simple_types env (Defs defs) = +let rewrite_simple_types env ast = let is_simple = function | QI_aux (QI_id kopt, annot) as qi when is_typ_kopt kopt || is_order_kopt kopt -> true | _ -> false @@ -2076,8 +2073,8 @@ let rewrite_simple_types env (Defs defs) = let simple_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp simple_exp); rewrite_pat = (fun _ -> fold_pat simple_pat) } in - let defs = Defs (List.map simple_def defs) in - rewrite_ast_base simple_defs defs + let ast = { ast with defs = List.map simple_def ast.defs } in + rewrite_ast_base simple_defs ast let rewrite_vector_concat_assignments env defs = let assign_tuple e_aux annot = @@ -2514,7 +2511,6 @@ let rewrite_ast_letbind_effects env = FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),fdannot) in let rewrite_def rewriters def = - (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with | DEF_val (LB_aux (lb, annot)) -> let rewrap lb = DEF_val (LB_aux (lb, annot)) in @@ -2862,7 +2858,7 @@ let construct_toplevel_string_append_func env f_id pat = let new_fun_def, env = Type_check.check_fundef env new_fun_def in List.flatten [new_val_spec; new_fun_def] -let rewrite_ast_toplevel_string_append env (Defs defs) = +let rewrite_ast_toplevel_string_append env ast = let new_defs = ref ([] : tannot def list) in let rec rewrite_pexp (Pat_aux (pexp_aux, pexp_annot) as pexp) = (* merge cases of Pat_exp and Pat_when *) @@ -2896,7 +2892,7 @@ let rewrite_ast_toplevel_string_append env (Defs defs) = let rewritten = rewrite_def { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } def in !new_defs @ [rewritten] in - Defs (List.map rewrite defs |> List.flatten) + { ast with defs = List.map rewrite ast.defs |> List.flatten } let rec rewrite_ast_pat_string_append env = @@ -3352,8 +3348,8 @@ let rewrite_ast_pat_lits rewrite_lit env ast = in let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in - let Defs defs = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in - Defs (List.map rewrite_def defs) + let ast = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in + { ast with defs = List.map rewrite_def ast.defs } (* Now all expressions have no blocks anymore, any term is a sequence of let-expressions, @@ -3821,13 +3817,13 @@ let rewrite_ast_remove_superfluous_returns env = } -let rewrite_ast_remove_e_assign env (Defs defs) = - let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs +let rewrite_ast_remove_e_assign env ast = + let loop_specs = fst (Type_error.check_defs initial_env (List.map gen_vs [("foreach#", "forall ('vars_in 'vars_out : Type). (int, int, int, bool, 'vars_in, 'vars_out) -> 'vars_out"); ("while#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out"); ("until#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out"); ("while#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out"); - ("until#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out")]))) in + ("until#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out")])) in let rewrite_exp _ e = replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in rewrite_ast_base @@ -3838,9 +3834,9 @@ let rewrite_ast_remove_e_assign env (Defs defs) = ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def ; rewrite_ast = rewrite_ast_base - } (Defs (loop_specs @ defs)) + } { ast with defs = loop_specs @ ast.defs } -let merge_funcls env (Defs defs) = +let merge_funcls env ast = let merge_function (FD_aux (FD_function (r,t,e,fcls),ann) as f) = match fcls with | [] | [_] -> f @@ -3858,7 +3854,7 @@ let merge_funcls env (Defs defs) = | DEF_fundef f -> DEF_fundef (merge_function f) | DEF_internal_mutrec fs -> DEF_internal_mutrec (List.map merge_function fs) | d -> d - in Defs (List.map merge_in_def defs) + in { ast with defs = List.map merge_in_def ast.defs } let rec exp_of_mpat ((MP_aux (mpat, (l,annot))) as mp_aux) = @@ -3899,7 +3895,7 @@ and pat_of_mpat (MP_aux (mpat, annot)) = | MP_typ (mpat, typ) -> P_aux (P_typ (typ, pat_of_mpat mpat), annot) | MP_as (mpat, id) -> P_aux (P_as (pat_of_mpat mpat, id), annot) -let rewrite_ast_realise_mappings _ (Defs defs) = +let rewrite_ast_realise_mappings _ ast = let realise_mpexps forwards mpexp1 mpexp2 = let mpexp_pat, mpexp_exp = if forwards then mpexp1, mpexp2 @@ -4112,7 +4108,7 @@ let rewrite_ast_realise_mappings _ (Defs defs) = [] end in - let has_def id = IdSet.mem id (ids_of_ast (Defs defs)) in + let has_def id = IdSet.mem id (ids_of_ast ast) in (if has_def forwards_id then [] else forwards_fun) @ (if has_def backwards_id then [] else backwards_fun) @@ -4126,7 +4122,7 @@ let rewrite_ast_realise_mappings _ (Defs defs) = | DEF_mapdef mdef -> realise_mapdef mdef | d -> [d] in - Defs (List.map rewrite_def defs |> List.flatten) + { ast with defs = List.map rewrite_def ast.defs |> List.flatten } (* Rewrite to make all pattern matches in Coq output exhaustive. Assumes that guards, vector patterns, etc have been rewritten already, @@ -4500,7 +4496,7 @@ end new functions that appear to be recursive but are not. This checks to see if the flag can be turned off. Doesn't handle mutual recursion for now. *) -let minimise_recursive_functions env (Defs defs) = +let minimise_recursive_functions env ast = let funcl_is_rec (FCL_aux (FCL_Funcl (id,pexp),_)) = fold_pexp { (pure_exp_alg false (||)) with @@ -4521,10 +4517,10 @@ let minimise_recursive_functions env (Defs defs) = let rewrite_def = function | DEF_fundef fd -> DEF_fundef (rewrite_function fd) | d -> d - in Defs (List.map rewrite_def defs) + in { ast with defs = List.map rewrite_def ast.defs } (* Move recursive function termination measures into the function definitions. *) -let move_termination_measures env (Defs defs) = +let move_termination_measures env ast = let scan_for id defs = let rec aux = function | [] -> None @@ -4551,11 +4547,11 @@ let move_termination_measures env (Defs defs) = end | (DEF_measure _)::t -> aux acc t | h::t -> aux (h::acc) t - in Defs (aux [] defs) + in { ast with defs = aux [] ast.defs } (* Make recursive functions with a measure use the measure as an explicit recursion limit, enforced by an assertion. *) -let rewrite_explicit_measure env (Defs defs) = +let rewrite_explicit_measure env ast = let scan_function measures = function | FD_aux (FD_function (Rec_aux (Rec_measure (mpat,mexp),rl),topt,effopt, FCL_aux (FCL_Funcl (id,_),_)::_),ann) -> @@ -4567,7 +4563,7 @@ let rewrite_explicit_measure env (Defs defs) = | DEF_internal_mutrec fds -> List.fold_left scan_function measures fds | _ -> measures in - let measures = List.fold_left scan_def Bindings.empty defs in + let measures = List.fold_left scan_def Bindings.empty ast.defs in let add_escape eff = union_effects eff (mk_effect [BE_escape]) in @@ -4699,7 +4695,7 @@ let rewrite_explicit_measure env (Defs defs) = (DEF_internal_mutrec fds)::(List.map (fun f -> DEF_fundef f) extras) | d -> [d] in - Defs (List.flatten (List.map rewrite_def defs)) + { ast with defs = List.flatten (List.map rewrite_def ast.defs) } (* Add a dummy assert to loops for backends that require loops to be able to fail. Note that the Coq backend will spot the assert and omit it. *) @@ -4735,14 +4731,14 @@ let recheck_defs_without_effects env defs = (* In realise_mappings we may have duplicated a user-supplied val spec, which causes problems for some targets. Keep the first one, except use the externs from the last one, as subsequent redefinitions override earlier ones. *) -let remove_duplicate_valspecs env (Defs defs) = +let remove_duplicate_valspecs env ast = let last_externs = List.fold_left (fun last_externs def -> match def with | DEF_spec (VS_aux (VS_val_spec (_, id, externs, _), _)) -> Bindings.add id externs last_externs - | _ -> last_externs) Bindings.empty defs + | _ -> last_externs) Bindings.empty ast.defs in let (_, rev_defs) = List.fold_left @@ -4754,14 +4750,14 @@ let remove_duplicate_valspecs env (Defs defs) = let externs = Bindings.find id last_externs in let vs = VS_aux (VS_val_spec (typschm, id, externs, cast), l) in (IdSet.add id set, (DEF_spec vs)::defs) - | _ -> (set, def::defs)) (IdSet.empty, []) defs - in Defs (List.rev rev_defs) + | _ -> (set, def::defs)) (IdSet.empty, []) ast.defs + in { ast with defs = List.rev rev_defs } (* Move loop termination measures into loop AST nodes. This is used before type checking so that we avoid the complexity of type checking separate measures. *) -let rec move_loop_measures (Defs defs) = +let rec move_loop_measures ast = let loop_measures = List.fold_left (fun m d -> @@ -4773,7 +4769,7 @@ let rec move_loop_measures (Defs defs) = | None -> measures | Some m -> m @ measures) m - | _ -> m) Bindings.empty defs + | _ -> m) Bindings.empty ast.defs in let do_exp exp_rec measures (E_aux (e,ann) as exp) = match e, measures with @@ -4799,7 +4795,7 @@ let rec move_loop_measures (Defs defs) = let m,rfcls = List.fold_left do_funcl (m,[]) fcls in m, (DEF_fundef (FD_aux (FD_function (r,t,e,List.rev rfcls),ann)))::acc | _ -> m, d::acc) - (loop_measures,[]) defs + (loop_measures,[]) ast.defs in let () = Bindings.iter (fun id -> function | [] -> () @@ -4807,11 +4803,11 @@ let rec move_loop_measures (Defs defs) = Reporting.print_err (id_loc id) "Warning" ("unused loop measure for function " ^ string_of_id id)) unused - in Defs (List.rev rev_defs) + in { ast with defs = List.rev rev_defs } -let rewrite_toplevel_consts target type_env (Defs defs) = - let istate = Constant_fold.initial_state (Defs defs) type_env in +let rewrite_toplevel_consts target type_env ast = + let istate = Constant_fold.initial_state ast type_env in let subst consts exp = let open Rewriter in let used_ids = fold_exp { (pure_exp_alg IdSet.empty IdSet.union) with e_id = IdSet.singleton } exp in @@ -4837,8 +4833,8 @@ let rewrite_toplevel_consts target type_env (Defs defs) = end | def -> (def :: revdefs, consts) in - let (revdefs, _) = List.fold_left rewrite_def ([], Bindings.empty) defs in - Defs (List.rev revdefs) + let (revdefs, _) = List.fold_left rewrite_def ([], Bindings.empty) ast.defs in + { ast with defs = List.rev revdefs } (* Hex literals are always a multiple of 4 bits long. If one of a different size is needed, users may truncate them down. This can be bad for isla because the original may be too long for the concrete bitvector diff --git a/src/sail.ml b/src/sail.ml index 0e9b8e27..38d4c2e8 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -457,13 +457,13 @@ let target name out_name ast type_envs = | None -> () | Some "sail" -> - Pretty_print_sail.pp_defs stdout ast + Pretty_print_sail.pp_ast stdout ast | Some "ocaml" -> let ocaml_generator_info = match !opt_ocaml_generators with | [] -> None - | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast, !opt_ocaml_generators) + | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast.defs, !opt_ocaml_generators) in let out = match !opt_file_out with None -> "out" | Some s -> s in Ocaml_backend.ocaml_compile out ast ocaml_generator_info diff --git a/src/scattered.ml b/src/scattered.ml index b8979f31..4b89a766 100644 --- a/src/scattered.ml +++ b/src/scattered.ml @@ -139,4 +139,4 @@ let rec descatter' funcls mapcls = function | def :: defs -> def :: descatter' funcls mapcls defs | [] -> [] -let descatter (Defs defs) = Defs (descatter' Bindings.empty Bindings.empty defs) +let descatter ast = { ast with defs = descatter' Bindings.empty Bindings.empty ast.defs } diff --git a/src/slice.ml b/src/slice.ml index 7611a54c..bdd0b19e 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -300,16 +300,18 @@ let add_def_to_graph graph def = end; !graph -let rec graph_of_ast (Defs defs) = +let rec graph_of_defs defs = let module G = Graph.Make(Node) in match defs with | def :: defs -> - let g = graph_of_ast (Defs defs) in + let g = graph_of_defs defs in add_def_to_graph g def | [] -> G.empty +let graph_of_ast ast = graph_of_defs ast.defs + let id_of_typedef (TD_aux (aux, _)) = match aux with | TD_abbrev (id, _, _) -> id @@ -324,8 +326,7 @@ let id_of_reg_dec (DEC_aux (aux, _)) = | DEC_config (id, _, _) -> id | _ -> assert false - -let filter_ast cuts g (Defs defs) = +let filter_ast cuts g ast = let rec filter_ast' g = let module NS = Set.Make(Node) in let module NM = Map.Make(Node) in @@ -358,7 +359,7 @@ let filter_ast cuts g (Defs defs) = | [] -> [] in - Defs (filter_ast' g defs) + { ast with defs = filter_ast' g ast.defs } let dot_of_ast out_chan ast = let module G = Graph.Make(Node) in diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index bb30e971..2c40b3ed 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -512,8 +512,8 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should be rewritten before now" -let group_defs consider_scatter_as_one (Defs defs) = - List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs +let group_defs consider_scatter_as_one ast = + List.map (fun d -> (fv_of_def false consider_scatter_as_one ast.defs d,d)) ast.defs (* @@ -591,11 +591,11 @@ let def_of_component graph defset comp = (* We could merge other stuff, in particular overloads, but don't need to just now *) | defs -> defs -let top_sort_defs (Defs defs) = +let top_sort_defs ast = let prelude, original_order, defset, graph = - List.fold_left add_def_to_graph ([], [], Namemap.empty, Namemap.empty) defs in + List.fold_left add_def_to_graph ([], [], Namemap.empty, Namemap.empty) ast.defs in let components = NameGraph.scc ~original_order:original_order graph in - Defs (prelude @ List.concat (List.map (def_of_component graph defset) components)) + { ast with defs = prelude @ List.concat (List.map (def_of_component graph defset) components) } (* Functions for finding the set of variables assigned to. Used in constant propagation diff --git a/src/specialize.ml b/src/specialize.ml index 3634b7bc..bbf74f46 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -117,15 +117,15 @@ let fix_instantiation spec instantiation = for some set of kinded-identifiers, specified by the is_kopt predicate. For example, polymorphic_functions is_int_kopt will return all Int-polymorphic functions. *) -let rec polymorphic_functions ctx (Defs defs) = +let rec polymorphic_functions ctx defs = match defs with | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, externs, _), _)) :: defs -> let is_polymorphic = List.exists ctx.is_polymorphic (quant_kopts typq) in if is_polymorphic && not (ctx.extern_filter externs) then - IdSet.add id (polymorphic_functions ctx (Defs defs)) + IdSet.add id (polymorphic_functions ctx defs) else - polymorphic_functions ctx (Defs defs) - | _ :: defs -> polymorphic_functions ctx (Defs defs) + polymorphic_functions ctx defs + | _ :: defs -> polymorphic_functions ctx defs | [] -> IdSet.empty (* When we specialize a function, we need to generate new name. To do @@ -209,11 +209,11 @@ let id_of_instantiation id instantiation = let str = string_of_instantiation instantiation in prepend_id (str ^ "#") id -let rec variant_generic_typ id (Defs defs) = +let rec variant_generic_typ id defs = match defs with | DEF_type (TD_aux (TD_variant (id', typq, _, _), _)) :: _ when Id.compare id id' = 0 -> mk_typ (Typ_app (id', List.map (fun kopt -> mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt))))) (quant_kopts typq))) - | _ :: defs -> variant_generic_typ id (Defs defs) + | _ :: defs -> variant_generic_typ id defs | [] -> failwith ("No variant with id " ^ string_of_id id) (* Returns a list of all the instantiations of a function id in an @@ -238,8 +238,8 @@ let rec instantiations_of spec id ast = | Typ_aux (Typ_app (variant_id, _), _) as typ -> let open Type_check in let instantiation = unify (fst annot) (env_of_annot annot) - (tyvars_of_typ (variant_generic_typ variant_id ast)) - (variant_generic_typ variant_id ast) + (tyvars_of_typ (variant_generic_typ variant_id ast.defs)) + (variant_generic_typ variant_id ast.defs) typ in instantiations := fix_instantiation spec instantiation :: !instantiations; @@ -259,7 +259,7 @@ let rec instantiations_of spec id ast = !instantiations let rec rewrite_polymorphic_calls spec id ast = - let vs_ids = val_spec_ids ast in + let vs_ids = val_spec_ids ast.defs in let rewrite_e_aux = function | E_aux (E_app (id', args), annot) as exp when Id.compare id id' = 0 -> @@ -368,9 +368,9 @@ let instantiate_constraints instantiation ncs = List.map (fun c -> List.fold_left (fun c (v, a) -> constraint_subst v a c) c (KBindings.bindings instantiation)) ncs let specialize_id_valspec spec instantiations id ast = - match split_ast (is_valspec id) ast with + match split_defs (is_valspec id) ast.defs with | None -> Reporting.unreachable (id_loc id) __POS__ ("Valspec " ^ string_of_id id ^ " does not exist!") - | Some (pre_ast, vs, post_ast) -> + | Some (pre_defs, vs, post_defs) -> let typschm, externs, is_cast, annot = match vs with | DEF_spec (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) -> typschm, externs, is_cast, annot | _ -> Reporting.unreachable (id_loc id) __POS__ "val-spec is not actually a val-spec" @@ -416,7 +416,7 @@ let specialize_id_valspec spec instantiations id ast = let specializations = List.map specialize_instance instantiations |> List.concat in - append_ast pre_ast (append_ast (Defs (vs :: specializations)) post_ast) + { ast with defs = pre_defs @ (vs :: specializations) @ post_defs } (* When we specialize a function definition we also need to specialize all the types that appear as annotations within the function @@ -450,9 +450,9 @@ let specialize_annotations instantiation fdef = annot) let specialize_id_fundef instantiations id ast = - match split_ast (is_fundef id) ast with + match split_defs (is_fundef id) ast.defs with | None -> ast - | Some (pre_ast, DEF_fundef fundef, post_ast) -> + | Some (pre_defs, DEF_fundef fundef, post_defs) -> let spec_ids = ref IdSet.empty in let specialize_fundef instantiation = let spec_id = id_of_instantiation id instantiation in @@ -463,10 +463,10 @@ let specialize_id_fundef instantiations id ast = end in let fundefs = List.map specialize_fundef instantiations |> List.concat in - append_ast pre_ast (append_ast (Defs (DEF_fundef fundef :: fundefs)) post_ast) + { ast with defs = pre_defs @ (DEF_fundef fundef :: fundefs) @ post_defs } | Some _ -> assert false (* unreachable *) -let specialize_id_overloads instantiations id (Defs defs) = +let specialize_id_overloads instantiations id ast = let ids = IdSet.of_list (List.map (id_of_instantiation id) instantiations) in let rec rewrite_overloads defs = @@ -478,7 +478,7 @@ let specialize_id_overloads instantiations id (Defs defs) = | [] -> [] in - Defs (rewrite_overloads defs) + { ast with defs = rewrite_overloads ast.defs } (* Once we've specialized a definition, it's original valspec should be unused, unless another polymorphic function called it. We @@ -501,7 +501,7 @@ let add_initial_calls ids = initial_calls := IdSet.union ids !initial_calls let remove_unused_valspecs env ast = let calls = ref !initial_calls in - let vs_ids = val_spec_ids ast in + let vs_ids = val_spec_ids ast.defs in let inspect_exp = function | E_aux (E_app (call, _), _) as exp -> @@ -515,23 +515,23 @@ let remove_unused_valspecs env ast = let unused = IdSet.filter (fun vs_id -> not (IdSet.mem vs_id !calls)) vs_ids in - let rec remove_unused (Defs defs) id = + let rec remove_unused defs id = match defs with | def :: defs when is_fundef id def -> - remove_unused (Defs defs) id + remove_unused defs id | def :: defs when is_valspec id def -> - remove_unused (Defs defs) id + remove_unused defs id | DEF_overload (overload_id, overloads) :: defs -> begin match List.filter (fun id' -> Id.compare id id' <> 0) overloads with - | [] -> remove_unused (Defs defs) id - | overloads -> DEF_overload (overload_id, overloads) :: remove_unused (Defs defs) id + | [] -> remove_unused defs id + | overloads -> DEF_overload (overload_id, overloads) :: remove_unused defs id end - | def :: defs -> def :: remove_unused (Defs defs) id + | def :: defs -> def :: remove_unused defs id | [] -> [] in - List.fold_left (fun ast id -> Defs (remove_unused ast id)) ast (IdSet.elements unused) + List.fold_left (fun ast id -> { ast with defs = remove_unused ast.defs id }) ast (IdSet.elements unused) let specialize_id spec id ast = let instantiations = instantiations_of spec id ast in @@ -543,7 +543,7 @@ let specialize_id spec id ast = ensure that the types they are specialized to appear before the function definitions in the AST. Therefore we pull all the type definitions (and default definitions) to the start of the AST. *) -let reorder_typedefs (Defs defs) = +let reorder_typedefs ast = let tdefs = ref [] in let rec filter_typedefs = function @@ -554,8 +554,8 @@ let reorder_typedefs (Defs defs) = | [] -> [] in - let others = filter_typedefs defs in - Defs (List.rev !tdefs @ others) + let others = filter_typedefs ast.defs in + { ast with defs = List.rev !tdefs @ others } let specialize_ids spec ids ast = let t = Profile.start () in @@ -571,7 +571,7 @@ let specialize_ids spec ids ast = | Some (f, i) -> let filename = f ^ "_spec_" ^ string_of_int i ^ ".sail" in let out_chan = open_out filename in - Pretty_print_sail.pp_defs out_chan ast; + Pretty_print_sail.pp_ast out_chan ast; close_out out_chan; opt_ddump_spec_ast := Some (f, i + 1) | None -> () @@ -593,7 +593,7 @@ let rec specialize_passes n spec env ast = if n = 0 then ast, env else - let ids = polymorphic_functions spec ast in + let ids = polymorphic_functions spec ast.defs in if IdSet.is_empty ids then ast, env else diff --git a/src/specialize.mli b/src/specialize.mli index 0d522189..d2157323 100644 --- a/src/specialize.mli +++ b/src/specialize.mli @@ -73,7 +73,7 @@ val int_specialization_with_externs : specialization argument specifies what X should be - it should be one of: [is_int_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util], or some combination of those. *) -val polymorphic_functions : specialization -> 'a ast -> IdSet.t +val polymorphic_functions : specialization -> 'a def list -> IdSet.t val add_initial_calls : IdSet.t -> unit diff --git a/src/splice.ml b/src/splice.ml index cb3307d9..478469a0 100644 --- a/src/splice.ml +++ b/src/splice.ml @@ -7,7 +7,7 @@ open Ast open Ast_defs open Ast_util -let scan_defs (Defs defs) = +let scan_ast { defs; _ } = let scan (ids, specs) = function | DEF_fundef fd -> IdSet.add (id_of_fundef fd) ids, specs @@ -19,7 +19,7 @@ let scan_defs (Defs defs) = "Definition in splice file isn't a spec or function") in List.fold_left scan (IdSet.empty, Bindings.empty) defs -let filter_old_ast repl_ids repl_specs (Defs defs) = +let filter_old_ast repl_ids repl_specs { defs; _ } = let check (rdefs,spec_found) def = match def with | DEF_fundef fd -> @@ -36,7 +36,7 @@ let filter_old_ast repl_ids repl_specs (Defs defs) = let rdefs, spec_found = List.fold_left check ([],IdSet.empty) defs in (List.rev rdefs, spec_found) -let filter_replacements spec_found (Defs defs) = +let filter_replacements spec_found { defs; _ } = let not_found = function | DEF_spec (VS_aux (VS_val_spec (_,id,_,_),_)) -> not (IdSet.mem id spec_found) | _ -> true @@ -47,9 +47,8 @@ let splice ast file = let repl_ast = Initial_check.process_ast ~generate:false (Parse_ast.Defs [(file, parsed_ast)]) in let repl_ast = Rewrites.move_loop_measures repl_ast in let repl_ast = map_ast_annot (fun (l,_) -> l,Type_check.empty_tannot) repl_ast in - let repl_ids, repl_specs = scan_defs repl_ast in + let repl_ids, repl_specs = scan_ast repl_ast in let defs1, specs_found = filter_old_ast repl_ids repl_specs ast in let defs2 = filter_replacements specs_found repl_ast in - let new_ast = Defs (defs1 @ defs2) in - Type_error.check Type_check.initial_env new_ast + Type_error.check Type_check.initial_env { ast with defs = defs1 @ defs2 } diff --git a/src/state.ml b/src/state.ml index 3491afd3..15475a36 100644 --- a/src/state.ml +++ b/src/state.ml @@ -61,9 +61,9 @@ open Pretty_print_sail let opt_type_grouped_regstate = ref false -let defs_of_string = ast_of_def_string +let defs_of_string str = (ast_of_def_string str).defs -let is_defined defs name = IdSet.mem (mk_id name) (ids_of_ast (Defs defs)) +let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs defs) let has_default_order defs = List.exists (function DEF_default (DT_aux (DT_order _, _)) -> true | _ -> false) defs @@ -122,7 +122,7 @@ let generate_regstate registers = in TD_record (mk_id "regstate", mk_typquant [], fields, false) in - Defs [DEF_type (TD_aux (regstate_def, (Unknown, ())))] + [DEF_type (TD_aux (regstate_def, (Unknown, ())))] let generate_initial_regstate defs = let registers = find_registers defs in @@ -260,7 +260,7 @@ let generate_regval_typ typs = (String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^ " }")] -let add_regval_conv id typ (Defs defs) = +let add_regval_conv id typ defs = let id = string_of_id id in let typ_str = to_string (doc_typ typ) in (* Create a function that converts from regval to the target type. *) @@ -276,8 +276,8 @@ let add_regval_conv id typ (Defs defs) = let to_val = Printf.sprintf "val %s : %s -> register_value" to_name typ_str in let to_function = Printf.sprintf "function %s v = Regval_%s(v)" to_name id in let to_defs = if is_defined defs to_name then [] else [to_val; to_function] in - let cdefs = concat_ast (List.map defs_of_string (from_defs @ to_defs)) in - append_ast (Defs defs) cdefs + let cdefs = List.concat (List.map defs_of_string (from_defs @ to_defs)) in + defs @ cdefs let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with | Typ_app _ when (is_vector_typ typ || is_bitvector_typ typ) && not (mwords && is_bitvector_typ typ) -> @@ -375,7 +375,7 @@ let register_refs_lem mwords registers = (* TODO Generate well-typedness predicate for register states (and events), asserting that all lists representing non-bit-vectors have the right length. *) -let generate_isa_lemmas mwords (Defs defs : tannot ast) = +let generate_isa_lemmas mwords defs = let rec drop_while f = function | x :: xs when f x -> drop_while f xs | xs -> xs @@ -553,12 +553,12 @@ let generate_regstate_defs mwords defs = in let defs = option_typ @ regval_typ @ regstate_typ @ initregstate - |> concat_ast + |> List.concat |> Bindings.fold add_regval_conv regtyps in Initial_check.opt_undefined_gen := gen_undef; defs -let add_regstate_defs mwords env (Defs defs) = - let reg_defs, env = Type_error.check env (generate_regstate_defs mwords defs) in - env, append_ast (Defs defs) reg_defs +let add_regstate_defs mwords env ast = + let reg_defs, env = Type_error.check_defs env (generate_regstate_defs mwords ast.defs) in + env, append_ast_defs ast reg_defs diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml index 11d66ef6..fc5a18bd 100644 --- a/src/toFromInterp_backend.ml +++ b/src/toFromInterp_backend.ml @@ -393,7 +393,7 @@ let tofrominterp_def def = match def with | DEF_type td -> group (frominterp_typedef td ^^ twice hardline ^^ tointerp_typedef td ^^ twice hardline) | _ -> empty -let tofrominterp_defs name (Defs defs) = +let tofrominterp_ast name { defs; _ } = (string "open Sail_lib;;" ^^ hardline) ^^ (string "open Value;;" ^^ hardline) ^^ (if !lem_mode then (string "open Sail2_instr_kinds;;" ^^ hardline) else empty) @@ -405,11 +405,11 @@ let tofrominterp_defs name (Defs defs) = ^^ (if not !mword_mode then (string "include ToFromInterp_lib_bitlist.Make(struct type t = Sail2_values.bitU0 let b0 = Sail2_values.B00 let b1 = Sail2_values.B10 end)" ^^ hardline) else empty) ^^ concat (List.map tofrominterp_def defs) -let tofrominterp_pp_defs name f defs = - ToChannel.pretty 1. 80 f (tofrominterp_defs name defs) +let tofrominterp_pp_ast name f ast = + ToChannel.pretty 1. 80 f (tofrominterp_ast name ast) -let tofrominterp_output maybe_dir name defs = +let tofrominterp_output maybe_dir name ast = let dir = match maybe_dir with Some dir -> dir | None -> "." in let out_chan = open_out (Filename.concat dir (name ^ "_toFromInterp2.ml")) in - tofrominterp_pp_defs name out_chan defs; + tofrominterp_pp_ast name out_chan ast; close_out out_chan diff --git a/src/type_check.ml b/src/type_check.ml index ab860a79..aeb9cf01 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -5350,8 +5350,8 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t = let size = Big_int.to_int size in let eval_index_nexp env nexp = int_of_nexp_opt (nexp_simp (Env.expand_nexp_synonyms env nexp)) in - let (Defs defs), env = - check env (Bitfield.macro (eval_index_nexp env, (typ_error env)) id size order ranges) in + let defs, env = + check_defs env (Bitfield.macro (eval_index_nexp env, (typ_error env)) id size order ranges) in defs, env | _ -> typ_error env l "Underlying bitfield type must be a constant-width bitvector" @@ -5420,20 +5420,26 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should have been rewritten before type checking" -and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot ast * Env.t = +and check_defs_progress : 'a. int -> int -> Env.t -> 'a def list -> tannot def list * Env.t = fun n total env defs -> match defs with - | [] -> Defs [], env + | [] -> [], env | def :: defs -> Util.progress "Type check " (string_of_int n ^ "/" ^ string_of_int total) n total; let (def, env) = check_def env def in - let Defs defs, env = check_defs (n + 1) total env defs in - Defs (def @ defs), env + let defs, env = check_defs_progress (n + 1) total env defs in + def @ defs, env -and check : 'a. Env.t -> 'a ast -> tannot ast * Env.t = - fun env (Defs defs) -> let total = List.length defs in check_defs 1 total env defs +and check_defs : 'a. Env.t -> 'a def list -> tannot def list * Env.t = + fun env defs -> let total = List.length defs in check_defs_progress 1 total env defs -and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list = +let check : 'a. Env.t -> 'a ast -> tannot ast * Env.t = + fun env ast -> + let total = List.length ast.defs in + let defs, env = check_defs_progress 1 total env ast.defs in + { ast with defs = defs }, env + +let rec check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list = fun env defs -> match defs with | [] -> [] diff --git a/src/type_check.mli b/src/type_check.mli index 74ad4441..24825e25 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -482,6 +482,8 @@ Some invariants that will hold of a fully checked AST are: Type_error.check *) val check : Env.t -> 'a ast -> tannot ast * Env.t +val check_defs : Env.t -> 'a def list -> tannot def list * Env.t + (** The same as [check], but exposes the intermediate type-checking environments so we don't have to always re-check the entire AST *) val check_with_envs : Env.t -> 'a def list -> (tannot def list * Env.t) list diff --git a/src/type_error.ml b/src/type_error.ml index 4faa774a..8b323714 100644 --- a/src/type_error.ml +++ b/src/type_error.ml @@ -186,6 +186,12 @@ let rec collapse_errors = function Err_because (err1, l, err2) | err -> err +let check_defs : 'a. Env.t -> 'a def list -> tannot def list * Env.t = + fun env defs -> + try Type_check.check_defs env defs with + | Type_error (env, l, err) -> + raise (Reporting.err_typ l (string_of_type_error err)) + let check : 'a. Env.t -> 'a ast -> tannot ast * Env.t = fun env defs -> try Type_check.check env defs with |