diff options
Diffstat (limited to 'checker/environ.mli')
-rw-r--r-- | checker/environ.mli | 52 |
1 files changed, 25 insertions, 27 deletions
diff --git a/checker/environ.mli b/checker/environ.mli index 628febbb..d3448b12 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -1,34 +1,33 @@ open Names -open Term +open Cic (* Environments *) type globals = { - env_constants : Declarations.constant_body Cmap_env.t; - env_inductives : Declarations.mutual_inductive_body Mindmap_env.t; + env_constants : constant_body Cmap_env.t; + env_inductives : mutual_inductive_body Mindmap_env.t; env_inductives_eq : kernel_name KNmap.t; - env_modules : Declarations.module_body MPmap.t; - env_modtypes : Declarations.module_type_body MPmap.t} + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; - env_engagement : Declarations.engagement option; + env_engagement : engagement option; } type env = { env_globals : globals; - env_named_context : named_context; env_rel_context : rel_context; env_stratification : stratification; - env_imports : Digest.t MPmap.t; + env_imports : Cic.vodigest MPmap.t; } val empty_env : env (* Engagement *) -val engagement : env -> Declarations.engagement option -val set_engagement : Declarations.engagement -> env -> env +val engagement : env -> Cic.engagement option +val set_engagement : Cic.engagement -> env -> env (* Digests *) -val add_digest : env -> dir_path -> Digest.t -> env -val lookup_digest : env -> dir_path -> Digest.t +val add_digest : env -> DirPath.t -> Cic.vodigest -> env +val lookup_digest : env -> DirPath.t -> Cic.vodigest (* de Bruijn variables *) val rel_context : env -> rel_context @@ -37,38 +36,37 @@ val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env val push_rec_types : name array * constr array * 'a -> env -> env -(* Named variables *) -val named_context : env -> named_context -val push_named : named_declaration -> env -> env -val lookup_named : identifier -> env -> named_declaration -val named_type : identifier -> env -> constr - (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val check_constraints : Univ.constraints -> env -> bool (* Constants *) -val lookup_constant : constant -> env -> Declarations.constant_body -val add_constant : constant -> Declarations.constant_body -> env -> env +val lookup_constant : constant -> env -> Cic.constant_body +val add_constant : constant -> Cic.constant_body -> env -> env +val constant_type : env -> constant puniverses -> constant_type Univ.constrained type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant -> constr +val constant_value : env -> constant puniverses -> constr val evaluable_constant : constant -> env -> bool +val is_projection : constant -> env -> bool +val lookup_projection : constant -> env -> projection_body + (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool val lookup_mind : - mutual_inductive -> env -> Declarations.mutual_inductive_body + mutual_inductive -> env -> Cic.mutual_inductive_body val add_mind : - mutual_inductive -> Declarations.mutual_inductive_body -> env -> env + mutual_inductive -> Cic.mutual_inductive_body -> env -> env (* Modules *) val add_modtype : - module_path -> Declarations.module_type_body -> env -> env + module_path -> Cic.module_type_body -> env -> env val shallow_add_module : - module_path -> Declarations.module_body -> env -> env + module_path -> Cic.module_body -> env -> env val shallow_remove_module : module_path -> env -> env -val lookup_module : module_path -> env -> Declarations.module_body -val lookup_modtype : module_path -> env -> Declarations.module_type_body +val lookup_module : module_path -> env -> Cic.module_body +val lookup_modtype : module_path -> env -> Cic.module_type_body |