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 =
 153    match CicParser.term_of_xml cicfilename uri false with
 154       (annobj, None) ->
 155         Deannotate.deannotate_obj annobj
 156     | _ -> assert false
 157   in
 158    Unix.unlink cicfilename ;
 159    res
 160 ;;
 161
 162 let add_every_constructor uri typeno kind =
 163  let module C = Cic in
 164   match (get_obj uri) with
 165       (C.InductiveDefinition (itys,_,_)) ->
 166         let string_uri = UriManager.string_of_uri uri in
 167         let sn = string_of_int (typeno + 1) in
 168         let (_,_,_,cons) = List.nth itys typeno in
 169          iteri
 170           (fun (_,cty,_) m ->
 171             let sm = string_of_int m in
 172              UriHash.add_uri
 173               (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
 174               kind
 175           ) cons
 176    | _ -> assert false
 177 ;;
 178
 179 let process_type term =
 180  let module U = UriManager in
 181  let module H = UriHash in
 182  let module C = Cic in
 183   let rec process_type_aux kind =
 184    function
 185     | C.Var uri ->
 186        H.add_uri (U.string_of_uri uri) kind
 187     | C.Cast (te,_) ->
 188        (* type ignored *)
 189        process_type_aux kind te
 190     | C.Prod (_,sou,ta) ->
 191        let (source_kind,target_kind) =
 192         match kind with
 193            H.Backbone -> (H.Branch,H.Backbone)
 194          | H.Branch -> (H.InHypothesis,H.InHypothesis)
 195          | H.InBody -> assert false
 196          | k -> (k,k)
 197        in
 198         process_type_aux source_kind sou ;
 199         process_type_aux target_kind ta
 200     | C.Lambda (_,sou,ta) ->
 201         let kind' = H.soften_classification kind in
 202          process_type_aux kind' sou ;
 203          process_type_aux kind' ta
 204     | C.LetIn (_,te,ta)->
 205        let kind' = H.soften_classification kind in
 206         process_type_aux kind' te ;
 207         process_type_aux kind ta
 208     | C.Appl (he::tl) ->
 209        let kind' = H.soften_classification kind in
 210         process_type_aux kind he ;
 211         List.iter (process_type_aux kind') tl
 212     | C.Appl _ -> assert false
 213     | C.Const (uri,_) ->
 214        UriHash.add_uri (U.string_of_uri uri) kind
 215     | C.Abst _ -> assert false
 216     | C.MutInd (uri,_,typeno) ->
 217        H.add_uri
 218         (U.string_of_uri uri ^ "#xpointer(1/" ^
 219           string_of_int (typeno + 1) ^ ")")
 220         kind
 221     | C.MutConstruct (uri,_,typeno,consno) ->
 222        H.add_uri
 223         (U.string_of_uri uri ^ "#xpointer(1/" ^
 224           string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
 225         kind
 226     | C.MutCase (uri,_,typeno,_,term,patterns) ->
 227        (* outtype ignored *)
 228        let kind' = H.soften_classification kind in
 229         add_every_constructor uri typeno kind' ;
 230         process_type_aux kind' term ;
 231         List.iter (process_type_aux kind') patterns
 232     | C.Fix (_,funs) ->
 233        let kind' = H.soften_classification kind in
 234         List.iter
 235          (function (_,_,bo,ty) ->
 236            process_type_aux kind' bo ;
 237            process_type_aux kind' ty ;
 238          ) funs
 239     | C.CoFix (_,funs) ->
 240        let kind' = H.soften_classification kind in
 241         List.iter
 242          (function (_,bo,ty) ->
 243            process_type_aux kind' bo ;
 244            process_type_aux kind' ty ;
 245          ) funs
 246     | _ -> ()
 247 in
 248  process_type_aux H.Backbone (CicMiniReduction.letin_nf term)
 249 ;;
 250
 251 let process_body =
 252  let module U = UriManager in
 253  let module H = UriHash in
 254  let module C = Cic in
 255   let rec process_body_aux =
 256    function
 257       C.Var uri ->
 258        H.add_uri (U.string_of_uri uri) H.InBody
 259     | C.Cast (te,ty) ->
 260        process_body_aux te ;
 261        process_body_aux ty
 262     | C.Prod (_,sou,ta) ->
 263        process_body_aux sou ;
 264        process_body_aux ta
 265     | C.Lambda (_,sou,ta) ->
 266        process_body_aux sou ;
 267        process_body_aux ta
 268     | C.LetIn (_,te,ta)->
 269        process_body_aux te ;
 270        process_body_aux ta
 271     | C.Appl l ->
 272        List.iter process_body_aux l
 273     | C.Const (uri,_) ->
 274        UriHash.add_uri (U.string_of_uri uri) H.InBody
 275     | C.Abst _ -> assert false
 276     | C.MutInd (uri,_,typeno) ->
 277        H.add_uri
 278         (U.string_of_uri uri ^ "#xpointer(1/" ^
 279           string_of_int (typeno + 1) ^ ")")
 280         H.InBody
 281     | C.MutConstruct (uri,_,typeno,consno) ->
 282        H.add_uri
 283         (U.string_of_uri uri ^ "#xpointer(1/" ^
 284           string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
 285         H.InBody
 286     | C.MutCase (uri,_,typeno,outtype,term,patterns) ->
 287        add_every_constructor uri typeno H.InBody ;
 288        process_body_aux outtype ;
 289        process_body_aux term ;
 290        List.iter process_body_aux patterns
 291     | C.Fix (_,funs) ->
 292        List.iter
 293         (function (_,_,bo,ty) ->
 294           process_body_aux bo ;
 295           process_body_aux ty ;
 296         ) funs
 297     | C.CoFix (_,funs) ->
 298        List.iter
 299         (function (_,bo,ty) ->
 300           process_body_aux bo ;
 301           process_body_aux ty ;
 302         ) funs
 303     | _ -> ()
 304 in
 305  process_body_aux
 306 ;;
 307
 308 let process_obj string_uri =
 309  let module U = UriManager in
 310  let module C = Cic in
 311   function
 312      (C.Definition (_,bo,ty,_)) ->
 313        process_type ty ;
 314        process_body bo ;
 315        output_file string_uri string_uri
 316    | (C.Axiom (_,ty,_)) ->
 317        process_type ty ;
 318        output_file string_uri string_uri
 319    | (C.Variable (_,bo,ty)) ->
 320        process_type ty ;
 321        begin
 322         match bo with
 323            (Some bo') -> process_body bo'
 324          | _ -> ()
 325        end ;
 326        output_file string_uri string_uri
 327    | (C.InductiveDefinition _) as id ->
 328        begin
 329         let id' =
 330          CicSubstitution.undebrujin_inductive_def
 331           (U.uri_of_string string_uri) id
 332         in
 333          match id' with
 334             (C.InductiveDefinition (itys,_,_)) ->
 335               iteri
 336                (fun (_,_,ty,cons) n ->
 337                  let sn = string_of_int n in
 338                   process_type ty ;
 339                   output_file
 340                    (string_uri ^ "#xpointer(1/" ^ sn ^ ")")
 341                    (string_uri ^ "," ^ sn) ;
 342                   iteri
 343                    (fun (_,cty,_) m ->
 344                      let sm = string_of_int m in
 345                       process_type cty ;
 346                       output_file
 347                        (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
 348                        (string_uri ^ "," ^ sn ^ "," ^ sm)
 349                    ) cons
 350                ) itys
 351           | _ -> assert false
 352        end
 353    | (C.CurrentProof _) -> assert false
 354 ;;
 355
 356 let mk_forward string_uri =
 357  let module U = UriManager in
 358   print_endline ("Now computing metadata of " ^ string_uri) ;
 359   flush stdout ;
 360   let uri = U.uri_of_string string_uri in
 361   let obj = get_obj uri in
 362    process_obj string_uri obj
 363 ;;
 364
 365 let _ =
 366  let usage_msg = "usage: mk_forward[.opt] URI" in
 367  let uri = ref "" in
 368   Arg.parse []
 369    (fun x ->
 370      if x = "" then
 371       begin
 372        prerr_string "No URI provided.\n" ;
 373        Arg.usage [] usage_msg ;
 374        exit (-1)
 375       end
 376      else if !uri = "" then
 377       uri := x
 378      else
 379       begin
 380        prerr_string "More than two arguments provided.\n" ;
 381        Arg.usage [] usage_msg ;
 382        exit (-1)
 383       end
 384    ) usage_msg ;
 385    if !uri = "" then
 386     begin
 387      prerr_string "No URI provided.\n" ;
 388      Arg.usage [] usage_msg ;
 389      exit (-1)
 390     end ;
 391    mk_forward !uri
 392 ;;