From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- vernac/assumptions.ml | 6 +++--- vernac/assumptions.mli | 4 ++-- vernac/auto_ind_decl.ml | 3 ++- vernac/class.ml | 3 ++- vernac/classes.ml | 1 + vernac/classes.mli | 2 +- vernac/command.ml | 5 +++-- vernac/command.mli | 2 +- vernac/declareDef.mli | 2 +- vernac/indschemes.ml | 3 ++- vernac/indschemes.mli | 2 +- vernac/lemmas.ml | 9 +++++---- vernac/lemmas.mli | 2 +- vernac/obligations.ml | 33 +++++++++++++++++---------------- vernac/obligations.mli | 12 ++++++------ vernac/record.ml | 5 +++-- vernac/record.mli | 2 +- vernac/search.ml | 2 +- vernac/search.mli | 2 +- 19 files changed, 54 insertions(+), 46 deletions(-) (limited to 'vernac') diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 09e645eea..d22024568 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -18,7 +18,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Declarations open Mod_subst open Globnames @@ -163,7 +163,7 @@ let label_of = function let fold_constr_with_full_binders g f n acc c = let open Context.Rel.Declaration in - match kind_of_term c with + match Constr.kind c with | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc | Cast (c,_, t) -> f n (f n acc c) t | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c @@ -182,7 +182,7 @@ let fold_constr_with_full_binders g f n acc c = let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd -let rec traverse current ctx accu t = match kind_of_term t with +let rec traverse current ctx accu t = match Constr.kind t with | Var id -> let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 77eb968d4..afe932ead 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Globnames open Printer @@ -28,4 +28,4 @@ val traverse : {!traverse} also applies. *) val assumptions : ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> - global_reference -> constr -> Term.types ContextObjectMap.t + global_reference -> constr -> types ContextObjectMap.t diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 539e5550f..3cf181441 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -13,6 +13,7 @@ open CErrors open Util open Pp open Term +open Constr open Vars open Termops open Declarations @@ -532,7 +533,7 @@ let eqI ind l = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff with Not_found -> user_err ~hdr:"AutoIndDecl.eqI" (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed."); - in (if Array.equal Term.eq_constr eA [||] then e else mkApp(e,eA)), eff + in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) (* Boolean->Leibniz *) diff --git a/vernac/class.ml b/vernac/class.ml index 061f3efcc..f26599973 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -11,6 +11,7 @@ open Util open Pp open Names open Term +open Constr open Vars open Termops open Entries @@ -148,7 +149,7 @@ let get_target t ind = let prods_of t = - let rec aux acc d = match kind_of_term d with + let rec aux acc d = match Constr.kind d with | Prod (_,c1,c2) -> aux (c1::acc) c2 | Cast (c,_,_) -> aux acc c | _ -> (d,acc) diff --git a/vernac/classes.ml b/vernac/classes.ml index 9a8fc9bc2..22117f7e1 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -9,6 +9,7 @@ (*i*) open Names open Term +open Constr open Vars open Environ open Nametab diff --git a/vernac/classes.mli b/vernac/classes.mli index fcdb5c3bc..c0f03227c 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -34,7 +34,7 @@ val declare_instance_constant : bool -> (* polymorphic *) Evd.evar_map -> (* Universes *) Constr.t -> (** body *) - Term.types -> (** type *) + Constr.types -> (** type *) Names.Id.t val new_instance : diff --git a/vernac/command.ml b/vernac/command.ml index f58ed065c..db3fa1955 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -10,6 +10,7 @@ open Pp open CErrors open Util open Term +open Constr open Vars open Termops open Environ @@ -44,7 +45,7 @@ let do_constraint poly l = Declare.do_constraint poly l let rec under_binders env sigma f n c = if Int.equal n 0 then f env sigma (EConstr.of_constr c) else - match kind_of_term c with + match Constr.kind c with | Lambda (x,t,c) -> mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c) | LetIn (x,b,t,c) -> @@ -652,7 +653,7 @@ let extract_mutual_inductive_declaration_components indl = let is_recursive mie = let rec is_recursive_constructor lift typ = - match Term.kind_of_term typ with + match Constr.kind typ with | Prod (_,arg,rest) -> not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) || is_recursive_constructor (lift+1) rest diff --git a/vernac/command.mli b/vernac/command.mli index 26b1d1aaf..5415d3308 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Entries open Libnames open Globnames diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 5dea0ba27..01a87818a 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -15,5 +15,5 @@ val declare_definition : Id.t -> definition_kind -> Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> +val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t -> Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 4bdc93a36..c0ddc7e2c 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -21,6 +21,7 @@ open Names open Declarations open Entries open Term +open Constr open Inductive open Decl_kinds open Indrec @@ -458,7 +459,7 @@ let build_combined_scheme env schemes = let find_inductive ty = let (ctx, arity) = decompose_prod ty in let (_, last) = List.hd ctx in - match kind_of_term last with + match Constr.kind last with | App (ind, args) -> let ind = destInd ind in let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index 659f12936..4b31389ab 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -8,7 +8,7 @@ open Loc open Names -open Term +open Constr open Environ open Vernacexpr diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 22f0d199c..be9de5b30 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -14,6 +14,7 @@ open Util open Pp open Names open Term +open Constr open Declarations open Declareops open Entries @@ -62,7 +63,7 @@ let adjust_guardness_conditions const = function { const with const_entry_body = Future.chain const.const_entry_body (fun ((body, ctx), eff) -> - match kind_of_term body with + match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> (* let possible_indexes = List.map2 (fun i c -> match i with Some i -> i | None -> @@ -97,7 +98,7 @@ let find_mutually_recursive_statements thms = let ind_hyps = List.flatten (List.map_i (fun i decl -> let t = RelDecl.get_type decl in - match kind_of_term t with + match Constr.kind t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in mind.mind_finite <> Decl_kinds.CoFinite -> @@ -107,7 +108,7 @@ let find_mutually_recursive_statements thms = let ind_ccl = let cclenv = push_rel_context hyps (Global.env()) in let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in - match kind_of_term (EConstr.Unsafe.to_constr whnf_ccl) with + match Constr.kind (EConstr.Unsafe.to_constr whnf_ccl) with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> @@ -246,7 +247,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t | Some body -> let body = norm body in let k = Kindops.logical_kind_of_goal_kind kind in - let rec body_i t = match kind_of_term t with + let rec body_i t = match Constr.kind t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 1e23c7314..1f46a385d 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Decl_kinds type 'a declaration_hook diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 785c842ba..e23146273 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -13,6 +13,7 @@ open Declare *) open Term +open Constr open Vars open Names open Evd @@ -55,7 +56,7 @@ let subst_evar_constr evs n idf t = let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in - let rec substrec (depth, fixrels) c = match kind_of_term c with + let rec substrec (depth, fixrels) c = match Constr.kind c with | Evar (k, args) -> let { ev_name = (id, idstr) ; ev_hyps = hyps ; ev_chop = chop } = @@ -85,15 +86,15 @@ let subst_evar_constr evs n idf t = in aux hyps args [] in if List.exists - (fun x -> match kind_of_term x with + (fun x -> match Constr.kind x with | Rel n -> Int.List.mem n fixrels | _ -> false) args then transparent := Id.Set.add idstr !transparent; mkApp (idf idstr, Array.of_list args) | Fix _ -> - map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c - | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c + Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c + | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c in let t' = substrec (0, []) t in t', !seen, !transparent @@ -103,9 +104,9 @@ let subst_evar_constr evs n idf t = where n binders were passed through. *) let subst_vars acc n t = let var_index id = Util.List.index Id.equal id acc in - let rec substrec depth c = match kind_of_term c with + let rec substrec depth c = match Constr.kind c with | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) - | _ -> map_constr_with_binders succ substrec depth c + | _ -> Constr.map_with_binders succ substrec depth c in substrec 0 t @@ -144,7 +145,7 @@ let rec chop_product n t = let pop t = Vars.lift (-1) t in if Int.equal n 0 then Some t else - match kind_of_term t with + match Constr.kind t with | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None | _ -> None @@ -273,7 +274,7 @@ let explain_no_obligations = function | None -> str "No obligations remaining" type obligation_info = - (Names.Id.t * Term.types * Evar_kinds.t Loc.located * + (Names.Id.t * types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array @@ -384,7 +385,7 @@ let subst_deps expand obls deps t = (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let rec prod_app t n = - match kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with + match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> @@ -400,13 +401,13 @@ let replace_appvars subst = let f, l = decompose_app c in if isVar f then try - let c' = List.map (map_constr aux) l in + let c' = List.map (Constr.map aux) l in let (t, b) = Id.List.assoc (destVar f) subst in mkApp (delayed_force hide_obligation, [| prod_applist t c'; applistc b c' |]) - with Not_found -> map_constr aux c - else map_constr aux c - in map_constr aux + with Not_found -> Constr.map aux c + else Constr.map aux c + in Constr.map aux let subst_prog expand obls ints prg = let subst = obl_substitution expand obls ints in @@ -490,7 +491,7 @@ let declare_definition prg = cst let rec lam_index n t acc = - match kind_of_term t with + match Constr.kind t with | Lambda (Name n', _, _) when Id.equal n n' -> acc | Lambda (_, _, b) -> @@ -566,9 +567,9 @@ let declare_mutual_definition l = let decompose_lam_prod c ty = let open Context.Rel.Declaration in let rec aux ctx c ty = - match kind_of_term c, kind_of_term ty with + match Constr.kind c, Constr.kind ty with | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when eq_constr b b' && eq_constr t t' -> + when Constr.equal b b' && Constr.equal t t' -> let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in aux ctx' c ty | _, LetIn (x', b', t', ty) -> diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 11c2553ae..d037fdcd8 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -7,7 +7,7 @@ (************************************************************************) open Environ -open Term +open Constr open Evd open Names open Globnames @@ -39,7 +39,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int -> translation from obligation identifiers to constrs, new term, new type *) type obligation_info = - (Id.t * Term.types * Evar_kinds.t Loc.located * + (Id.t * types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array (* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) @@ -51,13 +51,13 @@ type progress = (* Resolution status of a program *) val default_tactic : unit Proofview.tactic ref -val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> +val add_definition : Names.Id.t -> ?term:constr -> types -> Evd.evar_universe_context -> ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> - ?reduce:(Term.constr -> Term.constr) -> + ?reduce:(constr -> constr) -> ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = @@ -68,13 +68,13 @@ type fixpoint_kind = | IsCoFixpoint val add_mutual_definitions : - (Names.Id.t * Term.constr * Term.types * + (Names.Id.t * constr * types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> Evd.evar_universe_context -> ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> - ?reduce:(Term.constr -> Term.constr) -> + ?reduce:(constr -> constr) -> ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> notations -> fixpoint_kind -> unit diff --git a/vernac/record.ml b/vernac/record.ml index 5533fe5b3..1fd43624a 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -13,6 +13,7 @@ open Names open Globnames open Nameops open Term +open Constr open Vars open Environ open Declarations @@ -229,7 +230,7 @@ exception NotDefinable of record_error let subst_projection fid l c = let lv = List.length l in let bad_projs = ref [] in - let rec substrec depth c = match kind_of_term c with + let rec substrec depth c = match Constr.kind c with | Rel k -> (* We are in context [[params;fields;x:ind;...depth...]] *) if k <= depth+1 then @@ -244,7 +245,7 @@ let subst_projection fid l c = " field which has no name.") else mkRel (k-lv) - | _ -> map_constr_with_binders succ substrec depth c + | _ -> Constr.map_with_binders succ substrec depth c in let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *) let c'' = substrec 0 c' in diff --git a/vernac/record.mli b/vernac/record.mli index 1bcbf39b7..33c2fba89 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Vernacexpr open Constrexpr open Impargs diff --git a/vernac/search.ml b/vernac/search.ml index 0f56f81e7..6da6a0c2d 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -9,7 +9,7 @@ open Pp open Util open Names -open Term +open Constr open Declarations open Libobject open Environ diff --git a/vernac/search.mli b/vernac/search.mli index db54d732b..2eda3980a 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Pattern open Globnames -- cgit v1.2.3