From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 12 May 2005 09:01:45 +0000 (+0000)
Subject: handling of variables with body
X-Git-Tag: single_binding~84
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71215a7e5b10535b538776680dce5dc02e118c2f;p=helm.git

handling of variables with body
---

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index fdb1114fa..0ffe5980d 100644
--- 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