Merge pull request herd#1738 from herd/aslspec-unlabelled-records

[aslspec] more precise support for unlabelled records

Author: Roman-Manevich

asllib/aslspec/error.ml

@@ -150,11 +150,11 @@ let invalid_number_of_components label expr ~expected ~actual =
 let invalid_record_field_names expr expr_field_names record_type_field_names =
   spec_error
   @@ Format.asprintf
-       "The record expression %a has invalid field names: expected %s but \
-        found %s"
+       "The record expression %a has missing or invalid field names: expected \
+        %s but found %s"
        PP.pp_expr expr
-       (String.concat ", " expr_field_names)
        (String.concat ", " record_type_field_names)
+       (String.concat ", " expr_field_names)
 
 let non_field id expr =
   spec_error

asllib/aslspec/render.ml

@@ -750,15 +750,15 @@ module Make (S : SPEC_VALUE) = struct
               formal_opt_prose_pairs
           in
           substitute expr_prose formal_prose_pairs
-      | Record { label_opt = None; fields = _ } ->
-          (* TODO: to obtain the prose for unlabelled records, we need a map from
-                  record fields to the type that contains the record. *)
-          "<missing prose for unlabelled record>"
-      | Record { label_opt = Some name; fields } ->
-          let variant =
-            match Spec.defining_node_for_id S.spec name with
-            | Node_TypeVariant def -> def
-            | _ -> assert false
+      | Record { label_opt; fields } ->
+          let variant = Spec.record_variant_for_expr S.spec expr in
+          let name =
+            match label_opt with
+            | Some name -> name
+            | None ->
+                Format.asprintf "unlabelled record with fields [%a]"
+                  (PP.pp_sep_list ~sep:", " pp_print_string)
+                  (List.map fst fields)
           in
           let expr_prose =
             TypeVariant.prose_description variant

asllib/aslspec/spec.ml

@@ -235,13 +235,36 @@ let make_variant_id_to_containing_type ast =
         acc_map variants)
     StringMap.empty typedefs
 
+let make_field_to_containing_variant ast =
+  let typedefs =
+    List.filter_map (function Elem_Type def -> Some def | _ -> None) ast
+  in
+  List.fold_left
+    (fun acc_map { Type.variants } ->
+      List.fold_left
+        (fun acc_map ({ TypeVariant.term } as variant) ->
+          match term with
+          | Term.Record { fields } ->
+              let field_names = List.map (fun { Term.name } -> name) fields in
+              List.fold_left
+                (fun acc_map field_name ->
+                  StringMap.add field_name variant acc_map)
+                acc_map field_names
+          | _ -> acc_map)
+        acc_map variants)
+    StringMap.empty typedefs
+
 type t = {
   ast : AST.t;  (** The AST, added with builtin definitions, transformed. *)
   id_to_defining_node : definition_node StringMap.t;
       (** Associates identifiers with the AST nodes where they are defined. *)
   variant_id_to_containing_type : string StringMap.t;
       (** Associates variant labels with the name of the type that contains
           them. *)
+  field_to_containing_variant : TypeVariant.t StringMap.t;
+      (** Associates field names with the variant containing them. Since field
+          names are unique, there is only one variant containing a given field.
+      *)
   assign : Relation.t;
   reverse_assign : Relation.t;
   bottom_constant : Constant.t;
@@ -279,6 +302,7 @@ let update_spec_ast spec ast =
     ast;
     id_to_defining_node = make_symbol_table ast;
     variant_id_to_containing_type = make_variant_id_to_containing_type ast;
+    field_to_containing_variant = make_field_to_containing_variant ast;
   }
 
 let defined_ids self =
@@ -297,13 +321,26 @@ let defining_node_for_id self id =
   | Some def -> def
   | None -> Error.undefined_element id
 
-(** [relation_for_id self id] returns the relation definition node for the given
-    identifier [id], which is assumed to correspond to a relation definition. *)
 let relation_for_id self id =
   match defining_node_for_id self id with
   | Node_Relation def -> def
   | _ -> assert false
 
+let record_variant_for_expr spec expr =
+  match expr with
+  | Expr.Record { fields } ->
+      let first_field_name =
+        match fields with
+        | (field_name, _) :: _ -> field_name
+        | _ -> failwith "Record expression must have a non-empty list of fields"
+      in
+      StringMap.find first_field_name spec.field_to_containing_variant
+  | _ ->
+      let msg =
+        Format.asprintf "Expected record expression, found %a" PP.pp_expr expr
+      in
+      failwith msg
+
 let is_defined_id self id = StringMap.mem id self.id_to_defining_node
 let elements self = self.ast
 
@@ -2351,9 +2388,15 @@ module Check = struct
               in
               Term.Record { label_opt; fields = record_fields }
             in
+            let { TypeVariant.term = declared_type } =
+              record_variant_for_expr spec expr
+            in
             let () =
-              check_subsumed_by_opt_labelled_type spec inferred_type label_opt
-                ~context_expr:expr
+              if
+                not
+                  (CheckTypeInstantiations.subsumed spec inferred_type
+                     declared_type)
+              then Error.type_subsumption_failure inferred_type declared_type
             in
             (inferred_type, type_env)
         | RecordUpdate { record_expr; updates } -> (
@@ -2403,8 +2446,19 @@ module Check = struct
               Term.Tuple { label_opt; args = anonymous_typed_args }
             in
             let () =
-              check_subsumed_by_opt_labelled_type spec inferred_type label_opt
-                ~context_expr:expr
+              match label_opt with
+              | Some label -> (
+                  match StringMap.find label spec.id_to_defining_node with
+                  | Node_TypeVariant { TypeVariant.term = declared_type } ->
+                      if
+                        not
+                          (CheckTypeInstantiations.subsumed spec inferred_type
+                             declared_type)
+                      then
+                        Error.type_subsumption_failure inferred_type
+                          declared_type
+                  | _ -> Error.invalid_labelled_type label ~context_expr:expr)
+              | None -> ()
             in
             (inferred_type, type_env)
         | Relation { is_operator = true; name; args = [ lhs; rhs ] }
@@ -2585,24 +2639,6 @@ module Check = struct
       in
       (List.rev types, type_env)
 
-    (** [check_subsumed_by_opt_labelled_type spec actual_type label_opt
-         ~context_expr] checks that [actual_type] is subsumed by the labelled
-        type indicated by [label_opt], if any. The [context_expr] is used for
-        error reporting. *)
-    and check_subsumed_by_opt_labelled_type spec actual_type label_opt
-        ~context_expr =
-      match label_opt with
-      | Some label -> (
-          match StringMap.find label spec.id_to_defining_node with
-          | Node_TypeVariant { TypeVariant.term = declared_type } ->
-              if
-                not
-                  (CheckTypeInstantiations.subsumed spec actual_type
-                     declared_type)
-              then Error.type_subsumption_failure actual_type declared_type
-          | _ -> Error.invalid_labelled_type label ~context_expr)
-      | None -> ()
-
     and check_arg_types spec arg_exprs arg_types arg_formal_types ~context_expr
         =
       Utils.list_iter3
@@ -2957,29 +2993,31 @@ module Check = struct
                   ~expected:(List.length type_components)
                   ~actual:(List.length args)
           | None -> ())
-      | Record { label_opt; fields } -> (
+      | Record { fields } ->
           let expr_field_names, expr_field_inits = List.split fields in
           let () = check_expr_list_in_context expr_field_inits in
-          match label_opt with
-          | Some label ->
-              let record_type_fields =
-                match StringMap.find label id_to_defining_node with
-                | Node_TypeVariant { TypeVariant.term = Record { fields } } ->
-                    fields
-                | _ -> Error.illegal_lhs_application expr
-              in
-              let record_type_field_names =
-                List.map (fun { Term.name } -> name) record_type_fields
-              in
-              if
-                not
-                  (Utils.list_is_equal String.equal expr_field_names
-                     record_type_field_names)
-              then
-                Error.invalid_record_field_names expr expr_field_names
-                  record_type_field_names
-              else ()
-          | None -> ())
+          let { TypeVariant.term = record_term } =
+            record_variant_for_expr spec expr
+          in
+          let record_type_field_names =
+            match record_term with
+            | Term.Record { fields = record_fields } ->
+                List.map (fun { Term.name } -> name) record_fields
+            | _ -> failwith "Expected record term."
+          in
+          let expr_field_names_sorted =
+            List.sort String.compare expr_field_names
+          in
+          let record_type_field_names_sorted =
+            List.sort String.compare record_type_field_names
+          in
+          if
+            not
+              (Utils.string_list_is_subset expr_field_names
+                 record_type_field_names)
+          then
+            Error.invalid_record_field_names expr expr_field_names_sorted
+              record_type_field_names_sorted
       | RecordUpdate { record_expr; updates } ->
           let () = check_expr_in_context record_expr in
           let update_field_names, update_field_inits = List.split updates in
@@ -3421,6 +3459,7 @@ let make_spec_with_builtins ast =
     some_operator = get_relation "some";
     cond_operator = get_relation "cond_op";
     variant_id_to_containing_type = make_variant_id_to_containing_type ast;
+    field_to_containing_variant = make_field_to_containing_variant ast;
   }
 
 let from_ast ast =

asllib/aslspec/spec.mli

@@ -56,6 +56,10 @@ val relation_for_id : t -> string -> Relation.t
 (** [relation_for_id spec id] returns the relation definition for [id] in
     [spec], assuming it is defined as a relation. *)
 
+val record_variant_for_expr : t -> Expr.t -> TypeVariant.t
+(** [record_variant_for_expr spec expr] returns the record type variant
+    corresponding to [expr], assuming [expr] is a record expression. *)
+
 val is_defined_id : t -> string -> bool
 (** [is_defined_id spec id] returns [true] if [id] is defined in [spec] and
     [false] otherwise. *)

asllib/aslspec/tests.t/rule.expected

@@ -63,6 +63,10 @@ The relation
                                               { \condcase[H]{{ \texttt{a} \greaterthan \texttt{b} }}{{ \texttt{a}\numplus\texttt{b} }} }, \\
                                               { \condcase[H]{{ \texttt{a} \lessthan \texttt{b} }}{\texttt{b}} }
                                               \end{array}} } } } \hva\\
+ { { \texttt{y} \eqdef \left\{\begin{array}{lcl}
+                              \FIELDf & : & \texttt{a}\\
+                              \FIELDg & : & \texttt{b}
+                              \end{array}\right\} } } \hva\\
  { { \texttt{r\_f} \eqdef { \texttt{r}.\FIELDf\numplus\texttt{r}.\FIELDg } } } \hva\\
  { { \texttt{r'} \eqdef \texttt{r}\left\{\begin{array}{lcl}
                                          \FIELDf & : & \texttt{res}
@@ -76,6 +80,7 @@ The relation
 \AllApply
   \begin{itemize}
     \item define \texttt{res} as: if \texttt{a} is equal to \texttt{b} holds then \texttt{a}, if \texttt{a} is greater than \texttt{b} holds then the sum of all numbers in \texttt{a} and \texttt{b}, and if \texttt{a} is less than \texttt{b} holds then \texttt{b};
+    \item define \texttt{y} as: the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b};
     \item define \texttt{r\_f} as: the sum of all numbers in the field $\FIELDf$ of \texttt{r} and the field $\FIELDg$ of \texttt{r};
     \item define \texttt{r'} as: \texttt{r} with $\FIELDf$ updated to \texttt{res};
     \item \textbf{the result is:} the tuple consisting of:  (1) \texttt{res} (for \texttt{c}), and  (2) \texttt{r'}.

asllib/aslspec/tests.t/rule.spec

@@ -1,13 +1,14 @@
 typedef Num;
 
-typedef rec = [f: Num, g: Num];
+typedef rec = [f: Num, g: Num] { "the rec record with $\Fieldf$ value {f} and $\Fieldg$ value {g}" };
 
 typing relation r(a: Num, b: Num, r: rec) -> (c: Num, r': rec) {} =
     res := cond(
         a = b : a,
         a > b : a + b,
         a < b : b
     );
+    y := [f: a, g: b];
     r_f := r.f + r.g; // equivalent to r_f := (r.f + r.g);
     r' := r(f : res); // This is 'r' with its 'f' field updated to 'res'.
     --

asllib/aslspec/utils.ml

@@ -1,5 +1,7 @@
 (** Utility functions for functions that are not available in 4.08. *)
 
+module StringSet = Set.Make (String)
+
 (***************************************
  List-related utilities.
 ***************************************)
@@ -60,6 +62,11 @@ let rec list_iter3 f lst1 lst2 lst3 =
       list_iter3 f t1 t2 t3
   | _ -> invalid_arg "list_iter3: lists have different lengths"
 
+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-related utilities.
 ***************************************)