(fix) Better type errors when constructing concepts

Signed-off-by: Jerome Simeon <[email protected]>

mechanization/Backend/Lib/ECType.v

@@ -116,5 +116,67 @@ Module ECType(ergomodel:ErgoBackendModel).
 
   Definition ergoc_type_unpack {br:brand_relation} (t:ectype) : ectype_struct := proj1_sig t.
 
+  Program Definition ergoc_closed_from_open {m:brand_model} (t:ectype) : ectype :=
+    match untrec t with
+    | None => t
+    | Some (k, fields) => Rec Closed fields _
+    end.
+  Next Obligation.
+    assert (untrec t0 = Some (k, fields)) by auto; clear Heq_anonymous.
+    generalize (tunrec_correct k t0 H); intros.
+    elim H0; clear H0; intros.
+    auto.
+  Qed.
+
+  (* Stricter version of brand typing -- checks that t is a subtype of the closed form for type of b *)
+  Definition infer_brand_strict {m:brand_model} (b:brands) (t:ectype) : option (rtype * ectype) :=
+    if (subtype_dec t (ergoc_closed_from_open (brands_type b)))
+    then Some (Brand b, t)
+    else None.
+
+  Definition recminus {br:brand_relation} (rt:list (string*rtype)) (sl:list string) : list (string*rtype) :=
+    fold_left rremove sl rt.
+
+  (* Returns a pair with: fields in the expected brand not in the actual record + fields in the actual record not in the expected brand *)
+  Definition diff_record_types {m:brand_model} (b:brands) (t:ectype) : option (list string * list string) :=
+    match tunrec t with
+    | None => None
+    | Some (_, actual_rt) =>
+      match tunrec (ergoc_closed_from_open (brands_type b)) with
+      | None => None
+      | Some (_, expected_rt) =>
+        let in_expected_not_in_actual := recminus expected_rt (map fst actual_rt) in
+        let in_actual_not_in_expected := recminus actual_rt (map fst expected_rt) in
+        Some (map fst in_expected_not_in_actual, map fst in_actual_not_in_expected)
+      end
+    end.
+
+  Fixpoint rec_fields_that_are_not_subtype {m:brand_model} (t1 t2:list (string*ectype)) : list (string * ectype * ectype) :=
+    match t1, t2 with
+    | nil, _ => nil
+    | _, nil => nil
+    | (name1,t1)::rest1, (name2,t2)::rest2 =>
+      if string_dec name1 name2
+      then
+        if subtype_dec t2 t1
+        then
+          rec_fields_that_are_not_subtype rest1 rest2
+        else
+          (name1, t1, t2) :: rec_fields_that_are_not_subtype rest1 rest2
+      else
+        rec_fields_that_are_not_subtype rest1 rest2
+    end.
+
+  Definition fields_that_are_not_subtype {m:brand_model} (b:brands) (t:ectype) : list (string * ectype * ectype) :=
+    match tunrec t with
+    | None => nil
+    | Some (_, actual_rt) =>
+      match tunrec (ergoc_closed_from_open (brands_type b)) with
+      | None => nil
+      | Some (_, expected_rt) =>
+        rec_fields_that_are_not_subtype expected_rt actual_rt
+      end
+    end.
+
 End ECType.
 

mechanization/ErgoC/Lang/ErgoCType.v

@@ -81,6 +81,30 @@ Section ErgoCType.
     | _ => "This operator received unexpected arguments of type `" ++ (ergoc_type_to_string nsctxt arg1) ++ "' " ++ " and `" ++ (ergoc_type_to_string nsctxt arg2) ++ "'."
     end.
 
+  Definition ergo_format_new_error nsctxt (name:string) (actual:ergoc_type) : string :=
+    let concept_name := ergoc_type_to_string nsctxt (Brand (name::nil)) in
+    (* First check if all the fields are present and no extra field is present *)
+    match diff_record_types (name::nil) actual with
+    | None => "Concept name " ++ name ++ " does not match data"
+    | Some (nil, nil) =>
+      (* If all the fields are right, check if any of them is not a subtype *)
+      match fields_that_are_not_subtype (name::nil) actual with
+      | nil => "Concept " ++ name ++ " doesn't match data (one field is not a subtype)"
+      | (expected_name, expected_type, actual_type) :: _ =>
+        "Field `" ++ expected_name
+                  ++ "' has type `" ++ (ergoc_type_to_string nsctxt actual_type)
+                  ++ "' but should have type `" ++ (ergoc_type_to_string nsctxt expected_type) ++ "'"
+      end
+    | Some (nil, actual_name::nil) =>
+      "Unexpected field `" ++ actual_name ++ "' in type `" ++ concept_name ++ "'"
+    | Some (nil, actual_names) =>
+      "Unexpected fields `" ++ String.concat "', `" actual_names ++ "' in type `" ++ concept_name ++ "'"
+    | Some (expected_name::nil, _) =>
+      "Missing field `" ++ expected_name ++ "' in type `" ++ concept_name ++ "'"
+    | Some (expected_names, _) =>
+      "Missing fields `" ++ String.concat "', `" expected_names ++ "' in type `" ++ concept_name ++ "'"
+    end.
+
   Fixpoint ergo_type_expr nsctxt (ctxt : type_context) (expr : ergoc_expr) : eresult ergoc_type :=
     match expr with
     | EThisContract prov => efailure (ESystemError prov "No `this' in ergoc")
@@ -198,9 +222,8 @@ Section ErgoCType.
         (fun rs' =>
            (elift fst)
              (eresult_of_option
-                (ergoc_type_infer_unary_op
-                   (OpBrand (name::nil)) rs')
-                (ETypeError prov ("Concept name " ++ name ++ " doesn't match data")%string)))
+                (infer_brand_strict (name::nil) rs')
+                (ETypeError prov (ergo_format_new_error nsctxt name rs'))))
         (fold_left
            (fun sofar next =>
               eolift2