X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=50407ac7c923d7ff94116fe5aa98976e38f3f6f5;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=f9a26637d968db9c4e7cc3129d7f1223af035e55;hpb=e6023677f34f426d32a1bdbe391978ea7f7c44f6;p=helm.git diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index f9a26637d..50407ac7c 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -56,7 +56,7 @@ module OrderedMetadata = end module MetadataSet = Set.Make (OrderedMetadata) -module StringSet = Set.Make (String) +module UriManagerSet = UriManager.UriSet module S = MetadataSet @@ -130,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 @@ -241,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 @@ -272,20 +268,17 @@ 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) - -let compute_term start_pos term = S.elements (compute_term start_pos term) + S.union + (S.filter + (function + | `Obj (uri, _) when UriManagerSet.mem uri uris -> false + | _ -> true) + body_metadata) + type_metadata let depth_offset params = let non p x = not (p x) in @@ -294,17 +287,23 @@ let depth_offset 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 (_, Some _, _, _, _) -> S.empty | Cic.Variable (_, None, ty, params, _) -> - let metadata_of_vars = - List.flatten - (List.map (compute_var (next_pos pos)) params) in + 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 (Eq 0)) -> let pos = `MainHypothesis (Some (Eq (depth_offset params))) in - (compute pos ~body:None ~ty)@metadata_of_vars + let ty_metadata = compute_term pos ty in + S.union ty_metadata var_metadata | `InHypothesis -> - (compute pos ~body:None ~ty)@metadata_of_vars + let ty_metadata = compute_term pos ty in + S.union ty_metadata var_metadata | _ -> assert false) | _ -> assert false @@ -314,22 +313,36 @@ let compute_obj uri = | 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) + 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 (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 + 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 (Eq 0))) ~body ~ty