From b04f8c9dfa599b48544bac024eaa78e6b93c29d4 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 6 Sep 2018 14:26:36 +0100 Subject: Allow options to be set in the interactive mode Also allow options to be set via a pragma in Sail files --- src/isail.ml | 12 +++++++++++- src/process_file.ml | 55 +++++++++++++++++++++++++++++++--------------------- src/process_file.mli | 6 +++--- src/sail.ml | 2 +- 4 files changed, 48 insertions(+), 27 deletions(-) (limited to 'src') diff --git a/src/isail.ml b/src/isail.ml index 84b614a9..c3f869a3 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -194,6 +194,8 @@ let help = function "(:u | :unload) - Unload all loaded files." | ":output" -> ":output - Redirect evaluating expression output to a file." + | ":option" -> + ":option string - Parse string as if it was an option passed on the command line. Try :option -help." | cmd -> "Either invalid command passed to help, or no documentation for " ^ cmd ^ ". Try :help :help." @@ -253,7 +255,7 @@ let handle_input' input = else print_endline "Invalid argument for :clear, expected either :clear on or :clear off" | ":commands" -> let commands = - [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :clear :commands :help :output"; + [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :clear :commands :help :output :option"; "Normal mode commands - :elf :(l)oad :(u)nload"; "Evaluation mode commands - :(r)un :(s)tep :(n)ormal"; ""; @@ -269,6 +271,14 @@ let handle_input' input = in let ids = Specialize.polymorphic_functions is_kopt !interactive_ast in List.iter (fun id -> print_endline (string_of_id id)) (IdSet.elements ids) + | ":option" -> + begin + try + let args = Str.split (Str.regexp " +") arg in + Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) Sail.options (fun _ -> ()) ""; + with + | Arg.Bad message | Arg.Help message -> print_endline message + end; | ":spec" -> let ast, env = Specialize.specialize !interactive_ast !interactive_env in interactive_ast := ast; diff --git a/src/process_file.ml b/src/process_file.ml index 974c9a0c..096c4151 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -137,30 +137,41 @@ let rec realise_union_anon_rec_types (Parse_ast.TD_variant (union_id, name_scm_o let new_rec_def = DEF_type (TD_aux (TD_record (record_id, name_scm_opt, typq, fields, flag), Generated l)) in (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms) -let rec preprocess = function +let rec preprocess opts = function | [] -> [] | Parse_ast.DEF_pragma ("define", symbol, _) :: defs -> symbols := StringSet.add symbol !symbols; - preprocess defs + preprocess opts defs + + | Parse_ast.DEF_pragma ("option", command, l) :: defs -> + begin + try + let args = Str.split (Str.regexp " +") command in + Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) opts (fun _ -> ()) ""; + with + | Arg.Bad message | Arg.Help message -> raise (Reporting_basic.err_general l message) + end; + preprocess opts defs + | Parse_ast.DEF_pragma ("ifndef", symbol, l) :: defs -> let then_defs, else_defs, defs = cond_pragma l defs in if not (StringSet.mem symbol !symbols) then - preprocess (then_defs @ defs) + preprocess opts (then_defs @ defs) else - preprocess (else_defs @ defs) + preprocess opts (else_defs @ defs) | Parse_ast.DEF_pragma ("ifdef", symbol, l) :: defs -> let then_defs, else_defs, defs = cond_pragma l defs in if StringSet.mem symbol !symbols then - preprocess (then_defs @ defs) + preprocess opts (then_defs @ defs) else - preprocess (else_defs @ defs) + preprocess opts (else_defs @ defs) | Parse_ast.DEF_pragma ("include", file, l) :: defs -> let len = String.length file in if len = 0 then - (Util.warn "Skipping bad $include. No file argument."; preprocess defs) + (Util.warn "Skipping bad $include. No file argument."; preprocess opts defs) else if file.[0] = '"' && file.[len - 1] = '"' then let relative = match l with | Parse_ast.Range (pos, _) -> Filename.dirname (Lexing.(pos.pos_fname)) @@ -168,8 +179,8 @@ let rec preprocess = function in let file = String.sub file 1 (len - 2) in let (Parse_ast.Defs include_defs) = parse_file ~loc:l (Filename.concat relative file) in - let include_defs = preprocess include_defs in - include_defs @ preprocess defs + let include_defs = preprocess opts include_defs in + include_defs @ preprocess opts defs else if file.[0] = '<' && file.[len - 1] = '>' then let file = String.sub file 1 (len - 2) in let sail_dir = @@ -183,14 +194,14 @@ let rec preprocess = function in let file = Filename.concat sail_dir ("lib/" ^ file) in let (Parse_ast.Defs include_defs) = parse_file ~loc:l file in - let include_defs = preprocess include_defs in - include_defs @ preprocess defs + let include_defs = preprocess opts include_defs in + include_defs @ preprocess opts defs else let help = "Make sure the filename is surrounded by quotes or angle brackets" in - (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess defs) + (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs) | Parse_ast.DEF_pragma (p, arg, _) :: defs -> - (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess defs) + (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess opts defs) (* realise any anonymous record arms of variants *) | Parse_ast.DEF_type (Parse_ast.TD_aux @@ -204,25 +215,25 @@ let rec preprocess = function let generated_records = filter_records (List.map fst records_and_arms) in let rewritten_arms = List.map snd records_and_arms in let rewritten_union = Parse_ast.TD_variant (id, name_scm_opt, typq, rewritten_arms, flag) in - generated_records @ (Parse_ast.DEF_type (Parse_ast.TD_aux (rewritten_union, l))) :: preprocess defs + generated_records @ (Parse_ast.DEF_type (Parse_ast.TD_aux (rewritten_union, l))) :: preprocess opts defs | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs -> begin match atyp with - | Parse_ast.ATyp_inc -> symbols := StringSet.add "_DEFAULT_INC" !symbols; def :: preprocess defs - | Parse_ast.ATyp_dec -> symbols := StringSet.add "_DEFAULT_DEC" !symbols; def :: preprocess defs - | _ -> def :: preprocess defs + | Parse_ast.ATyp_inc -> symbols := StringSet.add "_DEFAULT_INC" !symbols; def :: preprocess opts defs + | Parse_ast.ATyp_dec -> symbols := StringSet.add "_DEFAULT_DEC" !symbols; def :: preprocess opts defs + | _ -> def :: preprocess opts defs end - | def :: defs -> def :: preprocess defs + | def :: defs -> def :: preprocess opts defs -let preprocess_ast (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess defs) +let preprocess_ast opts (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess opts defs) let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs -let load_file_no_check order f = convert_ast order (preprocess_ast (parse_file f)) +let load_file_no_check opts order f = convert_ast order (preprocess_ast opts (parse_file f)) -let load_file order env f = - let ast = convert_ast order (preprocess_ast (parse_file f)) in +let load_file opts order env f = + let ast = convert_ast order (preprocess_ast opts (parse_file f)) in Type_error.check env ast let opt_just_check = ref false diff --git a/src/process_file.mli b/src/process_file.mli index 8fdf9653..1ebb3014 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -53,7 +53,7 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs -val preprocess_ast : Parse_ast.defs -> Parse_ast.defs +val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_undefined: bool -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs @@ -64,8 +64,8 @@ val rewrite_ast_c : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs -val load_file_no_check : Ast.order -> string -> unit Ast.defs -val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t +val load_file_no_check : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> string -> unit Ast.defs +val load_file : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t val opt_just_check : bool ref val opt_ddump_tc_ast : bool ref diff --git a/src/sail.ml b/src/sail.ml index de186be9..ba19eb79 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -259,7 +259,7 @@ let load_files type_envs files = let ast = List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes) -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in - let ast = Process_file.preprocess_ast ast in + let ast = Process_file.preprocess_ast options ast in let ast = convert_ast Ast_util.inc_ord ast in let (ast, type_envs) = check_ast type_envs ast in -- cgit v1.2.3