From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: 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. --- pretyping/pretyping.ml | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'pretyping/pretyping.ml') 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 -- cgit v1.2.3