X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=50407ac7c923d7ff94116fe5aa98976e38f3f6f5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=784de4db63853cc469e8416234b7991b46a4d30f;hpb=20054808327ccec9d018b8cc54b31ccb44724f49;p=helm.git diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index 784de4db6..50407ac7c 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -56,25 +56,33 @@ module OrderedMetadata = end module MetadataSet = Set.Make (OrderedMetadata) -module StringSet = Set.Make (String) +module UriManagerSet = UriManager.UriSet 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) @@ -122,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 @@ -229,28 +237,28 @@ 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)) + (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 (`MainConclusion (Some 0)) 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 ~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.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 @@ -260,18 +268,81 @@ let compute ~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) + 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 + List.length (List.filter (non var_has_body) params) -let compute_term start_pos term = S.elements (compute_term start_pos term) +let rec compute_var pos uri = + let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + | Cic.Variable (_, Some _, _, _, _) -> S.empty + | Cic.Variable (_, None, ty, params, _) -> + 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 + let ty_metadata = compute_term pos ty in + S.union ty_metadata var_metadata + | `InHypothesis -> + let ty_metadata = compute_term pos ty in + S.union ty_metadata var_metadata + | _ -> 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 var_metadata = + List.fold_left + (fun metadata uri -> + S.union metadata (compute_var (`MainHypothesis (Some (Eq 0))) uri)) + S.empty + params + in + [ 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 = compute_ind pos ~uri ~types in + 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)