handling of variables with body

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index fdb1114fabdcb6e1a34639ffe21805ff9422bd7f..0ffe5980d183cd7ad8a4d8807c2b3adb5d0a55eb 100644 (file)
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -67,9 +67,17 @@ let incr_depth = function
   | `MainHypothesis (Some depth) -> `MainHypothesis (Some (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
@@ -279,19 +287,24 @@ let compute (pos:position) ~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 (_, body, ty, params, _) ->
+    | 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 0) -> 
-              let pos = `MainHypothesis(Some (List.length params)) in
-                (compute pos ~body ~ty)@metadata_of_vars
+              let pos = `MainHypothesis (Some (depth_offset params)) in
+                (compute pos ~body:None ~ty)@metadata_of_vars
           | `InHypothesis ->
-               (compute pos ~body ~ty)@metadata_of_vars
+               (compute pos ~body:None ~ty)@metadata_of_vars
           | _ -> assert false)
     | _ -> assert false 
 
@@ -300,7 +313,7 @@ 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 pos = `MainConclusion (Some (depth_offset params)) in
       let metadata = compute pos ~body ~ty
       in
       let metadata_of_vars = 
@@ -310,7 +323,7 @@ let compute_obj uri =
       [UriManager.string_of_uri uri, 
          UriManager.name_of_uri uri,metadata @ metadata_of_vars]
   | Cic.InductiveDefinition (types, params, _, _) ->
-      let pos = `MainConclusion(Some (List.length params)) in
+      let pos = `MainConclusion(Some (depth_offset params)) in
       let metadata_of_vars = 
         List.flatten 
           (List.map (compute_var (`MainHypothesis (Some 0))) params) in