From b4b1a1498463e8f9f32b88979781d281869fb0d4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 18 Oct 2000 14:58:14 +0000 Subject: Renommage canonique : declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@724 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 22 +++++++++++----------- library/declare.mli | 4 ++-- library/global.ml | 15 ++++++--------- library/global.mli | 18 +++++++----------- library/impargs.ml | 2 +- 5 files changed, 27 insertions(+), 34 deletions(-) diff --git a/library/declare.ml b/library/declare.ml index 6b45dedb0..e8aba9fe1 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -57,8 +57,8 @@ let _ = Summary.declare_summary "VARIABLE" let cache_variable (sp,((id,(d,_,_) as vd),imps)) = begin match d with (* Fails if not well-typed *) - | SectionLocalDecl ty -> Global.push_var_decl (id,ty) - | SectionLocalDef c -> Global.push_var_def (id,c) + | SectionLocalDecl ty -> Global.push_named_assum (id,ty) + | SectionLocalDef c -> Global.push_named_def (id,c) end; Nametab.push id sp; if imps then declare_var_implicits id; @@ -204,7 +204,7 @@ let is_variable id = let out_variable sp = let (id,(_,str,sticky)) = Spmap.find sp !vartab in - let (c,ty) = Global.lookup_var id in + let (c,ty) = Global.lookup_named id in ((id,c,ty),str,sticky) let variable_strength id = @@ -262,7 +262,7 @@ let occur_decl env (id,c,t) hyps = (* let rec find_common_hyps_then_abstract c env hyps' = function | (id,_,_ as d) :: hyps when occur_decl env d hyps' -> - find_common_hyps_then_abstract c (Environ.push_var d env) hyps' hyps + find_common_hyps_then_abstract c (Environ.push_named_decl d env) hyps' hyps | hyps -> Environ.it_mkNamedLambda_or_LetIn c hyps @@ -271,11 +271,11 @@ let find_common_hyps_then_abstract c env hyps' hyps = *) let find_common_hyps_then_abstract c env hyps' hyps = - snd (fold_var_context_both_sides + snd (fold_named_context_both_sides (fun (env,c) (id,_,_ as d) hyps -> if occur_decl env d hyps' then - (Environ.push_var d env,c) + (Environ.push_named_decl d env,c) else (env, Environ.it_mkNamedLambda_or_LetIn c hyps)) hyps @@ -283,9 +283,9 @@ let find_common_hyps_then_abstract c env hyps' hyps = let construct_sp_reference env sp id = let (oper,hyps) = global_sp_operator env sp id in - let hyps0 = Global.var_context () in + let hyps0 = Global.named_context () in let env0 = Environ.reset_context env in - let args = List.map mkVar (ids_of_var_context hyps) in + let args = List.map mkVar (ids_of_named_context hyps) in let body = match oper with | ConstRef sp -> mkConst (sp,Array.of_list args) | ConstructRef sp -> mkMutConstruct (sp,Array.of_list args) @@ -298,7 +298,7 @@ let construct_reference env kind id = let sp = Nametab.sp_of_id kind id in construct_sp_reference env sp id with Not_found -> - mkVar (let _ = Environ.lookup_var id env in id) + mkVar (let _ = Environ.lookup_named id env in id) let global_sp_reference sp id = construct_sp_reference (Global.env()) sp id @@ -351,8 +351,8 @@ let elimination_suffix = function let declare_eliminations sp i = let mib = Global.lookup_mind sp in - let ids = ids_of_var_context mib.mind_hyps in - if not (list_subset ids (ids_of_var_context (Global.var_context ()))) then + let ids = ids_of_named_context mib.mind_hyps in + if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then error ("Declarations of elimination scheme outside the section "^ "of the inductive definition is not implemented"); let ctxt = Array.of_list (List.map mkVar ids) in diff --git a/library/declare.mli b/library/declare.mli index 4a33500fc..cd931d94d 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -50,7 +50,7 @@ val constant_strength : section_path -> strength val constant_or_parameter_strength : section_path -> strength val is_variable : identifier -> bool -val out_variable : section_path -> var_declaration * strength * sticky +val out_variable : section_path -> named_declaration * strength * sticky val variable_strength : identifier -> strength @@ -58,7 +58,7 @@ val variable_strength : identifier -> strength construtor) corresponding to [id] in global environment, together with its definition environment. *) -val global_operator : path_kind -> identifier -> global_reference * var_context +val global_operator : path_kind -> identifier -> global_reference * named_context (*s [global_reference k id] returns the object corresponding to the name [id] in the global environment. It may be a constant, diff --git a/library/global.ml b/library/global.ml index 96fb689a3..52ea32986 100644 --- a/library/global.ml +++ b/library/global.ml @@ -28,22 +28,19 @@ let _ = let universes () = universes !global_env let context () = context !global_env -let var_context () = var_context !global_env +let named_context () = named_context !global_env + +let push_named_def idc = global_env := push_named_def idc !global_env +let push_named_assum idc = global_env := push_named_assum idc !global_env -let push_var_def idc = global_env := push_var_def idc !global_env -let push_var_decl idc = global_env := push_var_decl idc !global_env -(* -let push_rel_def nac = global_env := push_rel nac !global_env -let push_rel_decl nac = global_env := push_rel nac !global_env -*) let add_constant sp ce = global_env := add_constant sp ce !global_env let add_parameter sp c = global_env := add_parameter sp c !global_env let add_mind sp mie = global_env := add_mind sp mie !global_env let add_constraints c = global_env := add_constraints c !global_env -let pop_vars ids = global_env := pop_vars ids !global_env +let pop_named_decls ids = global_env := pop_named_decls ids !global_env -let lookup_var id = lookup_var id !global_env +let lookup_named id = lookup_named id !global_env (* let lookup_rel n = lookup_rel n !global_env *) diff --git a/library/global.mli b/library/global.mli index 16ed53785..88f690c54 100644 --- a/library/global.mli +++ b/library/global.mli @@ -21,23 +21,19 @@ val env : unit -> env val universes : unit -> universes val context : unit -> context -val var_context : unit -> var_context - -val push_var_decl : identifier * constr -> unit -val push_var_def : identifier * constr -> unit -(*i -val push_var : identifier * constr option * constr -> unit -val push_rel_decl : name * constr -> unit -val push_rel_def : name * constr -> unit -i*) +val named_context : unit -> named_context + +val push_named_assum : identifier * constr -> unit +val push_named_def : identifier * constr -> unit + val add_constant : section_path -> constant_entry -> unit val add_parameter : section_path -> constr -> unit val add_mind : section_path -> mutual_inductive_entry -> unit val add_constraints : constraints -> unit -val pop_vars : identifier list -> unit +val pop_named_decls : identifier list -> unit -val lookup_var : identifier -> constr option * typed_type +val lookup_named : identifier -> constr option * typed_type (*i val lookup_rel : int -> name * typed_type i*) val lookup_constant : section_path -> constant_body val lookup_mind : section_path -> mutual_inductive_body diff --git a/library/impargs.ml b/library/impargs.ml index e2cd81f4e..17cd54b2c 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -100,7 +100,7 @@ let var_table = ref Idmap.empty let declare_var_implicits id = let env = Global.env () in - let (_,ty) = lookup_var id env in + let (_,ty) = lookup_named id env in let imps = auto_implicits env (body_of_type ty) in var_table := Idmap.add id imps !var_table -- cgit v1.2.3