X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmetadata%2Fcreate2%2Fmk_forward%2Fmk_forward.ml;fp=helm%2Fmetadata%2Fcreate2%2Fmk_forward%2Fmk_forward.ml;h=0000000000000000000000000000000000000000;hp=e97ed33476e05b2c3e7072e2fca30a39dd1a89c1;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8 diff --git a/helm/metadata/create2/mk_forward/mk_forward.ml b/helm/metadata/create2/mk_forward/mk_forward.ml deleted file mode 100644 index e97ed3347..000000000 --- a/helm/metadata/create2/mk_forward/mk_forward.ml +++ /dev/null @@ -1,385 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 03/04/2001 *) -(* *) -(* Missing description *) -(* *) -(******************************************************************************) - -let iteri foo = - let counter = ref 0 in - List.iter (function e -> incr counter ; foo e !counter) -;; - -let pathname_of_uri uristring = - "forward" ^ - Str.replace_first (Str.regexp "^cic:") "" uristring -;; - -let make_dirs dirpath = - ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\"")) -;; - -module UriHash = - struct - type classification = - Backbone - | Branch - | InConclusion - | InHypothesis - | InBody - ;; - -let soften_classification = - function - Backbone -> InConclusion - | Branch -> InHypothesis - | InBody -> assert false - | k -> k -;; - - let hash = Hashtbl.create 117 ;; - - let add_uri uri kind = - let old_kinds = - try - Hashtbl.find hash uri - with - Not_found -> [] - in - let new_kinds = - match kind,old_kinds with - InBody,[] -> [InBody] - | InBody,_ -> old_kinds - | k,_ when List.mem k old_kinds -> old_kinds - | k,_ -> k::old_kinds - in - Hashtbl.replace hash uri new_kinds - ;; - - (* It also removes every element in the hash *) - let uris_fold foo init = - let xml_element_name_of_kind = - function - Backbone -> "MainConclusion" - | Branch -> "MainHypothesis" - | InConclusion -> "InConclusion" - | InHypothesis -> "InHypothesis" - | InBody -> "InBody" - in - let res = - Hashtbl.fold - (fun uri kinds i -> - List.fold_left - (fun j kind -> - foo j uri (xml_element_name_of_kind kind) - ) i kinds - ) hash init - in - Hashtbl.clear hash ; - res - ;; - end -;; - -let output_content () = - UriHash.uris_fold - (fun i uri kind -> - [< Xml.xml_nempty "h:refObj" [] - (Xml.xml_empty "h:Occurrence" - ["rdf:about","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#" ^ kind ; - "rdf:value",uri] - ) ; - i - >] - ) [<>] -;; - -let output_file cic_string_uri rdf_string_uri = - let module U = UriManager in - let module X = Xml in - let content = output_content () in - let rdf_uri = U.uri_of_string rdf_string_uri in - make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ; - X.pp - [< X.xml_cdata "\n" ; - X.xml_nempty "rdf:RDF" - ["xml:lang","en" ; - "xmlns:rdf","http://www.w3.org/1999/02/22-rdf-syntax-ns#"; - "xmlns:h","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#"] - - (try - Stream.empty content ; (* raise Stream.failure if not empty *) - X.xml_empty "h:Object" ["rdf:about",cic_string_uri] - with - Stream.Failure -> - X.xml_nempty "h:Object" ["rdf:about",cic_string_uri] content - ) - >] - (Some (pathname_of_uri rdf_string_uri ^ ".xml")) -;; - -let get_obj uri = - let cicfilename = Getter.getxml uri in - let res = CicParser.obj_of_xml cicfilename uri in - Unix.unlink cicfilename ; - res -;; - -let add_every_constructor uri typeno kind = - let module C = Cic in - match (get_obj uri) with - (C.InductiveDefinition (itys,_,_)) -> - let string_uri = UriManager.string_of_uri uri in - let sn = string_of_int (typeno + 1) in - let (_,_,_,cons) = List.nth itys typeno in - iteri - (fun (_,cty,_) m -> - let sm = string_of_int m in - UriHash.add_uri - (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")") - kind - ) cons - | _ -> assert false -;; - -let process_type term = - let module U = UriManager in - let module H = UriHash in - let module C = Cic in - let rec process_type_aux kind = - function - | C.Var uri -> - H.add_uri (U.string_of_uri uri) kind - | C.Cast (te,_) -> - (* type ignored *) - process_type_aux kind te - | C.Prod (_,sou,ta) -> - let (source_kind,target_kind) = - match kind with - H.Backbone -> (H.Branch,H.Backbone) - | H.Branch -> (H.InHypothesis,H.InHypothesis) - | H.InBody -> assert false - | k -> (k,k) - in - process_type_aux source_kind sou ; - process_type_aux target_kind ta - | C.Lambda (_,sou,ta) -> - let kind' = H.soften_classification kind in - process_type_aux kind' sou ; - process_type_aux kind' ta - | C.LetIn (_,te,ta)-> - let kind' = H.soften_classification kind in - process_type_aux kind' te ; - process_type_aux kind ta - | C.Appl (he::tl) -> - let kind' = H.soften_classification kind in - process_type_aux kind he ; - List.iter (process_type_aux kind') tl - | C.Appl _ -> assert false - | C.Const (uri,_) -> - UriHash.add_uri (U.string_of_uri uri) kind - | C.MutInd (uri,_,typeno) -> - H.add_uri - (U.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (typeno + 1) ^ ")") - kind - | C.MutConstruct (uri,_,typeno,consno) -> - H.add_uri - (U.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")") - kind - | C.MutCase (uri,_,typeno,_,term,patterns) -> - (* outtype ignored *) - let kind' = H.soften_classification kind in - add_every_constructor uri typeno kind' ; - process_type_aux kind' term ; - List.iter (process_type_aux kind') patterns - | C.Fix (_,funs) -> - let kind' = H.soften_classification kind in - List.iter - (function (_,_,bo,ty) -> - process_type_aux kind' bo ; - process_type_aux kind' ty ; - ) funs - | C.CoFix (_,funs) -> - let kind' = H.soften_classification kind in - List.iter - (function (_,bo,ty) -> - process_type_aux kind' bo ; - process_type_aux kind' ty ; - ) funs - | _ -> () -in - process_type_aux H.Backbone (CicMiniReduction.letin_nf term) -;; - -let process_body = - let module U = UriManager in - let module H = UriHash in - let module C = Cic in - let rec process_body_aux = - function - C.Var uri -> - H.add_uri (U.string_of_uri uri) H.InBody - | C.Cast (te,ty) -> - process_body_aux te ; - process_body_aux ty - | C.Prod (_,sou,ta) -> - process_body_aux sou ; - process_body_aux ta - | C.Lambda (_,sou,ta) -> - process_body_aux sou ; - process_body_aux ta - | C.LetIn (_,te,ta)-> - process_body_aux te ; - process_body_aux ta - | C.Appl l -> - List.iter process_body_aux l - | C.Const (uri,_) -> - UriHash.add_uri (U.string_of_uri uri) H.InBody - | C.MutInd (uri,_,typeno) -> - H.add_uri - (U.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (typeno + 1) ^ ")") - H.InBody - | C.MutConstruct (uri,_,typeno,consno) -> - H.add_uri - (U.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")") - H.InBody - | C.MutCase (uri,_,typeno,outtype,term,patterns) -> - add_every_constructor uri typeno H.InBody ; - process_body_aux outtype ; - process_body_aux term ; - List.iter process_body_aux patterns - | C.Fix (_,funs) -> - List.iter - (function (_,_,bo,ty) -> - process_body_aux bo ; - process_body_aux ty ; - ) funs - | C.CoFix (_,funs) -> - List.iter - (function (_,bo,ty) -> - process_body_aux bo ; - process_body_aux ty ; - ) funs - | _ -> () -in - process_body_aux -;; - -let process_obj string_uri = - let module U = UriManager in - let module C = Cic in - function - (C.Definition (_,bo,ty,_)) -> - process_type ty ; - process_body bo ; - output_file string_uri string_uri - | (C.Axiom (_,ty,_)) -> - process_type ty ; - output_file string_uri string_uri - | (C.Variable (_,bo,ty)) -> - process_type ty ; - begin - match bo with - (Some bo') -> process_body bo' - | _ -> () - end ; - output_file string_uri string_uri - | (C.InductiveDefinition _) as id -> - begin - let id' = - CicSubstitution.undebrujin_inductive_def - (U.uri_of_string string_uri) id - in - match id' with - (C.InductiveDefinition (itys,_,_)) -> - iteri - (fun (_,_,ty,cons) n -> - let sn = string_of_int n in - process_type ty ; - output_file - (string_uri ^ "#xpointer(1/" ^ sn ^ ")") - (string_uri ^ "," ^ sn) ; - iteri - (fun (_,cty,_) m -> - let sm = string_of_int m in - process_type cty ; - output_file - (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")") - (string_uri ^ "," ^ sn ^ "," ^ sm) - ) cons - ) itys - | _ -> assert false - end - | (C.CurrentProof _) -> assert false -;; - -let mk_forward string_uri = - let module U = UriManager in - print_endline ("Now computing metadata of " ^ string_uri) ; - flush stdout ; - let uri = U.uri_of_string string_uri in - let obj = get_obj uri in - process_obj string_uri obj -;; - -let _ = - let usage_msg = "usage: mk_forward[.opt] URI" in - let uri = ref "" in - Arg.parse [] - (fun x -> - if x = "" then - begin - prerr_string "No URI provided.\n" ; - Arg.usage [] usage_msg ; - exit (-1) - end - else if !uri = "" then - uri := x - else - begin - prerr_string "More than two arguments provided.\n" ; - Arg.usage [] usage_msg ; - exit (-1) - end - ) usage_msg ; - if !uri = "" then - begin - prerr_string "No URI provided.\n" ; - Arg.usage [] usage_msg ; - exit (-1) - end ; - mk_forward !uri -;;