X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=f9a26637d968db9c4e7cc3129d7f1223af035e55;hb=de4483296d06aac3df4da10d5401b1f97c4350ab;hp=784de4db63853cc469e8416234b7991b46a4d30f;hpb=20054808327ccec9d018b8cc54b31ccb44724f49;p=helm.git

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index 784de4db6..f9a26637d 100644
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -63,18 +63,26 @@ 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
         else
           set
-    | Cic.Var _ -> set
     | Cic.Meta (_, local_context) ->
         List.fold_left
           (fun set context ->
@@ -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
@@ -106,9 +114,9 @@ let compute_term pos term =
             let set = aux pos set source in
             aux pos set target)
     | Cic.Lambda (_, source, target) ->
-        assert (not (is_main_pos pos));
-        let set = aux pos set source in
-        aux pos set target
+        (*assert (not (is_main_pos pos));*)
+        let set = aux (next_pos pos) set source in
+        aux (next_pos pos) set target
     | Cic.LetIn (_, term, target) ->
         if is_main_pos pos then
           aux pos set (CicSubstitution.subst term target)
@@ -229,28 +237,32 @@ let compute_metas term =
   in
   aux false (IntSet.empty, IntSet.empty) term
 
-let compute_type uri typeno (name, _, ty, constructors) =
+  (** type of inductiveType *)
+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 (`MainConclusion (Some 0)) ty))
+    S.elements (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 (`MainConclusion (Some 0)) term)))
+        (uri, name, S.elements 
+                      (compute_term pos term)))
       constructors
   in
   type_metadata :: constructors_metadata
 
-let compute_ind ~uri ~types =
+let compute_ind pos ~uri ~types =
   let idx = ref ~-1 in
-  List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types)
+  List.concat 
+    (List.map 
+      (fun ty -> incr idx; compute_type pos uri !idx ty) types)
 
-let compute ~body ~ty =
-  let type_metadata = compute_term (`MainConclusion (Some 0)) ty in
+let compute (pos:position) ~body ~ty = 
+  let type_metadata = compute_term pos ty in
   let body_metadata =
     match body with
     | None -> S.empty
@@ -275,3 +287,49 @@ let compute ~body ~ty =
 
 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 (_, Some body, ty, params, _) -> []
+    | Cic.Variable (_, None, ty, params, _) ->
+	let metadata_of_vars = 
+          List.flatten 
+            (List.map (compute_var (next_pos pos)) params) in 
+	(match pos with
+	   | `MainHypothesis (Some (Eq 0)) -> 
+	       let pos = `MainHypothesis (Some (Eq (depth_offset params))) in
+		 (compute pos ~body:None ~ty)@metadata_of_vars
+	   | `InHypothesis ->
+	        (compute pos ~body:None ~ty)@metadata_of_vars
+	   | _ -> assert false)
+    | _ -> assert false 
+
+let compute_obj uri =
+  let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+  match o with
+  | Cic.Variable (_, body, ty, params, _)
+  | Cic.Constant (_, body, ty, params, _) -> 
+      let pos = `MainConclusion (Some (Eq (depth_offset params))) in
+      let metadata = compute pos ~body ~ty
+      in
+      let metadata_of_vars = 
+        List.flatten 
+          (List.map (compute_var (`MainHypothesis (Some (Eq 0)))) params) 
+      in
+      [UriManager.string_of_uri uri, 
+         UriManager.name_of_uri uri,metadata @ metadata_of_vars]
+  | Cic.InductiveDefinition (types, params, _, _) ->
+      let pos = `MainConclusion(Some (Eq (depth_offset params))) in
+      let metadata_of_vars = 
+        List.flatten 
+          (List.map (compute_var (`MainHypothesis (Some (Eq 0)))) params) in
+      let metadata = compute_ind pos ~uri ~types in
+	List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata
+  | Cic.CurrentProof _ -> assert false    
+
+
+let compute ~body ~ty = compute (`MainConclusion (Some (Eq 0))) ~body ~ty