Registering strict implicit arguments systematically.

2 files changed, 58 insertions, 28 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index d88d6f1066..e3c5c84b02 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -268,6 +268,9 @@ let compute_implicits_names env t =
   let _, impls = compute_implicits_gen false false false false true env t in
   List.map fst impls
 
+let compute_implicits_strict env t =
+  List.map snd (snd (compute_implicits_gen true true true true false env t))
+
 (* Extra information about implicit arguments *)
 
 type maximal_insertion = bool (* true = maximal contextual insertion *)
@@ -393,14 +396,16 @@ let set_manual_implicits env flags enriching autoimps l =
   merge 1 l autoimps
 
 let compute_semi_auto_implicits env f manual t =
-  match manual with
+  let strictimpls = compute_implicits_strict env t in
+  let auto = match manual with
   | [] ->
       if not f.auto then [DefaultImpArgs, []]
       else let _,l = compute_implicits_flags env f false t in
 	     [DefaultImpArgs, prepare_implicits f l]
   | _ ->
       let _,autoimpls = compute_auto_implicits env f f.auto t in
-      [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
+      [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] in
+  strictimpls,auto
 
 (*s Constants. *)
 
@@ -483,9 +488,21 @@ type implicit_discharge_request =
 
 let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
 
+let strict_implicits_of_global n ref =
+  try
+    let impls = fst (Refmap.find ref !implicits_table) in
+    let status = List.map (function
+    | Some (DepRigid (Hyp k) | DepFlexAndRigid (_,Hyp k)) -> k <= n
+    | _ -> false) impls in
+    let m = List.length status in
+    if m > n then fst (List.chop n status)
+    else if m < n then status @ List.make (n-m) false
+    else status
+  with Not_found -> anomaly (str "No strict implicit arguments." ++ Nametab.pr_global_env Idset.empty ref)
+
 let implicits_of_global ref =
   try
-    let l = Refmap.find ref !implicits_table in
+    let l = snd (Refmap.find ref !implicits_table) in
     try
       let rename_l = Arguments_renaming.arguments_names ref in
       let rename imp name = match imp, name with
@@ -513,14 +530,14 @@ let subst_implicits (subst,(req,l)) =
 
 let impls_of_context ctx =
   let map (id, impl, _, _) = match impl with
-  | Implicit -> Some (id, Manual, (true, true))
-  | _ -> None
+  | Implicit -> Some (* dummy *) Manual, Some (id, Manual, (true, true))
+  | _ -> None, None
   in
   let is_set (_, _, b, _) = match b with
   | None -> true
   | Some _ -> false
   in
-  List.rev_map map (List.filter is_set ctx)
+  List.split (List.rev_map map (List.filter is_set ctx))
 
 let section_segment_of_reference = function
   | ConstRef con -> pi1 (section_segment_of_constant con)
@@ -543,26 +560,33 @@ let discharge_implicits (_,(req,l)) =
     (try
       let vars = section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
-      let extra_impls = impls_of_context vars in
-      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+      let extrastrict, extra_impls = impls_of_context vars in
+      let oldstrict,oldimpls = snd (List.hd l) in
+      let newstrict = extrastrict @ oldstrict in
+      let newimpls = List.map (add_section_impls vars extra_impls) oldimpls in
+      let l' = [ref',(newstrict,newimpls)] in
       Some (ImplInteractive (ref',flags,exp),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
     (try
       let con' = pop_con con in
       let vars,_,_ = section_segment_of_constant con in
-      let extra_impls = impls_of_context vars in
-      let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
-      let l' = [ConstRef con',newimpls] in
+      let extrastrict, extra_impls = impls_of_context vars in
+      let oldstrict,oldimpls = snd (List.hd l) in
+      let newstrict = extrastrict @ oldstrict in
+      let newimpls = List.map (add_section_impls vars extra_impls) oldimpls in
+      let l' = [ConstRef con',(newstrict,newimpls)] in
 	Some (ImplConstant (con',flags),l')
     with Not_found -> (* con not defined in this section *) Some (req,l))
   | ImplMutualInductive (kn,flags) ->
     (try
-      let l' = List.map (fun (gr, l) ->
+      let l' = List.map (fun (gr, (newstrict,l)) ->
 	let vars = section_segment_of_reference gr in
-	let extra_impls = impls_of_context vars in
+        let extrastrict, extra_impls = impls_of_context vars in
+        let newstrict = extrastrict @ newstrict in
+        let newimpls = List.map (add_section_impls vars extra_impls) l in
 	((if isVarRef gr then gr else pop_global_reference gr),
-	 List.map (add_section_impls vars extra_impls) l)) l
+	 (newstrict,newimpls))) l
       in
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
@@ -571,15 +595,16 @@ let rebuild_implicits (req,l) =
   match req with
   | ImplLocal -> assert false
   | ImplConstant (con,flags) ->
-      let oldimpls = snd (List.hd l) in
-      let newimpls = compute_constant_implicits flags [] con in
-      req, [ConstRef con, List.map2 merge_impls oldimpls newimpls]
+      let _,oldimpls = snd (List.hd l) in
+      let newstrict,newimpls = compute_constant_implicits flags [] con in
+      req, [ConstRef con, (newstrict,List.map2 merge_impls oldimpls newimpls)]
   | ImplMutualInductive (kn,flags) ->
       let newimpls = compute_all_mib_implicits flags [] kn in
       let rec aux olds news =
 	match olds, news with
-	| (_, oldimpls) :: old, (gr, newimpls) :: tl ->
-	    (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl
+	| (_, (_,oldimpls)) :: old, (gr, (newstrict,newimpls)) :: tl ->
+	    (gr, (newstrict,List.map2 merge_impls oldimpls newimpls))
+            :: aux old tl
 	| [], [] -> []
 	| _, _ -> assert false
       in req, aux l newimpls
@@ -588,18 +613,19 @@ let rebuild_implicits (req,l) =
       (if isVarRef ref && is_in_section ref then ImplLocal else req),
       match o with
       | ImplAuto ->
-	  let oldimpls = snd (List.hd l) in
-	  let newimpls = compute_global_implicits flags [] ref in
-	    [ref,List.map2 merge_impls oldimpls newimpls]
+	  let _,oldimpls = snd (List.hd l) in
+	  let newstrict,newimpls = compute_global_implicits flags [] ref in
+	    [ref,(newstrict,List.map2 merge_impls oldimpls newimpls)]
       | ImplManual userimplsize ->
-	  let oldimpls = snd (List.hd l) in
+	  let _,oldimpls = snd (List.hd l) in
+	  let newstrict,newimpls = compute_global_implicits flags [] ref in
+          let newimpls = List.hd newimpls in
 	  if flags.auto then
-	    let newimpls = List.hd (compute_global_implicits flags [] ref) in
 	    let p = List.length (snd newimpls) - userimplsize in
 	    let newimpls = on_snd (List.firstn p) newimpls in
-	    [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
+	    [ref,(newstrict,List.map (fun o -> merge_impls o newimpls) oldimpls)]
 	  else
-	    [ref,oldimpls]
+	    [ref,(newstrict,oldimpls)]
 
 let classify_implicits (req,_ as obj) = match req with
 | ImplLocal -> Dispose
@@ -607,7 +633,8 @@ let classify_implicits (req,_ as obj) = match req with
 
 type implicits_obj =
     implicit_discharge_request *
-      (global_reference * implicits_list list) list
+      (global_reference *
+         (implicit_explanation option list * implicits_list list)) list
 
 let inImplicits : implicits_obj -> obj =
   declare_object {(default_object "IMPLICITS") with
@@ -692,11 +719,12 @@ let declare_manual_implicits local ref ?enriching l =
 	List.map (fun (imps,n) ->
 	  (LessArgsThan (nargs-n),
 	   set_manual_implicits env flags enriching autoimpls imps)) l in
+  let strictimpls = compute_implicits_strict env t in
   let req =
     if is_local local ref then ImplLocal
     else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
   in
-    add_anonymous_leaf (inImplicits (req,[ref,l']))
+    add_anonymous_leaf (inImplicits (req,[ref,(strictimpls,l')]))
 
 let maybe_declare_manual_implicits local ref ?enriching l =
   match l with
diff --git a/library/impargs.mli b/library/impargs.mli
index 297145f09c..3ba9285085 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -120,6 +120,8 @@ val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool
 
 val implicits_of_global : global_reference -> implicits_list list
 
+val strict_implicits_of_global : int -> global_reference -> bool list
+
 val extract_impargs_data :
   implicits_list list -> ((int * int) option * implicit_status list) list