+++ /dev/null
-*.cm[iaox] *.cmxa
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* 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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\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_ann i2a hid ;
- (match context_entry with
- Some (_,C.ADecl at) -> 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
- >]
-;;
-
-
-
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 29/11/2000 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-val pp_annotation :
- Cic.annobj -> (Cic.id, string) Hashtbl.t -> UriManager.uri ->
- Xml.token Stream.t
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 29/11/2000 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-val get_annotations : string -> (Cic.id, string) Hashtbl.t
+++ /dev/null
-(* 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) ^
- "</" ^ s ^ ">"
- )
- | 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)
-;;
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
-;;
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
+++ /dev/null
-*.cm[iaox] *.cmxa texCicTextualParser.ml texCicTextualParser.mli texCicTextualLexer.ml
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* 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 }
-{}
+++ /dev/null
-/* 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 <string> ID
-%token <int> META
-%token <int> NUM
-%token <int> RNUM
-%token <UriManager.uri> CONURI
-%token <UriManager.uri> VARURI
-%token <UriManager.uri * int> INDTYURI
-%token <UriManager.uri * int * int> 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 <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> 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)
- }
+++ /dev/null
-(* 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);;
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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))
projects / helm.git / commitdiff