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