Merge branch 'latex' into sail2

13 files changed, 417 insertions, 115 deletions

diff --git a/src/_tags b/src/_tags
index c5f4e127..826e87a5 100644
--- a/src/_tags
+++ b/src/_tags
@@ -1,11 +1,12 @@
 true: -traverse, debug, use_menhir
 <**/*.ml>: bin_annot, annot
 
-<sail.{byte,native}>: package(zarith), package(linksem), package(lem), use_pprint
-<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), use_pprint
+<sail.{byte,native}>: package(zarith), package(linksem), package(lem), package(omd), use_pprint
+<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), package(omd), use_pprint
 
 <isail.ml>: package(linenoise)
 <elf_loader.ml>: package(linksem)
+<latex.ml>: package(omd)
 <**/*.m{l,li}>: package(lem)
 
 <gen_lib>: include
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 037fd1a7..d61c96ed 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -296,7 +296,10 @@ let rec constraint_simp (NC_aux (nc_aux, l)) =
        | NC_aux (nc, _), NC_aux (NC_true, _) -> NC_true
        | _, _ -> NC_or (nc1, nc2)
        end
-
+    | NC_bounded_ge (nexp1, nexp2) ->
+       NC_bounded_ge (nexp_simp nexp1, nexp_simp nexp2)
+    | NC_bounded_le (nexp1, nexp2) ->
+       NC_bounded_le (nexp_simp nexp1, nexp_simp nexp2)
     | _ -> nc_aux
   in
   NC_aux (nc_aux, l)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 897f3ec2..4dd72980 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -920,8 +920,8 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
      let kids = List.map to_ast_var kids in
      let nc = to_ast_nexp_constraint k_env nc in
      ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs
-  | Parse_ast.DEF_pragma (_, _, l) ->
-     typ_error l "Encountered preprocessor directive in initial check" None None None
+  | Parse_ast.DEF_pragma (pragma, arg, l) ->
+     ((Finished(DEF_pragma (pragma, arg, l))), envs), partial_defs
   | 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
diff --git a/src/isail.ml b/src/isail.ml
index 7ec0848d..55f08f17 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -285,7 +285,7 @@ let handle_input' input =
             interactive_env := env;
             interactive_state := initial_state !interactive_ast Value.primops
          | ":pretty" ->
-            print_endline (Pretty_print_sail.to_string (Latex.latex_defs "sail_latex" !interactive_ast))
+            print_endline (Pretty_print_sail.to_string (Latex.defs !interactive_ast))
          | ":bytecode" ->
             let open PPrint in
             let open C_backend in
diff --git a/src/latex.ml b/src/latex.ml
index 4944c5e9..2f578f2c 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -51,51 +51,223 @@
 open Ast
 open Ast_util
 open PPrint
+open Printf
 
-let opt_prefix_latex = ref "sail"
+module StringSet = Set.Make(String);;
+
+let opt_prefix = ref "sail"
+let opt_directory = ref "sail_latex"
+
+let rec unique_postfix n =
+  if n < 0 then
+    ""
+  else if n >= 26 then
+    String.make 1 (Char.chr (n mod 26 + 65)) ^ unique_postfix (n - 26)
+  else
+    String.make 1 (Char.chr (n mod 26 + 65))
+
+type latex_state =
+  { mutable noindent : bool;
+    mutable this : id option;
+    mutable norefs : StringSet.t;
+    mutable generated_names : string Bindings.t
+  }
+
+let reset_state state =
+  state.noindent <- false;
+  state.this <- None;
+  state.norefs <- StringSet.empty;
+  state.generated_names <- Bindings.empty
+
+let state =
+  { noindent = false;
+    this = None;
+    norefs = StringSet.empty;
+    generated_names = Bindings.empty
+  }
+
+let rec unique_postfix n =
+  if n < 0 then
+    ""
+  else if n >= 26 then
+    String.make 1 (Char.chr (n mod 26 + 65)) ^ unique_postfix (n - 26)
+  else
+    String.make 1 (Char.chr (n mod 26 + 65))
+
+type id_category =
+  | Function
+  | Val
+  | Overload
+  | FunclCtor of id * int
+  | FunclNum of int
+  | FunclApp of string
 
 let replace_numbers str =
-  str
-  |> Str.global_replace (Str.regexp "0") "zero"
-  |> Str.global_replace (Str.regexp "1") "one"
-  |> Str.global_replace (Str.regexp "2") "two"
-  |> Str.global_replace (Str.regexp "3") "three"
-  |> Str.global_replace (Str.regexp "4") "four"
-  |> Str.global_replace (Str.regexp "5") "five"
-  |> Str.global_replace (Str.regexp "6") "six"
-  |> Str.global_replace (Str.regexp "7") "seven"
-  |> Str.global_replace (Str.regexp "8") "eight"
-  |> Str.global_replace (Str.regexp "9") "nine"
-
-let namecode_string str =
-  let str = Str.global_replace (Str.regexp "_") "" (Util.zencode_string str) in
-  replace_numbers (String.sub str 1 (String.length str - 1))
-
-let namecode_id id = namecode_string (string_of_id id)
+  let replacements =
+    [ ("0", "Zero");
+      ("1", "One");
+      ("2", "Two");
+      ("3", "Three");
+      ("4", "Four");
+      ("5", "Five");
+      ("6", "Six");
+      ("7", "Seven");
+      ("8", "Eight");
+      ("9", "Nine") ]
+  in
+  List.fold_left (fun str (from, into) -> Str.global_replace (Str.regexp_string from) into str) str replacements
+
+let category_name = function
+  | Function -> "fn"
+  | Val -> "val"
+  | Overload -> "overload"
+  | FunclNum n -> "fcl" ^ unique_postfix n
+  | FunclCtor (id, n) ->
+     let str = replace_numbers (Util.zencode_string (string_of_id id)) in
+     "fcl" ^ String.sub str 1 (String.length str - 1) ^ unique_postfix n
+  | FunclApp str -> "fcl" ^ str
+
+let category_name_val = function
+  | Val -> ""
+  | cat -> category_name cat
+
+let category_name_simple = function
+  | Function -> "fn"
+  | Val -> "val"
+  | Overload -> "overload"
+  | FunclNum _ -> "fcl"
+  | FunclCtor (_, _) -> "fcl"
+  | FunclApp _ -> "fcl"
+
+(* Generate a unique latex identifier from a Sail identifier. We store
+   a mapping from identifiers to strings in state so we always return
+   the same latex id for a sail id. *)
+let latex_id id =
+  if Bindings.mem id state.generated_names then
+    Bindings.find id state.generated_names
+  else
+    let str = string_of_id id in
+    let r = Str.regexp {|_\([a-zA-Z0-9]\)|} in
+    let str =
+      (* Convert to CamelCase. OCaml's regexp library is a bit arcane. *)
+      let str = ref str in
+      try
+        while true do
+          ignore (Str.search_forward r !str 0);
+          let replace = (Str.matched_group 0 !str).[1] |> Char.uppercase_ascii |> String.make 1 in
+          str := Str.replace_first r replace !str
+        done; ""
+      with Not_found -> !str
+    in
+    (* If we have any other weird symbols in the id, remove them using Util.zencode_string (removing the z prefix) *)
+    let str = Util.zencode_string str in
+    let str = String.sub str 1 (String.length str - 1) in
+    (* Latex only allows letters in identifiers, so replace all numbers *)
+    let str = replace_numbers str in
+
+    let generated = state.generated_names |> Bindings.bindings |> List.map snd |> StringSet.of_list in
+
+    (* The above makes maps different names to the same name, so we need
+     to keep track of what names we've generated an ensure that they
+     remain unique. *)
+    let rec unique n str =
+      if StringSet.mem (str ^ unique_postfix n) generated then
+        unique (n + 1) str
+      else
+        str ^ unique_postfix n
+    in
+    let str = unique (-1) str in
+    state.generated_names <- Bindings.add id str state.generated_names;
+    str
 
 let refcode_string str =
-  replace_numbers (Str.global_replace (Str.regexp "_") "zy" (Util.zencode_string str))
+  Str.global_replace (Str.regexp "_") "zy" (Util.zencode_string str)
 
 let refcode_id id = refcode_string (string_of_id id)
 
+let inline_code str = sprintf "\\lstinline{%s}" str
+
+let text_code str =
+  str
+  |> Str.global_replace (Str.regexp_string "_") "\\_"
+  |> Str.global_replace (Str.regexp_string ">") "$<$"
+  |> Str.global_replace (Str.regexp_string "<") "$>$"
+
+let replace_this str =
+  match state.this with
+  | Some id ->
+     str
+     |> Str.global_replace (Str.regexp_string "NAME") (text_code (string_of_id id))
+     |> Str.global_replace (Str.regexp_string "THIS") (inline_code (string_of_id id))
+  | None -> str
+
+let latex_of_markdown str =
+  let open Omd in
+  let open Printf in
+
+  let rec format_elem = function
+    | 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
+    | Emph elems -> sprintf "\\emph{%s}" (format elems)
+    | Bold elems -> sprintf "\\textbf{%s}" (format elems)
+    | Ref (r, "THIS", alt, _) ->
+       begin match state.this with
+       | Some id -> sprintf "\\hyperref[%s]{%s}" (refcode_string (string_of_id id)) (replace_this alt)
+       | None -> failwith "Cannot create link to THIS"
+       end
+    | Ref (r, name, alt, _) ->
+       (* special case for [id] (format as code) *)
+       let format_fn = if name = alt then inline_code else replace_this in
+       begin match r#get_ref name with
+       | None -> sprintf "\\hyperref[%s]{%s}" (refcode_string name) (format_fn alt)
+       | Some (link, _) -> sprintf "\\hyperref[%s]{%s}" (refcode_string link) (format_fn alt)
+       end
+    | Url (href, text, "") ->
+       sprintf "\\href{%s}{%s}" href (format text)
+    | Url (href, text, reference) ->
+       sprintf "%s\\footnote{%s~\\url{%s}}" (format text) reference href
+    | Code (_, code) ->
+       sprintf "\\lstinline`%s`" code
+    | Code_block (lang, code) ->
+       let lang = if lang = "" then "sail" else lang in
+       let uid = Digest.string str |> Digest.to_hex in
+       let chan = open_out (Filename.concat !opt_directory (sprintf "block%s.%s" uid lang)) in
+       output_string chan code;
+       close_out chan;
+       sprintf "\\lstinputlisting[language=%s]{%s/block%s.%s}" lang !opt_directory uid lang
+    | Ul list ->
+       "\\begin{itemize}\n\\item "
+       ^ Util.string_of_list "\n\\item " format list
+       ^ "\n\\end{itemize}"
+    | Br -> "\n"
+    | NL -> "\n"
+    | elem -> failwith ("Can't convert to latex: " ^ to_text [elem])
+
+  and format elems =
+    String.concat "" (List.map format_elem elems)
+  in
+
+  replace_this (format (of_string str))
+
 let docstring = function
-  | Parse_ast.Documented (str, _) -> string str
+  | Parse_ast.Documented (str, _) -> string (latex_of_markdown str)
   | _ -> empty
 
 let add_links str =
   let r = Str.regexp {|\([a-zA-Z0-9_]+\)\([ ]*\)(|} in
   let subst s =
-    let module StringSet = Set.Make(String) in
     let keywords = StringSet.of_list
       [ "function"; "forall"; "if"; "then"; "else"; "exit"; "return"; "match"; "vector";
         "assert"; "constraint"; "let"; "in"; "atom"; "range"; "throw"; "sizeof"; "foreach" ]
     in
     let fn = Str.matched_group 1 s in
     let spacing = Str.matched_group 2 s in
-    if StringSet.mem fn keywords then
+    if StringSet.mem fn keywords || StringSet.mem fn state.norefs then
       fn ^ spacing ^ "("
     else
-      Printf.sprintf {|#\hyperref[%s]{%s}#%s(|} (refcode_string fn) (Str.global_replace (Str.regexp "_") {|\_|} fn) spacing
+      Printf.sprintf "#\\hyperref[%s]{%s}#%s(" (refcode_string fn) (Str.global_replace (Str.regexp "_") {|\_|} fn) spacing
   in
   Str.global_substitute r subst str
 
@@ -116,30 +288,30 @@ let latex_loc no_loc l =
 
   | _ -> docstring l ^^ no_loc
 
-module StringSet = Set.Make(String)
-
 let commands = ref StringSet.empty
 
-let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l, _) as annot) =
-  let labelling = match label with
-    | None -> ""
-    | Some l -> Printf.sprintf "\\label{%s}" l
+let doc_spec_simple (VS_val_spec(ts,id,ext,is_cast)) =
+     Pretty_print_sail.doc_id id ^^ space
+     ^^ colon ^^ space
+     ^^ Pretty_print_sail.doc_typschm ~simple:true ts
+
+let rec latex_command cat id no_loc ((l, _) as annot) =
+  state.this <- Some id;
+  let labelling = match cat with
+    | Val -> sprintf "\\label{%s}" (refcode_id id)
+    | _ -> sprintf "\\label{%s%s}" (category_name cat) (refcode_id id)
   in
-  let cmd = !opt_prefix_latex ^ prefix ^ cmd in
-  let lcmd = String.lowercase_ascii cmd in  (* lowercase to avoid file names differing only by case *)
-  if StringSet.mem lcmd !commands then
-    latex_command ~label:label dir (cmd ^ "v") no_loc annot
-  else
-    begin
-      commands := StringSet.add lcmd !commands;
-      let oc = open_out (Filename.concat dir (cmd ^ ".tex")) in
-      output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l));
-      close_out oc;
-      string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s.tex}}" dir cmd)
-    end
+  (* To avoid problems with verbatim environments in commands, we have
+     to put the sail code for each command in a separate file. *)
+  let code_file = category_name cat ^ Util.file_encode_string (string_of_id id) ^ ".tex" in
+  let chan = open_out (Filename.concat !opt_directory code_file) in
+  let doc = if cat = Val then no_loc else latex_loc no_loc l in
+  output_string chan (Pretty_print_sail.to_string doc);
+  close_out chan;
 
-let latex_command_id ?prefix:(prefix="") dir id no_loc annot =
-  latex_command ~prefix:prefix ~label:(Some (refcode_id id)) dir (namecode_id id) no_loc annot
+  ksprintf string "\\newcommand{\\sail%s%s}{\\phantomsection%s\\saildoc%s{" (category_name cat) (latex_id id) labelling (category_name_simple cat)
+  ^^ docstring l ^^ string "}{"
+  ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file)
 
 let latex_label str id =
   string (Printf.sprintf "\\label{%s:%s}" str (Util.zencode_string (string_of_id id)))
@@ -148,44 +320,134 @@ let counter = ref 0
 
 let rec app_code (E_aux (exp, _)) =
   match exp with
-  | E_app (f, [exp]) -> namecode_id f ^ app_code exp
-  | E_app (f, _) -> namecode_id f
-  | E_id id -> namecode_id id
+  | E_app (f, [exp]) when Id.compare f (mk_id "Some") = 0 -> app_code exp
+  | E_app (f, [exp]) -> latex_id f ^ app_code exp
+  | E_app (f, _) -> latex_id f
+  | E_id id -> latex_id id
   | _ -> ""
 
-let rec latex_funcls dir def =
-  let next funcls = twice hardline ^^ latex_funcls dir def funcls in
-  let funcl_command (FCL_Funcl (id, pexp)) =
-    match pexp with
-    | Pat_aux (Pat_exp (P_aux (P_app (ctor, _), _), _), _) -> namecode_id id ^ namecode_id ctor
-    | Pat_aux (Pat_exp (_, exp), _) -> namecode_id id ^ app_code exp
-    | _ -> (incr counter; namecode_id id ^ String.make 1 (Char.chr (!counter + 64)))
+let latex_funcls def =
+  let module StringMap = Map.Make(String) in
+  let counter = ref 0 in
+  let app_codes = ref StringMap.empty in
+  let ctors = ref Bindings.empty in
+
+  let rec latex_funcls' def =
+    let counter = ref (-1) in
+    let next funcls = twice hardline ^^ latex_funcls' def funcls in
+    let funcl_command (FCL_Funcl (id, pexp)) =
+      match pexp with
+      | Pat_aux (Pat_exp (P_aux (P_app (ctor, _), _), _), _) ->
+         let n = try Bindings.find ctor !ctors with Not_found -> -1 in
+         ctors := Bindings.add ctor (n + 1) !ctors;
+         FunclCtor (ctor, n), id
+      | Pat_aux (Pat_exp (_, exp), _) ->
+         let ac = app_code exp in
+         let n = try StringMap.find ac !app_codes with Not_found -> -1 in
+         app_codes := StringMap.add ac (n + 1) !app_codes;
+         FunclApp (ac ^ unique_postfix n), id
+      | _ -> incr counter; (FunclNum (!counter + 64), id)
+    in
+    function
+    | (FCL_aux (funcl_aux, annot) as funcl) :: funcls ->
+       let cat, id = funcl_command funcl_aux in
+       let first = latex_command cat id (Pretty_print_sail.doc_funcl funcl) annot in
+       first ^^ next funcls
+    | [] -> empty
+  in
+  latex_funcls' def
+
+let process_pragma l command =
+  let n = try String.index command ' ' with Not_found -> String.length command in
+  let cmd = Str.string_before command n in
+  let arg = String.trim (Str.string_after command n) in
+
+  match cmd with
+  | "noindent" ->
+     state.noindent <- true;
+     None
+
+  | "noref" ->
+     state.norefs <- StringSet.add arg state.norefs;
+     None
+
+  | "newcommand" ->
+     let n = try String.index arg ' ' with Not_found -> failwith "No command given" in
+     let name = Str.string_before arg n in
+     let body = String.trim (latex_of_markdown (Str.string_after arg n)) in
+     Some (ksprintf string "\\newcommand{\\%s}{%s}" name body)
+
+  | _ ->
+     Util.warn (Printf.sprintf "Bad latex pragma %s" (Reporting.loc_to_string l));
+     None
+
+let defs (Defs defs) =
+  reset_state state;
+
+  let valspecs = ref IdSet.empty in
+  let fundefs = ref IdSet.empty in
+
+  let latex_def def =
+    match def with
+    | DEF_overload (id, ids) -> None
+                                  (*
+       let doc =
+         string (Printf.sprintf "overload %s = {%s}" (string_of_id id) (Util.string_of_list ", " string_of_id ids))
+       in
+       Some (latex_command Overload id doc (id_loc id, None))
+                                   *)
+
+    | DEF_spec (VS_aux (VS_val_spec (_, id, _, _) as vs, annot)) as def ->
+       valspecs := IdSet.add id !valspecs;
+       Some (latex_command Val id (doc_spec_simple vs) annot)
+
+    | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), annot)) as def ->
+       fundefs := IdSet.add id !fundefs;
+       Some (latex_command Function id (Pretty_print_sail.doc_def def) annot)
+
+    | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) as def ->
+       Some (latex_funcls def funcls)
+
+    | DEF_pragma ("latex", command, l) ->
+       process_pragma l command
+
+    | _ -> None
+  in
+
+  let rec process_defs = function
+    | [] -> empty
+    | def :: defs ->
+       let tex = match latex_def def with
+         | Some tex -> tex ^^ twice hardline
+         | None -> empty
+       in
+       tex ^^ process_defs defs
   in
-  function
-  | (FCL_aux (funcl_aux, annot) as funcl) :: funcls ->
-     let first = latex_command ~prefix:"fn" dir (funcl_command funcl_aux) (Pretty_print_sail.doc_funcl funcl) annot in
-     first ^^ next funcls
-  | [] -> empty
-
-let rec latex_defs dir (Defs defs) =
-  let next defs = twice hardline ^^ latex_defs dir (Defs defs) in
-  match defs with
-  | DEF_overload (id, ids) :: defs ->
-     let doc =
-       string (Printf.sprintf "overload %s = {%s}" (string_of_id id) (Util.string_of_list ", " string_of_id ids))
-     in
-     latex_command_id dir id doc (Parse_ast.Unknown, None)
-     ^^ next defs
-  | (DEF_type (TD_aux (TD_abbrev (id, _, _), annot)) as def) :: defs ->
-     latex_command_id dir id (Pretty_print_sail.doc_def def) annot ^^ next defs
-  | (DEF_type (TD_aux (TD_record (id, _, _, _, _), annot)) as def) :: defs ->
-     latex_command_id dir id (Pretty_print_sail.doc_def def) annot ^^ next defs
-  | (DEF_type (TD_aux (TD_enum (id, _, _, _), annot)) as def) :: defs ->
-     latex_command_id dir id (Pretty_print_sail.doc_def def) annot ^^ next defs
-  | (DEF_spec (VS_aux (VS_val_spec (_, id, _, _), annot)) as def) :: defs ->
-     latex_command_id dir id (Pretty_print_sail.doc_def def) annot ^^ next defs
-  | (DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), annot)) as def) :: defs ->
-     latex_command_id dir ~prefix:"fn" id (Pretty_print_sail.doc_def def) annot ^^ next defs
-  | (DEF_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) as def) :: defs -> latex_funcls dir def funcls ^^ next defs
-  | _ :: defs -> latex_defs dir (Defs defs)
-  | [] -> empty
+
+  let tex = process_defs defs in
+
+  (* Rather than having latex functions that use mangled names, like
+     \sailfnmyFunction for a function my_function, we can write
+     \sailfn{my_function} by generating a latex macro that compares
+     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}{\\sail%s%s}{}" (string_of_id id) (category_name cat) (latex_id id))
+                          (IdSet.elements ids)
+    ^ "}"
+    |> string
+  in
+  let ref_command cat ids =
+    sprintf "\\newcommand{\\%sref%s}[2]{\n  " !opt_prefix (category_name cat)
+    ^ Util.string_of_list "%\n  " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\hyperref[%s%s]{#2}}{}" (string_of_id id) (category_name_val cat) (refcode_id id))
+                          (IdSet.elements ids)
+    ^ "}"
+    |> string
+  in
+
+  tex
+  ^^ separate (twice hardline) [id_command Val !valspecs;
+                                ref_command Val !valspecs;
+                                id_command Function !fundefs;
+                                ref_command Function !fundefs]
+  ^^ hardline
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 31b1ed85..792c3d23 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -113,7 +113,7 @@ let rec doc_nexp =
   in
   nexp0
 
-let doc_nc =
+let doc_nc nc =
   let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in
   let rec atomic_nc (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
@@ -151,9 +151,9 @@ let doc_nc =
     | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
     | _ -> atomic_nc nc
   in
-  nc0
+  nc0 (constraint_simp nc)
 
-let rec doc_typ (Typ_aux (typ_aux, l)) =
+let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
   | Typ_app (id, []) -> doc_id id
@@ -177,7 +177,10 @@ let rec doc_typ (Typ_aux (typ_aux, l)) =
      separate space [doc_arg_typs typs; string "->"; doc_typ typ]
   | Typ_fn (typs, typ, Effect_aux (Effect_set effs, _)) ->
      let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in
-     separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
+     if simple then
+       separate space [doc_arg_typs typs; string "->"; doc_typ ~simple:simple typ]
+     else
+       separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
   | Typ_bidir (typ1, typ2) ->
      separate space [doc_typ typ1; string "<->"; doc_typ typ2]
   | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
@@ -217,24 +220,24 @@ let doc_quants quants =
   | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc
   | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
 
-let doc_binding ((TypQ_aux (tq_aux, _) as typq), typ) =
+let doc_binding ?(simple=false) ((TypQ_aux (tq_aux, _) as typq), typ) =
   match tq_aux with
-  | TypQ_no_forall -> doc_typ typ
-  | TypQ_tq [] -> doc_typ typ
+  | TypQ_no_forall -> doc_typ ~simple:simple typ
+  | TypQ_tq [] -> doc_typ ~simple:simple typ
   | TypQ_tq qs ->
      if !opt_use_heuristics && String.length (string_of_typquant typq) > 60 then
        let kopts, ncs = quant_split typq in
        if ncs = [] then
          string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ dot
-         ^//^ doc_typ typ
+         ^//^ doc_typ ~simple:simple typ
        else
          string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ comma
          ^//^ (separate_map (space ^^ string "&" ^^ space) doc_nc ncs ^^ dot
-               ^^ hardline ^^ doc_typ typ)
+               ^^ hardline ^^ doc_typ ~simple:simple typ)
      else
-       string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ
+       string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ ~simple:simple typ
 
-let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ)
+let doc_typschm ?(simple=false) (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding ~simple:simple (typq, typ)
 
 let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ
 
@@ -569,7 +572,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | _ -> string "TYPEDEF"
 
 
-let doc_spec (VS_aux (v, annot)) =
+let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) =
   let doc_extern ext =
     let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^
       utf8string ("\"" ^ String.escaped id ^  "\"")) (ext b) in
@@ -578,7 +581,7 @@ let doc_spec (VS_aux (v, annot)) =
   in
   match v with
   | VS_val_spec(ts,id,ext,is_cast) ->
-     docstring annot
+     if comment then docstring annot else empty
      ^^ string "val" ^^ space
      ^^ (if is_cast then (string "cast" ^^ space) else empty)
      ^^ doc_id id ^^ space
@@ -617,6 +620,8 @@ let rec doc_def def = group (match def with
      ^^ hardline ^^ string "}"
   | DEF_reg_dec dec -> doc_dec dec
   | DEF_scattered sdef -> doc_scattered sdef
+  | DEF_pragma (pragma, arg, l) ->
+     string ("$" ^ pragma ^ " " ^ arg)
   | DEF_fixity (prec, n, id) ->
      fixities := Bindings.add id (prec, Big_int.to_int n) !fixities;
      separate space [doc_prec prec; doc_int n; doc_id id]
diff --git a/src/process_file.ml b/src/process_file.ml
index 53293849..c3d0be0e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -75,7 +75,8 @@ let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs =
       with
       | Parser.Error ->
          let pos = Lexing.lexeme_start_p lexbuf in
-         raise (Fatal_error (Err_syntax (pos, "no information")))
+         let tok = Lexing.lexeme lexbuf in
+         raise (Fatal_error (Err_syntax (pos, "current token: " ^ tok)))
       | Lexer.LexError(s,p) ->
          raise (Fatal_error (Err_lex (p, s)))
     end
@@ -204,8 +205,8 @@ let rec preprocess opts = function
        let help = "Make sure the filename is surrounded by quotes or angle brackets" in
        (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs)
 
-  | Parse_ast.DEF_pragma (p, arg, _) :: defs ->
-     (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess opts defs)
+  | Parse_ast.DEF_pragma (p, arg, l) :: defs ->
+     Parse_ast.DEF_pragma (p, arg, l) :: preprocess opts defs
 
   (* realise any anonymous record arms of variants *)
   | Parse_ast.DEF_type (Parse_ast.TD_aux
diff --git a/src/rewriter.ml b/src/rewriter.ml
index cf04eef4..cf547307 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -358,6 +358,8 @@ let rewrite_def rewriters d = match d with
   | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
   | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
+  | DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l)
+  | DEF_constraint _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_constraint survived to rewritter")
   | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
 
 let rewrite_defs_base rewriters (Defs defs) =
diff --git a/src/sail.ml b/src/sail.ml
index df095e0e..c9cead2a 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -109,7 +109,7 @@ let options = Arg.align ([
     Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators),
     "<types> produce random generators for the given types");
   ( "-latex",
-    Arg.Set opt_print_latex,
+    Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ],
     " pretty print the input to latex");
   ( "-c",
     Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen],
@@ -167,7 +167,7 @@ let options = Arg.align ([
     Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f::!Pretty_print_coq.opt_debug_on),
     "<function> produce debug messages for Coq output on given function");
   ( "-latex_prefix",
-    Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix),
+    Arg.String (fun prefix -> Latex.opt_prefix := prefix),
     " set a custom prefix for generated latex command (default sail)");
   ( "-mono_split",
     Arg.String (fun s ->
@@ -366,15 +366,19 @@ let main() =
       (if !(opt_print_latex)
        then
          begin
+           Util.opt_warnings := true;
            let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in
-           try
-             if not (Sys.is_directory latex_dir) then begin
-                 prerr_endline ("Failure: latex output directory exists but is not a directory: " ^ latex_dir);
-                 exit 1
-               end
-           with Sys_error(_) -> Unix.mkdir latex_dir 0o755;
+           begin
+             try
+               if not (Sys.is_directory latex_dir) then begin
+                   prerr_endline ("Failure: latex output directory exists but is not a directory: " ^ latex_dir);
+                   exit 1
+                 end
+             with Sys_error(_) -> Unix.mkdir latex_dir 0o755
+           end;
+           Latex.opt_directory := latex_dir;
            let chan = open_out (Filename.concat latex_dir "commands.tex") in
-           output_string chan (Pretty_print_sail.to_string (Latex.latex_defs latex_dir ast));
+           output_string chan (Pretty_print_sail.to_string (Latex.defs ast));
            close_out chan
          end
        else ());
diff --git a/src/type_check.ml b/src/type_check.ml
index aa2d3473..0079d59f 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -73,6 +73,10 @@ let opt_no_lexp_bounds_check = ref false
    definitions *)
 let opt_constraint_synonyms = ref false
 
+(* opt_expand_valspec expands typedefs in valspecs during type check.
+   We prefer not to do it for latex output but it is otherwise a good idea. *)
+let opt_expand_valspec = ref true
+
 let depth = ref 0
 
 let rec indent n = match n with
@@ -4386,7 +4390,12 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
        in
        let env = Env.add_extern id ext_opt env in
        let env = if is_cast then Env.add_cast id env else env in
-       let typq, typ = expand_bind_synonyms ts_l env (typq, typ) in
+       let typq, typ =
+         if !opt_expand_valspec then 
+           expand_bind_synonyms ts_l env (typq, typ)
+         else
+           (typq, typ)
+       in
        let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in
        (vs, id, typq, typ, env)
   in
@@ -4532,6 +4541,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
      let checked_exp = crule check_exp env (strip_exp exp) typ in
      let env = Env.add_register id no_effect (mk_effect [BE_config]) typ env in
      [DEF_reg_dec (DEC_aux (DEC_config (id, typ, checked_exp), (l, Some ((env, typ, no_effect), Some typ))))], env
+  | DEF_pragma (pragma, arg, l) -> [DEF_pragma (pragma, arg, l)], env
   | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err ()
   | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
   | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Scattered given to type checker")
diff --git a/src/type_check.mli b/src/type_check.mli
index 1cb54770..dc1cfe97 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -71,6 +71,10 @@ val opt_no_lexp_bounds_check : bool ref
    definitions *)
 val opt_constraint_synonyms : bool ref
 
+(** opt_expand_valspec expands typedefs in valspecs during type check.
+   We prefer not to do it for latex output but it is otherwise a good idea. *)
+val opt_expand_valspec : bool ref
+
 (** {2 Type errors} *)
 
 type type_error =
diff --git a/src/util.ml b/src/util.ml
index 2e121a4f..5e5654d1 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -448,6 +448,14 @@ let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.ma
 
 let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str))
 
+(** Encode string for use as a filename. We can't use zencode directly
+   because some operating systems make the mistake of being
+   case-insensitive. *)
+let file_encode_string str =
+  let zstr = zencode_string str in
+  let md5 = Digest.to_hex (Digest.string zstr) in
+  String.lowercase_ascii zstr ^ String.lowercase_ascii md5
+
 let warn str =
   if !opt_warnings then
     prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str)
diff --git a/src/util.mli b/src/util.mli
index 1d80bc10..fd0242a3 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -57,8 +57,8 @@ val opt_colors : bool ref
 val butlast : 'a list -> 'a list
 
 (** Mixed useful things *)
-module Duplicate(S : Set.S) : sig 
-  type dups = 
+module Duplicate(S : Set.S) : sig
+  type dups =
     | No_dups of S.t
     | Has_dups of S.elt
   val duplicates : S.elt list -> dups
@@ -259,5 +259,7 @@ val warn : string -> unit
 val zencode_string : string -> string
 val zencode_upper_string : string -> string
 
+val file_encode_string : string -> string
+
 val log_line : string -> int -> string -> string
 val header : string -> int -> string