helm/metadata/create2/mk_forward/mk_forward.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 03/04/2001                                 *)
  32 (*                                                                            *)
  33 (*                            Missing description                             *)
  34 (*                                                                            *)
  35 (******************************************************************************)
  36
  37 let iteri foo =
  38  let counter = ref 0 in
  39   List.iter (function e -> incr counter ; foo e !counter)
  40 ;;
  41
  42 let pathname_of_uri uristring =
  43  "forward" ^
  44   Str.replace_first (Str.regexp "^cic:") "" uristring
  45 ;;
  46
  47 let make_dirs dirpath =
  48  ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\""))
  49 ;;
  50
  51 module UriHash =
  52  struct
  53   type classification =
  54      Backbone
  55    | Branch
  56    | InConclusion
  57    | InHypothesis
  58    | InBody
  59   ;;
  60
  61 let soften_classification =
  62  function
  63     Backbone -> InConclusion
  64   | Branch -> InHypothesis
  65   | InBody -> assert false
  66   | k -> k
  67 ;;
  68
  69   let hash = Hashtbl.create 117 ;;
  70
  71   let add_uri uri kind =
  72    let old_kinds =
  73     try
  74      Hashtbl.find hash uri
  75     with
  76      Not_found -> []
  77    in
  78     let new_kinds =
  79      match kind,old_kinds with
  80         InBody,[] -> [InBody]
  81       | InBody,_  -> old_kinds
  82       | k,_ when List.mem k old_kinds -> old_kinds
  83       | k,_ -> k::old_kinds
  84     in
  85      Hashtbl.replace hash uri new_kinds
  86   ;;
  87
  88   (* It also removes every element in the hash *)
  89   let uris_fold foo init =
  90    let xml_element_name_of_kind =
  91     function
  92        Backbone     -> "MainConclusion"
  93      | Branch       -> "MainHypothesis"
  94      | InConclusion -> "InConclusion"
  95      | InHypothesis -> "InHypothesis"
  96      | InBody       -> "InBody"
  97    in
  98     let res =
  99      Hashtbl.fold
 100       (fun uri kinds i ->
 101         List.fold_left
 102          (fun j kind ->
 103            foo j uri (xml_element_name_of_kind kind)
 104          ) i kinds
 105       ) hash init
 106     in
 107      Hashtbl.clear hash ;
 108      res
 109   ;;
 110  end
 111 ;;
 112
 113 let output_content () =
 114  UriHash.uris_fold
 115   (fun i uri kind ->
 116     [< Xml.xml_nempty "h:refObj" []
 117         (Xml.xml_empty "h:Occurrence"
 118           ["rdf:about","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#" ^ kind ;
 119            "rdf:value",uri]
 120         ) ;
 121        i
 122     >]
 123   ) [<>]
 124 ;;
 125
 126 let output_file cic_string_uri rdf_string_uri =
 127  let module U = UriManager in
 128  let module X = Xml in
 129   let content = output_content () in
 130   let rdf_uri = U.uri_of_string rdf_string_uri in
 131    make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ;
 132    X.pp
 133     [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 134        X.xml_nempty "rdf:RDF"
 135         ["xml:lang","en" ;
 136          "xmlns:rdf","http://www.w3.org/1999/02/22-rdf-syntax-ns#";
 137          "xmlns:h","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#"]
 138
 139         (try
 140           Stream.empty content ; (* raise Stream.failure if not empty *)
 141           X.xml_empty "h:Object" ["rdf:about",cic_string_uri]
 142          with
 143           Stream.Failure ->
 144            X.xml_nempty "h:Object" ["rdf:about",cic_string_uri] content
 145         )
 146     >]
 147     (Some (pathname_of_uri rdf_string_uri ^ ".xml"))
 148 ;;
 149
 150 let get_obj uri =
 151  let cicfilename = Getter.getxml uri in
 152   let res = CicParser.obj_of_xml cicfilename uri in
 153    Unix.unlink cicfilename ;
 154    res
 155 ;;
 156
 157 let add_every_constructor uri typeno kind =
 158  let module C = Cic in
 159   match (get_obj uri) with
 160       (C.InductiveDefinition (itys,_,_)) ->
 161         let string_uri = UriManager.string_of_uri uri in
 162         let sn = string_of_int (typeno + 1) in
 163         let (_,_,_,cons) = List.nth itys typeno in
 164          iteri
 165           (fun (_,cty,_) m ->
 166             let sm = string_of_int m in
 167              UriHash.add_uri
 168               (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
 169               kind
 170           ) cons
 171    | _ -> assert false
 172 ;;
 173
 174 let process_type term =
 175  let module U = UriManager in
 176  let module H = UriHash in
 177  let module C = Cic in
 178   let rec process_type_aux kind =
 179    function
 180     | C.Var uri ->
 181        H.add_uri (U.string_of_uri uri) kind
 182     | C.Cast (te,_) ->
 183        (* type ignored *)
 184        process_type_aux kind te
 185     | C.Prod (_,sou,ta) ->
 186        let (source_kind,target_kind) =
 187         match kind with
 188            H.Backbone -> (H.Branch,H.Backbone)
 189          | H.Branch -> (H.InHypothesis,H.InHypothesis)
 190          | H.InBody -> assert false
 191          | k -> (k,k)
 192        in
 193         process_type_aux source_kind sou ;
 194         process_type_aux target_kind ta
 195     | C.Lambda (_,sou,ta) ->
 196         let kind' = H.soften_classification kind in
 197          process_type_aux kind' sou ;
 198          process_type_aux kind' ta
 199     | C.LetIn (_,te,ta)->
 200        let kind' = H.soften_classification kind in
 201         process_type_aux kind' te ;
 202         process_type_aux kind ta
 203     | C.Appl (he::tl) ->
 204        let kind' = H.soften_classification kind in
 205         process_type_aux kind he ;
 206         List.iter (process_type_aux kind') tl
 207     | C.Appl _ -> assert false
 208     | C.Const (uri,_) ->
 209        UriHash.add_uri (U.string_of_uri uri) kind
 210     | C.Abst _ -> assert false
 211     | C.MutInd (uri,_,typeno) ->
 212        H.add_uri
 213         (U.string_of_uri uri ^ "#xpointer(1/" ^
 214           string_of_int (typeno + 1) ^ ")")
 215         kind
 216     | C.MutConstruct (uri,_,typeno,consno) ->
 217        H.add_uri
 218         (U.string_of_uri uri ^ "#xpointer(1/" ^
 219           string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
 220         kind
 221     | C.MutCase (uri,_,typeno,_,term,patterns) ->
 222        (* outtype ignored *)
 223        let kind' = H.soften_classification kind in
 224         add_every_constructor uri typeno kind' ;
 225         process_type_aux kind' term ;
 226         List.iter (process_type_aux kind') patterns
 227     | C.Fix (_,funs) ->
 228        let kind' = H.soften_classification kind in
 229         List.iter
 230          (function (_,_,bo,ty) ->
 231            process_type_aux kind' bo ;
 232            process_type_aux kind' ty ;
 233          ) funs
 234     | C.CoFix (_,funs) ->
 235        let kind' = H.soften_classification kind in
 236         List.iter
 237          (function (_,bo,ty) ->
 238            process_type_aux kind' bo ;
 239            process_type_aux kind' ty ;
 240          ) funs
 241     | _ -> ()
 242 in
 243  process_type_aux H.Backbone (CicMiniReduction.letin_nf term)
 244 ;;
 245
 246 let process_body =
 247  let module U = UriManager in
 248  let module H = UriHash in
 249  let module C = Cic in
 250   let rec process_body_aux =
 251    function
 252       C.Var uri ->
 253        H.add_uri (U.string_of_uri uri) H.InBody
 254     | C.Cast (te,ty) ->
 255        process_body_aux te ;
 256        process_body_aux ty
 257     | C.Prod (_,sou,ta) ->
 258        process_body_aux sou ;
 259        process_body_aux ta
 260     | C.Lambda (_,sou,ta) ->
 261        process_body_aux sou ;
 262        process_body_aux ta
 263     | C.LetIn (_,te,ta)->
 264        process_body_aux te ;
 265        process_body_aux ta
 266     | C.Appl l ->
 267        List.iter process_body_aux l
 268     | C.Const (uri,_) ->
 269        UriHash.add_uri (U.string_of_uri uri) H.InBody
 270     | C.Abst _ -> assert false
 271     | C.MutInd (uri,_,typeno) ->
 272        H.add_uri
 273         (U.string_of_uri uri ^ "#xpointer(1/" ^
 274           string_of_int (typeno + 1) ^ ")")
 275         H.InBody
 276     | C.MutConstruct (uri,_,typeno,consno) ->
 277        H.add_uri
 278         (U.string_of_uri uri ^ "#xpointer(1/" ^
 279           string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
 280         H.InBody
 281     | C.MutCase (uri,_,typeno,outtype,term,patterns) ->
 282        add_every_constructor uri typeno H.InBody ;
 283        process_body_aux outtype ;
 284        process_body_aux term ;
 285        List.iter process_body_aux patterns
 286     | C.Fix (_,funs) ->
 287        List.iter
 288         (function (_,_,bo,ty) ->
 289           process_body_aux bo ;
 290           process_body_aux ty ;
 291         ) funs
 292     | C.CoFix (_,funs) ->
 293        List.iter
 294         (function (_,bo,ty) ->
 295           process_body_aux bo ;
 296           process_body_aux ty ;
 297         ) funs
 298     | _ -> ()
 299 in
 300  process_body_aux
 301 ;;
 302
 303 let process_obj string_uri =
 304  let module U = UriManager in
 305  let module C = Cic in
 306   function
 307      (C.Definition (_,bo,ty,_)) ->
 308        process_type ty ;
 309        process_body bo ;
 310        output_file string_uri string_uri
 311    | (C.Axiom (_,ty,_)) ->
 312        process_type ty ;
 313        output_file string_uri string_uri
 314    | (C.Variable (_,bo,ty)) ->
 315        process_type ty ;
 316        begin
 317         match bo with
 318            (Some bo') -> process_body bo'
 319          | _ -> ()
 320        end ;
 321        output_file string_uri string_uri
 322    | (C.InductiveDefinition _) as id ->
 323        begin
 324         let id' =
 325          CicSubstitution.undebrujin_inductive_def
 326           (U.uri_of_string string_uri) id
 327         in
 328          match id' with
 329             (C.InductiveDefinition (itys,_,_)) ->
 330               iteri
 331                (fun (_,_,ty,cons) n ->
 332                  let sn = string_of_int n in
 333                   process_type ty ;
 334                   output_file
 335                    (string_uri ^ "#xpointer(1/" ^ sn ^ ")")
 336                    (string_uri ^ "," ^ sn) ;
 337                   iteri
 338                    (fun (_,cty,_) m ->
 339                      let sm = string_of_int m in
 340                       process_type cty ;
 341                       output_file
 342                        (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
 343                        (string_uri ^ "," ^ sn ^ "," ^ sm)
 344                    ) cons
 345                ) itys
 346           | _ -> assert false
 347        end
 348    | (C.CurrentProof _) -> assert false
 349 ;;
 350
 351 let mk_forward string_uri =
 352  let module U = UriManager in
 353   print_endline ("Now computing metadata of " ^ string_uri) ;
 354   flush stdout ;
 355   let uri = U.uri_of_string string_uri in
 356   let obj = get_obj uri in
 357    process_obj string_uri obj
 358 ;;
 359
 360 let _ =
 361  let usage_msg = "usage: mk_forward[.opt] URI" in
 362  let uri = ref "" in
 363   Arg.parse []
 364    (fun x ->
 365      if x = "" then
 366       begin
 367        prerr_string "No URI provided.\n" ;
 368        Arg.usage [] usage_msg ;
 369        exit (-1)
 370       end
 371      else if !uri = "" then
 372       uri := x
 373      else
 374       begin
 375        prerr_string "More than two arguments provided.\n" ;
 376        Arg.usage [] usage_msg ;
 377        exit (-1)
 378       end
 379    ) usage_msg ;
 380    if !uri = "" then
 381     begin
 382      prerr_string "No URI provided.\n" ;
 383      Arg.usage [] usage_msg ;
 384      exit (-1)
 385     end ;
 386    mk_forward !uri
 387 ;;