Change QuestionMark for better record field missing error message.

While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.

This is used to provide better error messages on missing record
fields.

1 files changed, 25 insertions, 6 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 18d6c1a5b..f7a1f3bf3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -566,7 +566,11 @@ let term_of_name = function
   | Name id -> DAst.make (GVar id)
   | Anonymous ->
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
-       DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), IntroAnonymous, None))
+       DAst.make (GHole (Evar_kinds.QuestionMark {
+           Evar_kinds.qm_obligation=st;
+           Evar_kinds.qm_name=Anonymous;
+           Evar_kinds.qm_record_field=None;
+      }, IntroAnonymous, None))
 
 let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
  | Anonymous -> (renaming,env), None, Anonymous
@@ -1370,7 +1374,8 @@ let sort_fields ~complete loc fields completer =
                (* the order does not matter as we sort them next,
                   List.rev_* is just for efficiency *)
                let remaining_fields =
-                 let complete_field (idx, _field_ref) = (idx, completer idx) in
+                 let complete_field (idx, field_ref) = (idx,
+                 completer idx field_ref record.Recordops.s_CONST) in
                  List.rev_map complete_field remaining_projs in
                List.rev_append remaining_fields acc
         in
@@ -1524,7 +1529,7 @@ let drop_notations_pattern looked_for genv =
     | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
     | CPatRecord l ->
       let sorted_fields =
-	sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in
+        sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in
       begin match sorted_fields with
 	| None -> DAst.make ?loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
@@ -1918,8 +1923,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
-                                                           IntroAnonymous, None))
+                     (fun _idx fieldname constructorname ->
+                         let open Evar_kinds in
+                         let fieldinfo : Evar_kinds.record_field =
+                             {fieldname=fieldname; recordname=inductive_of_constructor constructorname}
+                             in
+                         CAst.make ?loc @@ CHole (Some
+                 (Evar_kinds.QuestionMark {
+                     Evar_kinds.qm_obligation=st;
+                     Evar_kinds.qm_name=Anonymous;
+                     Evar_kinds.qm_record_field=Some fieldinfo
+                             }) , IntroAnonymous, None))
        in
        begin
 	  match fields with
@@ -2002,7 +2016,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
            (match naming with
            | IntroIdentifier id -> Evar_kinds.NamedHole id
-           | _ -> Evar_kinds.QuestionMark (st,Anonymous))
+           | _ -> Evar_kinds.QuestionMark
+           {
+               Evar_kinds.qm_obligation=st;
+           Evar_kinds.qm_name=Anonymous;
+           Evar_kinds.qm_record_field=None;
+        })
         | Some k -> k
         in
         let solve = match solve with