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