-OCAMLOPTIONS = -package netstring -package netclient -package pxp
-
+BIN_DIR = /usr/local/bin
+REQUIRES = helm-xml helm-cic_proof_checking
+PREDICATES = miniReduction
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
OCAMLDEP = ocamldep
OCAMLFIND = ocamlfind
OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS)
all: mk_forward
opt: mk_forward.opt
-DEPOBJS = xml.ml xml.mli csc_pxp_reader.ml configuration.ml \
- clientHTTP.ml clientHTTP.mli cic.ml deannotate.ml \
- uriManager.ml uriManager.mli getter.ml getter.mli \
- pxpUriResolver.ml cicParser3.ml cicParser3.mli \
- cicParser2.ml cicParser2.mli cicParser.ml \
- cicParser.mli cicSubstitution.ml cicSubstitution.mli \
- cicMiniReduction.ml cicMiniReduction.mli mk_forward.ml
-
-MKFORWARDOBJS = xml.cmo csc_pxp_reader.cmo configuration.cmo \
- clientHTTP.cmo cic.cmo deannotate.cmo \
- uriManager.cmo getter.cmo pxpUriResolver.ml \
- cicParser3.cmo cicParser2.cmo cicParser.cmo \
- cicSubstitution.cmo cicMiniReduction.cmo \
- mk_forward.cmo
+DEPOBJS = mk_forward.ml
+
+MKFORWARDOBJS = mk_forward.cmo
depend:
$(OCAMLDEP) $(DEPOBJS) > .depend
+++ /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 *)
-(* *)
-(* This module defines the internal representation of the objects (variables, *)
-(* blocks of (co)inductive definitions and constants) and the terms of cic *)
-(* *)
-(******************************************************************************)
-
-(* STUFF TO MANAGE IDENTIFIERS *)
-type id = string (* the abstract type of the (annotated) node identifiers *)
-type anntarget =
- Object of annobj
- | Term of annterm
-
-(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
-and sort =
- Prop
- | Set
- | Type
-and name =
- Name of string
- | Anonimous
-and term =
- Rel of int (* DeBrujin index *)
- | Var of UriManager.uri (* uri *)
- | Meta of int (* numeric id *)
- | Sort of sort (* sort *)
- | Implicit (* *)
- | Cast of term * term (* value, type *)
- | Prod of name * term * term (* binder, source, target *)
- | Lambda of name * term * term (* binder, source, target *)
- | LetIn of name * term * term (* binder, term, target *)
- | Appl of term list (* arguments *)
- | Const of UriManager.uri * int (* uri, number of cookings*)
- | Abst of UriManager.uri (* uri *)
- | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*)
- | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
- int * int (* typeno, consno *)
- (*CSC: serve cookingsno?*)
- | MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *)
- int * (* ind. typeno, *)
- term * term * (* outtype, ind. term *)
- term list (* patterns *)
- | Fix of int * inductiveFun list (* funno, functions *)
- | CoFix of int * coInductiveFun list (* funno, functions *)
-and obj =
- Definition of string * term * term * (* id, value, type, *)
- (int * UriManager.uri list) list (* parameters *)
- | Axiom of string * term *
- (int * UriManager.uri list) list (* id, type, parameters *)
- | Variable of string * term option * term (* name, body, type *)
- | CurrentProof of string * (int * term) list * (* name, conjectures, *)
- term * term (* value, type *)
- | InductiveDefinition of inductiveType list * (* inductive types, *)
- (int * UriManager.uri list) list * int (* parameters, n ind. pars *)
-and inductiveType =
- string * bool * term * (* typename, inductive, arity *)
- constructor list (* constructors *)
-and constructor =
- string * term * bool list option ref (* id, type, really recursive *)
-and inductiveFun =
- string * int * term * term (* name, ind. index, type, body *)
-and coInductiveFun =
- string * term * term (* name, type, body *)
-
-and annterm =
- ARel of id * annotation option ref *
- int * string option (* DeBrujin index, binder *)
- | AVar of id * annotation option ref *
- UriManager.uri (* uri *)
- | AMeta of id * annotation option ref * int (* numeric id *)
- | ASort of id * annotation option ref * sort (* sort *)
- | AImplicit of id * annotation option ref (* *)
- | ACast of id * annotation option ref *
- annterm * annterm (* value, type *)
- | AProd of id * annotation option ref *
- name * annterm * annterm (* binder, source, target *)
- | ALambda of id * annotation option ref *
- name * annterm * annterm (* binder, source, target *)
- | ALetIn of id * annotation option ref *
- name * annterm * annterm (* binder, term, target *)
- | AAppl of id * annotation option ref *
- annterm list (* arguments *)
- | AConst of id * annotation option ref *
- UriManager.uri * int (* uri, number of cookings*)
- | AAbst of id * annotation option ref *
- UriManager.uri (* uri *)
- | AMutInd of id * annotation option ref *
- UriManager.uri * int * int (* uri, cookingsno, typeno*)
- | AMutConstruct of id * annotation option ref *
- UriManager.uri * int * (* uri, cookingsno, *)
- int * int (* typeno, consno *)
- (*CSC: serve cookingsno?*)
- | AMutCase of id * annotation option ref *
- UriManager.uri * int * (* ind. uri, cookingsno *)
- int * (* ind. typeno, *)
- annterm * annterm * (* outtype, ind. term *)
- annterm list (* patterns *)
- | AFix of id * annotation option ref *
- int * anninductiveFun list (* funno, functions *)
- | ACoFix of id * annotation option ref *
- int * anncoInductiveFun list (* funno, functions *)
-and annobj =
- ADefinition of id * annotation option ref *
- string * (* id, *)
- annterm * annterm * (* value, type, *)
- (int * UriManager.uri list) list exactness (* parameters *)
- | AAxiom of id * annotation option ref *
- string * annterm * (* id, type *)
- (int * UriManager.uri list) list (* parameters *)
- | AVariable of id * annotation option ref *
- string * annterm option * annterm (* name, body, type *)
- | ACurrentProof of id * annotation option ref *
- string * (int * annterm) list * (* name, conjectures, *)
- annterm * annterm (* value, type *)
- | AInductiveDefinition of id *
- annotation option ref * anninductiveType list * (* inductive types , *)
- (int * UriManager.uri list) list * int (* parameters,n ind. pars*)
-and anninductiveType =
- string * bool * annterm * (* typename, inductive, arity *)
- annconstructor list (* constructors *)
-and annconstructor =
- string * annterm * bool list option ref (* id, type, really recursive *)
-and anninductiveFun =
- string * int * annterm * annterm (* name, ind. index, type, body *)
-and anncoInductiveFun =
- string * annterm * annterm (* name, type, body *)
-and annotation =
- string
-and 'a exactness =
- Possible of 'a (* an approximation to something *)
- | Actual of 'a (* something *)
-;;
+++ /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 rec letin_nf =
- let module C = Cic in
- function
- C.Rel _ as t -> t
- | C.Var _ as t -> t
- | C.Meta _ as t -> t
- | C.Sort _ as t -> t
- | C.Implicit as t -> t
- | C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty)
- | C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t)
- | C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t)
- | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t
- | C.Appl l -> C.Appl (List.map letin_nf l)
- | C.Const _ as t -> t
- | C.Abst _ as t -> t
- | C.MutInd _ as t -> t
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,letin_nf outt, letin_nf t,
- List.map letin_nf pl)
- | C.Fix (i,fl) ->
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) -> (name, i, letin_nf ty, letin_nf bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name, letin_nf ty, letin_nf bo))
- fl
- in
- C.CoFix (i, substitutedfl)
-;;
+++ /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 letin_nf : Cic.term -> Cic.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/.
- *)
-
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 24/01/2000 *)
-(* *)
-(* This is the main (top level) module of a parser for cic objects from xml *)
-(* files to the internal representation. It uses the modules cicParser2 *)
-(* (objects level) and cicParser3 (terms level) *)
-(* *)
-(******************************************************************************)
-
-exception Warnings;;
-
-class warner =
- object
- method warn w =
- print_endline ("WARNING: " ^ w) ;
- (raise Warnings : unit)
- end
-;;
-
-exception EmptyUri;;
-
-(* given an uri u it returns the list of tokens of the base uri of u *)
-(* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"] *)
-let tokens_of_uri uri =
- let uri' = UriManager.string_of_uri uri in
- let rec chop_list =
- function
- [] -> raise EmptyUri
- | he::[fn] -> [he]
- | he::tl -> he::(chop_list tl)
- in
- let trimmed_uri = Str.replace_first (Str.regexp "cic:") "" uri' in
- let list_of_tokens = Str.split (Str.regexp "/") trimmed_uri in
- chop_list list_of_tokens
-;;
-
-(* given the filename of an xml file of a cic object it returns its internal *)
-(* representation. process_annotations is true if the annotations do really *)
-(* matter *)
-let term_of_xml filename uri process_annotations =
- let module Y = Pxp_yacc in
- try
- let d =
- (* sets the current base uri to resolve relative URIs *)
- CicParser3.current_sp := tokens_of_uri uri ;
- CicParser3.current_uri := uri ;
- CicParser3.process_annotations := process_annotations ;
- CicParser3.ids_to_targets :=
- if process_annotations then Some (Hashtbl.create 500) else None ;
- let config = {Y.default_config with Y.warner = new warner} in
- Y.parse_document_entity config
-(*PXP (Y.ExtID (Pxp_types.System filename,
- new Pxp_reader.resolve_as_file ~url_of_id ()))
-*) (PxpUriResolver.from_file filename)
- CicParser3.domspec
- in
- let ids_to_targets = !CicParser3.ids_to_targets in
- let res = (CicParser2.get_term d#root, ids_to_targets) in
- CicParser3.ids_to_targets := None ; (* let's help the GC *)
- res
- with
- e ->
- print_endline ("Filename: " ^ filename ^ "\nException: ") ;
- 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> *)
-(* 22/03/2000 *)
-(* *)
-(* This is the main (top level) module of a parser for cic objects from xml *)
-(* files to the internal representation. It uses the modules cicParser2 *)
-(* (objects level) and cicParser3 (terms level) *)
-(* *)
-(******************************************************************************)
-
-(* given the filename of an xml file of a cic object and it's uri, it returns *)
-(* its internal annotated representation. The boolean is set to true if the *)
-(* annotations do really matter *)
-val term_of_xml :
- string -> UriManager.uri -> bool ->
- Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t option
+++ /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> *)
-(* 24/01/2000 *)
-(* *)
-(* This module is the objects level of a parser for cic objects from xml *)
-(* files to the internal representation. It uses the module cicParser3 *)
-(* cicParser3 (terms level) and it is used only through cicParser2 (top *)
-(* level). *)
-(* *)
-(******************************************************************************)
-
-exception IllFormedXml of int;;
-exception NotImplemented;;
-
-(* Utility functions that transform a Pxp attribute into something useful *)
-
-(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...." *)
-(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
-let mk_absolute_uris s =
- let l = (Str.split (Str.regexp ":") s) in
- let absolute_of_relative n v =
- let module P3 = CicParser3 in
- let rec mkburi =
- function
- (0,_) -> "/"
- | (n,he::tl) when n > 0 ->
- "/" ^ he ^ mkburi (n - 1, tl)
- | _ -> raise (IllFormedXml 12)
- in
- let m = List.length !P3.current_sp - (int_of_string n) in
- let buri = mkburi (m, !P3.current_sp) in
- UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
- in
- let rec absolutize =
- function
- [] -> []
- | [no ; vs] ->
- let vars = (Str.split (Str.regexp " ") vs) in
- [(int_of_string no, List.map (absolute_of_relative no) vars)]
- | no::vs::tl ->
- let vars = (Str.split (Str.regexp " ") vs) in
- let rec add_prefix =
- function
- [no2] -> ([], no2)
- | he::tl ->
- let (pvars, no2) = add_prefix tl in
- ((absolute_of_relative no he)::pvars, no2)
- | _ -> raise (IllFormedXml 11)
- in
- let (pvars, no2) = add_prefix vars in
- (int_of_string no, pvars)::(absolutize (no2::tl))
- | _ -> raise (IllFormedXml 10)
- in
- (* last parameter must be applied first *)
- absolutize l
-;;
-
-let option_uri_list_of_attr a1 a2 =
- let module T = Pxp_types in
- let parameters =
- match a1 with
- T.Value s -> mk_absolute_uris s
- | _ -> raise (IllFormedXml 0)
- in
- match a2 with
- T.Value "POSSIBLE" -> Cic.Possible parameters
- | T.Implied_value -> Cic.Actual parameters
- | _ -> raise (IllFormedXml 0)
-;;
-
-let uri_list_of_attr a =
- let module T = Pxp_types in
- match a with
- T.Value s -> mk_absolute_uris s
- | _ -> raise (IllFormedXml 0)
-;;
-
-let string_of_attr a =
- let module T = Pxp_types in
- match a with
- T.Value s -> s
- | _ -> raise (IllFormedXml 0)
-;;
-
-let int_of_attr a =
- int_of_string (string_of_attr a)
-;;
-
-let bool_of_attr a =
- bool_of_string (string_of_attr a)
-;;
-
-(* Other utility functions *)
-
-let get_content n =
- match n#sub_nodes with
- [ t ] -> t
- | _ -> raise (IllFormedXml 1)
-;;
-
-let register_id id node =
- if !CicParser3.process_annotations then
- match !CicParser3.ids_to_targets with
- None -> assert false
- | Some ids_to_targets ->
- Hashtbl.add ids_to_targets id (Cic.Object node)
-;;
-
-(* Functions that, given the list of sons of a node of the cic dom (objects *)
-(* level), retrieve the internal representation associated to the node. *)
-(* Everytime a cic term subtree is found, it is translated to the internal *)
-(* representation using the method to_cic_term defined in cicParser3. *)
-(* Each function raise IllFormedXml if something goes wrong, but this should *)
-(* be impossible due to the presence of the dtd *)
-(* The functions should really be obvious looking at their name and the cic *)
-(* dtd *)
-
-(* called when a CurrentProof is found *)
-let get_conjs_value_type l =
- let rec rget (c, v, t) l =
- let module D = Pxp_document in
- match l with
- [] -> (c, v, t)
- | conj::tl when conj#node_type = D.T_element "Conjecture" ->
- let no = int_of_attr (conj#attribute "no")
- and typ = (get_content conj)#extension#to_cic_term in
- rget ((no, typ)::c, v, t) tl
- | value::tl when value#node_type = D.T_element "body" ->
- let v' = (get_content value)#extension#to_cic_term in
- (match v with
- None -> rget (c, Some v', t) tl
- | _ -> raise (IllFormedXml 2)
- )
- | typ::tl when typ#node_type = D.T_element "type" ->
- let t' = (get_content typ)#extension#to_cic_term in
- (match t with
- None -> rget (c, v, Some t') tl
- | _ -> raise (IllFormedXml 3)
- )
- | _ -> raise (IllFormedXml 4)
- in
- match rget ([], None, None) l with
- (c, Some v, Some t) -> (c, v, t)
- | _ -> raise (IllFormedXml 5)
-;;
-
-(* used only by get_inductive_types; called one time for each inductive *)
-(* definitions in a block of inductive definitions *)
-let get_names_arity_constructors l =
- let rec rget (a,c) l =
- let module D = Pxp_document in
- match l with
- [] -> (a, c)
- | arity::tl when arity#node_type = D.T_element "arity" ->
- let a' = (get_content arity)#extension#to_cic_term in
- rget (Some a',c) tl
- | con::tl when con#node_type = D.T_element "Constructor" ->
- let id = string_of_attr (con#attribute "name")
- and ty = (get_content con)#extension#to_cic_term in
- rget (a,(id,ty,ref None)::c) tl
- | _ -> raise (IllFormedXml 9)
- in
- match rget (None,[]) l with
- (Some a, c) -> (a, List.rev c)
- | _ -> raise (IllFormedXml 8)
-;;
-
-(* called when an InductiveDefinition is found *)
-let rec get_inductive_types =
- function
- [] -> []
- | he::tl ->
- let tyname = string_of_attr (he#attribute "name")
- and inductive = bool_of_attr (he#attribute "inductive")
- and (arity,cons) =
- get_names_arity_constructors (he#sub_nodes)
- in
- (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
-;;
-
-(* This is the main function and also the only one used directly from *)
-(* cicParser. Given the root of the dom tree, it returns the internal *)
-(* representation of the cic object described in the tree *)
-(* It uses the previous functions and the to_cic_term method defined *)
-(* in cicParser3 (used for subtrees that encode cic terms) *)
-let rec get_term n =
- let module D = Pxp_document in
- let module C = Cic in
- let ntype = n # node_type in
- match ntype with
- D.T_element "Definition" ->
- let id = string_of_attr (n # attribute "name")
- and params =
- option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
- and (value, typ) =
- let sons = n#sub_nodes in
- match sons with
- [v ; t] when
- v#node_type = D.T_element "body" &&
- t#node_type = D.T_element "type" ->
- let v' = get_content v
- and t' = get_content t in
- (v'#extension#to_cic_term, t'#extension#to_cic_term)
- | _ -> raise (IllFormedXml 6)
- and xid = string_of_attr (n#attribute "id") in
- let res = C.ADefinition (xid, ref None, id, value, typ, params) in
- register_id xid res ;
- res
- | D.T_element "Axiom" ->
- let id = string_of_attr (n # attribute "name")
- and params = uri_list_of_attr (n # attribute "params")
- and typ =
- (get_content (get_content n))#extension#to_cic_term
- and xid = string_of_attr (n#attribute "id") in
- let res = C.AAxiom (xid, ref None, id, typ, params) in
- register_id xid res ;
- res
- | D.T_element "CurrentProof" ->
- let name = string_of_attr (n#attribute "name")
- and xid = string_of_attr (n#attribute "id") in
- let sons = n#sub_nodes in
- let (conjs, value, typ) = get_conjs_value_type sons in
- let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
- register_id xid res ;
- res
- | D.T_element "InductiveDefinition" ->
- let sons = n#sub_nodes
- and xid = string_of_attr (n#attribute "id") in
- let inductiveTypes = get_inductive_types sons
- and params = uri_list_of_attr (n#attribute "params")
- and nparams = int_of_attr (n#attribute "noParams") in
- let res =
- C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
- in
- register_id xid res ;
- res
- | D.T_element "Variable" ->
- let name = string_of_attr (n#attribute "name")
- and xid = string_of_attr (n#attribute "id")
- and (body, typ) =
- let sons = n#sub_nodes in
- match sons with
- [b ; t] when
- b#node_type = D.T_element "body" &&
- t#node_type = D.T_element "type" ->
- let b' = get_content b
- and t' = get_content t in
- (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
- | [t] when t#node_type = D.T_element "type" ->
- let t' = get_content t in
- (None, t'#extension#to_cic_term)
- | _ -> raise (IllFormedXml 6)
- in
- let res = C.AVariable (xid,ref None,name,body,typ) in
- register_id xid res ;
- res
- | D.T_element _
- | D.T_data
- | _ ->
- raise (IllFormedXml 7)
-;;
+++ /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> *)
-(* 24/01/2000 *)
-(* *)
-(* This module is the objects level of a parser for cic objects from xml *)
-(* files to the internal representation. It uses the module cicParser3 *)
-(* cicParser3 (terms level) and it is used only through cicParser2 (top *)
-(* level). *)
-(* *)
-(******************************************************************************)
-
-exception IllFormedXml of int
-exception NotImplemented
-
-(* This is the main function and also the only one used directly from *)
-(* cicParser. Given the root of the dom tree, it returns the internal *)
-(* representation of the cic object described in the tree *)
-(* It uses the previous functions and the to_cic_term method defined *)
-(* in cicParser3 (used for subtrees that encode cic terms) *)
-val get_term :
- < attribute : string -> Pxp_types.att_value;
- node_type : Pxp_document.node_type;
- sub_nodes : < attribute : string -> Pxp_types.att_value;
- node_type : Pxp_document.node_type;
- sub_nodes : CicParser3.cic_term Pxp_document.node list;
- .. >
- list;
- .. > ->
- Cic.annobj
+++ /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> *)
-(* 24/01/2000 *)
-(* *)
-(* This module is the terms level of a parser for cic objects from xml *)
-(* files to the internal representation. It is used by the module cicParser2 *)
-(* (objects level). It defines an extension of the standard dom using the *)
-(* object-oriented extension machinery of markup: an object with a method *)
-(* to_cic_term that returns the internal representation of the subtree is *)
-(* added to each node of the dom tree *)
-(* *)
-(******************************************************************************)
-
-exception IllFormedXml of int;;
-
-(* The hashtable from the current identifiers to the object or the terms *)
-let ids_to_targets = ref None;;
-
-(* The list of tokens of the current section path. *)
-(* Used to resolve relative URIs *)
-let current_sp = ref [];;
-
-(* The uri of the object been parsed *)
-let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
-
-(* True if annotation really matter *)
-let process_annotations = ref false;;
-
-(* Utility functions to map a markup attribute to something useful *)
-
-let cic_attr_of_xml_attr =
- function
- Pxp_types.Value s -> Cic.Name s
- | Pxp_types.Implied_value -> Cic.Anonimous
- | _ -> raise (IllFormedXml 1)
-
-let cic_sort_of_xml_attr =
- function
- Pxp_types.Value "Prop" -> Cic.Prop
- | Pxp_types.Value "Set" -> Cic.Set
- | Pxp_types.Value "Type" -> Cic.Type
- | _ -> raise (IllFormedXml 2)
-
-let int_of_xml_attr =
- function
- Pxp_types.Value n -> int_of_string n
- | _ -> raise (IllFormedXml 3)
-
-let uri_of_xml_attr =
- function
- Pxp_types.Value s -> UriManager.uri_of_string s
- | _ -> raise (IllFormedXml 4)
-
-let string_of_xml_attr =
- function
- Pxp_types.Value s -> s
- | _ -> raise (IllFormedXml 5)
-
-let binder_of_xml_attr =
- function
- Pxp_types.Value s -> if !process_annotations then Some s else None
- | _ -> raise (IllFormedXml 17)
-;;
-
-let register_id id node =
- if !process_annotations then
- match !ids_to_targets with
- None -> assert false
- | Some ids_to_targets ->
- Hashtbl.add ids_to_targets id (Cic.Term node)
-;;
-
-(* the "interface" of the class linked to each node of the dom tree *)
-
-class virtual cic_term =
- object (self)
-
- (* fields and methods ever required by markup *)
- val mutable node = (None : cic_term Pxp_document.node option)
-
- method clone = {< >}
- method node =
- match node with
- None ->
- assert false
- | Some n -> n
- method set_node n =
- node <- Some n
-
- (* a method that returns the internal representation of the tree (term) *)
- (* rooted in this node *)
- method virtual to_cic_term : Cic.annterm
- end
-;;
-
-(* the class of the objects linked to nodes that are not roots of cic terms *)
-class eltype_not_of_cic =
- object (self)
-
- inherit cic_term
-
- method to_cic_term = raise (IllFormedXml 6)
- end
-;;
-
-(* the class of the objects linked to nodes whose content is a cic term *)
-(* (syntactic sugar xml entities) e.g. <type> ... </type> *)
-class eltype_transparent =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- match n#sub_nodes with
- [ t ] -> t#extension#to_cic_term
- | _ -> raise (IllFormedXml 7)
- end
-;;
-
-(* A class for each cic node type *)
-
-class eltype_fix =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let nofun = int_of_xml_attr (n#attribute "noFun")
- and id = string_of_xml_attr (n#attribute "id")
- and functions =
- let sons = n#sub_nodes in
- List.map
- (function
- f when f#node_type = Pxp_document.T_element "FixFunction" ->
- let name = string_of_xml_attr (f#attribute "name")
- and recindex = int_of_xml_attr (f#attribute "recIndex")
- and (ty, body) =
- match f#sub_nodes with
- [t ; b] when
- t#node_type = Pxp_document.T_element "type" &&
- b#node_type = Pxp_document.T_element "body" ->
- (t#extension#to_cic_term, b#extension#to_cic_term)
- | _ -> raise (IllFormedXml 14)
- in
- (name, recindex, ty, body)
- | _ -> raise (IllFormedXml 13)
- ) sons
- in
- let res = Cic.AFix (id, ref None, nofun, functions) in
- register_id id res ;
- res
- end
-;;
-
-class eltype_cofix =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let nofun = int_of_xml_attr (n#attribute "noFun")
- and id = string_of_xml_attr (n#attribute "id")
- and functions =
- let sons = n#sub_nodes in
- List.map
- (function
- f when f#node_type = Pxp_document.T_element "CofixFunction" ->
- let name = string_of_xml_attr (f#attribute "name")
- and (ty, body) =
- match f#sub_nodes with
- [t ; b] when
- t#node_type = Pxp_document.T_element "type" &&
- b#node_type = Pxp_document.T_element "body" ->
- (t#extension#to_cic_term, b#extension#to_cic_term)
- | _ -> raise (IllFormedXml 16)
- in
- (name, ty, body)
- | _ -> raise (IllFormedXml 15)
- ) sons
- in
- let res = Cic.ACoFix (id, ref None, nofun, functions) in
- register_id id res ;
- res
- end
-;;
-
-class eltype_implicit =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AImplicit (id, ref None) in
- register_id id res ;
- res
- end
-;;
-
-class eltype_rel =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let value = int_of_xml_attr (n#attribute "value")
- and binder = binder_of_xml_attr (n#attribute "binder")
- and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.ARel (id,ref None,value,binder) in
- register_id id res ;
- res
- end
-;;
-
-class eltype_meta =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let value = int_of_xml_attr (n#attribute "no")
- and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AMeta (id,ref None,value) in
- register_id id res ;
- res
- end
-;;
-
-class eltype_var =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let name = string_of_xml_attr (n#attribute "relUri")
- and xid = string_of_xml_attr (n#attribute "id") in
- match Str.split (Str.regexp ",") name with
- [index; id] ->
- let get_prefix n =
- let rec aux =
- function
- (0,_) -> "/"
- | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
- | _ -> raise (IllFormedXml 19)
- in
- aux (List.length !current_sp - n,!current_sp)
- in
- let res =
- Cic.AVar
- (xid,ref None,
- (UriManager.uri_of_string
- ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
- )
- in
- register_id id res ;
- res
- | _ -> raise (IllFormedXml 18)
- end
-;;
-
-class eltype_apply =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let children = n#sub_nodes
- and id = string_of_xml_attr (n#attribute "id") in
- if List.length children < 2 then raise (IllFormedXml 8)
- else
- let res =
- Cic.AAppl
- (id,ref None,List.map (fun x -> x#extension#to_cic_term) children)
- in
- register_id id res ;
- res
- end
-;;
-
-class eltype_cast =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let sons = n#sub_nodes
- and id = string_of_xml_attr (n#attribute "id") in
- match sons with
- [te ; ty] when
- te#node_type = Pxp_document.T_element "term" &&
- ty#node_type = Pxp_document.T_element "type" ->
- let term = te#extension#to_cic_term
- and typ = ty#extension#to_cic_term in
- let res = Cic.ACast (id,ref None,term,typ) in
- register_id id res ;
- res
- | _ -> raise (IllFormedXml 9)
- end
-;;
-
-class eltype_sort =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let sort = cic_sort_of_xml_attr (n#attribute "value")
- and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.ASort (id,ref None,sort) in
- register_id id res ;
- res
- end
-;;
-
-class eltype_abst =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let value = uri_of_xml_attr (n#attribute "uri")
- and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AAbst (id,ref None,value) in
- register_id id res ;
- res
- end
-;;
-
-class eltype_const =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let module U = UriManager in
- let n = self#node in
- let value = uri_of_xml_attr (n#attribute "uri")
- and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0)
- in
- register_id id res ;
- res
- end
-;;
-
-class eltype_mutind =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let module U = UriManager in
- let n = self#node in
- let name = uri_of_xml_attr (n#attribute "uri")
- and noType = int_of_xml_attr (n#attribute "noType")
- and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AMutInd
- (id,ref None,name, U.relative_depth !current_uri name 0, noType)
- in
- register_id id res ;
- res
- end
-;;
-
-class eltype_mutconstruct =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let module U = UriManager in
- let n = self#node in
- let name = uri_of_xml_attr (n#attribute "uri")
- and noType = int_of_xml_attr (n#attribute "noType")
- and noConstr = int_of_xml_attr (n#attribute "noConstr")
- and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AMutConstruct
- (id, ref None, name, U.relative_depth !current_uri name 0,
- noType, noConstr)
- in
- register_id id res ;
- res
- end
-;;
-
-class eltype_prod =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let sons = n#sub_nodes
- and id = string_of_xml_attr (n#attribute "id") in
- match sons with
- [s ; t] when
- s#node_type = Pxp_document.T_element "source" &&
- t#node_type = Pxp_document.T_element "target" ->
- let name = cic_attr_of_xml_attr (t#attribute "binder")
- and source = s#extension#to_cic_term
- and target = t#extension#to_cic_term in
- let res = Cic.AProd (id,ref None,name,source,target) in
- register_id id res ;
- res
- | _ -> raise (IllFormedXml 10)
- end
-;;
-
-class eltype_mutcase =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let module U = UriManager in
- let n = self#node in
- let sons = n#sub_nodes
- and id = string_of_xml_attr (n#attribute "id") in
- match sons with
- ty::te::patterns when
- ty#node_type = Pxp_document.T_element "patternsType" &&
- te#node_type = Pxp_document.T_element "inductiveTerm" ->
- let ci = uri_of_xml_attr (n#attribute "uriType")
- and typeno = int_of_xml_attr (n#attribute "noType")
- and inductiveType = ty#extension#to_cic_term
- and inductiveTerm = te#extension#to_cic_term
- and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
- in
- let res =
- Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0,
- typeno,inductiveType,inductiveTerm,lpattern)
- in
- register_id id res ;
- res
- | _ -> raise (IllFormedXml 11)
- end
-;;
-
-class eltype_lambda =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let sons = n#sub_nodes
- and id = string_of_xml_attr (n#attribute "id") in
- match sons with
- [s ; t] when
- s#node_type = Pxp_document.T_element "source" &&
- t#node_type = Pxp_document.T_element "target" ->
- let name = cic_attr_of_xml_attr (t#attribute "binder")
- and source = s#extension#to_cic_term
- and target = t#extension#to_cic_term in
- let res = Cic.ALambda (id,ref None,name,source,target) in
- register_id id res ;
- res
- | _ -> raise (IllFormedXml 12)
- end
-;;
-
-class eltype_letin =
- object (self)
-
- inherit cic_term
-
- method to_cic_term =
- let n = self#node in
- let sons = n#sub_nodes
- and id = string_of_xml_attr (n#attribute "id") in
- match sons with
- [s ; t] when
- s#node_type = Pxp_document.T_element "term" &&
- t#node_type = Pxp_document.T_element "letintarget" ->
- let name = cic_attr_of_xml_attr (t#attribute "binder")
- and source = s#extension#to_cic_term
- and target = t#extension#to_cic_term in
- let res = Cic.ALetIn (id,ref None,name,source,target) in
- register_id id res ;
- res
- | _ -> raise (IllFormedXml 12)
- end
-;;
-
-(* The definition of domspec, an hashtable that maps each node type to the *)
-(* object that must be linked to it. Used by markup. *)
-
-let domspec =
- let module D = Pxp_document in
- D.make_spec_from_alist
- ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
- ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
- ~element_alist:
- [ "REL", (new D.element_impl (new eltype_rel)) ;
- "VAR", (new D.element_impl (new eltype_var)) ;
- "META", (new D.element_impl (new eltype_meta)) ;
- "SORT", (new D.element_impl (new eltype_sort)) ;
- "IMPLICIT", (new D.element_impl (new eltype_implicit)) ;
- "CAST", (new D.element_impl (new eltype_cast)) ;
- "PROD", (new D.element_impl (new eltype_prod)) ;
- "LAMBDA", (new D.element_impl (new eltype_lambda)) ;
- "LETIN", (new D.element_impl (new eltype_letin)) ;
- "APPLY", (new D.element_impl (new eltype_apply)) ;
- "CONST", (new D.element_impl (new eltype_const)) ;
- "ABST", (new D.element_impl (new eltype_abst)) ;
- "MUTIND", (new D.element_impl (new eltype_mutind)) ;
- "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ;
- "MUTCASE", (new D.element_impl (new eltype_mutcase)) ;
- "FIX", (new D.element_impl (new eltype_fix)) ;
- "COFIX", (new D.element_impl (new eltype_cofix)) ;
- "arity", (new D.element_impl (new eltype_transparent)) ;
- "term", (new D.element_impl (new eltype_transparent)) ;
- "type", (new D.element_impl (new eltype_transparent)) ;
- "body", (new D.element_impl (new eltype_transparent)) ;
- "source", (new D.element_impl (new eltype_transparent)) ;
- "target", (new D.element_impl (new eltype_transparent)) ;
- "letintarget", (new D.element_impl (new eltype_transparent)) ;
- "patternsType", (new D.element_impl (new eltype_transparent)) ;
- "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
- "pattern", (new D.element_impl (new eltype_transparent))
- ]
- ()
-;;
+++ /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> *)
-(* 24/01/2000 *)
-(* *)
-(* This module is the terms level of a parser for cic objects from xml *)
-(* files to the internal representation. It is used by the module cicParser2 *)
-(* (objects level). It defines an extension of the standard dom using the *)
-(* object-oriented extension machinery of markup: an object with a method *)
-(* to_cic_term that returns the internal representation of the subtree is *)
-(* added to each node of the dom tree *)
-(* *)
-(******************************************************************************)
-
-exception IllFormedXml of int
-
-val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref
-val current_sp : string list ref
-val current_uri : UriManager.uri ref
-val process_annotations : bool ref
-
-(* the "interface" of the class linked to each node of the dom tree *)
-class virtual cic_term :
- object ('a)
-
- (* fields and methods ever required by markup *)
- val mutable node : cic_term Pxp_document.node option
- method clone : 'a
- method node : cic_term Pxp_document.node
- method set_node : cic_term Pxp_document.node -> unit
-
- (* a method that returns the internal representation of the tree (term) *)
- (* rooted in this node *)
- method virtual to_cic_term : Cic.annterm
-
- end
-
-(* The definition of domspec, an hashtable that maps each node type to the *)
-(* object that must be linked to it. Used by markup. *)
-val domspec : cic_term Pxp_document.spec
+++ /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 lift n =
- let rec liftaux k =
- let module C = Cic in
- function
- C.Rel m ->
- if m < k then
- C.Rel m
- else
- C.Rel (m + n)
- | C.Var _ as t -> t
- | C.Meta _ as t -> t
- | C.Sort _ as t -> t
- | C.Implicit as t -> t
- | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
- | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
- | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
- | C.Appl l -> C.Appl (List.map (liftaux k) l)
- | C.Const _ as t -> t
- | C.Abst _ as t -> t
- | C.MutInd _ as t -> t
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
- C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t,
- List.map (liftaux k) pl)
- | C.Fix (i, fl) ->
- let len = List.length fl in
- let liftedfl =
- List.map
- (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
- fl
- in
- C.Fix (i, liftedfl)
- | C.CoFix (i, fl) ->
- let len = List.length fl in
- let liftedfl =
- List.map
- (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
- fl
- in
- C.CoFix (i, liftedfl)
- in
- liftaux 1
-;;
-
-let subst arg =
- let rec substaux k =
- let module C = Cic in
- function
- C.Rel n as t ->
- (match n with
- n when n = k -> lift (k - 1) arg
- | n when n < k -> t
- | _ -> C.Rel (n - 1)
- )
- | C.Var _ as t -> t
- | C.Meta _ as t -> t
- | C.Sort _ as t -> t
- | C.Implicit as t -> t
- | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) (*CSC ??? *)
- | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
- | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
- | C.Appl l -> C.Appl (List.map (substaux k) l)
- | C.Const _ as t -> t
- | C.Abst _ as t -> t
- | C.MutInd _ as t -> t
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
- List.map (substaux k) pl)
- | C.Fix (i,fl) ->
- let len = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let len = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
- fl
- in
- C.CoFix (i, substitutedfl)
- in
- substaux 1
-;;
-
-let undebrujin_inductive_def uri =
- function
- Cic.InductiveDefinition (dl,params,n_ind_params) ->
- let dl' =
- List.map
- (fun (name,inductive,arity,constructors) ->
- let constructors' =
- List.map
- (fun (name,ty,r) ->
- let ty' =
- let counter = ref (List.length dl) in
- List.fold_right
- (fun _ ->
- decr counter ;
- subst (Cic.MutInd (uri,0,!counter))
- ) dl ty
- in
- (name,ty',r)
- ) constructors
- in
- (name,inductive,arity,constructors')
- ) dl
- in
- Cic.InductiveDefinition (dl', params, n_ind_params)
- | obj -> obj
-;;
+++ /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 lift : int -> Cic.term -> Cic.term
-val subst : Cic.term -> Cic.term -> Cic.term
-val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj
+++ /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 HttpClientError of exn * string;;
-
-let send cmd =
- try
- ignore (Http_client.Convenience.http_get cmd)
- with
- e -> raise (HttpClientError (e,cmd))
-;;
-
-let get uri =
- try
- Http_client.Convenience.http_get uri
- with
- e -> raise (HttpClientError (e,uri))
-;;
-
-let get_and_save uri dest_filename =
- let reply = get uri
- and out_channel = open_out dest_filename in
- output_string out_channel reply ;
- close_out out_channel
-;;
-
-let get_and_save_to_tmp uri =
- let flat_string s s' c =
- let cs = String.copy s in
- for i = 0 to (String.length s) - 1 do
- if String.contains s' s.[i] then cs.[i] <- c
- done ;
- cs
- in
- let tmp_file = Configuration.tmp_dir ^ "/" ^ (flat_string uri ".-=:;!?/&" '_') in
- get_and_save uri tmp_file ;
- tmp_file
-;;
+++ /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 HttpClientError of exn * string;;
-val send : string -> unit
-val get : string -> string
-val get_and_save : string -> string -> unit
-val get_and_save_to_tmp : string -> string
+++ /dev/null
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 28/12/2000 *)
-(* *)
-(* This is the parser that reads the configuration file of helm *)
-(* *)
-(******************************************************************************)
-
-exception MalformedDir of string
-
-(* this should be the only hard coded constant *)
-let filename =
- let prefix =
- try
- Sys.getenv "HELM_CONFIGURATION_DIR"
- with
- Not_found -> "@HELM_CONFIGURATION_DIR@"
- in
- if prefix.[(String.length prefix) - 1] = '/' then
- raise (MalformedDir prefix) ;
- prefix ^ "/configuration.xml";;
-
-exception Warnings;;
-
-class warner =
- object
- method warn w =
- print_endline ("WARNING: " ^ w) ;
- (raise Warnings : unit)
- end
-;;
-
-let xml_document () =
- let module Y = Pxp_yacc in
- try
- let config = {Y.default_config with Y.warner = new warner} in
- Y.parse_document_entity config (Y.from_file filename) Y.default_spec
- with
- e ->
- print_endline (Pxp_types.string_of_exn e) ;
- raise e
-;;
-
-exception Impossible;;
-
-let vars = Hashtbl.create 14;;
-
-(* resolve <value-of> tags and returns the string values of the variable tags *)
-let rec resolve =
- let module D = Pxp_document in
- function
- [] -> ""
- | he::tl when he#node_type = D.T_element "value-of" ->
- (match he#attribute "var" with
- Pxp_types.Value var -> Hashtbl.find vars var
- | _ -> raise Impossible
- ) ^ resolve tl
- | he::tl when he#node_type = D.T_data ->
- he#data ^ resolve tl
- | _ -> raise Impossible
-;;
-
-(* we trust the xml file to be valid because of the validating xml parser *)
-let _ =
- List.iter
- (function
- n ->
- match n#node_type with
- Pxp_document.T_element var ->
- Hashtbl.add vars var (resolve (n#sub_nodes))
- | _ -> raise Impossible
- )
- ((xml_document ())#root#sub_nodes)
-;;
-
-(* try to read a configuration variable, given its name into the
- * configuration.xml file and its name into the shell environment.
- * The shell variable, if present, has precedence over configuration.xml
- *)
-let read_configuration_var_env xml_name env_name =
- try
- try
- Sys.getenv env_name
- with
- Not_found -> Hashtbl.find vars xml_name
- with
- Not_found ->
- Printf.printf "Sorry, cannot find variable `%s', please check your configuration\n" xml_name ;
- flush stdout ;
- raise Not_found
-
-let read_configuration_var xml_name =
- try
- Hashtbl.find vars xml_name
- with
- Not_found ->
- Printf.printf "Sorry, cannot find variable `%s', please check your configuration\n" xml_name ;
- flush stdout ;
- raise Not_found
-
-let helm_dir = read_configuration_var "helm_dir";;
-let dtd_dir = read_configuration_var "dtd_dir";;
-let style_dir = read_configuration_var_env "style_dir" "HELM_STYLE_DIR";;
-let servers_file = read_configuration_var "servers_file";;
-let uris_dbm = read_configuration_var "uris_dbm";;
-let dest = read_configuration_var "dest";;
-let indexname = read_configuration_var "indexname";;
-let tmp_dir = read_configuration_var "tmp_dir"
-let helm_dir = read_configuration_var "helm_dir";;
-let getter_url = read_configuration_var_env "getter_url" "HELM_GETTER_URL";;
-let processor_url = read_configuration_var_env "processor_url" "HELM_PROCESSOR_URL";;
-let annotations_dir = read_configuration_var_env "annotations_dir" "HELM_ANNOTATIONS_DIR"
-let annotations_url = read_configuration_var_env "annotations_url" "HELM_ANNOTATIONS_URL"
-
-let _ = Hashtbl.clear vars;;
-
+++ /dev/null
-(* $Id$
- * ----------------------------------------------------------------------
- * PXP: The polymorphic XML parser for Objective Caml.
- * Copyright by Gerd Stolpmann. See LICENSE for details.
- *)
-
-open Pxp_types;;
-exception Not_competent;;
-exception Not_resolvable of exn;;
-
-class type resolver =
- object
- method init_rep_encoding : rep_encoding -> unit
- method init_warner : collect_warnings -> unit
- method rep_encoding : rep_encoding
- method open_in : ext_id -> Lexing.lexbuf
- method close_in : unit
- method close_all : unit
- method change_encoding : string -> unit
- method clone : resolver
- end
-;;
-
-
-class virtual resolve_general
- =
- object (self)
- val mutable internal_encoding = `Enc_utf8
-
- val mutable encoding = `Enc_utf8
- val mutable encoding_requested = false
-
- val mutable warner = new drop_warnings
-
- val mutable enc_initialized = false
- val mutable wrn_initialized = false
-
- val mutable clones = []
-
- method init_rep_encoding e =
- internal_encoding <- e;
- enc_initialized <- true;
-
- method init_warner w =
- warner <- w;
- wrn_initialized <- true;
-
- method rep_encoding = (internal_encoding :> rep_encoding)
-
-(*
- method clone =
- ( {< encoding = `Enc_utf8;
- encoding_requested = false;
- >}
- : # resolver :> resolver )
-*)
-
- method private warn (k:int) =
- (* Called if a character not representable has been found.
- * k is the character code.
- *)
- if k < 0xd800 or (k >= 0xe000 & k <= 0xfffd) or
- (k >= 0x10000 & k <= 0x10ffff) then begin
- warner # warn ("Code point cannot be represented: " ^ string_of_int k);
- end
- else
- raise (WF_error("Code point " ^ string_of_int k ^
- " outside the accepted range of code points"))
-
-
- method private autodetect s =
- (* s must be at least 4 bytes long. The slot 'encoding' is
- * set to:
- * "UTF-16-BE": UTF-16/UCS-2 encoding big endian
- * "UTF-16-LE": UTF-16/UCS-2 encoding little endian
- * "UTF-8": UTF-8 encoding
- *)
- if String.length s < 4 then
- encoding <- `Enc_utf8
- else if String.sub s 0 2 = "\254\255" then
- encoding <- `Enc_utf16
- (* Note: Netconversion.recode will detect the big endianess, too *)
- else if String.sub s 0 2 = "\255\254" then
- encoding <- `Enc_utf16
- (* Note: Netconversion.recode will detect the little endianess, too *)
- else
- encoding <- `Enc_utf8
-
-
- method private virtual next_string : string -> int -> int -> int
- method private virtual init_in : ext_id -> unit
- method virtual close_in : unit
-
- method close_all =
- List.iter (fun r -> r # close_in) clones
-
- method open_in xid =
- assert(enc_initialized && wrn_initialized);
-
- encoding <- `Enc_utf8;
- encoding_requested <- false;
- self # init_in xid; (* may raise Not_competent *)
- (* init_in: may already set 'encoding' *)
-
- let buffer_max = 512 in
- let buffer = String.make buffer_max ' ' in
- let buffer_len = ref 0 in
- let buffer_end = ref false in
- let fillup () =
- if not !buffer_end & !buffer_len < buffer_max then begin
- let l =
- self # next_string buffer !buffer_len (buffer_max - !buffer_len) in
- if l = 0 then
- buffer_end := true
- else begin
- buffer_len := !buffer_len + l
- end
- end
- in
- let consume n =
- let l = !buffer_len - n in
- String.blit buffer n buffer 0 l;
- buffer_len := l
- in
-
- fillup();
- if not encoding_requested then self # autodetect buffer;
-
- Lexing.from_function
- (fun s n ->
- (* TODO: if encoding = internal_encoding, it is possible to
- * avoid copying buffer to s because s can be directly used
- * as buffer.
- *)
-
- fillup();
- if !buffer_len = 0 then
- 0
- else begin
- let m_in = !buffer_len in
- let m_max = if encoding_requested then n else 1 in
- let n_in, n_out, encoding' =
- if encoding = (internal_encoding : rep_encoding :> encoding) &&
- encoding_requested
- then begin
- (* Special case encoding = internal_encoding *)
- String.blit buffer 0 s 0 m_in;
- m_in, m_in, encoding
- end
- else
- Netconversion.recode
- ~in_enc:encoding
- ~in_buf:buffer
- ~in_pos:0
- ~in_len:m_in
- ~out_enc:(internal_encoding : rep_encoding :> encoding)
- ~out_buf:s
- ~out_pos:0
- ~out_len:n
- ~max_chars:m_max
- ~subst:(fun k -> self # warn k; "")
- in
- if n_in = 0 then
- (* An incomplete character at the end of the stream: *)
- raise Netconversion.Malformed_code;
- (* failwith "Badly encoded character"; *)
- encoding <- encoding';
- consume n_in;
- assert(n_out <> 0);
- n_out
- end)
-
- method change_encoding enc =
- if not encoding_requested then begin
- if enc <> "" then begin
- match Netconversion.encoding_of_string enc with
- `Enc_utf16 ->
- (match encoding with
- (`Enc_utf16_le | `Enc_utf16_be) -> ()
- | `Enc_utf16 -> assert false
- | _ ->
- raise(WF_error "Encoding of data stream and encoding declaration mismatch")
- )
- | e ->
- encoding <- e
- end;
- (* else: the autodetected encoding counts *)
- encoding_requested <- true;
- end;
- end
-;;
-
-
-class resolve_read_any_channel ?(close=close_in) ~channel_of_id () =
- object (self)
- inherit resolve_general as super
-
- val f_open = channel_of_id
- val mutable current_channel = None
- val close = close
-
- method private init_in (id:ext_id) =
- if current_channel <> None then
- failwith "Pxp_reader.resolve_read_any_channel # init_in";
- let ch, enc_opt = f_open id in (* may raise Not_competent *)
- begin match enc_opt with
- None -> ()
- | Some enc -> encoding <- enc; encoding_requested <- true
- end;
- current_channel <- Some ch;
-
- method private next_string s ofs len =
- match current_channel with
- None -> failwith "Pxp_reader.resolve_read_any_channel # next_string"
- | Some ch ->
- input ch s ofs len
-
- method close_in =
- match current_channel with
- None -> ()
- | Some ch ->
- close ch;
- current_channel <- None
-
- method clone =
- let c = new resolve_read_any_channel
- ?close:(Some close) f_open () in
- c # init_rep_encoding internal_encoding;
- c # init_warner warner;
- clones <- c :: clones;
- (c :> resolver)
-
- end
-;;
-
-
-class resolve_read_this_channel1 is_stale ?id ?fixenc ?close ch =
-
- let getchannel = ref (fun xid -> assert false) in
-
- object (self)
- inherit resolve_read_any_channel
- ?close
- (fun xid -> !getchannel xid)
- ()
- as super
-
- val mutable is_stale = is_stale
- (* The channel can only be read once. To avoid that the channel
- * is opened several times, the flag 'is_stale' is set after the
- * first time.
- *)
-
- val fixid = id
- val fixenc = fixenc
- val fixch = ch
-
- initializer
- getchannel := self # getchannel
-
- method private getchannel xid =
- begin match fixid with
- None -> ()
- | Some bound_xid ->
- if xid <> bound_xid then raise Not_competent
- end;
- ch, fixenc
-
- method private init_in (id:ext_id) =
- if is_stale then
- raise Not_competent
- else begin
- super # init_in id;
- is_stale <- true
- end
-
- method close_in =
- current_channel <- None
-
- method clone =
- let c = new resolve_read_this_channel1
- is_stale
- ?id:fixid ?fixenc:fixenc ?close:(Some close) fixch
- in
- c # init_rep_encoding internal_encoding;
- c # init_warner warner;
- clones <- c :: clones;
- (c :> resolver)
-
- end
-;;
-
-
-class resolve_read_this_channel =
- resolve_read_this_channel1 false
-;;
-
-
-class resolve_read_any_string ~string_of_id () =
- object (self)
- inherit resolve_general as super
-
- val f_open = string_of_id
- val mutable current_string = None
- val mutable current_pos = 0
-
- method private init_in (id:ext_id) =
- if current_string <> None then
- failwith "Pxp_reader.resolve_read_any_string # init_in";
- let s, enc_opt = f_open id in (* may raise Not_competent *)
- begin match enc_opt with
- None -> ()
- | Some enc -> encoding <- enc; encoding_requested <- true
- end;
- current_string <- Some s;
- current_pos <- 0;
-
- method private next_string s ofs len =
- match current_string with
- None -> failwith "Pxp_reader.resolve_read_any_string # next_string"
- | Some str ->
- let l = min len (String.length str - current_pos) in
- String.blit str current_pos s ofs l;
- current_pos <- current_pos + l;
- l
-
- method close_in =
- match current_string with
- None -> ()
- | Some _ ->
- current_string <- None
-
- method clone =
- let c = new resolve_read_any_string f_open () in
- c # init_rep_encoding internal_encoding;
- c # init_warner warner;
- clones <- c :: clones;
- (c :> resolver)
- end
-;;
-
-
-class resolve_read_this_string1 is_stale ?id ?fixenc str =
-
- let getstring = ref (fun xid -> assert false) in
-
- object (self)
- inherit resolve_read_any_string (fun xid -> !getstring xid) () as super
-
- val is_stale = is_stale
- (* For some reasons, it is not allowed to open a clone of the resolver
- * a second time when the original resolver is already open.
- *)
-
- val fixid = id
- val fixenc = fixenc
- val fixstr = str
-
- initializer
- getstring := self # getstring
-
- method private getstring xid =
- begin match fixid with
- None -> ()
- | Some bound_xid ->
- if xid <> bound_xid then raise Not_competent
- end;
- fixstr, fixenc
-
-
- method private init_in (id:ext_id) =
- if is_stale then
- raise Not_competent
- else
- super # init_in id
-
- method clone =
- let c = new resolve_read_this_string1
- (is_stale or current_string <> None)
- ?id:fixid ?fixenc:fixenc fixstr
- in
- c # init_rep_encoding internal_encoding;
- c # init_warner warner;
- clones <- c :: clones;
- (c :> resolver)
- end
-;;
-
-
-class resolve_read_this_string =
- resolve_read_this_string1 false
-;;
-
-
-class resolve_read_url_channel
- ?(base_url = Neturl.null_url)
- ?close
- ~url_of_id
- ~channel_of_url
- ()
-
- : resolver
- =
-
- let getchannel = ref (fun xid -> assert false) in
-
- object (self)
- inherit resolve_read_any_channel
- ?close
- (fun xid -> !getchannel xid)
- ()
- as super
-
- val base_url = base_url
- val mutable own_url = Neturl.null_url
-
- val url_of_id = url_of_id
- val channel_of_url = channel_of_url
-
-
- initializer
- getchannel := self # getchannel
-
- method private getchannel xid =
- let rel_url = url_of_id xid in (* may raise Not_competent *)
-
- try
- (* Now compute the absolute URL: *)
- let abs_url =
- if Neturl.url_provides ~scheme:true rel_url then
- rel_url
- else
- Neturl.apply_relative_url base_url rel_url in
- (* may raise Malformed_URL *)
-
- (* Simple check whether 'abs_url' is really absolute: *)
- if not(Neturl.url_provides ~scheme:true abs_url)
- then raise Not_competent;
-
- own_url <- abs_url;
- (* FIXME: Copy 'abs_url' ? *)
-
- (* Get and return the channel: *)
- channel_of_url xid abs_url (* may raise Not_competent *)
- with
- Neturl.Malformed_URL -> raise (Not_resolvable Neturl.Malformed_URL)
- | Not_competent -> raise (Not_resolvable Not_found)
-
- method clone =
- let c =
- new resolve_read_url_channel
- ?base_url:(Some own_url)
- ?close:(Some close)
- ~url_of_id:url_of_id
- ~channel_of_url:channel_of_url
- ()
- in
- c # init_rep_encoding internal_encoding;
- c # init_warner warner;
- clones <- c :: clones;
- (c :> resolve_read_url_channel)
- end
-;;
-
-
-type spec = [ `Not_recognized | `Allowed | `Required ]
-
-class resolve_as_file
- ?(file_prefix = (`Allowed :> spec))
- ?(host_prefix = (`Allowed :> spec))
- ?(system_encoding = `Enc_utf8)
- ?(map_private_id = (fun _ -> raise Not_competent))
- ?(open_private_id = (fun _ -> raise Not_competent))
- ()
- =
-
- let url_syntax =
- let enable_if =
- function
- `Not_recognized -> Neturl.Url_part_not_recognized
- | `Allowed -> Neturl.Url_part_allowed
- | `Required -> Neturl.Url_part_required
- in
- { Neturl.null_url_syntax with
- Neturl.url_enable_scheme = enable_if file_prefix;
- Neturl.url_enable_host = enable_if host_prefix;
- Neturl.url_enable_path = Neturl.Url_part_required;
- Neturl.url_accepts_8bits = true;
- }
- in
-
- let base_url_syntax =
- { Neturl.null_url_syntax with
- Neturl.url_enable_scheme = Neturl.Url_part_required;
- Neturl.url_enable_host = Neturl.Url_part_allowed;
- Neturl.url_enable_path = Neturl.Url_part_required;
- Neturl.url_accepts_8bits = true;
- }
- in
-
- let default_base_url =
- Neturl.make_url
- ~scheme: "file"
- ~host: ""
- ~path: (Neturl.split_path (Sys.getcwd() ^ "/"))
- base_url_syntax
- in
-
- let file_url_of_id xid =
- let file_url_of_sysname sysname =
- (* By convention, we can assume that sysname is a URL conforming
- * to RFC 1738 with the exception that it may contain non-ASCII
- * UTF-8 characters.
- *)
- try
- Neturl.url_of_string url_syntax sysname
- (* may raise Malformed_URL *)
- with
- Neturl.Malformed_URL -> raise Not_competent
- in
- let url =
- match xid with
- Anonymous -> raise Not_competent
- | Public (_,sysname) -> if sysname <> "" then file_url_of_sysname sysname
- else raise Not_competent
- | System sysname -> file_url_of_sysname sysname
- | Private pid -> map_private_id pid
- in
- let scheme =
- try Neturl.url_scheme url with Not_found -> "file" in
- let host =
- try Neturl.url_host url with Not_found -> "" in
-
- if scheme <> "file" then raise Not_competent;
- if host <> "" && host <> "localhost" then raise Not_competent;
-
- url
- in
-
- let channel_of_file_url xid url =
- match xid with
- Private pid -> open_private_id pid
- | _ ->
- ( try
- let path_utf8 =
- try Neturl.join_path (Neturl.url_path ~encoded:false url)
- with Not_found -> raise Not_competent
- in
-
- let path =
- Netconversion.recode_string
- ~in_enc: `Enc_utf8
- ~out_enc: system_encoding
- path_utf8 in
- (* May raise Malformed_code *)
-
- open_in_bin path, None
- (* May raise Sys_error *)
-
- with
- | Netconversion.Malformed_code -> assert false
- (* should not happen *)
- | Sys_error _ as e ->
- raise (Not_resolvable e)
- )
- in
-
- resolve_read_url_channel
- ~base_url: default_base_url
- ~url_of_id: file_url_of_id
- ~channel_of_url: channel_of_file_url
- ()
-;;
-
-
-let make_file_url ?(system_encoding = `Enc_utf8) ?(enc = `Enc_utf8) filename =
- let utf8_filename =
- Netconversion.recode_string
- ~in_enc: enc
- ~out_enc: `Enc_utf8
- filename
- in
-
- let utf8_abs_filename =
- if utf8_filename <> "" && utf8_filename.[0] = '/' then
- utf8_filename
- else
- let cwd = Sys.getcwd() in
- let cwd_utf8 =
- Netconversion.recode_string
- ~in_enc: system_encoding
- ~out_enc: `Enc_utf8 in
- cwd ^ "/" ^ utf8_filename
- in
-
- let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in
- let url = Neturl.make_url
- ~scheme:"file"
- ~host:"localhost"
- ~path:(Neturl.split_path utf8_abs_filename)
- syntax
- in
- url
-;;
-
-
-class lookup_public_id (catalog : (string * resolver) list) =
- let norm_catalog =
- List.map (fun (id,s) -> Pxp_aux.normalize_public_id id, s) catalog in
-( object (self)
- val cat = norm_catalog
- val mutable internal_encoding = `Enc_utf8
- val mutable warner = new drop_warnings
- val mutable active_resolver = None
-
- method init_rep_encoding enc =
- internal_encoding <- enc
-
- method init_warner w =
- warner <- w;
-
- method rep_encoding = internal_encoding
- (* CAUTION: This may not be the truth! *)
-
- method open_in xid =
-
- if active_resolver <> None then failwith "Pxp_reader.lookup_* # open_in";
-
- let r =
- match xid with
- Public(pubid,_) ->
- begin
- (* Search pubid in catalog: *)
- try
- let norm_pubid = Pxp_aux.normalize_public_id pubid in
- List.assoc norm_pubid cat
- with
- Not_found ->
- raise Not_competent
- end
- | _ ->
- raise Not_competent
- in
-
- let r' = r # clone in
- r' # init_rep_encoding internal_encoding;
- r' # init_warner warner;
- let lb = r' # open_in xid in (* may raise Not_competent *)
- active_resolver <- Some r';
- lb
-
- method close_in =
- match active_resolver with
- None -> ()
- | Some r -> r # close_in;
- active_resolver <- None
-
- method close_all =
- self # close_in
-
- method change_encoding (enc:string) =
- match active_resolver with
- None -> failwith "Pxp_reader.lookup_* # change_encoding"
- | Some r -> r # change_encoding enc
-
- method clone =
- let c = new lookup_public_id cat in
- c # init_rep_encoding internal_encoding;
- c # init_warner warner;
- c
- end : resolver )
-;;
-
-
-let lookup_public_id_as_file ?(fixenc:encoding option) catalog =
- let ch_of_id filename id =
- let ch = open_in_bin filename in (* may raise Sys_error *)
- ch, fixenc
- in
- let catalog' =
- List.map
- (fun (id,s) ->
- (id, new resolve_read_any_channel (ch_of_id s) ())
- )
- catalog
- in
- new lookup_public_id catalog'
-;;
-
-
-let lookup_public_id_as_string ?(fixenc:encoding option) catalog =
- let catalog' =
- List.map
- (fun (id,s) ->
- (id, new resolve_read_any_string (fun _ -> s, fixenc) ())
- )
- catalog
- in
- new lookup_public_id catalog'
-;;
-
-
-class lookup_system_id (catalog : (string * resolver) list) =
-( object (self)
- val cat = catalog
- val mutable internal_encoding = `Enc_utf8
- val mutable warner = new drop_warnings
- val mutable active_resolver = None
-
- method init_rep_encoding enc =
- internal_encoding <- enc
-
- method init_warner w =
- warner <- w;
-
- method rep_encoding = internal_encoding
- (* CAUTION: This may not be the truth! *)
-
-
- method open_in xid =
-
- if active_resolver <> None then failwith "Pxp_reader.lookup_system_id # open_in";
-
- let lookup sysid =
- try
- List.assoc sysid cat
- with
- Not_found ->
- raise Not_competent
- in
-
- let r =
- match xid with
- System sysid -> lookup sysid
- | Public(_,sysid) -> lookup sysid
- | _ -> raise Not_competent
- in
-
- let r' = r # clone in
- r' # init_rep_encoding internal_encoding;
- r' # init_warner warner;
- let lb = r' # open_in xid in (* may raise Not_competent *)
- active_resolver <- Some r';
- lb
-
-
- method close_in =
- match active_resolver with
- None -> ()
- | Some r -> r # close_in;
- active_resolver <- None
-
- method close_all =
- self # close_in
-
- method change_encoding (enc:string) =
- match active_resolver with
- None -> failwith "Pxp_reader.lookup_system # change_encoding"
- | Some r -> r # change_encoding enc
-
- method clone =
- let c = new lookup_system_id cat in
- c # init_rep_encoding internal_encoding;
- c # init_warner warner;
- c
- end : resolver)
-;;
-
-
-let lookup_system_id_as_file ?(fixenc:encoding option) catalog =
- let ch_of_id filename id =
- let ch = open_in_bin filename in (* may raise Sys_error *)
- ch, fixenc
- in
- let catalog' =
- List.map
- (fun (id,s) ->
- (id, new resolve_read_any_channel (ch_of_id s) ())
- )
- catalog
- in
- new lookup_system_id catalog'
-;;
-
-
-let lookup_system_id_as_string ?(fixenc:encoding option) catalog =
- let catalog' =
- List.map
- (fun (id,s) ->
- (id, new resolve_read_any_string (fun _ -> s, fixenc) ())
- )
- catalog
- in
- new lookup_system_id catalog'
-;;
-
-
-type combination_mode =
- Public_before_system
- | System_before_public
-;;
-
-
-class combine ?prefer ?(mode = Public_before_system) rl =
- object (self)
- val prefered_resolver = prefer
- val mode = mode
- val resolvers = (rl : resolver list)
- val mutable internal_encoding = `Enc_utf8
- val mutable warner = new drop_warnings
- val mutable active_resolver = None
- val mutable clones = []
-
- method init_rep_encoding enc =
- List.iter
- (fun r -> r # init_rep_encoding enc)
- rl;
- internal_encoding <- enc
-
- method init_warner w =
- List.iter
- (fun r -> r # init_warner w)
- rl;
- warner <- w;
-
- method rep_encoding = internal_encoding
- (* CAUTION: This may not be the truth! *)
-
- method open_in xid =
- let rec find_competent_resolver_for xid' rl =
- match rl with
- r :: rl' ->
- begin try
- r, (r # open_in xid')
- with
- Not_competent -> find_competent_resolver_for xid' rl'
- end;
- | [] ->
- raise Not_competent
- in
-
- let find_competent_resolver rl =
- match xid with
- Public(pubid,sysid) ->
- ( match mode with
- Public_before_system ->
- ( try
- find_competent_resolver_for(Public(pubid,"")) rl
- with
- Not_competent ->
- find_competent_resolver_for(System sysid) rl
- )
- | System_before_public ->
- ( try
- find_competent_resolver_for(System sysid) rl
- with
- Not_competent ->
- find_competent_resolver_for(Public(pubid,"")) rl
- )
- )
- | other ->
- find_competent_resolver_for other rl
- in
-
- if active_resolver <> None then failwith "Pxp_reader.combine # open_in";
- let r, lb =
- match prefered_resolver with
- None -> find_competent_resolver resolvers
- | Some r -> find_competent_resolver (r :: resolvers)
- in
- active_resolver <- Some r;
- lb
-
- method close_in =
- match active_resolver with
- None -> ()
- | Some r -> r # close_in;
- active_resolver <- None
-
- method close_all =
- List.iter (fun r -> r # close_in) clones
-
- method change_encoding (enc:string) =
- match active_resolver with
- None -> failwith "Pxp_reader.combine # change_encoding"
- | Some r -> r # change_encoding enc
-
- method clone =
- let c =
- match active_resolver with
- None ->
- new combine ?prefer:None ?mode:(Some mode)
- (List.map (fun q -> q # clone) resolvers)
- | Some r ->
- let r' = r # clone in
- new combine
- ?prefer:(Some r')
- ?mode:(Some mode)
- (List.map
- (fun q -> if q == r then r' else q # clone)
- resolvers)
- in
- c # init_rep_encoding internal_encoding;
- c # init_warner warner;
- clones <- c :: clones;
- c
- end
-
-
-
-(* ======================================================================
- * History:
- *
- * $Log$
- * Revision 1.1 2001/10/24 15:33:16 sacerdot
- * New procedure to create metadata committed and old procedure removed.
- * The new procedure is based on ocaml code and builds metadata for both
- * forward and backward pointers. The old one was based on a stylesheet.
- *
- * Revision 1.16 2001/07/01 09:46:40 gerd
- * Fix: resolve_read_url_channel does not use the base_url if
- * the current URL is already absolute
- *
- * Revision 1.15 2001/07/01 08:35:23 gerd
- * Instead of the ~auto_close argument, there is now a
- * ~close argument for several functions/classes. This allows some
- * additional action when the resolver is closed.
- *
- * Revision 1.14 2001/06/14 23:28:02 gerd
- * Fix: class combine works now with private IDs.
- *
- * Revision 1.13 2001/04/22 14:16:48 gerd
- * resolve_as_file: you can map private IDs to arbitrary channels.
- * resolve_read_url_channel: changed type of the channel_of_url
- * argument (ext_id is also passed)
- * More examples and documentation.
- *
- * Revision 1.12 2001/04/21 17:40:48 gerd
- * Bugfix in 'combine'
- *
- * Revision 1.11 2001/04/03 20:22:44 gerd
- * New resolvers for catalogs of PUBLIC and SYSTEM IDs.
- * Improved "combine": PUBLIC and SYSTEM IDs are handled
- * separately.
- * Rewritten from_file: Is now a simple application of the
- * Pxp_reader classes and functions. (The same has still to be done
- * for from_channel!)
- *
- * Revision 1.10 2001/02/01 20:38:49 gerd
- * New support for PUBLIC identifiers.
- *
- * Revision 1.9 2000/08/14 22:24:55 gerd
- * Moved the module Pxp_encoding to the netstring package under
- * the new name Netconversion.
- *
- * Revision 1.8 2000/07/16 18:31:09 gerd
- * The exception Illegal_character has been dropped.
- *
- * Revision 1.7 2000/07/09 15:32:01 gerd
- * Fix in resolve_this_channel, resolve_this_string
- *
- * Revision 1.6 2000/07/09 01:05:33 gerd
- * New methode 'close_all' that closes the clones, too.
- *
- * Revision 1.5 2000/07/08 16:24:56 gerd
- * Introduced the exception 'Not_resolvable' to indicate that
- * 'combine' should not try the next resolver of the list.
- *
- * Revision 1.4 2000/07/06 23:04:46 gerd
- * Quick fix for 'combine': The active resolver is "prefered",
- * but the other resolvers are also used.
- *
- * Revision 1.3 2000/07/06 21:43:45 gerd
- * Fix: Public(_,name) is now treated as System(name) if
- * name is non-empty.
- *
- * Revision 1.2 2000/07/04 22:13:30 gerd
- * Implemented the new API rev. 1.2 of pxp_reader.mli.
- *
- * Revision 1.1 2000/05/29 23:48:38 gerd
- * Changed module names:
- * Markup_aux into Pxp_aux
- * Markup_codewriter into Pxp_codewriter
- * Markup_document into Pxp_document
- * Markup_dtd into Pxp_dtd
- * Markup_entity into Pxp_entity
- * Markup_lexer_types into Pxp_lexer_types
- * Markup_reader into Pxp_reader
- * Markup_types into Pxp_types
- * Markup_yacc into Pxp_yacc
- * See directory "compatibility" for (almost) compatible wrappers emulating
- * Markup_document, Markup_dtd, Markup_reader, Markup_types, and Markup_yacc.
- *
- * ======================================================================
- * Old logs from markup_reader.ml:
- *
- * Revision 1.3 2000/05/29 21:14:57 gerd
- * Changed the type 'encoding' into a polymorphic variant.
- *
- * Revision 1.2 2000/05/20 20:31:40 gerd
- * Big change: Added support for various encodings of the
- * internal representation.
- *
- * Revision 1.1 2000/03/13 23:41:44 gerd
- * Initial revision; this code was formerly part of Markup_entity.
- *
- *
- *)
+++ /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 expect_possible_parameters = ref false;;
-
-exception NotExpectingPossibleParameters;;
-
-let rec deannotate_term =
- let module C = Cic in
- function
- C.ARel (_,_,n,_) -> C.Rel n
- | C.AVar (_,_,uri) -> C.Var uri
- | C.AMeta (_,_,n) -> C.Meta n
- | C.ASort (_,_,s) -> C.Sort s
- | C.AImplicit _ -> C.Implicit
- | C.ACast (_,_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
- | C.AProd (_,_,name,so,ta) ->
- C.Prod (name, deannotate_term so, deannotate_term ta)
- | C.ALambda (_,_,name,so,ta) ->
- C.Lambda (name, deannotate_term so, deannotate_term ta)
- | C.ALetIn (_,_,name,so,ta) ->
- C.LetIn (name, deannotate_term so, deannotate_term ta)
- | C.AAppl (_,_,l) -> C.Appl (List.map deannotate_term l)
- | C.AConst (_,_,uri, cookingsno) -> C.Const (uri, cookingsno)
- | C.AAbst (_,_,uri) -> C.Abst uri
- | C.AMutInd (_,_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i)
- | C.AMutConstruct (_,_,uri,cookingsno,i,j) ->
- C.MutConstruct (uri,cookingsno,i,j)
- | C.AMutCase (_,_,uri,cookingsno,i,outtype,te,pl) ->
- C.MutCase (uri,cookingsno,i,deannotate_term outtype,
- deannotate_term te, List.map deannotate_term pl)
- | C.AFix (_,_,funno,ifl) ->
- C.Fix (funno, List.map deannotate_inductiveFun ifl)
- | C.ACoFix (_,_,funno,ifl) ->
- C.CoFix (funno, List.map deannotate_coinductiveFun ifl)
-
-and deannotate_inductiveFun (name,index,ty,bo) =
- (name, index, deannotate_term ty, deannotate_term bo)
-
-and deannotate_coinductiveFun (name,ty,bo) =
- (name, deannotate_term ty, deannotate_term bo)
-;;
-
-let deannotate_inductiveType (name, isinductive, arity, cons) =
- (name, isinductive, deannotate_term arity,
- List.map (fun (id,ty,recs) -> (id,deannotate_term ty, recs)) cons)
-;;
-
-let deannotate_obj =
- let module C = Cic in
- function
- C.ADefinition (_, _, id, bo, ty, params) ->
- (match params with
- C.Possible params ->
- if !expect_possible_parameters then
- C.Definition (id, deannotate_term bo, deannotate_term ty, params)
- else
- raise NotExpectingPossibleParameters
- | C.Actual params ->
- C.Definition (id, deannotate_term bo, deannotate_term ty, params)
- )
- | C.AAxiom (_, _, id, ty, params) ->
- C.Axiom (id, deannotate_term ty, params)
- | C.AVariable (_, _, name, bo, ty) ->
- C.Variable (name,
- (match bo with None -> None | Some bo -> Some (deannotate_term bo)),
- deannotate_term ty)
- | C.ACurrentProof (_, _, name, conjs, bo, ty) ->
- C.CurrentProof (
- name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs,
- deannotate_term bo, deannotate_term ty
- )
- | C.AInductiveDefinition (_, _, tys, params, parno) ->
- C.InductiveDefinition ( List.map deannotate_inductiveType tys,
- params, parno)
-;;
+++ /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> *)
-(* 24/01/2000 *)
-(* *)
-(******************************************************************************)
-
-let getter_url = ref Configuration.getter_url;;
-
-let update () =
- (* deliver update request to http_getter *)
- ClientHTTP.send (!getter_url ^ "update")
-;;
-
-type format =
- Normal
- | GZipped
-;;
-
-let getxml ?(format=Normal) ?(patchdtd=true) uri =
- (* deliver getxml request to http_getter *)
- ClientHTTP.get_and_save_to_tmp
- (!getter_url ^ "getxml" ^
- "?uri=" ^ UriManager.string_of_uri uri ^
- "&format=" ^ (match format with Normal -> "normal" | GZipped -> "gzipped") ^
- "&patch_dtd=" ^ (match patchdtd with true -> "yes" | false -> "no")
- )
-;;
-
-let register uri url =
- (* deliver register request to http_getter *)
- ClientHTTP.send
- (!getter_url ^ "register" ^
- "?uri=" ^ (UriManager.string_of_uri uri) ^
- "&url=" ^ url)
-;;
+++ /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> *)
-(* 24/01/2000 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-(* THE URL OF THE HTTP GETTER *)
-val getter_url : string ref
-
-(* SIMPLE BINDINGS TO THE HTTP GETTER *)
-(* synchronize with the servers *)
-val update : unit -> unit
-
-type format =
- Normal
- | GZipped
-;;
-
-(* get the xml file *)
-(* defaults: format = Normal and patchdtd = true *)
-val getxml : ?format:format -> ?patchdtd:bool -> UriManager.uri -> string
-
-(* adds an (URI -> URL) entry in the map from URIs to URLs *)
-val register : UriManager.uri -> string -> unit
+++ /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> *)
-(* 11/10/2000 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-let resolve s =
- let starts_with s s' =
- if String.length s < String.length s' then
- false
- else
- (String.sub s 0 (String.length s')) = s'
- in
- if starts_with s "http:" then
- ClientHTTP.get_and_save_to_tmp s
- else
- s
-;;
-
-(*PXP 1.0
-let url_syntax =
- let enable_if =
- function
- `Not_recognized -> Neturl.Url_part_not_recognized
- | `Allowed -> Neturl.Url_part_allowed
- | `Required -> Neturl.Url_part_required
- in
- { Neturl.null_url_syntax with
- Neturl.url_enable_scheme = enable_if `Allowed;
- Neturl.url_enable_host = enable_if `Allowed;
- Neturl.url_enable_path = Neturl.Url_part_required;
- Neturl.url_accepts_8bits = true;
- }
-;;
-
-exception Unexpected;; (* Added when porting the file to PXP 1.1 *)
-
-let file_url_of_id xid =
- let file_url_of_sysname sysname =
- (* By convention, we can assume that sysname is a URL conforming
- * to RFC 1738 with the exception that it may contain non-ASCII
- * UTF-8 characters.
- *)
- try
- Neturl.url_of_string url_syntax sysname
- (* may raise Malformed_URL *)
- with
- Neturl.Malformed_URL -> raise Pxp_reader.Not_competent
- in
- let url =
- match xid with
- Pxp_types.Anonymous -> raise Pxp_reader.Not_competent
- | Pxp_types.Public (_,sysname) ->
- let sysname = resolve sysname in
- if sysname <> "" then file_url_of_sysname sysname
- else raise Pxp_reader.Not_competent
- | Pxp_types.System sysname ->
- let sysname = resolve sysname in
- file_url_of_sysname sysname
- | Pxp_types.Private pid -> raise Unexpected
- in
- let scheme =
- try Neturl.url_scheme url with Not_found -> "file" in
- let host =
- try Neturl.url_host url with Not_found -> "" in
-
- if scheme <> "file" then raise Pxp_reader.Not_competent;
- if host <> "" && host <> "localhost" then raise Pxp_reader.Not_competent;
-
- url
-;;
-
-let from_file ?system_encoding utf8_filename =
-
- let r =
- new Pxp_reader.resolve_as_file
- ?system_encoding:system_encoding
- ~url_of_id:file_url_of_id
- ()
- in
-
- let utf8_abs_filename =
- if utf8_filename <> "" && utf8_filename.[0] = '/' then
- utf8_filename
- else
- Sys.getcwd() ^ "/" ^ utf8_filename
- in
-
- let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in
- let url = Neturl.make_url
- ~scheme:"file"
- ~host:"localhost"
- ~path:(Neturl.split_path utf8_abs_filename)
- syntax
- in
-
- let xid = Pxp_types.System (Neturl.string_of_url url) in
-
-
- Pxp_yacc.ExtID(xid, r)
-;;
-*)
-
-(*PXP 1.1*)
-(* csc_pxp_reader.ml is an exact copy of PXP pxp_reader.ml *)
-(* The only reason is to loosen the interface *)
-
-class resolve_as_file
- ?(file_prefix = (`Allowed :> Csc_pxp_reader.spec))
- ?(host_prefix = (`Allowed :> Csc_pxp_reader.spec))
- ?(system_encoding = `Enc_utf8)
- ?(map_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent))
- ?(open_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent))
- ()
- =
-
- let url_syntax =
- let enable_if =
- function
- `Not_recognized -> Neturl.Url_part_not_recognized
- | `Allowed -> Neturl.Url_part_allowed
- | `Required -> Neturl.Url_part_required
- in
- { Neturl.null_url_syntax with
- Neturl.url_enable_scheme = enable_if file_prefix;
- Neturl.url_enable_host = enable_if host_prefix;
- Neturl.url_enable_path = Neturl.Url_part_required;
- Neturl.url_accepts_8bits = true;
- }
- in
-
- let base_url_syntax =
- { Neturl.null_url_syntax with
- Neturl.url_enable_scheme = Neturl.Url_part_required;
- Neturl.url_enable_host = Neturl.Url_part_allowed;
- Neturl.url_enable_path = Neturl.Url_part_required;
- Neturl.url_accepts_8bits = true;
- }
- in
-
- let default_base_url =
- Neturl.make_url
- ~scheme: "file"
- ~host: ""
- ~path: (Neturl.split_path (Sys.getcwd() ^ "/"))
- base_url_syntax
- in
-
- let file_url_of_id xid =
- let module P = Csc_pxp_reader in
- let module T = Pxp_types in
- let file_url_of_sysname sysname =
- (* By convention, we can assume that sysname is a URL conforming
- * to RFC 1738 with the exception that it may contain non-ASCII
- * UTF-8 characters.
- *)
- try
- Neturl.url_of_string url_syntax sysname
- (* may raise Malformed_URL *)
- with
- Neturl.Malformed_URL -> raise P.Not_competent
- in
- let url =
- match xid with
- T.Anonymous -> raise P.Not_competent
- | T.Public (_,sysname) -> let sysname = resolve sysname in
- if sysname <> "" then file_url_of_sysname sysname
- else raise P.Not_competent
- | T.System sysname -> let sysname = resolve sysname in
- file_url_of_sysname sysname
- | T.Private pid -> map_private_id pid
- in
- let scheme =
- try Neturl.url_scheme url with Not_found -> "file" in
- let host =
- try Neturl.url_host url with Not_found -> "" in
-
- if scheme <> "file" then raise P.Not_competent;
- if host <> "" && host <> "localhost" then raise P.Not_competent;
-
- url
- in
-
- let channel_of_file_url xid url =
- let module P = Csc_pxp_reader in
- let module T = Pxp_types in
- match xid with
- T.Private pid -> open_private_id pid
- | _ ->
- ( try
- let path_utf8 =
- try Neturl.join_path (Neturl.url_path ~encoded:false url)
- with Not_found -> raise P.Not_competent
- in
-
- let path =
- Netconversion.recode_string
- ~in_enc: `Enc_utf8
- ~out_enc: system_encoding
- path_utf8 in
- (* May raise Malformed_code *)
-
- open_in_bin path, None
- (* May raise Sys_error *)
-
- with
- | Netconversion.Malformed_code -> assert false
- (* should not happen *)
- | Sys_error _ as e ->
- raise (P.Not_resolvable e)
- )
- in
-
- Csc_pxp_reader.resolve_read_url_channel
- ~base_url: default_base_url
- ~url_of_id: file_url_of_id
- ~channel_of_url: channel_of_file_url
- ()
-;;
-
-let from_file ?(alt = []) ?system_encoding ?enc utf8_filename =
- let r =
- new resolve_as_file
- ?system_encoding:system_encoding
- ()
- in
-
- let url = Csc_pxp_reader.make_file_url
- ?system_encoding
- ?enc
- utf8_filename in
-
- let xid = Pxp_types.System (Neturl.string_of_url url) in
-
- Pxp_yacc.ExtID(xid, new Csc_pxp_reader.combine (r :: alt))
-;;
-
+++ /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/.
- *)
-
-(* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *)
-type uri = string array;;
-
-let eq uri1 uri2 =
- uri1 == uri2
-;;
-
-let string_of_uri uri = uri.(Array.length uri - 2);;
-let name_of_uri uri = uri.(Array.length uri - 1);;
-let buri_of_uri uri = uri.(Array.length uri - 3);;
-let depth_of_uri uri = Array.length uri - 2;;
-
-(*CSC: ora e' diventato poco efficiente, migliorare *)
-let relative_depth curi uri cookingsno =
- let rec length_of_current_prefix l1 l2 =
- match (l1, l2) with
- (he1::tl1, he2::tl2) when he1 == he2 ->
- 1 + length_of_current_prefix tl1 tl2
- | (_,_) -> 0
- in
- depth_of_uri uri -
- length_of_current_prefix
- (Array.to_list (Array.sub curi 0 (Array.length curi - (2 + cookingsno))))
- (Array.to_list (Array.sub uri 0 (Array.length uri - 2)))
- (*CSC: vecchio codice da eliminare
- if eq curi uri then 0
- else
- depth_of_uri uri -
- length_of_current_prefix (Array.to_list curi) (Array.to_list uri)
- *)
-;;
-
-module OrderedStrings =
- struct
- type t = string
- let compare (s1 : t) (s2 : t) = compare s1 s2
- end
-;;
-
-module SetOfStrings = Map.Make(OrderedStrings);;
-
-(*CSC: commento obsoleto ed errato *)
-(* Invariant: the map is the identity function, *)
-(* i.e. (SetOfStrings.find str !set_of_uri) == str *)
-let set_of_uri = ref SetOfStrings.empty;;
-let set_of_prefixes = ref SetOfStrings.empty;;
-
-(* similar to uri_of_string, but used for prefixes of uris *)
-let normalize prefix =
- try
- SetOfStrings.find prefix !set_of_prefixes
- with
- Not_found ->
- set_of_prefixes := SetOfStrings.add prefix prefix !set_of_prefixes ;
- prefix
-;;
-
-exception IllFormedUri of string;;
-
-let mk_prefixes str =
- let rec aux curi =
- function
- [he] ->
- let prefix_uri = curi ^ "/" ^ he
- and name = List.hd (Str.split (Str.regexp "\.") he) in
- [ normalize prefix_uri ; name ]
- | he::tl ->
- let prefix_uri = curi ^ "/" ^ he in
- (normalize prefix_uri)::(aux prefix_uri tl)
- | _ -> raise (IllFormedUri str)
- in
- let tokens = (Str.split (Str.regexp "/") str) in
- (* ty = "cic:" *)
- let (ty, sp) = (List.hd tokens, List.tl tokens) in
- aux ty sp
-;;
-
-let uri_of_string str =
- try
- SetOfStrings.find str !set_of_uri
- with
- Not_found ->
- let uri = Array.of_list (mk_prefixes str) in
- set_of_uri := SetOfStrings.add str uri !set_of_uri ;
- uri
-;;
-
-let cicuri_of_uri uri =
- let completeuri = string_of_uri uri in
- let newcompleteuri =
- (Str.replace_first (Str.regexp "\.types$") ""
- (Str.replace_first (Str.regexp "\.ann$") "" completeuri))
- in
- if completeuri = newcompleteuri then
- uri
- else
- let newuri = Array.copy uri in
- newuri.(Array.length uri - 2) <- newcompleteuri ;
- newuri
-;;
-
-let annuri_of_uri uri =
- let completeuri = string_of_uri uri in
- if Str.string_match (Str.regexp ".*\.ann$") completeuri 0 then
- uri
- else
- let newuri = Array.copy uri in
- newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ;
- newuri
-;;
-
-let uri_is_annuri uri =
- Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0
-;;
+++ /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/.
- *)
-
-type uri
-
-val eq : uri -> uri -> bool
-
-val uri_of_string : string -> uri
-
-val string_of_uri : uri -> string (* complete uri *)
-val name_of_uri : uri -> string (* name only (without extension)*)
-val buri_of_uri : uri -> string (* base uri only *)
-val depth_of_uri : uri -> int (* length of the path *)
-
-(* relative_depth curi uri cookingsno *)
-(* is the number of times to cook uri to use it when the current uri is curi *)
-(* cooked cookingsno times *)
-val relative_depth : uri -> uri -> int -> int
-
-(* given an uri, returns the uri of the corresponding cic file, *)
-(* i.e. removes the [.types][.ann] suffix *)
-val cicuri_of_uri : uri -> uri
-
-(* given an uri, returns the uri of the corresponding annotation file, *)
-(* i.e. adds the .ann suffix if not already present *)
-val annuri_of_uri : uri -> uri
-
-(* given an uri, tells if it refers to an annotation *)
-val uri_is_annuri : uri -> bool
+++ /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 *)
-(* *)
-(* A tactic to print Coq objects in XML *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 18/10/2000 *)
-(* *)
-(* This module defines a pretty-printer and the stream of commands to the pp *)
-(* *)
-(******************************************************************************)
-
-
-(* the type token for XML cdata, empty elements and not-empty elements *)
-(* Usage: *)
-(* Str cdata *)
-(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *)
-(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
-(* content *)
-type token = Str of string
- | Empty of string * (string * string) list
- | NEmpty of string * (string * string) list * token Stream.t
-;;
-
-(* currified versions of the constructors make the code more readable *)
-let xml_empty name attrs = [< 'Empty(name,attrs) >]
-let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >]
-let xml_cdata str = [< 'Str str >]
-
-(* Usage: *)
-(* pp tokens None pretty prints the output on stdout *)
-(* pp tokens (Some filename) pretty prints the output on the file filename *)
-let pp ?(quiet=false) strm fn =
- let channel = ref stdout in
- let rec pp_r m =
- parser
- [< 'Str a ; s >] ->
- print_spaces m ;
- fprint_string (a ^ "\n") ;
- pp_r m s
- | [< 'Empty(n,l) ; s >] ->
- print_spaces m ;
- fprint_string ("<" ^ n) ;
- List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
- fprint_string "/>\n" ;
- pp_r m s
- | [< 'NEmpty(n,l,c) ; s >] ->
- print_spaces m ;
- fprint_string ("<" ^ n) ;
- List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
- fprint_string ">\n" ;
- pp_r (m+1) c ;
- print_spaces m ;
- fprint_string ("</" ^ n ^ ">\n") ;
- pp_r m s
- | [< >] -> ()
- and print_spaces m =
- for i = 1 to m do fprint_string " " done
- and fprint_string str =
- output_string !channel str
- in
- match fn with
- Some filename ->
- channel := open_out filename ;
- pp_r 0 strm ;
- close_out !channel ;
- if not quiet then
- begin
- print_string ("\nWriting on file \"" ^ filename ^
- "\" was succesfull\n");
- flush stdout
- end
- | None ->
- pp_r 0 strm
-;;
+++ /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 *)
-(* *)
-(* A tactic to print Coq objects in XML *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 18/10/2000 *)
-(* *)
-(* This module defines a pretty-printer and the stream of commands to the pp *)
-(* *)
-(******************************************************************************)
-
-(* Tokens for XML cdata, empty elements and not-empty elements *)
-(* Usage: *)
-(* Str cdata *)
-(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *)
-(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
-(* content *)
-type token =
- | Str of string
- | Empty of string * (string * string) list
- | NEmpty of string * (string * string) list * token Stream.t
-
-(* currified versions of the token constructors make the code more readable *)
-val xml_empty : string -> (string * string) list -> token Stream.t
-val xml_nempty :
- string -> (string * string) list -> token Stream.t -> token Stream.t
-val xml_cdata : string -> token Stream.t
-
-(* The pretty printer for streams of token *)
-(* Usage: *)
-(* pp tokens None pretty prints the output on stdout *)
-(* pp tokens (Some filename) pretty prints the output on the file filename *)
-val pp : ?quiet:bool -> token Stream.t -> string option -> unit
projects / helm.git / commitdiff