From 82663b28a04d82e89bd041efd256c4838312e587 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 May 2019 10:03:42 +0200
Subject: Simplify implicit_quantifiers

After removing `Instance : !type` implicit_application is only used in
constrintern. We propagate constant arguments ?allow_partial and
combine_params_freevar.

Also remove unused functions.
---
 interp/constrintern.ml          |  5 +--
 interp/implicit_quantifiers.ml  | 83 ++++++++---------------------------------
 interp/implicit_quantifiers.mli | 17 +--------
 3 files changed, 19 insertions(+), 86 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1a81dc41a1..4c8aff3f2e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -392,9 +392,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
     env {loc;v=na} b' t ty =
   let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
   let ty, ids' =
-    if t then ty, ids else
-      Implicit_quantifiers.implicit_application ids
-	Implicit_quantifiers.combine_params_freevar ty
+    if t then ty, ids
+    else Implicit_quantifiers.implicit_application ids ty
   in
   let ty' = intern_type {env with ids = ids; unb = true} ty in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bac46c2d2f..e8d10488b2 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -66,9 +66,6 @@ let declare_generalizable ~local gen =
 
 let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table
 
-let ids_of_list l =
-  List.fold_right Id.Set.add l Id.Set.empty
-
 let is_global id =
   try ignore (Nametab.locate_extended (qualid_of_ident id)); true
   with Not_found -> false
@@ -105,26 +102,6 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
 
-let ids_of_names l =
-  List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l
-
-let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) =
-  let rec aux bdvars l c = match c with
-      ((CLocalAssum (n, _, c)) :: tl) ->
-	let bound = ids_of_names n in
-	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
-
-    | ((CLocalDef (n, c, t)) :: tl) ->
-        let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in
-	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in
-	  aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl
-
-    | CLocalPattern _ :: tl -> assert false
-    | [] -> bdvars, l
-  in aux bound l binders
-
 let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
   let rec vars bound vs c = match DAst.get c with
     | GVar id ->
@@ -149,7 +126,7 @@ let next_name_away_from na avoid =
   | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon")
   | Name id -> make_fresh avoid (Global.env ()) id
 
-let combine_params avoid fn applied needed =
+let combine_params avoid applied needed =
   let named, applied =
     List.partition
       (function
@@ -167,47 +144,30 @@ let combine_params avoid fn applied needed =
     (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false)
     named
   in
-  let is_unset (_, decl) = match decl with
-  | LocalAssum _ -> true
-  | LocalDef _ -> false
-  in
-  let needed = List.filter is_unset needed in
   let rec aux ids avoid app need =
     match app, need with
-	[], [] -> List.rev ids, avoid
 
-      | app, (_, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need when Id.List.mem_assoc id named ->
+      | _, (_, LocalDef _) :: need -> aux ids avoid app need
+
+      | [], [] -> List.rev ids, avoid
+
+      | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named ->
 	  aux (Id.List.assoc id named :: ids) avoid app need
 
-      | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need ->
+      | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need ->
 	  aux (x :: ids) avoid app need
 
-      | _, (Some cl, _ as d) :: need ->
-	  let t', avoid' = fn avoid d in
-	    aux (t' :: ids) avoid' app need
-
       | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
 
-      | [], (None, _ as decl) :: need ->
-	  let t', avoid' = fn avoid decl in
-	    aux (t' :: ids) avoid' app need
+      | _, (Some _, decl) :: need | [], (None, decl) :: need ->
+        let id' = next_name_away_from (RelDecl.get_name decl) avoid in
+        let t' = CAst.make @@ CRef (qualid_of_ident id',None) in
+        aux (t' :: ids) (Id.Set.add id' avoid) app need
 
       | (x,_) :: _, [] ->
 	  user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
-  in aux [] avoid applied needed
-
-let combine_params_freevar avoid (_, decl) =
-  let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-  (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
-
-let destClassApp cl =
-  let open CAst in
-  let loc = cl.loc in
-  match cl.v with
-    | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst)
-    | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst)
-    | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst)
-    | _ -> raise Not_found
+  in
+  aux [] avoid applied needed
 
 let destClassAppExpl cl =
   let open CAst in
@@ -217,7 +177,7 @@ let destClassAppExpl cl =
     | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst)
     | _ -> raise Not_found
 
-let implicit_application env ?(allow_partial=true) f ty =
+let implicit_application env ty =
   let is_class =
     try
       let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
@@ -230,24 +190,13 @@ let implicit_application env ?(allow_partial=true) f ty =
   match is_class with
   | None -> ty, env
   | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
-    let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+    let avoid = Id.Set.union env (Id.Set.of_list (free_vars_of_constr_expr ty ~bound:env [])) in
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let c = class_info env sigma gr in
     let (ci, rd) = c.cl_context in
-    if not allow_partial then
-      begin
-        let opt_succ x n = match x with
-          | None -> succ n
-          | Some _ -> n
-        in
-        let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
-        let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
-        if not (Int.equal needlen applen) then
-          mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
-      end;
     let pars = List.rev (List.combine ci rd) in
-    let args, avoid = combine_params avoid f par pars in
+    let args, avoid = combine_params avoid par pars in
     CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
 
 let warn_ignoring_implicit_status =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 437fef1753..d28d35f3a1 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -11,22 +11,14 @@
 open Names
 open Glob_term
 open Constrexpr
-open Libnames
 
 val declare_generalizable : local:bool -> lident list option -> unit
 
-val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t
-val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
-
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
 val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
   Id.t list -> Id.t list
 
-val free_vars_of_binders :
-  ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list
-
 (** Returns the generalizable free ids in left-to-right
    order with the location of their first occurrence *)
 
@@ -37,14 +29,7 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
-val combine_params_freevar :
-  Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
-  Constrexpr.constr_expr * Id.Set.t
-
-val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
-    Constrexpr.constr_expr * Id.Set.t) ->
-  constr_expr -> constr_expr * Id.Set.t
+val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t
 
 (* Should be likely located elsewhere *)
 exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
-- 
cgit v1.2.3


From 1c5e2508d6a9604ffd77eff3140a86eafbc672a9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 May 2019 10:54:14 +0200
Subject: Fix #10225 (Instance := {} accepts duplicate fields)

This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.

Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.
---
 interp/constrintern.ml          | 4 ++--
 interp/constrintern.mli         | 4 ++++
 interp/implicit_quantifiers.ml  | 3 ---
 interp/implicit_quantifiers.mli | 4 ----
 4 files changed, 6 insertions(+), 9 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4c8aff3f2e..63c936fa81 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1299,7 +1299,7 @@ let find_pattern_variable qid =
   if qualid_is_ident qid then qualid_basename qid
   else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
 
-let check_duplicate loc fields =
+let check_duplicate ?loc fields =
   let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
   let dups = List.duplicates eq fields in
   match dups with
@@ -1344,7 +1344,7 @@ let sort_fields ~complete loc fields completer =
           try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id
           with Not_found ->
             anomaly (str "Environment corruption for records.") in
-        let () = check_duplicate loc fields in
+        let () = check_duplicate ?loc fields in
         let (end_index,    (* one past the last field index *)
              first_field_index,  (* index of the first field of the record *)
              proj_list)    (* list of projections *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d4bc91f57..2e4d7479a9 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -189,3 +189,7 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b
 
 (** Placeholder for global option, should be moved to a parameter *)
 val get_asymmetric_patterns : unit -> bool
+
+val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit
+(** Check that a list of record field definitions doesn't contain
+    duplicates. *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e8d10488b2..32290f0430 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -23,9 +23,6 @@ open Libobject
 open Nameops
 open Context.Rel.Declaration
 
-exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
-let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m))
-
 module RelDecl = Context.Rel.Declaration
 (*i*)
 
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d28d35f3a1..8536a2dee0 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -30,7 +30,3 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t
-
-(* Should be likely located elsewhere *)
-exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
-val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a
-- 
cgit v1.2.3