diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/latex.ml | 32 | ||||
| -rw-r--r-- | src/parser.mly | 6 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 14 |
3 files changed, 29 insertions, 23 deletions
diff --git a/src/latex.ml b/src/latex.ml index f8e79540..f6aed63c 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -85,8 +85,8 @@ let add_links str = let subst s = let module StringSet = Set.Make(String) in let keywords = StringSet.of_list - [ "function"; "forall"; "if"; "then"; "else"; "exit"; "return"; "match"; - "assert"; "constraint"; "let"; "in"; "atom"; "range"; "throw" ] + [ "function"; "forall"; "if"; "then"; "else"; "exit"; "return"; "match"; "vector"; + "assert"; "constraint"; "let"; "in"; "atom"; "range"; "throw"; "sizeof" ] in let fn = Str.matched_group 1 s in let spacing = Str.matched_group 2 s in @@ -128,11 +128,12 @@ module StringSet = Set.Make(String) let commands = ref StringSet.empty -let rec latex_command ?label:(label=None) cmd no_loc ((l, _) as annot) = +let rec latex_command ?prefix:(prefix="") ?label:(label=None) cmd no_loc ((l, _) as annot) = let labelling = match label with | None -> "" - | Some l -> Printf.sprintf "\\phantomsection\\label{%s}" l + | Some l -> Printf.sprintf "\\phantomsection\\label{%s%s}" prefix l in + let cmd = prefix ^ cmd in if StringSet.mem cmd !commands then latex_command ~label:label (cmd ^ "v") no_loc annot else @@ -142,10 +143,11 @@ let rec latex_command ?label:(label=None) cmd no_loc ((l, _) as annot) = ^^ string (Printf.sprintf "\\newsavebox{\\box%s}\n\\begin{lrbox}{\\box%s}\n\\begin{lstlisting}" cmd cmd) ^^ hardline ^^ latex_loc no_loc l ^^ string "\\end{lstlisting}\n\\end{lrbox}" ^^ hardline - ^^ string (Printf.sprintf "\\newcommand{\\sail%s}{\\noindent\\usebox{\\box%s}%s}" cmd cmd labelling) + ^^ string (Printf.sprintf "\\newcommand{\\sail%s}{\\begin{sail}\\usebox{\\box%s}%s\\end{sail}}" cmd cmd labelling) end -let latex_command_id id no_loc annot = latex_command ~label:(Some (refcode_id id)) (namecode_id id) no_loc annot +let latex_command_id ?prefix:(prefix="") id no_loc annot = + latex_command ~prefix:prefix ~label:(Some (refcode_id id)) (namecode_id id) no_loc annot let latex_label str id = string (Printf.sprintf "\\label{%s:%s}" str (Util.zencode_string (string_of_id id))) @@ -165,23 +167,23 @@ let rec latex_funcls def = 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; refcode_id id ^ String.make 1 (Char.chr (!counter + 64))) + | _ -> (incr counter; namecode_id id ^ String.make 1 (Char.chr (!counter + 64))) in function | (FCL_aux (funcl_aux, annot) as funcl) :: funcls -> - latex_command (funcl_command funcl_aux) (Pretty_print_sail.doc_funcl funcl) annot ^^ next funcls + let first = latex_command ~prefix:"fn" (funcl_command funcl_aux) (Pretty_print_sail.doc_funcl funcl) annot in + first ^^ next funcls | [] -> empty let rec latex_defs (Defs defs) = let next defs = twice hardline ^^ latex_defs (Defs defs) in match defs with - | DEF_overload (id, ids) :: defs -> next defs - (* - string (Printf.sprintf {|\begin{lstlisting}[label={%s}]|} (refcode_id id)) ^^ hardline - ^^ string (Printf.sprintf "overload %s = {%s}" (string_of_id id) (Util.string_of_list ", " string_of_id ids)) - ^^ string {|\end{lstlisting}|} + | 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 id doc (Parse_ast.Unknown, None) ^^ next defs - *) | (DEF_type (TD_aux (TD_abbrev (id, _, _), annot)) as def) :: defs -> latex_command_id id (Pretty_print_sail.doc_def def) annot ^^ next defs | (DEF_type (TD_aux (TD_record (id, _, _, _, _), annot)) as def) :: defs -> @@ -191,7 +193,7 @@ let rec latex_defs (Defs defs) = | (DEF_spec (VS_aux (VS_val_spec (_, id, _, _), annot)) as def) :: defs -> latex_command_id 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 id (Pretty_print_sail.doc_def def) annot ^^ next defs + latex_command_id ~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 def funcls ^^ next defs | _ :: defs -> latex_defs (Defs defs) | [] -> empty diff --git a/src/parser.mly b/src/parser.mly index 97b6f28c..5b8c3af1 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1022,6 +1022,8 @@ atomic_exp: { mk_exp (E_vector_access ($1, $3)) $startpos $endpos } | atomic_exp Lsquare exp DotDot exp Rsquare { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos } + | atomic_exp Lsquare exp Comma exp Rsquare + { mk_exp (E_app (mk_id (Id "slice") $startpos($2) $endpos, [$1; $3; $5])) $startpos $endpos } | Struct Lcurly fexp_exp_list Rcurly { mk_exp (E_record $3) $startpos $endpos } | Lcurly exp With fexp_exp_list Rcurly @@ -1081,13 +1083,13 @@ funcls2: | id funcl_patexp { [mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos] } | id funcl_patexp And funcls2 - { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4 } + { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos($2) :: $4 } funcls: | id funcl_patexp_typ { let pexp, tannot = $2 in ([mk_funcl (FCL_Funcl ($1, pexp)) $startpos $endpos], tannot) } | id funcl_patexp And funcls2 - { (mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4, mk_tannotn) } + { (mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos($2) :: $4, mk_tannotn) } funcl_typ: | Forall typquant Dot typ diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index a63491a2..c0658a83 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -258,6 +258,8 @@ let fixities = [ (mk_id "^", (InfixR, 8)); (mk_id "*", (InfixL, 7)); + (mk_id "/", (InfixL, 7)); + (mk_id "%", (InfixL, 7)); (mk_id "+", (InfixL, 6)); (mk_id "-", (InfixL, 6)); (mk_id "!=", (Infix, 4)); @@ -265,6 +267,7 @@ let fixities = (mk_id "<", (Infix, 4)); (mk_id ">=", (Infix, 4)); (mk_id "<=", (Infix, 4)); + (mk_id "==", (Infix, 4)); (mk_id "&", (InfixR, 3)); (mk_id "|", (InfixR, 2)); ] @@ -355,15 +358,14 @@ and doc_infix n (E_aux (e_aux, _) as exp) = try match Bindings.find op !fixities with | (Infix, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r] - | (Infix, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]) - | (InfixL, m) when m >= n -> separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r] - | (InfixL, m) when m < n -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]) + | (Infix, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]) + | (InfixL, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r] + | (InfixL, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]) | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r] - | (InfixR, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) - | _ -> assert false + | (InfixR, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) with | Not_found -> - separate space [doc_atomic_exp l; doc_id op; doc_atomic_exp r] + parens (separate space [doc_atomic_exp l; doc_id op; doc_atomic_exp r]) end | _ -> doc_atomic_exp exp and doc_atomic_exp (E_aux (e_aux, _) as exp) = |