Add simple conditional processing and file include

Can now use C-style include declarations to include files within other sail files. This is done in such a way that all the location information is preserved in error messages. As an example:

$include "aarch64/prelude.sail"
$define SYM
$ifndef SYM
$include <../util.sail>
$endif

would include the file aarch64/prelude.sail relative to the file where the include is contained. It then defines a symbol SYM and includes another file if it is not defined. The <../util.sail> include will be accessed relative to $SAIL_DIR/lib, so $SAIL_DIR/lib/../util.sail in this case.

This can be used with the standard C trick of

$ifndef ONCE
$define ONCE
val f : unit -> unit
$endif

so no matter how many sail files include the above file, the valspec for f will only appear once.

Currently we just have $include, $define, $ifdef and $ifndef (with $else and $endif). We're using $ rather than # because # is already used in internal identifiers, although this could be switched.

9 files changed, 107 insertions, 4 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 87adb290..16df4648 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -826,9 +826,11 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
   | Parse_ast.DEF_reg_dec(dec) ->
     let d = to_ast_dec envs dec in
     ((Finished(DEF_reg_dec(d))),envs),partial_defs
+  | Parse_ast.DEF_pragma (_, _, l) ->
+     typ_error l "Encountered preprocessor directive in initial check" None None None
   | Parse_ast.DEF_internal_mutrec _ ->
      (* Should never occur because of remove_mutrec *)
-    typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None
+     typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None
   | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) ->
     (match sd with
     | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
diff --git a/src/lexer.mll b/src/lexer.mll
index 21b70c5f..77fba70b 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -186,9 +186,10 @@ let alphanum = letter|digit
 let startident = letter|'_'
 let ident = alphanum|['_''\'''#']
 let tyvar_start = '\''
-let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''@''^''|']
+let oper_char = ['!''%''&''*''+''-''.''/'':''<''=''>''@''^''|']
 let operator = (oper_char+ ('_' ident)?)
 let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
+let lchar = [^'\n']
 
 rule token = parse
   | ws
@@ -236,6 +237,8 @@ rule token = parse
   | "//"        { line_comment (Lexing.lexeme_start_p lexbuf) lexbuf; token lexbuf }
   | "/*"        { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
   | "*/"        { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
+  | "$" (ident+ as i) (lchar* as f) "\n"
+    { Lexing.new_line lexbuf; Pragma(i, String.trim f) }
   | "infix" ws (digit as p) ws (operator as op)
     { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators;
       Fixity (Infix, Big_int.of_string (Char.escaped p), op) }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 362333f3..5eb8038a 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -507,6 +507,7 @@ def =  (* Top-level definition *)
  | DEF_default of default_typing_spec (* default kind and type assumptions *)
  | DEF_scattered of scattered_def (* scattered definition *)
  | DEF_reg_dec of dec_spec (* register declaration *)
+ | DEF_pragma of string * string * l
  | DEF_internal_mutrec of fundef list
 
 
diff --git a/src/parser.mly b/src/parser.mly
index b11b4b61..32ee3368 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -182,6 +182,8 @@ let rec desugar_rchain chain s e =
 %token <string> Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l
 %token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
 
+%token <string * string> Pragma
+
 %token <Parse_ast.fixity_token> Fixity
 
 %start file
@@ -1246,6 +1248,8 @@ def:
     { DEF_default $1 }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
+  | Pragma
+    { DEF_pragma (fst $1, snd $1, loc $startpos $endpos) }
 
 defs_list:
   | def
diff --git a/src/process_file.ml b/src/process_file.ml
index ec280fbf..cb8c8011 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -76,12 +76,99 @@ let parse_file (f : string) : Parse_ast.defs =
     | Lexer.LexError(s,p) ->
        raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
 
+(* Simple preprocessor features for conditional file loading *)
+module StringSet = Set.Make(String)
+
+let symbols = ref StringSet.empty
+
+let cond_pragma defs =
+  let depth = ref 0 in
+  let in_then = ref true in
+  let then_defs = ref [] in
+  let else_defs = ref [] in
+
+  let push_def def =
+    if !in_then then
+      then_defs := (def :: !then_defs)
+    else
+      else_defs := (def :: !else_defs)
+  in
+  
+  let rec scan = function
+    | Parse_ast.DEF_pragma ("endif", _, _) :: defs when !depth = 0 ->
+       (List.rev !then_defs, List.rev !else_defs, defs)
+    | Parse_ast.DEF_pragma ("else", _, _) :: defs when !depth = 0 ->
+       in_then := false; scan defs
+    | (Parse_ast.DEF_pragma (p, _, _) as def) :: defs when p = "ifdef" || p = "ifndef" ->
+       incr depth; push_def def; scan defs
+    | (Parse_ast.DEF_pragma ("endif", _, _) as def) :: defs->
+       decr depth; push_def def; scan defs
+    | def :: defs ->
+       push_def def; scan defs
+    | [] -> failwith "$ifdef or $ifndef never ended"
+  in
+  scan defs
+         
+let rec preprocess = function
+  | [] -> []
+  | Parse_ast.DEF_pragma ("define", symbol, _) :: defs ->
+     symbols := StringSet.add symbol !symbols;
+     preprocess defs
+                
+  | Parse_ast.DEF_pragma ("ifndef", symbol, _) :: defs ->
+     let then_defs, else_defs, defs = cond_pragma defs in
+     if not (StringSet.mem symbol !symbols) then
+       preprocess (then_defs @ defs)
+     else
+       preprocess (else_defs @ defs)
+
+  | Parse_ast.DEF_pragma ("ifdef", symbol, _) :: defs ->
+     let then_defs, else_defs, defs = cond_pragma defs in
+     if StringSet.mem symbol !symbols then
+       preprocess (then_defs @ defs)
+     else
+       preprocess (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)
+     else if file.[0] = '"' && file.[len - 1] = '"' then
+       let relative = match l with
+         | Parse_ast.Range (pos, _) -> Filename.dirname (Lexing.(pos.pos_fname))
+         | _ -> failwith "Couldn't figure out relative path for $include. This really shouldn't ever happen."
+       in
+       let file = String.sub file 1 (len - 2) in
+       let (Parse_ast.Defs include_defs) = parse_file (Filename.concat relative file) in
+       let include_defs = preprocess include_defs in
+       include_defs @ preprocess defs
+     else if file.[0] = '<' && file.[len - 1] = '>' then
+       let file = String.sub file 1 (len - 2) in
+       let sail_dir =
+         try Sys.getenv "SAIL_DIR" with
+         | Not_found -> (failwith ("Environment variable SAIL_DIR unset. Cannot $include " ^ file))
+       in
+       let file = Filename.concat sail_dir ("lib/" ^ file) in
+       let (Parse_ast.Defs include_defs) = parse_file file in
+       let include_defs = preprocess include_defs in
+       include_defs @ preprocess 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)
+
+  | Parse_ast.DEF_pragma (p, arg, _) :: defs ->
+     (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess defs) 
+         
+  | def :: defs -> def :: preprocess defs
+
+let preprocess_ast (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess 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 (parse_file f)
+let load_file_no_check order f = convert_ast order (preprocess_ast (parse_file f))
 
 let load_file order env f =
-  let ast = convert_ast order (parse_file f) in
+  let ast = convert_ast order (preprocess_ast (parse_file f)) in
   Type_check.check env ast
 
 let opt_just_check = ref false
diff --git a/src/process_file.mli b/src/process_file.mli
index 82fe1cf7..d8094682 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -50,6 +50,7 @@
 
 val parse_file : 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 check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
 val monomorphise_ast : ((string * int) * string) list -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
 val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
diff --git a/src/sail.ml b/src/sail.ml
index b819350b..d5ef684b 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -193,6 +193,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 = convert_ast Ast_util.inc_ord ast in
 
   let (ast, type_envs) = check_ast type_envs ast in
diff --git a/src/util.ml b/src/util.ml
index 94bbc6dc..6d4b3726 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -413,3 +413,5 @@ let zchar c =
 let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str))
 
 let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str))
+
+let warn str = prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str)
diff --git a/src/util.mli b/src/util.mli
index 8fcf68be..c9eae02f 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -240,5 +240,7 @@ val cyan : string -> string
 val blue : string -> string
 val clear : string -> string
 
+val warn : string -> unit
+                        
 val zencode_string : string -> string
 val zencode_upper_string : string -> string