X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.mli;h=6ad40b8bb555c91f1f339fcb97861918b40eb724;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=51aa6458d11845d67f75dcccadf77ff65211483a;hpb=613bc202d0810f4386b393bfb369c62dfc78c68c;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli index 51aa6458d..6ad40b8bb 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -1,31 +1,30 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * http://cs.unibo.it/helm/. - *) +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) (* These are the only exceptions that will be raised *) exception TypeCheckerFailure of string Lazy.t exception AssertFailure of string Lazy.t +val set_logger: + ([ `Start_type_checking of NUri.uri + | `Type_checking_completed of NUri.uri + | `Type_checking_interrupted of NUri.uri + | `Type_checking_failed of NUri.uri + | `Trust_obj of NUri.uri + ] -> unit) -> unit + +val set_trust : (NCic.obj -> bool) -> unit + (* typechecks the object, raising an exception if illtyped *) val typecheck_obj : NCic.obj -> unit @@ -34,3 +33,28 @@ val typeof: NCic.context -> NCic.term -> NCic.term +val get_relevance : + metasenv:NCic.metasenv -> subst:NCic.substitution -> + NCic.context -> NCic.term -> NCic.term list -> bool list + +(* type_of_branch subst context leftno outtype + * (constr @ lefts) (ty_constr @ lefts) *) +val type_of_branch : + subst:NCic.substitution -> + NCic.context -> int -> NCic.term -> NCic.term -> NCic.term -> + NCic.term + +(* ind = indtype @ lefts + * arity1 = constructor type @ lefts + * arity2 = outtype *) +val check_allowed_sort_elimination : + subst:NCic.substitution -> + metasenv:NCic.metasenv -> + NReference.reference -> NCic.context -> + NCic.term -> NCic.term -> NCic.term -> unit + +(* Functions to be used by the refiner *) +val debruijn: NUri.uri -> int -> NCic.context -> NCic.term -> NCic.term +val are_all_occurrences_positive: + subst:NCic.substitution -> + NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool