diff options
68 files changed, 1071 insertions, 979 deletions
diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh new file mode 100644 index 0000000000..01d3068591 --- /dev/null +++ b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh @@ -0,0 +1,21 @@ +if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then + + elpi_CI_REF=pretyping-rm-global + elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi + + coqhammer_CI_REF=pretyping-rm-global + coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer + + equations_CI_REF=pretyping-rm-global + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + + ltac2_CI_REF=pretyping-rm-global + ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + paramcoq_CI_REF=pretyping-rm-global + paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq + + mtac2_CI_REF=pretyping-rm-global + mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 + +fi diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 24b1362e6d..b89b6b5765 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -212,7 +212,7 @@ let encode_record r = module PrintingRecordRecord = PrintingInductiveMake (struct - let encode = encode_record + let encode _env = encode_record let field = "Record" let title = "Types leading to pretty-printing using record notation: " let member_message s b = @@ -224,7 +224,7 @@ module PrintingRecordRecord = module PrintingRecordConstructor = PrintingInductiveMake (struct - let encode = encode_record + let encode _env = encode_record let field = "Constructor" let title = "Types leading to pretty-printing using constructor form: " let member_message s b = @@ -289,11 +289,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l let add_patt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l + Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l let add_cpatt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l + Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -364,7 +364,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@ let pattern_printable_in_both_syntax (ind,_ as c) = let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in - let nb_params = Inductiveops.inductive_nparams ind in + let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in List.exists (fun (_,impls) -> (List.length impls >= nb_params) && let params,args = Util.List.chop nb_params impls in @@ -526,7 +526,7 @@ let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = functi let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) - if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then + if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), []) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 749eb2289c..3329ba2047 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -643,7 +643,7 @@ let terms_of_binders bl = | PatCstr (c,l,_) -> let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in - let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in + let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with | bnd :: l -> @@ -738,7 +738,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with - | [pat] -> (glob_constr_of_cases_pattern pat, None) + | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in let terms = Id.Map.fold mk_env terms Id.Map.empty in @@ -800,7 +800,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with - | [pat] -> glob_constr_of_cases_pattern pat + | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try @@ -1197,10 +1197,10 @@ let check_or_pat_variables loc ids idsl = @return if letin are included *) let check_constructor_length env loc cstr len_pl pl0 = let n = len_pl + List.length pl0 in - if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else - (Int.equal n (Inductiveops.constructor_nalldecls cstr) || + if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else + (Int.equal n (Inductiveops.constructor_nalldecls env cstr) || (error_wrong_numarg_constructor ?loc env cstr - (Inductiveops.constructor_nrealargs cstr))) + (Inductiveops.constructor_nrealargs env cstr))) open Declarations @@ -1226,9 +1226,9 @@ let add_local_defs_and_check_length loc env g pl args = match g with have been given in the "explicit" arguments, which come from a "@C args" notation or from a custom user notation *) let pl' = insert_local_defs_in_pattern cstr pl in - let maxargs = Inductiveops.constructor_nalldecls cstr in + let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then - error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr); + error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); (* Two possibilities: either the args are given with explict variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be @@ -1258,15 +1258,15 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 in aux 0 (impl_list,pl2) let add_implicits_check_constructor_length env loc c len_pl1 pl2 = - let nargs = Inductiveops.constructor_nallargs c in - let nargs' = Inductiveops.constructor_nalldecls c in + let nargs = Inductiveops.constructor_nallargs env c in + let nargs' = Inductiveops.constructor_nalldecls env c in let impls_st = implicits_of_global (ConstructRef c) in add_implicits_check_length (error_wrong_numarg_constructor ?loc env c) nargs nargs' impls_st len_pl1 pl2 let add_implicits_check_ind_length env loc c len_pl1 pl2 = - let nallargs = inductive_nallargs_env env c in - let nalldecls = inductive_nalldecls_env env c in + let nallargs = inductive_nallargs env c in + let nalldecls = inductive_nalldecls env c in let impls_st = implicits_of_global (IndRef c) in add_implicits_check_length (error_wrong_numarg_inductive ?loc env c) nallargs nalldecls impls_st len_pl1 pl2 @@ -1274,8 +1274,8 @@ let add_implicits_check_ind_length env loc c len_pl1 pl2 = (** Do not raise NotEnoughArguments thanks to preconditions*) let chop_params_pattern loc ind args with_letin = let nparams = if with_letin - then Inductiveops.inductive_nparamdecls ind - else Inductiveops.inductive_nparams ind in + then Inductiveops.inductive_nparamdecls (Global.env()) ind + else Inductiveops.inductive_nparams (Global.env()) ind in assert (nparams <= List.length args); let params,args = List.chop nparams args in List.iter (fun c -> match DAst.get c with @@ -1295,10 +1295,11 @@ let find_constructor loc add_params ref = in cstr, match add_params with | Some nb_args -> + let env = Global.env () in let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr) - then Inductiveops.inductive_nparamdecls ind - else Inductiveops.inductive_nparams ind + if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr) + then Inductiveops.inductive_nparamdecls env ind + else Inductiveops.inductive_nparams env ind in List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) | None -> [] diff --git a/interp/declare.ml b/interp/declare.ml index 717f8ef49a..76b4bab2ce 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -346,6 +346,25 @@ let inInductive : mutual_inductive_entry -> obj = discharge_function = discharge_inductive; rebuild_function = rebuild_inductive } +let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c + +let load_prim _ p = cache_prim p + +let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c + +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) + +let inPrim : (Projection.Repr.t * Constant.t) -> obj = + declare_object { + (default_object "PRIMPROJS") with + cache_function = cache_prim ; + load_function = load_prim; + subst_function = subst_prim; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_prim } + +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) + let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = let id = Label.to_id label in let univs, u = match univs with @@ -360,7 +379,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let entry = definition_entry ~types ~univs term in let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - Recordops.declare_primitive_projection p cst + declare_primitive_projection p cst let declare_projections univs mind = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 854651e7b7..dffccf02fc 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -231,23 +231,25 @@ let implicit_application env ?(allow_partial=true) f ty = | Some ({CAst.loc;v=(id, par, inst)}, gr) -> let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in let c, avoid = - let c = class_info gr in - let (ci, rd) = c.cl_context in - if not allow_partial then - begin - let opt_succ x n = match x with - | None -> succ n - | Some _ -> n - in - let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in - let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in - if not (Int.equal needlen applen) then - mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd - end; - let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid f par pars in - CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid - in c, avoid + let env = Global.env () in + let sigma = Evd.from_env env in + let c = class_info env sigma gr in + let (ci, rd) = c.cl_context in + if not allow_partial then + begin + let opt_succ x n = match x with + | None -> succ n + | Some _ -> n + in + let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in + let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in + if not (Int.equal needlen applen) then + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd + end; + let pars = List.rev (List.combine ci rd) in + let args, avoid = combine_params avoid f par pars in + CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid + in c, avoid let warn_ignoring_implicit_status = CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" diff --git a/interp/notation.ml b/interp/notation.ml index b9aca82cf4..56504db04e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1516,7 +1516,7 @@ let uninterp_prim_token c = with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_cases_pattern c = - match glob_constr_of_closed_cases_pattern c with + match glob_constr_of_closed_cases_pattern (Global.env()) c with | exception Not_found -> raise Notation_ops.No_match | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7d7e10a05b..9801e56ca1 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -782,7 +782,7 @@ let rec pat_binder_of_term t = DAst.map (function | GApp (t, l) -> begin match DAst.get t with | GRef (ConstructRef cstr,_) -> - let nparams = Inductiveops.inductive_nparams (fst cstr) in + let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) | _ -> raise No_match @@ -909,7 +909,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) alp, add_env alp sigma var (DAst.make @@ GVar id) let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in + let env = Global.env () in + let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let patl' = Id.List.assoc var binders in @@ -1292,7 +1293,7 @@ let match_notation_constr u c (metas,pat) = | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with | [pat] -> - let v = glob_constr_of_cases_pattern pat in + let v = glob_constr_of_cases_pattern (Global.env()) pat in ((v,scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) -> @@ -1333,11 +1334,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in sigma,(0,l) | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in + let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then diff --git a/library/goptions.ml b/library/goptions.ml index 1b907fd966..b9c1802a72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -57,7 +57,7 @@ module MakeTable = type key val compare : t -> t -> int val table : (string * key table_of_A) list ref - val encode : key -> t + val encode : Environ.env -> key -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -111,10 +111,10 @@ module MakeTable = class table_of_A () = object - method add x = add_option (A.encode x) - method remove x = remove_option (A.encode x) + method add x = add_option (A.encode (Global.env()) x) + method remove x = remove_option (A.encode (Global.env()) x) method mem x = - let y = A.encode x in + let y = A.encode (Global.env()) x in let answer = MySet.mem y !t in Feedback.msg_info (A.member_message y answer) method print = print_table A.title A.printer !t @@ -142,7 +142,7 @@ struct type key = string let compare = String.compare let table = string_table - let encode x = x + let encode _env x = x let subst _ x = x let printer = str let key = A.key @@ -161,7 +161,7 @@ module type RefConvertArg = sig type t val compare : t -> t -> int - val encode : qualid -> t + val encode : Environ.env -> qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name diff --git a/library/goptions.mli b/library/goptions.mli index b91553bf3c..9925eb9e7b 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -89,8 +89,8 @@ module MakeRefTable : (A : sig type t val compare : t -> t -> int - val encode : qualid -> t - val subst : substitution -> t -> t + val encode : Environ.env -> qualid -> t + val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name val title : string diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 50fc2448fc..0e3b9fc2b6 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -67,7 +67,7 @@ let rec decompose_term env sigma t= let canon_mind = MutInd.make1 (MutInd.canonical mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in - let nargs=constructor_nallargs_env env (canon_ind,i_con) in + let nargs=constructor_nallargs env (canon_ind,i_con) in Constructor {ci_constr= ((canon_ind,i_con),u); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index c9cfd74362..9db7c8d8d3 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -854,7 +854,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = and extract_case env sg mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) - let ni = constructors_nrealargs_env env ip in + let ni = constructors_nrealargs env ip in let br_size = Array.length br in assert (Int.equal (Array.length ni) br_size); if Int.equal br_size 0 then begin diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 56b3dc97cf..4b7bc707d6 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -82,13 +82,13 @@ let pop t = Vars.lift (-1) t let kind_of_formula env sigma term = let normalize = special_nf env sigma in let cciterm = special_whd env sigma term in - match match_with_imp_term sigma cciterm with + match match_with_imp_term env sigma cciterm with Some (a,b)-> Arrow (a, pop b) |_-> - match match_with_forall_term sigma cciterm with + match match_with_forall_term env sigma cciterm with Some (_,a,b)-> Forall (a, b) |_-> - match match_with_nodep_ind sigma cciterm with + match match_with_nodep_ind env sigma cciterm with Some (i,l,n)-> let ind,u=EConstr.destInd sigma i in let u = EConstr.EInstance.kind sigma u in @@ -111,7 +111,7 @@ let kind_of_formula env sigma term = else Or((ind,u),l,is_trivial) | _ -> - match match_with_sigma_type sigma cciterm with + match match_with_sigma_type env sigma cciterm with Some (i,l)-> let (ind, u) = EConstr.destInd sigma i in let u = EConstr.EInstance.kind sigma u in diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 01b18e2f30..9f2ceb2c28 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -188,7 +188,7 @@ let empty_seq depth= let expand_constructor_hints = List.map_append (function | GlobRef.IndRef ind -> - List.init (Inductiveops.nconstructors ind) + List.init (Inductiveops.nconstructors (Global.env()) ind) (fun i -> GlobRef.ConstructRef (ind,i+1)) | gr -> [gr]) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 275b58f0aa..45a4e61846 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -317,7 +317,7 @@ let build_constructors_of_type ind' argl = Impargs.implicits_of_global constructref in let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) construct in @@ -330,7 +330,7 @@ let build_constructors_of_type ind' argl = let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) in - cases_pattern_of_glob_constr Anonymous pat_as_term + cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term ) ind.Declarations.mind_consnames @@ -415,7 +415,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function mkGVar id | PatCstr(constr,patternl,_) -> let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) constr in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 13ff19a46b..7b758da8e8 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -361,7 +361,7 @@ let rec pattern_to_term pt = DAst.with_val (function mkGVar id | PatCstr(constr,patternl,_) -> let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) constr in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a5c19f3217..e582362e25 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -382,8 +382,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let _ = List.map_i (fun i x -> - let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in - let env = Global.env () in + let env = Global.env () in + let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 75565c1a34..2d40ba6562 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -119,7 +119,7 @@ let app_poly_check env evars f args = (evars, cstrs), t let app_poly_nocheck env evars f args = - let evars, fc = f evars in + let evars, fc = f evars in evars, mkApp (fc, args) let app_poly_sort b = @@ -175,25 +175,29 @@ end) = struct let rewrite_relation_class = find_global relation_classes "RewriteRelation" - let proper_class = lazy (class_info (find_reference morphisms "Proper")) - let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy")) - - let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) - - let proper_type = - let l = lazy (Lazy.force proper_class).cl_impl in - fun (evd,cstrs) -> - let (evd, c) = Evarutil.new_global evd (Lazy.force l) in - (evd, cstrs), c - - let proper_proxy_type = - let l = lazy (Lazy.force proper_proxy_class).cl_impl in - fun (evd,cstrs) -> - let (evd, c) = Evarutil.new_global evd (Lazy.force l) in - (evd, cstrs), c + let proper_class = + let r = lazy (find_reference morphisms "Proper") in + fun env sigma -> class_info env sigma (Lazy.force r) + + let proper_proxy_class = + let r = lazy (find_reference morphisms "ProperProxy") in + fun env sigma -> class_info env sigma (Lazy.force r) + + let proper_proj env sigma = + mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs))) + + let proper_type env (sigma,cstrs) = + let l = (proper_class env sigma).cl_impl in + let (sigma, c) = Evarutil.new_global sigma l in + (sigma, cstrs), c + + let proper_proxy_type env (sigma,cstrs) = + let l = (proper_proxy_class env sigma).cl_impl in + let (sigma, c) = Evarutil.new_global sigma l in + (sigma, cstrs), c let proper_proof env evars carrier relation x = - let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in + let evars, goal = app_poly env evars (proper_proxy_type env) [| carrier ; relation; x |] in new_cstr_evar evars env goal let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env @@ -800,7 +804,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev in (* Actual signature found *) let cl_args = [| appmtype' ; signature ; appm |] in - let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type) + let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type env else TypeGlobal.proper_type env) cl_args in let env' = let dosub, appsub = @@ -1310,8 +1314,8 @@ module Strategies = in let evars, proof = let proxy = - if prop then PropGlobal.proper_proxy_type - else TypeGlobal.proper_proxy_type + if prop then PropGlobal.proper_proxy_type env + else TypeGlobal.proper_proxy_type env in let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in new_cstr_evar evars env mty @@ -1854,12 +1858,12 @@ let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans = let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) -let proper_projection sigma r ty = +let proper_projection env sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in let ctx, inst = decompose_prod_assum sigma ty in let mor, args = destApp sigma inst in let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in - let app = mkApp (Lazy.force PropGlobal.proper_proj, + let app = mkApp (PropGlobal.proper_proj env sigma, Array.append args [| instarg |]) in it_mkLambda_or_LetIn app ctx @@ -1869,7 +1873,7 @@ let declare_projection n instance_id r = let sigma = Evd.from_env env in let sigma,c = Evd.fresh_global env sigma r in let ty = Retyping.get_type_of env sigma c in - let term = proper_projection sigma c ty in + let term = proper_projection env sigma c ty in let sigma, typ = Typing.type_of env sigma term in let ctx, typ = decompose_prod_assum sigma typ in let typ = @@ -1924,7 +1928,7 @@ let build_morphism_signature env sigma m = rel) cstrs in - let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in + let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in let evd = solve_constraints env !evd in let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in @@ -1938,9 +1942,9 @@ let default_morphism sign m = let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in - let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in + let evars, morph = app_poly_check env evars (PropGlobal.proper_type env) [| t; sign; m |] in let evars, mor = resolve_one_typeclass env (goalevars evars) morph in - mor, proper_projection sigma mor morph + mor, proper_projection env sigma mor morph let warn_add_setoid_deprecated = CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> @@ -1984,8 +1988,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); + add_instance (Classes.mk_instance + (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst); pstate else @@ -1995,8 +1999,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ _ _ = function | Globnames.ConstRef cst -> - add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info + add_instance (Classes.mk_instance + (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index caaa547a07..e617f3d45e 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -30,7 +30,7 @@ let subst_quantified_hypothesis _ x = x let subst_declared_or_quantified_hypothesis _ x = x let subst_glob_constr_and_expr subst (c, e) = - (Detyping.subst_glob_constr subst c, e) + (Detyping.subst_glob_constr (Global.env()) subst c, e) let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) @@ -99,7 +99,9 @@ let subst_evaluable subst = let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) let subst_glob_constr_or_pattern subst (bvars,c,p) = - (bvars,subst_glob_constr subst c,subst_pattern subst p) + let env = Global.env () in + let sigma = Evd.from_env env in + (bvars,subst_glob_constr subst c,subst_pattern env sigma subst p) let subst_redexp subst = Redops.map_red_expr_gen diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4c65445b89..d1951cc18d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -98,16 +98,18 @@ let split = Tactics.split_with_bindings false [Tactypes.NoBindings] (** Test *) let is_empty _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> - if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail + if is_empty_type genv sigma (assoc_var "X1" ist) then idtac else fail (* Strictly speaking, this exceeds the propositional fragment as it matches also equality types (and solves them if a reflexivity) *) let is_unit_or_eq _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in - if test sigma (assoc_var "X1" ist) then idtac else fail + if test genv sigma (assoc_var "X1" ist) then idtac else fail let bugged_is_binary sigma t = isApp sigma t && @@ -121,23 +123,25 @@ let bugged_is_binary sigma t = (** Dealing with conjunction *) let is_conj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let ind = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) && - is_conjunction sigma + is_conjunction genv sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode ind then idtac else fail let flatten_contravariant_conj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_conjunction sigma + match match_with_conjunction genv sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with @@ -151,23 +155,25 @@ let flatten_contravariant_conj _ ist = (** Dealing with disjunction *) let is_disj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let t = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) && - is_disjunction sigma + is_disjunction genv sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode t then idtac else fail let flatten_contravariant_disj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_disjunction sigma + match match_with_disjunction genv sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 350bb9019e..675e4d2457 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -194,7 +194,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let sort = Tacticals.elimination_sort_of_goal gl in let gl, elim = if not is_case then - let t,gl= pf_fresh_global (Indrec.lookup_eliminator (kn,i) sort) gl in + let t,gl= pf_fresh_global (Indrec.lookup_eliminator env (kn,i) sort) gl in gl, t else Tacmach.pf_eapply (fun env sigma () -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 5abbc214de..4433f2fce7 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -340,7 +340,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in - let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in + let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = destConst elim in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in @@ -504,9 +504,9 @@ let rwprocess_rule dir rule gl = let sigma, rs2 = loop d sigma s a.(1) rs 0 in let s, sigma = sr sigma 1 in loop d sigma s a.(0) rs2 0 - | App (r_eq, a) when Hipattern.match_with_equality_type sigma t != None -> + | App (r_eq, a) when Hipattern.match_with_equality_type env sigma t != None -> let (ind, u) = EConstr.destInd sigma r_eq and rhs = Array.last a in - let np = Inductiveops.inductive_nparamdecls ind in + let np = Inductiveops.inductive_nparamdecls env ind in let indu = (ind, EConstr.EInstance.kind sigma u) in let ind_ct = Inductiveops.type_of_constructors env indu in let lhs0 = last_arg sigma (EConstr.of_constr (strip_prod_assum ind_ct.(0))) in diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 537fd7d7b4..075ebf006a 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -43,7 +43,7 @@ module AdaptorDb = struct term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db let subst_adaptor ( subst, (k, t as a)) = - let t' = Detyping.subst_glob_constr subst t in + let t' = Detyping.subst_glob_constr (Global.env()) subst t in if t' == t then a else k, t' let in_db = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e22368d5e5..d7a6c4c832 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -284,7 +284,7 @@ let rec find_row_ind = function let inductive_template env sigma tmloc ind = let sigma, indu = Evd.fresh_inductive_instance env sigma ind in - let arsign = inductive_alldecls_env env indu in + let arsign = inductive_alldecls env indu in let indu = on_snd EInstance.make indu in let hole_source i = match tmloc with | Some loc -> Loc.tag ~loc @@ Evar_kinds.TomatchTypeParameter (ind,i) @@ -313,7 +313,7 @@ let try_find_ind env sigma typ realnames = | Some names -> names | None -> let ind = fst (fst (dest_ind_family indf)) in - List.make (inductive_nrealdecls ind) Anonymous in + List.make (inductive_nrealdecls env ind) Anonymous in IsInd (typ,ind,names) let inh_coerce_to_ind env sigma0 loc ty tyi = @@ -1796,7 +1796,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t = | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc | App (f,v) when isConstruct sigma f -> let cstr,u = destConstruct sigma f in - let n = constructor_nrealargs_env !!env cstr in + let n = constructor_nrealargs !!env cstr in let l = List.lastn n (Array.to_list v) in let l,acc = List.fold_right_map reveal_pattern l acc in DAst.make (PatCstr (cstr,l,Anonymous)), acc @@ -1929,7 +1929,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in let ((ind,u),_) = dest_ind_family indf' in - let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in + let nrealargs_ctxt = inductive_nrealdecls env0 ind in let arsign, inds = get_arity env0 indf' in let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal = diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 5560e5e5f5..90ce1cc594 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -15,7 +15,6 @@ open Names open Constr open Libnames open Globnames -open Libobject open Mod_subst (* usage qque peu general: utilise aussi dans record *) @@ -288,7 +287,7 @@ let get_coercion_constructor env coe = let red x = fst (Reductionops.whd_all_stack env evd x) in match EConstr.kind evd (red (mkNamed coe.coe_value)) with | Constr.Construct (c, _) -> - c, Inductiveops.constructor_nrealargs c -1 + c, Inductiveops.constructor_nrealargs env c -1 | _ -> raise Not_found let lookup_pattern_path_between env (s,t) = @@ -305,8 +304,8 @@ let install_path_printer f = path_printer := f let print_path x = !path_printer x -let path_comparator : (inheritance_path -> inheritance_path -> bool) ref = - ref (fun _ _ -> false) +let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref = + ref (fun _ _ _ _ -> false) let install_path_comparator f = path_comparator := f @@ -319,24 +318,24 @@ let warn_ambiguous_path = (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) -let different_class_params i = +let different_class_params env i = let ci = class_info_from_index i in if (snd ci).cl_param > 0 then true else match fst ci with - | CL_IND i -> Global.is_polymorphic (IndRef i) - | CL_CONST c -> Global.is_polymorphic (ConstRef c) + | CL_IND i -> Environ.is_polymorphic env (IndRef i) + | CL_CONST c -> Environ.is_polymorphic env (ConstRef c) | _ -> false -let add_coercion_in_graph (ic,source,target) = +let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in let try_add_new_path (i,j as ij) p = - if not (Bijint.Index.equal i j) || different_class_params i then + if not (Bijint.Index.equal i j) || different_class_params env i then match lookup_path_between_class ij with | q -> - if not (compare_path p q) then + if not (compare_path env sigma p q) then ambig_paths := (ij,p)::!ambig_paths; false | exception Not_found -> (add_new_path ij p; true) @@ -374,31 +373,42 @@ type coercion = { coercion_params : int; } +let subst_coercion subst c = + let coe = subst_coe_typ subst c.coercion_type in + let cls = subst_cl_typ subst c.coercion_source in + let clt = subst_cl_typ subst c.coercion_target in + let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in + if c.coercion_type == coe && c.coercion_source == cls && + c.coercion_target == clt && c.coercion_is_proj == clp + then c + else { c with coercion_type = coe; coercion_source = cls; + coercion_target = clt; coercion_is_proj = clp; } + (* Computation of the class arity *) -let reference_arity_length ref = - let t, _ = Typeops.type_of_global_in_context (Global.env ()) ref in - List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *) +let reference_arity_length env sigma ref = + let t, _ = Typeops.type_of_global_in_context env ref in + List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t))) -let projection_arity_length p = - let len = reference_arity_length (ConstRef (Projection.Repr.constant p)) in +let projection_arity_length env sigma p = + let len = reference_arity_length env sigma (ConstRef (Projection.Repr.constant p)) in len - Projection.Repr.npars p -let class_params = function +let class_params env sigma = function | CL_FUN | CL_SORT -> 0 - | CL_CONST sp -> reference_arity_length (ConstRef sp) - | CL_PROJ sp -> projection_arity_length sp - | CL_SECVAR sp -> reference_arity_length (VarRef sp) - | CL_IND sp -> reference_arity_length (IndRef sp) + | CL_CONST sp -> reference_arity_length env sigma (ConstRef sp) + | CL_PROJ sp -> projection_arity_length env sigma sp + | CL_SECVAR sp -> reference_arity_length env sigma (VarRef sp) + | CL_IND sp -> reference_arity_length env sigma (IndRef sp) (* add_class : cl_typ -> locality_flag option -> bool -> unit *) -let add_class cl = - add_new_class cl { cl_param = class_params cl } +let add_class env sigma cl = + add_new_class cl { cl_param = class_params env sigma cl } -let cache_coercion (_, c) = - let () = add_class c.coercion_source in - let () = add_class c.coercion_target in +let declare_coercion env sigma c = + let () = add_class env sigma c.coercion_source in + let () = add_class env sigma c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in let xf = @@ -409,65 +419,7 @@ let cache_coercion (_, c) = coe_param = c.coercion_params; } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) - -let open_coercion i o = - if Int.equal i 1 then - cache_coercion o - -let subst_coercion (subst, c) = - let coe = subst_coe_typ subst c.coercion_type in - let cls = subst_cl_typ subst c.coercion_source in - let clt = subst_cl_typ subst c.coercion_target in - let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in - if c.coercion_type == coe && c.coercion_source == cls && - c.coercion_target == clt && c.coercion_is_proj == clp - then c - else { c with coercion_type = coe; coercion_source = cls; - coercion_target = clt; coercion_is_proj = clp; } - -let discharge_coercion (_, c) = - if c.coercion_local then None - else - let n = - try - let ins = Lib.section_instance c.coercion_type in - Array.length (snd ins) - with Not_found -> 0 - in - let nc = { c with - coercion_params = n + c.coercion_params; - coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; - } in - Some nc - -let classify_coercion obj = - if obj.coercion_local then Dispose else Substitute obj - -let inCoercion : coercion -> obj = - declare_object {(default_object "COERCION") with - open_function = open_coercion; - cache_function = cache_coercion; - subst_function = subst_coercion; - classify_function = classify_coercion; - discharge_function = discharge_coercion } - -let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = - let isproj = - match coef with - | ConstRef c -> Recordops.find_primitive_projection c - | _ -> None - in - let c = { - coercion_type = coef; - coercion_local = local; - coercion_is_id = isid; - coercion_is_proj = isproj; - coercion_source = cls; - coercion_target = clt; - coercion_params = ps; - } in - Lib.add_anonymous_leaf (inCoercion c) + add_coercion_in_graph env sigma (xf,is,it) (* For printing purpose *) let pr_cl_index = Bijint.Index.print @@ -490,7 +442,7 @@ module CoercionPrinting = struct type t = coe_typ let compare = GlobRef.Ordered.compare - let encode = coercion_of_reference + let encode _env = coercion_of_reference let subst = subst_coe_typ let printer x = Nametab.pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] diff --git a/pretyping/classops.mli b/pretyping/classops.mli index bd468e62ad..c04182930e 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -75,9 +75,19 @@ val inductive_class_of : inductive -> cl_index val class_args_of : env -> evar_map -> types -> constr list (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) -val declare_coercion : - coe_typ -> ?local:bool -> isid:bool -> - src:cl_typ -> target:cl_typ -> params:int -> unit +type coercion = { + coercion_type : coe_typ; + coercion_local : bool; + coercion_is_id : bool; + coercion_is_proj : Projection.Repr.t option; + coercion_source : cl_typ; + coercion_target : cl_typ; + coercion_params : int; +} + +val subst_coercion : substitution -> coercion -> coercion + +val declare_coercion : env -> evar_map -> coercion -> unit (** {6 Access to coercions infos } *) val coercion_exists : coe_typ -> bool @@ -101,7 +111,7 @@ val lookup_pattern_path_between : val install_path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit val install_path_comparator : - (inheritance_path -> inheritance_path -> bool) -> unit + (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 87d3880f99..eaa5736336 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -145,9 +145,9 @@ let add_name_opt na b t (nenv, env) = (****************************************************************************) (* Tools for printing of Cases *) -let encode_inductive r = +let encode_inductive env r = let indsp = Nametab.global_inductive r in - let constr_lengths = constructors_nrealargs indsp in + let constr_lengths = constructors_nrealargs env indsp in (indsp,constr_lengths) (* Parameterization of the translation from constr to ast *) @@ -159,15 +159,15 @@ let has_two_constructors lc = let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1 -let encode_bool ({CAst.loc} as r) = - let (x,lc) = encode_inductive r in +let encode_bool env ({CAst.loc} as r) = + let (x,lc) = encode_inductive env r in if not (has_two_constructors lc) then user_err ?loc ~hdr:"encode_if" (str "This type has not exactly two constructors."); x -let encode_tuple ({CAst.loc} as r) = - let (x,lc) = encode_inductive r in +let encode_tuple env ({CAst.loc} as r) = + let (x,lc) = encode_inductive env r in if not (isomorphic_to_tuple lc) then user_err ?loc ~hdr:"encode_tuple" (str "This type cannot be seen as a tuple type."); @@ -175,7 +175,7 @@ let encode_tuple ({CAst.loc} as r) = module PrintingInductiveMake = functor (Test : sig - val encode : qualid -> inductive + val encode : Environ.env -> qualid -> inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -1014,13 +1014,12 @@ let rec subst_cases_pattern subst = DAst.map (function let (f_subst_genarg, subst_genarg_hook) = Hook.make () -let rec subst_glob_constr subst = DAst.map (function +let rec subst_glob_constr env subst = DAst.map (function | GRef (ref,u) as raw -> let ref',t = subst_global subst ref in if ref' == ref then raw else (match t with | None -> GRef (ref', u) | Some t -> - let env = Global.env () in let evd = Evd.from_env env in let t = t.Univ.univ_abstracted_value in (* XXX This seems dangerous *) DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))) @@ -1032,33 +1031,33 @@ let rec subst_glob_constr subst = DAst.map (function | GPatVar _ as raw -> raw | GApp (r,rl) as raw -> - let r' = subst_glob_constr subst r - and rl' = List.Smart.map (subst_glob_constr subst) rl in + let r' = subst_glob_constr env subst r + and rl' = List.Smart.map (subst_glob_constr env subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') | GLambda (n,bk,r1,r2) as raw -> - let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in + let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in if r1' == r1 && r2' == r2 then raw else GLambda (n,bk,r1',r2') | GProd (n,bk,r1,r2) as raw -> - let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in + let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in if r1' == r1 && r2' == r2 then raw else GProd (n,bk,r1',r2') | GLetIn (n,r1,t,r2) as raw -> - let r1' = subst_glob_constr subst r1 in - let r2' = subst_glob_constr subst r2 in - let t' = Option.Smart.map (subst_glob_constr subst) t in + let r1' = subst_glob_constr env subst r1 in + let r2' = subst_glob_constr env subst r2 in + let t' = Option.Smart.map (subst_glob_constr env subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> let open CAst in - let rtno' = Option.Smart.map (subst_glob_constr subst) rtno + let rtno' = Option.Smart.map (subst_glob_constr env subst) rtno and rl' = List.Smart.map (fun (a,x as y) -> - let a' = subst_glob_constr subst a in + let a' = subst_glob_constr env subst a in let (n,topt) = x in let topt' = Option.Smart.map (fun ({loc;v=((sp,i),y)} as t) -> @@ -1069,7 +1068,7 @@ let rec subst_glob_constr subst = DAst.map (function (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = List.Smart.map (subst_cases_pattern subst) cpl - and r' = subst_glob_constr subst r in + and r' = subst_glob_constr env subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) branches @@ -1078,27 +1077,27 @@ let rec subst_glob_constr subst = DAst.map (function GCases (sty,rtno',rl',branches') | GLetTuple (nal,(na,po),b,c) as raw -> - let po' = Option.Smart.map (subst_glob_constr subst) po - and b' = subst_glob_constr subst b - and c' = subst_glob_constr subst c in + let po' = Option.Smart.map (subst_glob_constr env subst) po + and b' = subst_glob_constr env subst b + and c' = subst_glob_constr env subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') | GIf (c,(na,po),b1,b2) as raw -> - let po' = Option.Smart.map (subst_glob_constr subst) po - and b1' = subst_glob_constr subst b1 - and b2' = subst_glob_constr subst b2 - and c' = subst_glob_constr subst c in + let po' = Option.Smart.map (subst_glob_constr env subst) po + and b1' = subst_glob_constr env subst b1 + and b2' = subst_glob_constr env subst b2 + and c' = subst_glob_constr env subst c in if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else GIf (c',(na,po'),b1',b2') | GRec (fix,ida,bl,ra1,ra2) as raw -> - let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 - and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in + let ra1' = Array.Smart.map (subst_glob_constr env subst) ra1 + and ra2' = Array.Smart.map (subst_glob_constr env subst) ra2 in let bl' = Array.Smart.map (List.Smart.map (fun (na,k,obd,ty as dcl) -> - let ty' = subst_glob_constr subst ty in - let obd' = Option.Smart.map (subst_glob_constr subst) obd in + let ty' = subst_glob_constr env subst ty in + let obd' = Option.Smart.map (subst_glob_constr env subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else @@ -1116,8 +1115,8 @@ let rec subst_glob_constr subst = DAst.map (function else GHole (nknd, naming, nsolve) | GCast (r1,k) as raw -> - let r1' = subst_glob_constr subst r1 in - let k' = smartmap_cast_type (subst_glob_constr subst) k in + let r1' = subst_glob_constr env subst r1 in + let k' = smartmap_cast_type (subst_glob_constr env subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') ) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 8695d52b12..1a8e97efb8 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -37,7 +37,7 @@ val print_allow_match_default_clause : bool ref val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern -val subst_glob_constr : substitution -> glob_constr -> glob_constr +val subst_glob_constr : env -> substitution -> glob_constr -> glob_constr val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g @@ -87,7 +87,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig - val encode : Libnames.qualid -> Names.inductive + val encode : Environ.env -> Libnames.qualid -> Names.inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -95,7 +95,7 @@ module PrintingInductiveMake : sig type t = Names.inductive val compare : t -> t -> int - val encode : Libnames.qualid -> Names.inductive + val encode : Environ.env -> Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t val key : Goptions.option_name diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a4a078bfa0..4a941a68b1 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -73,11 +73,11 @@ let normalize_evar evd ev = | Evar (evk,args) -> (evk,args) | _ -> assert false -let get_polymorphic_positions sigma f = +let get_polymorphic_positions env sigma f = let open Declarations in match EConstr.kind sigma f with - | Ind (ind, u) | Construct ((ind, _), u) -> - let mib,oib = Global.lookup_inductive ind in + | Ind (ind, u) | Construct ((ind, _), u) -> + let mib,oib = Inductive.lookup_mind_specif env ind in (match oib.mind_arity with | RegularArity _ -> assert false | TemplateArity templ -> templ.template_param_levels) @@ -128,7 +128,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) let rec refresh_term_evars ~onevars ~top t = match EConstr.kind !evdref t with | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f -> - let pos = get_polymorphic_positions !evdref f in + let pos = get_polymorphic_positions env !evdref f in refresh_polymorphic_positions args pos; t | App (f, args) when top && isEvar !evdref f -> let f' = refresh_term_evars ~onevars:true ~top:false f in @@ -1203,17 +1203,17 @@ exception CannotProject of evar_map * EConstr.existential of subterms to eventually discard so as to be allowed to keep ti. *) -let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t = +let rec is_constrainable_in top env evd k (ev,(fv_rels,fv_ids) as g) t = let f,args = decompose_app_vect evd t in match EConstr.kind evd f with | Construct ((ind,_),u) -> - let n = Inductiveops.inductive_nparams ind in + let n = Inductiveops.inductive_nparams env ind in if n > Array.length args then true (* We don't try to be more clever *) else let params = fst (Array.chop n args) in - Array.for_all (is_constrainable_in false evd k g) params - | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args - | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2 + Array.for_all (is_constrainable_in false env evd k g) params + | Ind _ -> Array.for_all (is_constrainable_in false env evd k g) args + | Prod (na,t1,t2) -> is_constrainable_in false env evd k g t1 && is_constrainable_in false env evd k g t2 | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels @@ -1238,7 +1238,7 @@ let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_r | None -> (* t is an instance for a proper variable; we filter it along *) (* the free variables allowed to occur *) - (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t + (not force || noccur_evar env evd ev t) && is_constrainable_in true env evd k (ev,(fv_rels,fv_ids)) t exception EvarSolvedOnTheFly of evar_map * EConstr.constr diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 74432cc010..6da168711c 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -492,7 +492,7 @@ let is_gvar id c = match DAst.get c with | GVar id' -> Id.equal id id' | _ -> false -let rec cases_pattern_of_glob_constr na c = +let rec cases_pattern_of_glob_constr env na c = (* Forcing evaluation to ensure that the possible raising of Not_found is not delayed *) let c = DAst.force c in @@ -509,14 +509,14 @@ let rec cases_pattern_of_glob_constr na c = | GApp (c, l) -> begin match DAst.get c with | GRef (ConstructRef cstr,_) -> - let nparams = Inductiveops.inductive_nparams (fst cstr) in + let nparams = Inductiveops.inductive_nparams env (fst cstr) in let _,l = List.chop nparams l in - PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + PatCstr (cstr,List.map (cases_pattern_of_glob_constr env Anonymous) l,na) | _ -> raise Not_found end | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous -> (* A canonical encoding of aliases *) - DAst.get (cases_pattern_of_glob_constr na' b) + DAst.get (cases_pattern_of_glob_constr env na' b) | _ -> raise Not_found ) c @@ -539,8 +539,8 @@ let drop_local_defs params decls args = | _ -> assert false in aux decls args -let add_patterns_for_params_remove_local_defs (ind,j) l = - let (mib,mip) = Global.lookup_inductive ind in +let add_patterns_for_params_remove_local_defs env (ind,j) l = + let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.Declarations.mind_nparams in let l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then @@ -556,12 +556,12 @@ let add_alias ?loc na c = | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id)) (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function +let rec glob_constr_of_cases_pattern_aux env isclosed x = DAst.map_with_loc (fun ?loc -> function | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None)) | PatCstr (cstr,l,na) -> let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in - let l = add_patterns_for_params_remove_local_defs cstr l in - add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l)) + let l = add_patterns_for_params_remove_local_defs env cstr l in + add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux env isclosed) l)) | PatVar (Name id) when not isclosed -> GVar id | PatVar Anonymous when not isclosed -> @@ -571,14 +571,14 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo | _ -> raise Not_found ) x -let glob_constr_of_closed_cases_pattern p = match DAst.get p with +let glob_constr_of_closed_cases_pattern env p = match DAst.get p with | PatCstr (cstr,l,na) -> let loc = p.CAst.loc in - na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) + na,glob_constr_of_cases_pattern_aux env true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found -let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p +let glob_constr_of_cases_pattern env p = glob_constr_of_cases_pattern_aux env false p (* This has to be in some file... *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 2f0ac76235..df902a8fa7 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -94,14 +94,15 @@ val map_pattern : (glob_constr -> glob_constr) -> Evaluation is forced. Take the current alias as parameter, @raise Not_found if translation is impossible *) -val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g +val cases_pattern_of_glob_constr : Environ.env -> Name.t -> 'a glob_constr_g -> 'a cases_pattern_g -val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g +val glob_constr_of_closed_cases_pattern : Environ.env -> 'a cases_pattern_g -> Name.t * 'a glob_constr_g (** A canonical encoding of cases pattern into constr such that composed with [cases_pattern_of_glob_constr Anonymous] gives identity *) -val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g +val glob_constr_of_cases_pattern : Environ.env -> 'a cases_pattern_g -> 'a glob_constr_g -val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list +val add_patterns_for_params_remove_local_defs : Environ.env -> constructor -> + 'a cases_pattern_g list -> 'a cases_pattern_g list val empty_lvar : Ltac_pretype.ltac_var_map diff --git a/pretyping/heads.ml b/pretyping/heads.ml index 7590ac301b..ef27ca9b4e 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -33,17 +33,16 @@ type head_approximation = | NotImmediatelyComputableHead (* FIXME: maybe change interface here *) -let rec compute_head = function +let rec compute_head env = function | EvalConstRef cst -> - let env = Global.env() in let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in (match body with | None -> RigidHead (RigidParameter cst) | Some c -> kind_of_head env c) | EvalVarRef id -> - (match Global.lookup_named id with + (match lookup_named id env with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> - kind_of_head (Global.env()) c + kind_of_head env c | _ -> RigidHead RigidOther) and kind_of_head env t = @@ -51,14 +50,14 @@ and kind_of_head env t = | Rel n when n > k -> NotImmediatelyComputableHead | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) | Var id -> - (try on_subterm k l b (compute_head (EvalVarRef id)) + (try on_subterm k l b (compute_head env (EvalVarRef id)) with Not_found -> (* a goal variable *) match lookup_named id env with | LocalDef (_,c,_) -> aux k l c b | LocalAssum _ -> NotImmediatelyComputableHead) | Const (cst,_) -> - (try on_subterm k l b (compute_head (EvalConstRef cst)) + (try on_subterm k l b (compute_head env (EvalConstRef cst)) with Not_found -> CErrors.anomaly Pp.(str "constant not found in kind_of_head: " ++ diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 4f940fa16a..7615a17514 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -610,16 +610,20 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s) (* Look up function for the default elimination constant *) -let lookup_eliminator ind_sp s = +let lookup_eliminator env ind_sp s = let kn,i = ind_sp in - let mp,l = KerName.repr (MutInd.canonical kn) in - let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in + let mpu = KerName.modpath @@ MutInd.user kn in + let mpc = KerName.modpath @@ MutInd.canonical kn in + let ind_id = (lookup_mind kn env).mind_packets.(i).mind_typename in let id = add_suffix ind_id (elimination_suffix s) in + let l = Label.of_id id in + let knu = KerName.make mpu l in + let knc = KerName.make mpc l in (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) try - let cst =Global.constant_of_delta_kn (KerName.make mp (Label.of_id id)) in - let _ = Global.lookup_constant cst in + let cst = Constant.make knu knc in + let _ = lookup_constant cst env in ConstRef cst with Not_found -> (* Then try to get a user-defined eliminator in some other places *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 91a5651f7f..8eb571a8be 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -62,7 +62,7 @@ val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> (** Recursor names utilities *) -val lookup_eliminator : inductive -> Sorts.family -> GlobRef.t +val lookup_eliminator : env -> inductive -> Sorts.family -> GlobRef.t val elimination_suffix : Sorts.family -> string val make_elimination_ident : Id.t -> Sorts.family -> Id.t diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 678aebfbe6..b1c98da2c7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -112,162 +112,145 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = (* Number of constructors *) -let nconstructors ind = - let (_,mip) = Global.lookup_inductive ind in - Array.length mip.mind_consnames - -let nconstructors_env env ind = +let nconstructors env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in Array.length mip.mind_consnames -(* Arity of constructors excluding parameters, excluding local defs *) +let nconstructors_env env ind = nconstructors env ind +[@@ocaml.deprecated "Alias for Inductiveops.nconstructors"] -let constructors_nrealargs ind = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_consnrealargs +(* Arity of constructors excluding parameters, excluding local defs *) -let constructors_nrealargs_env env ind = +let constructors_nrealargs env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealargs -(* Arity of constructors excluding parameters, including local defs *) +let constructors_nrealargs_env env ind = constructors_nrealargs env ind +[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"] -let constructors_nrealdecls ind = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_consnrealdecls +(* Arity of constructors excluding parameters, including local defs *) -let constructors_nrealdecls_env env ind = +let constructors_nrealdecls env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls +let constructors_nrealdecls_env env ind = constructors_nrealdecls env ind +[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"] + (* Arity of constructors including parameters, excluding local defs *) -let constructor_nallargs (indsp,j) = - let (mib,mip) = Global.lookup_inductive indsp in +let constructor_nallargs env (ind,j) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealargs.(j-1) + mib.mind_nparams -let constructor_nallargs_env env ((kn,i),j) = - let mib = Environ.lookup_mind kn env in - let mip = mib.mind_packets.(i) in - mip.mind_consnrealargs.(j-1) + mib.mind_nparams +let constructor_nallargs_env env (indsp,j) = constructor_nallargs env (indsp,j) +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"] (* Arity of constructors including params, including local defs *) -let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *) - let (mib,mip) = Global.lookup_inductive indsp in +let constructor_nalldecls env (ind,j) = (* TOCHANGE en decls *) + let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) -let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *) - let mib = Environ.lookup_mind kn env in - let mip = mib.mind_packets.(i) in - mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) +let constructor_nalldecls_env env (indsp,j) = constructor_nalldecls env (indsp,j) +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"] (* Arity of constructors excluding params, excluding local defs *) -let constructor_nrealargs (ind,j) = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_consnrealargs.(j-1) - -let constructor_nrealargs_env env (ind,j) = +let constructor_nrealargs env (ind,j) = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealargs.(j-1) -(* Arity of constructors excluding params, including local defs *) +let constructor_nrealargs_env env (ind,j) = constructor_nrealargs env (ind,j) +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"] -let constructor_nrealdecls (ind,j) = (* TOCHANGE en decls *) - let (_,mip) = Global.lookup_inductive ind in - mip.mind_consnrealdecls.(j-1) +(* Arity of constructors excluding params, including local defs *) -let constructor_nrealdecls_env env (ind,j) = (* TOCHANGE en decls *) +let constructor_nrealdecls env (ind,j) = (* TOCHANGE en decls *) let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls.(j-1) -(* Length of arity, excluding params, excluding local defs *) +let constructor_nrealdecls_env env (ind,j) = constructor_nrealdecls env (ind,j) +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] -let inductive_nrealargs ind = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_nrealargs +(* Length of arity, excluding params, excluding local defs *) -let inductive_nrealargs_env env ind = +let inductive_nrealargs env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_nrealargs -(* Length of arity, excluding params, including local defs *) +let inductive_nrealargs_env env ind = inductive_nrealargs env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"] -let inductive_nrealdecls ind = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_nrealdecls +(* Length of arity, excluding params, including local defs *) -let inductive_nrealdecls_env env ind = +let inductive_nrealdecls env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_nrealdecls -(* Full length of arity (w/o local defs) *) +let inductive_nrealdecls_env env ind = inductive_nrealdecls env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"] -let inductive_nallargs ind = - let (mib,mip) = Global.lookup_inductive ind in - mib.mind_nparams + mip.mind_nrealargs +(* Full length of arity (w/o local defs) *) -let inductive_nallargs_env env ind = +let inductive_nallargs env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in mib.mind_nparams + mip.mind_nrealargs -(* Length of arity (w/o local defs) *) +let inductive_nallargs_env env ind = inductive_nallargs env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"] -let inductive_nparams ind = - let (mib,mip) = Global.lookup_inductive ind in - mib.mind_nparams +(* Length of arity (w/o local defs) *) -let inductive_nparams_env env ind = +let inductive_nparams env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in mib.mind_nparams -(* Length of arity (with local defs) *) +let inductive_nparams_env env ind = inductive_nparams env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"] -let inductive_nparamdecls ind = - let (mib,mip) = Global.lookup_inductive ind in - Context.Rel.length mib.mind_params_ctxt +(* Length of arity (with local defs) *) -let inductive_nparamdecls_env env ind = +let inductive_nparamdecls env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in Context.Rel.length mib.mind_params_ctxt -(* Full length of arity (with local defs) *) +let inductive_nparamdecls_env env ind = inductive_nparamdecls env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"] -let inductive_nalldecls ind = - let (mib,mip) = Global.lookup_inductive ind in - Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls +(* Full length of arity (with local defs) *) -let inductive_nalldecls_env env ind = +let inductive_nalldecls env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls -(* Others *) +let inductive_nalldecls_env env ind = inductive_nalldecls env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"] -let inductive_paramdecls (ind,u) = - let (mib,mip) = Global.lookup_inductive ind in - Inductive.inductive_paramdecls (mib,u) +(* Others *) -let inductive_paramdecls_env env (ind,u) = +let inductive_paramdecls env (ind,u) = let (mib,mip) = Inductive.lookup_mind_specif env ind in Inductive.inductive_paramdecls (mib,u) -let inductive_alldecls (ind,u) = - let (mib,mip) = Global.lookup_inductive ind in - Vars.subst_instance_context u mip.mind_arity_ctxt +let inductive_paramdecls_env env (ind,u) = inductive_paramdecls env (ind,u) +[@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecls"] -let inductive_alldecls_env env (ind,u) = +let inductive_alldecls env (ind,u) = let (mib,mip) = Inductive.lookup_mind_specif env ind in Vars.subst_instance_context u mip.mind_arity_ctxt -let constructor_has_local_defs (indsp,j) = - let (mib,mip) = Global.lookup_inductive indsp in +let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u) +[@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] + +let constructor_has_local_defs env (indsp,j) = + let (mib,mip) = Inductive.lookup_mind_specif env indsp in let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in not (Int.equal l1 l2) -let inductive_has_local_defs ind = - let (mib,mip) = Global.lookup_inductive ind in +let inductive_has_local_defs env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in let l1 = Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls in let l2 = mib.mind_nparams + mip.mind_nrealargs in not (Int.equal l1 l2) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index c74bbfe98b..cfc650938e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -61,70 +61,85 @@ val mis_nf_constructor_type : (** {6 Extract information from an inductive name} *) (** @return number of constructors *) -val nconstructors : inductive -> int +val nconstructors : env -> inductive -> int val nconstructors_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.nconstructors"] (** @return arity of constructors excluding parameters, excluding local defs *) -val constructors_nrealargs : inductive -> int array +val constructors_nrealargs : env -> inductive -> int array val constructors_nrealargs_env : env -> inductive -> int array +[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"] (** @return arity of constructors excluding parameters, including local defs *) -val constructors_nrealdecls : inductive -> int array +val constructors_nrealdecls : env -> inductive -> int array val constructors_nrealdecls_env : env -> inductive -> int array +[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"] (** @return the arity, excluding params, excluding local defs *) -val inductive_nrealargs : inductive -> int +val inductive_nrealargs : env -> inductive -> int val inductive_nrealargs_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"] (** @return the arity, excluding params, including local defs *) -val inductive_nrealdecls : inductive -> int +val inductive_nrealdecls : env -> inductive -> int val inductive_nrealdecls_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"] (** @return the arity, including params, excluding local defs *) -val inductive_nallargs : inductive -> int +val inductive_nallargs : env -> inductive -> int val inductive_nallargs_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"] (** @return the arity, including params, including local defs *) -val inductive_nalldecls : inductive -> int +val inductive_nalldecls : env -> inductive -> int val inductive_nalldecls_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"] (** @return nb of params without local defs *) -val inductive_nparams : inductive -> int +val inductive_nparams : env -> inductive -> int val inductive_nparams_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"] (** @return nb of params with local defs *) -val inductive_nparamdecls : inductive -> int +val inductive_nparamdecls : env -> inductive -> int val inductive_nparamdecls_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"] (** @return params context *) -val inductive_paramdecls : pinductive -> Constr.rel_context +val inductive_paramdecls : env -> pinductive -> Constr.rel_context val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context +[@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecl"] (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> Constr.rel_context +val inductive_alldecls : env -> pinductive -> Constr.rel_context val inductive_alldecls_env : env -> pinductive -> Constr.rel_context +[@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] (** {7 Extract information from a constructor name} *) (** @return param + args without letin *) -val constructor_nallargs : constructor -> int +val constructor_nallargs : env -> constructor -> int val constructor_nallargs_env : env -> constructor -> int +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"] (** @return param + args with letin *) -val constructor_nalldecls : constructor -> int +val constructor_nalldecls : env -> constructor -> int val constructor_nalldecls_env : env -> constructor -> int +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"] (** @return args without letin *) -val constructor_nrealargs : constructor -> int +val constructor_nrealargs : env -> constructor -> int val constructor_nrealargs_env : env -> constructor -> int +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"] (** @return args with letin *) -val constructor_nrealdecls : constructor -> int +val constructor_nrealdecls : env -> constructor -> int val constructor_nrealdecls_env : env -> constructor -> int +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] (** Is there local defs in params or args ? *) -val constructor_has_local_defs : constructor -> bool -val inductive_has_local_defs : inductive -> bool +val constructor_has_local_defs : env -> constructor -> bool +val inductive_has_local_defs : env -> inductive -> bool val allowed_sorts : env -> inductive -> Sorts.family list diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 4e3c77cb1a..b29afd1fd2 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -280,66 +280,64 @@ let rec liftn_pattern k n = function let lift_pattern k = liftn_pattern k 1 -let rec subst_pattern subst pat = +let rec subst_pattern env sigma subst pat = match pat with | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else (match t with | None -> PRef ref' | Some t -> - let env = Global.env () in - let evd = Evd.from_env env in - pattern_of_constr env evd t.Univ.univ_abstracted_value) + pattern_of_constr env sigma t.Univ.univ_abstracted_value) | PVar _ | PEvar _ | PRel _ | PInt _ -> pat | PProj (p,c) -> let p' = Projection.map (subst_mind subst) p in - let c' = subst_pattern subst c in + let c' = subst_pattern env sigma subst c in if p' == p && c' == c then pat else PProj(p',c') | PApp (f,args) -> - let f' = subst_pattern subst f in - let args' = Array.Smart.map (subst_pattern subst) args in + let f' = subst_pattern env sigma subst f in + let args' = Array.Smart.map (subst_pattern env sigma subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.Smart.map (subst_pattern subst) args in + let args' = List.Smart.map (subst_pattern env sigma subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && c2' == c2 then pat else PLambda (name,c1',c2') | PProd (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && c2' == c2 then pat else PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> - let c1' = subst_pattern subst c1 in - let t' = Option.Smart.map (subst_pattern subst) t in - let c2' = subst_pattern subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let t' = Option.Smart.map (subst_pattern env sigma subst) t in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') | PSort _ | PMeta _ -> pat | PIf (c,c1,c2) -> - let c' = subst_pattern subst c in - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in + let c' = subst_pattern env sigma subst c in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c' == c && c1' == c1 && c2' == c2 then pat else PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in - let typ' = subst_pattern subst typ in - let c' = subst_pattern subst c in + let typ' = subst_pattern env sigma subst typ in + let c' = subst_pattern env sigma subst c in let subst_branch ((i,n,c) as br) = - let c' = subst_pattern subst c in + let c' = subst_pattern env sigma subst c in if c' == c then br else (i,n,c') in let branches' = List.Smart.map subst_branch branches in @@ -347,13 +345,13 @@ let rec subst_pattern subst pat = then pat else PCase(cip', typ', c', branches') | PFix (lni,(lna,tl,bl)) -> - let tl' = Array.Smart.map (subst_pattern subst) tl in - let bl' = Array.Smart.map (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in + let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in if bl' == bl && tl' == tl then pat else PFix (lni,(lna,tl',bl')) | PCoFix (ln,(lna,tl,bl)) -> - let tl' = Array.Smart.map (subst_pattern subst) tl in - let bl' = Array.Smart.map (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in + let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in if bl' == bl && tl' == tl then pat else PCoFix (ln,(lna,tl',bl')) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 36317b3acf..3821fbf1a0 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -21,7 +21,7 @@ val constr_pattern_eq : constr_pattern -> constr_pattern -> bool val occur_meta_pattern : constr_pattern -> bool -val subst_pattern : substitution -> constr_pattern -> constr_pattern +val subst_pattern : Environ.env -> Evd.evar_map -> substitution -> constr_pattern -> constr_pattern val noccurn_pattern : int -> constr_pattern -> bool diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a6e3cfe085..0f7676cd19 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -644,7 +644,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env | None -> [] | Some ty -> let ((ind, i), u) = destConstruct sigma fj.uj_val in - let npars = inductive_nparams ind in + let npars = inductive_nparams !!env ind in if Int.equal npars 0 then [] else try @@ -1146,7 +1146,7 @@ let understand_ltac flags env sigma lvar kind c = let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let path_convertible p q = +let path_convertible env sigma p q = let open Classops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in @@ -1171,13 +1171,12 @@ let path_convertible p q = | [] -> anomaly (str "A coercion path shouldn't be empty.") in try - let e = Global.env () in - let sigma,tp = understand_tcc e (Evd.from_env e) (path_to_gterm p) in - let sigma,tq = understand_tcc e sigma (path_to_gterm q) in + let sigma,tp = understand_tcc env sigma (path_to_gterm p) in + let sigma,tq = understand_tcc env sigma (path_to_gterm q) in if Evd.has_undefined sigma then false else - let _ = Evarconv.unify_delay e sigma tp tq in true + let _ = Evarconv.unify_delay env sigma tp tq in true with Evarconv.UnableToUnify _ | PretypeError _ -> false let _ = Classops.install_path_comparator path_convertible diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index ef56458f99..1feb8acd5f 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -21,7 +21,6 @@ open Pp open Names open Globnames open Constr -open Libobject open Mod_subst open Reductionops @@ -50,10 +49,10 @@ let projection_table = type struc_tuple = constructor * (Name.t * bool) list * Constant.t option list -let load_structure i (_, (id,kl,projs)) = +let register_structure env (id,kl,projs) = let open Declarations in let ind = fst id in - let mib, mip = Global.lookup_inductive ind in + let mib, mip = Inductive.lookup_mind_specif env ind in let n = mib.mind_nparams in let struc = { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in @@ -62,10 +61,7 @@ let load_structure i (_, (id,kl,projs)) = List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc)) projs !projection_table -let cache_structure o = - load_structure 1 o - -let subst_structure (subst, (id, kl, projs as obj)) = +let subst_structure subst (id, kl, projs as obj) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) @@ -77,19 +73,6 @@ let subst_structure (subst, (id, kl, projs as obj)) = if projs' == projs && id' == id then obj else (id',kl,projs') -let discharge_structure (_, x) = Some x - -let inStruc : struc_tuple -> obj = - declare_object {(default_object "STRUCTURE") with - cache_function = cache_structure; - load_function = load_structure; - subst_function = subst_structure; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_structure } - -let declare_structure o = - Lib.add_anonymous_leaf (inStruc o) - let lookup_structure indsp = Indmap.find indsp !structure_table let lookup_projections indsp = (lookup_structure indsp).s_PROJ @@ -107,26 +90,9 @@ let is_projection cst = Cmap.mem cst !projection_table let prim_table = Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs" -let load_prim i (_,(p,c)) = +let register_primitive_projection p c = prim_table := Cmap_env.add c p !prim_table -let cache_prim p = load_prim 1 p - -let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c - -let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) - -let inPrim : (Projection.Repr.t * Constant.t) -> obj = - declare_object { - (default_object "PRIMPROJS") with - cache_function = cache_prim ; - load_function = load_prim; - subst_function = subst_prim; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_prim } - -let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) - let is_primitive_projection c = Cmap_env.mem c !prim_table let find_primitive_projection c = @@ -224,7 +190,7 @@ let warn_projection_no_head_constant = ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) -let compute_canonical_projections env warn (con,ind) = +let compute_canonical_projections env ~warn (con,ind) = let ctx = Environ.constant_context env con in let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in @@ -274,11 +240,8 @@ let warn_redundant_canonical_projection = ++ strbrk " by " ++ prj ++ strbrk " in " ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) -let add_canonical_structure warn o = - (* XXX: Undesired global access to env *) - let env = Global.env () in - let sigma = Evd.from_env env in - compute_canonical_projections env warn o |> +let register_canonical_structure ~warn env sigma o = + compute_canonical_projections env ~warn o |> List.iter (fun ((proj, (cs_pat, _ as pat)), s) -> let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in match assoc_pat cs_pat l with @@ -294,31 +257,13 @@ let add_canonical_structure warn o = warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s) ) -let open_canonical_structure i (_, o) = - if Int.equal i 1 then add_canonical_structure false o - -let cache_canonical_structure (_, o) = - add_canonical_structure true o - -let subst_canonical_structure (subst,(cst,ind as obj)) = +let subst_canonical_structure subst (cst,ind as obj) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) let cst' = subst_constant subst cst in let ind' = subst_ind subst ind in if cst' == cst && ind' == ind then obj else (cst',ind') -let discharge_canonical_structure (_,x) = Some x - -let inCanonStruc : Constant.t * inductive -> obj = - declare_object {(default_object "CANONICAL-STRUCTURE") with - open_function = open_canonical_structure; - cache_function = cache_canonical_structure; - subst_function = subst_canonical_structure; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_canonical_structure } - -let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) - (*s High-level declaration of a canonical structure *) let error_not_structure ref description = @@ -327,20 +272,17 @@ let error_not_structure ref description = (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ description)) -let check_and_decompose_canonical_structure ref = +let check_and_decompose_canonical_structure env sigma ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in - let env = Global.env () in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref (str "Could not find its value in the global environment.") in - let env = Global.env () in - let evd = Evd.from_env env in - let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in + let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with | App (f,args) -> f,args @@ -353,15 +295,12 @@ let check_and_decompose_canonical_structure ref = try lookup_structure indsp with Not_found -> error_not_structure ref - (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in + (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (sp,indsp) -let declare_canonical_structure ref = - add_canonical_structure (check_and_decompose_canonical_structure ref) - let lookup_canonical_conversion (proj,pat) = assoc_pat pat (GlobRef.Map.find proj !object_table) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 53a33f6bab..f0594d513a 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -26,7 +26,8 @@ type struc_typ = { type struc_tuple = constructor * (Name.t * bool) list * Constant.t option list -val declare_structure : struc_tuple -> unit +val register_structure : Environ.env -> struc_tuple -> unit +val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple (** [lookup_structure isp] returns the struc_typ associated to the inductive path [isp] if it corresponds to a structure, otherwise @@ -47,7 +48,7 @@ val find_projection : GlobRef.t -> struc_typ val is_projection : Constant.t -> bool (** Sets up the mapping from constants to primitive projections *) -val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit +val register_primitive_projection : Projection.Repr.t -> Constant.t -> unit val is_primitive_projection : Constant.t -> bool @@ -80,8 +81,12 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co val pr_cs_pattern : cs_pattern -> Pp.t val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ -val declare_canonical_structure : GlobRef.t -> unit +val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> + Constant.t * inductive -> unit +val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> ((GlobRef.t * cs_pattern) * obj_typ) list + +val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 20120f4182..38e254a5b4 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -121,7 +121,7 @@ let retype ?(polyprop=true) sigma = Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in - let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in + let n = inductive_nrealdecls env (fst (fst (dest_ind_family indf))) in let t = betazetaevar_applist sigma n p realargs in (match EConstr.kind sigma (whd_all env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 1496712bbc..ee27aea93f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -17,11 +17,8 @@ open Vars open Evd open Util open Typeclasses_errors -open Libobject open Context.Rel.Declaration -module RelDecl = Context.Rel.Declaration -module NamedDecl = Context.Named.Declaration (*i*) (* Core typeclasses hints *) @@ -38,12 +35,6 @@ let get_typeclasses_unique_solutions = ~key:["Typeclasses";"Unique";"Solutions"] ~value:false -let (add_instance_hint, add_instance_hint_hook) = Hook.make () -let add_instance_hint id = Hook.get add_instance_hint id - -let (remove_instance_hint, remove_instance_hint_hook) = Hook.make () -let remove_instance_hint id = Hook.get remove_instance_hint id - let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make () let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c @@ -97,18 +88,6 @@ let instance_impl is = is.is_impl let hint_priority is = is.is_info.hint_priority -let new_instance cl info glob impl = - let global = - if glob then Some (Lib.sections_depth ()) - else None - in - if match global with Some n -> n>0 && isVarRef impl | _ -> false then - CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable."); - { is_class = cl.cl_impl; - is_info = info ; - is_global = global ; - is_impl = impl } - (* * states management *) @@ -122,11 +101,10 @@ let typeclass_univ_instance (cl, u) = { cl with cl_context = on_snd subst_ctx cl.cl_context; cl_props = subst_ctx cl.cl_props} -let class_info c = +let class_info env sigma c = try GlobRef.Map.find c !classes with Not_found -> - let env = Global.env() in - not_a_class env (Evd.from_env env) (EConstr.of_constr (printable_constr_of_global c)) + not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c)) let global_class_of_constr env sigma c = try let gr, u = Termops.global_of_constr sigma c in @@ -142,8 +120,8 @@ let dest_class_arity env sigma c = let rels, c = decompose_prod_assum sigma c in rels, dest_class_app env sigma c -let class_of_constr sigma c = - try Some (dest_class_arity (Global.env ()) sigma c) +let class_of_constr env sigma c = + try Some (dest_class_arity env sigma c) with e when CErrors.noncritical e -> None let is_class_constr sigma c = @@ -176,103 +154,9 @@ let rec is_maybe_class_type evd c = let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c)) -(* - * classes persistent object - *) - -let load_class (_, cl) = +let load_class cl = classes := GlobRef.Map.add cl.cl_impl cl !classes -let cache_class = load_class - -let subst_class (subst,cl) = - let do_subst_con c = Mod_subst.subst_constant subst c - and do_subst c = Mod_subst.subst_mps subst c - and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in - let do_subst_context (grs,ctx) = - List.Smart.map (Option.Smart.map do_subst_gr) grs, - do_subst_ctx ctx in - let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> - (x, y, Option.Smart.map do_subst_con z)) projs in - { cl_univs = cl.cl_univs; - cl_impl = do_subst_gr cl.cl_impl; - cl_context = do_subst_context cl.cl_context; - cl_props = do_subst_ctx cl.cl_props; - cl_projs = do_subst_projs cl.cl_projs; - cl_strict = cl.cl_strict; - cl_unique = cl.cl_unique } - -let discharge_class (_,cl) = - let repl = Lib.replacement_context () in - let rel_of_variable_context ctx = List.fold_right - ( fun (decl,_) (ctx', subst) -> - let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in - (decl' :: ctx', NamedDecl.get_id decl :: subst) - ) ctx ([], []) in - let discharge_rel_context (subst, usubst) n rel = - let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in - let fold decl (ctx, k) = - let map c = subst_univs_level_constr usubst (substn_vars k subst c) in - RelDecl.map_constr map decl :: ctx, succ k - in - let ctx, _ = List.fold_right fold rel ([], n) in - ctx - in - let abs_context cl = - match cl.cl_impl with - | VarRef _ | ConstructRef _ -> assert false - | ConstRef cst -> Lib.section_segment_of_constant cst - | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in - let discharge_context ctx' subst (grs, ctx) = - let grs' = - let newgrs = List.map (fun decl -> - match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with - | None -> None - | Some (_, ((tc,_), _)) -> Some tc.cl_impl) - ctx' - in - grs @ newgrs - in grs', discharge_rel_context subst 1 ctx @ ctx' in - try - let info = abs_context cl in - let ctx = info.Lib.abstr_ctx in - let ctx, subst = rel_of_variable_context ctx in - let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in - let context = discharge_context ctx (subst, usubst) cl.cl_context in - let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in - let discharge_proj x = x in - { cl_univs = cl_univs'; - cl_impl = cl.cl_impl; - cl_context = context; - cl_props = props; - cl_projs = List.Smart.map discharge_proj cl.cl_projs; - cl_strict = cl.cl_strict; - cl_unique = cl.cl_unique - } - with Not_found -> (* not defined in the current section *) - cl - -let rebuild_class cl = - try - let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in - set_typeclass_transparency cst false false; cl - with e when CErrors.noncritical e -> cl - -let class_input : typeclass -> obj = - declare_object - { (default_object "type classes state") with - cache_function = cache_class; - load_function = (fun _ -> load_class); - open_function = (fun _ -> load_class); - classify_function = (fun x -> Substitute x); - discharge_function = (fun a -> Some (discharge_class a)); - rebuild_function = rebuild_class; - subst_function = subst_class } - -let add_class cl = - Lib.add_anonymous_leaf (class_input cl) - (** Build the subinstances hints. *) let check_instance env sigma c = @@ -295,7 +179,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = let ty = EConstr.of_constr ty in let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let rec aux pri c ty path = - match class_of_constr sigma ty with + match class_of_constr env sigma ty with | None -> [] | Some (rels, ((tc,u), args)) -> let instapp = @@ -336,136 +220,23 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = aux pri term ty [glob] (* - * instances persistent object + * interface functions *) -type instance_action = - | AddInstance - | RemoveInstance - -let load_instance inst = - let insts = +let load_instance inst = + let insts = try GlobRef.Map.find inst.is_class !instances with Not_found -> GlobRef.Map.empty in let insts = GlobRef.Map.add inst.is_impl inst insts in instances := GlobRef.Map.add inst.is_class insts !instances let remove_instance inst = - let insts = + let insts = try GlobRef.Map.find inst.is_class !instances with Not_found -> assert false in let insts = GlobRef.Map.remove inst.is_impl insts in instances := GlobRef.Map.add inst.is_class insts !instances -let cache_instance (_, (action, i)) = - match action with - | AddInstance -> load_instance i - | RemoveInstance -> remove_instance i - -let subst_instance (subst, (action, inst)) = action, - { inst with - is_class = fst (subst_global subst inst.is_class); - is_impl = fst (subst_global subst inst.is_impl) } - -let discharge_instance (_, (action, inst)) = - match inst.is_global with - | None -> None - | Some n -> - assert (not (isVarRef inst.is_impl)); - Some (action, - { inst with - is_global = Some (pred n); - is_class = inst.is_class; - is_impl = inst.is_impl }) - - -let is_local i = (i.is_global == None) - -let is_local_for_hint i = - match i.is_global with - | None -> true (* i.e. either no Global keyword not in section, or in section *) - | Some n -> n <> 0 (* i.e. in a section, declare the hint as local - since discharge is managed by rebuild_instance which calls again - add_instance_hint; don't ask hints to take discharge into account - itself *) - -let add_instance check inst = - let poly = Global.is_polymorphic inst.is_impl in - let local = is_local_for_hint inst in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local - inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path - local pri poly) - (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) - (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) - -let rebuild_instance (action, inst) = - let () = match action with - | AddInstance -> add_instance true inst - | _ -> () - in - (action, inst) - -let classify_instance (action, inst) = - if is_local inst then Dispose - else Substitute (action, inst) - -let instance_input : instance_action * instance -> obj = - declare_object - { (default_object "type classes instances state") with - cache_function = cache_instance; - load_function = (fun _ x -> cache_instance x); - open_function = (fun _ x -> cache_instance x); - classify_function = classify_instance; - discharge_function = discharge_instance; - rebuild_function = rebuild_instance; - subst_function = subst_instance } - -let add_instance i = - Lib.add_anonymous_leaf (instance_input (AddInstance, i)); - add_instance true i - -let remove_instance i = - Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); - remove_instance_hint i.is_impl - -let warning_not_a_class = - let name = "not-a-class" in - let category = "typeclasses" in - CWarnings.create ~name ~category (fun (n, ty) -> - let env = Global.env () in - let evd = Evd.from_env env in - Pp.(str "Ignored instance declaration for “" - ++ Nametab.pr_global_env Id.Set.empty n - ++ str "”: “" - ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty) - ++ str "” is not a class") - ) - -let declare_instance ?(warn = false) info local glob = - let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in - let info = Option.default {hint_priority = None; hint_pattern = None} info in - match class_of_constr Evd.empty (EConstr.of_constr ty) with - | Some (rels, ((tc,_), args) as _cl) -> - assert (not (isVarRef glob) || local); - add_instance (new_instance tc info (not local) glob) - | None -> if warn then warning_not_a_class (glob, ty) - -let add_class cl = - add_class cl; - List.iter (fun (n, inst, body) -> - match inst with - | Some (Backward, info) -> - (match body with - | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") - | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b)) - | _ -> ()) - cl.cl_projs - - -(* - * interface functions - *) let instance_constructor (cl,u) args = let lenpars = List.count is_local_assum (snd cl.cl_context) in @@ -497,8 +268,8 @@ let all_instances () = GlobRef.Map.fold (fun k v acc -> v :: acc) v acc) !instances [] -let instances r = - let cl = class_info r in instances_of cl +let instances env sigma r = + let cl = class_info env sigma r in instances_of cl let is_class gr = GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index f8aedf88c2..e42b82c51f 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Constr open Evd open Environ @@ -54,19 +53,25 @@ type typeclass = { no backtracking and sharing of resolution. *) } -type instance +type instance = { + is_class: GlobRef.t; + is_info: hint_info; + (* Sections where the instance should be redeclared, + None for discard, Some 0 for none. *) + is_global: int option; + is_impl: GlobRef.t; +} -val instances : GlobRef.t -> instance list +val instances : env -> evar_map -> GlobRef.t -> instance list val typeclasses : unit -> typeclass list val all_instances : unit -> instance list -val add_class : typeclass -> unit +val load_class : typeclass -> unit -val new_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance -val add_instance : instance -> unit +val load_instance : instance -> unit val remove_instance : instance -> unit -val class_info : GlobRef.t -> typeclass (** raises a UserError if not a class *) +val class_info : env -> evar_map -> GlobRef.t -> typeclass (** raises a UserError if not a class *) (** These raise a UserError if not a class. @@ -78,7 +83,8 @@ val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.E val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass (** Just return None if not a class *) -val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option +val class_of_constr : env -> evar_map -> EConstr.constr -> + (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option val instance_impl : instance -> GlobRef.t @@ -122,23 +128,9 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t val classes_transparent_state : unit -> TransparentState.t -val add_instance_hint_hook : - (global_reference_or_constr -> GlobRef.t list -> - bool (* local? *) -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t -val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t -val add_instance_hint : global_reference_or_constr -> GlobRef.t list -> - bool -> hint_info -> Decl_kinds.polymorphic -> unit -val remove_instance_hint : GlobRef.t -> unit - val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -(** Declares the given global reference as an instance of its type. - Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — - when said type is not a registered type class. *) -val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit - - (** Build the subinstances hints for a given typeclass object. check tells if we should check for existence of the subinstances and add only the missing ones. *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 89f72c874b..be71f44a5e 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -198,7 +198,7 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = - let specif = Global.lookup_inductive (fst ind) in + let specif = lookup_mind_specif env (fst ind) in let sorts = elim_sorts specif in let pj = Retyping.get_judgment_of env sigma p in let _, s = splay_prod env sigma pj.uj_type in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8bf86e9ef6..9541ea5882 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -952,5 +952,6 @@ let print_all_instances () = let print_instances r = let env = Global.env () in - let inst = instances r in + let sigma = Evd.from_env env in + let inst = instances env sigma r in prlist_with_sep fnl (pr_instance env) inst diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index a28f4597cf..c1ac7d201a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -362,7 +362,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm try match hdc with | Some (hd,_) when only_classes -> - let cl = Typeclasses.class_info hd in + let cl = Typeclasses.class_info env sigma hd in if cl.cl_strict then Evarutil.undefined_evars_of_term sigma concl else Evar.Set.empty @@ -1052,7 +1052,7 @@ let error_unresolvable env comp evd = | Some s -> Evar.Set.mem ev s in let fold ev evi (found, accu) = - let ev_class = class_of_constr evd evi.evar_concl in + let ev_class = class_of_constr env evd evi.evar_concl in if not (Option.is_empty ev_class) && is_part ev then (* focus on one instance if only one was searched for *) if not found then (true, Some ev) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 3ff2e3852d..d9d3764b2a 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -67,17 +67,17 @@ let contradiction_context = let id = NamedDecl.get_id d in let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in - if is_empty_type sigma typ then + if is_empty_type env sigma typ then simplest_elim (mkVar id) else match EConstr.kind sigma typ with - | Prod (na,t,u) when is_empty_type sigma u -> - let is_unit_or_eq = match_with_unit_or_eq_type sigma t in + | Prod (na,t,u) when is_empty_type env sigma u -> + let is_unit_or_eq = match_with_unit_or_eq_type env sigma t in Tacticals.New.tclORELSE (match is_unit_or_eq with | Some _ -> let hd,args = decompose_app sigma t in let (ind,_ as indu) = destInd sigma hd in - let nparams = Inductiveops.inductive_nparams_env env ind in + let nparams = Inductiveops.inductive_nparams env ind in let params = Util.List.firstn nparams args in let p = applist ((mkConstructUi (indu,1)), params) in (* Checking on the fly that it type-checks *) @@ -103,7 +103,7 @@ let contradiction_context = let is_negation_of env sigma typ t = match EConstr.kind sigma (whd_all env sigma t) with | Prod (na,t,u) -> - is_empty_type sigma u && is_conv_leq env sigma typ t + is_empty_type env sigma u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) = @@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) = let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in - if is_empty_type sigma ccl then + if is_empty_type env sigma ccl then Tacticals.New.tclTHEN (elim false None cl None) (Tacticals.New.tclTRY assumption) diff --git a/tactics/elim.ml b/tactics/elim.ml index 003b069b6e..71ea0098a3 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -81,12 +81,13 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> let type_of = pf_unsafe_type_of gl in + let env = pf_env gl in let sigma = project gl in let typc = type_of c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId - (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma)) + (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma)) (fun id -> clear [id]))); exact_no_check c ] end @@ -105,17 +106,17 @@ let head_in indl t gl = let decompose_these c l = Proofview.Goal.enter begin fun gl -> let indl = List.map (fun x -> x, Univ.Instance.empty) l in - general_decompose (fun sigma (_,t) -> head_in indl t gl) c + general_decompose (fun env sigma (_,t) -> head_in indl t gl) c end let decompose_and c = general_decompose - (fun sigma (_,t) -> is_record sigma t) + (fun env sigma (_,t) -> is_record env sigma t) c let decompose_or c = general_decompose - (fun sigma (_,t) -> is_disjunction sigma t) + (fun env sigma (_,t) -> is_disjunction env sigma t) c let h_decompose l c = decompose_these c l diff --git a/tactics/equality.ml b/tactics/equality.ml index 412fbbfd1b..3d760f1c3d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot = match EConstr.kind sigma hdcncl with | Ind (ind_sp,u) -> let pr1 = - lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) + lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) in begin match lft2rgt, cls with | Some true, None @@ -446,7 +446,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in - match match_with_equality_type sigma t with + match match_with_equality_type env sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels) @@ -462,7 +462,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac Proofview.tclEVARMAP >>= fun sigma -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type sigma t' with + match match_with_equality_type env sigma t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c @@ -743,7 +743,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let hd2,args2 = whd_all_stack env sigma t2 in match (EConstr.kind sigma hd1, EConstr.kind sigma hd2) with | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_) - when Int.equal (List.length args1) (constructor_nallargs_env env sp1) + when Int.equal (List.length args1) (constructor_nallargs env sp1) -> let sorts' = Sorts.List.intersect sorts (allowed_sorts env (fst sp1)) @@ -751,7 +751,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = (* both sides are fully applied constructors, so either we descend, or we can discriminate here. *) if eq_constructor sp1 sp2 then - let nparams = inductive_nparams_env env ind1 in + let nparams = inductive_nparams env ind1 in let params1,rargs1 = List.chop nparams args1 in let _,rargs2 = List.chop nparams args2 in let (mib,mip) = lookup_mind_specif env ind1 in @@ -966,9 +966,10 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let gen_absurdity id = Proofview.Goal.enter begin fun gl -> + let env = pf_env gl in let sigma = project gl in let hyp_typ = pf_get_hyp_typ id gl in - if is_empty_type sigma hyp_typ + if is_empty_type env sigma hyp_typ then simplest_elim (mkVar id) else @@ -1066,7 +1067,7 @@ let onNegatedEquality with_evars tac = let ccl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in match EConstr.kind sigma (hnf_constr env sigma ccl) with - | Prod (_,t,u) when is_empty_type sigma u -> + | Prod (_,t,u) when is_empty_type env sigma u -> tclTHEN introf (onLastHypId (fun id -> onEquality with_evars tac (mkVar id,NoBindings))) diff --git a/tactics/hints.ml b/tactics/hints.ml index f49b1660b8..11a8816159 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1064,7 +1064,9 @@ let subst_autohint (subst, obj) = in let subst_hint (k,data as hint) = let k' = Option.Smart.map subst_key k in - let pat' = Option.Smart.map (subst_pattern subst) data.pat in + let env = Global.env () in + let sigma = Evd.from_env env in + let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with | Res_pf (c,t,ctx) -> @@ -1353,7 +1355,7 @@ let interp_hints poly = let ind = global_inductive_with_alias qid in let mib,_ = Global.lookup_inductive ind in Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; - List.init (nconstructors ind) + List.init (nconstructors env ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in empty_hint_info, @@ -1389,7 +1391,7 @@ let expand_constructor_hints env sigma lems = List.map_append (fun (evd,lem) -> match EConstr.kind sigma lem with | Ind (ind,u) -> - List.init (nconstructors ind) + List.init (nconstructors env ind) (fun i -> let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd) (Evd.universe_context_set sigma) in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 08131f6309..e1dad9ad20 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -34,44 +34,42 @@ module RelDecl = Context.Rel.Declaration -- Eduardo (6/8/97). *) -type 'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option +type 'a matching_function = Environ.env -> Evd.evar_map -> EConstr.constr -> 'a option -type testing_function = Evd.evar_map -> EConstr.constr -> bool +type testing_function = Environ.env -> Evd.evar_map -> EConstr.constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 -let op2bool = function Some _ -> true | None -> false - -let match_with_non_recursive_type sigma t = +let match_with_non_recursive_type env sigma t = match EConstr.kind sigma t with | App _ -> let (hdapp,args) = decompose_app sigma t in (match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then + if (Environ.lookup_mind (fst ind) env).mind_finite == CoFinite then Some (hdapp,args) else None | _ -> None) | _ -> None -let is_non_recursive_type sigma t = op2bool (match_with_non_recursive_type sigma t) +let is_non_recursive_type env sigma t = Option.has_some (match_with_non_recursive_type env sigma t) (* Test dependencies *) (* NB: we consider also the let-in case in the following function, since they may appear in types of inductive constructors (see #2629) *) -let rec has_nodep_prod_after n sigma c = +let rec has_nodep_prod_after n env sigma c = match EConstr.kind sigma c with | Prod (_,_,b) | LetIn (_,_,_,b) -> ( n>0 || Vars.noccurn sigma 1 b) - && (has_nodep_prod_after (n-1) sigma b) + && (has_nodep_prod_after (n-1) env sigma b) | _ -> true -let has_nodep_prod sigma c = has_nodep_prod_after 0 sigma c +let has_nodep_prod env sigma c = has_nodep_prod_after 0 env sigma c (* A general conjunctive type is a non-recursive with-no-indices inductive type with only one constructor and no dependencies between argument; @@ -96,11 +94,11 @@ let rec whd_beta_prod sigma c = match EConstr.kind sigma c with | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c) | _ -> c -let match_with_one_constructor sigma style onlybinary allow_rec t = +let match_with_one_constructor env sigma style onlybinary allow_rec t = let (hdapp,args) = decompose_app sigma t in let res = match EConstr.kind sigma hdapp with | Ind ind -> - let (mib,mip) = Global.lookup_inductive (fst ind) in + let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in if Int.equal (Array.length mip.mind_consnames) 1 && (allow_rec || not (mis_is_recursive (fst ind,mib,mip))) && (Int.equal mip.mind_nrealargs 0) @@ -125,7 +123,7 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = let ctyp = whd_beta_prod sigma (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in - if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then + if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then (* Record or non strict conjunction *) Some (hdapp,List.rev cargs) else @@ -138,20 +136,20 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = | Some (hdapp, [_; _]) -> res | _ -> None -let match_with_conjunction ?(strict=false) ?(onlybinary=false) sigma t = - match_with_one_constructor sigma (Some strict) onlybinary false t +let match_with_conjunction ?(strict=false) ?(onlybinary=false) env sigma t = + match_with_one_constructor env sigma (Some strict) onlybinary false t -let match_with_record sigma t = - match_with_one_constructor sigma None false false t +let match_with_record env sigma t = + match_with_one_constructor env sigma None false false t -let is_conjunction ?(strict=false) ?(onlybinary=false) sigma t = - op2bool (match_with_conjunction sigma ~strict ~onlybinary t) +let is_conjunction ?(strict=false) ?(onlybinary=false) env sigma t = + Option.has_some (match_with_conjunction env sigma ~strict ~onlybinary t) -let is_record sigma t = - op2bool (match_with_record sigma t) +let is_record env sigma t = + Option.has_some (match_with_record env sigma t) -let match_with_tuple sigma t = - let t = match_with_one_constructor sigma None false true t in +let match_with_tuple env sigma t = + let t = match_with_one_constructor env sigma None false true t in Option.map (fun (hd,l) -> let ind = destInd sigma hd in let ind = on_snd (fun u -> EInstance.kind sigma u) ind in @@ -159,8 +157,8 @@ let match_with_tuple sigma t = let isrec = mis_is_recursive (fst ind,mib,mip) in (hd,l,isrec)) t -let is_tuple sigma t = - op2bool (match_with_tuple sigma t) +let is_tuple env sigma t = + Option.has_some (match_with_tuple env sigma t) (* A general disjunction type is a non-recursive with-no-indices inductive type with of which all constructors have a single argument; @@ -175,11 +173,11 @@ let test_strict_disjunction (mib, mip) = in Array.for_all_i check 0 mip.mind_nf_lc -let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = +let match_with_disjunction ?(strict=false) ?(onlybinary=false) env sigma t = let (hdapp,args) = decompose_app sigma t in let res = match EConstr.kind sigma hdapp with | Ind (ind,u) -> - let car = constructors_nrealargs ind in + let car = constructors_nrealargs env ind in let (mib,mip) = Global.lookup_inductive ind in if Array.for_all (fun ar -> Int.equal ar 1) car && not (mis_is_recursive (ind,mib,mip)) @@ -205,31 +203,31 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = | Some (hdapp,[_; _]) -> res | _ -> None -let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t = - op2bool (match_with_disjunction ~strict ~onlybinary sigma t) +let is_disjunction ?(strict=false) ?(onlybinary=false) env sigma t = + Option.has_some (match_with_disjunction ~strict ~onlybinary env sigma t) (* An empty type is an inductive type, possible with indices, that has no constructors *) -let match_with_empty_type sigma t = +let match_with_empty_type env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind, _) -> - let (mib,mip) = Global.lookup_inductive ind in + let (mib,mip) = Inductive.lookup_mind_specif env ind in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 0 then Some hdapp else None | _ -> None -let is_empty_type sigma t = op2bool (match_with_empty_type sigma t) +let is_empty_type env sigma t = Option.has_some (match_with_empty_type env sigma t) (* This filters inductive types with one constructor with no arguments; Parameters and indices are allowed *) -let match_with_unit_or_eq_type sigma t = +let match_with_unit_or_eq_type env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind , _) -> - let (mib,mip) = Global.lookup_inductive ind in + let (mib,mip) = Inductive.lookup_mind_specif env ind in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then Some hdapp @@ -237,14 +235,14 @@ let match_with_unit_or_eq_type sigma t = None | _ -> None -let is_unit_or_eq_type sigma t = op2bool (match_with_unit_or_eq_type sigma t) +let is_unit_or_eq_type env sigma t = Option.has_some (match_with_unit_or_eq_type env sigma t) (* A unit type is an inductive type with no indices but possibly (useless) parameters, and that has no arguments in its unique constructor *) -let is_unit_type sigma t = - match match_with_conjunction sigma t with +let is_unit_type env sigma t = + match match_with_conjunction env sigma t with | Some (_,[]) -> true | _ -> false @@ -331,15 +329,16 @@ let match_with_equation env sigma t = let is_inductive_equality ind = let (mib,mip) = Global.lookup_inductive ind in let nconstr = Array.length mip.mind_consnames in - Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0 + let env = Global.env () in + Int.equal nconstr 1 && Int.equal (constructor_nrealargs env (ind,1)) 0 -let match_with_equality_type sigma t = +let match_with_equality_type env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args) | _ -> None -let is_equality_type sigma t = op2bool (match_with_equality_type sigma t) +let is_equality_type env sigma t = Option.has_some (match_with_equality_type env sigma t) (* Arrows/Implication/Negation *) @@ -353,39 +352,39 @@ let match_arrow_pattern env sigma t = assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) | _ -> anomaly (Pp.str "Incorrect pattern matching.") -let match_with_imp_term sigma c = +let match_with_imp_term env sigma c = match EConstr.kind sigma c with | Prod (_,a,b) when Vars.noccurn sigma 1 b -> Some (a,b) | _ -> None -let is_imp_term sigma c = op2bool (match_with_imp_term sigma c) +let is_imp_term env sigma c = Option.has_some (match_with_imp_term env sigma c) let match_with_nottype env sigma t = try let (arg,mind) = match_arrow_pattern env sigma t in - if is_empty_type sigma mind then Some (mind,arg) else None + if is_empty_type env sigma mind then Some (mind,arg) else None with PatternMatchingFailure -> None -let is_nottype env sigma t = op2bool (match_with_nottype env sigma t) +let is_nottype env sigma t = Option.has_some (match_with_nottype env sigma t) (* Forall *) -let match_with_forall_term sigma c= +let match_with_forall_term env sigma c = match EConstr.kind sigma c with | Prod (nam,a,b) -> Some (nam,a,b) | _ -> None -let is_forall_term sigma c = op2bool (match_with_forall_term sigma c) +let is_forall_term env sigma c = Option.has_some (match_with_forall_term env sigma c) -let match_with_nodep_ind sigma t = +let match_with_nodep_ind env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind, _) -> - let (mib,mip) = Global.lookup_inductive ind in + let (mib,mip) = Inductive.lookup_mind_specif env ind in if Array.length (mib.mind_packets)>1 then None else let nodep_constr (ctx, cty) = let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in - has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in + has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) env sigma c in if Array.for_all nodep_constr mip.mind_nf_lc then let params= if Int.equal mip.mind_nrealargs 0 then args else @@ -395,9 +394,9 @@ let match_with_nodep_ind sigma t = None | _ -> None -let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t) +let is_nodep_ind env sigma t = Option.has_some (match_with_nodep_ind env sigma t) -let match_with_sigma_type sigma t = +let match_with_sigma_type env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind, _) -> @@ -405,7 +404,7 @@ let match_with_sigma_type sigma t = if Int.equal (Array.length (mib.mind_packets)) 1 && (Int.equal mip.mind_nrealargs 0) && (Int.equal (Array.length mip.mind_consnames)1) - && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma + && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) env sigma (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx)) then (*allowing only 1 existential*) @@ -414,7 +413,7 @@ let match_with_sigma_type sigma t = None | _ -> None -let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t) +let is_sigma_type env sigma t = Option.has_some (match_with_sigma_type env sigma t) (***** Destructing patterns bound to some theory *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 741f6713e3..b8c3ddb0f0 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -43,8 +43,8 @@ open Coqlib also work on ad-hoc disjunctions introduced by the user. (Eduardo, 6/8/97). *) -type 'a matching_function = evar_map -> constr -> 'a option -type testing_function = evar_map -> constr -> bool +type 'a matching_function = Environ.env -> evar_map -> constr -> 'a option +type testing_function = Environ.env -> evar_map -> constr -> bool val match_with_non_recursive_type : (constr * constr list) matching_function val is_non_recursive_type : testing_function @@ -83,8 +83,8 @@ val is_inductive_equality : inductive -> bool val match_with_equality_type : (constr * constr list) matching_function val is_equality_type : testing_function -val match_with_nottype : Environ.env -> (constr * constr) matching_function -val is_nottype : Environ.env -> testing_function +val match_with_nottype : (constr * constr) matching_function +val is_nottype : testing_function val match_with_forall_term : (Name.t Context.binder_annot * constr * constr) matching_function val is_forall_term : testing_function diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index aabfae444e..447b908a1d 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -259,10 +259,12 @@ let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) let subst_red_expr subs = + let env = Global.env () in + let sigma = Evd.from_env env in Redops.map_red_expr_gen (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) - (Patternops.subst_pattern subs) + (Patternops.subst_pattern env sigma subs) let inReduction : bool * string * red_expr -> obj = declare_object diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ec8d4d0e14..dcd63fe760 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -704,7 +704,8 @@ module New = struct (* computing the case/elim combinators *) let gl_make_elim ind = begin fun gl -> - let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in + let env = Proofview.Goal.env gl in + let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in let (sigma, c) = pf_apply Evd.fresh_global gl gr in (sigma, c) end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 206f35c8ba..066b9c7794 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1432,7 +1432,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_elim with_evars clear_flag (c,lbindc) {elimindex = None; elimbody = (elim,NoBindings); - elimrename = Some (false, constructors_nrealdecls (fst mind))}) + elimrename = Some (false, constructors_nrealdecls env (fst mind))}) end let general_case_analysis with_evars clear_flag (c,lbindc as cx) = @@ -1455,7 +1455,8 @@ exception IsNonrec let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite let find_ind_eliminator ind s gl = - let gr = lookup_eliminator ind s in + let env = Proofview.Goal.env gl in + let gr = lookup_eliminator env ind s in Tacmach.New.pf_apply Evd.fresh_global gl gr let find_eliminator c gl = @@ -1463,7 +1464,7 @@ let find_eliminator c gl = if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in evd, {elimindex = None; elimbody = (c,NoBindings); - elimrename = Some (true, constructors_nrealdecls ind)} + elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)} let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE @@ -1609,9 +1610,9 @@ let descend_in_conjunctions avoid tac (err, info) c = let t = Retyping.get_type_of env sigma c in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in let sign,ccl = EConstr.decompose_prod_assum sigma t in - match match_with_tuple sigma ccl with + match match_with_tuple env sigma ccl with | Some (_,_,isrec) -> - let n = (constructors_nrealargs ind).(0) in + let n = (constructors_nrealargs env ind).(0) in let sort = Tacticals.New.elimination_sort_of_goal gl in let IndType (indf,_) = find_rectype env sigma ccl in let (_,inst), params = dest_ind_family indf in @@ -2299,7 +2300,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_all = Tacmach.New.pf_apply whd_all gl in let t = whd_all (type_of (mkVar id)) in - let eqtac, thin = match match_with_equality_type sigma t with + let eqtac, thin = match match_with_equality_type env sigma t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then let id' = destVar sigma lhs in @@ -4128,7 +4129,7 @@ let guess_elim isrec dep s hyp0 gl = let sigma, elimc = if isrec && not (is_nonrec mind) then - let gr = lookup_eliminator mind s in + let gr = lookup_eliminator env mind s in Evd.fresh_global env sigma gr else let u = EInstance.kind sigma u in @@ -4739,9 +4740,10 @@ let reflexivity_red allowred = (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match match_with_equality_type sigma concl with + match match_with_equality_type env sigma concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings end diff --git a/vernac/canonical.ml b/vernac/canonical.ml new file mode 100644 index 0000000000..92d5731f92 --- /dev/null +++ b/vernac/canonical.ml @@ -0,0 +1,39 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +open Names +open Libobject +open Recordops + +let open_canonical_structure i (_, o) = + let env = Global.env () in + let sigma = Evd.from_env env in + if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o + +let cache_canonical_structure (_, o) = + let env = Global.env () in + let sigma = Evd.from_env env in + register_canonical_structure ~warn:true env sigma o + +let discharge_canonical_structure (_,x) = Some x + +let inCanonStruc : Constant.t * inductive -> obj = + declare_object {(default_object "CANONICAL-STRUCTURE") with + open_function = open_canonical_structure; + cache_function = cache_canonical_structure; + subst_function = (fun (subst,c) -> subst_canonical_structure subst c); + classify_function = (fun x -> Substitute x); + discharge_function = discharge_canonical_structure } + +let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) + +let declare_canonical_structure ref = + let env = Global.env () in + let sigma = Evd.from_env env in + add_canonical_structure (check_and_decompose_canonical_structure env sigma ref) diff --git a/vernac/canonical.mli b/vernac/canonical.mli new file mode 100644 index 0000000000..5b223a0615 --- /dev/null +++ b/vernac/canonical.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +open Names + +val declare_canonical_structure : GlobRef.t -> unit diff --git a/vernac/class.ml b/vernac/class.ml index 0837beccee..f3a279eab1 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -23,6 +23,7 @@ open Classops open Declare open Globnames open Decl_kinds +open Libobject let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -230,6 +231,58 @@ let check_source = function | Some (CL_FUN as s) -> raise (CoercionError (ForbiddenSourceClass s)) | _ -> () +let cache_coercion (_,c) = + let env = Global.env () in + let sigma = Evd.from_env env in + Classops.declare_coercion env sigma c + +let open_coercion i o = + if Int.equal i 1 then + cache_coercion o + +let discharge_coercion (_, c) = + if c.coercion_local then None + else + let n = + try + let ins = Lib.section_instance c.coercion_type in + Array.length (snd ins) + with Not_found -> 0 + in + let nc = { c with + coercion_params = n + c.coercion_params; + coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; + } in + Some nc + +let classify_coercion obj = + if obj.coercion_local then Dispose else Substitute obj + +let inCoercion : coercion -> obj = + declare_object {(default_object "COERCION") with + open_function = open_coercion; + cache_function = cache_coercion; + subst_function = (fun (subst,c) -> subst_coercion subst c); + classify_function = classify_coercion; + discharge_function = discharge_coercion } + +let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = + let isproj = + match coef with + | ConstRef c -> Recordops.find_primitive_projection c + | _ -> None + in + let c = { + coercion_type = coef; + coercion_local = local; + coercion_is_id = isid; + coercion_is_proj = isproj; + coercion_source = cls; + coercion_target = clt; + coercion_params = ps; + } in + Lib.add_anonymous_leaf (inCoercion c) + (* nom de la fonction coercion strength de f diff --git a/vernac/classes.ml b/vernac/classes.ml index d61d324941..9f233a2551 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -22,8 +22,10 @@ open Constrintern open Constrexpr open Context.Rel.Declaration open Class_tactics +open Libobject module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (*i*) open Decl_kinds @@ -49,17 +51,224 @@ let classes_transparent_state () = with Not_found -> TransparentState.empty let () = - Hook.set Typeclasses.add_instance_hint_hook - (fun inst path local info poly -> + Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; + Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state + +let add_instance_hint inst path local info poly = let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) | IsGlobal gr -> Hints.IsGlobRef gr in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst'])) ()); - Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; - Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state + [info, poly, false, Hints.PathHints path, inst'])) () + +let is_local_for_hint i = + match i.is_global with + | None -> true (* i.e. either no Global keyword not in section, or in section *) + | Some n -> n <> 0 (* i.e. in a section, declare the hint as local + since discharge is managed by rebuild_instance which calls again + add_instance_hint; don't ask hints to take discharge into account + itself *) + +let add_instance check inst = + let poly = Global.is_polymorphic inst.is_impl in + let local = is_local_for_hint inst in + add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local + inst.is_info poly; + List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path + local pri poly) + (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) + (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) + +let mk_instance cl info glob impl = + let global = + if glob then Some (Lib.sections_depth ()) + else None + in + if match global with Some n -> n>0 && isVarRef impl | _ -> false then + CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable."); + { is_class = cl.cl_impl; + is_info = info ; + is_global = global ; + is_impl = impl } + +(* + * instances persistent object + *) +let cache_instance (_, i) = + load_instance i + +let subst_instance (subst, inst) = + { inst with + is_class = fst (subst_global subst inst.is_class); + is_impl = fst (subst_global subst inst.is_impl) } + +let discharge_instance (_, inst) = + match inst.is_global with + | None -> None + | Some n -> + assert (not (isVarRef inst.is_impl)); + Some + { inst with + is_global = Some (pred n); + is_class = inst.is_class; + is_impl = inst.is_impl } + +let is_local i = (i.is_global == None) + +let rebuild_instance inst = + add_instance true inst; + inst + +let classify_instance inst = + if is_local inst then Dispose + else Substitute inst + +let instance_input : instance -> obj = + declare_object + { (default_object "type classes instances state") with + cache_function = cache_instance; + load_function = (fun _ x -> cache_instance x); + open_function = (fun _ x -> cache_instance x); + classify_function = classify_instance; + discharge_function = discharge_instance; + rebuild_function = rebuild_instance; + subst_function = subst_instance } + +let add_instance i = + Lib.add_anonymous_leaf (instance_input i); + add_instance true i + +let warning_not_a_class = + let name = "not-a-class" in + let category = "typeclasses" in + CWarnings.create ~name ~category (fun (n, ty) -> + let env = Global.env () in + let evd = Evd.from_env env in + Pp.(str "Ignored instance declaration for “" + ++ Nametab.pr_global_env Id.Set.empty n + ++ str "”: “" + ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty) + ++ str "” is not a class") + ) + +let declare_instance ?(warn = false) env sigma info local glob = + let ty, _ = Typeops.type_of_global_in_context env glob in + let info = Option.default {hint_priority = None; hint_pattern = None} info in + match class_of_constr env sigma (EConstr.of_constr ty) with + | Some (rels, ((tc,_), args) as _cl) -> + assert (not (isVarRef glob) || local); + add_instance (mk_instance tc info (not local) glob) + | None -> if warn then warning_not_a_class (glob, ty) + +(* + * classes persistent object + *) + +let cache_class (_,c) = load_class c + +let subst_class (subst,cl) = + let do_subst_con c = Mod_subst.subst_constant subst c + and do_subst c = Mod_subst.subst_mps subst c + and do_subst_gr gr = fst (subst_global subst gr) in + let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in + let do_subst_context (grs,ctx) = + List.Smart.map (Option.Smart.map do_subst_gr) grs, + do_subst_ctx ctx in + let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> + (x, y, Option.Smart.map do_subst_con z)) projs in + { cl_univs = cl.cl_univs; + cl_impl = do_subst_gr cl.cl_impl; + cl_context = do_subst_context cl.cl_context; + cl_props = do_subst_ctx cl.cl_props; + cl_projs = do_subst_projs cl.cl_projs; + cl_strict = cl.cl_strict; + cl_unique = cl.cl_unique } + +let discharge_class (_,cl) = + let open CVars in + let repl = Lib.replacement_context () in + let rel_of_variable_context ctx = List.fold_right + ( fun (decl,_) (ctx', subst) -> + let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in + (decl' :: ctx', NamedDecl.get_id decl :: subst) + ) ctx ([], []) in + let discharge_rel_context (subst, usubst) n rel = + let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in + let fold decl (ctx, k) = + let map c = subst_univs_level_constr usubst (substn_vars k subst c) in + RelDecl.map_constr map decl :: ctx, succ k + in + let ctx, _ = List.fold_right fold rel ([], n) in + ctx + in + let abs_context cl = + match cl.cl_impl with + | VarRef _ | ConstructRef _ -> assert false + | ConstRef cst -> Lib.section_segment_of_constant cst + | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in + let discharge_context ctx' subst (grs, ctx) = + let env = Global.env () in + let sigma = Evd.from_env env in + let grs' = + let newgrs = List.map (fun decl -> + match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr env sigma with + | None -> None + | Some (_, ((tc,_), _)) -> Some tc.cl_impl) + ctx' + in + grs @ newgrs + in grs', discharge_rel_context subst 1 ctx @ ctx' in + try + let info = abs_context cl in + let ctx = info.Lib.abstr_ctx in + let ctx, subst = rel_of_variable_context ctx in + let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in + let context = discharge_context ctx (subst, usubst) cl.cl_context in + let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in + let discharge_proj x = x in + { cl_univs = cl_univs'; + cl_impl = cl.cl_impl; + cl_context = context; + cl_props = props; + cl_projs = List.Smart.map discharge_proj cl.cl_projs; + cl_strict = cl.cl_strict; + cl_unique = cl.cl_unique + } + with Not_found -> (* not defined in the current section *) + cl + +let rebuild_class cl = + try + let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in + set_typeclass_transparency cst false false; cl + with e when CErrors.noncritical e -> cl + +let class_input : typeclass -> obj = + declare_object + { (default_object "type classes state") with + cache_function = cache_class; + load_function = (fun _ -> cache_class); + open_function = (fun _ -> cache_class); + classify_function = (fun x -> Substitute x); + discharge_function = (fun a -> Some (discharge_class a)); + rebuild_function = rebuild_class; + subst_function = subst_class } + +let add_class cl = + Lib.add_anonymous_leaf (class_input cl) + +let add_class env sigma cl = + add_class cl; + List.iter (fun (n, inst, body) -> + match inst with + | Some (Backward, info) -> + (match body with + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") + | Some b -> declare_instance ~warn:true env sigma (Some info) false (ConstRef b)) + | _ -> ()) + cl.cl_projs let intern_info {hint_priority;hint_pattern} = let env = Global.env() in @@ -72,10 +281,12 @@ let existing_instance glob g info = let c = Nametab.global g in let info = Option.default Hints.empty_hint_info info in let info = intern_info info in - let instance, _ = Typeops.type_of_global_in_context (Global.env ()) c in + let env = Global.env() in + let sigma = Evd.from_env env in + let instance, _ = Typeops.type_of_global_in_context env c in let _, r = Term.decompose_prod_assum instance in - match class_of_constr Evd.empty (EConstr.of_constr r) with - | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c) + match class_of_constr env sigma (EConstr.of_constr r) with + | Some (_, ((tc,u), _)) -> add_instance (mk_instance tc info glob c) | None -> user_err ?loc:g.CAst.loc ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") @@ -111,7 +322,9 @@ let id_of_class cl = let instance_hook k info global imps ?hook cst = Impargs.maybe_declare_manual_implicits false cst imps; let info = intern_info info in - Typeclasses.declare_instance (Some info) (not global) cst; + let env = Global.env () in + let sigma = Evd.from_env env in + declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = @@ -154,7 +367,9 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr imps; let pri = intern_info pri in - Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) + let env = Global.env () in + let sigma = Evd.from_env env in + declare_instance env sigma (Some pri) (not global) (ConstRef cst) in let obls, constr, typ = match term with @@ -360,96 +575,3 @@ let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) interp_instance_context ~program_mode env ctx pl bk cl in do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid - -let named_of_rel_context l = - let open Vars in - let acc, ctx = - List.fold_right - (fun decl (subst, ctx) -> - let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in - let d = match decl with - | LocalAssum (_,t) -> id, None, substl subst t - | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in - (mkVar id :: subst, d :: ctx)) - l ([], []) - in ctx - -let context ~pstate poly l = - let env = Global.env() in - let sigma = Evd.from_env env in - let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in - (* Note, we must use the normalized evar from now on! *) - let sigma = Evd.minimize_universes sigma in - let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in - let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in - let ctx = - try named_of_rel_context fullctx - with e when CErrors.noncritical e -> - user_err Pp.(str "Anonymous variables not allowed in contexts.") - in - let univs = - match ctx with - | [] -> assert false - | [_] -> Evd.univ_entry ~poly sigma - | _::_::_ -> - if Lib.sections_are_opened () - then - (* More than 1 variable in a section: we can't associate - universes to any specific variable so we declare them - separately. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context poly uctx; - if poly then Polymorphic_entry ([||], Univ.UContext.empty) - else Monomorphic_entry Univ.ContextSet.empty - end - else if poly then - (* Multiple polymorphic axioms: they are all polymorphic the same way. *) - Evd.univ_entry ~poly sigma - else - (* Multiple monomorphic axioms: declare universes separately - to avoid redeclaring them. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context poly uctx; - Monomorphic_entry Univ.ContextSet.empty - end - in - let fn status (id, b, t) = - let b, t = Option.map (to_constr sigma) b, to_constr sigma t in - if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - (* Declare the universe context once *) - let decl = match b with - | None -> - (ParameterEntry (None,(t,univs),None), IsAssumption Logical) - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - (DefinitionEntry entry, IsAssumption Logical) - in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in - match class_of_constr sigma (of_constr t) with - | Some (rels, ((tc,_), args) as _cl) -> - add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst)); - status - (* declare_subclasses (ConstRef cst) cl *) - | None -> status - else - let test (x, _) = match x with - | ExplByPos (_, Some id') -> Id.equal id id' - | _ -> false - in - let impl = List.exists test impls in - let decl = (Discharge, poly, Definitional) in - let nstatus = match b with - | None -> - pi3 (ComAssumption.declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl - Declaremods.NoInline (CAst.make id)) - | Some b -> - let decl = (Discharge, poly, Definition) in - let entry = Declare.definition_entry ~univs ~types:t b in - let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in - Lib.sections_are_opened () || Lib.is_modtype_strict () - in - status && nstatus - in - List.fold_left fn true (List.rev ctx) diff --git a/vernac/classes.mli b/vernac/classes.mli index 73e4b024ef..e7f90ff306 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,6 +22,12 @@ val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a (** Instance declaration *) +val declare_instance : ?warn:bool -> env -> Evd.evar_map -> + hint_info option -> bool -> GlobRef.t -> unit +(** Declares the given global reference as an instance of its type. + Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — + when said type is not a registered type class. *) + val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) @@ -64,6 +70,12 @@ val declare_new_instance : Hints.hint_info_expr -> unit +(** {6 Low level interface used by Add Morphism, do not use } *) +val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance +val add_instance : instance -> unit + +val add_class : env -> Evd.evar_map -> typeclass -> unit + (** Setting opacity *) val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit @@ -71,13 +83,3 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u (** For generation on names based on classes only *) val id_of_class : typeclass -> Id.t - -(** Context command *) - -(** returns [false] if, for lack of section, it declares an assumption - (unless in a module type). *) -val context - : pstate:Proof_global.t option - -> Decl_kinds.polymorphic - -> local_binder_expr list - -> bool diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index d7bd64067b..3406b6276f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -22,6 +22,7 @@ open Decl_kinds open Pretyping open Entries +module RelDecl = Context.Rel.Declaration (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) let axiom_into_instance = ref false @@ -59,7 +60,9 @@ match local with in let r = VarRef ident in let () = maybe_declare_manual_implicits true r imps in - let () = Typeclasses.declare_instance None true r in + let env = Global.env () in + let sigma = Evd.from_env env in + let () = Classes.declare_instance env sigma None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true false in (r,Univ.Instance.empty,true) @@ -77,7 +80,9 @@ match local with let () = maybe_declare_manual_implicits false gr imps in let () = Declare.declare_univ_binders gr pl in let () = assumption_message ident in - let () = if do_instance then Typeclasses.declare_instance None false gr in + let env = Global.env () in + let sigma = Evd.from_env env in + let () = if do_instance then Classes.declare_instance env sigma None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = match ctx with | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx @@ -173,7 +178,7 @@ let do_assumptions ~pstate ~program_mode kind nl l = let ubinders = Evd.universe_binders sigma in pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in - let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in + let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs @@ -206,3 +211,94 @@ let do_primitive id prim typopt = in let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") + +let named_of_rel_context l = + let open EConstr.Vars in + let open RelDecl in + let acc, ctx = + List.fold_right + (fun decl (subst, ctx) -> + let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in + let d = match decl with + | LocalAssum (_,t) -> id, None, substl subst t + | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in + (EConstr.mkVar id :: subst, d :: ctx)) + l ([], []) + in ctx + +let context ~pstate poly l = + let env = Global.env() in + let sigma = Evd.from_env env in + let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in + (* Note, we must use the normalized evar from now on! *) + let sigma = Evd.minimize_universes sigma in + let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in + let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in + let ctx = + try named_of_rel_context fullctx + with e when CErrors.noncritical e -> + user_err Pp.(str "Anonymous variables not allowed in contexts.") + in + let univs = + match ctx with + | [] -> assert false + | [_] -> Evd.univ_entry ~poly sigma + | _::_::_ -> + if Lib.sections_are_opened () + then + (* More than 1 variable in a section: we can't associate + universes to any specific variable so we declare them + separately. *) + begin + let uctx = Evd.universe_context_set sigma in + Declare.declare_universe_context poly uctx; + if poly then Polymorphic_entry ([||], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty + end + else if poly then + (* Multiple polymorphic axioms: they are all polymorphic the same way. *) + Evd.univ_entry ~poly sigma + else + (* Multiple monomorphic axioms: declare universes separately + to avoid redeclaring them. *) + begin + let uctx = Evd.universe_context_set sigma in + Declare.declare_universe_context poly uctx; + Monomorphic_entry Univ.ContextSet.empty + end + in + let fn status (id, b, t) = + let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in + if Lib.is_modtype () && not (Lib.sections_are_opened ()) then + (* Declare the universe context once *) + let decl = match b with + | None -> + (ParameterEntry (None,(t,univs),None), IsAssumption Logical) + | Some b -> + let entry = Declare.definition_entry ~univs ~types:t b in + (DefinitionEntry entry, IsAssumption Logical) + in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in + let env = Global.env () in + Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst); + status + else + let test (x, _) = match x with + | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id' + | _ -> false + in + let impl = List.exists test impls in + let decl = (Discharge, poly, Definitional) in + let nstatus = match b with + | None -> + pi3 (declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl + Declaremods.NoInline (CAst.make id)) + | Some b -> + let decl = (Discharge, poly, Definition) in + let entry = Declare.definition_entry ~univs ~types:t b in + let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in + Lib.sections_are_opened () || Lib.is_modtype_strict () + in + status && nstatus + in + List.fold_left fn true (List.rev ctx) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 32914cc11b..7c64317b70 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -9,8 +9,6 @@ (************************************************************************) open Names -open Constr -open Entries open Vernacexpr open Constrexpr open Decl_kinds @@ -25,19 +23,13 @@ val do_assumptions -> (ident_decl list * constr_expr) with_coercion list -> bool -(************************************************************************) -(** Internal API *) -(************************************************************************) - -(** Exported for Classes *) - (** returns [false] if the assumption is neither local to a section, nor in a module type and meant to be instantiated. *) val declare_assumption : pstate:Proof_global.t option -> coercion_flag -> assumption_kind - -> types in_universes_entry + -> Constr.types Entries.in_universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) @@ -45,4 +37,14 @@ val declare_assumption -> variable CAst.t -> GlobRef.t * Univ.Instance.t * bool +(** Context command *) + +(** returns [false] if, for lack of section, it declares an assumption + (unless in a module type). *) +val context + : pstate:Proof_global.t option + -> Decl_kinds.polymorphic + -> local_binder_expr list + -> bool + val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit diff --git a/vernac/himsg.ml b/vernac/himsg.ml index d329b81341..082b22b373 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -601,7 +601,7 @@ let rec explain_evar_kind env sigma evk ty = (pr_leconstr_env env sigma ty') src let explain_typeclass_resolution env sigma evi k = - match Typeclasses.class_of_constr sigma evi.evar_concl with + match Typeclasses.class_of_constr env sigma evi.evar_concl with | Some _ -> let env = Evd.evar_filtered_env evi in fnl () ++ str "Could not find an instance for " ++ @@ -614,7 +614,7 @@ let explain_placeholder_kind env sigma c e = | Some (SeveralInstancesFound n) -> strbrk " (several distinct possible type class instances found)" | None -> - match Typeclasses.class_of_constr sigma c with + match Typeclasses.class_of_constr env sigma c with | Some _ -> strbrk " (no type class instance found)" | _ -> mt () diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 1e733acc59..642695bda4 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -313,7 +313,9 @@ let warn_cannot_build_congruence = strbrk "Cannot build congruence scheme because eq is not found") let declare_congr_scheme ind = - if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin + let env = Global.env () in + let sigma = Evd.from_env env in + if Hipattern.is_equality_type env sigma (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true with e when CErrors.noncritical e -> false diff --git a/vernac/record.ml b/vernac/record.ml index cb67548667..74e5a03659 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -30,6 +30,7 @@ open Constrexpr open Constrexpr_ops open Goptions open Context.Rel.Declaration +open Libobject module RelDecl = Context.Rel.Declaration @@ -373,6 +374,27 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f open Typeclasses +let load_structure i (_, structure) = + Recordops.register_structure (Global.env()) structure + +let cache_structure o = + load_structure 1 o + +let subst_structure (subst, (id, kl, projs as obj)) = + Recordops.subst_structure subst obj + +let discharge_structure (_, x) = Some x + +let inStruc : Recordops.struc_tuple -> obj = + declare_object {(default_object "STRUCTURE") with + cache_function = cache_structure; + load_function = load_structure; + subst_function = subst_structure; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_structure } + +let declare_structure_entry o = + Lib.add_anonymous_leaf (inStruc o) let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = let nparams = List.length params in @@ -443,7 +465,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in - let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in + let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in rsp in List.mapi map record_data @@ -520,8 +542,10 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity List.map map inds in let ctx_context = + let env = Global.env () in + let sigma = Evd.from_env env in List.map (fun decl -> - match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with + match Typeclasses.class_of_constr env sigma (EConstr.of_constr (RelDecl.get_type decl)) with | Some (_, ((cl,_), _)) -> Some cl.cl_impl | None -> None) params, params @@ -548,12 +572,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity cl_props = fields; cl_projs = projs } in - add_class k; impl + let env = Global.env () in + let sigma = Evd.from_env env in + Classes.add_class env sigma k; impl in List.map map data -let add_constant_class env cst = +let add_constant_class env sigma cst = let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in let r = (Environ.lookup_constant cst env).const_relevance in let ctx, arity = decompose_prod_assum ty in @@ -566,10 +592,11 @@ let add_constant_class env cst = cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique } - in add_class tc; + in + Classes.add_class env sigma tc; set_typeclass_transparency (EvalConstRef cst) false false - -let add_inductive_class env ind = + +let add_inductive_class env sigma ind = let mind, oneind = Inductive.lookup_mind_specif env ind in let k = let ctx = oneind.mind_arity_ctxt in @@ -586,7 +613,8 @@ let add_inductive_class env ind = cl_projs = []; cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique } - in add_class k + in + Classes.add_class env sigma k let warn_already_existing_class = CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g -> @@ -594,11 +622,12 @@ let warn_already_existing_class = let declare_existing_class g = let env = Global.env () in + let sigma = Evd.from_env env in if Typeclasses.is_class g then warn_already_existing_class g else match g with - | ConstRef x -> add_constant_class env x - | IndRef x -> add_inductive_class env x + | ConstRef x -> add_constant_class env sigma x + | IndRef x -> add_inductive_class env sigma x | _ -> user_err ~hdr:"declare_existing_class" (Pp.str"Unsupported class type, only constants and inductives are allowed") diff --git a/vernac/record.mli b/vernac/record.mli index 9852840d12..12a2a765b5 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -24,6 +24,8 @@ val declare_projections : Constr.rel_context -> (Name.t * bool) list * Constant.t option list +val declare_structure_entry : Recordops.struc_tuple -> unit + val definition_structure : universe_decl_expr option -> inductive_kind -> template:bool option -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index ce93a8baaf..7f5c265eea 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -12,6 +12,7 @@ Vernacextend Ppvernac Proof_using Lemmas +Canonical Class Egramcoq Metasyntax @@ -21,11 +22,11 @@ Indschemes DeclareDef Obligations ComDefinition +Classes ComAssumption ComInductive ComFixpoint ComProgramFixpoint -Classes Record Assumptions Vernacstate diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index de8cdaa633..6c24b9ec75 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -572,7 +572,7 @@ let vernac_definition_hook p = function | Coercion -> Some (Class.add_coercion_hook p) | CanonicalStructure -> - Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure)) + Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure)) | SubClass -> Some (Class.add_subclass_hook p) | _ -> None @@ -1041,7 +1041,7 @@ let vernac_require from import qidl = (* Coercions and canonical structures *) let vernac_canonical r = - Recordops.declare_canonical_structure (smart_global r) + Canonical.declare_canonical_structure (smart_global r) let vernac_coercion ~atts ref qids qidt = let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in @@ -1075,7 +1075,7 @@ let vernac_declare_instance ~atts sup inst pri = Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri let vernac_context ~pstate ~poly l = - if not (Classes.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom + if not (ComAssumption.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom let vernac_existing_instance ~section_local insts = let glob = not section_local in |