Adding generic solvers to term holes. For now, no resolution mechanism nor

parsing is plugged.

7 files changed, 41 insertions, 17 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c9280582b..a5e822862 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1920,7 +1920,7 @@ let mk_JMeq typ x typ' y =
   mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |])
 
-let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true))
+let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), None)
 
 let constr_of_pat env evdref arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 4e0fc5de6..c29c443b6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -591,6 +591,8 @@ let rec subst_cases_pattern subst pat =
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (loc,((kn',i),j),cpl',n)
 
+let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
+
 let rec subst_glob_constr subst raw =
   match raw with
   | GRef (loc,ref) ->
@@ -674,14 +676,16 @@ let rec subst_glob_constr subst raw =
 
   | GSort _ -> raw
 
-  | GHole (loc,Evar_kinds.ImplicitArg (ref,i,b)) ->
-      let ref',_ = subst_global subst ref in
-	if ref' == ref then raw else
-	  GHole (loc,Evar_kinds.InternalHole)
-  | GHole (loc, (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _
-		|Evar_kinds.CasesType |Evar_kinds.InternalHole
-		|Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar
-		|Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _)) -> raw
+  | GHole (loc, knd, solve) ->
+    let nknd = match knd with
+    | Evar_kinds.ImplicitArg (ref, i, b) ->
+      let nref, _ = subst_global subst ref in
+      if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
+    | _ -> knd
+    in
+    let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in
+    if nsolve == solve && nknd = knd then raw
+    else GHole (loc, nknd, nsolve)
 
   | GCast (loc,r1,k) ->
       let r1' = subst_glob_constr subst r1 in
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cb478777f..97c636af7 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -60,6 +60,9 @@ val simple_cases_matrix_of_branches :
 val return_type_of_predicate :
   inductive -> int -> glob_constr -> predicate_pattern * glob_constr option
 
+val subst_genarg_hook :
+  (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t
+
 module PrintingInductiveMake :
   functor (Test : sig
     val encode : Libnames.reference -> Names.inductive
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 94ff780ec..b847a1390 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -245,7 +245,7 @@ let loc_of_glob_constr = function
   | GIf (loc,_,_,_,_) -> loc
   | GRec (loc,_,_,_,_,_) -> loc
   | GSort (loc,_) -> loc
-  | GHole (loc,_) -> loc
+  | GHole (loc,_,_) -> loc
   | GCast (loc,_,_) -> loc
 
 (**********************************************************************)
@@ -259,7 +259,7 @@ let rec cases_pattern_of_glob_constr na = function
       raise Not_found
     | Anonymous -> PatVar (loc,Name id)
     end
-  | GHole (loc,_) -> PatVar (loc,na)
+  | GHole (loc,_,_) -> PatVar (loc,na)
   | GRef (loc,ConstructRef cstr) ->
       PatCstr (loc,cstr,[],na)
   | GApp (loc,GRef (_,ConstructRef cstr),l) ->
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 79e3913a9..a2e8e4599 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -340,7 +340,7 @@ let rec pat_of_raw metas vars = function
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (loc,nal,(_,None),b,c) ->
       let mkGLambda c na =
-	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole),c) in
+	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, None),c) in
       let c = List.fold_left mkGLambda c nal in
       let cip =
 	{ cip_style = LetStyle;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 05968b6be..a7e1cf481 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -288,6 +288,8 @@ let pretype_sort evdref = function
 let new_type_evar evdref env loc =
   evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,Evar_kinds.InternalHole)) evdref
 
+let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
+
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
@@ -321,13 +323,24 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
       let k = Evar_kinds.MatchingVar (someta,n) in
 	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-  | GHole (loc,k) ->
+  | GHole (loc, k, None) ->
       let ty =
         match tycon with
         | Some ty -> ty
         | None ->
-	    new_type_evar evdref env loc in
-	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+          new_type_evar evdref env loc in
+        { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+
+  | GHole (loc, k, Some arg) ->
+      let ty =
+        match tycon with
+        | Some ty -> ty
+        | None ->
+          new_type_evar evdref env loc in
+      let ist = snd lvar in
+      let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in
+      let () = evdref := sigma in
+      { uj_val = c; uj_type = ty }
 
   | GRec (loc,fixkind,names,bl,lar,vdef) ->
       let rec type_bl env ctxt = function
@@ -717,7 +730,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
 and pretype_type valcon env evdref lvar = function
-  | GHole loc ->
+  | GHole (loc, knd, None) ->
       (match valcon with
        | Some v ->
            let s =
@@ -733,7 +746,7 @@ and pretype_type valcon env evdref lvar = function
 	       utj_type = s }
        | None ->
 	   let s = evd_comb0 new_sort_variable evdref in
-	     { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
+	     { utj_val = e_new_evar evdref env ~src:(loc, knd) (mkSort s);
 	       utj_type = s})
   | c ->
       let j = pretype empty_tycon env evdref lvar c in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 98306e57f..dd02423a8 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -125,3 +125,7 @@ val constr_out : Dyn.t -> constr
 
 val interp_sort : glob_sort -> sorts
 val interp_elimination_sort : glob_sort -> sorts_family
+
+val genarg_interp_hook :
+  (types -> env -> evar_map -> Genarg.typed_generic_argument Id.Map.t ->
+    Genarg.glob_generic_argument -> constr * evar_map) Hook.t