Add support for the -I parameter to jasmin2ec, jasmin-ct and jasmin2tex.

compiler/entry/commonCLI.ml

@@ -39,6 +39,14 @@ let call_conv =
     & opt call_conv Glob_options.Linux
     & info [ "call-conv"; "cc" ] ~docv:"OS" ~doc)
 
+let idirs =
+  let doc =
+    "Bind ident to path for 'from ident require ...'"
+  in
+  let info = Arg.info [ "I" ] ~docv:"ident:path" ~doc in
+  let conv = Arg.pair ~sep:':' Arg.string Arg.dir in
+  Arg.value (Arg.opt_all conv [] info)
+
 let warn =
   let doc = "Print warnings" in
   Arg.(value & flag & info [ "warn" ] ~doc)
@@ -65,9 +73,9 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op)
        and type rflag = rflag
        and type cond = cond
        and type asm_op = asm_op
-       and type extra_op = extra_op) pass file =
+       and type extra_op = extra_op) pass file idirs =
   let _env, pprog, _ast =
-    try Compile.parse_file Arch.arch_info file with
+    try Compile.parse_file Arch.arch_info file idirs with
     | Annot.AnnotationError (loc, code) ->
         hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code
     | Pretyping.TyError (loc, code) ->

compiler/entry/commonCLI.mli

@@ -4,6 +4,7 @@ open Cmdliner
 val get_arch_module : Utils.architecture -> Glob_options.call_conv -> (module Arch_full.Arch)
 val arch : Utils.architecture Term.t
 val call_conv : Glob_options.call_conv Term.t
+val idirs : (string * string) list Term.t
 val warn : bool Term.t
 val after_pass : Compiler.compiler_step Term.t
 
@@ -18,6 +19,7 @@ val parse_and_compile :
       and type xreg = 'xreg) ->
   Compiler.compiler_step ->
   string ->
+  (string * string) list ->
   ( unit,
     ( 'reg,
       'regx,

compiler/entry/jasmin2ec.ml

@@ -32,11 +32,11 @@ let extract_to_file prog arch pd asmOp model amodel fnames array_dir outfile =
 
 
 
-let parse_and_extract arch call_conv =
+let parse_and_extract arch call_conv idirs =
   let module A = (val get_arch_module arch call_conv) in
 
   let extract model amodel functions array_dir output pass file =
-    let prog = parse_and_compile (module A) pass file in
+    let prog = parse_and_compile (module A) pass file (idirs @ Glob_options.env_idirs) in
 
     extract_to_file prog arch A.reg_size A.asmOp model amodel functions
       array_dir output
@@ -122,6 +122,6 @@ let () =
   in
   Cmd.v info
     Term.(
-      const parse_and_extract $ arch $ call_conv $ model $ array_model
+      const parse_and_extract $ arch $ call_conv $ idirs $ model $ array_model
       $ functions $ array_dir $ output $ after_pass $ file $ warn)
   |> Cmd.eval |> exit

compiler/entry/jasmin2tex.ml

@@ -3,10 +3,10 @@ open Cmdliner
 open CommonCLI
 open Utils
 
-let parse_and_print arch call_conv =
+let parse_and_print arch call_conv idirs =
   let module A = (val get_arch_module arch call_conv) in
   let parse file =
-    try Compile.parse_file A.arch_info file with
+    try Compile.parse_file A.arch_info file (idirs @ Glob_options.env_idirs) with
     | Annot.AnnotationError (loc, code) ->
         hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code
     | Pretyping.TyError (loc, code) ->
@@ -54,6 +54,6 @@ let () =
   let info =
     Cmd.info "jasmin2tex" ~version:Glob_options.version_string ~doc ~man
   in
-  Cmd.v info Term.(const parse_and_print $ arch $ call_conv $ output $ file
+  Cmd.v info Term.(const parse_and_print $ arch $ call_conv $ idirs $ output $ file
     $ warn)
   |> Cmd.eval |> exit

compiler/entry/jasmin_ct.ml

@@ -3,10 +3,10 @@ open Cmdliner
 open CommonCLI
 open Utils
 
-let parse_and_check arch call_conv =
+let parse_and_check arch call_conv idirs =
   let module A = (val get_arch_module arch call_conv) in
   let check ~doit infer ct_list speculative pass file =
-    let prog = parse_and_compile (module A) pass file in
+    let prog = parse_and_compile (module A) pass file (idirs @ Glob_options.env_idirs) in
 
     if speculative then
       let prog =
@@ -88,6 +88,6 @@ let () =
   in
   Cmd.v info
     Term.(
-      const parse_and_check $ arch $ call_conv $ infer $ slice $ speculative
+      const parse_and_check $ arch $ call_conv $ idirs $ infer $ slice $ speculative
       $ after_pass $ file $ doit $ warn)
   |> Cmd.eval |> exit

compiler/src/compile.ml

@@ -11,11 +11,8 @@ let preprocess reg_size asmOp p =
 
 (* -------------------------------------------------------------------- *)
 
-let parse_file arch_info fname =
-  let env =
-    List.fold_left Pretyping.Env.add_from Pretyping.Env.empty
-      !Glob_options.idirs
-  in
+let parse_file arch_info fname idirs =
+  let env = List.fold_left Pretyping.Env.add_from Pretyping.Env.empty idirs in
   Pretyping.tt_program arch_info env fname
 
 (* -------------------------------------------------------------------- *)

compiler/src/compile.mli

@@ -15,6 +15,7 @@ val preprocess : wsize -> 'asm asmOp -> (unit, 'asm) pprog -> (unit, 'asm) prog
 val parse_file :
   ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Pretyping.arch_info ->
   string ->
+  (string * string) list ->
   ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op
   Pretyping.Env.env
   * ( unit,

compiler/src/glob_options.ml

@@ -99,8 +99,9 @@ let set_color c =
 let parse_jasmin_path s =
   s |> String.split_on_char ':' |> List.map (String.split ~by:"=")
 
-let idirs =
-  ref (try "JASMINPATH" |> Sys.getenv |> parse_jasmin_path with _ -> [])
+let env_idirs = try "JASMINPATH" |> Sys.getenv |> parse_jasmin_path with _ -> []
+
+let idirs = ref (env_idirs)
 
 let set_idirs s = 
   match String.split_on_char ':' s with

compiler/src/main_compiler.ml

@@ -114,7 +114,7 @@ let main () =
         | None -> () in
 
     let env, pprog, _ast =
-      try Compile.parse_file Arch.arch_info infile
+      try Compile.parse_file Arch.arch_info infile !Glob_options.idirs
       with
       | Annot.AnnotationError (loc, code) -> hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code
       | Pretyping.TyError (loc, code) -> hierror ~loc:(Lone loc) ~kind:"typing error" "%a" Pretyping.pp_tyerror code