aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-05-22 16:07:45 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-05-22 16:07:45 +0000
commit96876c750e05108e07dc1f29fa8db53f35f62f95 (patch)
tree4037c8fb2db4c945a86dbfbc8767322fda7728ff
parent4385c7c73868969617c04f74023ccf944e252bdc (diff)
fixed dependency problems with the checker
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10970 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build16
-rw-r--r--checker/environ.mli67
-rw-r--r--checker/term.mli111
3 files changed, 186 insertions, 8 deletions
diff --git a/Makefile.build b/Makefile.build
index 759b461d8..a5c6d6e5b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -895,14 +895,6 @@ endif
$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml
#End critical section
-%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml)
- $(SHOW)'OCAMLDEP $<'
- $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
-
-%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml)
- $(SHOW)'OCAMLDEP $<'
- $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
-
checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC)
$(SHOW)'OCAMLDEP $<'
$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) $< > "$@"
@@ -911,6 +903,14 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
$(SHOW)'OCAMLDEP $<'
$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) $< > "$@"
+%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml)
+ $(SHOW)'OCAMLDEP $<'
+ $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
+
+%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml)
+ $(SHOW)'OCAMLDEP $<'
+ $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
+
## Veerry nasty hack to keep ocamldep happy
%.ml: | %.ml4
$(SHOW)'TOUCH $@'
diff --git a/checker/environ.mli b/checker/environ.mli
new file mode 100644
index 000000000..a3f531dd0
--- /dev/null
+++ b/checker/environ.mli
@@ -0,0 +1,67 @@
+open Names
+open Term
+
+type globals = {
+ env_constants : Declarations.constant_body Cmap.t;
+ env_inductives : Declarations.mutual_inductive_body KNmap.t;
+ env_modules : Declarations.module_body MPmap.t;
+ env_modtypes : Declarations.module_type_body MPmap.t;
+ env_alias : module_path MPmap.t;
+}
+type stratification = {
+ env_universes : Univ.universes;
+ env_engagement : Declarations.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;
+}
+val empty_env : env
+val engagement : env -> Declarations.engagement option
+val universes : env -> Univ.universes
+val named_context : env -> named_context
+val rel_context : env -> rel_context
+val set_engagement : Declarations.engagement -> env -> env
+
+val add_digest : env -> dir_path -> Digest.t -> env
+val lookup_digest : env -> dir_path -> Digest.t
+
+val lookup_rel : int -> env -> rel_declaration
+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
+
+val push_named : named_declaration -> env -> env
+val lookup_named : identifier -> env -> named_declaration
+val named_type : identifier -> env -> constr
+
+val add_constraints : Univ.constraints -> env -> env
+
+val lookup_constant : constant -> env -> Declarations.constant_body
+val add_constant : constant -> Declarations.constant_body -> env -> env
+val constant_type : env -> constant -> Declarations.constant_type
+type const_evaluation_result = NoBody | Opaque
+exception NotEvaluableConst of const_evaluation_result
+val constant_value : env -> constant -> constr
+val constant_opt_value : env -> constant -> constr option
+val evaluable_constant : constant -> env -> bool
+
+val lookup_mind :
+ mutual_inductive -> env -> Declarations.mutual_inductive_body
+val scrape_mind : env -> mutual_inductive -> mutual_inductive
+val add_mind :
+ mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
+val mind_equiv : env -> inductive -> inductive -> bool
+
+val add_modtype :
+ module_path -> Declarations.module_type_body -> env -> env
+val shallow_add_module :
+ module_path -> Declarations.module_body -> env -> env
+val register_alias : module_path -> module_path -> env -> env
+val scrape_alias : module_path -> env -> module_path
+val lookup_module : module_path -> env -> Declarations.module_body
+val lookup_modtype : module_path -> env -> Declarations.module_type_body
+val lookup_alias : module_path -> env -> module_path
diff --git a/checker/term.mli b/checker/term.mli
new file mode 100644
index 000000000..30a2c03a5
--- /dev/null
+++ b/checker/term.mli
@@ -0,0 +1,111 @@
+open Names
+
+type existential_key = int
+type metavariable = int
+type case_style =
+ LetStyle
+ | IfStyle
+ | LetPatternStyle
+ | MatchStyle
+ | RegularStyle
+type case_printing = { ind_nargs : int; style : case_style; }
+type case_info = {
+ ci_ind : inductive;
+ ci_npar : int;
+ ci_cstr_nargs : int array;
+ ci_pp_info : case_printing;
+}
+type contents = Pos | Null
+type sorts = Prop of contents | Type of Univ.universe
+type sorts_family = InProp | InSet | InType
+val family_of_sort : sorts -> sorts_family
+type 'a pexistential = existential_key * 'a array
+type 'a prec_declaration = name array * 'a array * 'a array
+type 'a pfixpoint = (int array * int) * 'a prec_declaration
+type 'a pcofixpoint = int * 'a prec_declaration
+type cast_kind = VMcast | DEFAULTcast
+type constr =
+ Rel of int
+ | Var of identifier
+ | Meta of metavariable
+ | Evar of constr pexistential
+ | Sort of sorts
+ | Cast of constr * cast_kind * constr
+ | Prod of name * constr * constr
+ | Lambda of name * constr * constr
+ | LetIn of name * constr * constr * constr
+ | App of constr * constr array
+ | Const of constant
+ | Ind of inductive
+ | Construct of constructor
+ | Case of case_info * constr * constr * constr array
+ | Fix of constr pfixpoint
+ | CoFix of constr pcofixpoint
+type existential = constr pexistential
+type rec_declaration = constr prec_declaration
+type fixpoint = constr pfixpoint
+type cofixpoint = constr pcofixpoint
+val strip_outer_cast : constr -> constr
+val collapse_appl : constr -> constr
+val decompose_app : constr -> constr * constr list
+val applist : constr * constr list -> constr
+val iter_constr_with_binders :
+ ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
+exception LocalOccur
+val closedn : int -> constr -> bool
+val closed0 : constr -> bool
+val noccurn : int -> constr -> bool
+val noccur_between : int -> int -> constr -> bool
+val noccur_with_meta : int -> int -> constr -> bool
+val map_constr_with_binders :
+ ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+val exliftn : Esubst.lift -> constr -> constr
+val liftn : int -> int -> constr -> constr
+val lift : int -> constr -> constr
+type info = Closed | Open | Unknown
+type 'a substituend = { mutable sinfo : info; sit : 'a; }
+val lift_substituend : int -> constr substituend -> constr
+val make_substituend : 'a -> 'a substituend
+val substn_many : constr substituend array -> int -> constr -> constr
+val substnl : constr list -> int -> constr -> constr
+val substl : constr list -> constr -> constr
+val subst1 : constr -> constr -> constr
+
+type named_declaration = identifier * constr option * constr
+type rel_declaration = name * constr option * constr
+val map_named_declaration :
+ (constr -> constr) -> named_declaration -> named_declaration
+val map_rel_declaration :
+ (constr -> constr) -> rel_declaration -> rel_declaration
+val fold_named_declaration :
+ (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
+val fold_rel_declaration :
+ (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+type named_context = named_declaration list
+val empty_named_context : named_context
+val fold_named_context :
+ (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
+type section_context = named_context
+type rel_context = rel_declaration list
+val empty_rel_context : rel_context
+val rel_context_length : rel_context -> int
+val rel_context_nhyps : rel_context -> int
+val fold_rel_context :
+ (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val map_context : (constr -> constr) -> named_context -> named_context
+val map_rel_context : (constr -> constr) -> rel_context -> rel_context
+val extended_rel_list : int -> rel_context -> constr list
+val compose_lam : (name * constr) list -> constr -> constr
+val decompose_lam : constr -> (name * constr) list * constr
+val decompose_lam_n_assum : int -> constr -> rel_context * constr
+val mkProd_or_LetIn : name * constr option * constr -> constr -> constr
+val it_mkProd_or_LetIn : constr -> rel_context -> constr
+val decompose_prod_assum : constr -> rel_context * constr
+val decompose_prod_n_assum : int -> constr -> rel_context * constr
+
+type arity = rel_context * sorts
+val mkArity : arity -> constr
+val destArity : constr -> arity
+val isArity : constr -> bool
+val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+val eq_constr : constr -> constr -> bool