diff options
61 files changed, 717 insertions, 580 deletions
diff --git a/language/sail.ott b/language/sail.ott index a1dbda60..93ce382d 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -875,13 +875,6 @@ def :: 'DEF_' ::= | $ string1 string2 l :: :: pragma {{ com compiler directive }} -defs :: '' ::= - {{ com definition sequence }} - {{ auxparam 'a }} - | def1 .. defn :: :: Defs - - - terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} diff --git a/lib/coq/Operators_mwords.v b/lib/coq/Operators_mwords.v index 9b38c95c..bfbf6549 100644 --- a/lib/coq/Operators_mwords.v +++ b/lib/coq/Operators_mwords.v @@ -528,7 +528,7 @@ destruct n. compute. intuition. * simpl in *. destruct (weq v w). + subst. rewrite weqb_eq; tauto. - + rewrite weqb_ne; auto. intuition. + + rewrite weqb_ne; auto. split; congruence. * destruct v. Qed. diff --git a/src/cgen_backend.ml b/src/ast_defs.ml index 77029c9e..0826fb42 100644 --- a/src/cgen_backend.ml +++ b/src/ast_defs.ml @@ -49,29 +49,13 @@ (**************************************************************************) open Ast -open Ast_util -open PPrint -let to_string doc = - let b = Buffer.create 120 in - ToBuffer.pretty 1. 120 b doc; - Buffer.contents b +type 'a ast = { + defs : 'a def list; + comments : (string * Lexer.comment list) list + } -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 +let empty_ast = { + defs = []; + comments = [] + } diff --git a/src/ast_util.ml b/src/ast_util.ml index 3123d447..f1df1ff5 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Util module Big_int = Nat_big_num @@ -712,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_defs_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) @@ -1085,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_defs (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 @@ -1539,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_defs 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; comments = ast1.comments @ ast2.comments } +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 @@ -2216,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 6ac29123..21a546ee 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -51,6 +51,7 @@ (** Utilities and helper functions for operating on Sail ASTs *) open Ast +open Ast_defs module Big_int = Nat_big_num type mut = Immutable | Mutable @@ -354,7 +355,7 @@ val map_valspec_annot : ('a annot -> 'b annot) -> 'a val_spec -> 'b val_spec val map_scattered_annot : ('a annot -> 'b annot) -> 'a scattered_def -> 'b scattered_def val map_def_annot : ('a annot -> 'b annot) -> 'a def -> 'b def -val map_defs_annot : ('a annot -> 'b annot) -> 'a defs -> 'b defs +val map_ast_annot : ('a annot -> 'b annot) -> 'a ast -> 'b ast (** {2 Extract locations from terms} *) val id_loc : id -> Parse_ast.l @@ -454,17 +455,19 @@ val rename_valspec : id -> 'a val_spec -> 'a val_spec val rename_fundef : id -> 'a fundef -> 'a fundef -val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option +val split_defs : ('a def -> bool) -> 'a def list -> ('a def list * 'a def * 'a def list) option -val append_ast : 'a defs -> 'a defs -> 'a defs -val concat_ast : 'a defs list -> 'a defs +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 defs -> IdSet.t +val ids_of_defs : 'a def list -> IdSet.t +val ids_of_ast : 'a ast -> IdSet.t -val val_spec_ids : 'a defs -> IdSet.t +val val_spec_ids : 'a def list -> IdSet.t val pat_ids : 'a pat -> IdSet.t @@ -501,7 +504,7 @@ val extern_assoc : string -> (string * string) list -> string option the closest annotation or even finding an annotation at all. This is used by the Emacs mode to provide type-at-cursor functionality and we don't mind if it's a bit fuzzy in that context. *) -val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a defs -> (Ast.l * 'a) option +val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a ast -> (Ast.l * 'a) option (** {2 Substitutions} diff --git a/src/bitfield.ml b/src/bitfield.ml index 5b0a73b0..46c18735 100644 --- a/src/bitfield.ml +++ b/src/bitfield.ml @@ -52,17 +52,12 @@ module Big_int = Nat_big_num open Initial_check open Ast +open Ast_defs 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)) @@ -75,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 @@ -97,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 = @@ -108,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 @@ -127,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 @@ -145,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 @@ -161,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) = @@ -175,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/constant_fold.ml b/src/constant_fold.ml index 1c273df1..c9314002 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -302,7 +302,7 @@ let rec rewrite_constant_function_calls' fixed target ast = rewriters_base with rewrite_exp = (fun _ -> rw_exp fixed target ok not_ok istate) } in - let ast = rewrite_defs_base rw_defs ast in + let ast = rewrite_ast_base rw_defs ast in (* We keep iterating until we have no more re-writes to do *) if !rewrite_count > 0 then rewrite_constant_function_calls' fixed target ast diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index c190cffc..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_defs (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 @@ -894,4 +892,4 @@ let remove_impossible_int_cases _ = in let open Rewriter in let rewrite_exp _ = fold_exp { id_exp_alg with e_case = e_case; e_if = e_if } in - rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } + rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp } diff --git a/src/constant_propagation.mli b/src/constant_propagation.mli index 9c182cb0..fb2ad179 100644 --- a/src/constant_propagation.mli +++ b/src/constant_propagation.mli @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Type_check @@ -60,7 +61,7 @@ open Type_check val const_prop : string -> - tannot defs -> + tannot ast -> IdSet.t -> tannot exp Bindings.t * nexp KBindings.t -> tannot exp Bindings.t -> @@ -69,4 +70,4 @@ val const_prop : val referenced_vars : tannot exp -> IdSet.t -val remove_impossible_int_cases : 'a -> tannot defs -> tannot defs +val remove_impossible_int_cases : 'a -> tannot ast -> tannot ast diff --git a/src/constant_propagation_mutrec.ml b/src/constant_propagation_mutrec.ml index 03d8e154..421964f4 100644 --- a/src/constant_propagation_mutrec.ml +++ b/src/constant_propagation_mutrec.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Type_check open Rewriter @@ -158,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 @@ -166,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 @@ -183,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_defs target env (Defs defs) = +let rewrite_ast target env ({ defs; _ } as ast) = let rec rewrite = function | [] -> [] | DEF_internal_mutrec mutrecs :: ds -> @@ -205,7 +206,7 @@ let rewrite_defs target env (Defs defs) = | [] -> [infer_exp env (mk_lit_exp L_unit)] | args' -> args' in - if not (IdSet.mem id' (ids_of_defs (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 @@ -213,7 +214,7 @@ let rewrite_defs 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 @@ -234,7 +235,7 @@ let rewrite_defs 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) @@ -243,9 +244,9 @@ let rewrite_defs 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 828d1b5e..1b21e2be 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -49,8 +49,9 @@ (**************************************************************************) open Ast -open Util +open Ast_defs open Ast_util +open Util open Printf module Big_int = Nat_big_num @@ -846,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; comments = [] }, ctx let initial_ctx = { type_constructors = @@ -930,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 [] @@ -1025,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 [] @@ -1042,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 = @@ -1100,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 @@ -1122,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 5a352eee..6ca8ac80 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -51,6 +51,7 @@ (** Initial desugaring pass over AST after parsing *) open Ast +open Ast_defs open Ast_util (** {2 Options} *) @@ -96,14 +97,15 @@ val undefined_builtin_val_specs : unit def list (** If the generate flag is false, then we won't generate any auxilliary definitions, like the initialize_registers function *) -val process_ast : ?generate:bool -> Parse_ast.defs -> unit defs +val process_ast : ?generate:bool -> Parse_ast.defs -> unit ast (** {2 Parsing expressions and definitions from strings} *) val extern_of_string : id -> string -> unit def val val_spec_of_string : id -> string -> unit def -val ast_of_def_string : string -> unit defs -val ast_of_def_string_with : (Parse_ast.def list -> Parse_ast.def list) -> string -> unit defs +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 val typ_of_string : string -> typ val constraint_of_string : string -> n_constraint diff --git a/src/interactive.ml b/src/interactive.ml index 93df1dc0..20f16c6f 100644 --- a/src/interactive.ml +++ b/src/interactive.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Printf @@ -59,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/interactive.mli b/src/interactive.mli index b0cce425..0b087dc7 100644 --- a/src/interactive.mli +++ b/src/interactive.mli @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Type_check val opt_interactive : bool ref @@ -56,7 +57,7 @@ val opt_emacs_mode : bool ref val opt_suppress_banner : bool ref val opt_auto_interpreter_rewrites : bool ref -val ast : tannot defs ref +val ast : tannot ast ref val env : Env.t ref diff --git a/src/interpreter.ml b/src/interpreter.ml index b3e8fe31..b0faabce 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Value @@ -755,11 +756,11 @@ let exp_of_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) value = let pexp_of_funcl (FCL_aux (FCL_Funcl (_, pexp), _)) = pexp in E_aux (E_case (exp_of_value value, List.map pexp_of_funcl funcls), annot) -let rec ast_letbinds (Defs defs) = +let rec defs_letbinds defs = match defs with | [] -> [] - | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs) - | _ :: defs -> ast_letbinds (Defs defs) + | DEF_val lb :: defs -> lb :: defs_letbinds defs + | _ :: defs -> defs_letbinds defs let initial_lstate = { locals = Bindings.empty } @@ -945,11 +946,11 @@ let rec run_frame frame = let eval_exp state exp = run_frame (Step (lazy "", state, return exp, [])) -let initial_gstate primops ast env = +let initial_gstate primops defs env = { registers = Bindings.empty; allow_registers = true; primops = primops; - letbinds = ast_letbinds ast; + letbinds = defs_letbinds defs; fundefs = Bindings.empty; last_write_ea = None; typecheck_env = env; @@ -972,14 +973,14 @@ let rec initialize_registers allow_registers gstate = | _ -> gstate in function - | Defs (def :: defs) -> - initialize_registers allow_registers (process_def def) (Defs defs) - | Defs [] -> gstate + | def :: defs -> + initialize_registers allow_registers (process_def def) defs + | [] -> gstate let initial_state ?(registers=true) ast env primops = - let gstate = initial_gstate primops ast env in + let gstate = initial_gstate primops ast.defs env in let gstate = - { (initialize_registers registers gstate ast) + { (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 e7864751..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 []; + 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 []; + 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 b2447125..2fe21d93 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Jib open Jib_compile @@ -2195,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 @@ -2215,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 = @@ -2229,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_backend.mli b/src/jib/c_backend.mli index 2d3d3c2b..cbd0d36e 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -48,6 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) +open Ast_defs open Jib open Type_check @@ -99,7 +100,7 @@ val optimize_alias : bool ref val optimize_fixed_int : bool ref val optimize_fixed_bits : bool ref -val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx -val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit +val jib_of_ast : Env.t -> tannot ast -> cdef list * Jib_compile.ctx +val compile_ast : Env.t -> out_channel -> string list -> tannot ast -> unit -val compile_ast_clib : Env.t -> tannot Ast.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit +val compile_ast_clib : Env.t -> tannot ast -> (Jib_compile.ctx -> cdef list -> unit) -> unit diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml index 3cf56ba4..b92713ff 100644 --- a/src/jib/c_codegen.ml +++ b/src/jib/c_codegen.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Jib open Jib_compile @@ -1665,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 @@ -1685,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 42228cd6..cd4edd12 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Jib open Jib_util @@ -1641,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 @@ -1652,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 @@ -1668,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_compile.mli b/src/jib/jib_compile.mli index 30f379d8..a0acdd0d 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -52,6 +52,7 @@ open Anf open Ast +open Ast_defs open Ast_util open Jib open Type_check @@ -127,7 +128,7 @@ module Make(C: Config) : sig (see Util.progress). *) val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx - val compile_ast : ctx -> tannot defs -> cdef list * ctx + val compile_ast : ctx -> tannot ast -> cdef list * ctx end (** Adds some special functions to the environment that are used to diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 6cbd1b87..434ca8a9 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -50,6 +50,7 @@ open Anf open Ast +open Ast_defs open Ast_util open Jib open Jib_util @@ -90,7 +91,7 @@ type ctx = { tc_env : Type_check.Env.t; pragma_l : Ast.l; arg_stack : (int * string) Stack.t; - ast : Type_check.tannot defs; + ast : Type_check.tannot ast; shared : ctyp Bindings.t; preserved : IdSet.t; events : smt_exp Stack.t EventMap.t ref; @@ -117,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/jib/jib_smt.mli b/src/jib/jib_smt.mli index 616877e4..820f06d1 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Jib open Jib_util @@ -91,7 +92,7 @@ type ctx = { generating the SMT for. Used for error messages. *) arg_stack : (int * string) Stack.t; (** Used internally to keep track of function argument names *) - ast : Type_check.tannot defs; + ast : Type_check.tannot ast; (** The fully type-checked ast *) shared : ctyp Bindings.t; (** Shared variables. These variables do not get renamed by @@ -123,7 +124,7 @@ type ctx = { } (** Compile an AST into Jib suitable for SMT generation, and initialise a context. *) -val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * Jib_compile.ctx * ctx +val compile : Type_check.Env.t -> Type_check.tannot ast -> cdef list * Jib_compile.ctx * ctx (* TODO: Currently we internally use mutable stacks and queues to avoid any issues with stack overflows caused by some non @@ -153,7 +154,7 @@ module Make_optimizer(S : Sequence) : sig end val serialize_smt_model : - string -> Type_check.Env.t -> Type_check.tannot defs -> unit + string -> Type_check.Env.t -> Type_check.tannot ast -> unit val deserialize_smt_model : string -> cdef list * ctx @@ -164,5 +165,5 @@ val generate_smt : (string * string * l * 'a val_spec) Bindings.t (* See Property.find_properties *) -> (string -> string) (* Applied to each function name to generate the file name for the smtlib file *) -> Type_check.Env.t - -> Type_check.tannot defs + -> Type_check.tannot ast -> unit diff --git a/src/latex.ml b/src/latex.ml index be3e8748..9cb0b4d8 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open PPrint open Printf @@ -241,7 +242,7 @@ let latex_of_markdown str = | Paragraph elems -> let prepend = if state.noindent then (state.noindent <- false; "\\noindent ") else "" in prepend ^ format elems ^ "\n\n" - | Text str -> Str.global_replace (Str.regexp_string "_") "\\_" str + | Text str -> text_code str | Emph elems -> sprintf "\\emph{%s}" (format elems) | Bold elems -> sprintf "\\textbf{%s}" (format elems) | Ref (r, "THIS", alt, _) -> @@ -437,10 +438,15 @@ 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 + let preamble = string ("\\providecommand\\saildoclabelled[2]{\\phantomsection\\label{#1}#2}\n" ^ + "\\providecommand\\saildocval[2]{#1 #2}\n" ^ + "\\providecommand\\saildocfcl[2]{#1 #2}\n" ^ + "\\providecommand\\saildoctype[2]{#1 #2}\n" ^ + "\\providecommand\\saildocfn[2]{#1 #2}\n" ^ + "\\providecommand\\saildocoverload[2]{#1 #2}\n\n") in let overload_counter = ref 0 in @@ -500,7 +506,7 @@ let defs (Defs defs) = identifiers then outputs the correct mangled command. *) let id_command cat ids = sprintf "\\newcommand{\\%s%s}[1]{\n " !opt_prefix (category_name cat) - ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s}{}" (string_of_id id) (latex_cat_id cat id)) + ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s}{}" (text_code (string_of_id id)) (latex_cat_id cat id)) (IdSet.elements ids) ^ "}" |> string 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..c5d81af6 100644 --- a/src/libsail.mllib +++ b/src/libsail.mllib @@ -1,9 +1,9 @@ Anf Ast +Ast_defs 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 9bb47774..d86db99d 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -56,6 +56,7 @@ open Parse_ast open Ast +open Ast_defs open Ast_util module Big_int = Nat_big_num open Type_check @@ -657,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)]) @@ -681,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 *) @@ -772,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 @@ -1170,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'' } @@ -1337,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 @@ -1345,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 @@ -1454,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 @@ -1585,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 @@ -2760,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 *) @@ -2828,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 @@ -2865,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 @@ -3409,7 +3411,7 @@ and rewrite_exp exp = Rewriter.fold_exp { Rewriter.id_exp_alg with e_aux = rewri let mono_rewrite defs = let open Rewriter in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_exp = fun _ -> fold_exp { id_exp_alg with e_aux = rewrite_aux } } defs @@ -3682,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 @@ -3833,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 @@ -3843,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 = @@ -3907,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 @@ -4075,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; @@ -4093,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/monomorphise.mli b/src/monomorphise.mli index f8a17494..bf6c9520 100644 --- a/src/monomorphise.mli +++ b/src/monomorphise.mli @@ -48,6 +48,8 @@ (* SUCH DAMAGE. *) (**************************************************************************) +open Ast_defs + type options = { auto : bool; (* Analyse ast to find splits for monomorphisation *) debug_analysis : int; (* Debug output level for the automatic analysis *) @@ -59,17 +61,17 @@ val monomorphise : string -> (* Target backend *) options -> ((string * int) * string) list -> (* List of splits from the command line *) - Type_check.tannot Ast.defs -> - Type_check.tannot Ast.defs + Type_check.tannot ast -> + Type_check.tannot ast (* Rewrite (combinations of) variable-sized operations into fixed-sized operations *) -val mono_rewrites : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val mono_rewrites : Type_check.tannot ast -> Type_check.tannot ast (* Move complex nexps in function signatures into constraints *) -val rewrite_toplevel_nexps : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val rewrite_toplevel_nexps : Type_check.tannot ast -> Type_check.tannot ast (* Add casts across case splits *) -val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast (* Replace atom arguments which are fixed by a type parameter for a size with a singleton type *) -val rewrite_atoms_to_singletons : string -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val rewrite_atoms_to_singletons : string -> Type_check.tannot ast -> Type_check.tannot ast diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 98a43ebc..fed28b99 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open PPrint open Type_check @@ -634,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 -> [] @@ -660,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 @@ -682,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 @@ -925,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 = @@ -941,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 @@ -968,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 = @@ -985,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 -> @@ -1006,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 b0d05bef..fccf0f3a 100644 --- a/src/optimize.ml +++ b/src/optimize.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Rewriter @@ -64,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 @@ -111,4 +112,4 @@ let recheck (Defs defs) = | [] -> [] in - Defs (find_optimizations defs) + { ast with defs = find_optimizations defs } diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 5537f42c..2995b8a3 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -49,7 +49,8 @@ (**************************************************************************) open Ast +open Ast_defs open Type_check (* Prints on formatter the defs as Lem Ast nodes *) -val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> Env.t -> tannot defs -> string -> unit +val pp_ast_lem : (out_channel * string list) -> (out_channel * string list) -> Env.t -> tannot ast -> string -> unit diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index dbb0356d..7f28fac8 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -50,6 +50,7 @@ open Type_check open Ast +open Ast_defs open Ast_util open Reporting open Rewriter @@ -3231,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 @@ -3280,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 b18541a3..e40de7aa 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -50,6 +50,7 @@ open Type_check open Ast +open Ast_defs open Ast_util open Reporting open Rewriter @@ -1534,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 @@ -1560,7 +1560,7 @@ let find_exc_typ defs = | _ -> false in if List.exists is_exc_typ_def defs then "exception" else "unit" -let pp_defs_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 4114920a..ad4d5a75 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open PPrint @@ -768,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 @@ -823,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 a0245c8f..d67fba76 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -48,6 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) +open Ast_defs open PPrint open Pretty_print_common @@ -263,10 +264,10 @@ let opt_ddump_tc_ast = ref false let opt_ddump_rewrite_ast = ref None let opt_dno_cast = ref false -let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = +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 defs in - let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in + let ast, env = Type_error.check env ast 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) @@ -274,9 +275,15 @@ let load_files ?check:(check=false) options type_envs files = if !opt_memo_z3 then Constraint.load_digests () else (); let t = Profile.start () in - let ast = Parse_ast.Defs (List.map (fun f -> (f, parse_file f |> snd |> preprocess options)) files) in + + let parsed_files = List.map (fun f -> (f, parse_file f)) files in + + let comments = List.map (fun (f, (comments, _)) -> (f, comments)) parsed_files in + let ast = Parse_ast.Defs (List.map (fun (f, (_, file_ast)) -> (f, preprocess options file_ast)) parsed_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 ast = { ast with comments = comments } in + + let () = if !opt_ddump_initial_ast then Pretty_print_sail.pp_ast stdout ast else () in begin match !opt_reformat with | Some dir -> @@ -329,7 +336,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 @@ -357,7 +364,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 @@ -366,10 +373,10 @@ let output_lem filename libs type_env defs = open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in let ((o,_,_,_) as ext_o) = open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in - (Pretty_print.pp_defs_lem + (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) = @@ -377,7 +384,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 @@ -395,10 +402,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 @@ -407,49 +414,48 @@ 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_defs 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_defs_target tgt) +let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_ast_target tgt) -let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check +let rewrite_ast_check env = rewrite env Rewrites.rewrite_ast_check let descatter type_envs ast = let ast = Scattered.descatter ast in diff --git a/src/process_file.mli b/src/process_file.mli index ea00dd29..1c4cddc9 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -48,6 +48,8 @@ (* SUCH DAMAGE. *) (**************************************************************************) +open Ast_defs + (** Parse a file. The optional loc argument is the location of the $include directive that is importing the file, if applicable. *) val parse_file : ?loc:Parse_ast.l -> string -> Lexer.comment list * Parse_ast.def list @@ -57,10 +59,10 @@ val have_symbol : string -> bool val add_symbol : string -> unit val preprocess : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.def list -> Parse_ast.def list -val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t -val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t -val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t -val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t +val check_ast : Type_check.Env.t -> unit ast -> Type_check.tannot ast * Type_check.Env.t +val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t +val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t +val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t val opt_file_out : string option ref val opt_memo_z3 : bool ref @@ -82,9 +84,9 @@ type out_type = | Coq_out of string list (* If present, the strings are files to open in the coq backend*) val output : - string -> (* The path to the library *) - out_type -> (* Backend kind *) - (string * Type_check.Env.t * Type_check.tannot Ast.defs) list -> (*File names paired with definitions *) + string -> (* The path to the library *) + out_type -> (* Backend kind *) + (string * Type_check.Env.t * Type_check.tannot ast) list -> (*File names paired with definitions *) unit (** [always_replace_files] determines whether Sail only updates modified files. @@ -93,6 +95,6 @@ val output : the output file is only updated, if its content really changes. *) val always_replace_files : bool ref -val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot Ast.defs * Type_check.Env.t) +val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot ast * Type_check.Env.t) -val descatter : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t +val descatter : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t diff --git a/src/property.ml b/src/property.ml index 83594f4f..6a648bd8 100644 --- a/src/property.ml +++ b/src/property.ml @@ -49,10 +49,11 @@ (**************************************************************************) open Ast +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 @@ -68,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 -> @@ -117,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/property.mli b/src/property.mli index 66a732b9..2d366fa0 100644 --- a/src/property.mli +++ b/src/property.mli @@ -52,6 +52,7 @@ $counterexample pragmas. *) open Ast +open Ast_defs open Ast_util open Type_check @@ -66,7 +67,7 @@ open Type_check where prop_type is either "counterexample" or "property" and the location loc is the location that was attached to the pragma *) -val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t +val find_properties : 'a ast -> (string * string * l * 'a val_spec) Bindings.t (** For a property @@ -86,7 +87,7 @@ val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t generation/proving we want to ensure that inputs outside the constraints of the function are ignored. *) -val rewrite : tannot defs -> tannot defs +val rewrite : tannot ast -> tannot ast type event = Overflow | Assertion | Assumption | Match | Return diff --git a/src/rewriter.ml b/src/rewriter.ml index 3b68f493..c5d829f6 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -50,6 +50,7 @@ module Big_int = Nat_big_num open Ast +open Ast_defs open Ast_util open Type_check @@ -60,7 +61,7 @@ type 'a rewriters = { rewrite_let : 'a rewriters -> 'a letbind -> 'a letbind; rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef; rewrite_def : 'a rewriters -> 'a def -> 'a def; - rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; + rewrite_ast : 'a rewriters -> 'a ast -> 'a ast; } let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a @@ -385,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_defs_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_defs_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 -> @@ -400,7 +401,7 @@ let rewrite_defs_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 @@ -410,56 +411,6 @@ let rec takedrop n xs = let ys, xs = takedrop (n - 1) xs in x :: ys, xs -let rewrite_defs_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_defs_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; @@ -467,9 +418,9 @@ let rewriters_base = rewrite_lexp = rewrite_lexp; rewrite_fun = rewrite_fun; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} + rewrite_ast = rewrite_ast_base} -let rewrite_defs (Defs defs) = rewrite_defs_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 f61bcc66..ab071318 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -52,6 +52,7 @@ module Big_int = Nat_big_num open Ast +open Ast_defs open Type_check type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; @@ -60,7 +61,7 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; rewrite_let : 'a rewriters -> 'a letbind -> 'a letbind; rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef; rewrite_def : 'a rewriters -> 'a def -> 'a def; - rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; + rewrite_ast : 'a rewriters -> 'a ast -> 'a ast; } val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp @@ -68,14 +69,12 @@ val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp val rewriters_base : tannot rewriters (** The identity re-writer *) -val rewrite_defs : tannot defs -> tannot defs +val rewrite_ast : tannot ast -> tannot ast -val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs - -val rewrite_defs_base_parallel : int -> tannot rewriters -> tannot defs -> tannot defs +val rewrite_ast_base : tannot rewriters -> tannot ast -> tannot ast (** Same as rewrite_defs_base but display a progress bar when verbosity >= 1 *) -val rewrite_defs_base_progress : string -> tannot rewriters -> tannot defs -> tannot defs +val rewrite_ast_base_progress : string -> tannot rewriters -> tannot ast -> tannot ast val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp diff --git a/src/rewrites.ml b/src/rewrites.ml index 574356d4..57b71ec7 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -50,6 +50,7 @@ module Big_int = Nat_big_num open Ast +open Ast_defs open Ast_util open Type_check open Spec_analysis @@ -218,7 +219,7 @@ let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with | Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l) | _ -> nexp_aux -let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = +let rewrite_ast_nexp_ids, rewrite_typ_nexp_ids = let rec rewrite_typ env (Typ_aux (typ, l) as typ_aux) = match typ with | Typ_fn (arg_ts, ret_t, eff) -> Typ_aux (Typ_fn (List.map (rewrite_typ env) arg_ts, rewrite_typ env ret_t, eff), l) @@ -270,20 +271,20 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = | d -> Rewriter.rewrite_def rewriters d in - (fun env defs -> rewrite_defs_base { rewriters_base with + (fun env defs -> rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); rewrite_def = rewrite_def env } defs), rewrite_typ -let rewrite_defs_remove_assert defs = +let rewrite_ast_remove_assert defs = let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with | E_constraint _ -> E_assert (exp, str) | _ -> E_assert (E_aux (E_lit (mk_lit L_true), simple_annot l bool_typ), str) in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_assert = e_assert}) } defs @@ -594,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_defs_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; @@ -602,7 +603,7 @@ let rewrite_defs_remove_vector_concat env (Defs defs) = rewrite_lexp = rewrite_lexp; rewrite_fun = rewrite_fun_remove_vector_concat_pat; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} in + rewrite_ast = rewrite_ast_base} in let rewrite_def d = let d = rewriters.rewrite_def rewriters d in match d with @@ -611,7 +612,7 @@ let rewrite_defs_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 @@ -1187,7 +1188,7 @@ let rewrite_fun_remove_bitvector_pat | _ -> funcls in FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot)) -let rewrite_defs_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; @@ -1195,7 +1196,7 @@ let rewrite_defs_remove_bitvector_pats env (Defs defs) = rewrite_lexp = rewrite_lexp; rewrite_fun = rewrite_fun_remove_bitvector_pat; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base } in + rewrite_ast = rewrite_ast_base } in let rewrite_def d = let d = rewriters.rewrite_def rewriters d in match d with @@ -1206,13 +1207,13 @@ let rewrite_defs_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) *) -let rewrite_defs_remove_numeral_pats env = +let rewrite_ast_remove_numeral_pats env = let p_lit outer_env = function | L_aux (L_num n, l) -> let id = fresh_id "l__" Parse_ast.Unknown in @@ -1242,10 +1243,10 @@ let rewrite_defs_remove_numeral_pats env = FCL_aux (FCL_Funcl (id, fold_pexp exp_alg pexp), annot) in let rewrite_fun _ (FD_aux (FD_function (r_o, t_o, e_o, funcls), a)) = FD_aux (FD_function (r_o, t_o, e_o, List.map rewrite_funcl funcls), a) in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp; rewrite_fun = rewrite_fun } -let rewrite_defs_vector_string_pats_to_bit_list env = +let rewrite_ast_vector_string_pats_to_bit_list env = let rewrite_p_aux (pat, (annot : tannot annot)) = let env = env_of_annot annot in match pat with @@ -1265,7 +1266,7 @@ let rewrite_defs_vector_string_pats_to_bit_list env = let rewrite_exp rw exp = fold_exp { id_exp_alg with e_aux = rewrite_e_aux; pat_alg = pat_alg } exp in - rewrite_defs_base { rewriters_base with rewrite_pat = rewrite_pat; rewrite_exp = rewrite_exp } + rewrite_ast_base { rewriters_base with rewrite_pat = rewrite_pat; rewrite_exp = rewrite_exp } let rewrite_bit_lists_to_lits env = (* TODO Make all rewriting passes support bitvector literals instead of @@ -1298,7 +1299,7 @@ let rewrite_bit_lists_to_lits env = with _ -> rewrap e in let rewrite_exp rw = fold_exp { id_exp_alg with e_aux = e_aux; } in - rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } + rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp } (* Remove pattern guards by rewriting them to if-expressions within the pattern expression. *) @@ -1363,9 +1364,9 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd | _ -> funcls (* TODO is the empty list possible here? *) in FD_aux (FD_function(r,t,e,funcls),(l,fdannot)) -let rewrite_defs_guarded_pats env = - rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp_guarded_pats; - rewrite_fun = rewrite_fun_guarded_pats } +let rewrite_ast_guarded_pats env = + rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp_guarded_pats; + rewrite_fun = rewrite_fun_guarded_pats } let rec rewrite_lexp_to_rhs ((LEXP_aux(lexp,((l,_) as annot))) as le) = @@ -1396,7 +1397,7 @@ let updates_vars exp = fst (fold_exp { (compute_exp_alg false (||)) with e_assign = e_assign } exp) -(*Expects to be called after rewrite_defs; thus the following should not appear: +(*Expects to be called after rewrite_ast; thus the following should not appear: internal_exp of any form lit vectors in patterns or expressions *) @@ -1429,14 +1430,14 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f | _ -> rewrite_base full_exp -let rewrite_defs_exp_lift_assign env defs = rewrite_defs_base +let rewrite_ast_exp_lift_assign env defs = rewrite_ast_base {rewrite_exp = rewrite_exp_lift_assign_intro; rewrite_pat = rewrite_pat; rewrite_let = rewrite_let; rewrite_lexp = rewrite_lexp (*_lift_assign_intro*); rewrite_fun = rewrite_fun; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} defs + rewrite_ast = rewrite_ast_base} defs (* Rewrite assignments to register references into calls to a builtin function @@ -1446,9 +1447,9 @@ let rewrite_defs_exp_lift_assign env defs = rewrite_defs_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 @@ -1467,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 @@ -1477,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_defs_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 @@ -1645,12 +1646,12 @@ let rewrite_defs_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_defs_base + 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) @@ -1701,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 = @@ -1799,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 -> @@ -1939,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) @@ -1972,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) @@ -1985,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 = @@ -1997,7 +1995,7 @@ let rewrite_undefined mwords env = | _ -> exp in let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) } + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) } let rewrite_undefined_if_gen always_bitvector env defs = if !Initial_check.opt_undefined_gen @@ -2028,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 @@ -2075,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_defs_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 = @@ -2136,7 +2134,7 @@ let rewrite_vector_concat_assignments env defs = e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot) } in let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in - rewrite_defs_base assign_defs defs + rewrite_ast_base assign_defs defs let rewrite_tuple_assignments env defs = let assign_tuple e_aux annot = @@ -2161,7 +2159,7 @@ let rewrite_tuple_assignments env defs = e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot) } in let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in - rewrite_defs_base assign_defs defs + rewrite_ast_base assign_defs defs let rewrite_simple_assignments allow_fields env defs = let rec is_simple (LEXP_aux (aux, _)) = @@ -2187,9 +2185,9 @@ let rewrite_simple_assignments allow_fields env defs = e_aux = (fun (e_aux, annot) -> assign_e_aux e_aux annot) } in let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in - rewrite_defs_base assign_defs defs + rewrite_ast_base assign_defs defs -let rewrite_defs_remove_blocks env = +let rewrite_ast_remove_blocks env = let letbind_wild v body = let l = get_loc_exp v in let env = env_of v in @@ -2211,14 +2209,14 @@ let rewrite_defs_remove_blocks env = let alg = { id_exp_alg with e_aux = e_aux } in - rewrite_defs_base + rewrite_ast_base {rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } @@ -2248,7 +2246,7 @@ let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list | [] -> k [] | exp :: exps -> f exp (fun exp -> mapCont f exps (fun exps -> k (exp :: exps))) -let rewrite_defs_letbind_effects env = +let rewrite_ast_letbind_effects env = let rec value ((E_aux (exp_aux,_)) as exp) = not (effectful exp || updates_vars exp) @@ -2513,7 +2511,6 @@ let rewrite_defs_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 @@ -2527,17 +2524,17 @@ let rewrite_defs_letbind_effects env = DEF_internal_mutrec (List.map (rewrite_fun rewriters) fdefs) | d -> d in - rewrite_defs_base + rewrite_ast_base {rewrite_exp = rewrite_exp ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } -let rewrite_defs_internal_lets env = +let rewrite_ast_internal_lets env = let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with | LEXP_id id -> P_aux (P_id id, annot) @@ -2580,14 +2577,14 @@ let rewrite_defs_internal_lets env = E_let (LB_aux (LB_val (P_aux (paux, annot), exp1), annot), exp2) in let alg = { id_exp_alg with e_let = e_let; e_var = e_var } in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = (fun _ exp -> fold_exp alg (propagate_exp_effect exp)) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } @@ -2625,7 +2622,7 @@ let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot anno let pexp_rewriters rewrite_pexp = let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } let stringappend_counter = ref 0 @@ -2861,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_defs_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 *) @@ -2895,10 +2892,10 @@ let rewrite_defs_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_defs_pat_string_append env = +let rec rewrite_ast_pat_string_append env = let rec rewrite_pat env ((pat : tannot pat), (guards : tannot exp list), (expr : tannot exp)) = let guards_ref = ref guards in let expr_ref = ref expr in @@ -3146,7 +3143,7 @@ let fresh_mappingpatterns_id () = mappingpatterns_counter := !mappingpatterns_counter + 1; id -let rewrite_defs_mapping_patterns env = +let rewrite_ast_mapping_patterns env = let rec rewrite_pat env (pat, guards, expr) = let guards_ref = ref guards in let expr_ref = ref expr in @@ -3301,7 +3298,7 @@ let rewrite_lit_ocaml (L_aux (lit, _)) = match lit with | L_num _ | L_string _ | L_hex _ | L_bin _ | L_real _ | L_unit -> false | _ -> true -let rewrite_defs_pat_lits rewrite_lit env ast = +let rewrite_ast_pat_lits rewrite_lit env ast = let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) = let guards = ref [] in let counter = ref 0 in @@ -3351,8 +3348,8 @@ let rewrite_defs_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_defs_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, @@ -3402,7 +3399,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let typ' = typ_of exp in add_e_cast (env_of exp) typ' (E_aux (expaux, swaptyp typ' annot)) | _ -> - (* after rewrite_defs_letbind_effects there cannot be terms that have + (* after rewrite_ast_letbind_effects there cannot be terms that have effects/update local variables in "tail-position": check n_exp_term and where it is used. *) if overwrite then @@ -3524,7 +3521,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = else let e1 = rewrite_var_updates (add_vars overwrite e1 vars) in let e2 = rewrite_var_updates (add_vars overwrite e2 vars) in - (* after rewrite_defs_letbind_effects c has no variable updates *) + (* after rewrite_ast_letbind_effects c has no variable updates *) let env = env_of_annot annot in let typ = typ_of e1 in let eff = union_eff_exps [c;e1;e2] in @@ -3533,7 +3530,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | E_case (e1,ps) | E_try (e1, ps) -> let is_case = match expaux with E_case _ -> true | _ -> false in let vars, varpats = - (* for E_case, e1 needs no rewriting after rewrite_defs_letbind_effects *) + (* for E_case, e1 needs no rewriting after rewrite_ast_letbind_effects *) ((if is_case then [] else [e1]) @ List.map (fun (Pat_aux ((Pat_exp (_,e)|Pat_when (_,_,e)),_)) -> e) ps) |> List.map find_updated_vars @@ -3600,7 +3597,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = Same_vars (E_aux (E_cast (typ, exp'), annot)) end | _ -> - (* after rewrite_defs_letbind_effects this expression is pure and updates + (* after rewrite_ast_letbind_effects this expression is pure and updates no variables: check n_exp_term and where it's used. *) Same_vars (E_aux (expaux,annot)) in @@ -3672,7 +3669,7 @@ let remove_reference_types exp = -let rewrite_defs_remove_superfluous_letbinds env = +let rewrite_ast_remove_superfluous_letbinds env = let e_aux (exp,annot) = match exp with | E_let (LB_aux (LB_val (pat, exp1), _), exp2) @@ -3707,18 +3704,18 @@ let rewrite_defs_remove_superfluous_letbinds env = | _ -> E_aux (exp,annot) in let alg = { id_exp_alg with e_aux = e_aux } in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } (* FIXME: We shouldn't allow nested not-patterns *) -let rewrite_defs_not_pats env = +let rewrite_ast_not_pats env = let rewrite_pexp (pexp_aux, annot) = let rewrite_pexp' pat exp orig_guard = let guards = ref [] in @@ -3765,9 +3762,9 @@ let rewrite_defs_not_pats env = rewrite_pexp' pat exp (Some (strip_exp guard)) in let rw_exp = { id_exp_alg with pat_aux = rewrite_pexp } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) } + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) } -let rewrite_defs_remove_superfluous_returns env = +let rewrite_ast_remove_superfluous_returns env = let add_opt_cast typopt1 typopt2 annot exp = match typopt1, typopt2 with @@ -3809,37 +3806,37 @@ let rewrite_defs_remove_superfluous_returns env = | _ -> E_aux (exp,annot) in let alg = { id_exp_alg with e_aux = e_aux } in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } -let rewrite_defs_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_defs_base + rewrite_ast_base { rewrite_exp = rewrite_exp ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base - } (Defs (loop_specs @ defs)) + ; rewrite_ast = rewrite_ast_base + } { 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 @@ -3857,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) = @@ -3898,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_defs_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 @@ -4111,7 +4108,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) = [] end in - let has_def id = IdSet.mem id (ids_of_defs (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) @@ -4125,7 +4122,7 @@ let rewrite_defs_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, @@ -4482,14 +4479,14 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) = let rewrite env = let alg = { id_exp_alg with e_aux = rewrite_case } in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } @@ -4499,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 @@ -4520,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 @@ -4550,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) -> @@ -4566,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 @@ -4698,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. *) @@ -4721,7 +4718,7 @@ let rewrite_loops_with_escape_effect env defs = in E_aux (E_loop (l,m,guard,body),ann) | _ -> exp in - rewrite_defs_base { rewriters_base with rewrite_exp } defs + rewrite_ast_base { rewriters_base with rewrite_exp } defs let recheck_defs env defs = Type_error.check initial_env defs let recheck_defs_without_effects env defs = @@ -4734,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 @@ -4753,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 -> @@ -4772,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 @@ -4798,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 | [] -> () @@ -4806,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 @@ -4836,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 @@ -4852,7 +4849,7 @@ let rewrite_truncate_hex_literals _type_env defs = E_aux (E_lit (L_aux (L_bin truncation, l_ann)), annot) | _ -> E_aux (e, annot) in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_aux = rewrite_aux }) } defs @@ -4909,8 +4906,8 @@ let if_flag_env flag f env defs = if !flag then f env defs else defs, env type rewriter = - | Basic_rewriter of (Env.t -> tannot defs -> tannot defs) - | Checking_rewriter of (Env.t -> tannot defs -> tannot defs * Env.t) + | Basic_rewriter of (Env.t -> tannot ast -> tannot ast) + | Checking_rewriter of (Env.t -> tannot ast -> tannot ast * Env.t) | Bool_rewriter of (bool -> rewriter) | String_rewriter of (string -> rewriter) | Literal_rewriter of ((lit -> bool) -> rewriter) @@ -4956,11 +4953,11 @@ let all_rewrites = [ ("recheck_defs", Checking_rewriter recheck_defs); ("recheck_defs_without_effects", Checking_rewriter recheck_defs_without_effects); ("optimize_recheck_defs", Basic_rewriter (fun _ -> Optimize.recheck)); - ("realise_mappings", Basic_rewriter rewrite_defs_realise_mappings); + ("realise_mappings", Basic_rewriter rewrite_ast_realise_mappings); ("remove_duplicate_valspecs", Basic_rewriter remove_duplicate_valspecs); - ("toplevel_string_append", Basic_rewriter rewrite_defs_toplevel_string_append); - ("pat_string_append", Basic_rewriter rewrite_defs_pat_string_append); - ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns); + ("toplevel_string_append", Basic_rewriter rewrite_ast_toplevel_string_append); + ("pat_string_append", Basic_rewriter rewrite_ast_pat_string_append); + ("mapping_builtins", Basic_rewriter rewrite_ast_mapping_patterns); ("truncate_hex_literals", Basic_rewriter rewrite_truncate_hex_literals); ("mono_rewrites", Basic_rewriter mono_rewrites); ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps); @@ -4969,31 +4966,31 @@ let all_rewrites = [ ("atoms_to_singletons", String_rewriter (fun target -> (Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons target)))); ("add_bitvector_casts", Basic_rewriter Monomorphise.add_bitvector_casts); ("remove_impossible_int_cases", Basic_rewriter Constant_propagation.remove_impossible_int_cases); - ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_defs target))); + ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_ast target))); ("make_cases_exhaustive", Basic_rewriter MakeExhaustive.rewrite); ("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b))); - ("vector_string_pats_to_bit_list", Basic_rewriter rewrite_defs_vector_string_pats_to_bit_list); - ("remove_not_pats", Basic_rewriter rewrite_defs_not_pats); - ("pattern_literals", Literal_rewriter (fun f -> Basic_rewriter (rewrite_defs_pat_lits f))); + ("vector_string_pats_to_bit_list", Basic_rewriter rewrite_ast_vector_string_pats_to_bit_list); + ("remove_not_pats", Basic_rewriter rewrite_ast_not_pats); + ("pattern_literals", Literal_rewriter (fun f -> Basic_rewriter (rewrite_ast_pat_lits f))); ("vector_concat_assignments", Basic_rewriter rewrite_vector_concat_assignments); ("tuple_assignments", Basic_rewriter rewrite_tuple_assignments); ("simple_assignments", Basic_rewriter (rewrite_simple_assignments false)); ("simple_struct_assignments", Basic_rewriter (rewrite_simple_assignments true)); - ("remove_vector_concat", Basic_rewriter rewrite_defs_remove_vector_concat); - ("remove_bitvector_pats", Basic_rewriter rewrite_defs_remove_bitvector_pats); - ("remove_numeral_pats", Basic_rewriter rewrite_defs_remove_numeral_pats); - ("guarded_pats", Basic_rewriter rewrite_defs_guarded_pats); + ("remove_vector_concat", Basic_rewriter rewrite_ast_remove_vector_concat); + ("remove_bitvector_pats", Basic_rewriter rewrite_ast_remove_bitvector_pats); + ("remove_numeral_pats", Basic_rewriter rewrite_ast_remove_numeral_pats); + ("guarded_pats", Basic_rewriter rewrite_ast_guarded_pats); ("bit_lists_to_lits", Basic_rewriter rewrite_bit_lists_to_lits); - ("exp_lift_assign", Basic_rewriter rewrite_defs_exp_lift_assign); - ("early_return", Basic_rewriter rewrite_defs_early_return); - ("nexp_ids", Basic_rewriter rewrite_defs_nexp_ids); + ("exp_lift_assign", Basic_rewriter rewrite_ast_exp_lift_assign); + ("early_return", Basic_rewriter rewrite_ast_early_return); + ("nexp_ids", Basic_rewriter rewrite_ast_nexp_ids); ("fix_val_specs", Basic_rewriter rewrite_fix_val_specs); - ("remove_blocks", Basic_rewriter rewrite_defs_remove_blocks); - ("letbind_effects", Basic_rewriter rewrite_defs_letbind_effects); - ("remove_e_assign", Basic_rewriter rewrite_defs_remove_e_assign); - ("internal_lets", Basic_rewriter rewrite_defs_internal_lets); - ("remove_superfluous_letbinds", Basic_rewriter rewrite_defs_remove_superfluous_letbinds); - ("remove_superfluous_returns", Basic_rewriter rewrite_defs_remove_superfluous_returns); + ("remove_blocks", Basic_rewriter rewrite_ast_remove_blocks); + ("letbind_effects", Basic_rewriter rewrite_ast_letbind_effects); + ("remove_e_assign", Basic_rewriter rewrite_ast_remove_e_assign); + ("internal_lets", Basic_rewriter rewrite_ast_internal_lets); + ("remove_superfluous_letbinds", Basic_rewriter rewrite_ast_remove_superfluous_letbinds); + ("remove_superfluous_returns", Basic_rewriter rewrite_ast_remove_superfluous_returns); ("merge_function_clauses", Basic_rewriter merge_funcls); ("minimise_recursive_functions", Basic_rewriter minimise_recursive_functions); ("move_termination_measures", Basic_rewriter move_termination_measures); @@ -5083,7 +5080,7 @@ let rewrites_coq = [ ("minimise_recursive_functions", []); ("recheck_defs", []); ("exp_lift_assign", []); - (* ("remove_assert", rewrite_defs_remove_assert); *) + (* ("remove_assert", rewrite_ast_remove_assert); *) ("move_termination_measures", []); ("top_sort_defs", []); ("early_return", []); @@ -5188,7 +5185,7 @@ let rewrites_target tgt = | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Invalid target for rewriting: " ^ tgt)) -let rewrite_defs_target tgt = +let rewrite_ast_target tgt = List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) (rewrites_target tgt) let rewrite_check_annot = @@ -5215,9 +5212,9 @@ let rewrite_check_annot = let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> check_annot (E_aux (exp, annot))); pat_alg = { id_pat_alg with p_aux = (fun (pat, annot) -> check_pat (P_aux (pat, annot))) } } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); rewrite_pat = (fun _ -> check_pat) } -let rewrite_defs_check = [ +let rewrite_ast_check = [ ("check_annotations", fun env defs -> rewrite_check_annot defs, env); ] diff --git a/src/rewrites.mli b/src/rewrites.mli index 43a2e057..91a3536c 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Type_check (* Monomorphisation options *) @@ -64,17 +65,17 @@ val opt_dmono_continue : bool ref val fresh_id : string -> l -> id (* Move loop termination measures into loop AST nodes *) -val move_loop_measures : 'a defs -> 'a defs +val move_loop_measures : 'a ast -> 'a ast (* Re-write undefined to functions created by -undefined_gen flag *) -val rewrite_undefined : bool -> Env.t -> tannot defs -> tannot defs +val rewrite_undefined : bool -> Env.t -> tannot ast -> tannot ast (* Perform rewrites to create an AST supported for a specific target *) -val rewrite_defs_target : string -> (string * (Env.t -> tannot defs -> tannot defs * Env.t)) list +val rewrite_ast_target : string -> (string * (Env.t -> tannot ast -> tannot ast * Env.t)) list type rewriter = - | Basic_rewriter of (Env.t -> tannot defs -> tannot defs) - | Checking_rewriter of (Env.t -> tannot defs -> tannot defs * Env.t) + | Basic_rewriter of (Env.t -> tannot ast -> tannot ast) + | Checking_rewriter of (Env.t -> tannot ast -> tannot ast * Env.t) | Bool_rewriter of (bool -> rewriter) | String_rewriter of (string -> rewriter) | Literal_rewriter of ((lit -> bool) -> rewriter) @@ -98,6 +99,6 @@ val opt_coq_warn_nonexhaustive : bool ref (* This is a special rewriter pass that checks AST invariants without actually doing any re-writing *) -val rewrite_defs_check : (string * (Env.t -> tannot defs -> tannot defs * Env.t)) list +val rewrite_ast_check : (string * (Env.t -> tannot ast -> tannot ast * Env.t)) list val simple_typ : typ -> typ diff --git a/src/sail.ml b/src/sail.ml index 53a5cc5d..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 @@ -481,7 +481,7 @@ let target name out_name ast type_envs = else (l, Type_check.replace_env (Type_check.Env.set_prover None (Type_check.env_of_tannot tannot)) tannot) in - Marshal.to_string (Ast_util.map_defs_annot remove_prover ast, Type_check.Env.set_prover None type_envs) [Marshal.Compat_32] + Marshal.to_string (Ast_util.map_ast_annot remove_prover ast, Type_check.Env.set_prover None type_envs) [Marshal.Compat_32] |> Base64.encode_string |> output_string f; close_out f diff --git a/src/scattered.ml b/src/scattered.ml index 92cb3561..4b89a766 100644 --- a/src/scattered.ml +++ b/src/scattered.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util let funcl_id (FCL_aux (FCL_Funcl (id, _), _)) = id @@ -138,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 c249fb5a..bdd0b19e 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Rewriter @@ -299,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 @@ -323,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 @@ -357,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/slice.mli b/src/slice.mli index 0c15defb..ffc6f3bd 100644 --- a/src/slice.mli +++ b/src/slice.mli @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util type node = @@ -64,8 +65,8 @@ module Node : sig val compare : node -> node -> int end -val graph_of_ast : Type_check.tannot defs -> Graph.Make(Node).graph +val graph_of_ast : Type_check.tannot ast -> Graph.Make(Node).graph -val dot_of_ast : out_channel -> Type_check.tannot defs -> unit +val dot_of_ast : out_channel -> Type_check.tannot ast -> unit -val filter_ast : Set.Make(Node).t -> Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs +val filter_ast : Set.Make(Node).t -> Graph.Make(Node).graph -> Type_check.tannot ast -> Type_check.tannot ast diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 542ecaae..2c40b3ed 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -49,8 +49,9 @@ (**************************************************************************) open Ast -open Util +open Ast_defs open Ast_util +open Util module Nameset = Set.Make(String) @@ -511,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 (Ast.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 (* @@ -590,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/spec_analysis.mli b/src/spec_analysis.mli index 41ab9b6c..b111f6f0 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Util open Type_check @@ -76,7 +77,7 @@ val is_within_machine64 : typ -> nexp_range list -> triple *) (* produce a new ordering for defs, limiting to those listed in the list, which respects dependencies *) (* val restrict_defs : 'a defs -> string list -> 'a defs *) -val top_sort_defs : tannot defs -> tannot defs +val top_sort_defs : tannot ast -> tannot ast (** Return the set of mutable variables assigned to in the given AST. *) val assigned_vars : 'a exp -> IdSet.t diff --git a/src/specialize.ml b/src/specialize.ml index d705b83a..bbf74f46 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open Rewriter @@ -116,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 @@ -208,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 @@ -237,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; @@ -252,13 +253,13 @@ let rec instantiations_of spec id ast = let rewrite_pat = { id_pat_alg with p_aux = (fun (pat, annot) -> inspect_pat (P_aux (pat, annot))) } in let rewrite_exp = { id_exp_alg with pat_alg = rewrite_pat; e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in - let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); - rewrite_pat = (fun _ -> fold_pat rewrite_pat)} ast in + let _ = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); + rewrite_pat = (fun _ -> fold_pat rewrite_pat)} ast in !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 -> @@ -278,7 +279,7 @@ let rec rewrite_polymorphic_calls spec id ast = in let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = match typ_aux with @@ -367,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_defs (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" @@ -415,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 @@ -449,9 +450,9 @@ let specialize_annotations instantiation fdef = annot) let specialize_id_fundef instantiations id ast = - match split_defs (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 @@ -462,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 = @@ -477,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 @@ -500,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 -> @@ -510,27 +511,27 @@ let remove_unused_valspecs env ast = in let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in - let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast in + let _ = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast in 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 @@ -542,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 @@ -553,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 @@ -570,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 -> () @@ -592,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 ddfb0c67..d2157323 100644 --- a/src/specialize.mli +++ b/src/specialize.mli @@ -51,6 +51,7 @@ (** Rewrites for removing polymorphism from specifications *) open Ast +open Ast_defs open Ast_util open Type_check @@ -72,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 defs -> IdSet.t +val polymorphic_functions : specialization -> 'a def list -> IdSet.t val add_initial_calls : IdSet.t -> unit @@ -81,14 +82,14 @@ val add_initial_calls : IdSet.t -> unit AST with [Type_check.initial_env]. The env parameter is the environment to return if there is no polymorphism to remove, in which case specialize returns the AST unmodified. *) -val specialize : specialization -> Env.t -> tannot defs -> tannot defs * Env.t +val specialize : specialization -> Env.t -> tannot ast -> tannot ast * Env.t (** specialize' n performs at most n specialization passes. Useful for int_specialization which is not guaranteed to terminate. *) -val specialize_passes : int -> specialization -> Env.t -> tannot defs -> tannot defs * Env.t +val specialize_passes : int -> specialization -> Env.t -> tannot ast -> tannot ast * Env.t (** return all instantiations of a function id, with the instantiations filtered according to the specialization. *) -val instantiations_of : specialization -> id -> tannot defs -> typ_arg KBindings.t list +val instantiations_of : specialization -> id -> tannot ast -> typ_arg KBindings.t list val string_of_instantiation : typ_arg KBindings.t -> string diff --git a/src/splice.ml b/src/splice.ml index dd19e664..478469a0 100644 --- a/src/splice.ml +++ b/src/splice.ml @@ -4,9 +4,10 @@ *) 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 @@ -18,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 -> @@ -35,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 @@ -45,10 +46,9 @@ let splice ast file = let parsed_ast = Process_file.parse_file file |> snd in 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_defs_annot (fun (l,_) -> l,Type_check.empty_tannot) repl_ast in - let repl_ids, repl_specs = scan_defs 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_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 8d487d3e..15475a36 100644 --- a/src/state.ml +++ b/src/state.ml @@ -53,6 +53,7 @@ module Big_int = Nat_big_num open Initial_check open Type_check open Ast +open Ast_defs open Ast_util open PPrint open Pretty_print_common @@ -60,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_defs (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 @@ -121,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 @@ -259,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. *) @@ -275,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) -> @@ -374,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 defs) = +let generate_isa_lemmas mwords defs = let rec drop_while f = function | x :: xs when f x -> drop_while f xs | xs -> xs @@ -552,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 30b93d90..fc5a18bd 100644 --- a/src/toFromInterp_backend.ml +++ b/src/toFromInterp_backend.ml @@ -49,6 +49,7 @@ (**************************************************************************) open Ast +open Ast_defs open Ast_util open PPrint open Type_check @@ -392,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) @@ -404,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 86bfc251..aeb9cf01 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -49,8 +49,9 @@ (**************************************************************************) open Ast -open Util +open Ast_defs open Ast_util +open Util open Lazy module Big_int = Nat_big_num @@ -5349,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" @@ -5419,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 defs * 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_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 : 'a. Env.t -> 'a defs -> tannot defs * Env.t = - fun env (Defs defs) -> let total = List.length defs in check_defs 1 total env defs +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 -and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list = +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 75c0d2a2..24825e25 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -51,6 +51,7 @@ (** The type checker API *) open Ast +open Ast_defs open Ast_util module Big_int = Nat_big_num @@ -479,8 +480,10 @@ Some invariants that will hold of a fully checked AST are: check throws type_errors rather than Sail generic errors from Reporting. For a function that uses generic errors, use Type_error.check *) -val check : Env.t -> 'a defs -> tannot defs * Env.t +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 1ac771bf..8b323714 100644 --- a/src/type_error.ml +++ b/src/type_error.ml @@ -50,6 +50,7 @@ open Util open Ast +open Ast_defs open Ast_util open Type_check @@ -185,7 +186,13 @@ let rec collapse_errors = function Err_because (err1, l, err2) | err -> err -let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = +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 | Type_error (env, l, err) -> diff --git a/test/latex/candperm.commands.tex.exp b/test/latex/candperm.commands.tex.exp index 14153396..0ba8e659 100644 --- a/test/latex/candperm.commands.tex.exp +++ b/test/latex/candperm.commands.tex.exp @@ -1,19 +1,24 @@ \providecommand\saildoclabelled[2]{\phantomsection\label{#1}#2} +\providecommand\saildocval[2]{#1 #2} +\providecommand\saildocfcl[2]{#1 #2} +\providecommand\saildoctype[2]{#1 #2} +\providecommand\saildocfn[2]{#1 #2} +\providecommand\saildocoverload[2]{#1 #2} -\newcommand{\sailtypeast}{\saildoclabelled{typezast}{\saildoctype{}{\lstinputlisting[language=sail]{out/typezast6bb070d12e82e4887160cdfd016230c8.tex}}}} +\newcommand{\sailtypeast}{\saildoclabelled{sailtypezast}{\saildoctype{}{\lstinputlisting[language=sail]{out/typezast6bb070d12e82e4887160cdfd016230c8.tex}}}} -\newcommand{\sailvalexecute}{\saildoclabelled{zexecute}{\saildocval{}{\lstinputlisting[language=sail]{out/valzexecute33a689e3a631b9b905b85461d3814943.tex}}}} +\newcommand{\sailvalexecute}{\saildoclabelled{sailzexecute}{\saildocval{}{\lstinputlisting[language=sail]{out/valzexecute33a689e3a631b9b905b85461d3814943.tex}}}} -\newcommand{\sailfclCAndPermBrokenexecute}{\saildoclabelled{fclCAndPermBrokenzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability +\newcommand{\sailfclCAndPermBrokenexecute}{\saildoclabelled{sailfclCAndPermBrokenzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability register \emph{cs1} with the \cperms{} field set to the bitwise-AND of its previous value and bits 0 .. 10 of integer register \emph{rs2} and the \cuperms{} field set to the bitwise and of its previous value -and bits \hyperref\hyperref[ztablezGpseudocodezDconstants]{\lstinline{table:pseudocode-constants}}{\emph{first\_uperm}} .. -\hyperref\hyperref[ztablezGpseudocodezDconstants]{\lstinline{table:pseudocode-constants}}{\emph{last\_uperm}} of \emph{rd}. +and bits \hyperref\hyperref[sailztablezGpseudocodezDconstants]{\lstinline{table:pseudocode-constants}}{\emph{first\_uperm}} .. +\hyperref\hyperref[sailztablezGpseudocodezDconstants]{\lstinline{table:pseudocode-constants}}{\emph{last\_uperm}} of \emph{rd}. }{\lstinputlisting[language=sail]{out/fclCAndPermBrokenzexecute33a689e3a631b9b905b85461d3814943.tex}}}} -\newcommand{\sailfclCAndPermEscapedexecute}{\saildoclabelled{fclCAndPermEscapedzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability +\newcommand{\sailfclCAndPermEscapedexecute}{\saildoclabelled{sailfclCAndPermEscapedzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability register \emph{cs1} with the \cperms{} field set to the bitwise-AND of its previous value and bits 0 .. 10 of integer register \emph{rs2} and the \cuperms{} field set to the bitwise and of its previous value @@ -22,7 +27,7 @@ and bits \hyperref[table:pseudocode-constants]{\emph{first\_uperm}} .. }{\lstinputlisting[language=sail]{out/fclCAndPermEscapedzexecute33a689e3a631b9b905b85461d3814943.tex}}}} -\newcommand{\sailfclCAndPermMarkdownexecute}{\saildoclabelled{fclCAndPermMarkdownzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability +\newcommand{\sailfclCAndPermMarkdownexecute}{\saildoclabelled{sailfclCAndPermMarkdownzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability register \emph{cs1} with the \cperms{} field set to the bitwise-AND of its previous value and bits 0 .. 10 of integer register \emph{rs2} and the \cuperms{} field set to the bitwise and of its previous value @@ -31,7 +36,7 @@ and bits \hyperref[table:pseudocode-constants]{*first_uperm*} .. }{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownzexecute33a689e3a631b9b905b85461d3814943.tex}}}} -\newcommand{\sailfclCAndPermMarkdownWithRefMacroexecute}{\saildoclabelled{fclCAndPermMarkdownWithRefMacrozexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability +\newcommand{\sailfclCAndPermMarkdownWithRefMacroexecute}{\saildoclabelled{sailfclCAndPermMarkdownWithRefMacrozexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability register \emph{cs1} with the \cperms{} field set to the bitwise-AND of its previous value and bits 0 .. 10 of integer register \emph{rs2} and the \cuperms{} field set to the bitwise and of its previous value @@ -39,7 +44,7 @@ and bits \firstUPerm{} .. \lastUPerm{} of \emph{rd}. }{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownWithRefMacrozexecute33a689e3a631b9b905b85461d3814943.tex}}}} -\newcommand{\sailfclCAndPermMarkdownWithExceptionsexecute}{\saildoclabelled{fclCAndPermMarkdownWithExceptionszexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability +\newcommand{\sailfclCAndPermMarkdownWithExceptionsexecute}{\saildoclabelled{sailfclCAndPermMarkdownWithExceptionszexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability register \emph{cs1} with the \cperms{} field set to the bitwise-AND of its previous value and bits 0 .. 10 of integer register \emph{rs2} and the \cuperms{} field set to the bitwise and of its previous value @@ -60,7 +65,7 @@ An exception is raised if: \ifstrequal{#1}{execute}{\sailvalexecute}{}} \newcommand{\sailrefval}[2]{ - \ifstrequal{#1}{execute}{\hyperref[zexecute]{#2}}{}} + \ifstrequal{#1}{execute}{\hyperref[sailzexecute]{#2}}{}} \newcommand{\sailfn}[1]{ } @@ -72,4 +77,4 @@ An exception is raised if: \ifstrequal{#1}{ast}{\sailtypeast}{}} \newcommand{\sailreftype}[2]{ - \ifstrequal{#1}{ast}{\hyperref[typezast]{#2}}{}} + \ifstrequal{#1}{ast}{\hyperref[sailtypezast]{#2}}{}} diff --git a/test/latex/main.tex b/test/latex/main.tex new file mode 100644 index 00000000..a0948482 --- /dev/null +++ b/test/latex/main.tex @@ -0,0 +1,44 @@ +\documentclass{article} +\usepackage{etoolbox} +\usepackage{hyperref} +\usepackage{xcolor} +\usepackage{listings} +\lstdefinelanguage{sail} + { morekeywords={val,function,mapping,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof, + scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct, + foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw,constraint}, + keywordstyle={\bf\ttfamily\color{blue}}, + morestring=[b]", + stringstyle={\ttfamily\color{red}}, + morecomment=[l][\itshape\color{DarkGreen}]{//}, + morecomment=[s][\itshape\color{DarkGreen}]{/*}{*/}, + deletestring=[bd]{'}, + escapechar=\#, + emphstyle={\it}, + literate= + {\{|}{{$\{|$}}1 + {|\}}{{$|\}$}}1 + } + +\input{out/commands.tex} +\begin{document} + +\clearpage +type: \sailtype{cap\_uperms\_width} + +\clearpage +ref type: \sailreftype{cap\_uperms\_width}{ref to cap\_uperms\_width} + +\clearpage +val: \sailval{main} + +\clearpage +refval: \sailrefval{main}{ref to main} + +\clearpage +\sailfn{main} + +\clearpage +reffn: \sailreffn{main}{ref to main} + +\end{document} diff --git a/test/latex/reference-type.commands.tex.exp b/test/latex/reference-type.commands.tex.exp new file mode 100644 index 00000000..3c8c80ab --- /dev/null +++ b/test/latex/reference-type.commands.tex.exp @@ -0,0 +1,54 @@ +\providecommand\saildoclabelled[2]{\phantomsection\label{#1}#2} +\providecommand\saildocval[2]{#1 #2} +\providecommand\saildocfcl[2]{#1 #2} +\providecommand\saildoctype[2]{#1 #2} +\providecommand\saildocfn[2]{#1 #2} +\providecommand\saildocoverload[2]{#1 #2} + +\newcommand{\sailtypecapUpermsWidth}{\saildoclabelled{sailtypezcapzyupermszywidth}{\saildoctype{}{\lstinputlisting[language=sail]{out/typezcap_uperms_widthf6dfed0942499b0c2d58b90971faca40.tex}}}} + +\newcommand{\sailvalmain}{\saildoclabelled{sailzmain}{\saildocval{}{\lstinputlisting[language=sail]{out/valzmaine3ee21bf8f1dbb3fd716a5a1803d7e24.tex}}}} + +\newcommand{\sailfnmain}{\saildoclabelled{sailfnzmain}{\saildocfn{\begin{itemize} +\item Ref to \hyperref[sailzcapzyupermszywidth]{\lstinline{cap_uperms_width}} +\item Ref to \hyperref[sailzcapzyupermszywidth]{description} +\item Ref to \hyperref[sailztypez0capzyupermszywidth]{type description} +\item Ref to % FIXME: this should be using type\_description \hyperref[sailztypezycapzyupermszywidth]{type_description} +\item Ref to \sailreftype{cap\_uperms\_width}{uperms\_width} +\item Ref to \sailreftype{cap\_uperms\_width}{uperms\_width} +\end{itemize} +}{\lstinputlisting[language=sail]{out/fnzmaine3ee21bf8f1dbb3fd716a5a1803d7e24.tex}}}} + +\newcommand{\sailvalfunctionWithUnderscores}{\saildoclabelled{sailzfunctionzywithzyunderscores}{\saildocval{}{\lstinputlisting[language=sail]{out/valzfunction_with_underscores6e195bff96b3fe3d60b356f28519989f.tex}}}} + +\newcommand{\sailfnfunctionWithUnderscores}{\saildoclabelled{sailfnzfunctionzywithzyunderscores}{\saildocfn{\begin{itemize} +\item \hyperref[sailzfunction\_with\_underscores]{\lstinline{function\_with\_underscores}} +\item \hyperref[sailzfunctionzywithzyunderscores]{\lstinline{function_with_underscores}} +\item \hyperref[sailzNOTz0function\_with\_underscores]{function\_with\_underscores} +\item \hyperref[sailzNOTz0\lstinline{function_with_underscores}]{\lstinline{function_with_underscores}} +\item \hyperref[sailzfunction\_with\_underscores]{NOT function\_with\_underscores} +\item \hyperref[sailzfunctionzywithzyunderscores]{NOT \lstinline{function_with_underscores}} +\end{itemize} +}{\lstinputlisting[language=sail]{out/fnzfunction_with_underscores6e195bff96b3fe3d60b356f28519989f.tex}}}} + +\newcommand{\sailval}[1]{ + \ifstrequal{#1}{function\_with\_underscores}{\sailvalfunctionWithUnderscores}{}% + \ifstrequal{#1}{main}{\sailvalmain}{}} + +\newcommand{\sailrefval}[2]{ + \ifstrequal{#1}{function_with_underscores}{\hyperref[sailzfunctionzywithzyunderscores]{#2}}{}% + \ifstrequal{#1}{main}{\hyperref[sailzmain]{#2}}{}} + +\newcommand{\sailfn}[1]{ + \ifstrequal{#1}{function\_with\_underscores}{\sailfnfunctionWithUnderscores}{}% + \ifstrequal{#1}{main}{\sailfnmain}{}} + +\newcommand{\sailreffn}[2]{ + \ifstrequal{#1}{function_with_underscores}{\hyperref[sailfnzfunctionzywithzyunderscores]{#2}}{}% + \ifstrequal{#1}{main}{\hyperref[sailfnzmain]{#2}}{}} + +\newcommand{\sailtype}[1]{ + \ifstrequal{#1}{cap\_uperms\_width}{\sailtypecapUpermsWidth}{}} + +\newcommand{\sailreftype}[2]{ + \ifstrequal{#1}{cap_uperms_width}{\hyperref[sailtypezcapzyupermszywidth]{#2}}{}} diff --git a/test/latex/reference-type.sail b/test/latex/reference-type.sail new file mode 100644 index 00000000..d41ae10f --- /dev/null +++ b/test/latex/reference-type.sail @@ -0,0 +1,27 @@ +default Order dec + +$include <flow.sail> +$include <vector_dec.sail> + +type cap_uperms_width : Int = 4 +let cap_uperms_width = sizeof(cap_uperms_width) + +/*! + * - Ref to [cap_uperms_width] + * - Ref to [description][cap_uperms_width] + * - Ref to [type description][type cap_uperms_width] + * - Ref to % FIXME: this should be using type\_description [type_description][type_cap_uperms_width] + * - Ref to \sailreftype{cap_uperms_width}{uperms\_width} + * - Ref to \sailreftype{cap\_uperms\_width}{uperms\_width} + */ +function main() -> unit = return(()) + +/*! + * - [NAME] + * - [THIS] + * - [NAME][NOT NAME] + * - [THIS][NOT THIS] + * - [NOT NAME][NAME] + * - [NOT THIS][THIS] + */ +function function_with_underscores() -> unit = return(()) diff --git a/test/latex/run_tests.sh b/test/latex/run_tests.sh index 6ba3ce6f..17edb567 100755 --- a/test/latex/run_tests.sh +++ b/test/latex/run_tests.sh @@ -26,7 +26,6 @@ for testfile in *.sail; do exp_prefix=${testfile//.sail/} errmsg="Missing .exp files for $testfile?" for expected in "${exp_prefix}"*.exp; do - echo "expected=$expected" # remove prefix and suffix exp_file_name=${expected//${exp_prefix}./} generated_file="$temp_dir/out/${exp_file_name//.exp/}" @@ -42,10 +41,22 @@ for testfile in *.sail; do fi done if [ -z "$errmsg" ]; then - green "LaTeX for $testfile" "ok" + green "Generating LaTeX for $testfile" "ok" else - yellow "LaTeX for $testfile" "$errmsg" + yellow "Generating LaTeX for $testfile" "$errmsg" fi; + # Check that the generated latex builds: + if command -v latexmk > /dev/null; then + cp -f "$DIR/main.tex" "$temp_dir" + if latexmk -pdf -cd -file-line-error -interaction=batchmode "$temp_dir/main.tex" > /dev/null 2>&1; then + green "Building LaTeX for $testfile" "ok" + else + tail -n 50 "$temp_dir/main.log" + yellow "Building LaTeX for $testfile" "failed to build" + fi + else + red "Building LaTeX for $testfile" "latexmk not installed" + fi else red "failed to generate latex for $testfile" "fail" fi |