From: Stefano Zacchiroli Date: Fri, 17 Jun 2005 15:06:43 +0000 (+0000) Subject: removed! X-Git-Tag: INDEXING_NO_PROOFS~117 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=76371b115479873c07d16a047978394ebd4d495e;p=helm.git removed! --- diff --git a/helm/ocaml/cic_annotations/.cvsignore b/helm/ocaml/cic_annotations/.cvsignore deleted file mode 100644 index 6b3eba302..000000000 --- a/helm/ocaml/cic_annotations/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.cm[iaox] *.cmxa diff --git a/helm/ocaml/cic_annotations/.depend b/helm/ocaml/cic_annotations/.depend deleted file mode 100644 index 2c30fa7d7..000000000 --- a/helm/ocaml/cic_annotations/.depend +++ /dev/null @@ -1,8 +0,0 @@ -cicXPath.cmo: cicXPath.cmi -cicXPath.cmx: cicXPath.cmi -cicAnnotation2Xml.cmo: cicXPath.cmi cicAnnotation2Xml.cmi -cicAnnotation2Xml.cmx: cicXPath.cmx cicAnnotation2Xml.cmi -cicAnnotationParser2.cmo: cicAnnotationParser2.cmi -cicAnnotationParser2.cmx: cicAnnotationParser2.cmi -cicAnnotationParser.cmo: cicAnnotationParser2.cmi cicAnnotationParser.cmi -cicAnnotationParser.cmx: cicAnnotationParser2.cmx cicAnnotationParser.cmi diff --git a/helm/ocaml/cic_annotations/Makefile b/helm/ocaml/cic_annotations/Makefile deleted file mode 100644 index 2fbfe1bec..000000000 --- a/helm/ocaml/cic_annotations/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -PACKAGE = cic_annotations -REQUIRES = helm-cic helm-xml -PREDICATES = - -INTERFACE_FILES = cicXPath.mli cicAnnotation2Xml.mli cicAnnotationParser2.mli \ - cicAnnotationParser.mli -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -include ../Makefile.common diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml deleted file mode 100644 index 4c028208f..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ /dev/null @@ -1,165 +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/. - *) - -(*CSC codice cut & paste da cicPp e xmlcommand *) - -exception NotImplemented;; - -let dtdname = "http://www.cs.unibo.it/helm/dtd/annotations.dtd";; - -let get_ann ids_to_annotations = - CicXPath.get_annotation ids_to_annotations -;; - -let print_ann i2a id = - let module X = Xml in - let ann = get_ann i2a id in - match ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" [None,"of", id] (X.xml_cdata ann)) -;; - -(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) -(* It takes in input a hash table mapping ids to annotations, an annotated -term, and gives back a Xml.token Stream.t representing the .ann file *) -let print_term i2a = - let rec aux = - let module C = Cic in - let module X = Xml in - let module U = UriManager in - function - C.ARel (id,_,_,_) -> print_ann i2a id - | C.AMeta (id,_,_) -> print_ann i2a id - | C.ASort (id,_) -> print_ann i2a id - | C.AImplicit _ -> raise NotImplemented - | C.AProd (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] - | C.ACast (id,v,t) -> [< print_ann i2a id ; aux v ; aux t >] - | C.ALambda (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] - | C.ALetIn (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] - | C.AAppl (id,li) -> - [< print_ann i2a id ; - List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>] - >] - | C.AVar (id,_,exp_named_subst) - | C.AConst (id,_,exp_named_subst) - | C.AMutInd (id,_,_,exp_named_subst) - | C.AMutConstruct (id,_,_,_,exp_named_subst) -> - [< print_ann i2a id ; - List.fold_right - (fun (_,x) i -> [< aux x ; i >]) - exp_named_subst [<>] - >] - | C.AMutCase (id,_,_,ty,te,patterns) -> - [< print_ann i2a id ; - aux ty ; - aux te ; - List.fold_right - (fun x i -> [< aux x ; i>]) - patterns [<>] - >] - | C.AFix (id,_,funs) -> - [< print_ann i2a id ; - List.fold_right - (fun (_,_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] - >] - | C.ACoFix (id,no,funs) -> - [< print_ann i2a id ; - List.fold_right - (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] - >] - in - aux -;; - -let print_mutual_inductive_type i2a (_,_,_,arity,constructors) = - [< print_term i2a arity ; - List.fold_right - (fun (name,ty) i -> [< print_term i2a ty ; i >]) constructors [<>] - >] -;; - -let pp_annotation obj i2a curi = - let module C = Cic in - let module X = Xml in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n\n") ; - X.xml_nempty "Annotations" - [None, "of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] - begin - match obj with - C.AConstant (xid, xidobj, _, te, ty, _, _) -> - [< print_ann i2a xid ; - (match xidobj,te with - Some xidobj, Some te -> - [< print_ann i2a xidobj ; - print_term i2a te - >] - | None, None -> [<>] - | _,_ -> assert false - ) ; - print_term i2a ty - >] - | C.AVariable (xid, _, bo, ty,_, _) -> - [< print_ann i2a xid ; - (match bo with - None -> [<>] - | Some bo -> print_term i2a bo - ) ; - print_term i2a ty - >] - | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_, _) -> - [< print_ann i2a xid ; - print_ann i2a xidobj ; - List.fold_right - (fun (cid, _, context, t) i -> - [< print_ann i2a cid ; - List.fold_right - (fun (hid,context_entry) i -> - [ print_term i2a at - | Some (_,C.ADef at) -> print_term i2a at - | None -> [< >] - ) ; i - >] - ) context [< >]; - print_term i2a t ; i - >] - ) conjs [<>] ; - print_term i2a bo ; - print_term i2a ty - >] - | C.AInductiveDefinition (xid, tys, params, paramsno, _) -> - [< print_ann i2a xid ; - List.fold_right - (fun x i -> [< print_mutual_inductive_type i2a x ; i >]) - tys [< >] - >] - end - >] -;; - - - diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli b/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli deleted file mode 100644 index 69faf6e60..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli +++ /dev/null @@ -1,38 +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 *) -(* *) -(* *) -(******************************************************************************) - -val pp_annotation : - Cic.annobj -> (Cic.id, string) Hashtbl.t -> UriManager.uri -> - Xml.token Stream.t diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser.ml b/helm/ocaml/cic_annotations/cicAnnotationParser.ml deleted file mode 100644 index 2d04cbc80..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotationParser.ml +++ /dev/null @@ -1,42 +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/. - *) - -exception EmptyUri;; - -let get_annotations filename = - try - let d = - let config = PxpHelmConf.pxp_config in - Pxp_tree_parser.parse_document_entity config - (Pxp_types.from_file ~alt:[PxpUrlResolver.url_resolver] filename) - PxpHelmConf.pxp_spec - - in - CicAnnotationParser2.get_annotations d#root - with - e -> - print_endline (Pxp_types.string_of_exn e) ; - raise e -;; diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser.mli b/helm/ocaml/cic_annotations/cicAnnotationParser.mli deleted file mode 100644 index 582013e3e..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotationParser.mli +++ /dev/null @@ -1,36 +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 *) -(* *) -(* *) -(******************************************************************************) - -val get_annotations : string -> (Cic.id, string) Hashtbl.t diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser2.ml b/helm/ocaml/cic_annotations/cicAnnotationParser2.ml deleted file mode 100644 index 15d86f5cd..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotationParser2.ml +++ /dev/null @@ -1,96 +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/. - *) - -exception IllFormedXml of int;; - -(* Utility functions that transform a Pxp attribute into something useful *) - -let string_of_attr a = - let module T = Pxp_types in - match a with - T.Value s -> s - | _ -> raise (IllFormedXml 0) -;; - -exception DontKnowWhatToDo;; - -let rec string_of_annotations n = - let module D = Pxp_document in - let module T = Pxp_types in - match n#node_type with - D.T_element s -> - "<" ^ s ^ - List.fold_right - (fun att i -> - match n#attribute att with - T.Value s -> " " ^ att ^ "=\"" ^ s ^ "\"" ^ i - | T.Implied_value -> i - | T.Valuelist l -> " " ^ att ^ "=\"" ^ String.concat " " l ^ "\"" ^ i - ) (n#attribute_names) "" ^ - (match n#sub_nodes with - [] -> "/>" - | l -> - ">" ^ - String.concat "" (List.map string_of_annotations l) ^ - "" - ) - | D.T_data -> n#data - | _ -> raise DontKnowWhatToDo -;; - -let get_annotation_from_node n = - String.concat "" (List.map string_of_annotations (n#sub_nodes)) -;; - -exception MoreThanOneAnnotationFor of Cic.id;; - -let set_annotation ids_to_annotations id ann = - try - ignore (Hashtbl.find ids_to_annotations id) ; - raise (MoreThanOneAnnotationFor id) - with - Not_found -> Hashtbl.add ids_to_annotations id ann -;; - -let get_annotations n = - let module D = Pxp_document in - let module C = Cic in - let ids_to_annotations = Hashtbl.create 503 in - let annotate_elem n = - let ntype = n # node_type in - match ntype with - D.T_element "Annotation" -> - let of_uri = string_of_attr (n # attribute "of") in - set_annotation ids_to_annotations of_uri (get_annotation_from_node n) - | D.T_element _ | D.T_data -> - raise (IllFormedXml 1) - | _ -> raise DontKnowWhatToDo - in - match n # node_type with - D.T_element "Annotations" -> - List.iter annotate_elem (n # sub_nodes) ; - ids_to_annotations - | _ -> raise (IllFormedXml 2) -;; diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser2.mli b/helm/ocaml/cic_annotations/cicAnnotationParser2.mli deleted file mode 100644 index f16bb6fe8..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotationParser2.mli +++ /dev/null @@ -1,50 +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 *) -(* *) -(* *) -(******************************************************************************) - -exception IllFormedXml of int -val get_annotations : - < node_type : Pxp_document.node_type; - sub_nodes : < attribute : string -> Pxp_types.att_value; - node_type : Pxp_document.node_type; - sub_nodes : (< attribute : string -> Pxp_types.att_value; - attribute_names : string list; - data : string; - node_type : Pxp_document.node_type; - sub_nodes : 'a list; .. > as 'a) - list; - .. > - list; - .. > -> - (Cic.id, string) Hashtbl.t diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml deleted file mode 100644 index b9533d18f..000000000 --- a/helm/ocaml/cic_annotations/cicXPath.ml +++ /dev/null @@ -1,146 +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 *) -(* 14/06/2000 *) -(* *) -(* *) -(******************************************************************************) - -let get_annotation ids_to_annotations xpath = - try - Some (Hashtbl.find ids_to_annotations xpath) - with - Not_found -> None -;; - -exception MoreThanOneTargetFor of Cic.id;; - -(* creates a hashtable mapping each unique id to a node of the annotated -object *) -let get_ids_to_targets annobj = - let module C = Cic in - let ids_to_targets = Hashtbl.create 503 in - let set_target id target = - try - ignore (Hashtbl.find ids_to_targets id) ; - raise (MoreThanOneTargetFor id) - with - Not_found -> Hashtbl.add ids_to_targets id target - in - let rec add_target_term t = - match t with - C.ARel (id,_,_,_) - | C.AMeta (id,_,_) - | C.ASort (id,_) - | C.AImplicit (id, _) -> - set_target id (C.Term t) - | C.ACast (id,va,ty) -> - set_target id (C.Term t) ; - add_target_term va ; - add_target_term ty - | C.AProd (id,_,so,ta) - | C.ALambda (id,_,so,ta) - | C.ALetIn (id,_,so,ta) -> - set_target id (C.Term t) ; - add_target_term so ; - add_target_term ta - | C.AAppl (id,l) -> - set_target id (C.Term t) ; - List.iter add_target_term l - | C.AVar (id,_,exp_named_subst) - | C.AConst (id,_,exp_named_subst) - | C.AMutInd (id,_,_,exp_named_subst) - | C.AMutConstruct (id,_,_,_,exp_named_subst) -> - set_target id (C.Term t) ; - List.iter (function (_,t) -> add_target_term t) exp_named_subst - | C.AMutCase (id,_,_,ot,it,pl) -> - set_target id (C.Term t) ; - List.iter add_target_term (ot::it::pl) - | C.AFix (id,_,ifl) -> - set_target id (C.Term t) ; - List.iter - (function (_,_,_,ty,bo) -> - add_target_term ty ; - add_target_term bo - ) ifl - | C.ACoFix (id,_,cfl) -> - set_target id (C.Term t) ; - List.iter - (function (_,_,ty,bo) -> - add_target_term ty ; - add_target_term bo - ) cfl - in - let add_target_obj annobj = - match annobj with - C.AConstant (id,idbody,_,bo,ty,_,_) -> - set_target id (C.Object annobj) ; - (match idbody,bo with - Some idbody,Some bo -> - set_target idbody (C.ConstantBody annobj) ; - add_target_term bo - | None, None -> () - | _,_ -> assert false - ) ; - add_target_term ty - | C.AVariable (id,_,None,ty,_,_) -> - set_target id (C.Object annobj) ; - add_target_term ty - | C.AVariable (id,_,Some bo,ty,_,_) -> - set_target id (C.Object annobj) ; - add_target_term bo ; - add_target_term ty - | C.ACurrentProof (id,idbody,_,cl,bo,ty,_,_) -> - set_target id (C.Object annobj) ; - set_target idbody (C.ConstantBody annobj) ; - List.iter (function (cid,_,context, t) as annconj -> - set_target cid (C.Conjecture annconj) ; - List.iter - (function ((hid,h) as annhyp) -> - set_target hid (C.Hypothesis annhyp) ; - match h with - Some (_,C.ADecl at) -> add_target_term at - | Some (_,C.ADef at) -> add_target_term at - | None -> () - ) context; - add_target_term t) cl ; - add_target_term bo ; - add_target_term ty - | C.AInductiveDefinition (id,itl,_,_,_) -> - set_target id (C.Object annobj) ; - List.iter - (function (_,_,_,arity,cl) -> - add_target_term arity ; - List.iter (function (_,ty) -> add_target_term ty) cl - ) itl - in - add_target_obj annobj ; - ids_to_targets -;; diff --git a/helm/ocaml/cic_annotations/cicXPath.mli b/helm/ocaml/cic_annotations/cicXPath.mli deleted file mode 100644 index 23380e02a..000000000 --- a/helm/ocaml/cic_annotations/cicXPath.mli +++ /dev/null @@ -1,39 +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 *) -(* *) -(* *) -(******************************************************************************) - -val get_annotation : - (Cic.id, string) Hashtbl.t -> Cic.id -> string option - -val get_ids_to_targets : Cic.annobj -> (Cic.id, Cic.anntarget) Hashtbl.t diff --git a/helm/ocaml/tex_cic_textual_parser/.cvsignore b/helm/ocaml/tex_cic_textual_parser/.cvsignore deleted file mode 100644 index 1569cb433..000000000 --- a/helm/ocaml/tex_cic_textual_parser/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.cm[iaox] *.cmxa texCicTextualParser.ml texCicTextualParser.mli texCicTextualLexer.ml diff --git a/helm/ocaml/tex_cic_textual_parser/.depend b/helm/ocaml/tex_cic_textual_parser/.depend deleted file mode 100644 index 71156776a..000000000 --- a/helm/ocaml/tex_cic_textual_parser/.depend +++ /dev/null @@ -1,9 +0,0 @@ -texCicTextualParserContext.cmi: texCicTextualParser.cmi -texCicTextualParser.cmo: texCicTextualParser0.cmo texCicTextualParser.cmi -texCicTextualParser.cmx: texCicTextualParser0.cmx texCicTextualParser.cmi -texCicTextualParserContext.cmo: texCicTextualParser.cmi \ - texCicTextualParser0.cmo texCicTextualParserContext.cmi -texCicTextualParserContext.cmx: texCicTextualParser.cmx \ - texCicTextualParser0.cmx texCicTextualParserContext.cmi -texCicTextualLexer.cmo: texCicTextualParser.cmi -texCicTextualLexer.cmx: texCicTextualParser.cmx diff --git a/helm/ocaml/tex_cic_textual_parser/Makefile b/helm/ocaml/tex_cic_textual_parser/Makefile deleted file mode 100644 index b57b3a8ba..000000000 --- a/helm/ocaml/tex_cic_textual_parser/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -PACKAGE = tex_cic_textual_parser -REQUIRES = helm-cic helm-cic_textual_parser -PREDICATES = - -INTERFACE_FILES = texCicTextualParser.mli texCicTextualParserContext.mli -IMPLEMENTATION_FILES = texCicTextualParser0.ml $(INTERFACE_FILES:%.mli=%.ml) \ - texCicTextualLexer.ml -EXTRA_OBJECTS_TO_INSTALL = texCicTextualParser0.ml texCicTextualParser0.cmi \ - texCicTextualLexer.mll texCicTextualParser.mly - -EXTRA_OBJECTS_TO_CLEAN = texCicTextualParser.ml texCicTextualParser.mli \ - texCicTextualLexer.ml - -include ../Makefile.common diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll deleted file mode 100644 index 5ab17fa80..000000000 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll +++ /dev/null @@ -1,134 +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/. - *) - -{ - open TexCicTextualParser;; - module L = Lexing;; - module U = UriManager;; - - let indtyuri_of_uri uri = - let index_sharp = String.index uri '#' in - let index_num = index_sharp + 3 in - try - (UriManager.uri_of_string (String.sub uri 0 index_sharp), - int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1 - ) - with - Failure msg -> - raise (CicTextualParser0.LexerFailure "Not an inductive URI") - ;; - - let indconuri_of_uri uri = - let index_sharp = String.index uri '#' in - let index_div = String.rindex uri '/' in - let index_con = index_div + 1 in - try - (UriManager.uri_of_string (String.sub uri 0 index_sharp), - int_of_string - (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1, - int_of_string - (String.sub uri index_con (String.length uri - index_con)) - ) - with - Failure msg -> - raise (CicTextualParser0.LexerFailure "Not a constructor URI") - ;; - - (* TeX unquoting for "_" *) - let unquote str = - Str.global_replace (Str.regexp "\\\\_") "_" str - ;; -} -let dollar = '$' -let num = ['1'-'9']['0'-'9']* | '0' -let letter = ['A'-'Z' 'a'-'z'] -let alfa = letter | ['_' ''' '-'] | "\\_" -let ident = letter (alfa | num)* -let baseuri = '/'(ident '/')* ident '.' -let conuri = baseuri "con" -let varuri = baseuri "var" -let indtyuri = baseuri "ind#1/" num -let indconuri = baseuri "ind#1/" num "/" num -let blanks = [' ' '\t' '\n' '~' '{' '}'] | "\\;" | "\\rm" -rule token = - parse - blanks { token lexbuf } (* skip blanks *) - | "\\Case" { CASE } - | "\\Fix" { FIX } - | "\\CoFix" { COFIX } - | "\\Set" { SET } - | "\\Prop" { PROP } - | "\\Type" { TYPE } - | "\\CProp" { CPROP } - | ident { ID (unquote (L.lexeme lexbuf)) } - | conuri { CONURI - (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) } - | varuri { VARURI - (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) } - | indtyuri { INDTYURI - (indtyuri_of_uri ("cic:" ^ (unquote (L.lexeme lexbuf)))) } - | indconuri { INDCONURI - (indconuri_of_uri("cic:" ^ (unquote (L.lexeme lexbuf)))) } - | num '.' { - let lexeme = L.lexeme lexbuf in - RNUM (int_of_string - (String.sub lexeme 0 (String.length lexeme - 1))) - } - | num { NUM (int_of_string (L.lexeme lexbuf)) } - | '?' num { let lexeme = L.lexeme lexbuf in - META - (int_of_string - (String.sub lexeme 1 (String.length lexeme - 1))) } - | ":>" { CAST } - | ":=" { LETIN } - | '?' { IMPLICIT } - | '(' { LPAREN } - | ')' { RPAREN } - | "\\[" { LBRACKET } - | "\\]" { RBRACKET } - | "\\{" { LCURLY } - | "\\}" { RCURLY } - | ';' { SEMICOLON } - | "\\lambda" { LAMBDA } - | "\\pi" { PROD } - | "\\forall" { PROD } - | "\\eqt" { EQT } - | "\\neqt" { NEQT } - | ':' { COLON } - | '.' { DOT } - | "\\to" { ARROW } - | '_' { NONE } - | dollar { DOLLAR } - | eof { EOF } - (* Arithmetical operators *) - | "+." { RPLUS } - | "-." { RMINUS } - | "*." { RTIMES } - | "/." { RDIV } - | '+' { PLUS } - | '-' { MINUS } - | '*' { TIMES } - | '=' { EQ } -{} diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly deleted file mode 100644 index 41a36acc6..000000000 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly +++ /dev/null @@ -1,659 +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/. - */ - -%{ - open Cic;; - module U = UriManager;; - - exception InvalidSuffix of string;; - exception InductiveTypeURIExpected;; - exception UnknownIdentifier of string;; - exception ExplicitNamedSubstitutionAppliedToRel;; - exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;; - - (* merge removing duplicates of two lists free of duplicates *) - let union dom1 dom2 = - let rec filter = - function - [] -> [] - | he::tl -> - if List.mem he dom1 then filter tl else he::(filter tl) - in - dom1 @ (filter dom2) - ;; - - let get_index_in_list e = - let rec aux i = - function - [] -> raise Not_found - | (Some he)::_ when he = e -> i - | _::tl -> aux (i+1) tl - in - aux 1 - ;; - - (* Returns the first meta whose number is above the *) - (* number of the higher meta. *) - (*CSC: cut&pasted from proofEngine.ml *) - let new_meta () = - let rec aux = - function - None,[] -> 1 - | Some n,[] -> n - | None,(n,_,_)::tl -> aux (Some n,tl) - | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) - in - 1 + aux (None,!TexCicTextualParser0.metasenv) - ;; - - (* identity_relocation_list_for_metavariable i canonical_context *) - (* returns the identity relocation list, which is the list [1 ; ... ; n] *) - (* where n = List.length [canonical_context] *) - (*CSC: ma mi basta la lunghezza del contesto canonico!!!*) - (*CSC: cut&pasted from proofEngine.ml *) - let identity_relocation_list_for_metavariable canonical_context = - let canonical_context_length = List.length canonical_context in - let rec aux = - function - (_,[]) -> [] - | (n,None::tl) -> None::(aux ((n+1),tl)) - | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) - in - aux (1,canonical_context) - ;; - - let deoptionize_exp_named_subst = - function - None -> [], (function _ -> []) - | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst - ;; - - let term_of_con_uri uri exp_named_subst = - Const (uri,exp_named_subst) - ;; - - let term_of_var_uri uri exp_named_subst = - Var (uri,exp_named_subst) - ;; - - let term_of_indty_uri (uri,tyno) exp_named_subst = - MutInd (uri, tyno, exp_named_subst) - ;; - - let term_of_indcon_uri (uri,tyno,consno) exp_named_subst = - MutConstruct (uri, tyno, consno, exp_named_subst) - ;; - - let term_of_uri uri = - match uri with - CicTextualParser0.ConUri uri -> - term_of_con_uri uri - | CicTextualParser0.VarUri uri -> - term_of_var_uri uri - | CicTextualParser0.IndTyUri (uri,tyno) -> - term_of_indty_uri (uri,tyno) - | CicTextualParser0.IndConUri (uri,tyno,consno) -> - term_of_indcon_uri (uri,tyno,consno) - ;; - - let var_uri_of_id id interp = - let module CTP0 = CicTextualParser0 in - match interp (CicTextualParser0.Id id) with - None -> raise (UnknownIdentifier id) - | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri - | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable - ;; - - let indty_uri_of_id id interp = - let module CTP0 = CicTextualParser0 in - match interp (CicTextualParser0.Id id) with - None -> raise (UnknownIdentifier id) - | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno) - | Some _ -> raise InductiveTypeURIExpected - ;; - - let mk_implicit () = - let newmeta = new_meta () in - let newuniv = CicUniv.fresh () in - let new_canonical_context = [] in - let irl = - identity_relocation_list_for_metavariable new_canonical_context - in - TexCicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort (Type newuniv); - (* TASSI: ?? *) - newmeta+1, new_canonical_context, Meta (newmeta,irl); - newmeta+2, new_canonical_context, Meta (newmeta+1,irl) - ] @ !TexCicTextualParser0.metasenv ; - [], function _ -> Meta (newmeta+2,irl) - ;; -%} -%token ID -%token META -%token NUM -%token RNUM -%token CONURI -%token VARURI -%token INDTYURI -%token INDCONURI -%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE -%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF -%token DOLLAR -%token RPLUS RMINUS RTIMES RDIV -%token PLUS MINUS TIMES EQT EQ NEQT -%right ARROW -%nonassoc EQ EQT NEQT -%left PLUS MINUS RPLUS RMINUS -%left TIMES RTIMES RDIV -%start main -%type Cic.term)> main -%% -main: - | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */ - | DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof } - | DOLLAR DOLLAR DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof } - | expr EOF { $1 } - | DOLLAR expr DOLLAR EOF { $2 } - | DOLLAR DOLLAR expr DOLLAR DOLLAR EOF { $3 } - | expr SEMICOLON { $1 } /* FG: to read several terms in a row - * Do we need to clear some static variables? - */ -; -expr2: - | RNUM - { [], function interp -> - let rec cic_real_of_real = - function - 0 -> Cic.Const (HelmLibraryObjects.Reals.r0_URI, []) - | 1 -> Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]) - | n -> - Cic.Appl - [ Cic.Const - (HelmLibraryObjects.Reals.rplus_URI,[]) ; - Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]); - cic_real_of_real (n - 1) - ] - in - cic_real_of_real $1 - } - | NUM - { [], function interp -> - let rec cic_int_of_int = - function - 0 -> - Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,1,[]) - | n -> - Cic.Appl - [ Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,2,[]) ; - cic_int_of_int (n - 1) - ] - in - cic_int_of_int $1 - } - | expr2 RPLUS expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom = union dom1 dom2 in - dom, function interp -> - Cic.Appl - [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | expr2 RMINUS expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom = union dom1 dom2 in - dom, function interp -> - Cic.Appl - [Cic.Const (HelmLibraryObjects.Reals.rminus_URI,[]); - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | expr2 RTIMES expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom = union dom1 dom2 in - dom, function interp -> - Cic.Appl - [Cic.Const (HelmLibraryObjects.Reals.rmult_URI,[]) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | expr2 RDIV expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom = union dom1 dom2 in - dom, function interp -> - Cic.Appl - [Cic.Const (HelmLibraryObjects.Reals.rdiv_URI,[]) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | expr2 PLUS expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom = union dom1 dom2 in - dom, function interp -> - Cic.Appl - [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | expr2 MINUS expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom = union dom1 dom2 in - dom, function interp -> - Cic.Appl - [Cic.Const (HelmLibraryObjects.Peano.minus_URI,[]) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | expr2 TIMES expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom = union dom1 dom2 in - dom, function interp -> - Cic.Appl - [Cic.Const (HelmLibraryObjects.Peano.mult_URI,[]) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | expr2 EQ expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom3,mk_expr3 = mk_implicit () in - let dom = union dom1 (union dom2 dom3) in - dom, function interp -> - Cic.Appl - [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI,0,[]) ; - (mk_expr3 interp) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | CONURI exp_named_subst - { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in - dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp) - } - | VARURI exp_named_subst - { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in - dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp) - } - | INDTYURI exp_named_subst - { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in - dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp) - } - | INDCONURI exp_named_subst - { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in - dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp) - } - | ID exp_named_subst - { try - let res = - Rel (get_index_in_list (Name $1) !TexCicTextualParser0.binders) - in - (match $2 with - None -> ([], function _ -> res) - | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel) - ) - with - Not_found -> - let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in - let dom = union dom1 [CicTextualParser0.Id $1] in - dom, - function interp -> - match interp (CicTextualParser0.Id $1) with - None -> raise (UnknownIdentifier $1) - | Some (CicTextualParser0.Uri uri) -> - term_of_uri uri (mk_exp_named_subst interp) - | Some CicTextualParser0.Implicit -> - (*CSC: not very clean; to maximize code reusage *) - snd (mk_implicit ()) "" - | Some (CicTextualParser0.Term mk_term) -> - (mk_term interp) - } - | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY - { let dom1,mk_expr1 = $3 in - let dom2,mk_expr2 = $7 in - let dom3,mk_expr3 = $10 in - let dom = union dom1 (union dom2 dom3) in - dom, - function interp -> - MutCase - (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp)) - } - | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY - { let dom1,mk_expr1 = $3 in - let dom2,mk_expr2 = $7 in - let dom3,mk_expr3 = $10 in - let dom = - union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3)) - in - dom, - function interp -> - let uri,typeno = indty_uri_of_id $5 interp in - MutCase - (uri,typeno,(mk_expr2 interp),(mk_expr1 interp), - (mk_expr3 interp)) - } - | fixheader LCURLY exprseplist RCURLY - { let dom1,foo,ids_and_indexes,mk_types = $1 in - let dom2,mk_exprseplist = $3 in - let dom = union dom1 dom2 in - for i = 1 to List.length ids_and_indexes do - TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders - done ; - dom, - function interp -> - let types = mk_types interp in - let fixfunsbodies = (mk_exprseplist interp) in - let idx = - let rec find idx = - function - [] -> raise Not_found - | (name,_)::_ when name = foo -> idx - | _::tl -> find (idx+1) tl - in - find 0 ids_and_indexes - in - let fixfuns = - List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo)) - (List.combine ids_and_indexes types) fixfunsbodies - in - Fix (idx,fixfuns) - } - | cofixheader LCURLY exprseplist RCURLY - { let dom1,foo,ids,mk_types = $1 in - let dom2,mk_exprseplist = $3 in - let dom = union dom1 dom2 in - dom, - function interp -> - let types = mk_types interp in - let fixfunsbodies = (mk_exprseplist interp) in - let idx = - let rec find idx = - function - [] -> raise Not_found - | name::_ when name = foo -> idx - | _::tl -> find (idx+1) tl - in - find 0 ids - in - let fixfuns = - List.map2 (fun (name,ty) bo -> (name,ty,bo)) - (List.combine ids types) fixfunsbodies - in - for i = 1 to List.length fixfuns do - TexCicTextualParser0.binders := - List.tl !TexCicTextualParser0.binders - done ; - CoFix (idx,fixfuns) - } - | IMPLICIT - { mk_implicit () } - | SET { [], function _ -> Sort Set } - | PROP { [], function _ -> Sort Prop } - | TYPE { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)} - | CPROP { [], function _ -> Sort CProp } - | LPAREN expr CAST expr RPAREN - { let dom1,mk_expr1 = $2 in - let dom2,mk_expr2 = $4 in - let dom = union dom1 dom2 in - dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp)) - } - | META LBRACKET substitutionlist RBRACKET - { let dom,mk_substitutionlist = $3 in - dom, function interp -> Meta ($1, mk_substitutionlist interp) - } - | LPAREN expr exprlist RPAREN - { let length,dom2,mk_exprlist = $3 in - match length with - 0 -> $2 - | _ -> - let dom1,mk_expr1 = $2 in - let dom = union dom1 dom2 in - dom, - function interp -> - Appl ((mk_expr1 interp)::(mk_exprlist interp)) - } -; -exp_named_subst : - { None } - | LCURLY named_substs RCURLY - { Some $2 } -; -named_substs : - VARURI LETIN expr2 - { let dom,mk_expr = $3 in - dom, function interp -> [$1, mk_expr interp] } - | ID LETIN expr2 - { let dom1,mk_expr = $3 in - let dom = union [CicTextualParser0.Id $1] dom1 in - dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] } - | VARURI LETIN expr2 SEMICOLON named_substs - { let dom1,mk_expr = $3 in - let dom2,mk_named_substs = $5 in - let dom = union dom1 dom2 in - dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp) - } - | ID LETIN expr2 SEMICOLON named_substs - { let dom1,mk_expr = $3 in - let dom2,mk_named_substs = $5 in - let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in - dom, - function interp -> - (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp) - } -; -expr : - pihead expr - { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ; - let dom1,mk_expr1 = snd $1 in - let dom2,mk_expr2 = $2 in - let dom = union dom1 dom2 in - dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp) - } - | lambdahead expr - { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ; - let dom1,mk_expr1 = snd $1 in - let dom2,mk_expr2 = $2 in - let dom = union dom1 dom2 in - dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp) - } - | letinhead expr - { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ; - let dom1,mk_expr1 = snd $1 in - let dom2,mk_expr2 = $2 in - let dom = union dom1 dom2 in - dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp) - } - | expr2 - { $1 } -; -fixheader: - FIX ID LCURLY fixfunsdecl RCURLY - { let dom,ids_and_indexes,mk_types = $4 in - let bs = - List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes - in - TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ; - dom, $2, ids_and_indexes, mk_types - } -; -fixfunsdecl: - ID LPAREN NUM RPAREN COLON expr - { let dom,mk_expr = $6 in - dom, [$1,$3], function interp -> [mk_expr interp] - } - | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl - { let dom1,mk_expr = $6 in - let dom2,ids_and_indexes,mk_types = $8 in - let dom = union dom1 dom2 in - dom, ($1,$3)::ids_and_indexes, - function interp -> (mk_expr interp)::(mk_types interp) - } -; -cofixheader: - COFIX ID LCURLY cofixfunsdecl RCURLY - { let dom,ids,mk_types = $4 in - let bs = - List.rev_map (function name -> Some (Name name)) ids - in - TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ; - dom, $2, ids, mk_types - } -; -cofixfunsdecl: - ID COLON expr - { let dom,mk_expr = $3 in - dom, [$1], function interp -> [mk_expr interp] - } - | ID COLON expr SEMICOLON cofixfunsdecl - { let dom1,mk_expr = $3 in - let dom2,ids,mk_types = $5 in - let dom = union dom1 dom2 in - dom, $1::ids, - function interp -> (mk_expr interp)::(mk_types interp) - } -; -pihead: - PROD ID COLON expr DOT - { TexCicTextualParser0.binders := - (Some (Name $2))::!TexCicTextualParser0.binders; - let dom,mk_expr = $4 in - Cic.Name $2, (dom, function interp -> mk_expr interp) - } - | expr2 ARROW - { TexCicTextualParser0.binders := - (Some Anonymous)::!TexCicTextualParser0.binders ; - let dom,mk_expr = $1 in - Anonymous, (dom, function interp -> mk_expr interp) - } - | PROD ID DOT - { TexCicTextualParser0.binders := - (Some (Name $2))::!TexCicTextualParser0.binders; - let newmeta = new_meta () in - let newuniv = CicUniv.fresh () in - let new_canonical_context = [] in - let irl = - identity_relocation_list_for_metavariable new_canonical_context - in - TexCicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort (Type newuniv); - (* TASSI: ?? *) - newmeta+1, new_canonical_context, Meta (newmeta,irl) - ] @ !TexCicTextualParser0.metasenv ; - Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) - } -; -lambdahead: - LAMBDA ID COLON expr DOT - { TexCicTextualParser0.binders := - (Some (Name $2))::!TexCicTextualParser0.binders; - let dom,mk_expr = $4 in - Cic.Name $2, (dom, function interp -> mk_expr interp) - } - | LAMBDA ID DOT - { TexCicTextualParser0.binders := - (Some (Name $2))::!TexCicTextualParser0.binders; - let newmeta = new_meta () in - let newuniv = CicUniv.fresh () in - let new_canonical_context = [] in - let irl = - identity_relocation_list_for_metavariable new_canonical_context - in - TexCicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort (Type newuniv) ; - (* TASSI: ?? *) - newmeta+1, new_canonical_context, Meta (newmeta,irl) - ] @ !TexCicTextualParser0.metasenv ; - Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) - } -; -letinhead: - LAMBDA ID LETIN expr DOT - { TexCicTextualParser0.binders := - (Some (Name $2))::!TexCicTextualParser0.binders ; - let dom,mk_expr = $4 in - Cic.Name $2, (dom, function interp -> mk_expr interp) - } -; -branches: - { [], function _ -> [] } - | expr SEMICOLON branches - { let dom1,mk_expr = $1 in - let dom2,mk_branches = $3 in - let dom = union dom1 dom2 in - dom, function interp -> (mk_expr interp)::(mk_branches interp) - } - | expr - { let dom,mk_expr = $1 in - dom, function interp -> [mk_expr interp] - } -; -exprlist: - - { 0, [], function _ -> [] } - | expr exprlist - { let dom1,mk_expr = $1 in - let length,dom2,mk_exprlist = $2 in - let dom = union dom1 dom2 in - length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp) - } -; -exprseplist: - expr - { let dom,mk_expr = $1 in - dom, function interp -> [mk_expr interp] - } - | expr SEMICOLON exprseplist - { let dom1,mk_expr = $1 in - let dom2,mk_exprseplist = $3 in - let dom = union dom1 dom2 in - dom, function interp -> (mk_expr interp)::(mk_exprseplist interp) - } -; -substitutionlist: - { [], function _ -> [] } - | expr SEMICOLON substitutionlist - { let dom1,mk_expr = $1 in - let dom2,mk_substitutionlist = $3 in - let dom = union dom1 dom2 in - dom, - function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp) - } - | NONE SEMICOLON substitutionlist - { let dom,mk_exprsubstitutionlist = $3 in - dom, function interp -> None::(mk_exprsubstitutionlist interp) - } diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser0.ml b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser0.ml deleted file mode 100644 index 133f2e0bb..000000000 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser0.ml +++ /dev/null @@ -1,27 +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/. - *) - -let binders = ref ([] : (Cic.name option) list);; -let metasenv = ref ([] : Cic.metasenv);; diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml deleted file mode 100644 index e14259589..000000000 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml +++ /dev/null @@ -1,38 +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/. - *) - -let main ~context ~metasenv lexer lexbuf = - (* Warning: higly non-reentrant code!!! *) - TexCicTextualParser0.binders := context ; - TexCicTextualParser0.metasenv := metasenv ; - let dom,mk_term = TexCicTextualParser.main lexer lexbuf in - let metasenv' = !TexCicTextualParser0.metasenv in - dom, - function interp -> - TexCicTextualParser0.metasenv := metasenv' ; - let term = mk_term interp in - let metasenv = !TexCicTextualParser0.metasenv in - metasenv,term -;; diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.mli b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.mli deleted file mode 100644 index 492b52d09..000000000 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.mli +++ /dev/null @@ -1,31 +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/. - *) - -val main : - context:((Cic.name option) list) -> - metasenv:Cic.metasenv -> - (Lexing.lexbuf -> TexCicTextualParser.token) -> Lexing.lexbuf -> - CicTextualParser0.interpretation_domain_item list * - (CicTextualParser0.interpretation -> (Cic.metasenv * Cic.term))