helm/ocaml/metadata/metadataExtractor.ml

   1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 open MetadataTypes
  29
  30 let is_main_pos = function
  31   | `MainConclusion
  32   | `MainHypothesis -> true
  33   | _ -> false
  34
  35 let main_pos (pos: position): main_position =
  36   match pos with
  37   | `MainConclusion -> `MainConclusion
  38   | `MainHypothesis -> `MainHypothesis
  39   | _ -> assert false
  40
  41 let next_pos = function
  42   | `MainConclusion -> `InConclusion
  43   | `MainHypothesis -> `InHypothesis
  44   | pos -> pos
  45
  46 let string_of_uri = UriManager.string_of_uri
  47
  48 module OrderedMetadata =
  49   struct
  50     type t = MetadataTypes.metadata
  51     let compare m1 m2 = (* ignore universes in Cic.Type sort *)
  52       match (m1, m2) with
  53       | `Sort (Cic.Type _, p1, d1), `Sort (Cic.Type _, p2, d2) ->
  54           Pervasives.compare (p1, d2) (p2, d2)
  55       | _ -> Pervasives.compare m1 m2
  56   end
  57
  58 module MetadataSet = Set.Make (OrderedMetadata)
  59 module StringSet = Set.Make (String)
  60
  61 module S = MetadataSet
  62
  63 let unopt = function Some x -> x | None -> assert false
  64
  65 let incr_depth = function
  66   | None -> assert false
  67   | Some x -> Some (x + 1)
  68
  69 let compute_term pos term =
  70   let rec aux (pos: position) pi_depth set = function
  71     | Cic.Rel _ ->
  72         if is_main_pos pos then
  73           S.add (`Rel (main_pos pos, unopt pi_depth)) set
  74         else
  75           set
  76     | Cic.Var _ -> set
  77     | Cic.Meta (_, local_context) ->
  78         List.fold_left
  79           (fun set context ->
  80             match context with
  81             | None -> set
  82             | Some term -> aux pos pi_depth set term)
  83           set
  84           local_context
  85     | Cic.Sort sort ->
  86         if is_main_pos pos then
  87           S.add (`Sort (sort, main_pos pos, unopt pi_depth)) set
  88         else
  89           set
  90     | Cic.Implicit _ -> assert false
  91     | Cic.Cast (term, ty) ->
  92         (* TODO consider also ty? *)
  93         aux pos pi_depth set term
  94     | Cic.Prod (_, source, target) ->
  95         (match pos with
  96         | `MainConclusion ->
  97             let set = aux `MainHypothesis (Some 0) set source in
  98             aux pos (incr_depth pi_depth) set target
  99         | `MainHypothesis ->
 100             let set = aux `InHypothesis None set source in
 101             aux pos (incr_depth pi_depth) set target
 102         | `InConclusion
 103         | `InHypothesis
 104         | `InBody ->
 105             let set = aux pos None set source in
 106             aux pos None set target)
 107     | Cic.Lambda (_, source, target) ->
 108         assert (not (is_main_pos pos));
 109         let set = aux pos None set source in
 110         aux pos None set target
 111     | Cic.LetIn (_, term, target) ->
 112         if is_main_pos pos then
 113           aux pos pi_depth set (CicSubstitution.subst term target)
 114         else
 115           let set = aux pos None set term in
 116           aux pos None set target
 117     | Cic.Appl [] -> assert false
 118     | Cic.Appl (hd :: tl) ->
 119         let set = aux pos pi_depth set hd in
 120         List.fold_left
 121           (fun set term -> aux (next_pos pos) None set term)
 122           set tl
 123     | Cic.Const (uri, subst) ->
 124         let set = S.add (`Obj (string_of_uri uri, pos, pi_depth)) set in
 125         List.fold_left
 126           (fun set (_, term) -> aux (next_pos pos) None set term)
 127           set subst
 128     | Cic.MutInd (uri, typeno, subst) ->
 129         let uri = UriManager.string_of_uriref (uri, [typeno]) in
 130         let set = S.add (`Obj (uri, pos, pi_depth)) set in
 131         List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term)
 132           set subst
 133     | Cic.MutConstruct (uri, typeno, consno, subst) ->
 134         let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
 135         let set = S.add (`Obj (uri, pos, pi_depth)) set in
 136         List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term)
 137           set subst
 138     | Cic.MutCase (uri, _, outtype, term, pats) ->
 139         let pos = next_pos pos in
 140         let set = aux pos None set term in
 141         let set = aux pos None set outtype in
 142         List.fold_left (fun set term -> aux pos None set term) set pats
 143     | Cic.Fix (_, funs) ->
 144         let pos = next_pos pos in
 145         List.fold_left
 146           (fun set (_, _, ty, body) ->
 147             let set = aux pos None set ty in
 148             aux pos None set body)
 149           set funs
 150     | Cic.CoFix (_, funs) ->
 151         let pos = next_pos pos in
 152         List.fold_left
 153           (fun set (_, ty, body) ->
 154             let set = aux pos None set ty in
 155             aux pos None set body)
 156           set funs
 157   in
 158   aux pos (Some 0) S.empty term
 159
 160 let compute_type uri typeno (name, _, ty, constructors) =
 161   let consno = ref 0 in
 162   let type_metadata =
 163     (UriManager.string_of_uriref (uri, [typeno]), name,
 164     S.elements (compute_term `MainConclusion ty))
 165   in
 166   let constructors_metadata =
 167     List.map
 168       (fun (name, term) ->
 169         incr consno;
 170         let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
 171         (uri, name, S.elements (compute_term `MainConclusion term)))
 172       constructors
 173   in
 174   type_metadata :: constructors_metadata
 175
 176 let compute_ind ~uri ~types =
 177   let idx = ref ~-1 in
 178   List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types)
 179
 180 let compute ~body ~ty =
 181   let type_metadata = compute_term `MainConclusion ty in
 182   let body_metadata =
 183     match body with
 184     | None -> S.empty
 185     | Some body -> compute_term `InBody body
 186   in
 187   let uris =
 188     S.fold
 189       (fun metadata uris ->
 190         match metadata with
 191         | `Obj (uri, _, _) -> StringSet.add uri uris
 192         | _ -> uris)
 193       type_metadata StringSet.empty
 194   in
 195   S.elements
 196     (S.union
 197       (S.filter
 198         (function
 199           | `Obj (uri, _, _) when StringSet.mem uri uris -> false
 200           | _ -> true)
 201         body_metadata)
 202       type_metadata)
 203