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

parsing is plugged.

6 files changed, 48 insertions, 30 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 5edfc06141..c8a0e56385 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -235,7 +235,7 @@ let constr_loc = function
   | CCases (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
-  | CHole (loc, _) -> loc
+  | CHole (loc, _, _) -> loc
   | CPatVar (loc,_) -> loc
   | CEvar (loc,_,_) -> loc
   | CSort (loc,_) -> loc
@@ -332,14 +332,14 @@ let coerce_to_id = function
 
 let coerce_to_name = function
   | CRef (Ident (loc,id)) -> (loc,Name id)
-  | CHole (loc,_) -> (loc,Anonymous)
+  | CHole (loc,_,_) -> (loc,Anonymous)
   | a -> Errors.user_err_loc
         (constr_loc a,"coerce_to_name",
          str "This expression should be a name.")
 
 let rec raw_cases_pattern_expr_of_glob_constr looked_for = function
   | GVar (loc,id) -> RCPatAtom (loc,Some id)
-  | GHole (loc,_) -> RCPatAtom (loc,None)
+  | GHole (loc,_,_) -> RCPatAtom (loc,None)
   | GRef (loc,g) ->
     looked_for g;
     RCPatCstr (loc, g,[],[])
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 741ef9853a..ffb8a46ea1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -597,13 +597,13 @@ let rec extern inctx scopes vars r =
 
   | GVar (loc,id) -> CRef (Ident (loc,id))
 
-  | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
+  | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None, None)
 
   | GEvar (loc,n,l) ->
       extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
 
   | GPatVar (loc,n) ->
-      if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n)
+      if !print_meta_as_hole then CHole (loc, None, None) else CPatVar (loc,n)
 
   | GApp (loc,f,args) ->
       (match f with
@@ -748,7 +748,7 @@ let rec extern inctx scopes vars r =
 
   | GSort (loc,s) -> CSort (loc,extern_glob_sort s)
 
-  | GHole (loc,e) -> CHole (loc, Some e)
+  | GHole (loc,e,_) -> CHole (loc, Some e, None) (** TODO: extern tactics. *)
 
   | GCast (loc,c, c') ->
       CCast (loc,sub_extern true scopes vars c,
@@ -932,7 +932,7 @@ let extern_sort s = extern_glob_sort (detype_sort s)
 
 let any_any_branch =
   (* | _ => _ *)
-  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole))
+  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,None))
 
 let rec glob_of_pat env = function
   | PRef ref -> GRef (loc,ref)
@@ -945,7 +945,7 @@ let rec glob_of_pat env = function
 	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable")
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar (loc,id)
-  | PMeta None -> GHole (loc,Evar_kinds.InternalHole)
+  | PMeta None -> GHole (loc,Evar_kinds.InternalHole, None)
   | PMeta (Some n) -> GPatVar (loc,(false,n))
   | PApp (f,args) ->
       GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b957f317a1..0a2a459d38 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -354,7 +354,7 @@ let locate_if_isevar loc na = function
 	| Name id -> glob_constr_of_notation_constr loc
 	               (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> GHole (loc, Evar_kinds.BinderType na))
+      with Not_found -> GHole (loc, Evar_kinds.BinderType na, None))
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
@@ -401,7 +401,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
     env fvs in
   let bl = List.map
     (fun (id, loc) ->
-      (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id)))))
+      (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id), None))))
     fvs
   in
   let na = match na with
@@ -441,7 +441,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
   | LocalRawDef((loc,na as locna),def) ->
       let indef = intern env def in
       (push_name_env lvar (impls_term_list indef) env locna,
-      (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na)))::bl)
+      (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,None)))::bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -461,10 +461,10 @@ let intern_generalization intern env lvar loc bk ak c =
       in
 	if pi then
 	  (fun (id, loc') acc ->
-	    GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
+	    GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), None), acc))
 	else
 	  (fun (id, loc') acc ->
-	    GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
+	    GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), None), acc))
     in
       List.fold_right (fun (id, loc as lid) (env, acc) ->
 	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
@@ -562,7 +562,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
       let na =
         try snd (coerce_to_name (fst (Id.Map.find id terms)))
         with Not_found -> na in
-      GHole (loc,Evar_kinds.BinderType na)
+      GHole (loc,Evar_kinds.BinderType na,None)
     | NBinderList (x,_,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -1285,8 +1285,8 @@ let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i b = function
-  | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b))
-  | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b))
+  | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),None)
+  | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),None)
   | _ -> anomaly (Pp.str "Only refs have implicits")
 
 let exists_implicit_name id =
@@ -1459,13 +1459,13 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CRecord (loc, _, fs) ->
 	let cargs =
 	  sort_fields true loc fs
-	    (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true))) :: l)
+	    (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), None) :: l)
 	  in
 	begin
 	  match cargs with
 	    | None -> user_err_loc (loc, "intern", str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = List.make n (CHole (loc, None)) in
+		let pars = List.make n (CHole (loc, None, None)) in
 		let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
 	  intern env app
 	end
@@ -1497,9 +1497,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
 		   GCases(Loc.ghost,Term.RegularStyle,Some (GSort (Loc.ghost,GType None)), (* "return Type" *)
 			  List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
 			  [Loc.ghost,[],thepats, (* "|p1,..,pn" *)
-			   Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
+			   Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType,None)) rtnpo; (* "=> P" is there were a P "=> _" else *)
 			   Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
-			   GHole(Loc.ghost,Evar_kinds.ImpossibleCase) (* "=> _" *)]))
+			   GHole(Loc.ghost,Evar_kinds.ImpossibleCase,None) (* "=> _" *)]))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
@@ -1521,8 +1521,26 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	    (Loc.ghost,na') in
 	  intern_type env'' p) po in
         GIf (loc, c', (na', p'), intern env b1, intern env b2)
-    | CHole (loc, k) ->
-	GHole (loc, match k with Some k -> k | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true))
+    | CHole (loc, k, solve) ->
+        let k = match k with
+        | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true)
+        | Some k -> k
+        in
+        let solve = match solve with
+        | None -> None
+        | Some gen ->
+          let (cvars, lvars) = fst lvar in
+          let lvars = Id.Set.union lvars cvars in
+          let ist = {
+            Genintern.ltacvars = lvars;
+            ltacrecvars = Id.Map.empty;
+            gsigma = sigma;
+            genv = globalenv;
+          } in
+          let (_, glb) = Genintern.generic_intern ist gen in
+          Some glb
+        in
+	GHole (loc, k, solve)
     | CPatVar (loc, n) when allow_patvar ->
 	GPatVar (loc, n)
     | CPatVar (loc, _) ->
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d469f36faa..10b0884818 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -104,7 +104,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
       GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k)
   | NSort x -> GSort (loc,x)
-  | NHole x  -> GHole (loc,x)
+  | NHole x  -> GHole (loc, x, None)
   | NPatVar n -> GPatVar (loc,(false,n))
   | NRef x -> GRef (loc,x)
 
@@ -287,7 +287,7 @@ let notation_constr_and_vars_of_glob_constr a =
       NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
   | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
   | GSort (_,s) -> NSort s
-  | GHole (_,w) -> NHole w
+  | GHole (_,w,_) -> NHole w
   | GRef (_,r) -> NRef r
   | GPatVar (_,(_,n)) -> NPatVar n
   | GEvar _ ->
@@ -490,7 +490,7 @@ let abstract_return_type_context pi mklam tml rtno =
 let abstract_return_type_context_glob_constr =
   abstract_return_type_context (fun (_,_,nal) -> nal)
     (fun na c ->
-      GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole),c))
+      GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,None),c))
 
 let abstract_return_type_context_notation_constr =
   abstract_return_type_context snd
@@ -553,7 +553,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (_,Name id2) when Id.List.mem id2 (fst metas) ->
       let rhs = match na1 with
       | Name id1 -> GVar (Loc.ghost,id1)
-      | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole) in
+      | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,None) in
       alp, bind_env alp sigma id2 rhs
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
@@ -577,7 +577,7 @@ let rec match_iterated_binders islambda decls = function
       match_iterated_binders islambda ((na,bk,None,t)::decls) b
   | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
       match_iterated_binders islambda
-	((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na))::decls) b
+	((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,None))::decls) b
   | b -> (decls,b)
 
 let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
@@ -731,7 +731,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
      to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
   | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner ->
       let id' = Namegen.next_ident_away id (free_glob_vars b1) in
-      let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id')) in
+      let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),None) in
       let sigma = match t2 with
       | NHole _ -> sigma
       | NVar id2 -> bind_env alp sigma id2 t1
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 12c3dcbba3..77ca9e2673 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -115,7 +115,7 @@ let anonymize_if_reserved na t = match na with
             let ntn = notation_constr_of_glob_constr Id.Map.empty Id.Map.empty t in
             Pervasives.(=) ntn (find_reserved_type id) (** FIXME *)
             with UserError _ -> false)
-	then GHole (Loc.ghost,Evar_kinds.BinderType na)
+	then GHole (Loc.ghost,Evar_kinds.BinderType na,None)
 	else t
       with Not_found -> t)
   | Anonymous -> t
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7c9db3ef74..cea5060597 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -111,7 +111,7 @@ let fold_constr_expr_with_binders g f n acc = function
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
       let acc = List.fold_left (f n) acc (l@List.flatten ll) in
-      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None)) bl) acc bll
+      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None,None)) bl) acc bll
   | CGeneralization (_,_,_,c) -> f n acc c
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->