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.MutInd (uri,_,typeno) ->
 211        H.add_uri
 212         (U.string_of_uri uri ^ "#xpointer(1/" ^
 213           string_of_int (typeno + 1) ^ ")")
 214         kind
 215     | C.MutConstruct (uri,_,typeno,consno) ->
 216        H.add_uri
 217         (U.string_of_uri uri ^ "#xpointer(1/" ^
 218           string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
 219         kind
 220     | C.MutCase (uri,_,typeno,_,term,patterns) ->
 221        (* outtype ignored *)
 222        let kind' = H.soften_classification kind in
 223         add_every_constructor uri typeno kind' ;
 224         process_type_aux kind' term ;
 225         List.iter (process_type_aux kind') patterns
 226     | C.Fix (_,funs) ->
 227        let kind' = H.soften_classification kind in
 228         List.iter
 229          (function (_,_,bo,ty) ->
 230            process_type_aux kind' bo ;
 231            process_type_aux kind' ty ;
 232          ) funs
 233     | C.CoFix (_,funs) ->
 234        let kind' = H.soften_classification kind in
 235         List.iter
 236          (function (_,bo,ty) ->
 237            process_type_aux kind' bo ;
 238            process_type_aux kind' ty ;
 239          ) funs
 240     | _ -> ()
 241 in
 242  process_type_aux H.Backbone (CicMiniReduction.letin_nf term)
 243 ;;
 244
 245 let process_body =
 246  let module U = UriManager in
 247  let module H = UriHash in
 248  let module C = Cic in
 249   let rec process_body_aux =
 250    function
 251       C.Var uri ->
 252        H.add_uri (U.string_of_uri uri) H.InBody
 253     | C.Cast (te,ty) ->
 254        process_body_aux te ;
 255        process_body_aux ty
 256     | C.Prod (_,sou,ta) ->
 257        process_body_aux sou ;
 258        process_body_aux ta
 259     | C.Lambda (_,sou,ta) ->
 260        process_body_aux sou ;
 261        process_body_aux ta
 262     | C.LetIn (_,te,ta)->
 263        process_body_aux te ;
 264        process_body_aux ta
 265     | C.Appl l ->
 266        List.iter process_body_aux l
 267     | C.Const (uri,_) ->
 268        UriHash.add_uri (U.string_of_uri uri) H.InBody
 269     | C.MutInd (uri,_,typeno) ->
 270        H.add_uri
 271         (U.string_of_uri uri ^ "#xpointer(1/" ^
 272           string_of_int (typeno + 1) ^ ")")
 273         H.InBody
 274     | C.MutConstruct (uri,_,typeno,consno) ->
 275        H.add_uri
 276         (U.string_of_uri uri ^ "#xpointer(1/" ^
 277           string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
 278         H.InBody
 279     | C.MutCase (uri,_,typeno,outtype,term,patterns) ->
 280        add_every_constructor uri typeno H.InBody ;
 281        process_body_aux outtype ;
 282        process_body_aux term ;
 283        List.iter process_body_aux patterns
 284     | C.Fix (_,funs) ->
 285        List.iter
 286         (function (_,_,bo,ty) ->
 287           process_body_aux bo ;
 288           process_body_aux ty ;
 289         ) funs
 290     | C.CoFix (_,funs) ->
 291        List.iter
 292         (function (_,bo,ty) ->
 293           process_body_aux bo ;
 294           process_body_aux ty ;
 295         ) funs
 296     | _ -> ()
 297 in
 298  process_body_aux
 299 ;;
 300
 301 let process_obj string_uri =
 302  let module U = UriManager in
 303  let module C = Cic in
 304   function
 305      (C.Definition (_,bo,ty,_)) ->
 306        process_type ty ;
 307        process_body bo ;
 308        output_file string_uri string_uri
 309    | (C.Axiom (_,ty,_)) ->
 310        process_type ty ;
 311        output_file string_uri string_uri
 312    | (C.Variable (_,bo,ty)) ->
 313        process_type ty ;
 314        begin
 315         match bo with
 316            (Some bo') -> process_body bo'
 317          | _ -> ()
 318        end ;
 319        output_file string_uri string_uri
 320    | (C.InductiveDefinition _) as id ->
 321        begin
 322         let id' =
 323          CicSubstitution.undebrujin_inductive_def
 324           (U.uri_of_string string_uri) id
 325         in
 326          match id' with
 327             (C.InductiveDefinition (itys,_,_)) ->
 328               iteri
 329                (fun (_,_,ty,cons) n ->
 330                  let sn = string_of_int n in
 331                   process_type ty ;
 332                   output_file
 333                    (string_uri ^ "#xpointer(1/" ^ sn ^ ")")
 334                    (string_uri ^ "," ^ sn) ;
 335                   iteri
 336                    (fun (_,cty,_) m ->
 337                      let sm = string_of_int m in
 338                       process_type cty ;
 339                       output_file
 340                        (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
 341                        (string_uri ^ "," ^ sn ^ "," ^ sm)
 342                    ) cons
 343                ) itys
 344           | _ -> assert false
 345        end
 346    | (C.CurrentProof _) -> assert false
 347 ;;
 348
 349 let mk_forward string_uri =
 350  let module U = UriManager in
 351   print_endline ("Now computing metadata of " ^ string_uri) ;
 352   flush stdout ;
 353   let uri = U.uri_of_string string_uri in
 354   let obj = get_obj uri in
 355    process_obj string_uri obj
 356 ;;
 357
 358 let _ =
 359  let usage_msg = "usage: mk_forward[.opt] URI" in
 360  let uri = ref "" in
 361   Arg.parse []
 362    (fun x ->
 363      if x = "" then
 364       begin
 365        prerr_string "No URI provided.\n" ;
 366        Arg.usage [] usage_msg ;
 367        exit (-1)
 368       end
 369      else if !uri = "" then
 370       uri := x
 371      else
 372       begin
 373        prerr_string "More than two arguments provided.\n" ;
 374        Arg.usage [] usage_msg ;
 375        exit (-1)
 376       end
 377    ) usage_msg ;
 378    if !uri = "" then
 379     begin
 380      prerr_string "No URI provided.\n" ;
 381      Arg.usage [] usage_msg ;
 382      exit (-1)
 383     end ;
 384    mk_forward !uri
 385 ;;