From 71215a7e5b10535b538776680dce5dc02e118c2f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 12 May 2005 09:01:45 +0000 Subject: [PATCH] handling of variables with body --- helm/ocaml/metadata/metadataExtractor.ml | 27 ++++++++++++++++++------ 1 file changed, 20 insertions(+), 7 deletions(-) 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 -- 2.39.2