From 144f2ac7c7394a701808daa503a0b6ded5663fcc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 6 Sep 2013 21:50:35 +0200 Subject: Adding generic solvers to term holes. For now, no resolution mechanism nor parsing is plugged. --- dev/printers.mllib | 1 + grammar/q_constr.ml4 | 2 +- grammar/q_coqast.ml4 | 6 ++--- interp/constrexpr_ops.ml | 6 ++--- interp/constrextern.ml | 10 ++++---- interp/constrintern.ml | 46 ++++++++++++++++++++++++----------- interp/notation_ops.ml | 12 ++++----- interp/reserve.ml | 2 +- interp/topconstr.ml | 2 +- intf/constrexpr.mli | 2 +- intf/glob_term.mli | 2 +- parsing/egramcoq.ml | 2 +- parsing/g_constr.ml4 | 22 ++++++++--------- parsing/g_ltac.ml4 | 2 +- parsing/g_tactic.ml4 | 2 +- parsing/g_vernac.ml4 | 6 ++--- plugins/decl_mode/decl_interp.ml | 12 ++++----- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/funind/glob_termops.ml | 2 +- plugins/syntax/numbers_syntax.ml | 4 +-- pretyping/cases.ml | 2 +- pretyping/detyping.ml | 20 +++++++++------ pretyping/detyping.mli | 3 +++ pretyping/glob_ops.ml | 4 +-- pretyping/patternops.ml | 2 +- pretyping/pretyping.ml | 23 ++++++++++++++---- pretyping/pretyping.mli | 4 +++ printing/ppconstr.ml | 2 +- printing/ppvernac.ml | 2 +- tactics/extratactics.ml4 | 6 ++--- tactics/rewrite.ml | 2 +- toplevel/classes.ml | 4 +-- toplevel/command.ml | 2 +- toplevel/record.ml | 2 +- 35 files changed, 134 insertions(+), 91 deletions(-) diff --git a/dev/printers.mllib b/dev/printers.mllib index 1410cc7a0..2c4f84397 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -148,6 +148,7 @@ Impargs Syntax_def Implicit_quantifiers Smartlocate +Genintern Constrintern Modintern Constrextern diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index 130f14717..bfc38feb8 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -70,7 +70,7 @@ EXTEND | "0" [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >> | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> - | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False)) >> + | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),None) >> | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index d0fd618c7..02c00e3f0 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -161,10 +161,10 @@ let rec mlexpr_of_constr = function let loc = of_coqloc loc in <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >> | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CHole (loc, None) -> + | Constrexpr.CHole (loc, None, None) -> let loc = of_coqloc loc in - <:expr< Constrexpr.CHole $dloc$ None >> - | Constrexpr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" + <:expr< Constrexpr.CHole $dloc$ None None >> + | Constrexpr.CHole (loc, _, _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" | Constrexpr.CNotation(_,ntn,(subst,substl,[])) -> <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$ ($mlexpr_of_list mlexpr_of_constr subst$, diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 5edfc0614..c8a0e5638 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 741ef9853..ffb8a46ea 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 b957f317a..0a2a459d3 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 d469f36fa..10b088481 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 12c3dcbba..77ca9e267 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 7c9db3ef7..cea506059 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 _ -> diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 68a65c5c7..64bbd1e83 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -78,7 +78,7 @@ type constr_expr = constr_expr * constr_expr | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option) * constr_expr * constr_expr - | CHole of Loc.t * Evar_kinds.t option + | CHole of Loc.t * Evar_kinds.t option * Genarg.raw_generic_argument option | CPatVar of Loc.t * (bool * patvar) | CEvar of Loc.t * existential_key * constr_expr list option | CSort of Loc.t * glob_sort diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 315b11517..1d200ca79 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -46,7 +46,7 @@ type glob_constr = | GRec of Loc.t * fix_kind * Id.t array * glob_decl list array * glob_constr array * glob_constr array | GSort of Loc.t * glob_sort - | GHole of (Loc.t * Evar_kinds.t) + | GHole of (Loc.t * Evar_kinds.t * Genarg.glob_generic_argument option) | GCast of Loc.t * glob_constr * glob_constr cast_type and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index a6ac42cf1..d405de921 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -47,7 +47,7 @@ open Egramml (** Declare Notations grammar rules *) let constr_expr_of_name (loc,na) = match na with - | Anonymous -> CHole (loc,None) + | Anonymous -> CHole (loc,None,None) | Name id -> CRef (Ident (loc,id)) let cases_pattern_expr_of_name (loc,na) = match na with diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 08c1f1917..51214d91e 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -40,17 +40,17 @@ let mk_cast = function let binders_of_names l = List.map (fun (loc, na) -> LocalRawAssum ([loc, na], Default Explicit, - CHole (loc, Some (Evar_kinds.BinderType na)))) l + CHole (loc, Some (Evar_kinds.BinderType na), None))) l let binders_of_lidents l = List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Explicit, - CHole (loc, Some (Evar_kinds.BinderType (Name id))))) l + CHole (loc, Some (Evar_kinds.BinderType (Name id)), None))) l let mk_fixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with Some ty -> ty - | None -> CHole (loc, None) in + | None -> CHole (loc, None, None) in (id,ann,bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) = @@ -60,7 +60,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with Some ty -> ty - | None -> CHole (loc, None) in + | None -> CHole (loc, None, None) in (id,bl,ty,body) let mk_fix(loc,kw,id,dcls) = @@ -278,7 +278,7 @@ GEXTEND Gram | s=sort -> CSort (!@loc,s) | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n)) | s=string -> CPrim (!@loc, String s) - | "_" -> CHole (!@loc, None) + | "_" -> CHole (!@loc, None, None) | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ] ; fix_constr: @@ -369,11 +369,11 @@ GEXTEND Gram | s = string -> CPatPrim (!@loc, String s) ] ] ; impl_ident_tail: - [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(!@loc, None)) + [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(!@loc, None, None)) | idl=LIST1 name; ":"; c=lconstr; "}" -> (fun id -> LocalRawAssum (id::idl,Default Implicit,c)) | idl=LIST1 name; "}" -> - (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (!@loc, None))) + (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (!@loc, None, None))) | ":"; c=lconstr; "}" -> (fun id -> LocalRawAssum ([id],Default Implicit,c)) ] ] @@ -404,7 +404,7 @@ GEXTEND Gram binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2], - Default Explicit,CHole (!@loc,None))] + Default Explicit,CHole (!@loc, None, None))] | bl = closed_binder; bl' = binders -> bl@bl' ] ] @@ -413,7 +413,7 @@ GEXTEND Gram [ [ l = LIST0 binder -> List.flatten l ] ] ; binder: - [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None))] + [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None, None))] | bl = closed_binder -> bl ] ] ; closed_binder: @@ -426,13 +426,13 @@ GEXTEND Gram | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))] | "{"; id=name; "}" -> - [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None))] + [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> [LocalRawAssum (id::idl,Default Implicit,c)] | "{"; id=name; ":"; c=lconstr; "}" -> [LocalRawAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None))) (id::idl) + List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, None))) (id::idl) | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index d075a7790..c2dbd1d63 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -192,7 +192,7 @@ GEXTEND Gram | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None - in Def (na, t, Option.default (Term (CHole (Loc.ghost, None))) ty) + in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, None))) ty) ] ] ; match_context_rule: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b72bb0264..eb483c50c 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -424,7 +424,7 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit,CHole (!@loc, None)) + [ [ na=name -> ([na],Default Explicit,CHole (!@loc, None, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 81bd6a108..567bde9ca 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -323,7 +323,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> CHole (!@loc, None) ] ] + | -> CHole (!@loc, None, None) ] ] ; (* Inductive schemes *) scheme: @@ -372,7 +372,7 @@ GEXTEND Gram (None,DefExpr(id,mkCLambdaN (!@loc) l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None))) + [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -391,7 +391,7 @@ GEXTEND Gram t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (not (Option.is_empty coe),(id,mkCProdN (!@loc) l c)) | -> - fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None)))) ] + fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None, None)))) ] -> t l ]] ; diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index bbac10f0f..a722daca5 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -187,7 +187,7 @@ let interp_constr_or_thesis check_sort sigma env = function let abstract_one_hyp inject h glob = match h with Hvar (loc,(id,None)) -> - GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob) + GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), None), glob) | Hvar (loc,(id,Some typ)) -> GProd (Loc.ghost,Name id, Explicit, fst typ, glob) | Hprop st -> @@ -245,7 +245,7 @@ let rec glob_of_pat = let rec add_params n q = if n<=0 then q else add_params (pred n) (GHole(Loc.ghost, - Evar_kinds.TomatchTypeParameter(ind,n))::q) in + Evar_kinds.TomatchTypeParameter(ind,n), None)::q) in let args = List.map glob_of_pat lpat in glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr), add_params mind.Declarations.mind_nparams args) @@ -254,14 +254,14 @@ let prod_one_hyp = function (loc,(id,None)) -> (fun glob -> GProd (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id)), glob)) + GHole (loc,Evar_kinds.BinderType (Name id), None), glob)) | (loc,(id,Some typ)) -> (fun glob -> GProd (Loc.ghost,Name id, Explicit, fst typ, glob)) let prod_one_id (loc,id) glob = GProd (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id)), glob) + GHole (loc,Evar_kinds.BinderType (Name id), None), glob) let let_in_one_alias (id,pat) glob = GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) @@ -342,7 +342,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = GVar (loc,id)) params in let dum_args= List.init oib.Declarations.mind_nrealargs - (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) in + (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),None)) in glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function @@ -417,7 +417,7 @@ let abstract_one_arg = function (loc,(id,None)) -> (fun glob -> GLambda (Loc.ghost,Name id, Explicit, - GHole (loc,Evar_kinds.BinderType (Name id)), glob)) + GHole (loc,Evar_kinds.BinderType (Name id),None), glob)) | (loc,(id,Some typ)) -> (fun glob -> GLambda (Loc.ghost,Name id, Explicit, fst typ, glob)) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index db53dc932..b21037d25 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1276,7 +1276,7 @@ let understand_my_constr c gls = let nc = names_of_rel_context env in let rawc = Detyping.detype false [] nc c in let rec frob = function - | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand) + | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None) | rc -> map_glob_constr frob rc in Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index d34edb863..e856326c8 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -125,7 +125,7 @@ let mk_open_instance id gl m t= match t with GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in - GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name),t1) + GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1) | _-> anomaly (Pp.str "can't happen") in let ntt=try Pretyping.understand evmap env (raux m rawt) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 79cba2c7c..6a7f326e6 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -18,7 +18,7 @@ let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b) let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(Loc.ghost,s) -let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous) +let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,None) let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t) (* diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 1cce6cd70..b8c2b33fd 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -165,10 +165,10 @@ let word_of_pos_bigint dloc hght n = if hgt <= 0 then int31_of_pos_bigint dloc n else if equal n zero then - GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole)]) + GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, None)]) else let (h,l) = split_at hgt n in - GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole); + GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, None); decomp (hgt-1) h; decomp (hgt-1) l]) in 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 diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index b389ca790..92b4bf496 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -258,7 +258,7 @@ let pr_binder_among_many pr_c = function | LocalRawDef (na,c) -> let c,topt = match c with | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t - | _ -> c, CHole (Loc.ghost, None) in + | _ -> c, CHole (Loc.ghost, None, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 441e362b1..ba640863d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -250,7 +250,7 @@ let pr_module_binders l pr_c = prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | CHole (loc, k) -> mt() + | CHole (loc, k, _) -> mt() | _ as c -> brk(0,2) ++ str":" ++ pr_c c let pr_decl_notation prc ((loc,ntn),c,scopt) = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1c7b8d49f..c81e7ce3f 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -554,7 +554,7 @@ let subst_var_with_hole occ tid t = else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true)))) + Evar_kinds.QuestionMark(Evar_kinds.Define true), None))) else x | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t @@ -565,13 +565,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true)) -> + | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true))) + Evar_kinds.QuestionMark(Evar_kinds.Define true),s)) | c -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 337ae5241..2e3b6e1af 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1511,7 +1511,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2); (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CHole (Loc.ghost, None) +let cHole = CHole (Loc.ghost, None, None) let proper_projection r ty = let ctx, inst = decompose_prod_assum ty in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 728baadb4..bb34323cd 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -127,7 +127,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props (fun avoid (clname, (id, _, t)) -> match clname with | Some (cl, b) -> - let t = CHole (Loc.ghost, None) in + let t = CHole (Loc.ghost, None, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl @@ -228,7 +228,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Loc.ghost, Some Evar_kinds.GoalEvar) :: props), rest + (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, None) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/toplevel/command.ml b/toplevel/command.ml index 095bf5300..77219f9a2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -50,7 +50,7 @@ let rec under_binders env f n c = let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) - | CHole (loc, k) -> + | CHole (loc, k, _) -> let (has_no_args,name,params) = a in if not has_no_args then user_err_loc (loc,"", diff --git a/toplevel/record.ml b/toplevel/record.ml index cf5714546..2ef425bf2 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -43,7 +43,7 @@ let interp_fields_evars evars env impls_env nots l = let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) - | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None)) + | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, None)) let binders_of_decls = List.map binder_of_decl -- cgit v1.2.3