Commit 4fbafaac authored by BECKER Benedikt's avatar BECKER Benedikt

Separate commands for variables and fields with same name

parent bf322a3f
...@@ -68,32 +68,43 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com ...@@ -68,32 +68,43 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
fprintf fmt "\\%s%s%s" prefix (sanitize base) suffix fprintf fmt "\\%s%s%s" prefix (sanitize base) suffix
(** Print a string as a LaTeX command *) (** Print a string as a LaTeX command *)
let pp_command fmt ~arity name = let pp_command ~arity ~is_field fmt name =
if match sn_decode name with | SNword _ -> false | _ -> true then if match sn_decode name with | SNword _ -> false | _ -> true then
failwith ("pp_command: argument not word: "^name); failwith ("pp_command: argument not word: "^name);
let name, name', suffix = let name, name', suffix =
if arity = 0 then if arity = 0 then
match split_base_suffixes name with if is_field then
| Some (base, numbers, quotes) -> name^"field", name, ""
let numbers = else
match numbers with match split_base_suffixes name with
| Some s -> sprintf "_{%s}" s | Some (base, numbers, quotes) ->
| None -> "" in let numbers =
let quotes = match numbers with
match quotes with | Some s -> sprintf "_{%s}" s
| Some s -> s | None -> "" in
| None -> "" in let quotes =
base, base, numbers^quotes match quotes with
| _ -> name, name, "" | Some s -> s
| None -> "" in
base, base, numbers^quotes
| _ -> name, name, ""
else else
name^string_of_int arity, name, "" in (assert (not is_field);
name^string_of_int arity, name, "") in
record_command_shape name name' arity; record_command_shape name name' arity;
pp_command' ~suffix fmt name pp_command' ~suffix fmt name
let pp_var fmt id = let pp_var' ~arity fmt s =
pp_command fmt ~arity:0 id.id_str pp_command ~arity ~is_field:false fmt s
let pp_str str fmt () = fprintf fmt str let pp_var ~arity fmt id =
pp_var' ~arity fmt id.id_str
let pp_field fmt id =
pp_command ~arity:0 ~is_field:true fmt id.id_str
let pp_str str fmt () =
fprintf fmt str
let pp_command_shape ~comment_macros fmt {name; name'; arity} = let pp_command_shape ~comment_macros fmt {name; name'; arity} =
let rec mk_args acc = function let rec mk_args acc = function
...@@ -131,15 +142,15 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com ...@@ -131,15 +142,15 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
let pp_field pp fmt (qid, x) = let pp_field pp fmt (qid, x) =
fprintf fmt "%a\\texttt{=}%a" fprintf fmt "%a\\texttt{=}%a"
pp_var (id_of_qualid qid) pp x pp_field (id_of_qualid qid)
pp x
let rec pp_type fmt = function let rec pp_type fmt = function
| PTtyvar id -> | PTtyvar id ->
pp_var fmt id pp_var ~arity:0 fmt id
| PTtyapp (qid, ts) -> | PTtyapp (qid, ts) ->
let str = str_of_qualid qid in
let arity = List.length ts in let arity = List.length ts in
fprintf fmt "%a%a" (pp_command ~arity) str fprintf fmt "%a%a" (pp_var ~arity) (id_of_qualid qid)
(pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_type)) ts (pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_type)) ts
| PTtuple ts -> | PTtuple ts ->
fprintf fmt "(%a)" fprintf fmt "(%a)"
...@@ -160,11 +171,10 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com ...@@ -160,11 +171,10 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
| Pwild -> | Pwild ->
fprintf fmt "\\texttt{anything}" fprintf fmt "\\texttt{anything}"
| Pvar id -> | Pvar id ->
fprintf fmt "%a" pp_var id fprintf fmt "%a" (pp_var ~arity:0) id
| Papp (qid, ps) -> | Papp (qid, ps) ->
let str = str_of_qualid qid in
let arity = List.length ps in let arity = List.length ps in
fprintf fmt "%a%a" (pp_command ~arity) str fprintf fmt "%a%a" (pp_var ~arity) (id_of_qualid qid)
(pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_pattern)) ps (pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_pattern)) ps
| Prec fs -> | Prec fs ->
fprintf fmt "\\texttt{\\{}%a\\texttt{\\}}" fprintf fmt "\\texttt{\\{}%a\\texttt{\\}}"
...@@ -172,7 +182,7 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com ...@@ -172,7 +182,7 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
| Ptuple ps -> | Ptuple ps ->
fprintf fmt "(%a)" (pp_print_list ~pp_sep:(pp_str ", ") pp_pattern) ps fprintf fmt "(%a)" (pp_print_list ~pp_sep:(pp_str ", ") pp_pattern) ps
| Pas (p, id, _) -> | Pas (p, id, _) ->
fprintf fmt "%a \\texttt{as} %a" pp_pattern p pp_var id fprintf fmt "%a \\texttt{as} %a" pp_pattern p (pp_var ~arity:0) id
| Por (p1, p2) -> | Por (p1, p2) ->
fprintf fmt "%a \\texttt{|} %a" pp_pattern p1 pp_pattern p2 fprintf fmt "%a \\texttt{|} %a" pp_pattern p1 pp_pattern p2
| Pcast (p, ty) -> | Pcast (p, ty) ->
...@@ -204,7 +214,7 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com ...@@ -204,7 +214,7 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
| Tident qid -> | Tident qid ->
let id = id_of_qualid qid in let id = id_of_qualid qid in
(match sn_decode id.id_str with (match sn_decode id.id_str with
| SNword _ -> pp_var fmt id | SNword _ -> pp_var ~arity:0 fmt id
| _ -> fprintf fmt "(%s)" id.id_str) | _ -> fprintf fmt "(%s)" id.id_str)
| Tinnfix (t1, id, t2) | Tinnfix (t1, id, t2)
| Tinfix (t1, id, t2) -> | Tinfix (t1, id, t2) ->
...@@ -233,7 +243,7 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com ...@@ -233,7 +243,7 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
| SNword s, ts -> | SNword s, ts ->
let arity = List.length ts in let arity = List.length ts in
let pp_args = pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_term) in let pp_args = pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_term) in
fprintf fmt "%a%a" (pp_command ~arity) s pp_args ts fprintf fmt "%a%a" (pp_var' ~arity) s pp_args ts
| SNinfix s, [t1; t2] -> | SNinfix s, [t1; t2] ->
fprintf fmt "%a %s %a" pp_term t1 (sanitize_op s) pp_term t2 fprintf fmt "%a %s %a" pp_term t1 (sanitize_op s) pp_term t2
| SNprefix s, [t] | SNprefix s, [t]
...@@ -259,9 +269,8 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com ...@@ -259,9 +269,8 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
else None else None
with with
| Some (qid, ts) -> | Some (qid, ts) ->
let str = str_of_qualid qid in
let arity = List.length ts in let arity = List.length ts in
fprintf fmt "%a%a" (pp_command ~arity) str fprintf fmt "%a%a" (pp_var ~arity) (id_of_qualid qid)
(pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_term)) ts (pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_term)) ts
| None -> | None ->
fprintf fmt "%a %a" pp_term t1 pp_term t2) fprintf fmt "%a %a" pp_term t1 pp_term t2)
...@@ -274,7 +283,7 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com ...@@ -274,7 +283,7 @@ module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val com
fprintf fmt "\\texttt{if}~%a~\\texttt{then}~%a~\\texttt{else}~%a" fprintf fmt "\\texttt{if}~%a~\\texttt{then}~%a~\\texttt{else}~%a"
pp_term t1 pp_term t2 pp_term t3 pp_term t1 pp_term t2 pp_term t3
| Tlet (id, t1, t2) -> | Tlet (id, t1, t2) ->
fprintf fmt "\\textbf{let}~%a = %a~\\textbf{in}~%a" pp_var id fprintf fmt "\\textbf{let}~%a = %a~\\textbf{in}~%a" (pp_var ~arity:0) id
pp_term t1 pp_term t2 pp_term t1 pp_term t2
| Tquant (_, _, _, t) -> | Tquant (_, _, _, t) ->
pp_term fmt t pp_term fmt t
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment