Merge pull request #1740 from herd/aslspec-fixes

[aslspec] fixes

Author: Roman-Manevich

asllib/aslspec/render.ml

@@ -674,7 +674,7 @@ module Make (S : SPEC_VALUE) = struct
         missing prose templates. *)
     let prose_or_empty_message ~name prose =
       if Utils.string_is_empty prose then
-        Format.asprintf "<empty prose for %s>"
+        Format.asprintf "``empty prose for %s''"
           (Latex.spec_var_to_latex_var ~font_type:TextTT name)
       else prose
 
@@ -689,6 +689,15 @@ module Make (S : SPEC_VALUE) = struct
     *)
     let var_to_prose id = spec_var_to_latex_var ~font_type:TextTT id
 
+    (** Removes angle brackets from the template and substitutes the
+        placeholders with the provided substitutions. *)
+    let preprocess_template_and_substitute template substitutions =
+      (* Replace text inside angle brackets with the text itself. *)
+      let template =
+        Str.global_replace (Str.regexp "<\\([^>]*\\)>") "\\1" template
+      in
+      substitute template substitutions
+
     (** [expr_to_prose expr] converts an expression [expr] to its prose
         representation. *)
     let rec expr_to_prose expr =
@@ -749,7 +758,7 @@ module Make (S : SPEC_VALUE) = struct
                 | Some name -> Some (name, prose))
               formal_opt_prose_pairs
           in
-          substitute expr_prose formal_prose_pairs
+          preprocess_template_and_substitute expr_prose formal_prose_pairs
       | Record { label_opt; fields } ->
           let variant = Spec.record_variant_for_expr S.spec expr in
           let name =
@@ -764,12 +773,33 @@ module Make (S : SPEC_VALUE) = struct
             TypeVariant.prose_description variant
             |> prose_or_empty_message ~name
           in
+          let declared_fields =
+            match variant.term with
+            | Record { fields } -> fields
+            | _ -> assert false
+          in
+          (* A record expression is allowed to specify only a subset of the declared fields.
+             We figure those out, associate them with _, and append them to the explicitly
+             specified fields.
+          *)
+          let unspecified_defaults =
+            let declared_field_names =
+              List.map (fun field -> field.Term.name) declared_fields
+            in
+            let unspecified_fields =
+              Utils.string_list_difference declared_field_names
+                (List.map fst fields)
+            in
+            List.map
+              (fun field -> (field, Expr.Var Spec.ignore_var))
+              unspecified_fields
+          in
           let field_to_prose =
             List.map
               (fun (field, field_expr) -> (field, expr_to_prose field_expr))
-              fields
+              (fields @ unspecified_defaults)
           in
-          substitute expr_prose field_to_prose
+          preprocess_template_and_substitute expr_prose field_to_prose
       | RecordUpdate { record_expr; updates } ->
           let record_prose = expr_to_prose record_expr in
           let updates_prose =
@@ -837,7 +867,7 @@ module Make (S : SPEC_VALUE) = struct
                 relation.name
         in
         let formal_prose_pair = [ (formal_arg_name, args_prose) ] in
-        substitute expr_prose formal_prose_pair
+        preprocess_template_and_substitute expr_prose formal_prose_pair
       else
         let formal_arg_pairs = List.combine formal_args args in
         let formal_prose_pairs =
@@ -846,7 +876,7 @@ module Make (S : SPEC_VALUE) = struct
               named_args_for_opt_named_term opt_named_term arg)
             formal_arg_pairs
         in
-        substitute expr_prose formal_prose_pairs
+        preprocess_template_and_substitute expr_prose formal_prose_pairs
 
     (** [short_circuit_to_prose relation_name short_circuit] returns the prose
         for the short-circuit expressions added as superscripts. *)
@@ -956,6 +986,14 @@ module Make (S : SPEC_VALUE) = struct
         "one of the following applies". *)
       pp_prose_rule_elements fmt ~case_name:"" rule_elements
 
+    (** [pp_render_rule_math_and_prose fmt def] renders both the mathematical
+        inference rules and the prose description of the rules referenced by
+        [def] with the formatter [fmt]. *)
+    let pp_render_rule_math_and_prose fmt def =
+      pp_render_rule fmt def;
+      fprintf fmt "@.@.";
+      pp_render_rule_prose fmt def
+
     (** [pp_render_rule_macro fmt def] renders the LaTeX wrapper macro
         [\DefineRule{name}{...}] around the rendering of the mathematical
         inference rules referenced by [def] with the formatter [fmt]. *)
@@ -1010,7 +1048,7 @@ module Make (S : SPEC_VALUE) = struct
     | Elem_Type def -> pp_type_definition fmt def
     | Elem_Relation def -> pp_relation_definition fmt def
     | Elem_RenderTypes def -> RenderTypeSubsets.pp_render_types fmt def
-    | Elem_RenderRule def -> RenderRule.pp_render_rule fmt def
+    | Elem_RenderRule def -> RenderRule.pp_render_rule_math_and_prose fmt def
 
   (** [pp_elem_definition_macro fmt elem] renders a macro definition for an
       element of the specification. *)
@@ -1042,28 +1080,9 @@ module Make (S : SPEC_VALUE) = struct
             Latex.spec_var_to_latex_var ~font_type:Latex.Text name
           in
           match elem with
-          | Elem_Constant _ ->
-              fprintf fmt {|
-\section*{%s}
-%a
-|} latex_name pp_elem elem
-          | Elem_Relation _ ->
-              if is_operator elem then ()
-              else fprintf fmt {|
-\section*{%s}
-%a
-|} latex_name pp_elem elem
-          | Elem_Type _ ->
-              fprintf fmt {|
-\section*{%s}
-%a
-|} latex_name pp_elem elem
-          | Elem_RenderTypes _ ->
-              fprintf fmt {|
-\section*{%s}
-%a
-|} latex_name pp_elem elem
-          | Elem_RenderRule _ ->
+          | Elem_Relation _ when is_operator elem -> ()
+          | Elem_Constant _ | Elem_Type _ | Elem_RenderTypes _
+          | Elem_RenderRule _ | Elem_Relation _ ->
               fprintf fmt {|
 \section*{%s}
 %a

asllib/aslspec/spec.ml

@@ -1478,9 +1478,10 @@ module Check = struct
       (* Filters out identifiers that are definitely not variables. *)
       let is_non_var id =
         match StringMap.find_opt id id_to_defining_node with
-        | Some (Node_Constant _) | Some (Node_TypeVariant _) ->
-            (* Constants and variant labels are not variables. *)
+        | Some (Node_Constant _) | Some (Node_TypeVariant { term = Label _ }) ->
+            (* Constants and label variant are not variables. *)
             true
+        | Some (Node_TypeVariant _)
         | Some (Node_Type _)
         | Some (Node_RecordField _)
         | Some (Node_Relation _)

asllib/aslspec/utils.ml

@@ -62,11 +62,20 @@ let rec list_iter3 f lst1 lst2 lst3 =
       list_iter3 f t1 t2 t3
   | _ -> invalid_arg "list_iter3: lists have different lengths"
 
+(** [string_list_is_subset lst1 lst2] checks if all elements of [lst1] are
+    contained in [lst2]. *)
 let string_list_is_subset lst1 lst2 =
   let set1 = StringSet.of_list lst1 in
   let set2 = StringSet.of_list lst2 in
   StringSet.subset set1 set2
 
+(** [string_list_difference lst1 lst2] returns the list of elements that are in
+    [lst1] but not in [lst2]. *)
+let string_list_difference lst1 lst2 =
+  let set1 = StringSet.of_list lst1 in
+  let set2 = StringSet.of_list lst2 in
+  StringSet.elements (StringSet.diff set1 set2)
+
 (***************************************
  String-related utilities.
 ***************************************)

asllib/doc/asl.spec

@@ -6962,7 +6962,7 @@ typing function to_well_constrained(t: ty) ->
 
   case t_int_other {
     t =: T_Int(i);
-    i != Parameterized;
+    i != Parameterized(_);
     --
     t;
   }