From: Enrico Tassi Date: Wed, 30 Jan 2008 10:42:22 +0000 (+0000) Subject: basic organization of the new kernel X-Git-Tag: make_still_working~5650 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5f926fd66f345c273bc66cc3ab9b1344ad0eac25;p=helm.git basic organization of the new kernel --- diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml new file mode 100644 index 000000000..23ba6d084 --- /dev/null +++ b/helm/software/components/ng_kernel/nCic.ml @@ -0,0 +1,229 @@ +(* 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. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(* This module defines the internal representation of the objects (variables,*) +(* blocks of (co)inductive definitions and constants) and the terms of cic *) +(* *) +(*****************************************************************************) + +(* $Id: cic.ml 7190 2007-01-31 18:36:04Z sacerdot $ *) +(* +(* STUFF TO MANAGE IDENTIFIERS *) +type id = string (* the abstract type of the (annotated) node identifiers *) +type 'term explicit_named_substitution = (UriManager.uri * 'term) list + + +(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) + +type object_flavour = + [ `Definition + | `MutualDefinition + | `Fact + | `Lemma + | `Remark + | `Theorem + | `Variant + | `Axiom + ] + +type object_class = + [ `Coercion of int + | `Elim of sort (** elimination principle; if sort is Type, the universe is + * not relevant *) + | `Record of (string * bool * int) list (** + inductive type that encodes a record; the arguments are + the record fields names and if they are coercions and + then the coercion arity *) + | `Projection (** record projection *) + | `InversionPrinciple (** inversion principle *) + ] + +type attribute = + [ `Class of object_class + | `Flavour of object_flavour + | `Generated + ] +*) +type sort = + | Prop + | Set + | Type of CicUniv.universe + | CProp + +type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] + +type name = Name of string | Anonymous + +type local_context = int * (term list) option (* shift, subst (None means id) *) + +and term = + | Rel of int (* DeBruijn index, 1 based *) + | Meta of int * local_context + | Appl of term list (* arguments *) + | Prod of name * term * term (* binder, source, target *) + | Lambda of name * term * term (* binder, source, target *) + | LetIn of name * term * term * term (* binder, type, term, body *) + | Const of UriManager.uri (* uri contains indtypeno/constrno *) + | Sort of sort (* sort *) + | Implicit of implicit_annotation (* ... *) + | MutCase of UriManager.uri * (* ind. uri, *) + term * term * (* outtype, ind. term *) + term list (* patterns *) +and obj = + Constant of string * term option * term * (* id, body, type, *) + UriManager.uri list * attribute list (* parameters *) + | Variable of string * term option * term * (* name, body, type *) + UriManager.uri list * attribute list (* parameters *) + | CurrentProof of string * metasenv * term * (* name, conjectures, body, *) + term * UriManager.uri list * attribute list (* type, parameters *) + | InductiveDefinition of inductiveType list * (* inductive types, *) + UriManager.uri list * int * attribute list (* params, left params no *) +and inductiveType = + string * bool * term * (* typename, inductive, arity *) + constructor list (* constructors *) +and constructor = + string * term (* id, type *) +and inductiveFun = + string * int * term * term (* name, ind. index, type, body *) +and coInductiveFun = + string * term * term (* name, type, body *) + +(* a metasenv is a list of declarations of metas in declarations *) +(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) +(* depend on new ones. *) +and conjecture = int * context * term +and metasenv = conjecture list +and substitution = (int * (context * term * term)) list + + + +(* a metasenv is a list of declarations of metas in declarations *) +(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) +(* depend on new ones. *) +and annconjecture = id * int * anncontext * annterm +and annmetasenv = annconjecture list + +and annterm = + ARel of id * id * int * (* idref, DeBrujin index, *) + string (* binder *) + | AVar of id * UriManager.uri * (* uri, *) + annterm explicit_named_substitution (* explicit named subst. *) + | AMeta of id * int * (annterm option) list (* numeric id, *) + (* local context *) + | ASort of id * sort (* sort *) + | AImplicit of id * implicit_annotation option (* *) + | ACast of id * annterm * annterm (* value, type *) + | AProd of id * name * annterm * annterm (* binder, source, target *) + | ALambda of id * name * annterm * annterm (* binder, source, target *) + | ALetIn of id * name * annterm * annterm (* binder, term, target *) + | AAppl of id * annterm list (* arguments *) + | AConst of id * UriManager.uri * (* uri, *) + annterm explicit_named_substitution (* explicit named subst. *) + | AMutInd of id * UriManager.uri * int * (* uri, typeno *) + annterm explicit_named_substitution (* explicit named subst. *) + (* typeno is 0 based *) + | AMutConstruct of id * UriManager.uri * (* uri, *) + int * int * (* typeno, consno *) + annterm explicit_named_substitution (* explicit named subst. *) + (* typeno is 0 based *) + (* consno is 1 based *) + | AMutCase of id * UriManager.uri * (* ind. uri, *) + int * (* ind. typeno, *) + annterm * annterm * (* outtype, ind. term *) + annterm list (* patterns *) + | AFix of id * int * anninductiveFun list (* funno, functions *) + | ACoFix of id * int * anncoInductiveFun list (* funno, functions *) +and annobj = + AConstant of id * id option * string * (* name, *) + annterm option * annterm * (* body, type, *) + UriManager.uri list * attribute list (* parameters *) + | AVariable of id * + string * annterm option * annterm * (* name, body, type *) + UriManager.uri list * attribute list (* parameters *) + | ACurrentProof of id * id * + string * annmetasenv * (* name, conjectures, *) + annterm * annterm * UriManager.uri list * (* body,type,parameters *) + attribute list + | AInductiveDefinition of id * + anninductiveType list * (* inductive types , *) + UriManager.uri list * int * attribute list (* parameters,n ind. pars*) +and anninductiveType = + id * string * bool * annterm * (* typename, inductive, arity *) + annconstructor list (* constructors *) +and annconstructor = + string * annterm (* id, type *) +and anninductiveFun = + id * string * int * annterm * annterm (* name, ind. index, type, body *) +and anncoInductiveFun = + id * string * annterm * annterm (* name, type, body *) +and annotation = + string + +and context_entry = (* A declaration or definition *) + Decl of term + | Def of term * term option (* body, type (if known) *) + +and hypothesis = + (name * context_entry) option (* None means no more accessible *) + +and context = hypothesis list + +and anncontext_entry = (* A declaration or definition *) + ADecl of annterm + | ADef of annterm + +and annhypothesis = + id * (name * anncontext_entry) option (* None means no more accessible *) + +and anncontext = annhypothesis list +;; + +type lazy_term = + context -> metasenv -> CicUniv.universe_graph -> + term * metasenv * CicUniv.universe_graph + +type anntarget = + Object of annobj (* if annobj is a Constant, this is its type *) + | ConstantBody of annobj + | Term of annterm + | Conjecture of annconjecture + | Hypothesis of annhypothesis + +module CicHash = + Hashtbl.Make + (struct + type t = term + let equal = (==) + let hash = Hashtbl.hash_param 100 1000 + end) +;; + diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli new file mode 100644 index 000000000..ac6654cf9 --- /dev/null +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -0,0 +1,33 @@ +(* 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. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* NG: minimal wrapper on the old cicEnvironment, should provide only the + * functions strictly necessary to the typechecking algorithm *) + +val get_checked_obj : + NCicUniv.universe_graph -> NUriManager.uri -> + NCic.obj * NCicUniv.universe_graph + +(* EOF *) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli new file mode 100644 index 000000000..5dc181cde --- /dev/null +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -0,0 +1,31 @@ +(* 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/. + *) + +(* These are the only exceptions that will be raised *) +exception TypeCheckerFailure of string Lazy.t +exception AssertFailure of string Lazy.t + +(* typechecks the object, raising an exception if illtyped *) +val typecheck_obj : NCic.obj -> unit + diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml new file mode 100644 index 000000000..c0da8eb4b --- /dev/null +++ b/helm/software/components/ng_kernel/nUriManager.ml @@ -0,0 +1,245 @@ +(* 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. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id$ *) + +(* + * "cic:/a/b/c.con" => ("cic:/a/b/c.con", id ) + * "cic:/a/b/c.ind#xpointer(1/1)" => ("cic:/a/b/c.con#xpointer(1/1)", id) + * "cic:/a/b/c.ind#xpointer(1/1/1)" => ("cic:/a/b/c.con#xpointer(1/1/1)", id) + *) + +let fresh_id = + let id = ref 0 in + function () -> + incr id; + !id + +(* (uriwithxpointer, uniqueid) + * where uniqueid is used to build a set of uri *) +type uri = string * int;; + +let eq uri1 uri2 = + uri1 == uri2 +;; + +let string_of_uri (uri,_) = + uri + +let name_of_uri (uri, _) = + let xpointer_offset = + try String.rindex uri '#' with Not_found -> String.length uri - 1 + in + let index1 = String.rindex_from uri xpointer_offset '/' + 1 in + let index2 = String.rindex uri '.' in + String.sub uri index1 (index2 - index1) + +let nameext_of_uri (uri, _) = + let xpointer_offset, mah = + try String.rindex uri '#', 0 with Not_found -> String.length uri - 1, 1 + in + let index1 = String.rindex_from uri xpointer_offset '/' + 1 in + String.sub uri index1 (xpointer_offset - index1 + mah) + +let buri_of_uri (uri,_) = + let xpointer_offset = + try String.rindex uri '#' with Not_found -> String.length uri - 1 + in + let index = String.rindex_from uri xpointer_offset '/' in + String.sub uri 0 index + +module OrderedStrings = + struct + type t = string + let compare (s1 : t) (s2 : t) = compare s1 s2 + end +;; + +module MapStringsToUri = Map.Make(OrderedStrings);; + +(* Invariant: the map is the identity function, + * i.e. + * let str' = (MapStringsToUri.find str !set_of_uri) in + * str' == (MapStringsToUri.find str' !set_of_uri) + *) +let set_of_uri = ref MapStringsToUri.empty;; + +exception IllFormedUri of string;; + +let _dottypes = ".types" +let _types = "types",5 +let _dotuniv = ".univ" +let _univ = "univ",4 +let _dotann = ".ann" +let _ann = "ann",3 +let _var = "var",3 +let _dotbody = ".body" +let _con = "con",3 +let _ind = "ind",3 +let _xpointer = "#xpointer(1/" +let _con3 = "con" +let _var3 = "var" +let _ind3 = "ind" +let _ann3 = "ann" +let _univ4 = "univ" +let _types5 = "types" +let _xpointer8 = "xpointer" +let _cic5 = "cic:/" + +let is_malformed suri = + try + if String.sub suri 0 5 <> _cic5 then true + else + let len = String.length suri - 5 in + let last5 = String.sub suri len 5 in + let last4 = String.sub last5 1 4 in + let last3 = String.sub last5 2 3 in + if last3 = _con3 || last3 = _var3 || last3 = _ind3 || + last3 = _ann3 || last5 = _types5 || last5 = _dotbody || + last4 = _univ4 then + false + else + try + let index = String.rindex suri '#' + 1 in + let xptr = String.sub suri index 8 in + if xptr = _xpointer8 then + false + else + true + with Not_found -> true + with Invalid_argument _ -> true + +(* hash conses an uri *) +let uri_of_string suri = + try + MapStringsToUri.find suri !set_of_uri + with Not_found -> + if is_malformed suri then + raise (IllFormedUri suri) + else + let new_uri = suri, fresh_id () in + set_of_uri := MapStringsToUri.add suri new_uri !set_of_uri; + new_uri + + +let strip_xpointer ((uri,_) as olduri) = + try + let index = String.rindex uri '#' in + let no_xpointer = String.sub uri 0 index in + uri_of_string no_xpointer + with + Not_found -> olduri + +let clear_suffix uri ?(pat2="",0) pat1 = + try + let index = String.rindex uri '.' in + let index' = index + 1 in + let suffix = String.sub uri index' (String.length uri - index') in + if fst pat1 = suffix || fst pat2 = suffix then + String.sub uri 0 index + else + uri + with + Not_found -> assert false + +let has_suffix uri (pat,n) = + try + let suffix = String.sub uri (String.length uri - n) n in + pat = suffix + with + Not_found -> assert false + + +let cicuri_of_uri (uri, _) = uri_of_string (clear_suffix uri ~pat2:_types _ann) + +let annuri_of_uri (uri , _) = uri_of_string ((clear_suffix uri _ann) ^ _dotann) + +let uri_is_annuri (uri, _) = has_suffix uri _ann + +let uri_is_var (uri, _) = has_suffix uri _var + +let uri_is_con (uri, _) = has_suffix uri _con + +let uri_is_ind (uri, _) = has_suffix uri _ind + +let bodyuri_of_uri (uri, _) = + if has_suffix uri _con then + Some (uri_of_string (uri ^ _dotbody)) + else + None +;; + +(* these are bugged! + * we should remove _types, _univ, _ann all toghether *) +let innertypesuri_of_uri (uri, _) = + uri_of_string ((clear_suffix uri _types) ^ _dottypes) +;; +let univgraphuri_of_uri (uri,_) = + uri_of_string ((clear_suffix uri _univ) ^ _dotuniv) +;; + + +let uri_of_uriref (uri, _) typeno consno = + let typeno = typeno + 1 in + let suri = + match consno with + | None -> Printf.sprintf "%s%s%d)" uri _xpointer typeno + | Some n -> Printf.sprintf "%s%s%d/%d)" uri _xpointer typeno n + in + uri_of_string suri + +let compare (_,id1) (_,id2) = id1 - id2 + +module OrderedUri = +struct + type t = uri + let compare = compare (* the one above, not Pervasives.compare *) +end + +module UriSet = Set.Make (OrderedUri) + +(* +module OrderedUriPair = +struct + type t = uri * uri + let compare (u11, u12) (u21, u22) = + match compare u11 u21 with + | 0 -> compare u12 u22 + | x -> x +end + +module UriPairSet = Set.Make (OrderedUriPair) +*) + +module HashedUri = +struct + type t = uri + let equal = eq + let hash = snd +end + +module UriHashtbl = Hashtbl.Make (HashedUri) + + diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli new file mode 100644 index 000000000..5dd69e9d9 --- /dev/null +++ b/helm/software/components/ng_kernel/nUriManager.mli @@ -0,0 +1,33 @@ +(* 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. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception IllFormedUri of string Lazy.t;; + +type uri + +val eq: uri -> uri -> bool + +val string_of_uri: uri -> string + diff --git a/helm/software/components/ng_kernel/ngcic.ml b/helm/software/components/ng_kernel/ngcic.ml deleted file mode 100644 index 23ba6d084..000000000 --- a/helm/software/components/ng_kernel/ngcic.ml +++ /dev/null @@ -1,229 +0,0 @@ -(* 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. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(*****************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/11/2000 *) -(* *) -(* This module defines the internal representation of the objects (variables,*) -(* blocks of (co)inductive definitions and constants) and the terms of cic *) -(* *) -(*****************************************************************************) - -(* $Id: cic.ml 7190 2007-01-31 18:36:04Z sacerdot $ *) -(* -(* STUFF TO MANAGE IDENTIFIERS *) -type id = string (* the abstract type of the (annotated) node identifiers *) -type 'term explicit_named_substitution = (UriManager.uri * 'term) list - - -(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) - -type object_flavour = - [ `Definition - | `MutualDefinition - | `Fact - | `Lemma - | `Remark - | `Theorem - | `Variant - | `Axiom - ] - -type object_class = - [ `Coercion of int - | `Elim of sort (** elimination principle; if sort is Type, the universe is - * not relevant *) - | `Record of (string * bool * int) list (** - inductive type that encodes a record; the arguments are - the record fields names and if they are coercions and - then the coercion arity *) - | `Projection (** record projection *) - | `InversionPrinciple (** inversion principle *) - ] - -type attribute = - [ `Class of object_class - | `Flavour of object_flavour - | `Generated - ] -*) -type sort = - | Prop - | Set - | Type of CicUniv.universe - | CProp - -type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] - -type name = Name of string | Anonymous - -type local_context = int * (term list) option (* shift, subst (None means id) *) - -and term = - | Rel of int (* DeBruijn index, 1 based *) - | Meta of int * local_context - | Appl of term list (* arguments *) - | Prod of name * term * term (* binder, source, target *) - | Lambda of name * term * term (* binder, source, target *) - | LetIn of name * term * term * term (* binder, type, term, body *) - | Const of UriManager.uri (* uri contains indtypeno/constrno *) - | Sort of sort (* sort *) - | Implicit of implicit_annotation (* ... *) - | MutCase of UriManager.uri * (* ind. uri, *) - term * term * (* outtype, ind. term *) - term list (* patterns *) -and obj = - Constant of string * term option * term * (* id, body, type, *) - UriManager.uri list * attribute list (* parameters *) - | Variable of string * term option * term * (* name, body, type *) - UriManager.uri list * attribute list (* parameters *) - | CurrentProof of string * metasenv * term * (* name, conjectures, body, *) - term * UriManager.uri list * attribute list (* type, parameters *) - | InductiveDefinition of inductiveType list * (* inductive types, *) - UriManager.uri list * int * attribute list (* params, left params no *) -and inductiveType = - string * bool * term * (* typename, inductive, arity *) - constructor list (* constructors *) -and constructor = - string * term (* id, type *) -and inductiveFun = - string * int * term * term (* name, ind. index, type, body *) -and coInductiveFun = - string * term * term (* name, type, body *) - -(* a metasenv is a list of declarations of metas in declarations *) -(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) -(* depend on new ones. *) -and conjecture = int * context * term -and metasenv = conjecture list -and substitution = (int * (context * term * term)) list - - - -(* a metasenv is a list of declarations of metas in declarations *) -(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) -(* depend on new ones. *) -and annconjecture = id * int * anncontext * annterm -and annmetasenv = annconjecture list - -and annterm = - ARel of id * id * int * (* idref, DeBrujin index, *) - string (* binder *) - | AVar of id * UriManager.uri * (* uri, *) - annterm explicit_named_substitution (* explicit named subst. *) - | AMeta of id * int * (annterm option) list (* numeric id, *) - (* local context *) - | ASort of id * sort (* sort *) - | AImplicit of id * implicit_annotation option (* *) - | ACast of id * annterm * annterm (* value, type *) - | AProd of id * name * annterm * annterm (* binder, source, target *) - | ALambda of id * name * annterm * annterm (* binder, source, target *) - | ALetIn of id * name * annterm * annterm (* binder, term, target *) - | AAppl of id * annterm list (* arguments *) - | AConst of id * UriManager.uri * (* uri, *) - annterm explicit_named_substitution (* explicit named subst. *) - | AMutInd of id * UriManager.uri * int * (* uri, typeno *) - annterm explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - | AMutConstruct of id * UriManager.uri * (* uri, *) - int * int * (* typeno, consno *) - annterm explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - (* consno is 1 based *) - | AMutCase of id * UriManager.uri * (* ind. uri, *) - int * (* ind. typeno, *) - annterm * annterm * (* outtype, ind. term *) - annterm list (* patterns *) - | AFix of id * int * anninductiveFun list (* funno, functions *) - | ACoFix of id * int * anncoInductiveFun list (* funno, functions *) -and annobj = - AConstant of id * id option * string * (* name, *) - annterm option * annterm * (* body, type, *) - UriManager.uri list * attribute list (* parameters *) - | AVariable of id * - string * annterm option * annterm * (* name, body, type *) - UriManager.uri list * attribute list (* parameters *) - | ACurrentProof of id * id * - string * annmetasenv * (* name, conjectures, *) - annterm * annterm * UriManager.uri list * (* body,type,parameters *) - attribute list - | AInductiveDefinition of id * - anninductiveType list * (* inductive types , *) - UriManager.uri list * int * attribute list (* parameters,n ind. pars*) -and anninductiveType = - id * string * bool * annterm * (* typename, inductive, arity *) - annconstructor list (* constructors *) -and annconstructor = - string * annterm (* id, type *) -and anninductiveFun = - id * string * int * annterm * annterm (* name, ind. index, type, body *) -and anncoInductiveFun = - id * string * annterm * annterm (* name, type, body *) -and annotation = - string - -and context_entry = (* A declaration or definition *) - Decl of term - | Def of term * term option (* body, type (if known) *) - -and hypothesis = - (name * context_entry) option (* None means no more accessible *) - -and context = hypothesis list - -and anncontext_entry = (* A declaration or definition *) - ADecl of annterm - | ADef of annterm - -and annhypothesis = - id * (name * anncontext_entry) option (* None means no more accessible *) - -and anncontext = annhypothesis list -;; - -type lazy_term = - context -> metasenv -> CicUniv.universe_graph -> - term * metasenv * CicUniv.universe_graph - -type anntarget = - Object of annobj (* if annobj is a Constant, this is its type *) - | ConstantBody of annobj - | Term of annterm - | Conjecture of annconjecture - | Hypothesis of annhypothesis - -module CicHash = - Hashtbl.Make - (struct - type t = term - let equal = (==) - let hash = Hashtbl.hash_param 100 1000 - end) -;; - diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.mli b/helm/software/components/ng_kernel/oCicTypeChecker.mli new file mode 100644 index 000000000..07ee59206 --- /dev/null +++ b/helm/software/components/ng_kernel/oCicTypeChecker.mli @@ -0,0 +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. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* typechecks the OLD object using the NEW type checker, + * if illtyped returns false (no exceptions raised) + *) +val typecheck_obj : Cic.obj -> bool +