X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=50407ac7c923d7ff94116fe5aa98976e38f3f6f5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=fdb1114fabdcb6e1a34639ffe21805ff9422bd7f;hpb=26c3b57c2142bfd2242571109374c3203c7980dd;p=helm.git

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index fdb1114fa..50407ac7c 100644
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -56,20 +56,28 @@ module OrderedMetadata =
   end
 
 module MetadataSet = Set.Make (OrderedMetadata)
-module StringSet = Set.Make (String)
+module UriManagerSet = UriManager.UriSet
 
 module S = MetadataSet
 
 let unopt = function Some x -> x | None -> assert false
 
 let incr_depth = function
-  | `MainConclusion (Some depth) -> `MainConclusion (Some (depth + 1))
-  | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1))
+  | `MainConclusion (Some (Eq depth)) -> `MainConclusion (Some (Eq (depth + 1)))
+  | `MainHypothesis (Some (Eq depth)) -> `MainHypothesis (Some (Eq (depth + 1)))
   | _ -> assert false
 
+let var_has_body uri =
+  match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+  | Cic.Variable (_, Some body, _, _, _), _ -> true
+  | _ -> false
+
 let compute_term pos term =
   let rec aux (pos: position) set = function
-    | Cic.Rel _ 
+    | Cic.Var (uri, subst) when var_has_body uri ->
+        (* handles variables with body as constants *)
+        aux pos set (Cic.Const (uri, subst))
+    | Cic.Rel _
     | Cic.Var _ ->
         if is_main_pos pos then
           S.add (`Rel (main_pos pos)) set
@@ -95,7 +103,7 @@ let compute_term pos term =
     | Cic.Prod (_, source, target) ->
         (match pos with
         | `MainConclusion _ ->
-            let set = aux (`MainHypothesis (Some 0)) set source in
+            let set = aux (`MainHypothesis (Some (Eq 0))) set source in
             aux (incr_depth pos) set target
         | `MainHypothesis _ ->
             let set = aux `InHypothesis set source in
@@ -122,17 +130,17 @@ let compute_term pos term =
           (fun set term -> aux (next_pos pos) set term)
           set tl
     | Cic.Const (uri, subst) ->
-        let set = S.add (`Obj (string_of_uri uri, pos)) set in
+        let set = S.add (`Obj (uri, pos)) set in
         List.fold_left
           (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutInd (uri, typeno, subst) ->
-        let uri = UriManager.string_of_uriref (uri, [typeno]) in
+        let uri = UriManager.uri_of_uriref uri typeno None in
         let set = S.add (`Obj (uri, pos)) set in
         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutConstruct (uri, typeno, consno, subst) ->
-        let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
+        let uri = UriManager.uri_of_uriref uri typeno (Some consno) in
         let set = S.add (`Obj (uri, pos)) set in
         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
@@ -233,25 +241,21 @@ let compute_metas term =
 let compute_type pos uri typeno (name, _, ty, constructors) =
   let consno = ref 0 in
   let type_metadata =
-    (UriManager.string_of_uriref (uri, [typeno]), name,
-    S.elements (compute_term pos ty))
+    (UriManager.uri_of_uriref uri typeno None, name, (compute_term pos ty))
   in
   let constructors_metadata =
     List.map
       (fun (name, term) ->
         incr consno;
-        let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
-        (uri, name, S.elements 
-                      (compute_term pos term)))
+        let uri = UriManager.uri_of_uriref uri typeno (Some !consno) in
+        (uri, name, (compute_term pos term)))
       constructors
   in
   type_metadata :: constructors_metadata
 
 let compute_ind pos ~uri ~types =
   let idx = ref ~-1 in
-  List.concat 
-    (List.map 
-      (fun ty -> incr idx; compute_type pos uri !idx ty) types)
+  List.map (fun ty -> incr idx; compute_type pos uri !idx ty) types
 
 let compute (pos:position) ~body ~ty = 
   let type_metadata = compute_term pos ty in
@@ -264,34 +268,42 @@ let compute (pos:position) ~body ~ty =
     S.fold
       (fun metadata uris ->
         match metadata with
-        | `Obj (uri, _) -> StringSet.add uri uris
+        | `Obj (uri, _) -> UriManagerSet.add uri uris
         | _ -> uris)
-      type_metadata StringSet.empty
+      type_metadata UriManagerSet.empty
   in
-  S.elements 
-    (S.union
-      (S.filter
-        (function
-          | `Obj (uri, _) when StringSet.mem uri uris -> false
-          | _ -> true)
-        body_metadata)
-      type_metadata)
+  S.union
+    (S.filter
+      (function
+        | `Obj (uri, _) when UriManagerSet.mem uri uris -> false
+        | _ -> true)
+      body_metadata)
+    type_metadata
 
-let compute_term start_pos term = S.elements (compute_term start_pos term)
+let depth_offset params =
+  let non p x = not (p x) in
+  List.length (List.filter (non var_has_body) params)
 
 let rec compute_var pos uri =
   let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   match o with
-    | Cic.Variable (_, body, ty, params, _) ->
-	let metadata_of_vars = 
-          List.flatten 
-            (List.map (compute_var (next_pos pos)) params) in 
+    | Cic.Variable (_, Some _, _, _, _) -> S.empty
+    | Cic.Variable (_, None, ty, params, _) ->
+	let var_metadata = 
+          List.fold_left
+            (fun metadata uri ->
+              S.union metadata (compute_var (next_pos pos) uri))
+            S.empty
+            params
+        in
 	(match pos with
-	   | `MainHypothesis (Some 0) -> 
-	       let pos = `MainHypothesis(Some (List.length params)) in
-		 (compute pos ~body ~ty)@metadata_of_vars
+	   | `MainHypothesis (Some (Eq 0)) -> 
+	       let pos = `MainHypothesis (Some (Eq (depth_offset params))) in
+               let ty_metadata = compute_term pos ty in
+               S.union ty_metadata var_metadata
 	   | `InHypothesis ->
-	        (compute pos ~body ~ty)@metadata_of_vars
+               let ty_metadata = compute_term pos ty in
+               S.union ty_metadata var_metadata
 	   | _ -> assert false)
     | _ -> assert false 
 
@@ -300,23 +312,37 @@ let compute_obj uri =
   match o with
   | Cic.Variable (_, body, ty, params, _)
   | Cic.Constant (_, body, ty, params, _) -> 
-      let pos = `MainConclusion(Some (List.length params)) in
-      let metadata = compute pos ~body ~ty
-      in
-      let metadata_of_vars = 
-        List.flatten 
-          (List.map (compute_var (`MainHypothesis (Some 0))) params) 
+      let pos = `MainConclusion (Some (Eq (depth_offset params))) in
+      let metadata = compute pos ~body ~ty in
+      let var_metadata = 
+        List.fold_left
+          (fun metadata uri ->
+            S.union metadata (compute_var (`MainHypothesis (Some (Eq 0))) uri))
+          S.empty
+          params
       in
-      [UriManager.string_of_uri uri, 
-         UriManager.name_of_uri uri,metadata @ metadata_of_vars]
+      [ uri, 
+        UriManager.name_of_uri uri,
+        S.union metadata var_metadata ]
   | Cic.InductiveDefinition (types, params, _, _) ->
-      let pos = `MainConclusion(Some (List.length params)) in
-      let metadata_of_vars = 
-        List.flatten 
-          (List.map (compute_var (`MainHypothesis (Some 0))) params) in
+      let pos = `MainConclusion(Some (Eq (depth_offset params))) in
       let metadata = compute_ind pos ~uri ~types in
-	List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata
+      let var_metadata = 
+        List.fold_left
+          (fun metadata uri ->
+            S.union metadata (compute_var (`MainHypothesis (Some (Eq 0))) uri))
+          S.empty params
+      in
+      List.fold_left
+        (fun acc m -> 
+          (List.map (fun (uri,name,md) -> (uri,name,S.union md var_metadata)) m)
+          @ acc)
+        [] metadata
   | Cic.CurrentProof _ -> assert false    
 
+let compute_obj uri = 
+  List.map (fun (u, n, md) -> (u, n, S.elements md)) (compute_obj uri)
+  
+let compute ~body ~ty =
+  S.elements (compute (`MainConclusion (Some (Eq 0))) ~body ~ty)
 
-let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty