Allow options to be set in the interactive mode

Also allow options to be set via a pragma in Sail files

4 files changed, 48 insertions, 27 deletions

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 <file> - 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