diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-08 10:00:21 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 11:45:08 +0100 |
| commit | 9d991d36c07efbb6428e277573bd43f6d56788fc (patch) | |
| tree | 5e5578043c9a3bc1c259260e5074b228e68f6c1a | |
| parent | edc16686634e0700a46b79ba340ca0aac49afb0e (diff) | |
CLEANUP: kernel/context.ml{,i}
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
109 files changed, 959 insertions, 830 deletions
diff --git a/.gitignore b/.gitignore index 0466eac85..5c932ad02 100644 --- a/.gitignore +++ b/.gitignore @@ -98,6 +98,8 @@ doc/RecTutorial/RecTutorial.html doc/RecTutorial/RecTutorial.pdf doc/RecTutorial/RecTutorial.ps dev/doc/naming-conventions.pdf +dev/ocamldoc/*.html +dev/ocamldoc/*.css # .mll files diff --git a/Makefile.build b/Makefile.build index a3766a50f..fc5816616 100644 --- a/Makefile.build +++ b/Makefile.build @@ -838,7 +838,7 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) mli-doc: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -html' - $(HIDE)$(OCAMLFIND) ocamldoc -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ -css-style style.css @@ -860,7 +860,7 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) - $(OCAMLDOC_MLLIBD) ml-doc: - $(OCAMLFIND) ocamldoc -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) + $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d $(OCAMLDOC_MLLIBD) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2f62be9af..c143afd37 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,54 @@ ========================================= += CHANGES BETWEEN COQ V8.5 AND CQQ V8.6 = +========================================= + +- The interface of the Context module was changed. + Related types and functions were put in separate submodules. + The mapping from old identifiers to new identifiers is the following: + + Context.named_declaration ---> Context.Named.Declaration.t + Context.named_list_declaration ---> Context.NamedList.Declaration.t + Context.rel_declaration ---> Context.Rel.Declaration.t + Context.map_named_declaration ---> Context.Named.Declaration.map + Context.map_named_list_declaration ---> Context.NamedList.Declaration.map + Context.map_rel_declaration ---> Context.Rel.Declaration.map + Context.fold_named_declaration ---> Context.Named.Declaration.fold + Context.fold_rel_declaration ---> Context.Rel.Declaration.fold + Context.exists_named_declaration ---> Context.Named.Declaration.exists + Context.exists_rel_declaration ---> Context.Rel.Declaration.exists + Context.for_all_named_declaration ---> Context.Named.Declaration.for_all + Context.for_all_rel_declaration ---> Context.Rel.Declaration.for_all + Context.eq_named_declaration ---> Context.Named.Declaration.equal + Context.eq_rel_declaration ---> Context.Rel.Declaration.equal + Context.named_context ---> Context.Named.t + Context.named_list_context ---> Context.NamedList.t + Context.rel_context ---> Context.Rel.t + Context.empty_named_context ---> Context.Named.empty + Context.add_named_decl ---> Context.Named.add + Context.vars_of_named_context ---> Context.Named.to_vars + Context.lookup_named ---> Context.Named.lookup + Context.named_context_length ---> Context.Named.length + Context.named_context_equal ---> Context.Named.equal + Context.fold_named_context ---> Context.Named.fold_outside + Context.fold_named_list_context ---> Context.NamedList.fold + Context.fold_named_context_reverse ---> Context.Named.fold_inside + Context.instance_from_named_context ---> Context.Named.to_instance + Context.extended_rel_list ---> Context.Rel.to_extended_list + Context.extended_rel_vect ---> Context.Rel.to_extended_vect + Context.fold_rel_context ---> Context.Rel.fold_outside + Context.fold_rel_context_reverse ---> Context.Rel.fold_inside + Context.map_rel_context ---> Context.Rel.map + Context.map_named_context ---> Context.Named.map + Context.iter_rel_context ---> Context.Rel.iter + Context.iter_named_context ---> Context.Named.iter + Context.empty_rel_context ---> Context.Rel.empty + Context.add_rel_decl ---> Context.Rel.add + Context.lookup_rel ---> Context.Rel.lookup + Context.rel_context_length ---> Context.Rel.length + Context.rel_context_nhyps ---> Context.Rel.nhyps + Context.rel_context_tags ---> Context.Rel.to_tags + +========================================= = CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 = ========================================= diff --git a/engine/evd.mli b/engine/evd.mli index 57399f2b5..34169b021 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -10,7 +10,6 @@ open Util open Loc open Names open Term -open Context open Environ (** {5 Existential variables and unification states} @@ -105,8 +104,8 @@ type evar_info = { val make_evar : named_context_val -> types -> evar_info val evar_concl : evar_info -> constr -val evar_context : evar_info -> named_context -val evar_filtered_context : evar_info -> named_context +val evar_context : evar_info -> Context.Named.t +val evar_filtered_context : evar_info -> Context.Named.t val evar_hyps : evar_info -> named_context_val val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body @@ -223,7 +222,7 @@ val existential_opt_value : evar_map -> existential -> constr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) -val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info -> +val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> constr -> constr array -> constr @@ -423,7 +422,7 @@ val evar_list : constr -> existential list val evars_of_term : constr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : named_context -> Evar.Set.t +val evars_of_named_context : Context.Named.t -> Evar.Set.t val evars_of_filtered_evar_info : evar_info -> Evar.Set.t diff --git a/engine/namegen.mli b/engine/namegen.mli index f66bc6d88..617f6e522 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ (********************************************************************* @@ -39,13 +38,13 @@ val lambda_name : env -> Name.t * types * constr -> constr val prod_create : env -> types * types -> constr val lambda_create : env -> types * constr -> constr -val name_assumption : env -> rel_declaration -> rel_declaration -val name_context : env -> rel_context -> rel_context +val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t +val name_context : env -> Context.Rel.t -> Context.Rel.t -val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types -val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr -val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types -val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr +val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types +val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr +val it_mkProd_or_LetIn_name : env -> types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr (********************************************************************* Fresh names *) diff --git a/engine/termops.ml b/engine/termops.ml index c10c55220..ce640bacf 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Environ (* Sorts and sort family *) @@ -700,9 +699,9 @@ let replace_term = replace_term_gen eq_constr let vars_of_env env = let s = - Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) + Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id s) (named_context env) ~init:Id.Set.empty in - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s @@ -728,12 +727,12 @@ let lookup_rel_of_name id names = let empty_names_context = [] let ids_of_rel_context sign = - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) sign ~init:[] let ids_of_named_context sign = - Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] + Context.Named.fold_outside (fun (id,_,_) idl -> id::idl) sign ~init:[] let ids_of_context env = (ids_of_rel_context (rel_context env)) @@ -788,7 +787,7 @@ let split_app c = match kind_of_term c with c::(Array.to_list prev), last | _ -> assert false -type subst = (rel_context*constr) Evar.Map.t +type subst = (Context.Rel.t * constr) Evar.Map.t exception CannotFilter @@ -825,7 +824,7 @@ let filtering env cv_pb c1 c2 = in aux env cv_pb c1 c2; !evm -let decompose_prod_letin : constr -> int * rel_context * constr = +let decompose_prod_letin : constr -> int * Context.Rel.t * constr = let rec prodec_rec i l c = match kind_of_term c with | Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c @@ -861,7 +860,7 @@ let nb_prod_modulo_zeta x = | _ -> n in count 0 x -let align_prod_letin c a : rel_context * constr = +let align_prod_letin c a : Context.Rel.t * constr = let (lc,_,_) = decompose_prod_letin c in let (la,l,a) = decompose_prod_letin a in if not (la >= lc) then invalid_arg "align_prod_letin"; @@ -899,10 +898,10 @@ let process_rel_context f env = let sign = named_context_val env in let rels = rel_context env in let env0 = reset_with_named_context sign env in - Context.fold_rel_context f rels ~init:env0 + Context.Rel.fold_outside f rels ~init:env0 let assums_of_rel_context sign = - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,c,t) l -> match c with Some _ -> l @@ -912,7 +911,7 @@ let assums_of_rel_context sign = let map_rel_context_in_env f env sign = let rec aux env acc = function | d::sign -> - aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign + aux (push_rel d env) (Context.Rel.Declaration.map (f env) d :: acc) sign | [] -> acc in @@ -920,10 +919,10 @@ let map_rel_context_in_env f env sign = let map_rel_context_with_binders f sign = let rec aux k = function - | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign + | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign | [] -> [] in - aux (rel_context_length sign) sign + aux (Context.Rel.length sign) sign let substl_rel_context l = map_rel_context_with_binders (fun k -> substnl l (k-1)) @@ -955,7 +954,7 @@ let compact_named_context_reverse sign = if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 then (i1::l2,c2,t2)::q else ([i1],c1,t1)::l - in Context.fold_named_context_reverse compact ~init:[] sign + in Context.Named.fold_inside compact ~init:[] sign let compact_named_context sign = List.rev (compact_named_context_reverse sign) @@ -976,7 +975,7 @@ let global_vars_set_of_decl env = function let dependency_closure env sign hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = - Context.fold_named_context_reverse + Context.Named.fold_inside (fun (hs,hl) (x,_,_ as d) -> if Id.Set.mem x hs then (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs), diff --git a/engine/termops.mli b/engine/termops.mli index 6083f1ab5..0fbd1ee82 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -9,7 +9,6 @@ open Pp open Names open Term -open Context open Environ (** printers *) @@ -22,7 +21,7 @@ val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds val print_constr_env : env -> constr -> std_ppcmds val print_named_context : env -> std_ppcmds -val pr_rel_decl : env -> rel_declaration -> std_ppcmds +val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds @@ -31,7 +30,7 @@ val push_rel_assum : Name.t * types -> env -> env val push_rels_assum : (Name.t * types) list -> env -> env val push_named_rec_types : Name.t array * types array * 'a -> env -> env -val lookup_rel_id : Id.t -> rel_context -> int * constr option * types +val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types (** Associates the contents of an identifier in a [rel_context]. Raise [Not_found] if there is no such identifier. *) @@ -42,20 +41,20 @@ val rel_vect : int -> int -> constr array val rel_list : int -> int -> constr list (** iterators/destructors on terms *) -val mkProd_or_LetIn : rel_declaration -> types -> types -val mkProd_wo_LetIn : rel_declaration -> types -> types +val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types +val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types val it_mkProd : types -> (Name.t * types) list -> types val it_mkLambda : constr -> (Name.t * types) list -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types -val it_mkProd_wo_LetIn : types -> rel_context -> types -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkNamedProd_or_LetIn : types -> named_context -> types -val it_mkNamedProd_wo_LetIn : types -> named_context -> types -val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr +val it_mkProd_or_LetIn : types -> Context.Rel.t -> types +val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr +val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types +val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types +val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr +val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr (** {6 Generic iterators on constr} *) @@ -63,11 +62,11 @@ val map_constr_with_named_binders : (Name.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_binders_left_to_right : - (rel_declaration -> 'a -> 'a) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate @@ -81,11 +80,11 @@ val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b val fold_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b val iter_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit (**********************************************************************) @@ -110,7 +109,7 @@ val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool val dependent_univs : constr -> constr -> bool val dependent_univs_no_evar : constr -> constr -> bool -val dependent_in_decl : constr -> named_declaration -> bool +val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool val count_occurrences : constr -> constr -> int val collect_metas : constr -> int list val collect_vars : constr -> Id.Set.t (** for visible vars only *) @@ -164,11 +163,11 @@ exception CannotFilter (context,term), or raises [CannotFilter]. Warning: Outer-kernel sort subtyping are taken into account: c1 has to be smaller than c2 wrt. sorts. *) -type subst = (rel_context*constr) Evar.Map.t -val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst +type subst = (Context.Rel.t * constr) Evar.Map.t +val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst -val decompose_prod_letin : constr -> int * rel_context * constr -val align_prod_letin : constr -> constr -> rel_context * constr +val decompose_prod_letin : constr -> int * Context.Rel.t * constr +val align_prod_letin : constr -> constr -> Context.Rel.t * constr (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) @@ -197,51 +196,51 @@ val add_name : Name.t -> names_context -> names_context val lookup_name_of_rel : int -> names_context -> Name.t val lookup_rel_of_name : Id.t -> names_context -> int val empty_names_context : names_context -val ids_of_rel_context : rel_context -> Id.t list -val ids_of_named_context : named_context -> Id.t list +val ids_of_rel_context : Context.Rel.t -> Id.t list +val ids_of_named_context : Context.Named.t -> Id.t list val ids_of_context : env -> Id.t list val names_of_rel_context : env -> names_context (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) -val context_chop : int -> rel_context -> rel_context * rel_context +val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t (* [env_rel_context_chop n env] extracts out the [n] top declarations of the rel_context part of [env], counting both local definitions and hypotheses *) -val env_rel_context_chop : int -> env -> env * rel_context +val env_rel_context_chop : int -> env -> env * Context.Rel.t (** Set of local names *) val vars_of_env: env -> Id.Set.t val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) -val process_rel_context : (rel_declaration -> env -> env) -> env -> env -val assums_of_rel_context : rel_context -> (Name.t * constr) list -val lift_rel_context : int -> rel_context -> rel_context -val substl_rel_context : constr list -> rel_context -> rel_context -val smash_rel_context : rel_context -> rel_context (** expand lets in context *) +val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env +val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list +val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t +val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t +val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *) val map_rel_context_in_env : - (env -> constr -> constr) -> env -> rel_context -> rel_context + (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t val map_rel_context_with_binders : - (int -> constr -> constr) -> rel_context -> rel_context + (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t val fold_named_context_both_sides : - ('a -> named_declaration -> named_declaration list -> 'a) -> - named_context -> init:'a -> 'a -val mem_named_context : Id.t -> named_context -> bool -val compact_named_context : named_context -> named_list_context -val compact_named_context_reverse : named_context -> named_list_context + ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> + Context.Named.t -> init:'a -> 'a +val mem_named_context : Id.t -> Context.Named.t -> bool +val compact_named_context : Context.Named.t -> Context.NamedList.t +val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t val clear_named_body : Id.t -> env -> env val global_vars : env -> constr -> Id.t list -val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t +val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) -val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list +val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index a6c42b28c..d8b8bd461 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -187,12 +187,12 @@ let process_goal sigma g = Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = - let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in + let d = Context.NamedList.Declaration.map (Reductionops.nf_evar sigma) d in let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in (List.fold_right Environ.push_named d' env, (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in let (_env, hyps) = - Context.fold_named_list_context process_hyp + Context.NamedList.fold process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } diff --git a/interp/constrextern.mli b/interp/constrextern.mli index b797e455c..ff8ca0b7c 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Termops open Environ open Libnames @@ -42,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> sorts -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> - rel_context -> local_binder list + Context.Rel.t -> local_binder list (** Printing options *) val print_implicits : bool ref diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8a86d3022..918b75b0c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -101,7 +101,7 @@ let global_reference id = let construct_reference ctx id = try - Term.mkVar (let _ = Context.lookup_named id ctx in id) + Term.mkVar (let _ = Context.Named.lookup id ctx in id) with Not_found -> global_reference id @@ -685,7 +685,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = str "variable " ++ pr_id id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) - let _ = Context.lookup_named id namedctx in + let _ = Context.Named.lookup id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b671c9881..c851fbb36 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Evd open Environ open Libnames @@ -161,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map ref -> local_binder list -> - internalization_env * ((env * rel_context) * Impargs.manual_implicits) + internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) @@ -178,7 +177,7 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : named_context -> Id.t -> constr +val construct_reference : Context.Named.t -> Id.t -> constr val global_reference : Id.t -> constr val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr diff --git a/kernel/context.ml b/kernel/context.ml index 5923048fa..372f16a8d 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -15,137 +15,233 @@ (* This file defines types and combinators regarding indexes-based and names-based contexts *) -open Util -open Names - -(***************************************************************************) -(* Type of assumptions *) -(***************************************************************************) - -type named_declaration = Id.t * Constr.t option * Constr.t -type named_list_declaration = Id.t list * Constr.t option * Constr.t -type rel_declaration = Name.t * Constr.t option * Constr.t - -let map_named_declaration_skel f (id, (v : Constr.t option), ty) = - (id, Option.map f v, f ty) -let map_named_list_declaration = map_named_declaration_skel -let map_named_declaration = map_named_declaration_skel - -let map_rel_declaration = map_named_declaration - -let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) -let fold_rel_declaration = fold_named_declaration - -let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty -let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty - -let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty -let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty - -let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Id.equal i1 i2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 - -let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) = - Name.equal n1 n2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 - -(***************************************************************************) -(* Type of local contexts (telescopes) *) -(***************************************************************************) - -(*s Signatures of ordered optionally named variables, intended to be - accessed by de Bruijn indices (to represent bound variables) *) - -type rel_context = rel_declaration list - -let empty_rel_context = [] - -let add_rel_decl d ctxt = d::ctxt - -let rec lookup_rel n sign = - match n, sign with - | 1, decl :: _ -> decl - | n, _ :: sign -> lookup_rel (n-1) sign - | _, [] -> raise Not_found - -let rel_context_length = List.length +(** The modules defined below represent a {e local context} + as defined by Chapter 4 in the Reference Manual: -let rel_context_nhyps hyps = - let rec nhyps acc = function - | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in - nhyps 0 hyps + A {e local context} is an ordered list of of {e local declarations} + of names that we call {e variables}. -let rel_context_tags ctx = - let rec aux l = function - | [] -> l - | (_,Some _,_)::ctx -> aux (true::l) ctx - | (_,None,_)::ctx -> aux (false::l) ctx - in aux [] ctx + A {e local declaration} of some variable can be either: + - a {e local assumption}, or + - a {e local definition}. +*) -(*s Signatures of named hypotheses. Used for section variables and - goal assumptions. *) - -type named_context = named_declaration list -type named_list_context = named_list_declaration list - -let empty_named_context = [] - -let add_named_decl d sign = d::sign - -let rec lookup_named id = function - | (id',_,_ as decl) :: _ when Id.equal id id' -> decl - | _ :: sign -> lookup_named id sign - | [] -> raise Not_found - -let named_context_length = List.length -let named_context_equal = List.equal eq_named_declaration - -let vars_of_named_context ctx = - List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx - -let instance_from_named_context sign = - let filter = function - | (id, None, _) -> Some (Constr.mkVar id) - | (_, Some _, _) -> None - in - List.map_filter filter sign - -(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] - with n = |Δ| and with the local definitions of [Γ] skipped in - [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) - -let extended_rel_list n hyps = - let rec reln l p = function - | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps - | (_, Some _, _) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - -let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) - -let fold_named_context f l ~init = List.fold_right f l init -let fold_named_list_context f l ~init = List.fold_right f l init -let fold_named_context_reverse f ~init l = List.fold_left f init l - -(*s Signatures of ordered section variables *) -type section_context = named_context - -let fold_rel_context f l ~init:x = List.fold_right f l x -let fold_rel_context_reverse f ~init:x l = List.fold_left f x l - -let map_context f l = - let map_decl (n, body_o, typ as decl) = - let body_o' = Option.smartmap f body_o in - let typ' = f typ in - if body_o' == body_o && typ' == typ then decl else - (n, body_o', typ') - in - List.smartmap map_decl l - -let map_rel_context = map_context -let map_named_context = map_context +open Util +open Names -let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) -let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) +(** Representation of contexts that can capture anonymous as well as non-anonymous variables. + Individual declarations are then designated by de Bruijn indexes. *) +module Rel = + struct + (** Representation of {e local declarations}. + + [(name, None, typ)] represents a {e local assumption}. + In the Reference Manual we denote them as [(name:typ)]. + + [(name, Some value, typ)] represents a {e local definition}. + In the Reference Manual we denote them as [(name := value : typ)]. + *) + module Declaration = + struct + type t = Name.t * Constr.t option * Constr.t + + (** Map all terms in a given declaration. *) + let map f (n, v, ty) = (n, Option.map f v, f ty) + + (** Reduce all terms in a given declaration to a single value. *) + let fold f (_, v, ty) a = f ty (Option.fold_right f v a) + + (** Check whether any term in a given declaration satisfies a given predicate. *) + let exists f (_, v, ty) = Option.cata f false v || f ty + + (** Check whether all terms in a given declaration satisfy a given predicate. *) + let for_all f (_, v, ty) = Option.cata f true v && f ty + + (** Check whether the two given declarations are equal. *) + let equal (n1, v1, ty1) (n2, v2, ty2) = + Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2 + end + + (** Rel-context is represented as a list of declarations. + Inner-most declarations are at the beginning of the list. + Outer-most declarations are at the end of the list. *) + type t = Declaration.t list + + (** empty rel-context *) + let empty = [] + + (** Return a new rel-context enriched by with a given inner-most declaration. *) + let add d ctx = d :: ctx + + (** Return a declaration designated by a given de Bruijn index. + @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *) + let rec lookup n ctx = + match n, ctx with + | 1, decl :: _ -> decl + | n, _ :: sign -> lookup (n-1) sign + | _, [] -> raise Not_found + + (** Map all terms in a given rel-context. *) + let map f = + let map_decl (n, body_o, typ as decl) = + let body_o' = Option.smartmap f body_o in + let typ' = f typ in + if body_o' == body_o && typ' == typ then decl else + (n, body_o', typ') + in + List.smartmap map_decl + + (** Reduce all terms in a given rel-context to a single value. + Innermost declarations are processed first. *) + let fold_inside f ~init = List.fold_left f init + + (** Reduce all terms in a given rel-context to a single value. + Outermost declarations are processed first. *) + let fold_outside f l ~init = List.fold_right f l init + + (** Perform a given action on every declaration in a given rel-context. *) + let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b) + + (** Return the number of {e local declarations} in a given context. *) + let length = List.length + + (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + with n = |Δ| and with the local definitions of [Γ] skipped in + [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) + let nhyps = + let rec nhyps acc = function + | [] -> acc + | (_,None,_)::hyps -> nhyps (1+acc) hyps + | (_,Some _,_)::hyps -> nhyps acc hyps in + nhyps 0 + + (** Map a given rel-context to a list where each {e local assumption} is mapped to [true] + and each {e local definition} is mapped to [false]. *) + let to_tags = + let rec aux l = function + | [] -> l + | (_,Some _,_)::ctx -> aux (true::l) ctx + | (_,None,_)::ctx -> aux (false::l) ctx + in aux [] + + (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + with n = |Δ| and with the {e local definitions} of [Γ] skipped in + [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) + let to_extended_list n = + let rec reln l p = function + | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | (_, Some _, _) :: hyps -> reln l (p+1) hyps + | [] -> l + in + reln [] 1 + + (** [extended_vect n Γ] does the same, returning instead an array. *) + let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps) + end + +(** This module represents contexts that can capture non-anonymous variables. + Individual declarations are then designated by the identifiers they bind. *) +module Named = + struct + (** Representation of {e local declarations}. + + [(id, None, typ)] represents a {e local assumption}. + In the Reference Manual we denote them as [(name:typ)]. + + [(id, Some value, typ)] represents a {e local definition}. + In the Reference Manual we denote them as [(name := value : typ)]. + *) + module Declaration = + struct + (** Named-context is represented as a list of declarations. + Inner-most declarations are at the beginning of the list. + Outer-most declarations are at the end of the list. *) + type t = Id.t * Constr.t option * Constr.t + + (** Map all terms in a given declaration. *) + let map = Rel.Declaration.map + + (** Reduce all terms in a given declaration to a single value. *) + let fold f (_, v, ty) a = f ty (Option.fold_right f v a) + + (** Check whether any term in a given declaration satisfies a given predicate. *) + let exists f (_, v, ty) = Option.cata f false v || f ty + + (** Check whether all terms in a given declaration satisfy a given predicate. *) + let for_all f (_, v, ty) = Option.cata f true v && f ty + + (** Check whether the two given declarations are equal. *) + let equal (i1, v1, ty1) (i2, v2, ty2) = + Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2 + end + + type t = Declaration.t list + + (** empty named-context *) + let empty = [] + + (** empty named-context *) + let add d ctx = d :: ctx + + (** Return a declaration designated by a given de Bruijn index. + @raise Not_found if the designated identifier is not present in the designated named-context. *) + let rec lookup id = function + | (id',_,_ as decl) :: _ when Id.equal id id' -> decl + | _ :: sign -> lookup id sign + | [] -> raise Not_found + + (** Map all terms in a given named-context. *) + let map f = + let map_decl (n, body_o, typ as decl) = + let body_o' = Option.smartmap f body_o in + let typ' = f typ in + if body_o' == body_o && typ' == typ then decl else + (n, body_o', typ') + in + List.smartmap map_decl + + (** Reduce all terms in a given named-context to a single value. + Innermost declarations are processed first. *) + let fold_inside f ~init = List.fold_left f init + + (** Reduce all terms in a given named-context to a single value. + Outermost declarations are processed first. *) + let fold_outside f l ~init = List.fold_right f l init + + (** Perform a given action on every declaration in a given named-context. *) + let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b) + + (** Return the number of {e local declarations} in a given named-context. *) + let length = List.length + + (** Check whether given two named-contexts are equal. *) + let equal = List.equal Declaration.equal + + (** Return the set of all identifiers bound in a given named-context. *) + let to_vars = + List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty + + (** [instance_from_named_context Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it + gives [Var id1, Var id3]. All [idj] are supposed distinct. *) + let to_instance = + let filter = function + | (id, None, _) -> Some (Constr.mkVar id) + | (_, Some _, _) -> None + in + List.map_filter filter + end + +module NamedList = + struct + module Declaration = + struct + type t = Id.t list * Constr.t option * Constr.t + let map = Named.Declaration.map + end + type t = Declaration.t list + let fold f l ~init = List.fold_right f l init + end + +type section_context = Named.t diff --git a/kernel/context.mli b/kernel/context.mli index 735467747..0db82beb5 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -6,131 +6,186 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** The modules defined below represent a {e local context} + as defined by Chapter 4 in the Reference Manual: + + A {e local context} is an ordered list of of {e local declarations} + of names that we call {e variables}. + + A {e local declaration} of some variable can be either: + - a {e local assumption}, or + - a {e local definition}. + + {e Local assumptions} are denoted in the Reference Manual as [(name : typ)] and + {e local definitions} are there denoted as [(name := value : typ)]. +*) + open Names -(** TODO: cleanup *) +(** Representation of contexts that can capture anonymous as well as non-anonymous variables. + Individual declarations are then designated by de Bruijn indexes. *) +module Rel : +sig + (** Representation of {e local declarations}. + + [(name, None, typ)] represents a {e local assumption}. + + [(name, Some value, typ)] represents a {e local definition}. + *) + module Declaration : + sig + type t = Name.t * Constr.t option * Constr.t + + (** Map all terms in a given declaration. *) + val map : (Constr.t -> Constr.t) -> t -> t + + (** Reduce all terms in a given declaration to a single value. *) + val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + + (** Check whether any term in a given declaration satisfies a given predicate. *) + val exists : (Constr.t -> bool) -> t -> bool + + (** Check whether all terms in a given declaration satisfy a given predicate. *) + val for_all : (Constr.t -> bool) -> t -> bool + + (** Check whether the two given declarations are equal. *) + val equal : t -> t -> bool + end + + (** Rel-context is represented as a list of declarations. + Inner-most declarations are at the beginning of the list. + Outer-most declarations are at the end of the list. *) + type t = Declaration.t list + + (** empty rel-context *) + val empty : t + + (** Return a new rel-context enriched by with a given inner-most declaration. *) + val add : Declaration.t -> t -> t + + (** Return a declaration designated by a given de Bruijn index. + @raise Not_found if the designated de Bruijn index outside the range. *) + val lookup : int -> t -> Declaration.t + + (** Map all terms in a given rel-context. *) + val map : (Constr.t -> Constr.t) -> t -> t -(** {6 Declarations} *) -(** A {e declaration} has the form [(name,body,type)]. It is either an - {e assumption} if [body=None] or a {e definition} if - [body=Some actualbody]. It is referred by {e name} if [na] is an - identifier or by {e relative index} if [na] is not an identifier - (in the latter case, [na] is of type [name] but just for printing - purpose) *) + (** Reduce all terms in a given rel-context to a single value. + Innermost declarations are processed first. *) + val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a -type named_declaration = Id.t * Constr.t option * Constr.t -type named_list_declaration = Id.t list * Constr.t option * Constr.t -type rel_declaration = Name.t * Constr.t option * Constr.t + (** Reduce all terms in a given rel-context to a single value. + Outermost declarations are processed first. *) + val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a -val map_named_declaration : - (Constr.t -> Constr.t) -> named_declaration -> named_declaration -val map_named_list_declaration : - (Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration -val map_rel_declaration : - (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration + (** Perform a given action on every declaration in a given rel-context. *) + val iter : (Constr.t -> unit) -> t -> unit -val fold_named_declaration : - (Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a -val fold_rel_declaration : - (Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a + (** Return the number of {e local declarations} in a given context. *) + val length : t -> int -val exists_named_declaration : - (Constr.t -> bool) -> named_declaration -> bool -val exists_rel_declaration : - (Constr.t -> bool) -> rel_declaration -> bool + (** Return the number of {e local assumptions} in a given rel-context. *) + val nhyps : t -> int -val for_all_named_declaration : - (Constr.t -> bool) -> named_declaration -> bool -val for_all_rel_declaration : - (Constr.t -> bool) -> rel_declaration -> bool + (** Map a given rel-context to a list where each {e local assumption} is mapped to [true] + and each {e local definition} is mapped to [false]. *) + val to_tags : t -> bool list -val eq_named_declaration : - named_declaration -> named_declaration -> bool + (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + with n = |Δ| and with the {e local definitions} of [Γ] skipped in + [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) + val to_extended_list : int -> t -> Constr.t list -val eq_rel_declaration : - rel_declaration -> rel_declaration -> bool + (** [extended_vect n Γ] does the same, returning instead an array. *) + val to_extended_vect : int -> t -> Constr.t array +end -(** {6 Signatures of ordered named declarations } *) +(** This module represents contexts that can capture non-anonymous variables. + Individual declarations are then designated by the identifiers they bind. *) +module Named : +sig + (** Representation of {e local declarations}. -type named_context = named_declaration list -type section_context = named_context -type named_list_context = named_list_declaration list -type rel_context = rel_declaration list -(** In [rel_context], more recent declaration is on top *) + [(id, None, typ)] represents a {e local assumption}. -val empty_named_context : named_context -val add_named_decl : named_declaration -> named_context -> named_context -val vars_of_named_context : named_context -> Id.Set.t + [(id, Some value, typ)] represents a {e local definition}. + *) + module Declaration : + sig + type t = Id.t * Constr.t option * Constr.t -val lookup_named : Id.t -> named_context -> named_declaration + (** Map all terms in a given declaration. *) + val map : (Constr.t -> Constr.t) -> t -> t -(** number of declarations *) -val named_context_length : named_context -> int + (** Reduce all terms in a given declaration to a single value. *) + val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a -(** named context equality *) -val named_context_equal : named_context -> named_context -> bool + (** Check whether any term in a given declaration satisfies a given predicate. *) + val exists : (Constr.t -> bool) -> t -> bool -(** {6 Recurrence on [named_context]: older declarations processed first } *) -val fold_named_context : - (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a + (** Check whether all terms in a given declaration satisfy a given predicate. *) + val for_all : (Constr.t -> bool) -> t -> bool -val fold_named_list_context : - (named_list_declaration -> 'a -> 'a) -> named_list_context -> init:'a -> 'a + (** Check whether the two given declarations are equal. *) + val equal : t -> t -> bool + end -(** newer declarations first *) -val fold_named_context_reverse : - ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a + (** Rel-context is represented as a list of declarations. + Inner-most declarations are at the beginning of the list. + Outer-most declarations are at the end of the list. *) + type t = Declaration.t list -(** {6 Section-related auxiliary functions } *) + (** empty named-context *) + val empty : t -(** [instance_from_named_context Ω] builds an instance [args] such - that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local - definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it - gives [Var id1, Var id3]. All [idj] are supposed distinct. *) -val instance_from_named_context : named_context -> Constr.t list + (** Return a new rel-context enriched by with a given inner-most declaration. *) + val add : Declaration.t -> t -> t -(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] - with n = |Δ| and with the local definitions of [Γ] skipped in - [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) -val extended_rel_list : int -> rel_context -> Constr.t list + (** Return a declaration designated by an identifier of the variable bound in that declaration. + @raise Not_found if the designated identifier is not bound in a given named-context. *) + val lookup : Id.t -> t -> Declaration.t -(** [extended_rel_vect n Γ] does the same, returning instead an array. *) -val extended_rel_vect : int -> rel_context -> Constr.t array + (** Map all terms in a given named-context. *) + val map : (Constr.t -> Constr.t) -> t -> t -(** {6 ... } *) -(** Signatures of ordered optionally named variables, intended to be - accessed by de Bruijn indices *) + (** Reduce all terms in a given named-context to a single value. + Innermost declarations are processed first. *) + val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a -(** {6 Recurrence on [rel_context]: older declarations processed first } *) -val fold_rel_context : - (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a + (** Reduce all terms in a given named-context to a single value. + Outermost declarations are processed first. *) + val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a -(** newer declarations first *) -val fold_rel_context_reverse : - ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a + (** Perform a given action on every declaration in a given named-context. *) + val iter : (Constr.t -> unit) -> t -> unit -(** {6 Map function of [rel_context] } *) -val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context + (** Return the number of {e local declarations} in a given named-context. *) + val length : t -> int -(** {6 Map function of [named_context] } *) -val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context + (** Check whether given two named-contexts are equal. *) + val equal : t -> t -> bool -(** {6 Map function of [rel_context] } *) -val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit + (** Return the set of all identifiers bound in a given named-context. *) + val to_vars : t -> Id.Set.t -(** {6 Map function of [named_context] } *) -val iter_named_context : (Constr.t -> unit) -> named_context -> unit + (** [instance_from_named_context Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it + gives [Var id1, Var id3]. All [idj] are supposed distinct. *) + val to_instance : t -> Constr.t list +end -(** {6 Contexts of declarations referred to by de Bruijn indices } *) +module NamedList : +sig + module Declaration : + sig + type t = Id.t list * Constr.t option * Constr.t + val map : (Constr.t -> Constr.t) -> t -> t + end -val empty_rel_context : rel_context -val add_rel_decl : rel_declaration -> rel_context -> rel_context + type t = Declaration.t list -val lookup_rel : int -> rel_context -> rel_declaration -(** Size of the [rel_context] including LetIns *) -val rel_context_length : rel_context -> int -(** Size of the [rel_context] without LetIns *) -val rel_context_nhyps : rel_context -> int -(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *) -val rel_context_tags : rel_context -> bool list + val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a +end +type section_context = Named.t diff --git a/kernel/cooking.ml b/kernel/cooking.ml index be71bd7b4..1302e71c9 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -173,7 +173,7 @@ let expmod_constr_subst cache modlist subst c = let cook_constr { Opaqueproof.modlist ; abstract } c = let cache = RefTable.create 13 in let expmod = expmod_constr_subst cache modlist (pi2 abstract) in - let hyps = Context.map_named_context expmod (pi1 abstract) in + let hyps = Context.Named.map expmod (pi1 abstract) in abstract_constant_body (expmod c) hyps let lift_univs cb subst = @@ -195,13 +195,13 @@ let cook_constant env { from = cb; info } = let abstract, usubst, abs_ctx = abstract in let usubst, univs = lift_univs cb usubst in let expmod = expmod_constr_subst cache modlist usubst in - let hyps = Context.map_named_context expmod abstract in + let hyps = Context.Named.map expmod abstract in let body = on_body modlist (hyps, usubst, abs_ctx) (fun c -> abstract_constant_body (expmod c) hyps) cb.const_body in let const_hyps = - Context.fold_named_context (fun (h,_,_) hyps -> + Context.Named.fold_outside (fun (h,_,_) hyps -> List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index aa9ef66fe..2067eb899 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -15,7 +15,6 @@ open Util open Names open Term -open Context open Vm open Cemitcodes open Cbytecodes @@ -190,7 +189,7 @@ and slot_for_fv env fv = let nv = Pre_env.lookup_named_val id env in begin match force_lazy_val nv with | None -> - let _, b, _ = Context.lookup_named id env.env_named_context in + let _, b, _ = Context.Named.lookup id env.env_named_context in fill_fv_cache nv id val_of_named idfun b | Some (v, _) -> v end @@ -198,7 +197,7 @@ and slot_for_fv env fv = let rv = Pre_env.lookup_rel_val i env in begin match force_lazy_val rv with | None -> - let _, b, _ = lookup_rel i env.env_rel_context in + let _, b, _ = Context.Rel.lookup i env.env_rel_context in fill_fv_cache rv i val_of_rel env_of_rel b | Some (v, _) -> v end diff --git a/kernel/declarations.mli b/kernel/declarations.mli index dc5c17a75..981dfe05e 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -8,7 +8,6 @@ open Names open Term -open Context (** This module defines the internal representation of global declarations. This includes global constants/axioms, mutual @@ -38,7 +37,7 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (types, rel_context * template_arity) declaration_arity +type constant_type = (types, Context.Rel.t * template_arity) declaration_arity (** Inlining level of parameters at functor applications. None means no inlining *) @@ -117,7 +116,7 @@ type one_inductive_body = { mind_typename : Id.t; (** Name of the type: [Ii] *) - mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *) mind_arity : inductive_arity; (** Arity sort and original user arity *) @@ -171,7 +170,7 @@ type mutual_inductive_body = { mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) - mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *) + mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) mind_polymorphic : bool; (** Is it polymorphic or not *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 73cfd0122..6239d3c8d 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -254,7 +254,7 @@ let subst_mind_body sub mib = mind_nparams = mib.mind_nparams; mind_nparams_rec = mib.mind_nparams_rec; mind_params_ctxt = - Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt; + Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; diff --git a/kernel/environ.ml b/kernel/environ.ml index 09fe64d77..da540bb05 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -24,7 +24,6 @@ open Errors open Util open Names open Term -open Context open Vars open Declarations open Pre_env @@ -70,7 +69,7 @@ let empty_context env = (* Rel context *) let lookup_rel n env = - lookup_rel n env.env_rel_context + Context.Rel.lookup n env.env_rel_context let evaluable_rel n env = match lookup_rel n env with @@ -81,7 +80,7 @@ let nb_rel env = env.env_nb_rel let push_rel = push_rel -let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x +let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in @@ -120,7 +119,7 @@ let map_named_val f (ctxt,ctxtv) = in (map ctxt, ctxtv) -let empty_named_context = empty_named_context +let empty_named_context = Context.Named.empty let push_named = push_named let push_named_context = List.fold_right push_named @@ -130,11 +129,11 @@ let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named id env = Context.lookup_named id env.env_named_context -let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt +let lookup_named id env = Context.Named.lookup id env.env_named_context +let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt let eq_named_context_val c1 c2 = - c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2) + c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) (* A local const is evaluable if it is defined *) @@ -153,7 +152,7 @@ let reset_with_named_context (ctxt,ctxtv) env = { env with env_named_context = ctxt; env_named_vals = ctxtv; - env_rel_context = empty_rel_context; + env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0 } @@ -176,7 +175,7 @@ let fold_named_context f env ~init = in fold_right env let fold_named_context_reverse f ~init env = - Context.fold_named_context_reverse f ~init:init (named_context env) + Context.Named.fold_inside f ~init:init (named_context env) (* Universe constraints *) @@ -389,11 +388,11 @@ let add_mind kn mib env = let lookup_constant_variables c env = let cmap = lookup_constant c env in - Context.vars_of_named_context cmap.const_hyps + Context.Named.to_vars cmap.const_hyps let lookup_inductive_variables (kn,i) env = let mis = lookup_mind kn env in - Context.vars_of_named_context mis.mind_hyps + Context.Named.to_vars mis.mind_hyps let lookup_constructor_variables (ind,_) env = lookup_inductive_variables ind env @@ -427,7 +426,7 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = - Context.fold_named_context_reverse + Context.Named.fold_inside (fun need (id,copt,t) -> if Id.Set.mem id need then let globc = @@ -443,9 +442,9 @@ let really_needed env needed = let keep_hyps env needed = let really_needed = really_needed env needed in - Context.fold_named_context + Context.Named.fold_outside (fun (id,_,_ as d) nsign -> - if Id.Set.mem id really_needed then add_named_decl d nsign + if Id.Set.mem id really_needed then Context.Named.add d nsign else nsign) (named_context env) ~init:empty_named_context diff --git a/kernel/environ.mli b/kernel/environ.mli index 2eab32e72..f3fe4d6ae 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Declarations open Univ @@ -42,8 +41,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t -val rel_context : env -> rel_context -val named_context : env -> named_context +val rel_context : env -> Context.Rel.t +val named_context : env -> Context.Named.t val named_context_val : env -> named_context_val val opaque_tables : env -> Opaqueproof.opaquetab @@ -60,25 +59,25 @@ val empty_context : env -> bool (** {5 Context of de Bruijn variables ([rel_context]) } *) val nb_rel : env -> int -val push_rel : rel_declaration -> env -> env -val push_rel_context : rel_context -> env -> env +val push_rel : Context.Rel.Declaration.t -> env -> env +val push_rel_context : Context.Rel.t -> env -> env val push_rec_types : rec_declaration -> env -> env (** Looks up in the context of local vars referred by indice ([rel_context]) raises [Not_found] if the index points out of the context *) -val lookup_rel : int -> env -> rel_declaration +val lookup_rel : int -> env -> Context.Rel.Declaration.t val evaluable_rel : int -> env -> bool (** {6 Recurrence on [rel_context] } *) val fold_rel_context : - (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a (** {5 Context of variables (section variables and goal assumptions) } *) -val named_context_of_val : named_context_val -> named_context +val named_context_of_val : named_context_val -> Context.Named.t val named_vals_of_val : named_context_val -> Pre_env.named_vals -val val_of_named_context : named_context -> named_context_val +val val_of_named_context : Context.Named.t -> named_context_val val empty_named_context_val : named_context_val @@ -88,18 +87,18 @@ val empty_named_context_val : named_context_val val map_named_val : (constr -> constr) -> named_context_val -> named_context_val -val push_named : named_declaration -> env -> env -val push_named_context : named_context -> env -> env +val push_named : Context.Named.Declaration.t -> env -> env +val push_named_context : Context.Named.t -> env -> env val push_named_context_val : - named_declaration -> named_context_val -> named_context_val + Context.Named.Declaration.t -> named_context_val -> named_context_val (** Looks up in the context of local vars referred by names ([named_context]) raises [Not_found] if the Id.t is not found *) -val lookup_named : variable -> env -> named_declaration -val lookup_named_val : variable -> named_context_val -> named_declaration +val lookup_named : variable -> env -> Context.Named.Declaration.t +val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option @@ -107,11 +106,11 @@ val named_body : variable -> env -> constr option (** {6 Recurrence on [named_context]: older declarations processed first } *) val fold_named_context : - (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : - ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a + ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a (** This forgets named and rel contexts *) val reset_context : env -> env @@ -228,7 +227,7 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> section_context +val keep_hyps : env -> Id.Set.t -> Context.section_context (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is @@ -258,22 +257,22 @@ exception Hyp_not_found return [tail::(f head (id,_,_) (rev tail))::head]. the value associated to id should not change *) val apply_to_hyp : named_context_val -> variable -> - (named_context -> named_declaration -> named_context -> named_declaration) -> + (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> named_context_val (** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into [tail::(id,_,_)::head] and return [(g tail)::(f (id,_,_))::head]. *) val apply_to_hyp_and_dependent_on : named_context_val -> variable -> - (named_declaration -> named_context_val -> named_declaration) -> - (named_declaration -> named_context_val -> named_declaration) -> + (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) -> + (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) -> named_context_val val insert_after_hyp : named_context_val -> variable -> - named_declaration -> - (named_context -> unit) -> named_context_val + Context.Named.Declaration.t -> + (Context.Named.t -> unit) -> named_context_val -val remove_hyps : Id.Set.t -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val +val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index b625478f2..85c74534e 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -90,7 +90,7 @@ let judge_of_variable env id = variables of the current env *) (* TODO: check order? *) let check_hyps_inclusion env f c sign = - Context.fold_named_context + Context.Named.fold_outside (fun (id,_,ty1) () -> try let ty2 = named_type id env in diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 11df40caf..da2d213ff 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Declarations open Declareops open Inductive @@ -341,7 +340,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor of rel_context * constr list + | LocalNotConstructor of Context.Rel.t * constr list | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -361,7 +360,7 @@ let explain_ind_err id ntyp env nbpar c err = raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) | LocalNotConstructor (paramsctxt,args)-> - let nparams = rel_context_nhyps paramsctxt in + let nparams = Context.Rel.nhyps paramsctxt in raise (InductiveError (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams, List.length args - nparams))) @@ -384,7 +383,7 @@ let failwith_non_pos_list n ntypes l = (* Check the inductive type is called with the expected parameters *) let check_correct_par (env,n,ntypes,_) hyps l largs = - let nparams = rel_context_nhyps hyps in + let nparams = Context.Rel.nhyps hyps in let largs = Array.of_list largs in if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); @@ -465,8 +464,8 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else arguments (used to generate induction schemes, so a priori less relevant to the kernel). *) let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = - let lparams = rel_context_length hyps in - let nmr = rel_context_nhyps hyps in + let lparams = Context.Rel.length hyps in + let nmr = Context.Rel.nhyps hyps in (** Positivity of one argument [c] of a constructor (i.e. the constructor [cn] has a type of the shape [… -> c … -> P], where, more generally, the arrows may be dependent). *) @@ -617,13 +616,13 @@ let check_positivity kn env_ar params inds = let ntypes = Array.length inds in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = Array.rev_to_list rc in - let lparams = rel_context_length params in - let nmr = rel_context_nhyps params in + let lparams = Context.Rel.length params in + let nmr = Context.Rel.nhyps params in let check_one i (_,lcnames,lc,(sign,_)) = let ra_env = List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in - let nargs = rel_context_nhyps sign - nmr in + let nargs = Context.Rel.nhyps sign - nmr in check_positivity_one ienv params (kn,i) nargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in @@ -697,7 +696,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params matching with a parameter context. *) let indty, paramsletsubst = (* [ty] = [Ind inst] is typed in context [params] *) - let inst = extended_rel_vect 0 paramslet in + let inst = Context.Rel.to_extended_vect 0 paramslet in let ty = mkApp (mkIndU indu, inst) in (* [Ind inst] is typed in context [params-wo-let] *) let inst' = rel_list 0 nparamargs in @@ -710,7 +709,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params in let ci = let print_info = - { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in + { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in { ci_ind = ind; ci_npar = nparamargs; ci_cstr_ndecls = mind_consnrealdecls; @@ -783,8 +782,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in - let nparamargs = rel_context_nhyps params in - let nparamdecls = rel_context_length params in + let nparamargs = Context.Rel.nhyps params in + let nparamdecls = Context.Rel.length params in let subst, ctx = Univ.abstract_universes p ctx in let params = Vars.subst_univs_level_context subst params in let env_ar = @@ -799,10 +798,10 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let consnrealdecls = - Array.map (fun (d,_) -> rel_context_length d - rel_context_length params) + Array.map (fun (d,_) -> Context.Rel.length d - Context.Rel.length params) splayed_lc in let consnrealargs = - Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params) + Array.map (fun (d,_) -> Context.Rel.nhyps d - Context.Rel.nhyps params) splayed_lc in (* Elimination sorts *) let arkind,kelim = @@ -835,8 +834,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re { mind_typename = id; mind_arity = arkind; mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign; - mind_nrealargs = rel_context_nhyps ar_sign - nparamargs; - mind_nrealdecls = rel_context_length ar_sign - nparamdecls; + mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs; + mind_nrealdecls = Context.Rel.length ar_sign - nparamdecls; mind_kelim = kelim; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealdecls; diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 01acdce5c..1fe47b1a5 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -42,6 +42,6 @@ val enforce_indices_matter : unit -> unit val is_indices_matter : unit -> bool val compute_projections : pinductive -> Id.t -> Id.t -> - int -> Context.rel_context -> int array -> int array -> - Context.rel_context -> Context.rel_context -> + int -> Context.Rel.t -> int array -> int array -> + Context.Rel.t -> Context.Rel.t -> (constant array * projection_body array) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 632b4daea..f9a6e04c1 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Declarations open Declareops open Environ @@ -77,7 +76,7 @@ let instantiate_params full t u args sign = let fail () = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = - Context.fold_rel_context + Context.Rel.fold_outside (fun (_,copt,_) (largs,subs,ty) -> match (copt, largs, kind_of_term ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) @@ -297,7 +296,7 @@ let build_dependent_inductive ind (_,mip) params = applist (mkIndU ind, List.map (lift mip.mind_nrealdecls) params - @ extended_rel_list 0 realargs) + @ Context.Rel.to_extended_list 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option @@ -350,12 +349,12 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let build_one_branch i cty = let typi = full_constructor_instantiate (ind,u,specif,params) cty in let (cstrsign,ccl) = decompose_prod_assum typi in - let nargs = rel_context_length cstrsign in + let nargs = Context.Rel.length cstrsign in let (_,allargs) = decompose_app ccl in let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in vargs @ [dep_cstr] in let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in @@ -499,7 +498,7 @@ let subterm_var p renv = with Failure _ | Invalid_argument _ -> Not_subterm let push_ctxt_renv renv ctxt = - let n = rel_context_length ctxt in + let n = Context.Rel.length ctxt in { env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv } @@ -701,7 +700,7 @@ let restrict_spec env spec p = else let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) - if noccur_with_meta 1 (rel_context_length absctx) ar then spec + if noccur_with_meta 1 (Context.Rel.length absctx) ar then spec else let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in @@ -843,7 +842,7 @@ let filter_stack_domain env ci p stack = let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) - if noccur_with_meta 1 (rel_context_length absctx) ar then stack + if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack else let env = push_rel_context absctx env in let rec filter_stack env ar stack = let t = whd_betadeltaiota env ar in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 5847d25f6..541fb8282 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Univ open Declarations open Environ @@ -35,7 +34,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list -val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context +val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t val instantiate_inductive_constraints : mutual_inductive_body -> universe_instance -> constraints @@ -86,7 +85,7 @@ val build_branches_type : constr list -> constr -> types array (** Return the arity of an inductive type *) -val mind_arity : one_inductive_body -> rel_context * sorts_family +val mind_arity : one_inductive_body -> Context.Rel.t * sorts_family val inductive_sort_family : one_inductive_body -> sorts_family @@ -111,8 +110,8 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : sorts array -> universe -val instantiate_universes : env -> rel_context -> - template_arity -> constr Lazy.t array -> rel_context * sorts +val instantiate_universes : env -> Context.Rel.t -> + template_arity -> constr Lazy.t array -> Context.Rel.t * sorts (** {6 Debug} *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 98b2d6d2e..dd6ef1c66 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -8,7 +8,6 @@ open Errors open Names open Term -open Context open Declarations open Util open Nativevalues @@ -1826,15 +1825,15 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = in let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in let auxdefs = List.fold_right get_named_val fv_named auxdefs in - let lvl = rel_context_length env.env_rel_context in + let lvl = Context.Rel.length env.env_rel_context in let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in let aux_name = fresh_lname Anonymous in auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) and compile_rel env sigma univ auxdefs n = - let (_,body,_) = lookup_rel n env.env_rel_context in - let n = rel_context_length env.env_rel_context - n in + let (_,body,_) = Context.Rel.lookup n env.env_rel_context in + let n = Context.Rel.length env.env_rel_context - n in match body with | Some t -> let code = lambda_of_constr env sigma t in @@ -1844,7 +1843,7 @@ and compile_rel env sigma univ auxdefs n = Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs and compile_named env sigma univ auxdefs id = - let (_,body,_) = lookup_named id env.env_named_context in + let (_,body,_) = Context.Named.lookup id env.env_named_context in match body with | Some t -> let code = lambda_of_constr env sigma t in diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index badb15b56..bfddf8286 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t } + abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 009ff82ff..5b743a4c7 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -48,7 +48,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t } + abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } (* The type has two caveats: 1) cook_constr is defined after diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 615b9d49b..9fcec1114 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,7 +15,6 @@ open Util open Names -open Context open Univ open Term open Declarations @@ -66,9 +65,9 @@ type named_vals = (Id.t * lazy_val) list type env = { env_globals : globals; - env_named_context : named_context; + env_named_context : Context.Named.t; env_named_vals : named_vals; - env_rel_context : rel_context; + env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification; @@ -77,7 +76,7 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = named_context * named_vals +type named_context_val = Context.Named.t * named_vals let empty_named_context_val = [],[] @@ -87,9 +86,9 @@ let empty_env = { env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; - env_named_context = empty_named_context; + env_named_context = Context.Named.empty; env_named_vals = []; - env_rel_context = empty_rel_context; + env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0; env_stratification = { @@ -107,7 +106,7 @@ let nb_rel env = env.env_nb_rel let push_rel d env = let rval = ref VKnone in { env with - env_rel_context = add_rel_decl d env.env_rel_context; + env_rel_context = Context.Rel.add d env.env_rel_context; env_rel_val = rval :: env.env_rel_val; env_nb_rel = env.env_nb_rel + 1 } @@ -127,7 +126,7 @@ let env_of_rel n env = let push_named_context_val d (ctxt,vals) = let id,_,_ = d in let rval = ref VKnone in - add_named_decl d ctxt, (id,rval)::vals + Context.Named.add d ctxt, (id,rval)::vals let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); @@ -135,7 +134,7 @@ let push_named d env = let id,body,_ = d in let rval = ref VKnone in { env_globals = env.env_globals; - env_named_context = Context.add_named_decl d env.env_named_context; + env_named_context = Context.Named.add d env.env_named_context; env_named_vals = (id, rval) :: env.env_named_vals; env_rel_context = env.env_rel_context; env_rel_val = env.env_rel_val; diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index b499ac0c5..9cd940a88 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Declarations open Univ @@ -46,9 +45,9 @@ type named_vals = (Id.t * lazy_val) list type env = { env_globals : globals; - env_named_context : named_context; + env_named_context : Context.Named.t; env_named_vals : named_vals; - env_rel_context : rel_context; + env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification; @@ -57,7 +56,7 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = named_context * named_vals +type named_context_val = Context.Named.t * named_vals val empty_named_context_val : named_context_val @@ -66,15 +65,15 @@ val empty_env : env (** Rel context *) val nb_rel : env -> int -val push_rel : rel_declaration -> env -> env +val push_rel : Context.Rel.Declaration.t -> env -> env val lookup_rel_val : int -> env -> lazy_val val env_of_rel : int -> env -> env (** Named context *) val push_named_context_val : - named_declaration -> named_context_val -> named_context_val -val push_named : named_declaration -> env -> env + Context.Named.Declaration.t -> named_context_val -> named_context_val +val push_named : Context.Named.Declaration.t -> env -> env val lookup_named_val : Id.t -> env -> lazy_val val env_of_named : Id.t -> env -> env diff --git a/kernel/reduction.ml b/kernel/reduction.ml index bf2ee2707..78222c6b6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -20,7 +20,6 @@ open Util open Names open Term open Vars -open Context open Univ open Environ open Closure @@ -741,10 +740,10 @@ let dest_prod env = match kind_of_term t with | Prod (n,a,c0) -> let d = (n,None,a) in - decrec (push_rel d env) (add_rel_decl d m) c0 + decrec (push_rel d env) (Context.Rel.add d m) c0 | _ -> m,t in - decrec env empty_rel_context + decrec env Context.Rel.empty (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = @@ -753,17 +752,17 @@ let dest_prod_assum env = match kind_of_term rty with | Prod (x,t,c) -> let d = (x,None,t) in - prodec_rec (push_rel d env) (add_rel_decl d l) c + prodec_rec (push_rel d env) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> let d = (x,Some b,t) in - prodec_rec (push_rel d env) (add_rel_decl d l) c + prodec_rec (push_rel d env) (Context.Rel.add d l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> let rty' = whd_betadeltaiota env rty in if Term.eq_constr rty' rty then l, rty else prodec_rec env l rty' in - prodec_rec env empty_rel_context + prodec_rec env Context.Rel.empty let dest_lam_assum env = let rec lamec_rec env l ty = @@ -771,14 +770,14 @@ let dest_lam_assum env = match kind_of_term rty with | Lambda (x,t,c) -> let d = (x,None,t) in - lamec_rec (push_rel d env) (add_rel_decl d l) c + lamec_rec (push_rel d env) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> let d = (x,Some b,t) in - lamec_rec (push_rel d env) (add_rel_decl d l) c + lamec_rec (push_rel d env) (Context.Rel.add d l) c | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty in - lamec_rec env empty_rel_context + lamec_rec env Context.Rel.empty exception NotArity diff --git a/kernel/reduction.mli b/kernel/reduction.mli index f7a8d88c2..35daff7b5 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -7,7 +7,6 @@ (************************************************************************) open Term -open Context open Environ (*********************************************************************** @@ -99,9 +98,9 @@ val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) -val dest_prod : env -> types -> rel_context * types -val dest_prod_assum : env -> types -> rel_context * types -val dest_lam_assum : env -> types -> rel_context * types +val dest_prod : env -> types -> Context.Rel.t * types +val dest_prod_assum : env -> types -> Context.Rel.t * types +val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity diff --git a/kernel/term.ml b/kernel/term.ml index 455248dd5..19f4b7a23 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -10,7 +10,6 @@ open Util open Pp open Errors open Names -open Context open Vars (**********************************************************************) @@ -590,24 +589,24 @@ let decompose_lam_n n = let decompose_prod_assum = let rec prodec_rec l c = match kind_of_term c with - | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) c - | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c + | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) c + | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in - prodec_rec empty_rel_context + prodec_rec Context.Rel.empty (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) let decompose_lam_assum = let rec lamdec_rec l c = match kind_of_term c with - | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) c - | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in - lamdec_rec empty_rel_context + lamdec_rec Context.Rel.empty (* Given a positive integer n, decompose a product or let-in term of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair @@ -619,12 +618,12 @@ let decompose_prod_n_assum n = let rec prodec_rec l n c = if Int.equal n 0 then l,c else match kind_of_term c with - | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c + | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | c -> error "decompose_prod_n_assum: not enough assumptions" in - prodec_rec empty_rel_context n + prodec_rec Context.Rel.empty n (* Given a positive integer n, decompose a lambda or let-in term [fun (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted @@ -638,12 +637,12 @@ let decompose_lam_n_assum n = let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match kind_of_term c with - | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) n c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" in - lamdec_rec empty_rel_context n + lamdec_rec Context.Rel.empty n (* Same, counting let-in *) let decompose_lam_n_decls n = @@ -652,12 +651,12 @@ let decompose_lam_n_decls n = let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match kind_of_term c with - | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_decls: not enough abstractions" in - lamdec_rec empty_rel_context n + lamdec_rec Context.Rel.empty n let prod_assum t = fst (decompose_prod_assum t) let prod_n_assum n t = fst (decompose_prod_n_assum n t) @@ -678,7 +677,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = rel_context * sorts +type arity = Context.Rel.t * sorts let destArity = let rec prodec_rec l c = diff --git a/kernel/term.mli b/kernel/term.mli index 972a67ebe..c45e04338 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Context (** {5 Redeclaration of types from module Constr and Sorts} @@ -213,14 +212,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr val mkNamedProd : Id.t -> types -> types -> types (** Constructs either [(x:t)c] or [[x=b:t]c] *) -val mkProd_or_LetIn : rel_declaration -> types -> types -val mkProd_wo_LetIn : rel_declaration -> types -> types -val mkNamedProd_or_LetIn : named_declaration -> types -> types -val mkNamedProd_wo_LetIn : named_declaration -> types -> types +val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types +val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types +val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types +val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types (** Constructs either [[x:t]c] or [[x=b:t]c] *) -val mkLambda_or_LetIn : rel_declaration -> constr -> constr -val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr +val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr +val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr (** {5 Other term constructors. } *) @@ -262,8 +261,8 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types +val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr +val it_mkProd_or_LetIn : types -> Context.Rel.t -> types (** In [lambda_applist c args], [c] is supposed to have the form [λΓ.c] with [Γ] without let-in; it returns [c] with the variables @@ -314,29 +313,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) -val decompose_prod_assum : types -> rel_context * types +val decompose_prod_assum : types -> Context.Rel.t * types (** Idem with lambda's *) -val decompose_lam_assum : constr -> rel_context * constr +val decompose_lam_assum : constr -> Context.Rel.t * constr (** Idem but extract the first [n] premisses, counting let-ins. *) -val decompose_prod_n_assum : int -> types -> rel_context * types +val decompose_prod_n_assum : int -> types -> Context.Rel.t * types (** Idem for lambdas, _not_ counting let-ins *) -val decompose_lam_n_assum : int -> constr -> rel_context * constr +val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr (** Idem, counting let-ins *) -val decompose_lam_n_decls : int -> constr -> rel_context * constr +val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr (** Return the premisses/parameters of a type/term (let-in included) *) -val prod_assum : types -> rel_context -val lam_assum : constr -> rel_context +val prod_assum : types -> Context.Rel.t +val lam_assum : constr -> Context.Rel.t (** Return the first n-th premisses/parameters of a type (let included and counted) *) -val prod_n_assum : int -> types -> rel_context +val prod_n_assum : int -> types -> Context.Rel.t (** Return the first n-th premisses/parameters of a term (let included but not counted) *) -val lam_n_assum : int -> constr -> rel_context +val lam_n_assum : int -> constr -> Context.Rel.t (** Remove the premisses/parameters of a type/term *) val strip_prod : types -> types @@ -369,7 +368,7 @@ val under_outer_cast : (constr -> constr) -> constr -> constr Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = rel_context * sorts +type arity = Context.Rel.t * sorts (** Build an "arity" from its canonical form *) val mkArity : arity -> types diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a566028d4..db50a393b 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -16,7 +16,6 @@ open Errors open Util open Names open Term -open Context open Declarations open Environ open Entries @@ -246,8 +245,8 @@ let infer_declaration ~trust env kn dcl = let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t | TemplateArity (ctx,_) -> - Context.fold_rel_context - (fold_rel_declaration + Context.Rel.fold_outside + (Context.Rel.Declaration.fold (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4f32fdce8..35f53b7e7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Declarations open Environ open Entries @@ -99,7 +98,7 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = - Context.fold_named_context + Context.Named.fold_outside (fun (id,b1,ty1) () -> try let (_,b2,ty2) = lookup_named id env in @@ -561,6 +560,6 @@ let infer_local_decls env decls = | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, add_rel_decl d l) - | [] -> (env, empty_rel_context) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) in inferec env decls diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 010b2b6f0..bcaa6b63e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -9,7 +9,6 @@ open Names open Univ open Term -open Context open Environ open Entries open Declarations @@ -28,7 +27,7 @@ val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * rel_context) + env -> (Id.t * local_entry) list -> (env * Context.Rel.t) (** {6 Basic operations of the typing machine. } *) @@ -128,4 +127,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> section_context -> unit +val check_hyps_inclusion : env -> constr -> Context.section_context -> unit diff --git a/kernel/vars.ml b/kernel/vars.ml index a00c7036f..53543e043 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -8,7 +8,6 @@ open Names open Esubst -open Context (*********************) (* Occurring *) @@ -160,9 +159,9 @@ let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c -let substnl_decl laml k r = map_rel_declaration (fun c -> substnl laml k c) r -let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r -let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r +let substnl_decl laml k r = Context.Rel.Declaration.map (fun c -> substnl laml k c) r +let substl_decl laml r = Context.Rel.Declaration.map (fun c -> substnl laml 0 c) r +let subst1_decl lam r = Context.Rel.Declaration.map (fun c -> subst1 lam c) r (* Build a substitution from an instance, inserting missing let-ins *) @@ -302,7 +301,7 @@ let subst_univs_level_constr subst c = if !changed then c' else c let subst_univs_level_context s = - map_rel_context (subst_univs_level_constr s) + Context.Rel.map (subst_univs_level_constr s) let subst_instance_constr subst c = if Univ.Instance.is_empty subst then c @@ -343,7 +342,7 @@ let subst_instance_constr subst c = let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx - else map_rel_context (fun x -> subst_instance_constr s x) ctx + else Context.Rel.map (fun x -> subst_instance_constr s x) ctx type id_key = constant tableKey let eq_id_key x y = Names.eq_table_key Constant.equal x y diff --git a/kernel/vars.mli b/kernel/vars.mli index a84cf0114..659990806 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -8,7 +8,6 @@ open Names open Constr -open Context (** {6 Occur checks } *) @@ -69,10 +68,10 @@ type substl = constr list as if usable in [applist] while the substitution is represented the other way round, i.e. ending with either [u₁] or [c₁], as if usable for [substl]. *) -val subst_of_rel_context_instance : rel_context -> constr list -> substl +val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl (** For compatibility: returns the substitution reversed *) -val adjust_subst_to_rel_context : rel_context -> constr list -> constr list +val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates @@ -92,13 +91,13 @@ val subst1 : constr -> constr -> constr accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *) -val substnl_decl : substl -> int -> rel_declaration -> rel_declaration +val substnl_decl : substl -> int -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t (** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *) -val substl_decl : substl -> rel_declaration -> rel_declaration +val substl_decl : substl -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t (** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *) -val subst1_decl : constr -> rel_declaration -> rel_declaration +val subst1_decl : constr -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t (** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by [cj] in [t]. *) @@ -136,11 +135,11 @@ val subst_univs_constr : universe_subst -> constr -> constr (** Level substitutions for polymorphism. *) val subst_univs_level_constr : universe_level_subst -> constr -> constr -val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context +val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t (** Instance substitution for polymorphism. *) val subst_instance_constr : universe_instance -> constr -> constr -val subst_instance_context : universe_instance -> rel_context -> rel_context +val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t type id_key = constant tableKey val eq_id_key : id_key -> id_key -> bool diff --git a/library/decls.ml b/library/decls.ml index 8d5085f70..b5f9143b8 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -11,7 +11,6 @@ open Util open Names -open Context open Decl_kinds open Libnames @@ -55,7 +54,7 @@ let initialize_named_context_for_proof () = Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = - fold_named_context + Context.Named.fold_outside (fun (id,_,_) sec_ids -> try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) diff --git a/library/global.mli b/library/global.mli index 09ed4eb0a..d6547105d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -21,7 +21,7 @@ val env_is_initial : unit -> bool val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.named_context +val named_context : unit -> Context.Named.t (** {6 Enriching the global environment } *) @@ -73,7 +73,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.named_declaration +val lookup_named : variable -> Context.Named.Declaration.t val lookup_constant : constant -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body diff --git a/library/lib.mli b/library/lib.mli index bb8831759..874fc89fb 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -164,7 +164,7 @@ type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t val instance_from_variable_context : variable_context -> Names.Id.t array -val named_of_variable_context : variable_context -> Context.named_context +val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.constant -> abstr_info val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info @@ -175,8 +175,8 @@ val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit val add_section_constant : bool (* is_projection *) -> - Names.constant -> Context.named_context -> unit -val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit + Names.constant -> Context.Named.t -> unit +val add_section_kn : Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) @@ -189,6 +189,6 @@ val discharge_inductive : Names.inductive -> Names.inductive (* discharging a constant in one go *) val full_replacement_context : unit -> Opaqueproof.work_list list val full_section_segment_of_constant : - Names.constant -> (Context.named_context -> Context.named_context) list + Names.constant -> (Context.Named.t -> Context.Named.t) list diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 2dc2420c4..923743ece 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -11,7 +11,6 @@ open Util open Names open Term open Vars -open Context open Declarations open Declareops open Environ diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 6c7b09383..d306112ce 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -7,7 +7,6 @@ (************************************************************************) open Term -open Context open Globnames val qflag : bool ref @@ -27,7 +26,7 @@ type counter = bool -> metavariable val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array val ind_hyps : int -> pinductive -> constr list -> - Proof_type.goal Tacmach.sigma -> rel_context array + Proof_type.goal Tacmach.sigma -> Context.Rel.t array type atoms = {positive:constr list;negative:constr list} diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f57f12f66..ad18ea95a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -3,7 +3,6 @@ open Errors open Util open Term open Vars -open Context open Namegen open Names open Declarations @@ -230,7 +229,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta -let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = +let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = let nochange ?t' msg = begin observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t ); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index bbe2f1a3a..e2c3bbb97 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -3,7 +3,6 @@ open Errors open Util open Term open Vars -open Context open Namegen open Names open Pp @@ -30,7 +29,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let env = Global.env () in let env_with_params = Environ.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in - let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context) : rel_context = + let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t = match predicates with | [] -> [] |(Name x,v,t)::predicates -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 5d92fca5e..80de8e764 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env = let new_env = add_pat_variables env pat typ in let res = fst ( - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,v,t) (env,ctxt) -> match na with | Anonymous -> assert false diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index e3455e770..be04728e0 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -19,7 +19,6 @@ open Pp open Names open Term open Vars -open Context open Termops open Declarations open Glob_term @@ -258,27 +257,27 @@ type merge_infos = lnk2: int merged_arg array; (** rec params which remain rec param (ie not linked) *) - recprms1: rel_declaration list; - recprms2: rel_declaration list; + recprms1: Context.Rel.Declaration.t list; + recprms2: Context.Rel.Declaration.t list; nrecprms1: int; nrecprms2: int; (** rec parms which became non parm (either linked to something or because after a rec parm that became non parm) *) - otherprms1: rel_declaration list; - otherprms2: rel_declaration list; + otherprms1: Context.Rel.Declaration.t list; + otherprms2: Context.Rel.Declaration.t list; notherprms1:int; notherprms2:int; (** args which remain args in merge *) - args1:rel_declaration list; - args2:rel_declaration list; + args1:Context.Rel.Declaration.t list; + args2:Context.Rel.Declaration.t list; nargs1:int; nargs2:int; (** functional result args *) - funresprms1: rel_declaration list; - funresprms2: rel_declaration list; + funresprms1: Context.Rel.Declaration.t list; + funresprms2: Context.Rel.Declaration.t list; nfunresprms1:int; nfunresprms2:int; } @@ -851,7 +850,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift lident , bindlist , Some cstr_expr , lcstor_expr -let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = +let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] (Global.env()) Evd.empty t in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b894cb8ea..adcaa6441 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Namegen open Declarations @@ -131,7 +130,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool*(Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * rel_declaration + | Abstract of int * Context.Rel.Declaration.t type tomatch_stack = tomatch_status list @@ -602,7 +601,7 @@ let relocate_index_tomatch n1 n2 = NonDepAlias :: genrec depth rest | Abstract (i,d) :: rest -> let i = relocate_rel n1 n2 depth i in - Abstract (i,map_rel_declaration (relocate_index n1 n2 depth) d) + Abstract (i, Context.Rel.Declaration.map (relocate_index n1 n2 depth) d) :: genrec (depth+1) rest in genrec 0 @@ -635,7 +634,7 @@ let replace_tomatch n c = | NonDepAlias :: rest -> NonDepAlias :: replrec depth rest | Abstract (i,d) :: rest -> - Abstract (i,map_rel_declaration (replace_term n c depth) d) + Abstract (i, Context.Rel.Declaration.map (replace_term n c depth) d) :: replrec (depth+1) rest in replrec 0 @@ -660,7 +659,7 @@ let rec liftn_tomatch_stack n depth = function NonDepAlias :: liftn_tomatch_stack n depth rest | Abstract (i,d)::rest -> let i = if i<depth then i else i+n in - Abstract (i,map_rel_declaration (liftn n depth) d) + Abstract (i, Context.Rel.Declaration.map (liftn n depth) d) ::(liftn_tomatch_stack n (depth+1) rest) let lift_tomatch_stack n = liftn_tomatch_stack n 1 @@ -921,7 +920,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = let tms = List.fold_right2 (fun par arg tomatch -> match kind_of_term par with | Rel i -> relocate_index_tomatch (i+n) (destRel arg) tomatch - | _ -> tomatch) (realargs@[cur]) (extended_rel_list 0 sign) + | _ -> tomatch) (realargs@[cur]) (Context.Rel.to_extended_list 0 sign) (lift_tomatch_stack n tms) in (* Pred is already dependent in the current term to match (if *) (* (na<>Anonymous) and its realargs; we just need to adjust it to *) @@ -1118,7 +1117,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with | [], _ -> brs,tomatch,pred,[] | n::deps, Abstract (i,d) :: tomatch -> - let d = map_rel_declaration (nf_evar evd) d in + let d = Context.Rel.Declaration.map (nf_evar evd) d in let is_d = match d with (_, None, _) -> false | _ -> true in if is_d || List.exists (fun c -> dependent_decl (lift k c) d) tocheck && Array.exists (is_dependent_branch k) brs then @@ -1187,7 +1186,7 @@ let group_equations pb ind current cstrs mat = let rec generalize_problem names pb = function | [] -> pb, [] | i::l -> - let (na,b,t as d) = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in + let (na,b,t as d) = Context.Rel.Declaration.map (lift i) (Environ.lookup_rel i pb.env) in let pb',deps = generalize_problem names pb l in begin match (na, b) with | Anonymous, Some _ -> pb', deps @@ -1230,7 +1229,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* We adjust the terms to match in the context they will be once the *) (* context [x1:T1,..,xn:Tn] will have been pushed on the current env *) let typs' = - List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in + List.map_i (fun i d -> (mkRel i, Context.Rel.Declaration.map (lift i) d)) 1 typs in let extenv = push_rel_context typs pb.env in @@ -1560,8 +1559,8 @@ let matx_of_eqns env eqns = *) let adjust_to_extended_env_and_remove_deps env extenv subst t = - let n = rel_context_length (rel_context env) in - let n' = rel_context_length (rel_context extenv) in + let n = Context.Rel.length (rel_context env) in + let n' = Context.Rel.length (rel_context extenv) in (* We first remove the bindings that are dependently typed (they are difficult to manage and it is not sure these are so useful in practice); Notes: @@ -1673,8 +1672,8 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = | None -> (* This is the situation we are building a return predicate and we are in an impossible branch *) - let n = rel_context_length (rel_context env) in - let n' = rel_context_length (rel_context tycon_env) in + let n = Context.Rel.length (rel_context env) in + let n' = Context.Rel.length (rel_context tycon_env) in let impossible_case_type, u = e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in (lift (n'-n) impossible_case_type, mkSort u) @@ -1744,7 +1743,7 @@ let build_inversion_problem loc env sigma tms t = let n = List.length sign in let decls = - List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in + List.map_i (fun i d -> (mkRel i, Context.Rel.Declaration.map (lift i) d)) 1 sign in let pb_env = push_rel_context sign env in let decls = diff --git a/pretyping/cases.mli b/pretyping/cases.mli index c599766ab..4ec71956b 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Evd open Environ open Inductiveops @@ -45,11 +44,11 @@ val compile_cases : val constr_of_pat : Environ.env -> Evd.evar_map ref -> - rel_declaration list -> + Context.Rel.Declaration.t list -> Glob_term.cases_pattern -> Names.Id.t list -> Glob_term.cases_pattern * - (rel_declaration list * Term.constr * + (Context.Rel.Declaration.t list * Term.constr * (Term.types * Term.constr list) * Glob_term.cases_pattern) * Names.Id.t list @@ -83,7 +82,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool * (Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * rel_declaration + | Abstract of int * Context.Rel.Declaration.t type tomatch_stack = tomatch_status list @@ -117,7 +116,7 @@ val prepare_predicate : Loc.t -> Environ.env -> Evd.evar_map -> (Term.types * tomatch_type) list -> - Context.rel_context list -> + Context.Rel.t list -> Constr.constr option -> 'a option -> (Evd.evar_map * Names.name list * Term.constr) list diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 5e99521a1..0b0bd8304 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -17,7 +17,6 @@ open Termops open Reductionops open Term open Vars -open Context open Pattern open Patternops open Misctypes @@ -269,8 +268,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in - let n = rel_context_length ctx_b2 in - let n' = rel_context_length ctx_b2' in + let n = Context.Rel.length ctx_b2 in + let n' = Context.Rel.length ctx_b2' in if noccur_between 1 n b2 && noccur_between 1 n' b2' then let f l (na,_,t) = (Anonymous,na,t)::l in let ctx_br = List.fold_left f ctx ctx_b2 in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index dab82fa22..4ca066feb 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -12,7 +12,6 @@ open Util open Names open Term open Vars -open Context open Inductiveops open Environ open Glob_term @@ -199,7 +198,7 @@ let computable p k = engendrera un prédicat non dépendant) *) let sign,ccl = decompose_lam_assum p in - Int.equal (rel_context_length sign) (k + 1) + Int.equal (Context.Rel.length sign) (k + 1) && noccur_between 1 (k+1) ccl @@ -315,7 +314,7 @@ let is_nondep_branch c l = try (* FIXME: do better using tags from l *) let sign,ccl = decompose_lam_n_decls (List.length l) c in - noccur_between 1 (rel_context_length sign) ccl + noccur_between 1 (Context.Rel.length sign) ccl with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) false diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index eb158686a..f8f8093c0 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ open Glob_term open Termops @@ -46,7 +45,7 @@ val detype_case : val detype_sort : evar_map -> sorts -> glob_sort val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> - evar_map -> rel_context -> glob_decl list + evar_map -> Context.Rel.t -> glob_decl list val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index fe26dcd28..c6c397135 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -11,7 +11,6 @@ open Errors open Names open Term open Vars -open Context open Environ open Termops open Evd @@ -501,7 +500,7 @@ let solve_pattern_eqn env l c = match kind_of_term a with (* Rem: if [a] links to a let-in, do as if it were an assumption *) | Rel n -> - let d = map_rel_declaration (lift n) (lookup_rel n env) in + let d = Context.Rel.Declaration.map (lift n) (lookup_rel n env) in mkLambda_or_LetIn d c' | Var id -> let d = lookup_named id env in mkNamedLambda_or_LetIn d c' diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 3c3afac54..f001d6e3e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -12,7 +12,6 @@ open Pp open Names open Term open Vars -open Context open Termops open Namegen open Pre_env @@ -78,12 +77,12 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = let env_nf_evar sigma env = process_rel_context - (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env + (fun d e -> push_rel (Context.Rel.Declaration.map (nf_evar sigma) d) e) env let env_nf_betaiotaevar sigma env = process_rel_context (fun d e -> - push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env + push_rel (Context.Rel.Declaration.map (Reductionops.nf_betaiota sigma) d) e) env let nf_evars_universes evm = Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm) @@ -106,10 +105,10 @@ let nf_evar_map_universes evm = Evd.raw_map (fun _ -> map_evar_info f) evm, f let nf_named_context_evar sigma ctx = - Context.map_named_context (nf_evar sigma) ctx + Context.Named.map (nf_evar sigma) ctx let nf_rel_context_evar sigma ctx = - Context.map_rel_context (nf_evar sigma) ctx + Context.Rel.map (nf_evar sigma) ctx let nf_env_evar sigma env = let nc' = nf_named_context_evar sigma (Environ.named_context env) in @@ -303,7 +302,7 @@ let push_rel_context_to_named_context env typ = (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, vsubst, _, env) = - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,c,t) (subst, vsubst, avoid, env) -> let id = (* ppedrot: we want to infer nicer names for the refine tactic, but diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 96648bb11..867917c9c 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Evd open Environ @@ -129,7 +128,7 @@ val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.M [nf_evar]. *) val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t -val undefined_evars_of_named_context : evar_map -> named_context -> Evar.Set.t +val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t (** [occur_evar_upto sigma k c] returns [true] if [k] appears in @@ -170,8 +169,8 @@ val jv_nf_evar : val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_named_context_evar : evar_map -> named_context -> named_context -val nf_rel_context_evar : evar_map -> rel_context -> rel_context +val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t +val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t val nf_env_evar : evar_map -> env -> env val nf_evar_info : evar_map -> evar_info -> evar_info diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 47d9654e5..1366c34ce 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -7,7 +7,6 @@ (************************************************************************) open Locus -open Context open Term open Evd open Pretype_errors @@ -50,7 +49,7 @@ val replace_term_occ_modulo : occurrences or_like_first -> val replace_term_occ_decl_modulo : (occurrences * hyp_location_flag) or_like_first -> 'a testing_function -> (unit -> constr) -> - named_declaration -> named_declaration + Context.Named.Declaration.t -> Context.Named.Declaration.t (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC), @@ -62,7 +61,7 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first -> closed [c] at positions [occl] by [Rel 1] in [decl]. *) val subst_closed_term_occ_decl : env -> evar_map -> (occurrences * hyp_location_flag) or_like_first -> - constr -> named_declaration -> named_declaration * evar_map + constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map (** Miscellaneous *) val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 3f21842e3..40175dac9 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -19,7 +19,6 @@ open Globnames open Nameops open Term open Vars -open Context open Namegen open Declarations open Declareops @@ -61,7 +60,7 @@ let check_privacy_block mib = let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in - let indf = make_ind_family(pind, Context.extended_rel_list 0 lnamespar) in + let indf = make_ind_family(pind, Context.Rel.to_extended_list 0 lnamespar) in let constrs = get_constructors env indf in let projs = get_projections env indf in @@ -92,8 +91,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let pbody = appvect (mkRel (ndepar + nbprod), - if dep then Context.extended_rel_vect 0 deparsign - else Context.extended_rel_vect 1 arsign) in + if dep then Context.Rel.to_extended_vect 0 deparsign + else Context.Rel.to_extended_vect 1 arsign) in let p = it_mkLambda_or_LetIn_name env' ((if dep then mkLambda_name env' else mkLambda) @@ -165,7 +164,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let base = applist (lift i pk,realargs) in if depK then Reduction.beta_appvect - base [|applist (mkRel (i+1), Context.extended_rel_list 0 sign)|] + base [|applist (mkRel (i+1), Context.Rel.to_extended_list 0 sign)|] else base | _ -> assert false @@ -237,7 +236,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> let realargs = List.skipn nparrec largs - and arg = appvect (mkRel (i+1), Context.extended_rel_vect 0 hyps) in + and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in applist(lift i fk,realargs@[arg]) | _ -> assert false in @@ -312,29 +311,29 @@ let mis_make_indrec env sigma listdepkind mib u = (* arity in the context of the fixpoint, i.e. P1..P_nrec f1..f_nbconstruct *) - let args = Context.extended_rel_list (nrec+nbconstruct) lnamesparrec in + let args = Context.Rel.to_extended_list (nrec+nbconstruct) lnamesparrec in let indf = make_ind_family((indi,u),args) in let arsign,_ = get_arity env indf in let depind = build_dependent_inductive env indf in let deparsign = (Anonymous,None,depind)::arsign in - let nonrecpar = rel_context_length lnonparrec in - let larsign = rel_context_length deparsign in + let nonrecpar = Context.Rel.length lnonparrec in + let larsign = Context.Rel.length deparsign in let ndepar = larsign - nonrecpar in let dect = larsign+nrec+nbconstruct in (* constructors in context of the Cases expr, i.e. P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *) - let args' = Context.extended_rel_list (dect+nrec) lnamesparrec in - let args'' = Context.extended_rel_list ndepar lnonparrec in + let args' = Context.Rel.to_extended_list (dect+nrec) lnamesparrec in + let args'' = Context.Rel.to_extended_list ndepar lnonparrec in let indf' = make_ind_family((indi,u),args'@args'') in let branches = let constrs = get_constructors env indf' in let fi = Termops.rel_vect (dect-i-nctyi) nctyi in let vecfi = Array.map - (fun f -> appvect (f, Context.extended_rel_vect ndepar lnonparrec)) + (fun f -> appvect (f, Context.Rel.to_extended_vect ndepar lnonparrec)) fi in Array.map3 @@ -355,9 +354,9 @@ let mis_make_indrec env sigma listdepkind mib u = let deparsign' = (Anonymous,None,depind')::arsign' in let pargs = - let nrpar = Context.extended_rel_list (2*ndepar) lnonparrec - and nrar = if dep then Context.extended_rel_list 0 deparsign' - else Context.extended_rel_list 1 arsign' + let nrpar = Context.Rel.to_extended_list (2*ndepar) lnonparrec + and nrar = if dep then Context.Rel.to_extended_list 0 deparsign' + else Context.Rel.to_extended_list 1 arsign' in nrpar@nrar in @@ -400,14 +399,14 @@ let mis_make_indrec env sigma listdepkind mib u = let typtyi = let concl = - let pargs = if dep then Context.extended_rel_vect 0 deparsign - else Context.extended_rel_vect 1 arsign + let pargs = if dep then Context.Rel.to_extended_vect 0 deparsign + else Context.Rel.to_extended_vect 1 arsign in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs) in it_mkProd_or_LetIn_name env concl deparsign in - mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp) + mrec (i+nctyi) (Context.Rel.nhyps arsign ::ln) (typtyi::ltyp) (deftyi::ldef) rest | [] -> let fixn = Array.of_list (List.rev ln) in @@ -428,7 +427,7 @@ let mis_make_indrec env sigma listdepkind mib u = else let recarg = (dest_subterms recargsvec.(tyi)).(j) in let recarg = recargpar@recarg in - let vargs = Context.extended_rel_list (nrec+i+j) lnamesparrec in + let vargs = Context.Rel.to_extended_list (nrec+i+j) lnamesparrec in let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in let p_0 = type_rec_branch @@ -442,7 +441,7 @@ let mis_make_indrec env sigma listdepkind mib u = in let rec put_arity env i = function | ((indi,u),_,_,dep,kinds)::rest -> - let indf = make_ind_family ((indi,u), Context.extended_rel_list i lnamesparrec) in + let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list i lnamesparrec) in let s = Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) evdref kinds diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index f429c51eb..1e3ff0fa2 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Termops open Declarations open Declareops @@ -142,12 +141,12 @@ let constructor_nallargs_env env ((kn,i),j) = let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *) let (mib,mip) = Global.lookup_inductive indsp in - mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) + 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) + rel_context_length (mib.mind_params_ctxt) + mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) (* Arity of constructors excluding params, excluding local defs *) @@ -213,21 +212,21 @@ let inductive_nparams_env env ind = let inductive_nparamdecls ind = let (mib,mip) = Global.lookup_inductive ind in - rel_context_length mib.mind_params_ctxt + Context.Rel.length mib.mind_params_ctxt let inductive_nparamdecls_env env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in - rel_context_length mib.mind_params_ctxt + Context.Rel.length mib.mind_params_ctxt (* Full length of arity (with local defs) *) let inductive_nalldecls ind = let (mib,mip) = Global.lookup_inductive ind in - rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls + Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls let inductive_nalldecls_env env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in - rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls + Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls (* Others *) @@ -249,13 +248,13 @@ let inductive_alldecls_env env (ind,u) = let constructor_has_local_defs (indsp,j) = let (mib,mip) = Global.lookup_inductive indsp in - let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) 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 l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls 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) @@ -273,11 +272,11 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in let ind_tags = - rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in + Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = Array.map2 (fun c n -> let d,_ = decompose_prod_assum c in - rel_context_tags (List.firstn n d)) + Context.Rel.to_tags (List.firstn n d)) mip.mind_nf_lc mip.mind_consnrealdecls in let print_info = { ind_tags; cstr_tags; style } in { ci_ind = ind; @@ -292,7 +291,7 @@ type constructor_summary = { cs_cstr : pconstructor; cs_params : constr list; cs_nargs : int; - cs_args : rel_context; + cs_args : Context.Rel.t; cs_concl_realargs : constr array } @@ -306,10 +305,10 @@ let lift_constructor n cs = { (* Accept either all parameters or only recursively uniform ones *) let instantiate_params t params sign = - let nnonrecpar = rel_context_nhyps sign - List.length params in + let nnonrecpar = Context.Rel.nhyps sign - List.length params in (* Adjust the signature if recursively non-uniform parameters are not here *) let _,sign = context_chop nnonrecpar sign in - let _,t = decompose_prod_n_assum (rel_context_length sign) t in + let _,t = decompose_prod_n_assum (Context.Rel.length sign) t in let subst = subst_of_rel_context_instance sign params in substl subst t @@ -323,7 +322,7 @@ let get_constructor ((ind,u as indu),mib,mip,params) j = let vargs = List.skipn (List.length params) allargs in { cs_cstr = (ith_constructor_of_inductive ind j,u); cs_params = params; - cs_nargs = rel_context_length args; + cs_nargs = Context.Rel.length args; cs_args = args; cs_concl_realargs = Array.of_list vargs } @@ -374,14 +373,14 @@ let build_dependent_constructor cs = applist (mkConstructU cs.cs_cstr, (List.map (lift cs.cs_nargs) cs.cs_params) - @(extended_rel_list 0 cs.cs_args)) + @(Context.Rel.to_extended_list 0 cs.cs_args)) let build_dependent_inductive env ((ind, params) as indf) = let arsign,_ = get_arity env indf in let nrealargs = List.length arsign in applist (mkIndU ind, - (List.map (lift nrealargs) params)@(extended_rel_list 0 arsign)) + (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign)) (* builds the arity of an elimination predicate in sort [s] *) @@ -506,7 +505,7 @@ let set_pattern_names env ind brv = let arities = Array.map (fun c -> - rel_context_length ((prod_assum c)) - + Context.Rel.length ((prod_assum c)) - mib.mind_nparams) mip.mind_nf_lc in Array.map2 (set_names env) arities brv diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 9036f521e..42a00a7e2 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Declarations open Environ open Evd @@ -92,12 +91,12 @@ val inductive_nparamdecls : inductive -> int val inductive_nparamdecls_env : env -> inductive -> int (** @return params context *) -val inductive_paramdecls : pinductive -> rel_context -val inductive_paramdecls_env : env -> pinductive -> rel_context +val inductive_paramdecls : pinductive -> Context.Rel.t +val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> rel_context -val inductive_alldecls_env : env -> pinductive -> rel_context +val inductive_alldecls : pinductive -> Context.Rel.t +val inductive_alldecls_env : env -> pinductive -> Context.Rel.t (** {7 Extract information from a constructor name} *) @@ -133,9 +132,9 @@ val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> type constructor_summary = { cs_cstr : pconstructor; (* internal name of the constructor plus universes *) - cs_params : constr list; (* parameters of the constructor in current ctx *) - cs_nargs : int; (* length of arguments signature (letin included) *) - cs_args : rel_context; (* signature of the arguments (letin included) *) + cs_params : constr list; (* parameters of the constructor in current ctx *) + cs_nargs : int; (* length of arguments signature (letin included) *) + cs_args : Context.Rel.t; (* signature of the arguments (letin included) *) cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *) } val lift_constructor : int -> constructor_summary -> constructor_summary @@ -148,11 +147,11 @@ val get_projections : env -> inductive_family -> constant array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> rel_context * sorts_family +val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : env -> bool -> inductive_family -> rel_context +val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 014828028..34191db34 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Context open Term open Globnames open Glob_term diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ce6d18985..6d9ed9a30 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,7 +28,6 @@ open Names open Evd open Term open Vars -open Context open Termops open Reductionops open Environ @@ -311,7 +310,7 @@ let ltac_interp_name_env k0 lvar env = specification of pretype which accepts to start with a non empty rel_context) *) (* tail is the part of the env enriched by pretyping *) - let n = rel_context_length (rel_context env) - k0 in + let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let env = pop_rel_context n env in let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in @@ -529,14 +528,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = (na,None,ty'.utj_val) in let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl + type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in - let ctxtv = Array.map (type_bl env empty_rel_context) bl in + type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in + let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = Array.map2 (fun e ar -> @@ -563,7 +562,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) let (ctxt,ty) = - decompose_prod_n_assum (rel_context_length ctxt) + decompose_prod_n_assum (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in let nenv = push_rel_context ctxt newenv in let j = pretype (mk_tycon ty) nenv evdref lvar def in @@ -884,7 +883,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let pred = nf_evar !evdref pred in let p = nf_evar !evdref p in let f cs b = - let n = rel_context_length cs.cs_args in + let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist (pi, [build_dependent_constructor cs]) in let csgn = @@ -1017,7 +1016,7 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function let ise_pretype_gen flags env sigma lvar kind c = let evdref = ref sigma in - let k0 = rel_context_length (rel_context env) in + let k0 = Context.Rel.length (rel_context env) in let c' = match kind with | WithoutTypeConstraint -> (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val @@ -1059,7 +1058,7 @@ let on_judgment f j = let understand_judgment env sigma c = let evdref = ref sigma in - let k0 = rel_context_length (rel_context env) in + let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in let j = on_judgment (fun c -> let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in @@ -1067,7 +1066,7 @@ let understand_judgment env sigma c = in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = - let k0 = rel_context_length (rel_context env) in + let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment (fun c -> let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3f02e4bfb..f59f88032 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -11,7 +11,6 @@ open Util open Names open Term open Vars -open Context open Termops open Univ open Evd @@ -1466,17 +1465,17 @@ let splay_prod_assum env sigma = match kind_of_term t with | Prod (x,t,c) -> prodec_rec (push_rel (x,None,t) env) - (add_rel_decl (x, None, t) l) c + (Context.Rel.add (x, None, t) l) c | LetIn (x,b,t,c) -> prodec_rec (push_rel (x, Some b, t) env) - (add_rel_decl (x, Some b, t) l) c + (Context.Rel.add (x, Some b, t) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> let t' = whd_betadeltaiota env sigma t in if Term.eq_constr t t' then l,t else prodec_rec env l t' in - prodec_rec env empty_rel_context + prodec_rec env Context.Rel.empty let splay_arity env sigma c = let l, c = splay_prod env sigma c in @@ -1491,20 +1490,20 @@ let splay_prod_n env sigma n = match kind_of_term (whd_betadeltaiota env sigma c) with | Prod (n,a,c0) -> decrec (push_rel (n,None,a) env) - (m-1) (add_rel_decl (n,None,a) ln) c0 + (m-1) (Context.Rel.add (n,None,a) ln) c0 | _ -> invalid_arg "splay_prod_n" in - decrec env n empty_rel_context + decrec env n Context.Rel.empty let splay_lam_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Lambda (n,a,c0) -> decrec (push_rel (n,None,a) env) - (m-1) (add_rel_decl (n,None,a) ln) c0 + (m-1) (Context.Rel.add (n,None,a) ln) c0 | _ -> invalid_arg "splay_lam_n" in - decrec env n empty_rel_context + decrec env n Context.Rel.empty let is_sort env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 43c98bbd4..5195784a4 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Univ open Evd open Environ @@ -218,10 +217,10 @@ val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts val sort_of_arity : env -> evar_map -> constr -> sorts -val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr -val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr +val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr +val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr val splay_prod_assum : - env -> evar_map -> constr -> rel_context * constr + env -> evar_map -> constr -> Context.Rel.t * constr val is_sort : env -> evar_map -> types -> bool type 'a miota_args = { diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 89ba46dbc..70345c509 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -8,7 +8,6 @@ open Term open Evd -open Context open Environ (** This family of functions assumes its constr argument is known to be @@ -44,6 +43,6 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> val type_of_global_reference_knowing_conclusion : env -> evar_map -> constr -> types -> evar_map * types -val sorts_of_context : env -> evar_map -> rel_context -> sorts list +val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index deb03f516..c4f22987f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -12,7 +12,6 @@ open Globnames open Decl_kinds open Term open Vars -open Context open Evd open Util open Typeclasses_errors @@ -59,10 +58,10 @@ type typeclass = { cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : (global_reference * bool) option list * rel_context; + cl_context : (global_reference * bool) option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) - cl_props : rel_context; + cl_props : Context.Rel.t; (* The method implementaions as projections. *) cl_projs : (Name.t * (direction * int option) option * constant option) list; @@ -127,7 +126,7 @@ let typeclass_univ_instance (cl,u') = in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') in - let subst_ctx = Context.map_rel_context (subst_univs_level_constr subst) in + let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context); cl_props = subst_ctx cl.cl_props}, u' @@ -204,7 +203,7 @@ let discharge_class (_,cl) = (decl :: ctx', n :: subst) ) ctx ([], []) in let discharge_rel_context subst n rel = - let rel = map_rel_context (Cooking.expmod_constr repl) rel in + let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in let ctx, _ = List.fold_right (fun (id, b, t) (ctx, k) -> @@ -287,7 +286,7 @@ let build_subclasses ~check env sigma glob pri = | None -> [] | Some (rels, ((tc,u), args)) -> let instapp = - Reductionops.whd_beta sigma (appvectc c (Context.extended_rel_vect 0 rels)) + Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels)) in let projargs = Array.of_list (args @ [instapp]) in let projs = List.map_filter diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index b3170b970..f56af19a0 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -9,7 +9,6 @@ open Names open Globnames open Term -open Context open Evd open Environ @@ -24,10 +23,10 @@ type typeclass = { (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the typeclass argument is a direct superclass and the global reference gives a direct link to the class itself. *) - cl_context : (global_reference * bool) option list * rel_context; + cl_context : (global_reference * bool) option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) - cl_props : rel_context; + cl_props : Context.Rel.t; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if @@ -68,7 +67,7 @@ val dest_class_app : env -> constr -> typeclass puniverses * constr list val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : constr -> (rel_context * (typeclass puniverses * constr list)) option +val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option val instance_impl : instance -> global_reference diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 585f066db..7a918ee87 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,7 +9,6 @@ (*i*) open Names open Term -open Context open Environ open Constrexpr open Globnames @@ -20,7 +19,7 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *) + | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 7982fc852..b72d4db63 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -9,7 +9,6 @@ open Loc open Names open Term -open Context open Environ open Constrexpr open Globnames @@ -19,7 +18,7 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * Id.t located (** Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *) + | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *) exception TypeClassError of env * typeclass_error @@ -27,5 +26,5 @@ val not_a_class : env -> constr -> 'a val unbound_method : env -> global_reference -> Id.t located -> 'a -val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a +val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e8a0df484..b42a70b34 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1582,7 +1582,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = | AllOccurrences, InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in - if Context.eq_named_declaration d newdecl + if Context.Named.Declaration.equal d newdecl && not (indirectly_dependent c d depdecls) then if check_occs && not (in_every_hyp occs) @@ -1634,7 +1634,7 @@ type abstraction_request = type 'r abstraction_result = Names.Id.t * named_context_val * - Context.named_declaration list * Names.Id.t option * + Context.Named.Declaration.t list * Names.Id.t option * types * (constr, 'r) Sigma.sigma option let make_abstraction env evd ccl abs = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 51a51f375..14bcb4a06 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -77,7 +77,7 @@ val finish_evar_resolution : ?flags:Pretyping.inference_flags -> type 'r abstraction_result = Names.Id.t * named_context_val * - Context.named_declaration list * Names.Id.t option * + Context.Named.Declaration.t list * Names.Id.t option * types * (constr, 'r) Sigma.sigma option val make_abstraction : env -> 'r Sigma.t -> constr -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c59e085e5..38eea9170 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -53,7 +53,7 @@ let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in - let ndecls = Context.rel_context_length mib.mind_params_ctxt in + let ndecls = Context.Rel.length mib.mind_params_ctxt in if Int.equal ndecls 0 then ctyp else let _,ctyp = decompose_prod_n_assum ndecls ctyp in diff --git a/printing/printer.ml b/printing/printer.ml index 2e112f9ac..773127c77 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -293,7 +293,7 @@ let pr_named_context_of env sigma = hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_named_context env sigma ne_context = - hv 0 (Context.fold_named_context + hv 0 (Context.Named.fold_outside (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) ne_context ~init:(mt ())) @@ -306,7 +306,7 @@ let pr_rel_context_of env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env sigma = let sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d pps -> let pidt = pr_var_list_decl env sigma d in (pps ++ fnl () ++ pidt)) @@ -333,7 +333,7 @@ let pr_context_limit n env sigma = else let k = lgsign-n in let _,sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d (i,pps) -> if i < k then (i+1, (pps ++str ".")) @@ -726,7 +726,7 @@ let prterm = pr_lconstr type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (* An opaque constant. *) | Transparent of constant diff --git a/printing/printer.mli b/printing/printer.mli index 5c60b8936..bdb295a47 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -10,7 +10,6 @@ open Pp open Names open Globnames open Term -open Context open Environ open Pattern open Evd @@ -109,13 +108,13 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds -val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds -val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds -val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds +val pr_var_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds +val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds +val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds -val pr_named_context : env -> evar_map -> named_context -> std_ppcmds +val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds val pr_named_context_of : env -> evar_map -> std_ppcmds -val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds +val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds val pr_rel_context_of : env -> evar_map -> std_ppcmds val pr_context_of : env -> evar_map -> std_ppcmds @@ -165,7 +164,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) type context_object = | Variable of Id.t (** A section variable or a Let definition *) (** An axiom and the type it inhabits (if an axiom of the empty type) *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (** An opaque constant. *) | Transparent of constant (** A transparent constant *) diff --git a/printing/printmod.ml b/printing/printmod.ml index d6f847cc7..d277d3782 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,7 +65,6 @@ let get_new_id locals id = (** Inductive declarations *) -open Context open Termops open Reduction @@ -90,7 +89,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = extended_rel_list 0 params in + let args = Context.Rel.to_extended_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in @@ -144,7 +143,7 @@ let print_record env mind mib = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = extended_rel_list 0 params in + let args = Context.Rel.to_extended_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist env cstrtypes.(0) args in diff --git a/proofs/goal.mli b/proofs/goal.mli index a00a95a2f..46318b789 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -67,7 +67,7 @@ module V82 : sig val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma + val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/proofs/logic.ml b/proofs/logic.ml index 1ba14e7d4..e80f5a64c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Environ open Reductionops diff --git a/proofs/logic.mli b/proofs/logic.mli index d034b73c5..d33f56bb7 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -53,4 +53,4 @@ exception RefinerError of refiner_error val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> - Context.named_declaration -> Environ.named_context_val + Context.Named.Declaration.t -> Environ.named_context_val diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 9f2a00135..155b2cfca 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -215,7 +215,7 @@ let solve_by_implicit_tactic env sigma evk = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try diff --git a/proofs/proofview.mli b/proofs/proofview.mli index a92abcbbf..aac56e565 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -446,7 +446,7 @@ module Goal : sig environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) val concl : ([ `NF ], 'r) t -> Term.constr - val hyps : ([ `NF ], 'r) t -> Context.named_context + val hyps : ([ `NF ], 'r) t -> Context.Named.t val env : ('a, 'r) t -> Environ.env val sigma : ('a, 'r) t -> 'r Sigma.t val extra : ('a, 'r) t -> Evd.Store.t diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ba62b2cb2..de7025062 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -197,10 +197,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.named_context = pf_hyps goal in + let oldhyps:Context.Named.t = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.named_context list = + let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in let newhyps = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index a81555ff5..2959787d4 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Context open Evd open Proof_type @@ -16,7 +15,7 @@ val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 57c60cbee..dc0cf81a7 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -48,7 +48,7 @@ let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = try - Context.lookup_named id (pf_hyps gls) + Context.Named.lookup id (pf_hyps gls) with Not_found -> raise (RefinerError (NoSuchHyp id)) @@ -198,7 +198,7 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.hyps gl in let sign = - try Context.lookup_named id hyps + try Context.Named.lookup id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index c45fd250c..b7915e837 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ open Evd open Proof_type @@ -34,18 +33,18 @@ val apply_sig_tac : val pf_concl : goal sigma -> types val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t (*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> named_declaration +val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> named_declaration +val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t @@ -123,9 +122,9 @@ module New : sig val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration + val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types diff --git a/tactics/auto.ml b/tactics/auto.ml index 4fb4b3263..a170c27fb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -327,7 +327,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let env = Proofview.Goal.env gl in let nf c = Evarutil.nf_evar sigma c in let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in - let hyp = Context.map_named_declaration nf decl in + let hyp = Context.Named.Declaration.map nf decl in let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list env sigma hintl local_db) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 64a68ba6b..2c713a021 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -49,7 +49,6 @@ open Util open Names open Term open Vars -open Context open Declarations open Environ open Inductive @@ -71,8 +70,8 @@ let build_dependent_inductive ind (mib,mip) = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist (mkIndU ind, - extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt - @ extended_rel_list 0 realargs) + Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt + @ Context.Rel.to_extended_list 0 realargs) let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s @@ -109,7 +108,7 @@ let get_sym_eq_data env (ind,u) = error "Inductive equalities with local definitions in arity not supported."; let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; (* This can be relaxed... *) let params,constrargs = List.chop mib.mind_nparams constrargs in if mip.mind_nrealargs > mib.mind_nparams then @@ -144,7 +143,7 @@ let get_non_sym_eq_data env (ind,u) = error "Inductive equalities with local definitions in arity not supported"; let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let _,constrargs = List.chop mib.mind_nparams constrargs in let constrargs = List.map (Vars.subst_instance_constr u) constrargs in @@ -170,7 +169,7 @@ let build_sym_scheme env ind = let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n = - mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in + mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let applied_ind = build_dependent_inductive indu specif in let realsign_ind = @@ -183,7 +182,7 @@ let build_sym_scheme env ind = my_it_mkLambda_or_LetIn_name (lift_rel_context (nrealargs+1) realsign_ind) (mkApp (mkIndU indu,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect 1 nrealargs; rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), @@ -224,13 +223,13 @@ let build_sym_involutive_scheme env ind = get_sym_eq_data env indu in let eq,eqrefl,ctx = get_coq_eq ctx in let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in - let cstr n = mkApp (mkConstructUi (indu,1),extended_rel_vect n paramsctxt) in + let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let applied_ind = build_dependent_inductive indu specif in let applied_ind_C = mkApp (mkIndU indu, Array.append - (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt) + (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt) (rel_vect (nrealargs+1) nrealargs)) in let realsign_ind = name_context env ((Name varH,None,applied_ind)::realsign) in @@ -244,15 +243,15 @@ let build_sym_involutive_scheme env ind = (mkApp (eq,[| mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect (2*nrealargs+2) nrealargs; rel_vect 1 nrealargs]); mkApp (sym,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect 1 nrealargs; rel_vect (2*nrealargs+2) nrealargs; [|mkApp (sym,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect (2*nrealargs+2) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]])|]]); @@ -335,7 +334,7 @@ let build_l2r_rew_scheme dep env ind kind = let eq,eqrefl,ctx = get_coq_eq ctx in let cstr n p = mkApp (mkConstructUi(indu,1), - Array.concat [extended_rel_vect n paramsctxt1; + Array.concat [Context.Rel.to_extended_vect n paramsctxt1; rel_vect p nrealargs]) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in @@ -343,12 +342,12 @@ let build_l2r_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let applied_ind_P = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1; rel_vect 0 nrealargs; rel_vect nrealargs nrealargs]) in let applied_ind_G = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+3) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1; rel_vect (nrealargs+3) nrealargs; rel_vect 0 nrealargs]) in let realsign_P = lift_rel_context nrealargs realsign in @@ -359,10 +358,10 @@ let build_l2r_rew_scheme dep env ind kind = lift_rel_context (nrealargs+3) realsign) in let applied_sym_C n = mkApp(sym, - Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in + Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in let applied_sym_G = mkApp(sym, - Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1; + Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1; rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]]) in @@ -372,7 +371,7 @@ let build_l2r_rew_scheme dep env ind kind = let ci = make_case_info (Global.env()) ind RegularStyle in let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in let applied_PC = - mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign) + mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign) (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in let applied_PG = mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs) @@ -382,11 +381,11 @@ let build_l2r_rew_scheme dep env ind kind = (if dep then [|mkRel 2|] else [||])) in let applied_sym_sym = mkApp (sym,Array.concat - [extended_rel_vect (2*nrealargs+4) paramsctxt1; + [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1; rel_vect 4 nrealargs; rel_vect (nrealargs+4) nrealargs; [|mkApp (sym,Array.concat - [extended_rel_vect (2*nrealargs+4) paramsctxt1; + [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1; rel_vect (nrealargs+4) nrealargs; rel_vect 4 nrealargs; [|mkRel 2|]])|]]) in @@ -409,7 +408,7 @@ let build_l2r_rew_scheme dep env ind kind = mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]), applied_PR)), mkApp (sym_involutive, - Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]), + Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]), [|main_body|]) else main_body)))))) @@ -448,7 +447,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = get_sym_eq_data env indu in let cstr n p = mkApp (mkConstructUi(indu,1), - Array.concat [extended_rel_vect n paramsctxt1; + Array.concat [Context.Rel.to_extended_vect n paramsctxt1; rel_vect p nrealargs]) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in @@ -456,12 +455,12 @@ let build_l2r_forward_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let applied_ind_P = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (4*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1; rel_vect 0 nrealargs; rel_vect (nrealargs+1) nrealargs]) in let applied_ind_P' = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+1) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1; rel_vect 0 nrealargs; rel_vect (2*nrealargs+1) nrealargs]) in let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in @@ -539,7 +538,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) = get_non_sym_eq_data env indu in let cstr n = - mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in + mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in let constrargs_cstr = constrargs@[cstr 0] in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in @@ -555,8 +554,8 @@ let build_r2l_forward_rew_scheme dep env ind kind = applist (mkVar varP,if dep then constrargs_cstr else constrargs) in let applied_PG = mkApp (mkVar varP, - if dep then extended_rel_vect 0 realsign_ind - else extended_rel_vect 1 realsign) in + if dep then Context.Rel.to_extended_vect 0 realsign_ind + else Context.Rel.to_extended_vect 1 realsign) in let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign_ind @@ -600,12 +599,12 @@ let fix_r2l_forward_rew_scheme (c, ctx') = | hp :: p :: ind :: indargs -> let c' = my_it_mkLambda_or_LetIn indargs - (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p) - (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp) - (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind) + (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 1) p) + (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 2) hp) + (mkLambda_or_LetIn (Context.Rel.Declaration.map (lift 2) ind) (Reductionops.whd_beta Evd.empty (applist (c, - extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) + Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) in c', ctx' | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme") @@ -744,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind = let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then + if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in let varB = fresh env (Id.of_string "B") in @@ -760,8 +759,8 @@ let build_congr env (eq,refl,ctx) ind = (mkNamedLambda varH (applist (mkIndU indu, - extended_rel_list (mip.mind_nrealargs+2) paramsctxt @ - extended_rel_list 0 realsign)) + Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @ + Context.Rel.to_extended_list 0 realsign)) (mkCase (ci, my_it_mkLambda_or_LetIn_name (lift_rel_context (mip.mind_nrealargs+3) realsign) @@ -769,9 +768,9 @@ let build_congr env (eq,refl,ctx) ind = (Anonymous, applist (mkIndU indu, - extended_rel_list (2*mip.mind_nrealdecls+3) + Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3) paramsctxt - @ extended_rel_list 0 realsign), + @ Context.Rel.to_extended_list 0 realsign), mkApp (eq, [|mkVar varB; mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]); diff --git a/tactics/equality.ml b/tactics/equality.ml index 92ebcb272..7d15e9ee6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1574,7 +1574,7 @@ let unfold_body x = Proofview.Goal.enter { enter = begin fun gl -> (** We normalize the given hypothesis immediately. *) let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let (_, xval, _) = Context.lookup_named x hyps in + let (_, xval, _) = Context.Named.lookup x hyps in let xval = match xval with | None -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") @@ -1656,7 +1656,7 @@ let subst_one_var dep_proof_ok x = (** [is_eq_x] ensures nf_evar on its side *) let hyps = Proofview.Goal.hyps gl in let test hyp _ = is_eq_x gl varx hyp in - Context.fold_named_context test ~init:() hyps; + Context.Named.fold_outside test ~init:() hyps; errorlabstrm "Subst" (str "Cannot find any non-recursive equality over " ++ pr_id x ++ str".") diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 92682fc7a..f311e47f6 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -315,7 +315,7 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in + let c = Reductionops.whd_beta Evd.empty (mkApp (c, Context.Rel.to_extended_vect 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in let id = diff --git a/tactics/hints.mli b/tactics/hints.mli index 3a0521f66..b48fb776e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -10,7 +10,6 @@ open Pp open Util open Names open Term -open Context open Environ open Globnames open Decl_kinds @@ -192,7 +191,7 @@ val make_resolves : If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : - env -> evar_map -> named_declaration -> hint_entry list + env -> evar_map -> Context.Named.Declaration.t -> hint_entry list (** [make_extern pri pattern tactic_expr] *) diff --git a/tactics/inv.ml b/tactics/inv.ml index ed1a62795..3574990f6 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Namegen open Environ @@ -97,7 +96,7 @@ let make_inv_predicate env evd indf realargs id status concl = (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) in - let nhyps = rel_context_length hyps in + let nhyps = Context.Rel.length hyps in let env' = push_rel_context hyps env in (* Now the arity is pushed, and we need to construct the pairs * ai,mkRel(n-i+1) *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 75e69bc09..9154c50c8 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -14,7 +14,6 @@ open Term open Vars open Termops open Namegen -open Context open Evd open Printer open Reductionops @@ -157,7 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = fold_named_context (fun env (id,_,_ as d) (revargs,hyps) -> if Id.List.mem id ivars then - ((mkVar id)::revargs,add_named_decl d hyps) + ((mkVar id)::revargs, Context.Named.add d hyps) else (revargs,hyps)) env ~init:([],[]) @@ -206,8 +205,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = fold_named_context (fun env (id,_,_ as d) sign -> if mem_named_context id global_named_context then sign - else add_named_decl d sign) - invEnv ~init:empty_named_context + else Context.Named.add d sign) + invEnv ~init:Context.Named.empty end in let avoid = ref [] in let { sigma=sigma } = Proof.V82.subgoals pf in @@ -218,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let h = next_ident_away (Id.of_string "H") !avoid in let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in avoid := h::!avoid; - ownSign := add_named_decl (h,None,ty) !ownSign; + ownSign := Context.Named.add (h,None,ty) !ownSign; applist (mkVar h, inst) | _ -> map_constr fill_holes c in diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 40a18ac45..1de47b2be 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -71,7 +71,7 @@ val cl_rewrite_clause : bool -> Locus.occurrences -> Id.t option -> tactic val is_applied_rewrite_relation : - env -> evar_map -> Context.rel_context -> constr -> types option + env -> evar_map -> Context.Rel.t -> constr -> types option val declare_relation : ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t -> diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli index d8e6dd0ae..090207bcc 100644 --- a/tactics/tactic_matching.mli +++ b/tactics/tactic_matching.mli @@ -43,7 +43,7 @@ val match_term : val match_goal: Environ.env -> Evd.evar_map -> - Context.named_context -> + Context.Named.t -> Term.constr -> (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index e181c8e14..aaef0f072 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -12,7 +12,6 @@ open Util open Names open Term open Termops -open Context open Declarations open Tacmach open Clenv @@ -154,8 +153,8 @@ type branch_args = { branchnames : Tacexpr.intro_patterns} type branch_assumptions = { - ba : branch_args; (* the branch args *) - assums : named_context} (* the list of assumptions introduced *) + ba : branch_args; (* the branch args *) + assums : Context.Named.t} (* the list of assumptions introduced *) let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 80e01a8d0..d8aa3161e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -9,7 +9,6 @@ open Pp open Names open Term -open Context open Tacmach open Proof_type open Tacexpr @@ -60,29 +59,29 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic val onNthHypId : int -> (Id.t -> tactic) -> tactic val onNthHyp : int -> (constr -> tactic) -> tactic -val onNthDecl : int -> (named_declaration -> tactic) -> tactic +val onNthDecl : int -> (Context.Named.Declaration.t -> tactic) -> tactic val onLastHypId : (Id.t -> tactic) -> tactic val onLastHyp : (constr -> tactic) -> tactic -val onLastDecl : (named_declaration -> tactic) -> tactic +val onLastDecl : (Context.Named.Declaration.t -> tactic) -> tactic val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic val onNLastHyps : int -> (constr list -> tactic) -> tactic -val onNLastDecls : int -> (named_context -> tactic) -> tactic +val onNLastDecls : int -> (Context.Named.t -> tactic) -> tactic val lastHypId : goal sigma -> Id.t val lastHyp : goal sigma -> constr -val lastDecl : goal sigma -> named_declaration +val lastDecl : goal sigma -> Context.Named.Declaration.t val nLastHypsId : int -> goal sigma -> Id.t list val nLastHyps : int -> goal sigma -> constr list -val nLastDecls : int -> goal sigma -> named_context +val nLastDecls : int -> goal sigma -> Context.Named.t -val afterHyp : Id.t -> goal sigma -> named_context +val afterHyp : Id.t -> goal sigma -> Context.Named.t val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> tactic) -> (Id.t -> tactic) -> Id.t -> tactic -val onHyps : (goal sigma -> named_context) -> - (named_context -> tactic) -> tactic +val onHyps : (goal sigma -> Context.Named.t) -> + (Context.Named.t -> tactic) -> tactic (** {6 Tacticals applying to goal components } *) @@ -99,18 +98,18 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) type branch_args = { - ity : pinductive; (** the type we were eliminating on *) + ity : pinductive; (** the type we were eliminating on *) largs : constr list; (** its arguments *) branchnum : int; (** the branch number *) pred : constr; (** the predicate we used *) nassums : int; (** the number of assumptions to be introduced *) branchsign : bool list; (** the signature of the branch. - true=recursive argument, false=constant *) + true=recursive argument, false=constant *) branchnames : intro_patterns} type branch_assumptions = { - ba : branch_args; (** the branch args *) - assums : named_context} (** the list of assumptions introduced *) + ba : branch_args; (** the branch args *) + assums : Context.Named.t} (** the list of assumptions introduced *) (** [check_disjunctive_pattern_size loc pats n] returns an appropriate error message if |pats| <> n *) @@ -223,7 +222,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context + val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> @@ -232,11 +231,11 @@ module New : sig val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic val onLastHypId : (identifier -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic - val onLastDecl : (named_declaration -> unit tactic) -> unit tactic + val onLastDecl : (Context.Named.Declaration.t -> unit tactic) -> unit tactic - val onHyps : ([ `NF ], named_context) Proofview.Goal.enter -> - (named_context -> unit tactic) -> unit tactic - val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic + val onHyps : ([ `NF ], Context.Named.t) Proofview.Goal.enter -> + (Context.Named.t -> unit tactic) -> unit tactic + val afterHyp : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic val tryAllHyps : (identifier -> unit tactic) -> unit tactic val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2e7adc513..f2319804e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Find_subterm open Namegen @@ -1405,7 +1404,7 @@ let make_projection env sigma params cstr sign elim i n c u = then let t = lift (i+1-n) t in let abselim = beta_applist (elim,params@[t;branch]) in - let c = beta_applist (abselim, [mkApp (c, extended_rel_vect 0 sign)]) in + let c = beta_applist (abselim, [mkApp (c, Context.Rel.to_extended_vect 0 sign)]) in Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign) else None @@ -1413,7 +1412,7 @@ let make_projection env sigma params cstr sign elim i n c u = (* goes from left to right when i increases! *) match List.nth l i with | Some proj -> - let args = extended_rel_vect 0 sign in + let args = Context.Rel.to_extended_vect 0 sign in let proj = if Environ.is_projection proj env then mkProj (Projection.make proj false, mkApp (c, args)) @@ -2528,7 +2527,7 @@ let bring_hyps hyps = let store = Proofview.Goal.extra gl in let concl = Tacmach.New.pf_nf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in - let args = Array.of_list (instance_from_named_context hyps) in + let args = Array.of_list (Context.Named.to_instance hyps) in Proofview.Refine.refine { run = begin fun sigma -> let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newcl in @@ -2589,7 +2588,7 @@ let generalize_dep ?(with_let=false) c gl = d::toquant else toquant in - let to_quantify = Context.fold_named_context seek sign ~init:[] in + let to_quantify = Context.Named.fold_outside seek sign ~init:[] in let to_quantify_rev = List.rev to_quantify in let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in @@ -2609,7 +2608,7 @@ let generalize_dep ?(with_let=false) c gl = in let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',project gl) in - let args = instance_from_named_context to_quantify_rev in + let args = Context.Named.to_instance to_quantify_rev in tclTHENLIST [tclEVARS evd; apply_type cl'' (if Option.is_empty body then c::args else args); @@ -2687,7 +2686,7 @@ let quantify lconstr = let unfold_body x gl = let hyps = pf_hyps gl in let xval = - match Context.lookup_named x hyps with + match Context.Named.lookup x hyps with (_,Some xval,_) -> xval | _ -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") in @@ -3108,20 +3107,20 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) - nparams: int; (* number of parameters *) - predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) - npredicates: int; (* Number of predicates *) - branches: rel_context; (* branchr,...,branch1 *) - nbranches: int; (* Number of branches *) - args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *) - nargs: int; (* number of arguments *) - indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) - if HI is in premisses, None otherwise *) - concl: types; (* Qi x1...xni HI (f...), HI and (f...) - are optional and mutually exclusive *) - indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) - farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) + params: Context.Rel.t; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + nparams: int; (* number of parameters *) + predicates: Context.Rel.t; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + npredicates: int; (* Number of predicates *) + branches: Context.Rel.t; (* branchr,...,branch1 *) + nbranches: int; (* Number of branches *) + args: Context.Rel.t; (* (xni, Ti_ni) ... (x1, Ti_1) *) + nargs: int; (* number of arguments *) + indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni) + if HI is in premisses, None otherwise *) + concl: types; (* Qi x1...xni HI (f...), HI and (f...) + are optional and mutually exclusive *) + indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) + farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) } let empty_scheme = @@ -3280,7 +3279,7 @@ let hyps_of_vars env sign nogen hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = - Context.fold_named_context_reverse + Context.Named.fold_inside (fun (hs,hl) (x,_,_ as d) -> if Id.Set.mem x nogen then (hs,hl) else if Id.Set.mem x hs then (hs,x::hl) @@ -3511,7 +3510,7 @@ let occur_rel n c = We also return the conclusion. *) let decompose_paramspred_branch_args elimt = - let rec cut_noccur elimt acc2 : rel_context * rel_context * types = + let rec cut_noccur elimt acc2 : Context.Rel.t * Context.Rel.t * types = match kind_of_term elimt with | Prod(nme,tpe,elimt') -> let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in @@ -3520,7 +3519,7 @@ let decompose_paramspred_branch_args elimt = else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl | App(_, _) | Rel _ -> acc2 , [] , elimt | _ -> error_ind_scheme "" in - let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types = + let rec cut_occur elimt acc1 : Context.Rel.t * Context.Rel.t * Context.Rel.t * types = match kind_of_term elimt with | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1) | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl @@ -3648,7 +3647,7 @@ let compute_scheme_signature scheme names_info ind_type_guess = let ind_is_ok = List.equal Term.eq_constr (List.lastn scheme.nargs indargs) - (extended_rel_list 0 scheme.args) in + (Context.Rel.to_extended_list 0 scheme.args) in if not (ccl_arg_ok && ind_is_ok) then error_ind_scheme "the conclusion of" in (cond, check_concl) @@ -4563,10 +4562,10 @@ let abstract_subproof id gk tac = List.fold_right (fun (id,_,_ as d) (s1,s2) -> if mem_named_context id current_sign && - interpretable_as_section_decl evdref (Context.lookup_named id current_sign) d + interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d then (s1,push_named_context_val d s2) - else (add_named_decl d s1,s2)) - global_sign (empty_named_context,empty_named_context_val) in + else (Context.Named.add d s1,s2)) + global_sign (Context.Named.empty, empty_named_context_val) in let id = next_global_ident_away id (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in let concl = @@ -4594,7 +4593,7 @@ let abstract_subproof id gk tac = in let const, args = if !shrink_abstract then shrink_entry sign const - else (const, List.rev (instance_from_named_context sign)) + else (const, List.rev (Context.Named.to_instance sign)) in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f5695ff06..873a11bd2 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -9,7 +9,6 @@ open Loc open Names open Term -open Context open Environ open Proof_type open Evd @@ -33,9 +32,9 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool val introduction : ?check:bool -> Id.t -> unit Proofview.tactic val refine : constr -> tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic -val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic +val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic -val convert_hyp_no_check : named_declaration -> unit Proofview.tactic +val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic val thin : Id.t list -> tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> tactic @@ -50,7 +49,7 @@ val convert_leq : constr -> constr -> unit Proofview.tactic val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t -val find_intro_names : rel_context -> goal sigma -> Id.t list +val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic @@ -180,7 +179,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) val apply_type : constr -> constr list -> tactic -val bring_hyps : named_context -> unit Proofview.tactic +val bring_hyps : Context.Named.t -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic @@ -239,20 +238,20 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) - nparams: int; (** number of parameters *) - predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) - npredicates: int; (** Number of predicates *) - branches: rel_context; (** branchr,...,branch1 *) - nbranches: int; (** Number of branches *) - args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *) - nargs: int; (** number of arguments *) - indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni) - if HI is in premisses, None otherwise *) - concl: types; (** Qi x1...xni HI (f...), HI and (f...) - are optional and mutually exclusive *) - indarg_in_concl: bool; (** true if HI appears at the end of conclusion *) - farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) + params: Context.Rel.t; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + nparams: int; (** number of parameters *) + predicates: Context.Rel.t; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + npredicates: int; (** Number of predicates *) + branches: Context.Rel.t; (** branchr,...,branch1 *) + nbranches: int; (** Number of branches *) + args: Context.Rel.t; (** (xni, Ti_ni) ... (x1, Ti_1) *) + nargs: int; (** number of arguments *) + indarg: Context.Rel.Declaration.t option; (** Some (H,I prm1..prmp x1...xni) + if HI is in premisses, None otherwise *) + concl: types; (** Qi x1...xni HI (f...), HI and (f...) + are optional and mutually exclusive *) + indarg_in_concl: bool; (** true if HI appears at the end of conclusion *) + farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) } val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index a71588fe0..470485438 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -141,7 +141,7 @@ let label_of = function | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn) | VarRef id -> Label.of_id id -let push (r : Context.rel_declaration) (ctx : Context.rel_context) = r :: ctx +let push (r : Context.Rel.Declaration.t) (ctx : Context.Rel.t) = r :: ctx let rec traverse current ctx accu t = match kind_of_term t with | Var id -> diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli index 9c9f81bd2..61beb26c8 100644 --- a/toplevel/assumptions.mli +++ b/toplevel/assumptions.mli @@ -22,7 +22,7 @@ open Printer val traverse : Label.t -> constr -> (Refset_env.t * Refset_env.t Refmap_env.t * - (label * Context.rel_context * types) list Refmap_env.t) + (label * Context.Rel.t * types) list Refmap_env.t) (** Collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type). The above warning of diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 98686fb1b..56106928e 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -15,7 +15,6 @@ open Util open Pp open Term open Vars -open Context open Termops open Declarations open Names @@ -103,7 +102,7 @@ let mkFullInd (ind,u) n = context_chop (nparams-nparrec) mib.mind_params_ctxt in if nparrec > 0 then mkApp (mkIndU (ind,u), - Array.of_list(extended_rel_list (nparrec+n) lnamesparrec)) + Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec)) else mkIndU (ind,u) let check_bool_is_defined () = @@ -138,7 +137,7 @@ let build_beq_scheme mode kn = | Name s -> Id.of_string ("eq_"^(Id.to_string s)) | Anonymous -> Id.of_string "eq_A" in - let ext_rel_list = extended_rel_list 0 lnamesparrec in + let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in let lift_cnt = ref 0 in let eqs_typ = List.map (fun aa -> let a = lift !lift_cnt aa in @@ -234,7 +233,7 @@ let build_beq_scheme mode kn = Cn => match Y with ... end |] part *) let ci = make_case_info env (fst ind) MatchStyle in let constrs n = get_constructors env (make_ind_family (ind, - extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in + Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (Lazy.force ff) in diff --git a/toplevel/class.ml b/toplevel/class.ml index 22baa5e61..28a39b570 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -12,7 +12,6 @@ open Pp open Names open Term open Vars -open Context open Termops open Entries open Environ @@ -198,13 +197,13 @@ let build_id_coercion idf_opt source poly = let val_f = it_mkLambda_or_LetIn (mkLambda (Name Namegen.default_dependent_ident, - applistc vs (extended_rel_list 0 lams), + applistc vs (Context.Rel.to_extended_list 0 lams), mkRel 1)) lams in let typ_f = it_mkProd_wo_LetIn - (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t)) + (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t)) lams in (* juste pour verification *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 9cdb46064..ab18350c5 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -351,7 +351,7 @@ let context poly l = let evars = ref (Evd.from_env env) in let _, ((env', fullctx), impls) = interp_context_evars env evars l in let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in - let fullctx = Context.map_rel_context subst fullctx in + let fullctx = Context.Rel.map subst fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in let ctx = diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 2b7e9e4fe..80ed24629 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Context open Environ open Constrexpr open Typeclasses @@ -15,9 +14,9 @@ open Libnames (** Errors *) -val mismatched_params : env -> constr_expr list -> rel_context -> 'a +val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a -val mismatched_props : env -> constr_expr list -> rel_context -> 'a +val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a (** Instance declaration *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 91cfddb54..500769aca 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -12,7 +12,6 @@ open Util open Flags open Term open Vars -open Context open Termops open Entries open Environ @@ -87,7 +86,7 @@ let interp_definition pl bl p red_option c ctypopt = match ctypopt with None -> let subst = evd_comb0 Evd.nf_univ_variables evdref in - let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in + let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in @@ -100,7 +99,7 @@ let interp_definition pl bl p red_option c ctypopt = | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in let subst = evd_comb0 Evd.nf_univ_variables evdref in - let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in + let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in let nf, subst = Evarutil.e_nf_evars_and_universes evdref in @@ -125,7 +124,7 @@ let interp_definition pl bl p red_option c ctypopt = definition_entry ~types:typ ~poly:p ~univs:uctx body in - red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, pl, imps + red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); @@ -566,7 +565,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, _, impls) -> userimpls @ - lift_implicits (rel_context_nhyps ctx_params) impls) arities in + lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in @@ -592,11 +591,11 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let nf x = nf' (nf x) in let arities = List.map nf' arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in - let ctx_params = map_rel_context nf ctx_params in + let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in let pl, uctx = Evd.universe_context ?names:pl evd in List.iter (check_evars env_params Evd.empty evd) arities; - iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; + Context.Rel.iter (check_evars env0 Evd.empty evd) ctx_params; List.iter (fun (_,ctyps,_) -> List.iter (check_evars env_ar_params Evd.empty evd) ctyps) constructors; @@ -610,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_lc = ctypes }) indl arities aritypoly constructors in let impls = - let len = rel_context_nhyps ctx_params in + let len = Context.Rel.nhyps ctx_params in List.map2 (fun indimpls (_,_,cimpls) -> indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index b6da21e5a..9416b7e7a 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -9,7 +9,6 @@ open Names open Errors open Util -open Context open Term open Vars open Entries @@ -37,8 +36,8 @@ let detype_param = function let abstract_inductive hyps nparams inds = let ntyp = List.length inds in - let nhyp = named_context_length hyps in - let args = instance_from_named_context (List.rev hyps) in + let nhyp = Context.Named.length hyps in + let args = Context.Named.to_instance (List.rev hyps) in let args = Array.of_list args in let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in let inds' = @@ -100,7 +99,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = Array.to_list mip.mind_consnames, Array.to_list lc)) mib.mind_packets in - let sechyps' = map_named_context (expmod_constr modlist) sechyps in + let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in let abs_ctx = Univ.instantiate_univ_context abs_ctx in let univs = Univ.UContext.union abs_ctx univs in diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index 386e4e3ef..2984a0be8 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -6,10 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Context open Declarations open Entries open Opaqueproof val process_inductive : - named_context Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry + Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index cac81a939..e27e41437 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -13,7 +13,6 @@ open Declare *) open Term -open Context open Vars open Names open Evd @@ -44,7 +43,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: named_context; + ev_hyps: Context.Named.t; ev_status: Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; @@ -191,7 +190,7 @@ open Environ let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in - let nc_len = Context.named_context_length nc in + let nc_len = Context.Named.length nc in let evm = Evarutil.nf_evar_map_undefined evm in let evl = Evarutil.non_instantiated evm in let evl = Evar.Map.bindings evl in diff --git a/toplevel/record.ml b/toplevel/record.ml index 3a75004b0..12699b02b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -13,7 +13,6 @@ open Names open Globnames open Nameops open Term -open Context open Vars open Environ open Declarations @@ -148,8 +147,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = else arity, evars in let evars, nf = Evarutil.nf_evars_and_universes evars in - let newps = map_rel_context nf newps in - let newfs = map_rel_context nf newfs in + let newps = Context.Rel.map nf newps in + let newfs = Context.Rel.map nf newfs in let ce t = Evarutil.check_evars env0 Evd.empty evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps); List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs); @@ -244,8 +243,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) in - let rp = applist (r, Context.extended_rel_list 0 paramdecls) in - let paramargs = Context.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) + let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in + let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*) let x = Name binder_name in let fields = instantiate_possibly_recursive_type indu paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in @@ -353,7 +352,7 @@ open Typeclasses let declare_structure finite poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in - let args = Context.extended_rel_list nfields params in + let args = Context.Rel.to_extended_list nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let binder_name = diff --git a/toplevel/record.mli b/toplevel/record.mli index eccb5d29d..f68adcec8 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Vernacexpr open Constrexpr open Impargs @@ -22,15 +21,15 @@ val primitive_flag : bool ref val declare_projections : inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t -> - coercion_flag list -> manual_explicitation list list -> rel_context -> + coercion_flag list -> manual_explicitation list list -> Context.Rel.t -> (Name.t * bool) list * constant option list val declare_structure : Decl_kinds.recursivity_kind -> bool (** polymorphic?*) -> Univ.universe_context -> Id.t -> Id.t -> - manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *) + manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> - Impargs.manual_explicitation list list -> rel_context -> (** fields *) + Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t -> bool -> (** coercion? *) bool list -> (** field coercions *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 28b5bace1..2dacc04f0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1580,7 +1580,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in - let (id,bdyopt,typ) = Context.lookup_named id hyps in + let (id,bdyopt,typ) = Context.Named.lookup id hyps in let natureofid = match bdyopt with | None -> "Hypothesis" | Some bdy ->"Constant (let in)" in |