From fb3367a180abd237b4096fe398178dd14b994f6d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 27 Jan 2004 17:07:44 +0000 Subject: [PATCH] added CicUtil module with just lookup_meta function --- helm/ocaml/cic/.depend | 3 +++ helm/ocaml/cic/Makefile | 6 ++++-- helm/ocaml/cic/cicUtil.ml | 32 ++++++++++++++++++++++++++++++++ helm/ocaml/cic/cicUtil.mli | 28 ++++++++++++++++++++++++++++ 4 files changed, 67 insertions(+), 2 deletions(-) create mode 100644 helm/ocaml/cic/cicUtil.ml create mode 100644 helm/ocaml/cic/cicUtil.mli diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 3bf9bfede..567c610f4 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -2,6 +2,7 @@ deannotate.cmi: cic.cmo cicParser3.cmi: cic.cmo cicParser2.cmi: cic.cmo cicParser3.cmi cicParser.cmi: cic.cmo +cicUtil.cmi: cic.cmo deannotate.cmo: cic.cmo deannotate.cmi deannotate.cmx: cic.cmx deannotate.cmi cicParser3.cmo: cic.cmo cicParser3.cmi @@ -10,5 +11,7 @@ cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi cicParser.cmx: cicParser2.cmx cicParser3.cmx deannotate.cmx cicParser.cmi +cicUtil.cmo: cicUtil.cmi +cicUtil.cmx: cicUtil.cmi helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmx: cic.cmx diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index 1789cd67e..d1106fb7e 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -2,8 +2,10 @@ PACKAGE = cic REQUIRES = helm-urimanager helm-pxp PREDICATES = -INTERFACE_FILES = deannotate.mli cicParser3.mli cicParser2.mli cicParser.mli -IMPLEMENTATION_FILES = cic.ml $(INTERFACE_FILES:%.mli=%.ml) helmLibraryObjects.ml +INTERFACE_FILES = \ + deannotate.mli cicParser3.mli cicParser2.mli cicParser.mli cicUtil.mli +IMPLEMENTATION_FILES = \ + cic.ml $(INTERFACE_FILES:%.mli=%.ml) helmLibraryObjects.ml EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml new file mode 100644 index 000000000..a8195a311 --- /dev/null +++ b/helm/ocaml/cic/cicUtil.ml @@ -0,0 +1,32 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +exception Meta_not_found of int + +let lookup_meta index metasenv = + try + List.find (fun (index', _, _) -> index = index') metasenv + with Not_found -> raise (Meta_not_found index) + diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli new file mode 100644 index 000000000..a2548f933 --- /dev/null +++ b/helm/ocaml/cic/cicUtil.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) +exception Meta_not_found of int + +val lookup_meta: int -> Cic.metasenv -> Cic.conjecture + -- 2.39.2