From 5f926fd66f345c273bc66cc3ab9b1344ad0eac25 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Jan 2008 10:42:22 +0000 Subject: [PATCH] basic organization of the new kernel --- .../ng_kernel/{ngcic.ml => nCic.ml} | 0 .../components/ng_kernel/nCicEnvironment.mli | 33 +++ .../components/ng_kernel/nCicTypeChecker.mli | 31 +++ .../components/ng_kernel/nUriManager.ml | 245 ++++++++++++++++++ .../components/ng_kernel/nUriManager.mli | 33 +++ .../components/ng_kernel/oCicTypeChecker.mli | 30 +++ 6 files changed, 372 insertions(+) rename helm/software/components/ng_kernel/{ngcic.ml => nCic.ml} (100%) create mode 100644 helm/software/components/ng_kernel/nCicEnvironment.mli create mode 100644 helm/software/components/ng_kernel/nCicTypeChecker.mli create mode 100644 helm/software/components/ng_kernel/nUriManager.ml create mode 100644 helm/software/components/ng_kernel/nUriManager.mli create mode 100644 helm/software/components/ng_kernel/oCicTypeChecker.mli diff --git a/helm/software/components/ng_kernel/ngcic.ml b/helm/software/components/ng_kernel/nCic.ml similarity index 100% rename from helm/software/components/ng_kernel/ngcic.ml rename to helm/software/components/ng_kernel/nCic.ml 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/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 + -- 2.39.5