From 61e6bc97a7d5efb58f9b91738f1dd64404091137 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 7 Nov 2018 18:40:57 +0000
Subject: Move inline forall in function definitions

* Previously we allowed the following bizarre syntax for a forall
  quantifier on a function:

  val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit

  this commit changes this to the more sane:

  val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit

  Having talked about it today, we could consider adding the syntax

  val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit

  which would avoid the forall (by implicitly quantifying variables in
  the constraint), and be slightly more friendly especially for
  documentation purposes. Only RISC-V used this syntax, so all uses of
  it there have been switched to the new style.

* Second, there is a new (somewhat experimental) syntax for
  existentials, that is hopefully more readable and closer to
  minisail:

  val foo(x: int, y: int) -> int('m) with 'm >= 2

  "type('n) with constraint" is equivalent to minisail: {'n: type | constraint}
  the type variables in typ are implicitly quantified, so this is equivalent to
  {'n, constraint. typ('n)}

  In order to make this syntax non-ambiguous we have to use == in
  constraints rather than =, but this is a good thing anyway because
  the previous situation where = was type level equality and == term
  level equality was confusing. Now all the type type-level and
  term-level operators can be consistent. However, to avoid breaking
  anything = is still allowed in non-with constraints, and produces a
  deprecated warning when parsed.
---
 src/initial_check.ml |  5 ++++
 src/lexer.mll        |  7 ++---
 src/parse_ast.ml     |  1 +
 src/parser.mly       | 74 ++++++++++++++++++++++++++++++++++++++++------------
 4 files changed, 66 insertions(+), 21 deletions(-)

(limited to 'src')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index f98b11d8..897f3ec2 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -251,6 +251,11 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
                   let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in
                   let exist_typ = to_ast_typ k_env def_ord atyp in
                   Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ)
+               | Parse_ast.ATyp_with (atyp, nc) ->
+                  let exist_typ = to_ast_typ k_env def_ord atyp in
+                  let kids = KidSet.elements (tyvars_of_typ exist_typ) in
+                  let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in
+                  Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ)
                | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None
               ), l)
 
diff --git a/src/lexer.mll b/src/lexer.mll
index 8b229772..de8eed7f 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -97,8 +97,7 @@ let operators = ref
   (List.fold_left
      (fun r (x, y) -> M.add x y r)
      M.empty
-     [ ("==", mk_operator Infix 4 "==");
-       ("/", mk_operator InfixL 7 "/");
+     [ ("/", mk_operator InfixL 7 "/");
        ("%", mk_operator InfixL 7 "%");
      ])
 
@@ -224,9 +223,7 @@ rule token = parse
   | ","                                 { Comma }
   | ".."                                { DotDot }
   | "."                                 { Dot }
-  | "==" as op
-    { try M.find op !operators
-      with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
+  | "=="                                { EqEq(r"==") }
   | "="                                 { (Eq(r"=")) }
   | ">"					{ (Gt(r">")) }
   | "-"					{ Minus }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index d19e85ed..30f87bc3 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -156,6 +156,7 @@ atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders
  | ATyp_tup of (atyp) list (* Tuple type *)
  | ATyp_app of id * (atyp) list (* type constructor application *)
  | ATyp_exist of kid list * n_constraint * atyp
+ | ATyp_with of atyp * n_constraint
 
 and atyp = 
    ATyp_aux of atyp_aux * l
diff --git a/src/parser.mly b/src/parser.mly
index bd7c2f62..12286e13 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -197,6 +197,7 @@ let rec desugar_rchain chain s e =
 
 %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
 %token <string> Colon ColonColon (* CaretCaret *) TildeTilde ExclEq
+%token <string> EqEq
 %token <string> GtEq
 %token <string> LtEq
 
@@ -260,6 +261,7 @@ id:
   | Op Plus { mk_id (DeIid "+") $startpos $endpos }
   | Op Minus { mk_id (DeIid "-") $startpos $endpos }
   | Op Star { mk_id (DeIid "*") $startpos $endpos }
+  | Op EqEq { mk_id (DeIid "==") $startpos $endpos }
   | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos }
   | Op Lt { mk_id (DeIid "<") $startpos $endpos }
   | Op Gt { mk_id (DeIid ">") $startpos $endpos }
@@ -337,9 +339,12 @@ atomic_nc:
     { mk_nc NC_true $startpos $endpos }
   | False
     { mk_nc NC_false $startpos $endpos }
-  | typ Eq typ
+  | typ0 Eq typ0
+    { Util.warn ("Deprecated syntax, use == instead at " ^ Reporting.loc_to_string (loc $startpos($2) $endpos($2)) ^ "\n");
+      mk_nc (NC_equal ($1, $3)) $startpos $endpos }
+  | typ0 EqEq typ0
     { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
-  | typ ExclEq typ
+  | typ0 ExclEq typ0
     { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
   | nc_lchain
     { desugar_lchain $1 $startpos $endpos }
@@ -350,6 +355,38 @@ atomic_nc:
   | kid In Lcurly num_list Rcurly
     { mk_nc (NC_set ($1, $4)) $startpos $endpos }
 
+new_nc:
+  | new_nc Bar new_nc_and
+    { mk_nc (NC_or ($1, $3)) $startpos $endpos }
+  | nc_and
+    { $1 }
+
+new_nc_and:
+  | new_nc_and Amp new_atomic_nc
+    { mk_nc (NC_and ($1, $3)) $startpos $endpos }
+  | new_atomic_nc
+    { $1 }
+
+new_atomic_nc:
+  | Where id Lparen typ_list Rparen
+    { mk_nc (NC_app ($2, $4)) $startpos $endpos }
+  | True
+    { mk_nc NC_true $startpos $endpos }
+  | False
+    { mk_nc NC_false $startpos $endpos }
+  | typ0 EqEq typ0
+    { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
+  | typ0 ExclEq typ0
+    { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
+  | nc_lchain
+    { desugar_lchain $1 $startpos $endpos }
+  | nc_rchain
+    { desugar_rchain $1 $startpos $endpos }
+  | Lparen new_nc Rparen
+    { $2 }
+  | kid In Lcurly num_list Rcurly
+    { mk_nc (NC_set ($1, $4)) $startpos $endpos }
+
 num_list:
   | Num
     { [$1] }
@@ -357,28 +394,30 @@ num_list:
     { $1 :: $3 }
 
 nc_lchain:
-  | typ LtEq typ
+  | typ0 LtEq typ0
     { [LC_nexp $1; LC_lteq; LC_nexp $3] }
-  | typ Lt typ
+  | typ0 Lt typ0
     { [LC_nexp $1; LC_lt; LC_nexp $3] }
-  | typ LtEq nc_lchain
+  | typ0 LtEq nc_lchain
     { LC_nexp $1 :: LC_lteq :: $3 }
-  | typ Lt nc_lchain
+  | typ0 Lt nc_lchain
     { LC_nexp $1 :: LC_lt :: $3 }
 
 nc_rchain:
-  | typ GtEq typ
+  | typ0 GtEq typ0
     { [RC_nexp $1; RC_gteq; RC_nexp $3] }
-  | typ Gt typ
+  | typ0 Gt typ0
     { [RC_nexp $1; RC_gt; RC_nexp $3] }
-  | typ GtEq nc_rchain
+  | typ0 GtEq nc_rchain
     { RC_nexp $1 :: RC_gteq :: $3 }
-  | typ Gt nc_rchain
+  | typ0 Gt nc_rchain
     { RC_nexp $1 :: RC_gt :: $3 }
 
 typ:
   | typ0
     { $1 }
+  | typ0 With new_nc
+    { mk_typ (ATyp_with ($1, $3)) $startpos $endpos }
 
 /* The following implements all nine levels of user-defined precedence for
 operators in types, with both left, right and non-associative operators */
@@ -677,8 +716,8 @@ pat_string_append:
 pat1:
   | atomic_pat
     { $1 }
-  | atomic_pat Bar pat1
-    { mk_pat (P_or ($1, $3)) $startpos $endpos }
+  (* | atomic_pat Bar pat1
+    { mk_pat (P_or ($1, $3)) $startpos $endpos } *)
   | atomic_pat At pat_concat
     { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
   | atomic_pat ColonColon pat1
@@ -890,6 +929,7 @@ exp4:
   | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 EqEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "==") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp5 { $1 }
@@ -1104,12 +1144,14 @@ funcl_patexp:
 funcl_patexp_typ:
   | pat Eq exp
     { (mk_pexp (Pat_exp ($1, $3)) $startpos $endpos, mk_tannotn) }
-  | pat MinusGt funcl_typ Eq exp
-    { (mk_pexp (Pat_exp ($1, $5)) $startpos $endpos, $3) }
+  | pat MinusGt typ Eq exp
+    { (mk_pexp (Pat_exp ($1, $5)) $startpos $endpos, mk_tannot mk_typqn $3 $startpos $endpos($3)) }
+  | Forall typquant Dot pat MinusGt typ Eq exp
+    { (mk_pexp (Pat_exp ($4, $8)) $startpos $endpos, mk_tannot $2 $6 $startpos $endpos($6)) }
   | Lparen pat If_ exp Rparen Eq exp
     { (mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos, mk_tannotn) }
-  | Lparen pat If_ exp Rparen MinusGt funcl_typ Eq exp
-    { (mk_pexp (Pat_when ($2, $4, $9)) $startpos $endpos, $7) }
+  | Forall typquant Dot Lparen pat If_ exp Rparen MinusGt typ Eq exp
+    { (mk_pexp (Pat_when ($5, $7, $12)) $startpos $endpos, mk_tannot $2 $10 $startpos $endpos($10)) }
 
 funcl:
   | id funcl_patexp
-- 
cgit v1.2.3


From 953bfdd18c71bcd6c486aac74fe145104c3b2a4d Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 7 Nov 2018 18:56:28 +0000
Subject: Improvements to latex generation

The main changes so far are:

* Allow markdown formatting in doc comments. We parse the markdown
  using Omd, which is a OCaml library for parsing markdown. The nice
  thing about this library is it's pure OCaml and has no dependencies
  other the the stdlib. Incidentally it was also developed at OCaml
  labs. Using markdown keeps our doc-comments from becoming latex
  specfic, and having an actual parser is _much_ nicer than trying to
  hackily process latex in doc-comments using OCamls somewhat sub-par
  regex support.

* More sane conversion latex identifiers the main approach is to
  convert Sail identifiers to lowerCamelCase, replacing numbers with
  words, and then add a 'category' code based on the type of
  identifier, so for a function we'd have fnlowerCamelCase and for
  type synonym typelowerCamelCase etc. Because this transformation is
  non-injective we keep track of identifiers we've generated so we end
  up with identifierA, identifierB, identifierC when there are
  collisions.

* Because we parse markdown in doc comments doc comments can use Sail
  identifiers directly in hyperlinks, without having to care about how
  they are name-mangled down into TeX compatible things.

* Allow directives to be passed through the compiler to
  backends. There are various $latex directives that modify the latex
  output. Most usefully there's a

  $latex newcommand name markdown

  directive that uses the markdown parser to generate latex
  commands. An example of why this is useful is bellow. We can also use

  $latex noref id

  To suppress automatically inserting links to an identifier

* Refactor the latex generator to make the overall generation process
  cleaner

* Work around the fact that some operating systems consider
  case-sensitive file names to be a good thing

* Fix a bug where latex generation wouldn't occur unless the directory
  specified by -o didn't exist

This isn't quite all the requested features for good CHERI
documentation, but new features should be much easier to add now.
---
 src/_tags                |   5 +-
 src/initial_check.ml     |   4 +-
 src/isail.ml             |   2 +-
 src/latex.ml             | 380 +++++++++++++++++++++++++++++++++++++----------
 src/pretty_print_sail.ml |   6 +-
 src/process_file.ml      |   7 +-
 src/rewriter.ml          |   2 +
 src/sail.ml              |  20 ++-
 src/type_check.ml        |   1 +
 src/util.ml              |   8 +
 src/util.mli             |   6 +-
 11 files changed, 339 insertions(+), 102 deletions(-)

(limited to 'src')

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/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..e5029e0e 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -51,51 +51,204 @@
 open Ast
 open Ast_util
 open PPrint
+open Printf
 
-let opt_prefix_latex = ref "sail"
+module StringSet = Set.Make(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 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
+  | FunclNum of int
+  | FunclApp of string
+
+let category_name = function
+  | Function -> "fn"
+  | Val -> "val"
+  | Overload -> "overload"
+  | FunclNum n -> "fcl" ^ unique_postfix n
+  | FunclCtor id ->  Util.zencode_string (string_of_id id) ^ "fcl"
+  | FunclApp str -> "fcl" ^ str
+
+(* 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 replacements =
+      [ ("0", "Zero");
+        ("1", "One");
+        ("2", "Two");
+        ("3", "Three");
+        ("4", "Four");
+        ("5", "Five");
+        ("6", "Six");
+        ("7", "Seven");
+        ("8", "Eight");
+        ("9", "Nine") ]
+    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 = List.fold_left (fun str (from, into) -> Str.global_replace (Str.regexp_string from) into str) str replacements 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, _) ->
+       begin match r#get_ref name with
+       | None -> sprintf "\\hyperref[%s]{%s}" (refcode_string name) (replace_this alt)
+       | Some (link, _) -> sprintf "\\hyperref[%s]{%s}" (refcode_string link) (replace_this 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 +269,24 @@ 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 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
+  output_string chan (Pretty_print_sail.to_string (latex_loc no_loc l));
+  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" (category_name cat) (latex_id id) labelling
+  ^^ docstring l
+  ^^ 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 +295,113 @@ 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]) -> 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 counter = ref 0 in
+
+  let rec latex_funcls' def =
+    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, _), _), _), _) -> (FunclCtor ctor, id)
+      | Pat_aux (Pat_exp (_, exp), _) -> (FunclApp (app_code exp), 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, _, _), annot)) as def ->
+       valspecs := IdSet.add id !valspecs;
+       Some (latex_command Val id (Pretty_print_sail.doc_def def) 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
-  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 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
+
+  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
+
+  tex
+  ^^ separate (twice hardline) [id_command Val !valspecs;
+                                id_command Function !fundefs]
+  ^^ hardline
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index d71b32b2..c23b5ecc 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -567,7 +567,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
@@ -576,7 +576,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
@@ -615,6 +615,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 bb789d0a..3788d269 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 3505ecf4..a7f780b9 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -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 ->
@@ -359,15 +359,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 c32529e4..46b67930 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4483,6 +4483,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/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
-- 
cgit v1.2.3


From a63c2e692792d69ae7ab9b9ef9b66ad2e5d2fe0b Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 12 Nov 2018 16:15:45 +0000
Subject: Improve latex naming scheme and avoid collisions

---
 src/latex.ml | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index e5029e0e..f9154db2 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -107,7 +107,9 @@ let category_name = function
   | Val -> "val"
   | Overload -> "overload"
   | FunclNum n -> "fcl" ^ unique_postfix n
-  | FunclCtor id ->  Util.zencode_string (string_of_id id) ^ "fcl"
+  | FunclCtor id ->
+     let str = Util.zencode_string (string_of_id id) in
+     "fcl" ^ String.sub str 1 (String.length str - 1)
   | FunclApp str -> "fcl" ^ str
 
 (* Generate a unique latex identifier from a Sail identifier. We store
@@ -208,7 +210,7 @@ let latex_of_markdown str =
     | Url (href, text, "") ->
        sprintf "\\href{%s}{%s}" href (format text)
     | Url (href, text, reference) ->
-       sprintf "%s\footnote{%s~\url{%s}}" (format text) reference href
+       sprintf "%s\\footnote{%s~\\url{%s}}" (format text) reference href
     | Code (_, code) ->
        sprintf "\\lstinline`%s`" code
     | Code_block (lang, code) ->
@@ -295,20 +297,28 @@ let counter = ref 0
 
 let rec app_code (E_aux (exp, _)) =
   match exp with
+  | 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 latex_funcls def =
+  let module StringMap = Map.Make(String) in
   let counter = ref 0 in
+  let app_codes = ref StringMap.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, _), _), _), _) -> (FunclCtor ctor, id)
-      | Pat_aux (Pat_exp (_, exp), _) -> (FunclApp (app_code exp), 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
-- 
cgit v1.2.3


From 518776b45c4ad1f689bcd89ea6583c92583982a8 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 12 Nov 2018 16:32:59 +0000
Subject: Fix numbers in constructor arguments

Also ensure no collisions for function clause constructor categories
---
 src/latex.ml | 43 +++++++++++++++++++++++++------------------
 1 file changed, 25 insertions(+), 18 deletions(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index f9154db2..3c0ce03a 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -98,18 +98,33 @@ type id_category =
   | Function
   | Val
   | Overload
-  | FunclCtor of id
+  | FunclCtor of id * int
   | FunclNum of int
   | FunclApp of string
 
+let replace_numbers str =
+  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 ->
-     let str = Util.zencode_string (string_of_id id) in
-     "fcl" ^ String.sub str 1 (String.length str - 1)
+  | 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
 
 (* Generate a unique latex identifier from a Sail identifier. We store
@@ -120,18 +135,6 @@ let latex_id id =
     Bindings.find id state.generated_names
   else
     let str = string_of_id id in
-    let replacements =
-      [ ("0", "Zero");
-        ("1", "One");
-        ("2", "Two");
-        ("3", "Three");
-        ("4", "Four");
-        ("5", "Five");
-        ("6", "Six");
-        ("7", "Seven");
-        ("8", "Eight");
-        ("9", "Nine") ]
-    in
     let r = Str.regexp {|_\([a-zA-Z0-9]\)|} in
     let str =
       (* Convert to CamelCase. OCaml's regexp library is a bit arcane. *)
@@ -148,7 +151,7 @@ let latex_id id =
     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 = List.fold_left (fun str (from, into) -> Str.global_replace (Str.regexp_string from) into str) str replacements in
+    let str = replace_numbers str in
 
     let generated = state.generated_names |> Bindings.bindings |> List.map snd |> StringSet.of_list in
 
@@ -307,13 +310,17 @@ 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, _), _), _), _) -> (FunclCtor ctor, id)
+      | 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
-- 
cgit v1.2.3


From f638a84add3ed60261bb86544e4332fd2180e1a6 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 12 Nov 2018 17:26:17 +0000
Subject: Add referencing commands to generated latex

---
 src/latex.ml | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index 3c0ce03a..9b1e6da2 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -127,6 +127,10 @@ let category_name = function
      "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
+
 (* 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. *)
@@ -417,8 +421,17 @@ let defs (Defs defs) =
     ^ "}"
     |> 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;
-                                id_command Function !fundefs]
+                                ref_command Val !valspecs;
+                                id_command Function !fundefs;
+                                ref_command Function !fundefs]
   ^^ hardline
-- 
cgit v1.2.3


From 0ea65cc4199e4a1924da93139c4790d9b85bb745 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 14 Nov 2018 15:32:45 +0000
Subject: latex: use callback macro saildocxxx (one per top-level category) to
 give usere more flexibility about formatting generated latex.

---
 src/latex.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index 9b1e6da2..e0dba234 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -131,6 +131,14 @@ 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. *)
@@ -293,9 +301,9 @@ let rec latex_command cat id no_loc ((l, _) as annot) =
   output_string chan (Pretty_print_sail.to_string (latex_loc no_loc l));
   close_out chan;
 
-  ksprintf string "\\newcommand{\\sail%s%s}{\\phantomsection%s" (category_name cat) (latex_id id) labelling
-  ^^ docstring l
-  ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}" (Filename.concat !opt_directory code_file)
+  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)))
-- 
cgit v1.2.3


From 5f00f0d75cfaabb89f2ec22115392443539664bd Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 14 Nov 2018 15:33:10 +0000
Subject: Use code style For [id] refs in doc comments.

---
 src/latex.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index e0dba234..a86731b6 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -218,9 +218,11 @@ let latex_of_markdown str =
        | 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) (replace_this alt)
-       | Some (link, _) -> sprintf "\\hyperref[%s]{%s}" (refcode_string link) (replace_this alt)
+       | 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)
-- 
cgit v1.2.3


From c631ae96bbe9d659a8b3dbb1fc0c7ac812c2d43f Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 15 Nov 2018 15:13:06 +0000
Subject: ast_utils: simplify numeric constraints in inequalities.

---
 src/ast_util.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/ast_util.ml b/src/ast_util.ml
index f0b6508b..71b3299a 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)
-- 
cgit v1.2.3


From 81ce65d8213b9dc26e204512408e6a340fe985fa Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 15 Nov 2018 17:12:37 +0000
Subject: Add simple valspec printing in latex that drops effects and other
 extraneous details (TODO make this optional).

---
 src/latex.ml             | 12 +++++++++---
 src/pretty_print_sail.ml | 25 ++++++++++++++-----------
 2 files changed, 23 insertions(+), 14 deletions(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index a86731b6..2f578f2c 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -290,6 +290,11 @@ let latex_loc no_loc l =
 
 let commands = ref StringSet.empty
 
+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
@@ -300,7 +305,8 @@ let rec latex_command cat id no_loc ((l, _) as annot) =
      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
-  output_string chan (Pretty_print_sail.to_string (latex_loc no_loc l));
+  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;
 
   ksprintf string "\\newcommand{\\sail%s%s}{\\phantomsection%s\\saildoc%s{" (category_name cat) (latex_id id) labelling (category_name_simple cat)
@@ -391,9 +397,9 @@ let defs (Defs defs) =
        Some (latex_command Overload id doc (id_loc id, None))
                                    *)
 
-    | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), annot)) as def ->
+    | DEF_spec (VS_aux (VS_val_spec (_, id, _, _) as vs, annot)) as def ->
        valspecs := IdSet.add id !valspecs;
-       Some (latex_command Val id (Pretty_print_sail.doc_def def) annot)
+       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;
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index c23b5ecc..7608f78b 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
 
-- 
cgit v1.2.3


From 2a906e05a3313a25967833b10bb895db95d08165 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 15 Nov 2018 17:13:38 +0000
Subject: When outputing latex do not expand type synonyms in val specs during
 type check.

---
 src/sail.ml        |  2 +-
 src/type_check.ml  | 11 ++++++++++-
 src/type_check.mli |  4 ++++
 3 files changed, 15 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/sail.ml b/src/sail.ml
index a7f780b9..9208190d 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],
diff --git a/src/type_check.ml b/src/type_check.ml
index 46b67930..4ad93a0c 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
@@ -4337,7 +4341,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
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 =
-- 
cgit v1.2.3