diff options
| author | Hugo Herbelin | 2014-08-12 14:03:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-12 10:39:32 +0200 |
| commit | 012fe1a96ba81ab0a7fa210610e3f25187baaf1d (patch) | |
| tree | 32282ac2f1198738c8c545b19215ff0a0d9ef6ce | |
| parent | b720cd3cbefa46da784b68a8e016a853f577800c (diff) | |
Referring to evars by names. Added a parser for evars (but parsing of
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
69 files changed, 1165 insertions, 668 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 56c71d88f5..4fedbec8e9 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -200,8 +200,8 @@ let ppuniverse_context_future c = let ppuniverses u = pp (Univ.pr_universes u) let ppenv e = pp - (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ - str "[" ++ pr_rel_context e (rel_context e) ++ str "]") + (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ + str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x)) @@ -457,7 +457,7 @@ let in_current_context f c = let (evmap,sign) = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in - f (fst (Constrintern.interp_constr evmap sign c))(*FIXME*) + f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*) (* We expand the result of preprocessing to be independent of camlp4 diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5e03d27732..61c60c02f2 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -122,7 +122,7 @@ let query (s,id) = Stm.query ~at:id s; read_stdout () let hyp_next_tac sigma env (id,_,ast) = let id_s = Names.Id.to_string id in - let type_s = string_of_ppcmds (pr_ltype_env env ast) in + let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in [ ("clear "^id_s),("clear "^id_s^"."); ("apply "^id_s),("apply "^id_s^"."); @@ -184,10 +184,10 @@ let process_goal sigma g = let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in + string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d = let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in - (string_of_ppcmds (pr_var_list_decl min_env d)) in + (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in let hyps = List.map process_hyp (compact_named_context (Environ.named_context env)) in { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } @@ -222,7 +222,7 @@ let evars () = let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in - let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar ev); } in + let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in Some el with Proof_global.NoCurrentProof -> None diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 1ba0cafa7a..ca36f4c9f8 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -151,9 +151,8 @@ let rec constr_expr_eq e1 e2 = | CHole _, CHole _ -> true | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) -> (b1 : bool) == b2 && Id.equal i1 i2 - | CEvar (_, ev1, c1), CEvar (_, ev2, c2) -> - Evar.equal ev1 ev2 && - Option.equal (List.equal constr_expr_eq) c1 c2 + | CEvar (_, id1, c1), CEvar (_, id2, c2) -> + Id.equal id1 id2 && Option.equal (List.equal instance_eq) c1 c2 | CSort(_,s1), CSort(_,s2) -> Miscops.glob_sort_eq s1 s2 | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) -> @@ -226,6 +225,9 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = List.equal (List.equal constr_expr_eq) el1 el2 && List.equal (List.equal local_binder_eq) bl1 bl2 +and instance_eq (x1,c1) (x2,c2) = + Id.equal x1 x2 && constr_expr_eq c1 c2 + let constr_loc = function | CRef (Ident (loc,_),_) -> loc | CRef (Qualid (loc,_),_) -> loc diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ad159bb605..9a6f8b22cd 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -142,7 +142,7 @@ let insert_pat_alias loc p = function (* conversion of references *) let extern_evar loc n l = - if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None) +(* if !print_evar_arguments then*) CEvar (loc,n,l) (*else CEvar (loc,n,None)*) (** We allow customization of the global_reference printer. For instance, in the debugger the tables of global references @@ -674,7 +674,7 @@ let rec extern inctx scopes vars r = | 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) + extern_evar loc n (Option.map (List.map (on_snd (extern false scopes vars))) l) | GPatVar (loc,n) -> if !print_meta_as_hole then CHole (loc, None, None) else CPatVar (loc,n) @@ -988,7 +988,7 @@ let extern_glob_type vars c = let loc = Loc.ghost (* for constr and pattern, locations are lost *) -let extern_constr_gen goal_concl_style scopt env t = +let extern_constr_gen goal_concl_style scopt env sigma t = (* "goal_concl_style" means do alpha-conversion using the "goal" convention *) (* i.e.: avoid using the names of goal/section/rel variables and the short *) (* names of global definitions of current module when computing names for *) @@ -998,20 +998,20 @@ let extern_constr_gen goal_concl_style scopt env t = (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then ids_of_context env else [] in let rel_env_names = names_of_rel_context env in - let r = Detyping.detype goal_concl_style avoid rel_env_names t in + let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in let vars = vars_of_env env in extern false (scopt,[]) vars r -let extern_constr_in_scope goal_concl_style scope env t = - extern_constr_gen goal_concl_style (Some scope) env t +let extern_constr_in_scope goal_concl_style scope env sigma t = + extern_constr_gen goal_concl_style (Some scope) env sigma t -let extern_constr goal_concl_style env t = - extern_constr_gen goal_concl_style None env t +let extern_constr goal_concl_style env sigma t = + extern_constr_gen goal_concl_style None env sigma t -let extern_type goal_concl_style env t = +let extern_type goal_concl_style env sigma t = let avoid = if goal_concl_style then ids_of_context env else [] in let rel_env_names = names_of_rel_context env in - let r = Detyping.detype goal_concl_style avoid rel_env_names t in + let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in extern_glob_type (vars_of_env env) r let extern_sort s = extern_glob_sort (detype_sort s) @@ -1023,10 +1023,14 @@ let any_any_branch = (* | _ => _ *) (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,None)) -let rec glob_of_pat env = function +let rec glob_of_pat env sigma = function | PRef ref -> GRef (loc,ref,None) | PVar id -> GVar (loc,id) - | PEvar (n,l) -> GEvar (loc,n,Some (Array.map_to_list (glob_of_pat env) l)) + | PEvar (evk,l) -> + let test id = function PVar id' -> Id.equal id id' | _ -> false in + let l = Evd.evar_instance_array test (Evd.find sigma evk) l in + let id = Evd.evar_ident evk sigma in + GEvar (loc,id,Some (List.map (on_snd (glob_of_pat env sigma)) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -1036,29 +1040,29 @@ let rec glob_of_pat env = function GVar (loc,id) | PMeta None -> GHole (loc,Evar_kinds.InternalHole, None) | PMeta (Some n) -> GPatVar (loc,(false,n)) - | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef p,None),[glob_of_pat env c]) + | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef p,None),[glob_of_pat env sigma c]) | PApp (f,args) -> - GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args) + GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> GApp (loc,GPatVar (loc,(true,n)), - List.map (glob_of_pat env) args) + List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> - GProd (loc,na,Explicit,glob_of_pat env t,glob_of_pat (na::env) c) + GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) | PLetIn (na,t,c) -> - GLetIn (loc,na,glob_of_pat env t, glob_of_pat (na::env) c) + GLetIn (loc,na,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) | PLambda (na,t,c) -> - GLambda (loc,na,Explicit,glob_of_pat env t, glob_of_pat (na::env) c) + GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) | PIf (c,b1,b2) -> - GIf (loc, glob_of_pat env c, (Anonymous,None), - glob_of_pat env b1, glob_of_pat env b2) + GIf (loc, glob_of_pat env sigma c, (Anonymous,None), + glob_of_pat env sigma b1, glob_of_pat env sigma b2) | PCase ({cip_style=LetStyle; cip_ind_args=None},PMeta None,tm,[(0,n,b)]) -> - let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env b) in - GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env tm,b) + let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in + GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env sigma tm,b) | PCase (info,p,tm,bl) -> let mat = match bl, info.cip_ind with | [], _ -> [] | _, Some ind -> - let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env c)) bl in + let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in simple_cases_matrix_of_branches ind bl' | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive") in @@ -1067,18 +1071,18 @@ let rec glob_of_pat env = function let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with | PMeta None, _, _ -> (Anonymous,None),None | _, Some ind, Some nargs -> - return_type_of_predicate ind nargs (glob_of_pat env p) + return_type_of_predicate ind nargs (glob_of_pat env sigma p) | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") in - GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat) - | PFix f -> Detyping.detype false [] env (mkFix f) - | PCoFix c -> Detyping.detype false [] env (mkCoFix c) + GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) + | PFix f -> Detyping.detype false [] env sigma (mkFix f) + | PCoFix c -> Detyping.detype false [] env sigma (mkCoFix c) | PSort s -> GSort (loc,s) -let extern_constr_pattern env pat = - extern true (None,[]) Id.Set.empty (glob_of_pat env pat) +let extern_constr_pattern env sigma pat = + extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) -let extern_rel_context where env sign = - let a = detype_rel_context where [] (names_of_rel_context env) sign in +let extern_rel_context where env sigma sign = + let a = detype_rel_context where [] (names_of_rel_context env) sigma sign in let vars = vars_of_env env in pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index e1acb45021..a994d86931 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -26,17 +26,18 @@ open Misctypes val extern_cases_pattern : Id.Set.t -> cases_pattern -> cases_pattern_expr val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr -val extern_constr_pattern : names_context -> constr_pattern -> constr_expr +val extern_constr_pattern : names_context -> Evd.evar_map -> + constr_pattern -> constr_expr (** If [b=true] in [extern_constr b env c] then the variables in the first level of quantification clashing with the variables in [env] are renamed *) -val extern_constr : bool -> env -> constr -> constr_expr -val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr +val extern_constr : bool -> env -> Evd.evar_map -> constr -> constr_expr +val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference -val extern_type : bool -> env -> types -> constr_expr +val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : sorts -> glob_sort -val extern_rel_context : constr option -> env -> +val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder list (** Printing options *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d34c43d3d8..ff96340cde 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1581,10 +1581,12 @@ let internalize globalenv env allow_patvar lvar c = GHole (loc, k, solve) | CPatVar (loc, n) when allow_patvar -> GPatVar (loc, n) + | CPatVar (loc, (false,n)) -> + GEvar (loc, n, None) | CPatVar (loc, _) -> - raise (InternalizationError (loc,IllegalMetavariable)) + raise (InternalizationError (loc,IllegalMetavariable)) | CEvar (loc, n, l) -> - GEvar (loc, n, Option.map (List.map (intern env)) l) + GEvar (loc, n, Option.map (List.map (on_snd (intern env))) l) | CSort (loc, s) -> GSort(loc,s) | CCast (loc, c1, c2) -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 9461cebb0f..1aac1c53d1 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -356,7 +356,7 @@ let notation_constr_of_glob_constr nenv a = (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = - let t = Detyping.detype false avoiding [] t in + let t = Detyping.detype false avoiding [] Evd.empty t in let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; diff --git a/interp/reserve.ml b/interp/reserve.ml index 272e6c8d1c..33c21eea59 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -108,7 +108,7 @@ let constr_key c = let revert_reserved_type t = try let reserved = KeyMap.find (constr_key t) !reserve_revtable in - let t = Detyping.detype false [] [] t in + let t = Detyping.detype false [] [] Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index eb39a9bde6..bc2f7df248 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -82,7 +82,7 @@ type constr_expr = * constr_expr * constr_expr | 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 + | CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list option | CSort of Loc.t * glob_sort | CCast of Loc.t * constr_expr * constr_expr cast_type | CNotation of Loc.t * notation * constr_notation_substitution diff --git a/intf/glob_term.mli b/intf/glob_term.mli index d0b6939e24..9aca2306a0 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -19,6 +19,8 @@ open Globnames open Decl_kinds open Misctypes +type existential_name = Id.t + (** The kind of patterns that occurs in "match ... with ... end" locs here refers to the ident's location, not whole pat *) @@ -30,7 +32,7 @@ type cases_pattern = type glob_constr = | GRef of (Loc.t * global_reference * glob_level list option) | GVar of (Loc.t * Id.t) - | GEvar of Loc.t * existential_key * glob_constr list option + | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list option | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 new file mode 100644 index 0000000000..55b3fe9031 --- /dev/null +++ b/parsing/g_xml.ml4 @@ -0,0 +1,290 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Compat +open Pp +open Errors +open Util +open Names +open Pcoq +open Glob_term +open Tacexpr +open Libnames +open Globnames +open Detyping +open Misctypes +open Decl_kinds +open Genredexpr +open Tok (* necessary for camlp4 *) + +(* Generic xml parser without raw data *) + +type attribute = string * (Loc.t * string) +type xml = XmlTag of Loc.t * string * attribute list * xml list + +let check_tags loc otag ctag = + if not (String.equal otag ctag) then + user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++ + str "does not match open xml tag " ++ str otag ++ str ".") + +let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry) + +GEXTEND Gram + GLOBAL: xml_eoi; + + xml_eoi: + [ [ x = xml; EOI -> x ] ] + ; + xml: + [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml; + "<"; "/"; ctag = IDENT; ">" -> + check_tags (!@loc) otag ctag; + XmlTag (!@loc,ctag,attrs,l) + | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" -> + XmlTag (!@loc,tag,attrs,[]) + ] ] + ; + attr: + [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ] + ; +END + +(* Errors *) + +let error_bad_arity loc n = + let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in + user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^").")) + +(* Interpreting attributes *) + +let nmtoken (loc,a) = + try int_of_string a + with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") + +let get_xml_attr s al = + try String.List.assoc s al + with Not_found -> error ("No attribute "^s) + +(* Interpreting specific attributes *) + +let ident_of_cdata (loc,a) = Id.of_string a + +let uri_of_data s = + try + let n = String.index s ':' in + let p = String.index s '.' in + let s = String.sub s (n+2) (p-n-2) in + for i = 0 to String.length s - 1 do + match s.[i] with + | '/' -> s.[i] <- '.' + | _ -> () + done; + qualid_of_string s + with Not_found | Invalid_argument _ -> + error ("Malformed URI \""^s^"\"") + +let constant_of_cdata (loc,a) = + let q = uri_of_data a in + try Nametab.locate_constant q + with Not_found -> error ("No such constant "^string_of_qualid q) + +let global_of_cdata (loc,a) = + let q = uri_of_data a in + try Nametab.locate q + with Not_found -> error ("No such global "^string_of_qualid q) + +let inductive_of_cdata a = match global_of_cdata a with + | IndRef (kn,_) -> kn + | _ -> error (string_of_qualid (uri_of_data (snd a)) ^" is not an inductive") + +let ltacref_of_cdata (loc,a) = + let q = uri_of_data a in + try (loc,Nametab.locate_tactic q) + with Not_found -> error ("No such ltac "^string_of_qualid q) + +let sort_of_cdata (loc,a) = match a with + | "Prop" -> GProp + | "Set" -> GSet + | "Type" -> GType None + | _ -> user_err_loc (loc,"",str "sort expected.") + +let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) + +let get_xml_inductive_kn al = + inductive_of_cdata (* uriType apparent synonym of uri *) + (try get_xml_attr "uri" al + with UserError _ -> get_xml_attr "uriType" al) + +let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al) + +let get_xml_inductive al = + (get_xml_inductive_kn al, nmtoken (get_xml_attr "noType" al)) + +let get_xml_constructor al = + (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al)) + +let get_xml_binder al = + try Name (ident_of_cdata (String.List.assoc "binder" al)) + with Not_found -> Anonymous + +let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al) + +let get_xml_name al = ident_of_cdata (get_xml_attr "name" al) + +let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al) + +let get_xml_no al = Evar.unsafe_of_int (nmtoken (get_xml_attr "no" al)) + +(* A leak in the xml dtd: arities of constructor need to know global env *) + +let compute_branches_lengths ind = + let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in + mip.Declarations.mind_consnrealdecls + +let compute_inductive_ndecls ind = + Inductiveops.inductive_nrealdecls ind + +(* Interpreting constr as a glob_constr *) + +let rec interp_xml_constr = function + | XmlTag (loc,"REL",al,[]) -> + GVar (loc, get_xml_ident al) + | XmlTag (loc,"VAR",al,[]) -> + error "XML parser: unable to interp free variables" + | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) -> + let body,decls = List.sep_last xl in + let ctx = List.map interp_xml_decl decls in + List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b)) + ctx (interp_xml_target body) + | XmlTag (loc,"PROD",al,(_::_ as xl)) -> + let body,decls = List.sep_last xl in + let ctx = List.map interp_xml_decl decls in + List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b)) + ctx (interp_xml_target body) + | XmlTag (loc,"LETIN",al,(_::_ as xl)) -> + let body,defs = List.sep_last xl in + let ctx = List.map interp_xml_def defs in + List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b)) + ctx (interp_xml_target body) + | XmlTag (loc,"APPLY",_,x::xl) -> + GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl) + | XmlTag (loc,"instantiate",_, + (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) -> + GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl) + | XmlTag (loc,"META",al,xl) -> + GEvar (loc, get_xml_name al, Some (List.map interp_xml_substitution xl)) + | XmlTag (loc,"CONST",al,[]) -> + GRef (loc, ConstRef (get_xml_constant al), None) + | XmlTag (loc,"MUTCASE",al,x::y::yl) -> + let ind = get_xml_inductive al in + let p = interp_xml_patternsType x in + let tm = interp_xml_inductiveTerm y in + let vars = compute_branches_lengths ind in + let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl + in + let mat = simple_cases_matrix_of_branches ind brs in + let n = compute_inductive_ndecls ind in + let nal,rtn = return_type_of_predicate ind n p in + GCases (loc,RegularStyle,rtn,[tm,nal],mat) + | XmlTag (loc,"MUTIND",al,[]) -> + GRef (loc, IndRef (get_xml_inductive al), None) + | XmlTag (loc,"MUTCONSTRUCT",al,[]) -> + GRef (loc, ConstructRef (get_xml_constructor al), None) + | XmlTag (loc,"FIX",al,xl) -> + let li,lnct = List.split (List.map interp_xml_FixFunction xl) in + let ln,lc,lt = List.split3 lnct in + let lctx = List.map (fun _ -> []) ln in + GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt) + | XmlTag (loc,"COFIX",al,xl) -> + let ln,lc,lt = List.split3 (List.map interp_xml_CoFixFunction xl) in + GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) + | XmlTag (loc,"CAST",al,[x1;x2]) -> + GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2)) + | XmlTag (loc,"SORT",al,[]) -> + GSort (loc, get_xml_sort al) + | XmlTag (loc,s,_,_) -> + user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") + +and interp_xml_tag s = function + | XmlTag (loc,tag,al,xl) when String.equal tag s -> (loc,al,xl) + | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "", + str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".") + +and interp_xml_constr_alias s x = + match interp_xml_tag s x with + | (_,_,[x]) -> interp_xml_constr x + | (loc,_,_) -> error_bad_arity loc 1 + +and interp_xml_term x = interp_xml_constr_alias "term" x +and interp_xml_type x = interp_xml_constr_alias "type" x +and interp_xml_target x = interp_xml_constr_alias "target" x +and interp_xml_body x = interp_xml_constr_alias "body" x +and interp_xml_pattern x = interp_xml_constr_alias "pattern" x +and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x +and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x +and interp_xml_arg x = interp_xml_constr_alias "arg" x +and interp_xml_substitution x = + match interp_xml_tag "substitution" x with + _, al, [x] -> get_xml_name al, interp_xml_constr x + | loc, _, _ -> error_bad_arity loc 1 + (* no support for empty substitution from official dtd *) + +and interp_xml_decl_alias s x = + match interp_xml_tag s x with + | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x) + | (loc,_,_) -> error_bad_arity loc 1 + +and interp_xml_def x = interp_xml_decl_alias "def" x +and interp_xml_decl x = interp_xml_decl_alias "decl" x + +and interp_xml_recursionOrder x = + let (loc, al, l) = interp_xml_tag "RecursionOrder" x in + let (locs, s) = get_xml_attr "type" al in + match s, l with + | "Structural", [] -> GStructRec + | "Structural", _ -> error_bad_arity loc 0 + | "WellFounded", [c] -> GWfRec (interp_xml_type c) + | "WellFounded", _ -> error_bad_arity loc 1 + | "Measure", [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r)) + | "Measure", _ -> error_bad_arity loc 2 + | _ -> user_err_loc (locs,"",str "Invalid recursion order.") + +and interp_xml_FixFunction x = + match interp_xml_tag "FixFunction" x with + | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *) + ((Some (nmtoken (get_xml_attr "recIndex" al)), + interp_xml_recursionOrder x1), + (get_xml_name al, interp_xml_type x2, interp_xml_body x3)) + | (loc,al,[x1;x2]) -> + ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec), + (get_xml_name al, interp_xml_type x1, interp_xml_body x2)) + | (loc,_,_) -> + error_bad_arity loc 1 + +and interp_xml_CoFixFunction x = + match interp_xml_tag "CoFixFunction" x with + | (loc,al,[x1;x2]) -> + (get_xml_name al, interp_xml_type x1, interp_xml_body x2) + | (loc,_,_) -> + error_bad_arity loc 1 + +(* Interpreting tactic argument *) + +let rec interp_xml_tactic_arg = function + | XmlTag (loc,"TERM",[],[x]) -> + ConstrMayEval (ConstrTerm (interp_xml_constr x,None)) + | XmlTag (loc,"CALL",al,xl) -> + let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in + TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl) + | XmlTag (loc,s,_,_) -> + user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") + +let parse_tactic_arg ch = + interp_xml_tactic_arg + (Pcoq.Gram.entry_parse xml_eoi + (Pcoq.Gram.parsable (Stream.of_channel ch))) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index e0aee15e60..541b599209 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -316,7 +316,7 @@ let rec match_aliases names constr = function let args,bnames,body = match_aliases qnames body q in st::args,bnames,body -let detype_ground c = Detyping.detype false [] [] c +let detype_ground c = Detyping.detype false [] [] Evd.empty c let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let et,pinfo = diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b5566127f1..c5a474d39f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1034,12 +1034,12 @@ let thesis_for obj typ per_info env= let ind,u = destInd cind in let _ = if not (eq_ind ind per_info.per_ind) then errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in compose_prod rc (Reductionops.whd_beta Evd.empty hd2) @@ -1273,7 +1273,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let understand_my_constr c gls = let env = pf_env gls in let nc = names_of_rel_context env in - let rawc = Detyping.detype false [] nc c in + let rawc = Detyping.detype false [] nc Evd.empty c in let rec frob = function | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None) | rc -> map_glob_constr frob rc diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index a930245b65..9d909fda30 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -26,8 +26,8 @@ let pr_goal gs = let preamb,thesis,penv,pc = (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), (str "thesis := " ++ fnl ()), - Printer.pr_context_of env, - Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g) + Printer.pr_context_of env sigma, + Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 7f63c4200d..be2e44cff6 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -20,6 +20,8 @@ let pr_label = function Anonymous -> mt () | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () +let pr_constr env c = pr_constr env Evd.empty c + let pr_justification_items env = function Some [] -> mt () | Some (_::_ as l) -> diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 076107450b..6fd934654d 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -118,7 +118,7 @@ let mk_open_instance id idc gl m t= let nid=(fresh_id avoid var_id gl) in (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in let nt=it_mkLambda_or_LetIn revt (aux m []) in - let rawt=Detyping.detype false [] [] nt in + let rawt=Detyping.detype false [] [] evmap nt in let rec raux n t= if Int.equal n 0 then t else match t with diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 43bb6dbbf8..afa178832f 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -231,7 +231,7 @@ let extend_with_auto_hints l seq gl= let print_cmap map= let print_entry c l s= - let xc=Constrextern.extern_constr false (Global.env ()) c in + let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in str "| " ++ prlist Printer.pr_global l ++ str " : " ++ diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index aba93de479..700f67a74c 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -599,7 +599,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = | App(f,[| _;_;args2 |]) -> args2 | _ -> observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++ - pr_lconstr_env (pf_env g') new_term_value_eq + pr_lconstr_env (pf_env g') Evd.empty new_term_value_eq ); anomaly (Pp.str "cannot compute new term value") in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 587af35acb..36942636ff 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -340,7 +340,7 @@ let raw_push_named (na,raw_value,raw_typ) env = let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = - observe (str "new rel env := " ++ Printer.pr_rel_context_of env); + observe (str "new rel env := " ++ Printer.pr_rel_context_of env Evd.empty); match pat with | PatVar(_,na) -> Environ.push_rel (na,None,typ) env @@ -376,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env = ~init:(env,[]) ) in - observe (str "new var env := " ++ Printer.pr_named_context_of res); + observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty); res @@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ = function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i)) + (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty csta.(i)) ) in let patl_as_term = @@ -488,7 +488,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let rt_as_constr,ctx = Pretyping.understand Evd.empty env rt in let rt_typ = Typing.type_of env Evd.empty rt_as_constr in - let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in + let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in @@ -743,7 +743,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve in let raw_typ_of_id = Detyping.detype false [] - (Termops.names_of_rel_context env_with_pat_ids) typ_of_id + (Termops.names_of_rel_context env_with_pat_ids) Evd.empty typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) pat_ids @@ -787,7 +787,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.map3 (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in - let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in + let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) Evd.empty typ_as_constr in let pat_as_term = pattern_to_term pat in List.fold_right (fun id acc -> @@ -795,7 +795,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve then (Prod (Name id), let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in let raw_typ_of_id = - Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id + Detyping.detype false [] (Termops.names_of_rel_context new_env) Evd.empty typ_of_id in raw_typ_of_id )::acc @@ -951,7 +951,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = GRef (Loc.ghost,Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] - (Termops.names_of_rel_context env) + (Termops.names_of_rel_context env) Evd.empty p) params)@(Array.to_list (Array.make (List.length args' - nparam) @@ -980,10 +980,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | Name id' -> (id',Detyping.detype false [] (Termops.names_of_rel_context env) + Evd.empty arg)::acc else if isVar var_as_constr then (destVar var_as_constr,Detyping.detype false [] (Termops.names_of_rel_context env) + Evd.empty arg)::acc else acc ) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 953e1f049c..e2273972e7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -538,7 +538,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) Evd.empty)) typel in let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> @@ -768,8 +768,8 @@ let make_graph (f_ref:global_reference) = let env = Global.env () in let extern_body,extern_type = with_full_print (fun () -> - (Constrextern.extern_constr false env body, - Constrextern.extern_type false env + (Constrextern.extern_constr false env Evd.empty body, + Constrextern.extern_type false env Evd.empty ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type) ) ) diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 0886e7f711..0117adede0 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -773,7 +773,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let mkrawcor nme avoid typ = (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in - Detyping.detype false (Id.Set.elements avoid) [] substindtyp in + Detyping.detype false (Id.Set.elements avoid) [] Evd.empty substindtyp in let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) @@ -821,11 +821,11 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let typ = glob_constr_to_constr_expr tp in LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) [] params in - let concl = Constrextern.extern_constr false (Global.env()) concl in + let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in let arity,_ = List.fold_left (fun (acc,env) (nm,_,c) -> - let typ = Constrextern.extern_constr false env c in + let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (nm,None,c) env in CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) @@ -854,7 +854,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> - let traw = Detyping.detype false [] [] t in + let traw = Detyping.detype false [] [] Evd.empty t in GProd (Loc.ghost,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false diff --git a/pretyping/cases.ml b/pretyping/cases.ml index f9bd2d4058..62bfef8866 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -41,22 +41,24 @@ type pattern_matching_error = | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array -exception PatternMatchingError of env * pattern_matching_error +exception PatternMatchingError of env * evar_map * pattern_matching_error -let raise_pattern_matching_error (loc,ctx,te) = - Loc.raise loc (PatternMatchingError(ctx,te)) +let raise_pattern_matching_error (loc,env,sigma,te) = + Loc.raise loc (PatternMatchingError(env,sigma,te)) -let error_bad_pattern_loc loc cstr ind = - raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind)) +let error_bad_pattern_loc loc env sigma cstr ind = + raise_pattern_matching_error + (loc, env, sigma, BadPattern (cstr,ind)) let error_bad_constructor_loc loc cstr ind = - raise_pattern_matching_error (loc, Global.env(), BadConstructor (cstr,ind)) + raise_pattern_matching_error + (loc, Global.env(), Evd.empty, BadConstructor (cstr,ind)) let error_wrong_numarg_constructor_loc loc env c n = - raise_pattern_matching_error (loc, env, WrongNumargConstructor(c,n)) + raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargConstructor(c,n)) let error_wrong_numarg_inductive_loc loc env c n = - raise_pattern_matching_error (loc, env, WrongNumargInductive(c,n)) + raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n)) let rec list_try_compile f = function | [a] -> f a @@ -479,18 +481,18 @@ let check_and_adjust_constructor env ind cstrs = function with Not_found -> error_bad_constructor_loc loc cstr ind -let check_all_variables typ mat = +let check_all_variables env sigma typ mat = List.iter (fun eqn -> match current_pattern eqn with | PatVar (_,id) -> () | PatCstr (loc,cstr_sp,_,_) -> - error_bad_pattern_loc loc cstr_sp typ) + error_bad_pattern_loc loc env sigma cstr_sp typ) mat let check_unused_pattern env eqn = if not !(eqn.used) then raise_pattern_matching_error - (eqn.eqn_loc, env, UnusedClause eqn.patterns) + (eqn.eqn_loc, env, Evd.empty, UnusedClause eqn.patterns) let set_used_pattern eqn = eqn.used := true @@ -1254,7 +1256,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let () = match submat with | [] -> raise_pattern_matching_error - (Loc.ghost, pb.env, NonExhaustive (complete_history history)) + (Loc.ghost, pb.env, Evd.empty, NonExhaustive (complete_history history)) | _ -> () in @@ -1301,7 +1303,7 @@ and match_current pb (initial,tomatch) = let ((current,typ),deps,dep) = tomatch in match typ with | NotInd (_,typ) -> - check_all_variables typ pb.mat; + check_all_variables pb.env !(pb.evdref) typ pb.mat; compile_all_variables initial tomatch pb | IsInd (_,(IndType(indf,realargs) as indt),names) -> let mind,_ = dest_ind_family indf in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d875edd796..e51055cef6 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -27,7 +27,7 @@ type pattern_matching_error = | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array -exception PatternMatchingError of env * pattern_matching_error +exception PatternMatchingError of env * evar_map * pattern_matching_error val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 3a355b91a9..3bd23a8025 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -393,7 +393,7 @@ let detype_instance l = if Univ.Instance.is_empty l then None else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l))) -let rec detype (isgoal:bool) avoid env t = +let rec detype isgoal avoid env sigma t = match kind_of_term (collapse_appl t) with | Rel n -> (try match lookup_name_of_rel n env with @@ -404,25 +404,26 @@ let rec detype (isgoal:bool) avoid env t = in GVar (dl, Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) - GEvar (dl, Evar.unsafe_of_int n, None) + (* using numbers to be unparsable *) + GEvar (dl, Id.of_string (string_of_int n), None) | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id, None) with Not_found -> GVar (dl, id)) | Sort s -> GSort (dl,detype_sort s) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> - detype isgoal avoid env c1 + detype isgoal avoid env sigma c1 | Cast (c1,k,c2) -> - let d1 = detype isgoal avoid env c1 in - let d2 = detype isgoal avoid env c2 in + let d1 = detype isgoal avoid env sigma c1 in + let d2 = detype isgoal avoid env sigma c2 in let cast = match k with | VMcast -> CastVM d2 | NATIVEcast -> CastNative d2 | _ -> CastConv d2 in GCast(dl,d1,cast) - | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c - | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c - | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c + | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env sigma na ty c + | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env sigma na ty c + | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env sigma na b c | App (f,args) -> let mkapp f' args' = match f' with @@ -430,30 +431,34 @@ let rec detype (isgoal:bool) avoid env t = GApp (dl,f',args''@args') | _ -> GApp (dl,f',args') in - mkapp (detype isgoal avoid env f) - (Array.map_to_list (detype isgoal avoid env) args) + mkapp (detype isgoal avoid env sigma f) + (Array.map_to_list (detype isgoal avoid env sigma) args) | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u) | Proj (p,c) -> - GProj (dl, p, detype isgoal avoid env c) - | Evar (ev,cl) -> - GEvar (dl, ev, - Some (List.map (detype isgoal avoid env) (Array.to_list cl))) + GProj (dl, p, detype isgoal avoid env sigma c) + | Evar (evk,cl) -> + let id,l = + try Evd.evar_ident evk sigma, + Some (Evd.evar_instance_array isVarId (Evd.find sigma evk) cl) + with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), None in + GEvar (dl,id, + Option.map (List.map (on_snd (detype isgoal avoid env sigma))) l) | Ind (ind_sp,u) -> GRef (dl, IndRef ind_sp, detype_instance u) | Construct (cstr_sp,u) -> GRef (dl, ConstructRef cstr_sp, detype_instance u) | Case (ci,p,c,bl) -> let comp = computable p (ci.ci_pp_info.ind_nargs) in - detype_case comp (detype isgoal avoid env) - (detype_eqns isgoal avoid env ci comp) + detype_case comp (detype isgoal avoid env sigma) + (detype_eqns isgoal avoid env sigma ci comp) is_nondep_branch avoid (ci.ci_ind,ci.ci_pp_info.style, ci.ci_cstr_ndecls,ci.ci_pp_info.ind_nargs) (Some p) c bl - | Fix (nvn,recdef) -> detype_fix isgoal avoid env nvn recdef - | CoFix (n,recdef) -> detype_cofix isgoal avoid env n recdef + | Fix (nvn,recdef) -> detype_fix isgoal avoid env sigma nvn recdef + | CoFix (n,recdef) -> detype_cofix isgoal avoid env sigma n recdef -and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = +and detype_fix isgoal avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left (fun (avoid, env, l) na -> @@ -462,14 +467,14 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = (avoid, env, []) names in let n = Array.length tys in let v = Array.map3 - (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t)) + (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env sigma c (lift n t)) bodies tys vn in GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -and detype_cofix isgoal avoid env n (names,tys,bodies) = +and detype_cofix isgoal avoid env sigma n (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left (fun (avoid, env, l) na -> @@ -478,14 +483,14 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) = (avoid, env, []) names in let ntys = Array.length tys in let v = Array.map2 - (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t)) + (fun c t -> share_names isgoal 0 [] def_avoid def_env sigma c (lift ntys t)) bodies tys in GRec(dl,GCoFix n,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -and share_names isgoal n l avoid env c t = +and share_names isgoal n l avoid env sigma c t = match kind_of_term c, kind_of_term t with (* factorize even when not necessary to have better presentation *) | Lambda (na,t,c), Prod (na',t',c') -> @@ -493,45 +498,45 @@ and share_names isgoal n l avoid env c t = Name _, _ -> na | _, Name _ -> na' | _ -> na in - let t = detype isgoal avoid env t in + let t = detype isgoal avoid env sigma t in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) env in - share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env c c' + share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env sigma c c' (* May occur for fix built interactively *) | LetIn (na,b,t',c), _ when n > 0 -> - let t' = detype isgoal avoid env t' in - let b = detype isgoal avoid env b in + let t' = detype isgoal avoid env sigma t' in + let b = detype isgoal avoid env sigma b in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) env in - share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c (lift 1 t) + share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env sigma c (lift 1 t) (* Only if built with the f/n notation or w/o let-expansion in types *) | _, LetIn (_,b,_,t) when n > 0 -> - share_names isgoal n l avoid env c (subst1 b t) + share_names isgoal n l avoid env sigma c (subst1 b t) (* If it is an open proof: we cheat and eta-expand *) | _, Prod (na',t',c') when n > 0 -> - let t' = detype isgoal avoid env t' in + let t' = detype isgoal avoid env sigma t' in let id = next_name_away na' avoid in let avoid = id::avoid and env = add_name (Name id) env in let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c' + share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> if n>0 then msg_warning (strbrk "Detyping.detype: cannot factorize fix enough"); - let c = detype isgoal avoid env c in - let t = detype isgoal avoid env t in + let c = detype isgoal avoid env sigma c in + let t = detype isgoal avoid env sigma t in (List.rev l,c,t) -and detype_eqns isgoal avoid env ci computable constructs consnargsl bl = +and detype_eqns isgoal avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous isgoal (avoid,env) ci bl in - List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c)) + List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env sigma c)) mat with e when Errors.noncritical e -> Array.to_list - (Array.map3 (detype_eqn isgoal avoid env) constructs consnargsl bl) + (Array.map3 (detype_eqn isgoal avoid env sigma) constructs consnargsl bl) -and detype_eqn isgoal avoid env constr construct_nargs branch = +and detype_eqn isgoal avoid env sigma constr construct_nargs branch = let make_pat x avoid env b ids = if force_wildcard () && noccurn 1 b then PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids @@ -544,7 +549,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch = if Int.equal n 0 then (dl, Id.Set.elements ids, [PatCstr(dl, constr, List.rev patlist,Anonymous)], - detype isgoal avoid env b) + detype isgoal avoid env sigma b) else match kind_of_term b with | Lambda (x,_,b) -> @@ -569,18 +574,18 @@ and detype_eqn isgoal avoid env constr construct_nargs branch = in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder isgoal bk avoid env na ty c = +and detype_binder isgoal bk avoid env sigma na ty c = let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in let na',avoid' = match bk with | BLetIn -> compute_displayed_let_name_in flag avoid na c | _ -> compute_displayed_name_in flag avoid na c in - let r = detype isgoal avoid' (add_name na' env) c in + let r = detype isgoal avoid' (add_name na' env) sigma c in match bk with - | BProd -> GProd (dl, na',Explicit,detype false avoid env ty, r) - | BLambda -> GLambda (dl, na',Explicit,detype false avoid env ty, r) - | BLetIn -> GLetIn (dl, na',detype false avoid env ty, r) + | BProd -> GProd (dl, na',Explicit,detype false avoid env sigma ty, r) + | BLambda -> GLambda (dl, na',Explicit,detype false avoid env sigma ty, r) + | BLetIn -> GLetIn (dl, na',detype false avoid env sigma ty, r) -let detype_rel_context where avoid env sign = +let detype_rel_context where avoid env sigma sign = let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function | [] -> [] @@ -595,8 +600,8 @@ let detype_rel_context where avoid env sign = else compute_displayed_name_in (RenamingElsewhereFor (env,c)) avoid na c in - let b = Option.map (detype false avoid env) b in - let t = detype false avoid env t in + let b = Option.map (detype false avoid env sigma) b in + let t = detype false avoid env sigma t in (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest in aux avoid env (List.rev sign) @@ -619,7 +624,7 @@ let rec subst_glob_constr subst raw = | GRef (loc,ref,u) -> let ref',t = subst_global subst ref in if ref' == ref then raw else - detype false [] [] t + detype false [] [] Evd.empty t | GVar _ -> raw | GEvar _ -> raw diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 2cca25fd25..8a8302b8bf 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -14,6 +14,7 @@ open Glob_term open Termops open Mod_subst open Misctypes +open Evd (** Should we keep details of universes during detyping ? *) val print_universes : bool ref @@ -27,7 +28,8 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr [isgoal] tells if naming must avoid global-level synonyms as intro does [ctx] gives the names of the free variables *) -val detype : bool -> Id.t list -> names_context -> constr -> glob_constr +val detype : bool -> Id.t list -> names_context -> + evar_map -> constr -> glob_constr val detype_case : bool -> ('a -> glob_constr) -> @@ -40,7 +42,7 @@ val detype_case : val detype_sort : sorts -> glob_sort val detype_rel_context : constr option -> Id.t list -> names_context -> - rel_context -> glob_decl list + evar_map -> rel_context -> glob_decl list (** look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_displayed : env -> constr -> Id.t -> int option diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 6d77658087..9f5de8c903 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -146,13 +146,7 @@ let restrict_evar_key evd evk filter candidates = let candidates = match candidates with | NoUpdate -> evi.evar_candidates | UpdateWith c -> Some c in - let ccl = evi.evar_concl in - let sign = evar_hyps evi in - let src = evi.evar_source in - let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in - let ctxt = Filter.filter_list filter (evar_context evi) in - let id_inst = inst_of_vars ctxt in - Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk + restrict_evar evd evk filter candidates end (* Restrict an applied evar and returns its restriction in the same context *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d14aa23a7e..306032ed9f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -342,6 +342,10 @@ let push_rel_context_to_named_context env typ = let default_source = (Loc.ghost,Evar_kinds.InternalHole) +let restrict_evar evd evk filter candidates = + let evk' = new_untyped_evar () in + Evd.restrict evk evk' filter ?candidates evd, evk' + let new_pure_evar_full evd evi = let evk = new_untyped_evar () in let evd = Evd.add evd evk evi in diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index fc27d4776e..2d3dd33a34 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -48,6 +48,9 @@ val e_new_type_evar : evar_map ref -> val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr +val restrict_evar : evar_map -> existential_key -> Filter.t -> + constr list option -> evar_map * existential_key + (** Polymorphic constants *) val new_global : evar_map -> Globnames.global_reference -> evar_map * constr diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ff04bda809..17928f26ea 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -219,6 +219,17 @@ let map_evar_info f evi = evar_concl = f evi.evar_concl; evar_candidates = Option.map (List.map f) evi.evar_candidates } +type existential_name = Id.t + +let evar_ident_info evi = + match evi.evar_source with + | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id + | _,Evar_kinds.VarInstance id -> id + | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" + | _ -> + let env = reset_with_named_context evi.evar_hyps (Global.env()) in + Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous + (* spiwack: Revised hierarchy : - Evar.Map ( Maps of existential_keys ) - EvarInfoMap ( .t = evar_info Evar.Map.t * evar_info Evar.Map ) @@ -231,7 +242,7 @@ exception NotInstantiatedEvar (* Note: let-in contributes to the instance *) -let make_evar_instance_array info args = +let evar_instance_array test_id info args = let len = Array.length args in let rec instrec filter ctxt i = match filter, ctxt with | [], [] -> @@ -242,7 +253,7 @@ let make_evar_instance_array info args = | true :: filter, (id, _, _) :: ctxt -> if i < len then let c = Array.unsafe_get args i in - if isVarId id c then instrec filter ctxt (succ i) + if test_id id c then instrec filter ctxt (succ i) else (id, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () @@ -250,13 +261,18 @@ let make_evar_instance_array info args = match Filter.repr (evar_filter info) with | None -> let map i (id, _, _) = - if (i < len) then (id, Array.unsafe_get args i) + if (i < len) then + let c = Array.unsafe_get args i in + if test_id id c then None else Some (id,c) else instance_mismatch () in - List.map_i map 0 (evar_context info) + List.map_filter_i map (evar_context info) | Some filter -> instrec filter (evar_context info) 0 +let make_evar_instance_array info args = + evar_instance_array isVarId info args + let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in match inst with @@ -580,6 +596,7 @@ type evar_map = { last_mods : Evar.Set.t; metas : clbinding Metamap.t; effects : Declareops.side_effects; + evar_names : Id.t EvMap.t * existential_key Idmap.t; } (*** Lifting primitive from EvarMap. ***) @@ -594,9 +611,23 @@ let progress_evar_map d1 d2 = let add d e i = match i.evar_body with | Evar_empty -> - { d with undf_evars = EvMap.add e i d.undf_evars; } + let evar_names = + let (evtoid,idtoev as x) = d.evar_names in + if EvMap.mem e evtoid then + x + else + let id = evar_ident_info i in + let id = Namegen.next_ident_away_from id + (fun id -> Idmap.mem id idtoev) in + (EvMap.add e id evtoid, Idmap.add id e idtoev) in + { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } | Evar_defined _ -> - { d with defn_evars = EvMap.add e i d.defn_evars; } + let evar_names = + let (evtoid,idtoev as x) = d.evar_names in + try let id = EvMap.find e evtoid in + (EvMap.remove e evtoid, Idmap.remove id idtoev) + with Not_found -> x in + { d with defn_evars = EvMap.add e i d.defn_evars; evar_names } let remove d e = let undf_evars = EvMap.remove e d.undf_evars in @@ -742,6 +773,7 @@ let empty = { last_mods = Evar.Set.empty; metas = Metamap.empty; effects = Declareops.no_seff; + evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) } let from_env ?ctx e = @@ -772,6 +804,15 @@ let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (find d evk).evar_source +let evar_ident evk evd = + try EvMap.find evk (fst evd.evar_names) + with Not_found -> + (* Unnamed (non-dependent) evar *) + Id.of_string (string_of_existential evk) + +let evar_key id evd = + Idmap.find id (snd evd.evar_names) + let define_aux def undef evk body = let oldinfo = try EvMap.find evk undef @@ -792,7 +833,12 @@ let define evk body evd = | [] -> evd.last_mods | _ -> Evar.Set.add evk evd.last_mods in - { evd with defn_evars; undf_evars; last_mods; } + let evar_names = + let (evtoid,idtoev) = evd.evar_names in + let id = EvMap.find evk evtoid in + (EvMap.remove evk evtoid, Idmap.remove id idtoev) + in + { evd with defn_evars; undf_evars; last_mods; evar_names } let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?(filter=Filter.identity) ?candidates ?(store=Store.empty) evd = @@ -810,7 +856,32 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evar_candidates = candidates; evar_extra = store; } in - { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; } + let evar_names = + let (evtoid,idtoev) = evd.evar_names in + let id = evar_ident_info evar_info in + let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in + (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + in + { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names } + +let restrict evk evk' filter ?candidates evd = + let evar_info = EvMap.find evk evd.undf_evars in + let evar_info' = + { evar_info with evar_filter = filter; + evar_candidates = candidates; + evar_extra = Store.empty } in + let evar_names = + let (evtoid,idtoev) = evd.evar_names in + let id = EvMap.find evk evtoid in + (EvMap.add evk' id (EvMap.remove evk evtoid), + Idmap.add id evk' (Idmap.remove id idtoev)) + in + let ctxt = Filter.filter_list filter (evar_context evar_info) in + let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in + let body = mkEvar(evk',id_inst) in + let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in + { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; + defn_evars; evar_names } (* extracts conversion problems that satisfy predicate p *) (* Note: conv_pbs not satisying p are stored back in reverse order *) @@ -1273,7 +1344,9 @@ let set_metas evd metas = { conv_pbs = evd.conv_pbs; last_mods = evd.last_mods; metas; - effects = evd.effects; } + effects = evd.effects; + evar_names = evd.evar_names; +} let meta_list evd = metamap_to_list evd.metas @@ -1406,6 +1479,11 @@ let subst_defined_metas bl c = | _ -> map_constr substrec c in try Some (substrec c) with Not_found -> None +let evar_source_of_meta mv evd = + match meta_name evd mv with + | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar) + | Name id -> (Loc.ghost,Evar_kinds.VarInstance id) + (*******************************************************************) type open_constr = evar_map * constr @@ -1633,23 +1711,24 @@ let pr_evar_map_gen with_univs pr_evars sigma = in evs ++ svs ++ cstrs ++ metas -let pr_evar_list l = +let pr_evar_list sigma l = let pr (ev, evi) = h 0 (str (string_of_existential ev) ++ - str "==" ++ pr_evar_info evi) + str "==" ++ pr_evar_info evi ++ + str " {" ++ pr_id (evar_ident ev sigma) ++ str "}") in h 0 (prlist_with_sep fnl pr l) let pr_evar_by_depth depth sigma = match depth with | None -> (* Print all evars *) - str"EVARS:"++brk(0,1)++pr_evar_list (to_list sigma)++fnl() + str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl() | Some n -> (* Print all evars *) str"UNDEFINED EVARS:"++ (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++ brk(0,1)++ - pr_evar_list (evar_dependency_closure n sigma)++fnl() + pr_evar_list sigma (evar_dependency_closure n sigma)++fnl() let pr_evar_by_filter filter sigma = let defined = Evar.Map.filter filter sigma.defn_evars in @@ -1657,12 +1736,12 @@ let pr_evar_by_filter filter sigma = let prdef = if Evar.Map.is_empty defined then mt () else str "DEFINED EVARS:" ++ brk (0, 1) ++ - pr_evar_list (Evar.Map.bindings defined) + pr_evar_list sigma (Evar.Map.bindings defined) in let prundef = if Evar.Map.is_empty undefined then mt () else str "UNDEFINED EVARS:" ++ brk (0, 1) ++ - pr_evar_list (Evar.Map.bindings undefined) + pr_evar_list sigma (Evar.Map.bindings undefined) in prdef ++ prundef diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 28e978edf1..0d88415e2c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -224,6 +224,9 @@ val existential_opt_value : evar_map -> existential -> constr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) +val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info -> + 'a array -> (Id.t * 'a) list + val instantiate_evar_array : evar_info -> constr -> constr array -> constr val subst_evar_defs_light : substitution -> evar_map -> evar_map @@ -241,10 +244,18 @@ val evar_declare : evar_map -> evar_map (** Convenience function. Just a wrapper around {!add}. *) +val restrict : evar -> evar -> Filter.t -> ?candidates:constr list -> + evar_map -> evar_map + val evar_source : existential_key -> evar_map -> Evar_kinds.t located (** Convenience function. Wrapper around {!find} to recover the source of an evar in a given evar map. *) +val evar_ident : existential_key -> evar_map -> Id.t + +val evar_key : Id.t -> evar_map -> existential_key + +val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located (** {5 Side-effects} *) val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 73bb343eeb..8a4fd65a19 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -63,9 +63,9 @@ let cast_type_eq eq t1 t2 = match t1, t2 with let rec glob_constr_eq c1 c2 = match c1, c2 with | GRef (_, gr1, _), GRef (_, gr2, _) -> eq_gr gr1 gr2 | GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2 -| GEvar (_, ev1, arg1), GEvar (_, ev2, arg2) -> - Evar.equal ev1 ev2 && - Option.equal (fun l1 l2 -> List.equal glob_constr_eq l1 l2) arg1 arg2 +| GEvar (_, id1, arg1), GEvar (_, id2, arg2) -> + Id.equal id1 id2 && + Option.equal (fun l1 l2 -> List.equal instance_eq l1 l2) arg1 arg2 | GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) -> (b1 : bool) == b2 && Id.equal pat1 pat2 | GApp (_, f1, arg1), GApp (_, f2, arg2) -> @@ -134,6 +134,9 @@ and fix_recursion_order_eq o1 o2 = match o1, o2 with glob_constr_eq c1 c2 && Option.equal glob_constr_eq o1 o2 | _ -> false +and instance_eq (x1,c1) (x2,c2) = + Id.equal x1 x2 && glob_constr_eq c1 c2 + let map_glob_constr_left_to_right f = function | GApp (loc,g,args) -> let comp1 = f g in diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 8e1b51a7d3..245c7f9437 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -120,7 +120,8 @@ let hdchar env c = | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> let id = match lna.(i) with Name id -> id | _ -> assert false in lowercase_first_char id - | Meta _ | Evar _ | Case (_, _, _, _) -> "y" + | Evar _ (* We could do better... *) + | Meta _ | Case (_, _, _, _) -> "y" in hdrec 0 c diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 5828e7f433..4206663566 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -157,7 +157,7 @@ let pattern_of_constr sigma t = | Evar_kinds.MatchingVar (b,id) -> ctx := (id,None,existential_type sigma ev)::!ctx; assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt) + | Evar_kinds.GoalEvar _ -> PEvar (evk,Array.map pattern_of_constr ctxt) | _ -> PMeta None) | Case (ci,p,a,br) -> let cip = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6d98602b51..f26d2d638e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -386,6 +386,8 @@ let is_GHole = function | GHole _ -> true | _ -> false +let evars = ref Id.Map.empty + let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type resolve_tc in @@ -405,13 +407,17 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id) tycon - | GEvar (loc, evk, instopt) -> + | GEvar (loc, id, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) + let evk = + try Evd.evar_key id !evdref + with Not_found -> + user_err_loc (loc,"",str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = match instopt with | None -> Array.of_list (instance_from_named_context hyps) - | Some inst -> failwith "Evar subtitutions not implemented" in + | Some inst -> error "Non-identity subtitutions of existential variables not implemented" in let c = mkEvar (evk, args) in let j = (Retyping.get_judgment_of env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index ceb01fd95c..a00fec30e8 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,9 +1,9 @@ Locusops Termops +Namegen Evd Reductionops Vnorm -Namegen Inductiveops Nativenorm Retyping diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b4c578abb2..91447573f2 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -28,7 +28,7 @@ open Pretype_errors (* Errors *) type reduction_tactic_error = - InvalidAbstraction of env * constr * (env * Type_errors.type_error) + InvalidAbstraction of env * Evd.evar_map * constr * (env * Type_errors.type_error) exception ReductionTacticError of reduction_tactic_error @@ -1112,7 +1112,7 @@ let pattern_occs loccs_trm env sigma c = let _ = Typing.type_of env sigma abstr_trm in applist(abstr_trm, List.map snd loccs_trm) with Type_errors.TypeError (env',t) -> - raise (ReductionTacticError (InvalidAbstraction (env,abstr_trm,(env',t)))) + raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) (* Used in several tactics. *) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 6d12d5d44c..db59787a11 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -17,7 +17,7 @@ open Locus open Univ type reduction_tactic_error = - InvalidAbstraction of env * constr * (env * Type_errors.type_error) + InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) exception ReductionTacticError of reduction_tactic_error diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a3bd06ed5d..c74ed19a8b 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -497,7 +497,7 @@ let is_instance = function | _ -> false let is_implicit_arg = function -| Evar_kinds.GoalEvar -> false +| Evar_kinds.GoalEvar _ -> false | _ -> true (* match k with *) (* ImplicitArg (ref, (n, id), b) -> true *) @@ -538,10 +538,10 @@ open Evar_kinds type evar_filter = existential_key -> Evar_kinds.t -> bool let all_evars _ _ = true -let all_goals _ = function GoalEvar -> true | _ -> false +let all_goals _ = function GoalEvar _ -> true | _ -> false let no_goals ev evi = not (all_goals ev evi) let no_goals_or_obligations _ = function - | GoalEvar | QuestionMark _ -> false + | GoalEvar _ | QuestionMark _ -> false | _ -> true let mark_resolvability filter b sigma = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d89cde1ae9..63c30eb351 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -125,11 +125,6 @@ let rec subst_meta_instances bl c = (** [env] should be the context in which the metas live *) -let evar_source_of_meta mv evd = - match Evd.meta_name evd mv with - | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar) - | Name id -> (Loc.ghost,Evar_kinds.VarInstance id) - let pose_all_metas_as_evars env evd t = let evdref = ref evd in let rec aux t = match kind_of_term t with @@ -139,7 +134,7 @@ let pose_all_metas_as_evars env evd t = | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in - let src = evar_source_of_meta mv !evdref in + let src = Evd.evar_source_of_meta mv !evdref in let ev = Evarutil.e_new_evar evdref env ~src ty in evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; ev) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0fb97ad16e..6956ec4481 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -174,15 +174,13 @@ let pr_prim_token = function | Numeral n -> str (Bigint.to_string n) | String s -> qs s -let pr_evar pr n l = - hov 0 (str (Evd.string_of_existential n) ++ +let pr_evar pr id l = + hov 0 (str "?" ++ pr_id id ++ (match l with + | None | Some [] -> mt() | Some l -> - spc () ++ pr_in_comment - (fun l -> - str"[" ++ hov 0 (prlist_with_sep pr_comma (pr ltop) l) ++ str"]") - (List.rev l) - | None -> mt())) + let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in + str"@{" ++ hov 0 (prlist_with_sep pr_comma f l) ++ str"}")) let las = lapp let lpator = 100 diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 647d5702e0..841eb60392 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1096,7 +1096,7 @@ let _ = Hook.set Tactic_debug.tactic_printer (fun x -> pr_glob_tactic (Global.env()) x) let _ = Hook.set Tactic_debug.match_pattern_printer - (fun env hyp -> pr_match_pattern (pr_constr_pattern_env env) hyp) + (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp) let _ = Hook.set Tactic_debug.match_rule_printer (fun rl -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 6e45cb6b07..b084c0dd1c 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -38,7 +38,7 @@ type object_pr = { print_named_decl : Id.t * constr option * types -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds; } @@ -395,9 +395,9 @@ let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MOD (**** Printing declarations and judgments *) (**** Gallina layer *****) -let gallina_print_typed_value_in_env env (trm,typ) = - (pr_lconstr_env env trm ++ fnl () ++ - str " : " ++ pr_ltype_env env typ) +let gallina_print_typed_value_in_env env sigma (trm,typ) = + (pr_lconstr_env env sigma trm ++ fnl () ++ + str " : " ++ pr_ltype_env env sigma typ) (* To be improved; the type should be used to provide the types in the abstractions. This should be done recursively inside pr_lconstr, so that @@ -541,9 +541,9 @@ let gallina_print_context with_values = in prec -let gallina_print_eval red_fun env evmap _ {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env evmap trm in - (str " = " ++ gallina_print_typed_value_in_env env (ntrm,typ)) +let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = + let ntrm = red_fun env sigma trm in + (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) (******************************************) (**** Printing abstraction layer *) @@ -581,15 +581,15 @@ let print_eval x = !object_pr.print_eval x (**** Printing declarations and judgments *) (**** Abstract layer *****) -let print_typed_value x = print_typed_value_in_env (Global.env ()) x +let print_typed_value x = print_typed_value_in_env (Global.env ()) Evd.empty x -let print_judgment env {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env (trm, typ) +let print_judgment env sigma {uj_val=trm;uj_type=typ} = + print_typed_value_in_env env sigma (trm, typ) -let print_safe_judgment env j = +let print_safe_judgment env sigma j = let trm = Safe_typing.j_val j in let typ = Safe_typing.j_type j in - print_typed_value_in_env env (trm, typ) + print_typed_value_in_env env sigma (trm, typ) (*********************) (* *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 595637745d..9d558733a5 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -27,8 +27,8 @@ val print_full_context_typ : unit -> std_ppcmds val print_full_pure_context : unit -> std_ppcmds val print_sec_context : reference -> std_ppcmds val print_sec_context_typ : reference -> std_ppcmds -val print_judgment : env -> unsafe_judgment -> std_ppcmds -val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds +val print_judgment : env -> Evd.evar_map -> unsafe_judgment -> std_ppcmds +val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds @@ -69,7 +69,7 @@ type object_pr = { print_named_decl : Id.t * constr option * types -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds } diff --git a/printing/printer.ml b/printing/printer.ml index f105e8031c..781f89f1a1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -28,6 +28,11 @@ let emacs_str s = let delayed_emacs_cmd s = if !Flags.print_emacs then s () else str "" +let get_current_context () = + try Pfedit.get_current_goal_context () + with e when Logic.catchable_exception e -> + (Evd.empty, Global.env()) + (**********************************************************************) (** Terms *) @@ -39,10 +44,10 @@ let delayed_emacs_cmd s = and only names of goal/section variables and rel names that do _not_ occur in the scope of the binder to be printed are avoided. *) -let pr_constr_core goal_concl_style env t = - pr_constr_expr (extern_constr goal_concl_style env t) -let pr_lconstr_core goal_concl_style env t = - pr_lconstr_expr (extern_constr goal_concl_style env t) +let pr_constr_core goal_concl_style env sigma t = + pr_constr_expr (extern_constr goal_concl_style env sigma t) +let pr_lconstr_core goal_concl_style env sigma t = + pr_lconstr_expr (extern_constr goal_concl_style env sigma t) let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env @@ -50,45 +55,59 @@ let pr_constr_env env = pr_constr_core false env let pr_lconstr_goal_style_env env = pr_lconstr_core true env let pr_constr_goal_style_env env = pr_constr_core true env -let pr_open_lconstr_env env (_,c) = pr_lconstr_env env c -let pr_open_constr_env env (_,c) = pr_constr_env env c +let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c +let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c (* NB do not remove the eta-redexes! Global.env() has side-effects... *) -let pr_lconstr t = pr_lconstr_env (Global.env()) t -let pr_constr t = pr_constr_env (Global.env()) t +let pr_lconstr t = + let (sigma, env) = get_current_context () in + pr_lconstr_env env sigma t +let pr_constr t = + let (sigma, env) = get_current_context () in + pr_constr_env env sigma t let pr_open_lconstr (_,c) = pr_lconstr c let pr_open_constr (_,c) = pr_constr c -let pr_constr_under_binders_env_gen pr env (ids,c) = +let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* Warning: clashes can occur with variables of same name in env but *) (* we also need to preserve the actual names of the patterns *) (* So what to do? *) let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in - pr (Termops.push_rels_assum assums env) c + pr (Termops.push_rels_assum assums env) sigma c let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env -let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c -let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c +let pr_constr_under_binders c = + let (sigma, env) = get_current_context () in + pr_constr_under_binders_env env sigma c +let pr_lconstr_under_binders c = + let (sigma, env) = get_current_context () in + pr_lconstr_under_binders_env env sigma c -let pr_type_core goal_concl_style env t = - pr_constr_expr (extern_type goal_concl_style env t) -let pr_ltype_core goal_concl_style env t = - pr_lconstr_expr (extern_type goal_concl_style env t) +let pr_type_core goal_concl_style env sigma t = + pr_constr_expr (extern_type goal_concl_style env sigma t) +let pr_ltype_core goal_concl_style env sigma t = + pr_lconstr_expr (extern_type goal_concl_style env sigma t) let pr_goal_concl_style_env env = pr_ltype_core true env let pr_ltype_env env = pr_ltype_core false env let pr_type_env env = pr_type_core false env -let pr_ltype t = pr_ltype_env (Global.env()) t -let pr_type t = pr_type_env (Global.env()) t +let pr_ltype t = + let (sigma, env) = get_current_context () in + pr_ltype_env env sigma t +let pr_type t = + let (sigma, env) = get_current_context () in + pr_type_env env sigma t -let pr_ljudge_env env j = - (pr_lconstr_env env j.uj_val, pr_lconstr_env env j.uj_type) +let pr_ljudge_env env sigma j = + (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type) -let pr_ljudge j = pr_ljudge_env (Global.env()) j +let pr_ljudge j = + let (sigma, env) = get_current_context () in + pr_ljudge_env env sigma j let pr_lglob_constr_env env c = pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c) @@ -96,26 +115,30 @@ let pr_glob_constr_env env c = pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c) let pr_lglob_constr c = - pr_lconstr_expr (extern_glob_constr Id.Set.empty c) + let (sigma, env) = get_current_context () in + pr_lglob_constr_env env c let pr_glob_constr c = - pr_constr_expr (extern_glob_constr Id.Set.empty c) + let (sigma, env) = get_current_context () in + pr_glob_constr_env env c -let pr_cases_pattern t = - pr_cases_pattern_expr (extern_cases_pattern Id.Set.empty t) +let pr_lconstr_pattern_env env sigma c = + pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c) +let pr_constr_pattern_env env sigma c = + pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c) -let pr_lconstr_pattern_env env c = - pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c) -let pr_constr_pattern_env env c = - pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c) +let pr_cases_pattern t = + pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t) let pr_lconstr_pattern t = - pr_lconstr_pattern_expr (extern_constr_pattern Termops.empty_names_context t) + let (sigma, env) = get_current_context () in + pr_lconstr_pattern_env env sigma t let pr_constr_pattern t = - pr_constr_pattern_expr (extern_constr_pattern Termops.empty_names_context t) + let (sigma, env) = get_current_context () in + pr_constr_pattern_env env sigma t let pr_sort s = pr_glob_sort (extern_sort s) -let _ = Termops.set_print_constr pr_lconstr_env +let _ = Termops.set_print_constr (fun env -> pr_lconstr_env env Evd.empty) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" let pr_univ_cstr (c:Univ.constraints) = @@ -157,7 +180,7 @@ let dirpath_of_global = function let qualid_of_global env r = Libnames.make_qualid (dirpath_of_global r) (id_of_global env r) -let safe_gen f env c = +let safe_gen f env sigma c = let orig_extern_ref = Constrextern.get_extern_reference () in let extern_ref loc vars r = try orig_extern_ref loc vars r @@ -166,7 +189,7 @@ let safe_gen f env c = in Constrextern.set_extern_reference extern_ref; try - let p = f env c in + let p = f env sigma c in Constrextern.set_extern_reference orig_extern_ref; p with e when Errors.noncritical e -> @@ -175,8 +198,13 @@ let safe_gen f env c = let safe_pr_lconstr_env = safe_gen pr_lconstr_env let safe_pr_constr_env = safe_gen pr_constr_env -let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t -let safe_pr_constr t = safe_pr_constr_env (Global.env()) t +let safe_pr_lconstr t = + let (sigma, env) = get_current_context () in + safe_pr_lconstr_env env sigma t + +let safe_pr_constr t = + let (sigma, env) = get_current_context () in + safe_pr_constr_env env sigma t let pr_universe_ctx c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then @@ -197,10 +225,10 @@ let pr_puniverses f env (c,u) = else mt ()) let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) -let pr_existential_key evk = str (string_of_existential evk) -let pr_existential env ev = pr_lconstr_env env (mkEvar ev) -let pr_inductive env ind = pr_lconstr_env env (mkInd ind) -let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr) +let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma) +let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) +let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind) +let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr) let pr_pconstant = pr_puniverses pr_constant let pr_pinductive = pr_puniverses pr_inductive @@ -219,33 +247,33 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) -let pr_var_decl_skel pr_id env (id,c,typ) = +let pr_var_decl_skel pr_id env sigma (id,c,typ) = let pbody = match c with | None -> (mt ()) | Some c -> (* Force evaluation *) - let pb = pr_lconstr_core true env c in + let pb = pr_lconstr_core true env sigma c in let pb = if isCast c then surround pb else pb in (str" := " ++ pb ++ cut () ) in - let pt = pr_ltype_core true env typ in + let pt = pr_ltype_core true env sigma typ in let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) -let pr_var_decl env (id,c,typ) = - pr_var_decl_skel pr_id env (id,c,typ) +let pr_var_decl env sigma (id,c,typ) = + pr_var_decl_skel pr_id env sigma (id,c,typ) -let pr_var_list_decl env (l,c,typ) = - hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env (l,c,typ)) +let pr_var_list_decl env sigma (l,c,typ) = + hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) -let pr_rel_decl env (na,c,typ) = +let pr_rel_decl env sigma (na,c,typ) = let pbody = match c with | None -> mt () | Some c -> (* Force evaluation *) - let pb = pr_lconstr_core true env c in + let pb = pr_lconstr_core true env sigma c in let pb = if isCast c then surround pb else pb in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = pr_ltype_core true env typ in + let ptyp = pr_ltype_core true env sigma typ in match na with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) @@ -256,48 +284,48 @@ let pr_rel_decl env (na,c,typ) = * It's printed out from outermost to innermost, so it's readable. *) (* Prints a signature, all declarations on the same line if possible *) -let pr_named_context_of env = - let make_decl_list env d pps = pr_var_decl env d :: pps in +let pr_named_context_of env sigma = + let make_decl_list env d pps = pr_var_decl env sigma d :: pps in let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) -let pr_named_context env ne_context = +let pr_named_context env sigma ne_context = hv 0 (Context.fold_named_context - (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d) + (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) ne_context ~init:(mt ())) -let pr_rel_context env rel_context = - pr_binders (extern_rel_context None env rel_context) +let pr_rel_context env sigma rel_context = + pr_binders (extern_rel_context None env sigma rel_context) -let pr_rel_context_of env = - pr_rel_context env (rel_context env) +let pr_rel_context_of env sigma = + pr_rel_context env sigma (rel_context env) (* Prints an env (variables and de Bruijn). Separator: newline *) -let pr_context_unlimited env = +let pr_context_unlimited env sigma = let sign_env = fold_named_context (fun env d pps -> - let pidt = pr_var_decl env d in (pps ++ fnl () ++ pidt)) + let pidt = pr_var_decl env sigma d in (pps ++ fnl () ++ pidt)) env ~init:(mt ()) in let db_env = fold_rel_context (fun env d pps -> - let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat)) + let pnat = pr_rel_decl env sigma d in (pps ++ fnl () ++ pnat)) env ~init:(mt ()) in (sign_env ++ db_env) -let pr_ne_context_of header env = +let pr_ne_context_of header env sigma = if List.is_empty (Environ.rel_context env) && List.is_empty (Environ.named_context env) then (mt ()) - else let penv = pr_context_unlimited env in (header ++ penv ++ fnl ()) + else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ()) -let pr_context_limit n env = +let pr_context_limit n env sigma = let named_context = Environ.named_context env in let lgsign = List.length named_context in if n >= lgsign then - pr_context_unlimited env + pr_context_unlimited env sigma else let k = lgsign-n in let _,sign_env = @@ -306,7 +334,7 @@ let pr_context_limit n env = if i < k then (i+1, (pps ++str ".")) else - let pidt = pr_var_decl env d in + let pidt = pr_var_decl env sigma d in (i+1, (pps ++ fnl () ++ str (emacs_str "") ++ pidt))) @@ -315,7 +343,7 @@ let pr_context_limit n env = let db_env = fold_rel_context (fun env d pps -> - let pnat = pr_rel_decl env d in + let pnat = pr_rel_decl env sigma d in (pps ++ fnl () ++ str (emacs_str "") ++ pnat)) @@ -323,9 +351,9 @@ let pr_context_limit n env = in (sign_env ++ db_env) -let pr_context_of env = match Flags.print_hyps_limit () with - | None -> hv 0 (pr_context_unlimited env) - | Some n -> hv 0 (pr_context_limit n env) +let pr_context_of env sigma = match Flags.print_hyps_limit () with + | None -> hv 0 (pr_context_unlimited env sigma) + | Some n -> hv 0 (pr_context_limit n env sigma) (* display goal parts (Proof mode) *) @@ -350,8 +378,8 @@ let default_pr_goal gs = let env = Goal.V82.env sigma g in let preamb,thesis,penv,pc = mt (), mt (), - pr_context_of env, - pr_goal_concl_style_env env (Goal.V82.concl sigma g) + pr_context_of env sigma, + pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ @@ -368,42 +396,42 @@ let pr_goal_tag g = let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in - let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in + let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in str (emacs_str "") ++ str "subgoal " ++ int n ++ pr_goal_tag g ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) -let pr_evgl_sign gl = - let ps = pr_named_context_of (evar_env gl) in - let _, l = match Filter.repr (evar_filter gl) with +let pr_evgl_sign sigma evi = + let env = evar_env evi in + let ps = pr_named_context_of env sigma in + let _, l = match Filter.repr (evar_filter evi) with | None -> [], [] - | Some f -> List.filter2 (fun b c -> not b) f (evar_context gl) + | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in let ids = List.rev_map pi1 l in let warn = if List.is_empty ids then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") in - let pc = pr_lconstr gl.evar_concl in + let pc = pr_lconstr_env env sigma evi.evar_concl in hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn) (* Print an existential variable *) -let pr_evar (ev, evd) = - let pegl = pr_evgl_sign evd in - (hov 0 (str (string_of_existential ev) ++ str " : " ++ pegl)) +let pr_evar sigma (evk, evi) = + let pegl = pr_evgl_sign sigma evi in + hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl) (* Print an enumerated list of existential variables *) -let rec pr_evars_int i = function +let rec pr_evars_int sigma i = function | [] -> mt () - | (ev,evd)::rest -> - let pegl = pr_evgl_sign evd in + | (evk,evi)::rest -> (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ - str (string_of_existential ev) ++ str " : " ++ pegl)) ++ - (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int (i+1) rest) + pr_evar sigma (evk,evi))) ++ + (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int sigma (i+1) rest) -let pr_evars_int i evs = pr_evars_int i (Evar.Map.bindings evs) +let pr_evars_int sigma i evs = pr_evars_int sigma i (Evar.Map.bindings evs) let default_pr_subgoal n sigma = let rec prrec p = function @@ -423,13 +451,13 @@ let emacs_print_dependent_evars sigma seeds = let evars = Evarutil.gather_dependent_evars sigma seeds in let evars = Evar.Map.fold begin fun e i s -> - let e' = str (string_of_existential e) in + let e' = pr_existential_key sigma e in match i with | None -> s ++ str" " ++ e' ++ str " open," | Some i -> s ++ str " " ++ e' ++ str " using " ++ Evar.Set.fold begin fun d s -> - str (string_of_existential d) ++ str " " ++ s + pr_existential_key sigma d ++ str " " ++ s end i (str ",") end evars (str "") in @@ -505,7 +533,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals (str"No more subgoals." ++ emacs_print_dependent_evars sigma seeds) else - let pei = pr_evars_int 1 exl in + let pei = pr_evars_int sigma 1 exl in (str "No more subgoals but non-instantiated existential " ++ str "variables:" ++ fnl () ++ (hov 0 pei) ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ @@ -744,13 +772,14 @@ let pr_polymorphic b = open Termops open Reduction -let print_params env params = - if List.is_empty params then mt () else pr_rel_context env params ++ brk(1,2) +let print_params env sigma params = + if List.is_empty params then mt () + else pr_rel_context env sigma params ++ brk(1,2) let print_constructors envpar names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c) + (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar Evd.empty c) (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -770,8 +799,8 @@ let print_one_inductive env mib ((_,i) as ind) = let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in hov 0 ( - pr_id mip.mind_typename ++ brk(1,4) ++ print_params env params ++ - str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++ + pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++ + str ": " ++ pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes let print_mutual_inductive env mind mib = @@ -828,15 +857,15 @@ let print_record env mind mib = hov 0 ( pr_polymorphic mib.mind_polymorphic ++ str keyword ++ pr_id mip.mind_typename ++ brk(1,4) ++ - print_params env params ++ - str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ + print_params env Evd.empty params ++ + str ": " ++ pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++ str ":= " ++ pr_id mip.mind_consnames.(0)) ++ brk(1,2) ++ hv 2 (str "{ " ++ prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ - pr_lconstr_env envpar c) fields) ++ str" }" ++ + pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++ pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) let pr_mutual_inductive_body env mind mib = diff --git a/printing/printer.mli b/printing/printer.mli index 6be2080535..bac864dc6a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -21,45 +21,45 @@ open Glob_term (** Terms *) -val pr_lconstr_env : env -> constr -> std_ppcmds +val pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds val pr_lconstr : constr -> std_ppcmds -val pr_lconstr_goal_style_env : env -> constr -> std_ppcmds +val pr_lconstr_goal_style_env : env -> evar_map -> constr -> std_ppcmds -val pr_constr_env : env -> constr -> std_ppcmds +val pr_constr_env : env -> evar_map -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds -val pr_constr_goal_style_env : env -> constr -> std_ppcmds +val pr_constr_goal_style_env : env -> evar_map -> constr -> std_ppcmds (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" in case of remaining issues (such as reference not in env). *) -val safe_pr_lconstr_env : env -> constr -> std_ppcmds +val safe_pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds val safe_pr_lconstr : constr -> std_ppcmds -val safe_pr_constr_env : env -> constr -> std_ppcmds +val safe_pr_constr_env : env -> evar_map -> constr -> std_ppcmds val safe_pr_constr : constr -> std_ppcmds -val pr_open_constr_env : env -> open_constr -> std_ppcmds +val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds val pr_open_constr : open_constr -> std_ppcmds -val pr_open_lconstr_env : env -> open_constr -> std_ppcmds +val pr_open_lconstr_env : env -> evar_map -> open_constr -> std_ppcmds val pr_open_lconstr : open_constr -> std_ppcmds -val pr_constr_under_binders_env : env -> constr_under_binders -> std_ppcmds +val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds val pr_constr_under_binders : constr_under_binders -> std_ppcmds -val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds +val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds -val pr_goal_concl_style_env : env -> types -> std_ppcmds -val pr_ltype_env : env -> types -> std_ppcmds +val pr_goal_concl_style_env : env -> evar_map -> types -> std_ppcmds +val pr_ltype_env : env -> evar_map -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds -val pr_type_env : env -> types -> std_ppcmds +val pr_type_env : env -> evar_map -> types -> std_ppcmds val pr_type : types -> std_ppcmds -val pr_ljudge_env : env -> unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge_env : env -> evar_map -> unsafe_judgment -> std_ppcmds * std_ppcmds val pr_ljudge : unsafe_judgment -> std_ppcmds * std_ppcmds val pr_lglob_constr_env : env -> glob_constr -> std_ppcmds @@ -68,10 +68,10 @@ val pr_lglob_constr : glob_constr -> std_ppcmds val pr_glob_constr_env : env -> glob_constr -> std_ppcmds val pr_glob_constr : glob_constr -> std_ppcmds -val pr_lconstr_pattern_env : env -> constr_pattern -> std_ppcmds +val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds val pr_lconstr_pattern : constr_pattern -> std_ppcmds -val pr_constr_pattern_env : env -> constr_pattern -> std_ppcmds +val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds val pr_constr_pattern : constr_pattern -> std_ppcmds val pr_cases_pattern : cases_pattern -> std_ppcmds @@ -90,8 +90,8 @@ val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds val pr_global : global_reference -> std_ppcmds val pr_constant : env -> constant -> std_ppcmds -val pr_existential_key : existential_key -> std_ppcmds -val pr_existential : env -> existential -> std_ppcmds +val pr_existential_key : evar_map -> existential_key -> std_ppcmds +val pr_existential : env -> evar_map -> existential -> std_ppcmds val pr_constructor : env -> constructor -> std_ppcmds val pr_inductive : env -> inductive -> std_ppcmds val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds @@ -103,17 +103,17 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds (** Contexts *) -val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds +val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds -val pr_var_decl : env -> named_declaration -> std_ppcmds -val pr_var_list_decl : env -> named_list_declaration -> std_ppcmds -val pr_rel_decl : env -> rel_declaration -> std_ppcmds +val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds +val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds +val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds -val pr_named_context : env -> named_context -> std_ppcmds -val pr_named_context_of : env -> std_ppcmds -val pr_rel_context : env -> rel_context -> std_ppcmds -val pr_rel_context_of : env -> std_ppcmds -val pr_context_of : env -> std_ppcmds +val pr_named_context : env -> evar_map -> named_context -> std_ppcmds +val pr_named_context_of : env -> evar_map -> std_ppcmds +val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds +val pr_rel_context_of : env -> evar_map -> std_ppcmds +val pr_context_of : env -> evar_map -> std_ppcmds (** Predicates *) @@ -131,8 +131,8 @@ val pr_concl : int -> evar_map -> goal -> std_ppcmds val pr_open_subgoals : ?proof:Proof.proof -> unit -> std_ppcmds val pr_nth_open_subgoal : int -> std_ppcmds -val pr_evar : (evar * evar_info) -> std_ppcmds -val pr_evars_int : int -> evar_info Evar.Map.t -> std_ppcmds +val pr_evar : evar_map -> (evar * evar_info) -> std_ppcmds +val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds diff --git a/printing/printmod.ml b/printing/printmod.ml index ffee2e244b..488ac71772 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -146,13 +146,13 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env + hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) (Typeops.type_of_constant_type env cb.const_type)) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env (Mod_subst.force_constr l)) + Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ Printer.pr_universe_ctx cb.const_universes) | SFBmind mib -> diff --git a/proofs/clenv.ml b/proofs/clenv.ml index c6f0f2ee0d..6f607133d7 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -270,6 +270,33 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl = clenv_unify CUMUL ~flags (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv +let adjust_meta_source evd mv = function + | loc,Evar_kinds.VarInstance id -> + let rec match_name c l = + match kind_of_term c, l with + | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id + | Lambda (_,_,c), a::l -> match_name c l + | _ -> None in + (* This is very ad hoc code so that an evar inherits the name of the binder + in situations like "ex_intro (fun x => P) ?ev p" *) + let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) -> + if Metaset.mem mv t.freemetas then + let f,l = decompose_app t.rebus in + match kind_of_term f with + | Meta mv'' -> + (match meta_opt_fvalue evd mv'' with + | Some (c,_) -> match_name c.rebus l + | None -> None) + | Evar ev -> + (match existential_opt_value evd ev with + | Some c -> match_name c l + | None -> None) + | _ -> None + else None in + let id = try List.find_map f (Evd.meta_list evd) with Not_found -> id in + loc,Evar_kinds.VarInstance id + | src -> src + (* [clenv_pose_metas_as_evars clenv dep_mvs] * For each dependent evar in the clause-env which does not have a value, * pose a value for it by constructing a fresh evar. We do this in @@ -306,8 +333,10 @@ let clenv_pose_metas_as_evars clenv dep_mvs = (* This assumes no cycle in the dependencies - is it correct ? *) if occur_meta ty then fold clenv (mvs@[mv]) else + let src = evar_source_of_meta mv clenv.evd in + let src = adjust_meta_source clenv.evd mv src in let (evd,evar) = - new_evar clenv.evd (cl_env clenv) ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in + new_evar clenv.evd (cl_env clenv) ~src ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 98a97a91c0..5f97e72fab 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -23,7 +23,9 @@ let depends_on_evar evk _ (pbty,_,t1,t2) = try Evar.equal (head_evar t2) evk with NoHeadEvar -> false -let define_and_solve_constraints evk c evd = +let define_and_solve_constraints evk c env evd = + if Termops.occur_evar evk c then + Pretype_errors.error_occur_check env evd evk c; let evd = define evk c evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in match @@ -55,7 +57,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) in - define_and_solve_constraints evk typed_c (evars_reset_evd sigma' sigma) + define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) (* vernac command Existential *) diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 19a1f77584..4df280e233 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -254,12 +254,12 @@ let db_mc_pattern_success debug = else return () (* Prints a failure message for an hypothesis pattern *) -let db_hyp_pattern_failure debug env (na,hyp) = +let db_hyp_pattern_failure debug env sigma (na,hyp) = is_debug debug >>= fun db -> if db then msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^ " cannot match: ") ++ - Hook.get prmatchpatt env hyp) + Hook.get prmatchpatt env sigma hyp) else return () (* Prints a matching failure message for a rule *) diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index bf85073606..864739089d 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -11,6 +11,7 @@ open Pattern open Names open Tacexpr open Term +open Evd (** This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -18,7 +19,7 @@ open Term val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t val match_pattern_printer : - (env -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t + (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t val match_rule_printer : ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t @@ -53,7 +54,7 @@ val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t (** Prints a failure message for an hypothesis pattern *) val db_hyp_pattern_failure : - debug_info -> env -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t + debug_info -> env -> evar_map -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t (** Prints a matching failure message for a rule *) val db_matching_failure : debug_info -> unit Proofview.NonLogical.t diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 65166ec115..a51c4a962c 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -285,7 +285,7 @@ let find_applied_relation metas loc env sigma c left2right = | Some c -> c | None -> user_err_loc (loc, "decompose_applied_relation", - str"The type" ++ spc () ++ Printer.pr_constr_env env ctype ++ + str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 286ae7696b..61e9347709 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -211,7 +211,7 @@ let catchable = function | Refiner.FailError _ -> true | e -> Logic.catchable_exception e -let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) +let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l) @@ -395,7 +395,7 @@ let hints_tac hints = | [] -> if not foundone && !typeclasses_debug then msg_debug (pr_depth info.auto_depth ++ str": no match for " ++ - Printer.pr_constr_env (Goal.V82.env s gl) concl ++ + Printer.pr_constr_env (Goal.V82.env s gl) s concl ++ spc () ++ int (List.length poss) ++ str" possibilities"); fk () in aux 1 false poss } diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index a98d2be0bd..33505c7fcf 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -17,7 +17,20 @@ open Locus (* The instantiate tactic *) -let instantiate_tac n (ist,rawc) ido = +let instantiate_evar evk (ist,rawc) sigma = + let evi = Evd.find sigma evk in + let filtered = Evd.evar_filtered_env evi in + let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in + let lvar = { + Pretyping.ltac_constrs = constrvars; + ltac_uconstrs = Names.Id.Map.empty; + ltac_idents = Names.Id.Map.empty; + ltac_genargs = ist.Geninterp.lfun; + } in + let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in + tclEVARS sigma' + +let instantiate_tac n c ido = Proofview.V82.tactic begin fun gl -> let sigma = gl.sigma in let evl = @@ -37,21 +50,20 @@ let instantiate_tac n (ist,rawc) ido = (match decl with (_,Some body,_) -> evar_list sigma body | _ -> error "Not a defined hypothesis.") in - if List.length evl < n then - error "Not enough uninstantiated existential variables."; - if n <= 0 then error "Incorrect existential variable index."; - let evk,_ = List.nth evl (n-1) in - let evi = Evd.find sigma evk in - let filtered = Evd.evar_filtered_env evi in - let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in - let lvar = { - Pretyping.ltac_constrs = constrvars; - ltac_uconstrs = Names.Id.Map.empty; - ltac_idents = Names.Id.Map.empty; - ltac_genargs = ist.Geninterp.lfun; - } in - let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in - tclEVARS sigma' gl + if List.length evl < n then + error "Not enough uninstantiated existential variables."; + if n <= 0 then error "Incorrect existential variable index."; + let evk,_ = List.nth evl (n-1) in + instantiate_evar evk c sigma gl + end + +let instantiate_tac_by_name id c = + Proofview.V82.tactic begin fun gl -> + let sigma = gl.sigma in + let evk = + try Evd.evar_key id sigma + with Not_found -> error "Unknown existential variable." in + instantiate_evar evk c sigma gl end let let_evar name typ = diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 51ad3861df..cf84ad1f2d 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -14,4 +14,7 @@ open Locus val instantiate_tac : int -> Tacinterp.interp_sign * Glob_term.glob_constr -> (Id.t * hyp_location_flag, unit) location -> unit Proofview.tactic +val instantiate_tac_by_name : Id.t -> + Tacinterp.interp_sign * Glob_term.glob_constr -> unit Proofview.tactic + val let_evar : Name.t -> Term.types -> unit Proofview.tactic diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index a2a8675a81..e11f4c5878 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -152,12 +152,12 @@ let intern_place ist = function ConclLocation () -> ConclLocation () | HypLocation (id,hl) -> HypLocation (Tacintern.intern_hyp ist id,hl) -let interp_place ist env = function +let interp_place ist env sigma = function ConclLocation () -> ConclLocation () - | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist env id,hl) + | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist env sigma id,hl) let interp_place ist gl p = - Tacmach.project gl , interp_place ist (Tacmach.pf_env gl) p + Tacmach.project gl , interp_place ist (Tacmach.pf_env gl) (Tacmach.project gl) p let subst_place subst pl = pl diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 4498c3197b..f701918670 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -449,12 +449,13 @@ END open Tacticals TACTIC EXTEND instantiate - [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> + [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> + [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ] +| [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> [ Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals ] | [ "instantiate" ] -> [ Proofview.V82.nf_evar_goals ] END - (**********************************************************************) (** Nijmegen "step" tactic for setoid rewriting *) @@ -628,8 +629,8 @@ let hResolve id c occ t gl = let env = Termops.clear_named_body id (pf_env gl) in let env_ids = Termops.ids_of_context env in let env_names = Termops.names_of_rel_context env in - let c_raw = Detyping.detype true env_ids env_names c in - let t_raw = Detyping.detype true env_ids env_names t in + let c_raw = Detyping.detype true env_ids env_names sigma c in + let t_raw = Detyping.detype true env_ids env_names sigma t in let rec resolve_hole t_hole = try Pretyping.understand sigma env t_hole diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 248acb8c8f..e9dace8581 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -28,9 +28,9 @@ open Tacticals.New open Tactics open Decl_kinds -let no_inductive_inconstr env constr = +let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ - pr_lconstr_env env constr ++ + pr_lconstr_env env sigma constr ++ str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++ spc () ++ str "or of the type of constructors" ++ spc () ++ str "is hidden by constant definitions.") @@ -181,7 +181,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let ind = try find_rectype env sigma i with Not_found -> - errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) + errorlabstrm "inversion_scheme" (no_inductive_inconstr env sigma i) in let (invEnv,invGoal) = compute_first_inversion_scheme env sigma ind sort dep_option @@ -261,7 +261,7 @@ let lemInv id c gls = | UserError (a,b) -> errorlabstrm "LemInv" (str "Cannot refine current goal with the lemma " ++ - pr_lconstr_env (Global.env()) c) + pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c) let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index bd58b0651b..5b24facc34 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -2004,7 +2004,7 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) let not_declared env ty rel = - Tacticals.New.tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ + Tacticals.New.tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++ str ty ++ str" relation. Maybe you need to require the Setoid library") let setoid_proof ty fn fallback = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c1df201a35..a243667a5a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -125,17 +125,17 @@ let pr_value env v = else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in match env with - | Some env -> pr_lconstr_env env c + | Some (env,sigma) -> pr_lconstr_env env sigma c | _ -> str "a term" else if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in match env with - | Some env -> pr_lconstr_env env c + | Some (env,sigma) -> pr_lconstr_env env sigma c | _ -> str "a term" else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in match env with - | Some env -> pr_lconstr_under_binders_env env c + | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c | _ -> str "a term" else str "a value of type" ++ spc () ++ pr_argument_type (genarg_tag v) @@ -279,25 +279,25 @@ let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") -let interp_ident_gen fresh ist env id = - try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some env) (dloc,id) +let interp_ident_gen fresh ist env sigma id = + try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some (env,sigma)) (dloc,id) with Not_found -> id let interp_ident = interp_ident_gen false let interp_fresh_ident = interp_ident_gen true -let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) +let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) (project gl) (* Interprets an optional identifier which must be fresh *) -let interp_fresh_name ist env = function +let interp_fresh_name ist env sigma = function | Anonymous -> Anonymous - | Name id -> Name (interp_fresh_ident ist env id) + | Name id -> Name (interp_fresh_ident ist env sigma id) -let interp_intro_pattern_var loc ist env id = - try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env) (loc,id) +let interp_intro_pattern_var loc ist env sigma id = + try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some (env,sigma)) (loc,id) with Not_found -> IntroNaming (IntroIdentifier id) -let interp_intro_pattern_naming_var loc ist env id = - try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some env) (loc,id) +let interp_intro_pattern_naming_var loc ist env sigma id = + try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some (env,sigma)) (loc,id) with Not_found -> IntroIdentifier id let interp_hint_base ist s = @@ -324,31 +324,31 @@ let interp_int_or_var_list ist l = List.flatten (List.map (interp_int_or_var_as_list ist) l) (* Interprets a bound variable (especially an existing hypothesis) *) -let interp_hyp ist env (loc,id as locid) = +let interp_hyp ist env sigma (loc,id as locid) = (* Look first in lfun for a value coercible to a variable *) - try try_interp_ltac_var (coerce_to_hyp env) ist (Some env) locid + try try_interp_ltac_var (coerce_to_hyp env) ist (Some (env,sigma)) locid with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id else Loc.raise loc (Logic.RefinerError (Logic.NoSuchHyp id)) -let interp_hyp_list_as_list ist env (loc,id as x) = +let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env (Id.Map.find id ist.lfun) - with Not_found | CannotCoerceTo _ -> [interp_hyp ist env x] + with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x] -let interp_hyp_list ist gl l = - List.flatten (List.map (interp_hyp_list_as_list ist gl) l) +let interp_hyp_list ist env sigma l = + List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l) -let interp_move_location ist gl = function - | MoveAfter id -> MoveAfter (interp_hyp ist gl id) - | MoveBefore id -> MoveBefore (interp_hyp ist gl id) +let interp_move_location ist env sigma = function + | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id) + | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id) | MoveFirst -> MoveFirst | MoveLast -> MoveLast -let interp_reference ist env = function +let interp_reference ist env sigma = function | ArgArg (_,r) -> r | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_reference env) ist (Some env) (loc, id) + try try_interp_ltac_var (coerce_to_reference env) ist (Some (env,sigma)) (loc, id) with Not_found -> try let (v, _, _) = Environ.lookup_named id env in @@ -361,7 +361,7 @@ let try_interp_evaluable env (loc, id) = | (_, Some _, _) -> EvalVarRef id | _ -> error_not_evaluable (VarRef id) -let interp_evaluable ist env = function +let interp_evaluable ist env sigma = function | ArgArg (r,Some (loc,id)) -> (* Maybe [id] has been introduced by Intro-like tactics *) begin @@ -373,7 +373,7 @@ let interp_evaluable ist env = function end | ArgArg (r,None) -> r | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) (loc, id) + try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id) with Not_found -> try try_interp_evaluable env (loc, id) with Not_found -> error_global_not_found_loc loc (qualid_of_ident id) @@ -382,11 +382,11 @@ let interp_evaluable ist env = function let interp_occurrences ist occs = Locusops.occurrences_map (interp_int_or_var_list ist) occs -let interp_hyp_location ist gl ((occs,id),hl) = - ((interp_occurrences ist occs,interp_hyp ist gl id),hl) +let interp_hyp_location ist env sigma ((occs,id),hl) = + ((interp_occurrences ist occs,interp_hyp ist env sigma id),hl) -let interp_clause ist gl { onhyps=ol; concl_occs=occs } : clause = - { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol; +let interp_clause ist env sigma { onhyps=ol; concl_occs=occs } : clause = + { onhyps=Option.map(List.map (interp_hyp_location ist env sigma)) ol; concl_occs=interp_occurrences ist occs } (* Interpretation of constructions *) @@ -430,7 +430,7 @@ let extract_ids ids lfun = let default_fresh_id = Id.of_string "H" -let interp_fresh_id ist env l = +let interp_fresh_id ist env sigma l = let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with | None -> [] @@ -443,7 +443,7 @@ let interp_fresh_id ist env l = let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> Id.to_string (interp_ident ist env id)) l) in + | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in let s = if Lexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env @@ -616,11 +616,11 @@ let pf_interp_type ist gl = interp_type ist (pf_env gl) (project gl) (* Interprets a reduction expression *) -let interp_unfold ist env (occs,qid) = - (interp_occurrences ist occs,interp_evaluable ist env qid) +let interp_unfold ist env sigma (occs,qid) = + (interp_occurrences ist occs,interp_evaluable ist env sigma qid) -let interp_flag ist env red = - { red with rConst = List.map (interp_evaluable ist env) red.rConst } +let interp_flag ist env sigma red = + { red with rConst = List.map (interp_evaluable ist env sigma) red.rConst } let interp_constr_with_occurrences ist sigma env (occs,c) = let (sigma,c_interp) = interp_constr ist sigma env c in @@ -638,16 +638,16 @@ let interp_constr_with_occurrences_and_name_as_list = (fun ist env sigma (occ_c,na) -> let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in sigma, (c_interp, - interp_fresh_name ist env na)) + interp_fresh_name ist env sigma na)) -let interp_red_expr ist sigma env = function - | Unfold l -> sigma , Unfold (List.map (interp_unfold ist env) l) +let interp_red_expr ist env sigma = function + | Unfold l -> sigma , Unfold (List.map (interp_unfold ist env sigma) l) | Fold l -> let (sigma,l_interp) = interp_constr_list ist env sigma l in sigma , Fold l_interp - | Cbv f -> sigma , Cbv (interp_flag ist env f) - | Cbn f -> sigma , Cbn (interp_flag ist env f) - | Lazy f -> sigma , Lazy (interp_flag ist env f) + | Cbv f -> sigma , Cbv (interp_flag ist env sigma f) + | Cbn f -> sigma , Cbn (interp_flag ist env sigma f) + | Lazy f -> sigma , Lazy (interp_flag ist env sigma f) | Pattern l -> let (sigma,l_interp) = Evd.MonadR.List.map_right @@ -664,7 +664,7 @@ let interp_red_expr ist sigma env = function let interp_may_eval f ist env sigma = function | ConstrEval (r,c) -> - let (sigma,redexp) = interp_red_expr ist sigma env r in + let (sigma,redexp) = interp_red_expr ist env sigma r in let (sigma,c_interp) = f ist env sigma c in sigma , (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp) | ConstrContext ((loc,s),c) -> @@ -724,11 +724,11 @@ let rec message_of_value v = Ftactic.return (str "<tactic>") else if has_type v (topwit wit_constr) then let v = out_gen (topwit wit_constr) v in - Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) v) end + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) v) end else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in Ftactic.nf_enter begin fun gl -> - Ftactic.return (pr_constr_under_binders_env (pf_env gl) c) + Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Proofview.Goal.sigma gl) c) end else if has_type v (topwit wit_unit) then Ftactic.return (str "()") @@ -736,13 +736,13 @@ let rec message_of_value v = Ftactic.return (int (out_gen (topwit wit_int) v)) else if has_type v (topwit wit_intro_pattern) then let p = out_gen (topwit wit_intro_pattern) v in - let print env c = pr_constr_env env (snd (c env Evd.empty)) in + let print env sigma c = pr_constr_env env sigma (snd (c env Evd.empty)) in Ftactic.nf_enter begin fun gl -> - Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) c) p) + Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Proofview.Goal.sigma gl) c) p) end else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) c) end + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) c) end else match Value.to_list v with | Some l -> Ftactic.List.map message_of_value l >>= fun l -> @@ -776,14 +776,14 @@ let rec interp_intro_pattern ist env sigma = function let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in sigma, (loc, IntroAction pat) | loc, IntroNaming (IntroIdentifier id) -> - sigma, (loc, interp_intro_pattern_var loc ist env id) + sigma, (loc, interp_intro_pattern_var loc ist env sigma id) | loc, IntroNaming pat -> - sigma, (loc, IntroNaming (interp_intro_pattern_naming loc ist env pat)) + sigma, (loc, IntroNaming (interp_intro_pattern_naming loc ist env sigma pat)) | loc, IntroForthcoming _ as x -> sigma, x -and interp_intro_pattern_naming loc ist env = function - | IntroFresh id -> IntroFresh (interp_fresh_ident ist env id) - | IntroIdentifier id -> interp_intro_pattern_naming_var loc ist env id +and interp_intro_pattern_naming loc ist env sigma = function + | IntroFresh id -> IntroFresh (interp_fresh_ident ist env sigma id) + | IntroIdentifier id -> interp_intro_pattern_naming_var loc ist env sigma id | (IntroWildcard | IntroAnonymous) as x -> x and interp_intro_pattern_action ist env sigma = function @@ -809,9 +809,9 @@ and interp_intro_pattern_list_as_list ist env sigma = function List.fold_map (interp_intro_pattern ist env) sigma l) | l -> List.fold_map (interp_intro_pattern ist env) sigma l -let interp_intro_pattern_naming_option ist env = function +let interp_intro_pattern_naming_option ist env sigma = function | None -> None - | Some (loc,pat) -> Some (loc, interp_intro_pattern_naming loc ist env pat) + | Some (loc,pat) -> Some (loc, interp_intro_pattern_naming loc ist env sigma pat) let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None @@ -833,7 +833,7 @@ let interp_intro_pattern_option ist env sigma = function let interp_in_hyp_as ist env sigma (clear,id,ipat) = let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in - sigma,(clear,interp_hyp ist env id,ipat) + sigma,(clear,interp_hyp ist env sigma id,ipat) let interp_quantified_hypothesis ist = function | AnonHyp n -> AnonHyp n @@ -850,11 +850,11 @@ let interp_binding_name ist = function try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id) with Not_found -> NamedHyp id -let interp_declared_or_quantified_hypothesis ist env = function +let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id) + (coerce_to_decl_or_quant_hyp env) ist (Some (env,sigma)) (dloc,id) with Not_found -> NamedHyp id let interp_binding ist env sigma (loc,b,c) = @@ -1018,7 +1018,8 @@ let mk_constr_value ist gl c = let mk_open_constr_value ist gl c = let (sigma,c_interp) = pf_apply (interp_open_constr ist) gl c in sigma, Value.of_constr c_interp -let mk_hyp_value ist gl c = Value.of_constr (mkVar (interp_hyp ist gl c)) +let mk_hyp_value ist env sigma c = + Value.of_constr (mkVar (interp_hyp ist env sigma c)) let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c) let pack_sigma (sigma,c) = {it=c;sigma=sigma;} @@ -1134,10 +1135,10 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | IntOrVarArgType -> Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)) | IdentArgType -> - Ftactic.return (value_of_ident (interp_fresh_ident ist env + Ftactic.return (value_of_ident (interp_fresh_ident ist env sigma (out_gen (glbwit wit_ident) x))) | VarArgType -> - Ftactic.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x)) + Ftactic.return (mk_hyp_value ist env sigma (out_gen (glbwit wit_var) x)) | GenArgType -> f (out_gen (glbwit wit_genarg) x) | ConstrArgType -> let (sigma,v) = @@ -1166,7 +1167,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | ListArgType VarArgType -> let wit = glbwit (wit_list wit_var) in Ftactic.return ( - let ans = List.map (mk_hyp_value ist env) (out_gen wit x) in + let ans = List.map (mk_hyp_value ist env sigma) (out_gen wit x) in in_gen (topwit (wit_list wit_genarg)) ans ) | ListArgType IntOrVarArgType -> @@ -1175,7 +1176,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) | ListArgType IdentArgType -> let wit = glbwit (wit_list wit_ident) in - let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in + let mk_ident x = value_of_ident (interp_fresh_ident ist env sigma x) in let ans = List.map mk_ident (out_gen wit x) in Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) | ListArgType t -> @@ -1307,7 +1308,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = interp_app loc ist fv largs | TacFreshId l -> Ftactic.enter begin fun gl -> - let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in + let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) l in Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) end | TacPretype c -> @@ -1525,9 +1526,9 @@ and interp_genarg ist env sigma concl gl x = (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x))) | IdentArgType -> in_gen (topwit wit_ident) - (interp_fresh_ident ist env (out_gen (glbwit wit_ident) x)) + (interp_fresh_ident ist env sigma (out_gen (glbwit wit_ident) x)) | VarArgType -> - in_gen (topwit wit_var) (interp_hyp ist env (out_gen (glbwit wit_var) x)) + in_gen (topwit wit_var) (interp_hyp ist env sigma (out_gen (glbwit wit_var) x)) | GenArgType -> in_gen (topwit wit_genarg) (interp_genarg (out_gen (glbwit wit_genarg) x)) | ConstrArgType -> @@ -1542,11 +1543,11 @@ and interp_genarg ist env sigma concl gl x = in_gen (topwit wit_constr_may_eval) c_interp | QuantHypArgType -> in_gen (topwit wit_quant_hyp) - (interp_declared_or_quantified_hypothesis ist env + (interp_declared_or_quantified_hypothesis ist env sigma (out_gen (glbwit wit_quant_hyp) x)) | RedExprArgType -> let (sigma,r_interp) = - interp_red_expr ist !evdref env (out_gen (glbwit wit_red_expr) x) + interp_red_expr ist env !evdref (out_gen (glbwit wit_red_expr) x) in evdref := sigma; in_gen (topwit wit_red_expr) r_interp @@ -1567,7 +1568,7 @@ and interp_genarg ist env sigma concl gl x = let (sigma,v) = interp_genarg_constr_list ist env !evdref x in evdref := sigma; v - | ListArgType VarArgType -> interp_genarg_var_list ist env x + | ListArgType VarArgType -> interp_genarg_var_list ist env sigma x | ListArgType _ -> let list_unpacker wit l = let map x = @@ -1618,9 +1619,9 @@ and interp_genarg_constr_list ist env sigma x = let (sigma,lc) = interp_constr_list ist env sigma lc in sigma , in_gen (topwit (wit_list wit_constr)) lc -and interp_genarg_var_list ist env x = +and interp_genarg_var_list ist env sigma x = let lc = out_gen (glbwit (wit_list wit_var)) x in - let lc = interp_hyp_list ist env lc in + let lc = interp_hyp_list ist env sigma lc in in_gen (topwit (wit_list wit_var)) lc (* Interprets tactic expressions : returns a "constr" *) @@ -1644,6 +1645,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = end >>= fun result -> Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in @@ -1651,7 +1653,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = debugging_step ist (fun () -> Pptactic.pr_glob_tactic env e ++ fnl() ++ str " has value " ++ fnl() ++ - pr_constr_env env cresult) + pr_constr_env env sigma cresult) end <*> Ftactic.return cresult with CannotCoerceTo _ -> @@ -1681,8 +1683,9 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacIntroMove (ido,hto) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let mloc = interp_move_location ist env hto in - Tactics.intro_move (Option.map (interp_fresh_ident ist env) ido) mloc + let sigma = Proofview.Goal.sigma gl in + let mloc = interp_move_location ist env sigma hto in + Tactics.intro_move (Option.map (interp_fresh_ident ist env sigma) ido) mloc end | TacExact c -> Proofview.V82.tactic begin fun gl -> @@ -1724,39 +1727,41 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacFix (idopt,n) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - Proofview.V82.tactic (Tactics.fix (Option.map (interp_fresh_ident ist env) idopt) n) + let sigma = Proofview.Goal.sigma gl in + Proofview.V82.tactic (Tactics.fix (Option.map (interp_fresh_ident ist env sigma) idopt) n) end | TacMutualFix (id,n,l) -> Proofview.V82.tactic begin fun gl -> let env = pf_env gl in let f sigma (id,n,c) = let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in - sigma , (interp_fresh_ident ist env id,n,c_interp) in + sigma , (interp_fresh_ident ist env sigma id,n,c_interp) in let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in tclTHEN (tclEVARS sigma) - (Tactics.mutual_fix (interp_fresh_ident ist env id) n l_interp 0) + (Tactics.mutual_fix (interp_fresh_ident ist env sigma id) n l_interp 0) gl end | TacCofix idopt -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - Proofview.V82.tactic (Tactics.cofix (Option.map (interp_fresh_ident ist env) idopt)) + let sigma = Proofview.Goal.sigma gl in + Proofview.V82.tactic (Tactics.cofix (Option.map (interp_fresh_ident ist env sigma) idopt)) end | TacMutualCofix (id,l) -> Proofview.V82.tactic begin fun gl -> let env = pf_env gl in let f sigma (id,c) = let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in - sigma , (interp_fresh_ident ist env id,c_interp) in + sigma , (interp_fresh_ident ist env sigma id,c_interp) in let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in tclTHEN (tclEVARS sigma) - (Tactics.mutual_cofix (interp_fresh_ident ist env id) l_interp 0) + (Tactics.mutual_cofix (interp_fresh_ident ist env sigma id) l_interp 0) gl end | TacAssert (b,t,ipat,c) -> @@ -1786,8 +1791,8 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let clp = interp_clause ist env clp in - let eqpat = interp_intro_pattern_naming_option ist env eqpat in + let clp = interp_clause ist env sigma clp in + let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in if Locusops.is_nowhere clp then (* We try to fully-typecheck the term *) let (sigma,c_interp) = @@ -1799,7 +1804,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Tactics.letin_tac with_eq na c None cl in Proofview.V82.tclEVARS sigma <*> - let_tac b (interp_fresh_name ist env na) c_interp clp eqpat + let_tac b (interp_fresh_name ist env sigma na) c_interp clp eqpat else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = @@ -1807,8 +1812,9 @@ and interp_atomic ist tac : unit Proofview.tactic = let with_eq = if b then None else Some (true,id) in Tactics.letin_pat_tac with_eq na c cl in - let_pat_tac b (interp_fresh_name ist env na) - (interp_pure_open_constr ist env sigma c) clp eqpat + Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) + (let_pat_tac b (interp_fresh_name ist env sigma na) + (interp_pure_open_constr ist env sigma c) clp) sigma eqpat end (* Automation tactics *) @@ -1841,14 +1847,14 @@ and interp_atomic ist tac : unit Proofview.tactic = List.fold_map begin fun sigma (c,(ipato,ipats)) -> (* TODO: move sigma as a side-effect *) let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in - let ipato = interp_intro_pattern_naming_option ist env ipato in + let ipato = interp_intro_pattern_naming_option ist env sigma ipato in let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in sigma,(c,(ipato,ipats)) end sigma l in let sigma,el = Option.fold_map (interp_constr_with_bindings ist env) sigma el in - let interp_clause = interp_clause ist env in + let interp_clause = interp_clause ist env sigma in let cls = Option.map interp_clause cls in Tacticals.New.tclWITHHOLES ev (Tactics.induction_destruct isrec ev) sigma (l,el,cls) end @@ -1859,25 +1865,26 @@ and interp_atomic ist tac : unit Proofview.tactic = (* Context management *) | TacClear (b,l) -> Proofview.V82.tactic begin fun gl -> - let l = interp_hyp_list ist (pf_env gl) l in + let l = interp_hyp_list ist (pf_env gl) (project gl) l in if b then Tactics.keep l gl else Tactics.clear l gl end | TacClearBody l -> Proofview.Goal.enter begin fun gl -> - Tactics.clear_body (interp_hyp_list ist (Tacmach.New.pf_env gl) l) + Tactics.clear_body (interp_hyp_list ist (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) l) end | TacMove (dep,id1,id2) -> Proofview.V82.tactic begin fun gl -> - Tactics.move_hyp dep (interp_hyp ist (pf_env gl) id1) - (interp_move_location ist (pf_env gl) id2) + Tactics.move_hyp dep (interp_hyp ist (pf_env gl) (project gl) id1) + (interp_move_location ist (pf_env gl) (project gl) id2) gl end | TacRename l -> Proofview.V82.tactic begin fun gl -> let env = pf_env gl in + let sigma = project gl in Tactics.rename_hyp (List.map (fun (id1,id2) -> - interp_hyp ist env id1, - interp_fresh_ident ist env (snd id2)) l) + interp_hyp ist env sigma id1, + interp_fresh_ident ist env sigma (snd id2)) l) gl end @@ -1892,10 +1899,10 @@ and interp_atomic ist tac : unit Proofview.tactic = (* Conversion *) | TacReduce (r,cl) -> Proofview.V82.tactic begin fun gl -> - let (sigma,r_interp) = interp_red_expr ist (project gl) (pf_env gl) r in + let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in tclTHEN (tclEVARS sigma) - (Tactics.reduce r_interp (interp_clause ist (pf_env gl) cl)) + (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) gl end | TacChange (None,c,cl) -> @@ -1914,7 +1921,7 @@ and interp_atomic ist tac : unit Proofview.tactic = then interp_type ist env sigma c else interp_constr ist env sigma c in - (Tactics.change None c_interp (interp_clause ist (pf_env gl) cl)) + (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)) gl end | TacChange (Some op,c,cl) -> @@ -1931,7 +1938,7 @@ and interp_atomic ist tac : unit Proofview.tactic = with e when to_catch e (* Hack *) -> errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") in - (Tactics.change (Some op) c_interp (interp_clause ist env cl)) + (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) gl end end @@ -1940,7 +1947,8 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacSymmetry c -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let cl = interp_clause ist env c in + let sigma = Proofview.Goal.sigma gl in + let cl = interp_clause ist env sigma c in Tactics.intros_symmetry cl end @@ -1951,7 +1959,8 @@ and interp_atomic ist tac : unit Proofview.tactic = let f env sigma = interp_open_constr_with_bindings ist env sigma c in (b,m,keep,f)) l in let env = Proofview.Goal.env gl in - let cl = interp_clause ist env cl in + let sigma = Proofview.Goal.sigma gl in + let cl = interp_clause ist env sigma cl in Equality.general_multi_rewrite ev l cl (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) @@ -1970,7 +1979,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in sigma , Some c_interp in - let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in + let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma,ids = interp_or_and_intro_pattern_option ist env sigma ids in Proofview.V82.tclEVARS sigma <*> Inv.dinv k c_interp ids dqhyps end @@ -1978,8 +1987,8 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let hyps = interp_hyp_list ist env idl in - let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in + let hyps = interp_hyp_list ist env sigma idl in + let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma, ids = interp_or_and_intro_pattern_option ist env sigma ids in Proofview.V82.tclEVARS sigma <*> Inv.inv_clause k ids hyps dqhyps end @@ -1988,8 +1997,8 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (sigma,c_interp) = interp_constr ist env sigma c in - let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in - let hyps = interp_hyp_list ist env idl in + let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in + let hyps = interp_hyp_list ist env sigma idl in Proofview.V82.tclEVARS sigma <*> Leminv.lemInv_clause dqhyps c_interp @@ -2078,11 +2087,11 @@ let () = declare_uniform wit_pre_ident let () = - let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) ref) in + let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) (project gl) ref) in Geninterp.register_interp0 wit_ref interp; let interp ist gl pat = interp_intro_pattern ist (pf_env gl) (project gl) pat in Geninterp.register_interp0 wit_intro_pattern interp; - let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) pat) in + let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) (project gl) pat) in Geninterp.register_interp0 wit_clause_dft_concl interp; let interp ist gl s = interp_sort (project gl) s in Geninterp.register_interp0 wit_sort interp @@ -2109,7 +2118,7 @@ let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k let interp_redexp env sigma r = let ist = default_ist () in let gist = { fully_empty_glob_sign with genv = env; } in - interp_red_expr ist sigma env (intern_red_expr gist r) + interp_red_expr ist env sigma (intern_red_expr gist r) (***************************************************************************) (* Embed tactics in raw or glob tactic expr *) @@ -2164,13 +2173,14 @@ let dummy_id = Id.of_string "_" let lift_constr_tac_to_ml_tac vars tac = let tac _ ist = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let map = function | None -> None | Some id -> let c = Id.Map.find id ist.lfun in try Some (coerce_to_closed_constr env c) with CannotCoerceTo ty -> - error_ltac_variable Loc.ghost dummy_id (Some env) c ty + error_ltac_variable Loc.ghost dummy_id (Some (env,sigma)) c ty in let args = List.map_filter map vars in tac args ist diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 54e604fe47..3524b00c60 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -77,7 +77,8 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map (** Interprets tactic expressions *) -val interp_hyp : interp_sign -> Environ.env -> Id.t Loc.located -> Id.t +val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> + Id.t Loc.located -> Id.t val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr bindings -> Evd.evar_map * constr bindings @@ -105,13 +106,15 @@ val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> uni (** Internals that can be useful for syntax extensions. *) -val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> Id.t Loc.located -> 'a +val interp_ltac_var : (value -> 'a) -> interp_sign -> + (Environ.env * Evd.evar_map) option -> Id.t Loc.located -> 'a val interp_int : interp_sign -> Id.t Loc.located -> int val interp_int_or_var : interp_sign -> int or_var -> int -val error_ltac_variable : Loc.t -> Id.t -> Environ.env option -> value -> string -> 'a +val error_ltac_variable : Loc.t -> Id.t -> + (Environ.env * Evd.evar_map) option -> value -> string -> 'a (** Transforms a constr-expecting tactic into a tactic finding its arguments in the Ltac environment according to the given names. *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3a14f4da72..d24645968a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -152,7 +152,7 @@ end let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y -let clear_dependency_msg env id = function +let clear_dependency_msg env sigma id = function | Evarutil.OccurHypInSimpleClause None -> pr_id id ++ str " is used in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> @@ -160,12 +160,12 @@ let clear_dependency_msg env id = function | Evarutil.EvarTypingBreak ev -> str "Cannot remove " ++ pr_id id ++ strbrk " without breaking the typing of " ++ - Printer.pr_existential env ev ++ str"." + Printer.pr_existential env sigma ev ++ str"." -let error_clear_dependency env id err = - errorlabstrm "" (clear_dependency_msg env id err) +let error_clear_dependency env sigma id err = + errorlabstrm "" (clear_dependency_msg env sigma id err) -let replacing_dependency_msg env id = function +let replacing_dependency_msg env sigma id = function | Evarutil.OccurHypInSimpleClause None -> str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> @@ -174,20 +174,20 @@ let replacing_dependency_msg env id = function | Evarutil.EvarTypingBreak ev -> str "Cannot change " ++ pr_id id ++ strbrk " without breaking the typing of " ++ - Printer.pr_existential env ev ++ str"." + Printer.pr_existential env sigma ev ++ str"." -let error_replacing_dependency env id err = - errorlabstrm "" (replacing_dependency_msg env id err) +let error_replacing_dependency env sigma id err = + errorlabstrm "" (replacing_dependency_msg env sigma id err) let thin l gl = try thin l gl with Evarutil.ClearDependencyError (id,err) -> - error_clear_dependency (pf_env gl) id err + error_clear_dependency (pf_env gl) (project gl) id err let thin_for_replacing l gl = try Tacmach.thin l gl with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) id err + error_replacing_dependency (pf_env gl) (project gl) id err let apply_clear_request clear_flag dft c = let check_isvar c = @@ -271,7 +271,7 @@ let assert_before_then_gen b naming t tac = (fun gl -> try internal_cut b id t gl with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) id err)) + error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) end @@ -289,7 +289,7 @@ let assert_after_then_gen b naming t tac = (fun gl -> try internal_cut_rev b id t gl with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) id err)) + error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) end @@ -1563,7 +1563,7 @@ let clear_wildcards ids = with ClearDependencyError (id,err) -> (* Intercept standard [thin] error message *) Loc.raise loc - (error_clear_dependency (pf_env gl) (Id.of_string "_") err)) + (error_clear_dependency (pf_env gl) (project gl) (Id.of_string "_") err)) ids) (* Takes a list of booleans, and introduces all the variables diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 4cf8f4145a..ae1179597b 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -79,8 +79,8 @@ let process_vernac_interp_error exn = match exn with wrap_vernac_error exn (Himsg.explain_module_internalization_error e) | RecursionSchemeError e -> wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e) - | Cases.PatternMatchingError (env,e) -> - wrap_vernac_error exn (Himsg.explain_pattern_matching_error env e) + | Cases.PatternMatchingError (env,sigma,e) -> + wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 115c245f38..df07026f6f 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -845,7 +845,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let error () = user_err_loc (constr_loc r, "Command.build_wellfounded", - Printer.pr_constr_env env rel ++ str " is not an homogeneous binary relation.") + Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") in try let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e7be7b4790..5f7a7c3530 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -70,8 +70,8 @@ let contract3' env a b c = function (** Printers *) let pr_lconstr c = quote (pr_lconstr c) -let pr_lconstr_env e c = quote (pr_lconstr_env e c) -let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) +let pr_lconstr_env e s c = quote (pr_lconstr_env e s c) +let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t) (** A canonisation procedure for constr such that comparing there externalisation catches more equalities *) @@ -90,31 +90,31 @@ let canonize_constr c = canonize_binders c (** Tries to realize when the two terms, albeit different are printed the same. *) -let display_eq ~flags env t1 t2 = +let display_eq ~flags env sigma t1 t2 = (* terms are canonized, then their externalisation is compared syntactically *) let open Constrextern in let t1 = canonize_constr t1 in let t2 = canonize_constr t2 in - let ct1 = Flags.with_options flags (fun () -> extern_constr false env t1) () in - let ct2 = Flags.with_options flags (fun () -> extern_constr false env t2) () in + let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in + let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in Constrexpr_ops.constr_expr_eq ct1 ct2 (** This function adds some explicit printing flags if the two arguments are printed alike. *) -let rec pr_explicit_aux env t1 t2 = function +let rec pr_explicit_aux env sigma t1 t2 = function | [] -> (** no specified flags: default. *) - (quote (Printer.pr_lconstr_env env t1), quote (Printer.pr_lconstr_env env t2)) + (quote (Printer.pr_lconstr_env env sigma t1), quote (Printer.pr_lconstr_env env sigma t2)) | flags :: rem -> - let equal = display_eq ~flags env t1 t2 in + let equal = display_eq ~flags env sigma t1 t2 in if equal then (** The two terms are the same from the user point of view *) - pr_explicit_aux env t1 t2 rem + pr_explicit_aux env sigma t1 t2 rem else let open Constrextern in - let ct1 = Flags.with_options flags (fun () -> extern_constr false env t1) () + let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in - let ct2 = Flags.with_options flags (fun () -> extern_constr false env t2) () + let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in quote (Ppconstr.pr_lconstr_expr ct1), quote (Ppconstr.pr_lconstr_expr ct2) @@ -127,7 +127,7 @@ let explicit_flags = [print_implicits; print_coercions; print_no_symbol]; (** Then more! *) [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ] -let pr_explicit env t1 t2 = pr_explicit_aux env t1 t2 explicit_flags +let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags let pr_db env i = try @@ -136,8 +136,8 @@ let pr_db env i = | Anonymous, _, _ -> str "<>" with Not_found -> str "UNBOUND_REL_" ++ int i -let explain_unbound_rel env n = - let pe = pr_ne_context_of (str "In environment") env in +let explain_unbound_rel env sigma n = + let pe = pr_ne_context_of (str "In environment") env sigma in str "Unbound reference: " ++ pe ++ str "The reference " ++ int n ++ str " is free." @@ -147,15 +147,15 @@ let explain_unbound_var env v = let explain_not_type env sigma j = let j = Evarutil.j_nf_evar sigma j in - let pe = pr_ne_context_of (str "In environment") env in - let pc,pt = pr_ljudge_env env j in + let pe = pr_ne_context_of (str "In environment") env sigma in + let pc,pt = pr_ljudge_env env sigma j in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ str "has type" ++ spc () ++ pt ++ spc () ++ str "which should be Set, Prop or Type." -let explain_bad_assumption env j = - let pe = pr_ne_context_of (str "In environment") env in - let pc,pt = pr_ljudge_env env j in +let explain_bad_assumption env sigma j = + let pe = pr_ne_context_of (str "In environment") env sigma in + let pc,pt = pr_ljudge_env env sigma j in pe ++ str "Cannot declare a variable or hypothesis over the term" ++ brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++ str "because this term is not a type." @@ -178,10 +178,10 @@ let pr_puniverses f env (c,u) = str"(*" ++ Univ.Instance.pr u ++ str"*)" else mt()) -let explain_elim_arity env ind sorts c pj okinds = +let explain_elim_arity env sigma ind sorts c pj okinds = let env = make_all_name_different env in let pi = pr_inductive env (fst ind) in - let pc = pr_lconstr_env env c in + let pc = pr_lconstr_env env sigma c in let msg = match okinds with | Some(kp,ki,explanation) -> let pki = pr_sort_family ki in @@ -194,7 +194,7 @@ let explain_elim_arity env ind sorts c pj okinds = | WrongArity -> "wrong arity" in let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in - let ppt = pr_lconstr_env env ((strip_prod_assum pj.uj_type)) in + let ppt = pr_lconstr_env env sigma ((strip_prod_assum pj.uj_type)) in hov 0 (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++ str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++ @@ -215,8 +215,8 @@ let explain_elim_arity env ind sorts c pj okinds = let explain_case_not_inductive env sigma cj = let cj = Evarutil.j_nf_evar sigma cj in let env = make_all_name_different env in - let pc = pr_lconstr_env env cj.uj_val in - let pct = pr_lconstr_env env cj.uj_type in + let pc = pr_lconstr_env env sigma cj.uj_val in + let pct = pr_lconstr_env env sigma cj.uj_type in match kind_of_term cj.uj_type with | Evar _ -> str "Cannot infer a type for this expression." @@ -228,8 +228,8 @@ let explain_case_not_inductive env sigma cj = let explain_number_branches env sigma cj expn = let cj = Evarutil.j_nf_evar sigma cj in let env = make_all_name_different env in - let pc = pr_lconstr_env env cj.uj_val in - let pct = pr_lconstr_env env cj.uj_type in + let pc = pr_lconstr_env env sigma cj.uj_val in + let pct = pr_lconstr_env env sigma cj.uj_type in str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ str "of type" ++ brk(1,1) ++ pct ++ spc () ++ str "expects " ++ int expn ++ str " branches." @@ -238,18 +238,18 @@ let explain_ill_formed_branch env sigma c ci actty expty = let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in let c = Evarutil.nf_evar sigma c in let env = make_all_name_different env in - let pc = pr_lconstr_env env c in - let pa, pe = pr_explicit env (simp actty) (simp expty) in + let pc = pr_lconstr_env env sigma c in + let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ spc () ++ strbrk "the branch for constructor" ++ spc () ++ quote (pr_puniverses pr_constructor env ci) ++ spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe ++ str "." -let explain_generalization env (name,var) j = - let pe = pr_ne_context_of (str "In environment") env in - let pv = pr_ltype_env env var in - let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) j in +let explain_generalization env sigma (name,var) j = + let pe = pr_ne_context_of (str "In environment") env sigma in + let pv = pr_ltype_env env sigma var in + let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++ str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++ str "it has type" ++ spc () ++ pt ++ @@ -261,18 +261,18 @@ let explain_unification_error env sigma p1 p2 = function match e with | OccurCheck (evk,rhs) -> let rhs = Evarutil.nf_evar sigma rhs in - spc () ++ str "(cannot define " ++ quote (pr_existential_key evk) ++ - strbrk " with term " ++ pr_lconstr_env env rhs ++ + spc () ++ str "(cannot define " ++ quote (pr_existential_key sigma evk) ++ + strbrk " with term " ++ pr_lconstr_env env sigma rhs ++ strbrk " that would depend on itself)" | NotClean ((evk,args),c) -> let c = Evarutil.nf_evar sigma c in let args = Array.map (Evarutil.nf_evar sigma) args in - spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key evk) - ++ strbrk " because " ++ pr_lconstr_env env c ++ + spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key sigma evk) + ++ strbrk " because " ++ pr_lconstr_env env sigma c ++ strbrk " is not in its scope" ++ (if Array.is_empty args then mt() else strbrk ": available arguments are " ++ - pr_sequence (pr_lconstr_env env) (List.rev (Array.to_list args))) ++ + pr_sequence (pr_lconstr_env env sigma) (List.rev (Array.to_list args))) ++ str ")" | NotSameArgSize | NotSameHead | NoCanonicalStructure -> (* Error speaks from itself *) mt () @@ -282,17 +282,17 @@ let explain_unification_error env sigma p1 p2 = function let t1 = Evarutil.nf_evar sigma t1 in let t2 = Evarutil.nf_evar sigma t2 in if not (eq_constr t1 p1) || not (eq_constr t2 p2) then - let t1, t2 = pr_explicit env t1 t2 in + let t1, t2 = pr_explicit env sigma t1 t2 in spc () ++ str "(cannot unify " ++ t1 ++ strbrk " and " ++ t2 ++ str ")" else mt () | MetaOccurInBody evk -> - spc () ++ str "(instance for " ++ quote (pr_existential_key evk) ++ + spc () ++ str "(instance for " ++ quote (pr_existential_key sigma evk) ++ strbrk " refers to a metavariable - please report your example)" | InstanceNotSameType (evk,env,t,u) -> - let t, u = pr_explicit env t u in + let t, u = pr_explicit env sigma t u in spc () ++ str "(unable to find a well-typed instantiation for " ++ - quote (pr_existential_key evk) ++ strbrk ": cannot unify " ++ + quote (pr_existential_key sigma evk) ++ strbrk ": cannot unify " ++ t ++ strbrk " and " ++ u ++ str ")" | UnifUnivInconsistency p -> if !Constrextern.print_universes then @@ -306,9 +306,9 @@ let explain_actual_type env sigma j t reason = let j = Evarutil.j_nf_betaiotaevar sigma j in let t = Reductionops.nf_betaiota sigma t in (** Actually print *) - let pe = pr_ne_context_of (str "In environment") env in - let pc = pr_lconstr_env env (Environ.j_val j) in - let (pt, pct) = pr_explicit env t (Environ.j_type j) in + let pe = pr_ne_context_of (str "In environment") env sigma in + let pc = pr_lconstr_env env sigma (Environ.j_val j) in + let (pt, pct) = pr_explicit env sigma t (Environ.j_type j) in let ppreason = explain_unification_error env sigma j.uj_type t reason in pe ++ hov 0 ( @@ -323,17 +323,17 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let actualtyp = Reductionops.nf_betaiota sigma actualtyp in let rator = Evarutil.j_nf_evar sigma rator in let env = make_all_name_different env in - let actualtyp, exptyp = pr_explicit env actualtyp exptyp in + let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in let nargs = Array.length randl in -(* let pe = pr_ne_context_of (str "in environment") env in*) - let pr,prt = pr_ljudge_env env rator in +(* let pe = pr_ne_context_of (str "in environment") env sigma in*) + let pr,prt = pr_ljudge_env env sigma rator in let term_string1 = str (String.plural nargs "term") in let term_string2 = if nargs>1 then str "The " ++ pr_nth n ++ str " term" else str "This term" in let appl = prvect_with_sep fnl (fun c -> - let pc,pct = pr_ljudge_env env c in + let pc,pct = pr_ljudge_env env sigma c in hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl in str "Illegal application: " ++ (* pe ++ *) fnl () ++ @@ -350,13 +350,13 @@ let explain_cant_apply_not_functional env sigma rator randl = let rator = Evarutil.j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in -(* let pe = pr_ne_context_of (str "in environment") env in*) - let pr = pr_lconstr_env env rator.uj_val in - let prt = pr_lconstr_env env rator.uj_type in +(* let pe = pr_ne_context_of (str "in environment") env sigma in*) + let pr = pr_lconstr_env env sigma rator.uj_val in + let prt = pr_lconstr_env env sigma rator.uj_type in let appl = prvect_with_sep fnl (fun c -> - let pc = pr_lconstr_env env c.uj_val in - let pct = pr_lconstr_env env c.uj_type in + let pc = pr_lconstr_env env sigma c.uj_val in + let pct = pr_lconstr_env env sigma c.uj_type in hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl in str "Illegal application (Non-functional construction): " ++ @@ -369,20 +369,20 @@ let explain_cant_apply_not_functional env sigma rator randl = let explain_unexpected_type env sigma actual_type expected_type = let actual_type = Evarutil.nf_evar sigma actual_type in let expected_type = Evarutil.nf_evar sigma expected_type in - let pract, prexp = pr_explicit env actual_type expected_type in + let pract, prexp = pr_explicit env sigma actual_type expected_type in str "Found type" ++ spc () ++ pract ++ spc () ++ str "where" ++ spc () ++ prexp ++ str " was expected." let explain_not_product env sigma c = let c = Evarutil.nf_evar sigma c in - let pr = pr_lconstr_env env c in + let pr = pr_lconstr_env env sigma c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ (if is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) -let explain_ill_formed_rec_body env err names i fixenv vdefj = +let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = let prt_name i = match names.(i) with Name id -> str "Recursive definition of " ++ pr_id id @@ -394,7 +394,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = | NotEnoughAbstractionInFixBody -> str "Not enough abstractions in the definition" | RecursionNotOnInductiveType c -> - str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ + str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ str "which should be an inductive type" | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> let arg_env = make_all_name_different arg_env in @@ -415,7 +415,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = pr_sequence pr_db lt in str "Recursive call to " ++ called ++ spc () ++ strbrk "has principal argument equal to" ++ spc () ++ - pr_lconstr_env arg_env arg ++ strbrk " instead of " ++ vars + pr_lconstr_env arg_env sigma arg ++ strbrk " instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = @@ -426,45 +426,45 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = (* CoFixpoint guard errors *) | CodomainNotInductiveType c -> - str "The codomain is" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ + str "The codomain is" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ str "which should be a coinductive type" | NestedRecursiveOccurrences -> str "Nested recursive occurrences" | UnguardedRecursiveCall c -> - str "Unguarded recursive call in" ++ spc () ++ pr_lconstr_env env c + str "Unguarded recursive call in" ++ spc () ++ pr_lconstr_env env sigma c | RecCallInTypeOfAbstraction c -> str "Recursive call forbidden in the domain of an abstraction:" ++ - spc () ++ pr_lconstr_env env c + spc () ++ pr_lconstr_env env sigma c | RecCallInNonRecArgOfConstructor c -> str "Recursive call on a non-recursive argument of constructor" ++ - spc () ++ pr_lconstr_env env c + spc () ++ pr_lconstr_env env sigma c | RecCallInTypeOfDef c -> str "Recursive call forbidden in the type of a recursive definition" ++ - spc () ++ pr_lconstr_env env c + spc () ++ pr_lconstr_env env sigma c | RecCallInCaseFun c -> str "Invalid recursive call in a branch of" ++ - spc () ++ pr_lconstr_env env c + spc () ++ pr_lconstr_env env sigma c | RecCallInCaseArg c -> str "Invalid recursive call in the argument of \"match\" in" ++ spc () ++ - pr_lconstr_env env c + pr_lconstr_env env sigma c | RecCallInCasePred c -> str "Invalid recursive call in the \"return\" clause of \"match\" in" ++ - spc () ++ pr_lconstr_env env c + spc () ++ pr_lconstr_env env sigma c | NotGuardedForm c -> - str "Sub-expression " ++ pr_lconstr_env env c ++ + str "Sub-expression " ++ pr_lconstr_env env sigma c ++ strbrk " not in guarded form (should be a constructor," ++ strbrk " an abstraction, a match, a cofix or a recursive call)" | ReturnPredicateNotCoInductive c -> str "The return clause of the following pattern matching should be" ++ strbrk " a coinductive type:" ++ - spc () ++ pr_lconstr_env env c + spc () ++ pr_lconstr_env env sigma c in prt_name i ++ str " is ill-formed." ++ fnl () ++ - pr_ne_context_of (str "In environment") env ++ + pr_ne_context_of (str "In environment") env sigma ++ st ++ str "." ++ fnl () ++ (try (* May fail with unresolved globals. *) let fixenv = make_all_name_different fixenv in - let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in + let pvd = pr_lconstr_env fixenv sigma vdefj.(i).uj_val in str"Recursive definition is:" ++ spc () ++ pvd ++ str "." with e when Errors.noncritical e -> mt ()) @@ -472,8 +472,8 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs = let vdefj = Evarutil.jv_nf_evar sigma vdefj in let vargs = Array.map (Evarutil.nf_evar sigma) vargs in let env = make_all_name_different env in - let pvd = pr_lconstr_env env vdefj.(i).uj_val in - let pvdt, pv = pr_explicit env vdefj.(i).uj_type vargs.(i) in + let pvd = pr_lconstr_env env sigma vdefj.(i).uj_val in + let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in str "The " ++ (match vdefj with [|_|] -> mt () | _ -> pr_nth (i+1) ++ spc ()) ++ str "recursive definition" ++ spc () ++ pvd ++ spc () ++ @@ -483,24 +483,23 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs = let explain_cant_find_case_type env sigma c = let c = Evarutil.nf_evar sigma c in let env = make_all_name_different env in - let pe = pr_lconstr_env env c in + let pe = pr_lconstr_env env sigma c in str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." let explain_occur_check env sigma ev rhs = let rhs = Evarutil.nf_evar sigma rhs in let env = make_all_name_different env in - let id = Evd.string_of_existential ev in - let pt = pr_lconstr_env env rhs in - str "Cannot define " ++ str id ++ str " with term" ++ brk(1,1) ++ - pt ++ spc () ++ str "that would depend on itself." + let pt = pr_lconstr_env env sigma rhs in + str "Cannot define " ++ pr_existential_key sigma ev ++ str " with term" ++ + brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself." -let pr_ne_context_of header footer env = +let pr_ne_context_of header footer env sigma = if List.is_empty (Environ.rel_context env) && List.is_empty (Environ.named_context env) then footer - else pr_ne_context_of header env + else pr_ne_context_of header env sigma -let explain_evar_kind env evi = function +let explain_evar_kind env sigma evi = function | Evar_kinds.QuestionMark _ -> str "this placeholder" | Evar_kinds.CasesType -> str "the type of this pattern-matching problem" @@ -517,8 +516,8 @@ let explain_evar_kind env evi = function str "an internal placeholder" ++ Option.cata (fun evi -> let env = Evd.evar_filtered_env evi in - str " of type " ++ pr_lconstr_env env evi.evar_concl ++ - pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env) + str " of type " ++ pr_lconstr_env env sigma evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env sigma) (mt ()) evi | Evar_kinds.TomatchTypeParameter (tyi,n) -> str "the " ++ pr_nth n ++ @@ -538,19 +537,19 @@ let explain_unsolvability = function | Some (SeveralInstancesFound n) -> strbrk " (several distinct possible instances found)" -let explain_typeclass_resolution env evi k = +let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr evi.evar_concl with | Some c -> let env = Evd.evar_filtered_env evi in fnl () ++ str "Could not find an instance for " ++ - pr_lconstr_env env evi.evar_concl ++ - pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env + pr_lconstr_env env sigma evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env sigma | _ -> mt() -let explain_unsolvable_implicit env evi k explain = - str "Cannot infer " ++ explain_evar_kind env (Some evi) k ++ +let explain_unsolvable_implicit env sigma evi k explain = + str "Cannot infer " ++ explain_evar_kind env sigma (Some evi) k ++ explain_unsolvability explain ++ str "." ++ - explain_typeclass_resolution env evi k + explain_typeclass_resolution env sigma evi k let explain_var_not_found env id = str "The variable" ++ spc () ++ pr_id id ++ @@ -572,61 +571,61 @@ let explain_cannot_unify env sigma m n e = let env = make_all_name_different env in let m = Evarutil.nf_evar sigma m in let n = Evarutil.nf_evar sigma n in - let pm, pn = pr_explicit env m n in + let pm, pn = pr_explicit env sigma m n in let ppreason = explain_unification_error env sigma m n e in - let pe = pr_ne_context_of (str "In environment") (mt ()) env in + let pe = pr_ne_context_of (str "In environment") (mt ()) env sigma in pe ++ str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++ str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "." let explain_cannot_unify_local env sigma m n subn = - let pm = pr_lconstr_env env m in - let pn = pr_lconstr_env env n in - let psubn = pr_lconstr_env env subn in + let pm = pr_lconstr_env env sigma m in + let pn = pr_lconstr_env env sigma n in + let psubn = pr_lconstr_env env sigma subn in str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++ str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++ psubn ++ str " contains local variables." -let explain_refiner_cannot_generalize env ty = +let explain_refiner_cannot_generalize env sigma ty = str "Cannot find a well-typed generalisation of the goal with type: " ++ - pr_lconstr_env env ty ++ str "." + pr_lconstr_env env sigma ty ++ str "." -let explain_no_occurrence_found env c id = - str "Found no subterm matching " ++ pr_lconstr_env env c ++ +let explain_no_occurrence_found env sigma c id = + str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++ str " in " ++ (match id with | Some id -> pr_id id | None -> str"the current goal") ++ str "." -let explain_cannot_unify_binding_type env m n = - let pm = pr_lconstr_env env m in - let pn = pr_lconstr_env env n in +let explain_cannot_unify_binding_type env sigma m n = + let pm = pr_lconstr_env env sigma m in + let pn = pr_lconstr_env env sigma n in str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "." -let explain_cannot_find_well_typed_abstraction env p l e = +let explain_cannot_find_well_typed_abstraction env sigma p l e = str "Abstracting over the " ++ str (String.plural (List.length l) "term") ++ spc () ++ - hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++ - str "leads to a term" ++ spc () ++ pr_lconstr_goal_style_env env p ++ + hov 0 (pr_enum (pr_lconstr_env env sigma) l) ++ spc () ++ + str "leads to a term" ++ spc () ++ pr_lconstr_goal_style_env env sigma p ++ spc () ++ str "which is ill-typed." ++ (match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e) -let explain_wrong_abstraction_type env na abs expected result = +let explain_wrong_abstraction_type env sigma na abs expected result = let ppname = match na with Name id -> pr_id id ++ spc () | _ -> mt () in str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++ - pr_lconstr_env env expected ++ strbrk " with abstraction " ++ - pr_lconstr_env env abs ++ strbrk " of incompatible type " ++ - pr_lconstr_env env result ++ str "." + pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++ + pr_lconstr_env env sigma abs ++ strbrk " of incompatible type " ++ + pr_lconstr_env env sigma result ++ str "." let explain_abstraction_over_meta _ m n = strbrk "Too complex unification problem: cannot find a solution for both " ++ pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "." -let explain_non_linear_unification env m t = +let explain_non_linear_unification env sigma m t = strbrk "Cannot unambiguously instantiate " ++ pr_name m ++ str ":" ++ strbrk " which would require to abstract twice on " ++ - pr_lconstr_env env t ++ str "." + pr_lconstr_env env sigma t ++ str "." let explain_unsatisfied_constraints env cst = strbrk "Unsatisfied constraints: " ++ Univ.pr_constraints cst ++ @@ -636,17 +635,17 @@ let explain_type_error env sigma err = let env = make_all_name_different env in match err with | UnboundRel n -> - explain_unbound_rel env n + explain_unbound_rel env sigma n | UnboundVar v -> explain_unbound_var env v | NotAType j -> explain_not_type env sigma j | BadAssumption c -> - explain_bad_assumption env c + explain_bad_assumption env sigma c | ReferenceVariables (id,c) -> explain_reference_variables id c | ElimArity (ind, aritylst, c, pj, okinds) -> - explain_elim_arity env ind aritylst c pj okinds + explain_elim_arity env sigma ind aritylst c pj okinds | CaseNotInductive cj -> explain_case_not_inductive env sigma cj | NumberBranches (cj, n) -> @@ -654,7 +653,7 @@ let explain_type_error env sigma err = | IllFormedBranch (c, i, actty, expty) -> explain_ill_formed_branch env sigma c i actty expty | Generalization (nvar, c) -> - explain_generalization env nvar c + explain_generalization env sigma nvar c | ActualType (j, pt) -> explain_actual_type env sigma j pt None | CantApplyBadType (t, rator, randl) -> @@ -662,7 +661,7 @@ let explain_type_error env sigma err = | CantApplyNonFunctional (rator, randl) -> explain_cant_apply_not_functional env sigma rator randl | IllFormedRecBody (err, lna, i, fixenv, vdefj) -> - explain_ill_formed_rec_body env err lna i fixenv vdefj + explain_ill_formed_rec_body env sigma err lna i fixenv vdefj | IllTypedRecBody (i, lna, vdefj, vargs) -> explain_ill_typed_rec_body env sigma i lna vdefj vargs | WrongCaseInfo (ind,ci) -> @@ -683,13 +682,13 @@ let explain_cannot_unify_occurrences env sigma nested (cl2,pos2,t2) (cl1,pos1,t1 else "Found incompatible occurrences of the pattern" in let ppreason = match e with None -> mt() | Some (c1,c2,e) -> explain_unification_error env sigma c1 c2 (Some e) in str s ++ str ":" ++ - spc () ++ str "Matched term " ++ pr_lconstr_env env t2 ++ + spc () ++ str "Matched term " ++ pr_lconstr_env env sigma t2 ++ strbrk " at position " ++ pr_position (cl2,pos2) ++ strbrk " is not compatible with matched term " ++ - pr_lconstr_env env t1 ++ strbrk " at position " ++ + pr_lconstr_env env sigma t1 ++ strbrk " at position " ++ pr_position (cl1,pos1) ++ ppreason ++ str "." -let pr_constraints printenv env evd evars cstrs = +let pr_constraints printenv env sigma evars cstrs = let (ev, evi) = Evar.Map.choose evars in if Evar.Map.for_all (fun ev' evi' -> eq_named_context_val evi.evar_hyps evi'.evar_hyps) evars @@ -698,22 +697,22 @@ let pr_constraints printenv env evd evars cstrs = let pe = if printenv then pr_ne_context_of (str "In environment:") (mt ()) - (reset_with_named_context evi.evar_hyps env) ++ fnl () + (reset_with_named_context evi.evar_hyps env) sigma ++ fnl () else mt () in let evs = prlist_with_sep (fun () -> fnl ()) - (fun (ev, evi) -> str(string_of_existential ev) ++ + (fun (ev, evi) -> pr_existential_key sigma ev ++ str " : " ++ pr_lconstr evi.evar_concl) l in pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs) else let filter evk _ = Evar.Map.mem evk evars in - pr_evar_map_filter ~with_univs:false filter evd + pr_evar_map_filter ~with_univs:false filter sigma -let explain_unsatisfiable_constraints env evd constr comp = - let (_, constraints) = Evd.extract_all_conv_pbs evd in - let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined evd) in +let explain_unsatisfiable_constraints env sigma constr comp = + let (_, constraints) = Evd.extract_all_conv_pbs sigma in + let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined sigma) in (** Only keep evars that are subject to resolution and members of the given component. *) let is_kept evk evi = match comp with @@ -728,17 +727,17 @@ let explain_unsatisfiable_constraints env evd constr comp = match constr with | None -> str "Unable to satisfy the following constraints:" ++ fnl () ++ - pr_constraints true env evd undef constraints + pr_constraints true env sigma undef constraints | Some (ev, k) -> let cstr = let remaining = Evar.Map.remove ev undef in if not (Evar.Map.is_empty remaining) then str "With the following constraints:" ++ fnl () ++ - pr_constraints false env evd remaining constraints + pr_constraints false env sigma remaining constraints else mt () in let info = Evar.Map.find ev undef in - explain_typeclass_resolution env info k ++ fnl () ++ cstr + explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr let explain_pretype_error env sigma err = let env = Evarutil.env_nf_betaiotaevar sigma env in @@ -751,7 +750,7 @@ let explain_pretype_error env sigma err = let j = {uj_val = c; uj_type = actty} in explain_actual_type env sigma j t (Some e) | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs - | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp + | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env sigma evi k exp | VarNotFound id -> explain_var_not_found env id | UnexpectedType (actual,expect) -> let env, actual, expect = contract2 env actual expect in @@ -761,16 +760,16 @@ let explain_pretype_error env sigma err = let env, m, n = contract2 env m n in explain_cannot_unify env sigma m n e | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn - | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty - | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id - | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n + | CannotGeneralize ty -> explain_refiner_cannot_generalize env sigma ty + | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env sigma c id + | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n | CannotFindWellTypedAbstraction (p,l,e) -> - explain_cannot_find_well_typed_abstraction env p l + explain_cannot_find_well_typed_abstraction env sigma p l (Option.map (fun (env',e) -> explain_type_error env' sigma e) e) | WrongAbstractionType (n,a,t,u) -> - explain_wrong_abstraction_type env n a t u + explain_wrong_abstraction_type env sigma n a t u | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n - | NonLinearUnification (m,c) -> explain_non_linear_unification env m c + | NonLinearUnification (m,c) -> explain_non_linear_unification env sigma m c | TypingError t -> explain_type_error env sigma t | CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e | UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp @@ -793,9 +792,9 @@ let explain_not_match_error = function str "the body of definitions differs" | NotConvertibleTypeField (env, typ1, typ2) -> str "expected type" ++ spc () ++ - quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env Evd.empty typ2) ++ spc () ++ str "but found type" ++ spc () ++ - quote (Printer.safe_pr_lconstr_env env typ1) + quote (Printer.safe_pr_lconstr_env env Evd.empty typ1) | NotSameConstructorNamesField -> str "constructor names differ" | NotSameInductiveNameInBlockField -> @@ -919,7 +918,7 @@ let explain_module_internalization_error = function (* Typeclass errors *) let explain_not_a_class env c = - pr_constr_env env c ++ str" is not a declared type class." + pr_constr_env env Evd.empty c ++ str" is not a declared type class." let explain_unbound_method env cid id = str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ @@ -932,7 +931,7 @@ let pr_constr_exprs exprs = let explain_mismatched_contexts env c i j = str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ - hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env j) ++ + hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env Evd.empty j) ++ fnl () ++ brk (1,1) ++ hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i) @@ -994,19 +993,19 @@ let explain_refiner_error = function (* Inductive errors *) let error_non_strictly_positive env c v = - let pc = pr_lconstr_env env c in - let pv = pr_lconstr_env env v in + let pc = pr_lconstr_env env Evd.empty c in + let pv = pr_lconstr_env env Evd.empty v in str "Non strictly positive occurrence of " ++ pv ++ str " in" ++ brk(1,1) ++ pc ++ str "." let error_ill_formed_inductive env c v = - let pc = pr_lconstr_env env c in - let pv = pr_lconstr_env env v in + let pc = pr_lconstr_env env Evd.empty c in + let pv = pr_lconstr_env env Evd.empty v in str "Not enough arguments applied to the " ++ pv ++ str " in" ++ brk(1,1) ++ pc ++ str "." let error_ill_formed_constructor env id c v nparams nargs = - let pv = pr_lconstr_env env v in + let pv = pr_lconstr_env env Evd.empty v in let atomic = Int.equal (nb_prod c) 0 in str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ @@ -1026,12 +1025,12 @@ let error_ill_formed_constructor env id c v nparams nargs = let pr_ltype_using_barendregt_convention_env env c = (* Use goal_concl_style as an approximation of Barendregt's convention (?) *) - quote (pr_goal_concl_style_env env c) + quote (pr_goal_concl_style_env env Evd.empty c) let error_bad_ind_parameters env c n v1 v2 = let pc = pr_ltype_using_barendregt_convention_env env c in - let pv1 = pr_lconstr_env env v1 in - let pv2 = pr_lconstr_env env v2 in + let pv1 = pr_lconstr_env env Evd.empty v1 in + let pv2 = pr_lconstr_env env Evd.empty v2 in str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ str " as " ++ pr_nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "." @@ -1049,7 +1048,7 @@ let error_same_names_overlap idl = prlist_with_sep pr_comma pr_id idl ++ str "." let error_not_an_arity env c = - str "The type" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ + str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++ str "is not an arity." let error_bad_entry () = @@ -1100,9 +1099,9 @@ let explain_recursion_scheme_error = function (* Pattern-matching errors *) -let explain_bad_pattern env cstr ty = +let explain_bad_pattern env sigma cstr ty = let env = make_all_name_different env in - let pt = pr_lconstr_env env ty in + let pt = pr_lconstr_env env sigma ty in let pc = pr_constructor env cstr in str "Found the constructor " ++ pc ++ brk(1,1) ++ str "while matching a term of type " ++ pt ++ brk(1,1) ++ @@ -1143,18 +1142,18 @@ let explain_non_exhaustive env pats = str (String.plural (List.length pats) "pattern") ++ spc () ++ hov 0 (pr_sequence pr_cases_pattern pats) -let explain_cannot_infer_predicate env typs = +let explain_cannot_infer_predicate env sigma typs = let env = make_all_name_different env in let pr_branch (cstr,typ) = let cstr,_ = decompose_app cstr in - str "For " ++ pr_lconstr_env env cstr ++ str ": " ++ pr_lconstr_env env typ + str "For " ++ pr_lconstr_env env sigma cstr ++ str ": " ++ pr_lconstr_env env sigma typ in str "Unable to unify the types found in the branches:" ++ spc () ++ hov 0 (prlist_with_sep fnl pr_branch (Array.to_list typs)) -let explain_pattern_matching_error env = function +let explain_pattern_matching_error env sigma = function | BadPattern (c,t) -> - explain_bad_pattern env c t + explain_bad_pattern env sigma c t | BadConstructor (c,ind) -> explain_bad_constructor env c ind | WrongNumargConstructor (c,n) -> @@ -1166,12 +1165,12 @@ let explain_pattern_matching_error env = function | NonExhaustive tms -> explain_non_exhaustive env tms | CannotInferPredicate typs -> - explain_cannot_infer_predicate env typs + explain_cannot_infer_predicate env sigma typs let explain_reduction_tactic_error = function - | Tacred.InvalidAbstraction (env,c,(env',e)) -> + | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) -> str "The abstracted term" ++ spc () ++ - quote (pr_goal_concl_style_env env c) ++ + quote (pr_goal_concl_style_env env sigma c) ++ spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' Evd.empty e diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index bdc3eb7070..72f4149855 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -31,7 +31,7 @@ val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds val explain_refiner_error : refiner_error -> std_ppcmds val explain_pattern_matching_error : - env -> pattern_matching_error -> std_ppcmds + env -> Evd.evar_map -> pattern_matching_error -> std_ppcmds val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> std_ppcmds diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 9694c2d7ff..1c556d9b67 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -856,7 +856,7 @@ let rec solve_obligation prg num tac = ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps) | _ -> ())); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Printer.pr_constr_env (Global.env ()) obl.obl_type); + Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type); ignore (Pfedit.by (snd (get_default_tactic ()))); Option.iter (fun tac -> Pfedit.set_end_tac tac) tac | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " @@ -962,7 +962,7 @@ let show_obligations_of_prg ?(msg=true) prg = decr showed; msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (Id.to_string n) ++ str ":" ++ spc () ++ - hov 1 (Printer.pr_constr_env (Global.env ()) x.obl_type ++ + hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++ str "." ++ fnl ()))) | Some _ -> ()) obls @@ -979,8 +979,8 @@ let show_term n = let prg = get_prog_err n in let n = prg.prg_name in (str (Id.to_string n) ++ spc () ++ str":" ++ spc () ++ - Printer.pr_constr_env (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () - ++ Printer.pr_constr_env (Global.env ()) prg.prg_body) + Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl () + ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) obls = diff --git a/toplevel/search.ml b/toplevel/search.ml index 6a7d2c8118..9632e1c79e 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -85,8 +85,8 @@ let generic_search = iter_declarations (** Standard display *) -let plain_display accu ref a c = - let pc = pr_lconstr_env a c in +let plain_display accu ref env c = + let pc = pr_lconstr_env env Evd.empty c in let pr = pr_global ref in accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu @@ -312,7 +312,7 @@ let interface_search flags = let answer = { coq_object_prefix = prefix; coq_object_qualid = qualid; - coq_object_object = string_of_ppcmds (pr_lconstr_env env constr); + coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr); } in ans := answer :: !ans; in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b8baca9eb0..33a78110c3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -69,7 +69,7 @@ let show_top_evars () = let pfts = get_pftreestate () in let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in - msg_notice (pr_evars_int 1 (Evarutil.non_instantiated sigma)) + msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma)) let show_universes () = let pfts = get_pftreestate () in @@ -1117,7 +1117,7 @@ let default_env () = { let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let t,ctx = Constrintern.interp_type Evd.empty (Global.env()) c in - let t = Detyping.detype false [] [] t in + let t = Detyping.detype false [] [] Evd.empty t in let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl @@ -1469,13 +1469,13 @@ let vernac_check_may_eval redexp glopt rc = let c = nf c in let j = try - Evarutil.check_evars env sigma sigma' c; + Evarutil.check_evars env Evd.empty sigma' c; Arguments_renaming.rename_typing env c with Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) -> Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in match redexp with | None -> - msg_notice (print_judgment env j ++ Printer.pr_universe_ctx uctx) + msg_notice (print_judgment env sigma' j ++ Printer.pr_universe_ctx uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in @@ -1489,14 +1489,14 @@ let vernac_declare_reduction locality s r = (* The same but avoiding the current goal context if any *) let vernac_global_check c = let env = Global.env() in - let evmap = Evd.from_env env in - let c,ctx = interp_constr evmap env c in + let sigma = Evd.from_env env in + let c,ctx = interp_constr sigma env c in let senv = Global.safe_env() in let cstrs = snd (Evd.evar_universe_context_set ctx) in let senv = Safe_typing.add_constraints cstrs senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - msg_notice (print_safe_judgment env j) + msg_notice (print_safe_judgment env sigma j) let vernac_print = function | PrintTables -> msg_notice (print_tables ()) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 32f2473c50..c8054cf433 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -177,7 +177,7 @@ let send_whelp req s = let _ = CUnix.run_command ~hook:print_string command in () let whelp_constr req c = - let c = detype false [whelm_special] [] c in + let c = detype false [whelm_special] [] Evd.empty c in send_whelp req (make_string uri_of_constr c) let whelp_constr_expr req c = |