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 depth -> `MainConclusion depth
  38   | `MainHypothesis depth -> `MainHypothesis depth
  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 _, pos1), `Sort (Cic.Type _, pos2) ->
  54           Pervasives.compare pos1 pos2
  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   | `MainConclusion (Some depth) -> `MainConclusion (Some (depth + 1))
  67   | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1))
  68   | _ -> assert false
  69
  70 let compute_term pos term =
  71   let rec aux (pos: position) set = function
  72     | Cic.Rel _ ->
  73         if is_main_pos pos then
  74           S.add (`Rel (main_pos pos)) set
  75         else
  76           set
  77     | Cic.Var _ -> set
  78     | Cic.Meta (_, local_context) ->
  79         List.fold_left
  80           (fun set context ->
  81             match context with
  82             | None -> set
  83             | Some term -> aux (next_pos pos) set term)
  84           set
  85           local_context
  86     | Cic.Sort sort ->
  87         if is_main_pos pos then
  88           S.add (`Sort (sort, main_pos pos)) set
  89         else
  90           set
  91     | Cic.Implicit _ -> assert false
  92     | Cic.Cast (term, ty) ->
  93         (* TODO consider also ty? *)
  94         aux pos set term
  95     | Cic.Prod (_, source, target) ->
  96         (match pos with
  97         | `MainConclusion _ ->
  98             let set = aux (`MainHypothesis (Some 0)) set source in
  99             aux (incr_depth pos) set target
 100         | `MainHypothesis _ ->
 101             let set = aux `InHypothesis set source in
 102             aux (incr_depth pos) set target
 103         | `InConclusion
 104         | `InHypothesis
 105         | `InBody ->
 106             let set = aux pos set source in
 107             aux pos set target)
 108     | Cic.Lambda (_, source, target) ->
 109         assert (not (is_main_pos pos));
 110         let set = aux pos set source in
 111         aux pos set target
 112     | Cic.LetIn (_, term, target) ->
 113         if is_main_pos pos then
 114           aux pos set (CicSubstitution.subst term target)
 115         else
 116           let set = aux pos set term in
 117           aux pos set target
 118     | Cic.Appl [] -> assert false
 119     | Cic.Appl (hd :: tl) ->
 120         let set = aux pos set hd in
 121         List.fold_left
 122           (fun set term -> aux (next_pos pos) set term)
 123           set tl
 124     | Cic.Const (uri, subst) ->
 125         let set = S.add (`Obj (string_of_uri uri, pos)) set in
 126         List.fold_left
 127           (fun set (_, term) -> aux (next_pos pos) set term)
 128           set subst
 129     | Cic.MutInd (uri, typeno, subst) ->
 130         let uri = UriManager.string_of_uriref (uri, [typeno]) in
 131         let set = S.add (`Obj (uri, pos)) set in
 132         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
 133           set subst
 134     | Cic.MutConstruct (uri, typeno, consno, subst) ->
 135         let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
 136         let set = S.add (`Obj (uri, pos)) set in
 137         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
 138           set subst
 139     | Cic.MutCase (uri, _, outtype, term, pats) ->
 140         let pos = next_pos pos in
 141         let set = aux pos set term in
 142         let set = aux pos set outtype in
 143         List.fold_left (fun set term -> aux pos set term) set pats
 144     | Cic.Fix (_, funs) ->
 145         let pos = next_pos pos in
 146         List.fold_left
 147           (fun set (_, _, ty, body) ->
 148             let set = aux pos set ty in
 149             aux pos set body)
 150           set funs
 151     | Cic.CoFix (_, funs) ->
 152         let pos = next_pos pos in
 153         List.fold_left
 154           (fun set (_, ty, body) ->
 155             let set = aux pos set ty in
 156             aux pos set body)
 157           set funs
 158   in
 159   aux pos S.empty term
 160
 161 module OrderedInt =
 162 struct
 163   type t = int
 164   let compare = Pervasives.compare
 165 end
 166
 167 module IntSet = Set.Make (OrderedInt)
 168
 169 let compute_metas term =
 170   let rec aux in_hyp ((concl_metas, hyp_metas) as acc) cic =
 171     match cic with
 172     | Cic.Rel _
 173     | Cic.Sort _
 174     | Cic.Var _ -> acc
 175     | Cic.Meta (no, local_context) ->
 176         let acc =
 177           if in_hyp then
 178             (concl_metas, IntSet.add no hyp_metas)
 179           else
 180             (IntSet.add no concl_metas, hyp_metas)
 181         in
 182         List.fold_left
 183           (fun set context ->
 184             match context with
 185             | None -> set
 186             | Some term -> aux in_hyp set term)
 187           acc
 188           local_context
 189     | Cic.Implicit _ -> assert false
 190     | Cic.Cast (term, ty) ->
 191         (* TODO consider also ty? *)
 192         aux in_hyp acc term
 193     | Cic.Prod (_, source, target) ->
 194         if in_hyp then
 195           let acc = aux in_hyp acc source in
 196           aux in_hyp acc target
 197         else
 198           let acc = aux true acc source in
 199           aux in_hyp acc target
 200     | Cic.Lambda (_, source, target) ->
 201         let acc = aux in_hyp acc source in
 202         aux in_hyp acc target
 203     | Cic.LetIn (_, term, target) ->
 204         aux in_hyp acc (CicSubstitution.subst term target)
 205     | Cic.Appl [] -> assert false
 206     | Cic.Appl (hd :: tl) ->
 207         let acc = aux in_hyp acc hd in
 208         List.fold_left (fun acc term -> aux in_hyp acc term) acc tl
 209     | Cic.Const (_, subst)
 210     | Cic.MutInd (_, _, subst)
 211     | Cic.MutConstruct (_, _, _, subst) ->
 212         List.fold_left (fun acc (_, term) -> aux in_hyp acc term) acc subst
 213     | Cic.MutCase (uri, _, outtype, term, pats) ->
 214         let acc = aux in_hyp acc term in
 215         let acc = aux in_hyp acc outtype in
 216         List.fold_left (fun acc term -> aux in_hyp acc term) acc pats
 217     | Cic.Fix (_, funs) ->
 218         List.fold_left
 219           (fun acc (_, _, ty, body) ->
 220             let acc = aux in_hyp acc ty in
 221             aux in_hyp acc body)
 222           acc funs
 223     | Cic.CoFix (_, funs) ->
 224         List.fold_left
 225           (fun acc (_, ty, body) ->
 226             let acc = aux in_hyp acc ty in
 227             aux in_hyp acc body)
 228           acc funs
 229   in
 230   aux false (IntSet.empty, IntSet.empty) term
 231
 232 let compute_type uri typeno (name, _, ty, constructors) =
 233   let consno = ref 0 in
 234   let type_metadata =
 235     (UriManager.string_of_uriref (uri, [typeno]), name,
 236     S.elements (compute_term (`MainConclusion (Some 0)) ty))
 237   in
 238   let constructors_metadata =
 239     List.map
 240       (fun (name, term) ->
 241         incr consno;
 242         let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
 243         (uri, name, S.elements (compute_term (`MainConclusion (Some 0)) term)))
 244       constructors
 245   in
 246   type_metadata :: constructors_metadata
 247
 248 let compute_ind ~uri ~types =
 249   let idx = ref ~-1 in
 250   List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types)
 251
 252 let compute ~body ~ty =
 253   let type_metadata = compute_term (`MainConclusion (Some 0)) ty in
 254   let body_metadata =
 255     match body with
 256     | None -> S.empty
 257     | Some body -> compute_term `InBody body
 258   in
 259   let uris =
 260     S.fold
 261       (fun metadata uris ->
 262         match metadata with
 263         | `Obj (uri, _) -> StringSet.add uri uris
 264         | _ -> uris)
 265       type_metadata StringSet.empty
 266   in
 267   S.elements
 268     (S.union
 269       (S.filter
 270         (function
 271           | `Obj (uri, _) when StringSet.mem uri uris -> false
 272           | _ -> true)
 273         body_metadata)
 274       type_metadata)
 275
 276 let compute_term start_pos term = S.elements (compute_term start_pos term)
 277