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. --- .merlin | 2 +- editors/sail2-mode.el | 3 +- language/sail.ott | 2 + lib/flow.sail | 2 +- lib/vector_dec.sail | 2 - 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 +- 16 files changed, 345 insertions(+), 107 deletions(-) diff --git a/.merlin b/.merlin index 7d00b00d..d764f5eb 100644 --- a/.merlin +++ b/.merlin @@ -9,4 +9,4 @@ S src/lem_interp/** S src/pprint/** S src/test/** B src/_build/** -PKG num str unix uint zarith linksem lem \ No newline at end of file +PKG num str unix uint zarith linksem lem omd linenoise \ No newline at end of file diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index ac3c199c..e7b115ba 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -21,7 +21,8 @@ "uint64_t" "int64_t" "bv_t" "mpz_t")) (defconst sail2-special - '("_prove" "create" "kill" "convert" "undefined" "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option")) + '("_prove" "create" "kill" "convert" "undefined" + "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$latex")) (defconst sail2-font-lock-keywords `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face) diff --git a/language/sail.ott b/language/sail.ott index 59d51d68..c86f9a33 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -1038,6 +1038,8 @@ def :: 'DEF_' ::= | constraint id ( kid1 , ... , kidn ) = n_constraint :: :: constraint | fundef1 .. fundefn :: I :: internal_mutrec {{ com internal representation of mutually recursive functions }} + | $ string1 string2 l :: :: pragma + {{ com compiler directive }} defs :: '' ::= {{ com definition sequence }} diff --git a/lib/flow.sail b/lib/flow.sail index 5ee9a74a..cdc6b2fd 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -11,7 +11,7 @@ therefore be included in just about every Sail specification. val eq_unit : (unit, unit) -> bool -val "eq_bit" : (bit, bit) -> bool +val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool function eq_unit(_, _) = true diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 8abcd218..37e10c2f 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -5,8 +5,6 @@ $include type bits ('n : Int) = vector('n, dec, bit) -val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool - val eq_bits = { ocaml: "eq_list", lem: "eq_vec", 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 -: package(zarith), package(linksem), package(lem), use_pprint -: package(zarith), package(linenoise), package(linksem), package(lem), use_pprint +: package(zarith), package(linksem), package(lem), package(omd), use_pprint +: package(zarith), package(linenoise), package(linksem), package(lem), package(omd), use_pprint : package(linenoise) : package(linksem) +: package(omd) <**/*.m{l,li}>: package(lem) : 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), " 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