[aslspec] prose generation

Author: Roman-Manevich

asllib/aslspec/builtins.spec

@@ -1,20 +1,22 @@
-operator cond_case[T](Bool, T) -> T
+operator cond_case[T](c: Bool, r: T) -> T
 {
   math_macro = \condcase,
   custom = true,
+  prose_application = "if {c} holds then {r}",
 };
 
 // TODO: add a custom rendering where all conditions
 // and all values are properly aligned.
 // Perhaps this can be achieved by adding a raw attribute to macros, which doesn't wrap them with braces.
 // TODO: add custom syntac for cases.
-variadic operator cond_op[T](list1(T)) -> T
+variadic operator cond_op[T](cases: list1(T)) -> T
 {
   math_macro = \condop,
   custom = true,
+  prose_application = "{cases}",
 };
 
-constant bot { "bottom", math_macro = \bot };
+constant bot { "the bottom value", math_macro = \bot };
 
 constant None { "the empty \optionalterm{}" };
 
@@ -74,39 +76,45 @@ operator some[T](T) -> option(T)
 operator assign[T](lhs: T, rhs: T) -> Bool
 {
   math_macro = \eqdef,
+  prose_application = "define {lhs} as {rhs}",
 };
 
 operator reverse_assign[T](lhs: T, rhs: T) -> Bool
 {
-  math_macro = \eqname,
+  math_macro = \reverseeqdef,
+  prose_application = "{lhs} is {rhs}",
 };
 
 operator equal[T](a: T, b: T) -> (c: Bool)
 {
   math_macro = \equal,
-  prose_application = "equating {a} to {b} yields {c}",
+  prose_application = "{a} is equal to {b}",
 };
 
-operator not_equal[T](T, T) -> Bool
+operator not_equal[T](a: T, b: T) -> Bool
 {
   math_macro = \notequal,
+  prose_application = "{a} is not equal to {b}",
 };
 
-operator if_then_else[T](Bool, T, T) -> T
+operator if_then_else[T](c: Bool, r_true: T, r_false: T) -> T
 {
   math_macro = \ifthenelseop,
+  prose_application = "if {c} then {r_true} else {r_false}"
 };
 
-variadic operator and(list1(Bool)) -> Bool
+variadic operator and(conjuncts: list1(Bool)) -> Bool
 {
   associative = true,
   math_macro = \land,
+  prose_application = "all of the following hold: {conjuncts}"
 };
 
-variadic operator or(list1(Bool)) -> Bool
+variadic operator or(disjuncts: list1(Bool)) -> Bool
 {
   associative = true,
   math_macro = \lor,
+  prose_application = "one of the following holds: {disjuncts}"
 };
 
 operator list_and(list0(Bool)) -> Bool
@@ -119,16 +127,18 @@ operator list_or(list0(Bool)) -> Bool
   math_macro = \listor,
 };
 
-operator not(Bool) -> Bool
+operator not(b: Bool) -> Bool
 {
   math_macro = \opnot,
+  prose_application = "the logical negation of {b}",
 };
 
 // This is negation, specialized to a single variable to allow
 // the macro to drop the parenthesis around the variable.
-operator not_single(Bool) -> Bool
+operator not_single(b: Bool) -> Bool
 {
   math_macro = \opnotvar,
+  prose_application = "the logical negation of {b}",
 };
 
 operator iff(Bool, Bool) -> Bool
@@ -141,15 +151,17 @@ operator implies(Bool, Bool) -> Bool
   math_macro = \implies,
 };
 
-variadic operator num_plus[NumType](list1(NumType)) -> NumType
+variadic operator num_plus[NumType](addends: list1(NumType)) -> NumType
 {
   associative = true,
   math_macro = \numplus,
+  prose_application = "the addition of {addends}"
 };
 
-operator num_minus[NumType](NumType, NumType) -> NumType
+operator num_minus[NumType](a: NumType, b: NumType) -> NumType
 {
   math_macro = \numminus,
+  prose_application = "{a} minus {b}",
 };
 
 operator num_negate[NumType](NumType) -> NumType
@@ -158,9 +170,10 @@ operator num_negate[NumType](NumType) -> NumType
 };
 
 // Negation for number types.
-operator negate[NumType](NumType) -> NumType
+operator negate[NumType](n: NumType) -> NumType
 {
   math_macro = \negate,
+  prose_application = "the negation of {n}"
 };
 
 variadic operator num_times[NumType](list1(NumType)) -> NumType

asllib/aslspec/latex.ml

@@ -3,6 +3,7 @@
 open Format
 open AST
 open LayoutUtils
+module StringMap = Map.Make (String)
 
 let regex_underscore = Str.regexp_string "_"
 let regexp_spaces_segment = Str.regexp "[ \t]+"
@@ -72,12 +73,27 @@ let elem_name_to_math_macro elem_name =
 let pp_comma = fun fmt () -> fprintf fmt ", "
 let pp_noop = fun _fmt () -> ()
 
+let substitute template bindings =
+  let substitutions_map =
+    List.fold_left
+      (fun acc_map (var_str, replacement) ->
+        let template_var = spec_var_to_template_var var_str in
+        StringMap.add template_var replacement acc_map)
+      StringMap.empty bindings
+  in
+  let template_var_regexp = Str.regexp "{[a-zA-Z0-9_']+}" in
+  Utils.string_replace_all template_var_regexp
+    (fun var ->
+      match StringMap.find_opt var substitutions_map with
+      | Some replacement -> replacement
+      | None -> var)
+    template
+
 (** [substitute_spec_vars_by_latex_vars math_mode s vars] returns a string [s]
     with every instance of [{my_var}] substituted by [\texttt{my\_var}]. If
     [math_mode] is true [{my_var}] is substituted by [$\texttt{my\_var}$]. This
     makes the returned string suitable to typesetting with LaTeX. *)
 let substitute_spec_vars_by_latex_vars ~math_mode str vars =
-  let module StringMap = Map.Make (String) in
   (* Create a map from template variables to LaTeX variables
     to make replacement efficient. *)
   let substitutions_map =
@@ -282,3 +298,13 @@ let pp_fields pp_field_name pp_field_value fmt (fields, layout) =
         (PP.pp_sep_list ~sep:", " pp_field)
         fmt fields_values_with_layouts
   | Unspecified -> assert false
+
+(** [pp_itemized_list pp_elem fmt elements] formats a LaTeX itemized list of
+    [elements], where each element is formatted using [pp_elem]. *)
+let pp_itemized_list pp_elem fmt elements =
+  let pp_item pp_elem fmt element = fprintf fmt "\\item %a" pp_elem element in
+  fprintf fmt "@[<v>\\begin{itemize}@;<0 2>%a@;<0 0>\\end{itemize}@]"
+    (pp_print_list
+       ~pp_sep:(fun fmt () -> fprintf fmt "@;<0 2>")
+       (pp_item pp_elem))
+    elements