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 var_has_body uri =
  71   match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
  72   | Cic.Variable (_, Some body, _, _, _), _ -> true
  73   | _ -> false
  74
  75 let compute_term pos term =
  76   let rec aux (pos: position) set = function
  77     | Cic.Var (uri, subst) when var_has_body uri ->
  78         (* handles variables with body as constants *)
  79         aux pos set (Cic.Const (uri, subst))
  80     | Cic.Rel _
  81     | Cic.Var _ ->
  82         if is_main_pos pos then
  83           S.add (`Rel (main_pos pos)) set
  84         else
  85           set
  86     | Cic.Meta (_, local_context) ->
  87         List.fold_left
  88           (fun set context ->
  89             match context with
  90             | None -> set
  91             | Some term -> aux (next_pos pos) set term)
  92           set
  93           local_context
  94     | Cic.Sort sort ->
  95         if is_main_pos pos then
  96           S.add (`Sort (sort, main_pos pos)) set
  97         else
  98           set
  99     | Cic.Implicit _ -> assert false
 100     | Cic.Cast (term, ty) ->
 101         (* TODO consider also ty? *)
 102         aux pos set term
 103     | Cic.Prod (_, source, target) ->
 104         (match pos with
 105         | `MainConclusion _ ->
 106             let set = aux (`MainHypothesis (Some 0)) set source in
 107             aux (incr_depth pos) set target
 108         | `MainHypothesis _ ->
 109             let set = aux `InHypothesis set source in
 110             aux (incr_depth pos) set target
 111         | `InConclusion
 112         | `InHypothesis
 113         | `InBody ->
 114             let set = aux pos set source in
 115             aux pos set target)
 116     | Cic.Lambda (_, source, target) ->
 117         (*assert (not (is_main_pos pos));*)
 118         let set = aux (next_pos pos) set source in
 119         aux (next_pos pos) set target
 120     | Cic.LetIn (_, term, target) ->
 121         if is_main_pos pos then
 122           aux pos set (CicSubstitution.subst term target)
 123         else
 124           let set = aux pos set term in
 125           aux pos set target
 126     | Cic.Appl [] -> assert false
 127     | Cic.Appl (hd :: tl) ->
 128         let set = aux pos set hd in
 129         List.fold_left
 130           (fun set term -> aux (next_pos pos) set term)
 131           set tl
 132     | Cic.Const (uri, subst) ->
 133         let set = S.add (`Obj (string_of_uri uri, pos)) set in
 134         List.fold_left
 135           (fun set (_, term) -> aux (next_pos pos) set term)
 136           set subst
 137     | Cic.MutInd (uri, typeno, subst) ->
 138         let uri = UriManager.string_of_uriref (uri, [typeno]) in
 139         let set = S.add (`Obj (uri, pos)) set in
 140         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
 141           set subst
 142     | Cic.MutConstruct (uri, typeno, consno, subst) ->
 143         let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
 144         let set = S.add (`Obj (uri, pos)) set in
 145         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
 146           set subst
 147     | Cic.MutCase (uri, _, outtype, term, pats) ->
 148         let pos = next_pos pos in
 149         let set = aux pos set term in
 150         let set = aux pos set outtype in
 151         List.fold_left (fun set term -> aux pos set term) set pats
 152     | Cic.Fix (_, funs) ->
 153         let pos = next_pos pos in
 154         List.fold_left
 155           (fun set (_, _, ty, body) ->
 156             let set = aux pos set ty in
 157             aux pos set body)
 158           set funs
 159     | Cic.CoFix (_, funs) ->
 160         let pos = next_pos pos in
 161         List.fold_left
 162           (fun set (_, ty, body) ->
 163             let set = aux pos set ty in
 164             aux pos set body)
 165           set funs
 166   in
 167   aux pos S.empty term
 168
 169 module OrderedInt =
 170 struct
 171   type t = int
 172   let compare = Pervasives.compare
 173 end
 174
 175 module IntSet = Set.Make (OrderedInt)
 176
 177 let compute_metas term =
 178   let rec aux in_hyp ((concl_metas, hyp_metas) as acc) cic =
 179     match cic with
 180     | Cic.Rel _
 181     | Cic.Sort _
 182     | Cic.Var _ -> acc
 183     | Cic.Meta (no, local_context) ->
 184         let acc =
 185           if in_hyp then
 186             (concl_metas, IntSet.add no hyp_metas)
 187           else
 188             (IntSet.add no concl_metas, hyp_metas)
 189         in
 190         List.fold_left
 191           (fun set context ->
 192             match context with
 193             | None -> set
 194             | Some term -> aux in_hyp set term)
 195           acc
 196           local_context
 197     | Cic.Implicit _ -> assert false
 198     | Cic.Cast (term, ty) ->
 199         (* TODO consider also ty? *)
 200         aux in_hyp acc term
 201     | Cic.Prod (_, source, target) ->
 202         if in_hyp then
 203           let acc = aux in_hyp acc source in
 204           aux in_hyp acc target
 205         else
 206           let acc = aux true acc source in
 207           aux in_hyp acc target
 208     | Cic.Lambda (_, source, target) ->
 209         let acc = aux in_hyp acc source in
 210         aux in_hyp acc target
 211     | Cic.LetIn (_, term, target) ->
 212         aux in_hyp acc (CicSubstitution.subst term target)
 213     | Cic.Appl [] -> assert false
 214     | Cic.Appl (hd :: tl) ->
 215         let acc = aux in_hyp acc hd in
 216         List.fold_left (fun acc term -> aux in_hyp acc term) acc tl
 217     | Cic.Const (_, subst)
 218     | Cic.MutInd (_, _, subst)
 219     | Cic.MutConstruct (_, _, _, subst) ->
 220         List.fold_left (fun acc (_, term) -> aux in_hyp acc term) acc subst
 221     | Cic.MutCase (uri, _, outtype, term, pats) ->
 222         let acc = aux in_hyp acc term in
 223         let acc = aux in_hyp acc outtype in
 224         List.fold_left (fun acc term -> aux in_hyp acc term) acc pats
 225     | Cic.Fix (_, funs) ->
 226         List.fold_left
 227           (fun acc (_, _, ty, body) ->
 228             let acc = aux in_hyp acc ty in
 229             aux in_hyp acc body)
 230           acc funs
 231     | Cic.CoFix (_, funs) ->
 232         List.fold_left
 233           (fun acc (_, ty, body) ->
 234             let acc = aux in_hyp acc ty in
 235             aux in_hyp acc body)
 236           acc funs
 237   in
 238   aux false (IntSet.empty, IntSet.empty) term
 239
 240   (** type of inductiveType *)
 241 let compute_type pos uri typeno (name, _, ty, constructors) =
 242   let consno = ref 0 in
 243   let type_metadata =
 244     (UriManager.string_of_uriref (uri, [typeno]), name,
 245     S.elements (compute_term pos ty))
 246   in
 247   let constructors_metadata =
 248     List.map
 249       (fun (name, term) ->
 250         incr consno;
 251         let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
 252         (uri, name, S.elements
 253                       (compute_term pos term)))
 254       constructors
 255   in
 256   type_metadata :: constructors_metadata
 257
 258 let compute_ind pos ~uri ~types =
 259   let idx = ref ~-1 in
 260   List.concat
 261     (List.map
 262       (fun ty -> incr idx; compute_type pos uri !idx ty) types)
 263
 264 let compute (pos:position) ~body ~ty =
 265   let type_metadata = compute_term pos ty in
 266   let body_metadata =
 267     match body with
 268     | None -> S.empty
 269     | Some body -> compute_term `InBody body
 270   in
 271   let uris =
 272     S.fold
 273       (fun metadata uris ->
 274         match metadata with
 275         | `Obj (uri, _) -> StringSet.add uri uris
 276         | _ -> uris)
 277       type_metadata StringSet.empty
 278   in
 279   S.elements
 280     (S.union
 281       (S.filter
 282         (function
 283           | `Obj (uri, _) when StringSet.mem uri uris -> false
 284           | _ -> true)
 285         body_metadata)
 286       type_metadata)
 287
 288 let compute_term start_pos term = S.elements (compute_term start_pos term)
 289
 290 let depth_offset params =
 291   let non p x = not (p x) in
 292   List.length (List.filter (non var_has_body) params)
 293
 294 let rec compute_var pos uri =
 295   let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 296   match o with
 297     | Cic.Variable (_, Some body, ty, params, _) -> []
 298     | Cic.Variable (_, None, ty, params, _) ->
 299         let metadata_of_vars =
 300           List.flatten
 301             (List.map (compute_var (next_pos pos)) params) in
 302         (match pos with
 303            | `MainHypothesis (Some 0) ->
 304                let pos = `MainHypothesis (Some (depth_offset params)) in
 305                  (compute pos ~body:None ~ty)@metadata_of_vars
 306            | `InHypothesis ->
 307                 (compute pos ~body:None ~ty)@metadata_of_vars
 308            | _ -> assert false)
 309     | _ -> assert false
 310
 311 let compute_obj uri =
 312   let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 313   match o with
 314   | Cic.Variable (_, body, ty, params, _)
 315   | Cic.Constant (_, body, ty, params, _) ->
 316       let pos = `MainConclusion (Some (depth_offset params)) in
 317       let metadata = compute pos ~body ~ty
 318       in
 319       let metadata_of_vars =
 320         List.flatten
 321           (List.map (compute_var (`MainHypothesis (Some 0))) params)
 322       in
 323       [UriManager.string_of_uri uri,
 324          UriManager.name_of_uri uri,metadata @ metadata_of_vars]
 325   | Cic.InductiveDefinition (types, params, _, _) ->
 326       let pos = `MainConclusion(Some (depth_offset params)) in
 327       let metadata_of_vars =
 328         List.flatten
 329           (List.map (compute_var (`MainHypothesis (Some 0))) params) in
 330       let metadata = compute_ind pos ~uri ~types in
 331         List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata
 332   | Cic.CurrentProof _ -> assert false
 333
 334
 335 let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty