X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=50407ac7c923d7ff94116fe5aa98976e38f3f6f5;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=d06e9a4bf5197b0da61bc34efe335e984222bfc3;hpb=9cd69dd86ed337478461241d497265ccc59f819a;p=helm.git diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index d06e9a4bf..50407ac7c 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -56,31 +56,39 @@ 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 -> match context with | None -> set - | Some term -> aux pos set term) + | Some term -> aux (next_pos pos) set term) set local_context | Cic.Sort sort -> @@ -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 @@ -158,28 +166,99 @@ let compute_term pos term = in aux pos S.empty term -let compute_type uri typeno (name, _, ty, constructors) = +module OrderedInt = +struct + type t = int + let compare = Pervasives.compare +end + +module IntSet = Set.Make (OrderedInt) + +let compute_metas term = + let rec aux in_hyp ((concl_metas, hyp_metas) as acc) cic = + match cic with + | Cic.Rel _ + | Cic.Sort _ + | Cic.Var _ -> acc + | Cic.Meta (no, local_context) -> + let acc = + if in_hyp then + (concl_metas, IntSet.add no hyp_metas) + else + (IntSet.add no concl_metas, hyp_metas) + in + List.fold_left + (fun set context -> + match context with + | None -> set + | Some term -> aux in_hyp set term) + acc + local_context + | Cic.Implicit _ -> assert false + | Cic.Cast (term, ty) -> + (* TODO consider also ty? *) + aux in_hyp acc term + | Cic.Prod (_, source, target) -> + if in_hyp then + let acc = aux in_hyp acc source in + aux in_hyp acc target + else + let acc = aux true acc source in + aux in_hyp acc target + | Cic.Lambda (_, source, target) -> + let acc = aux in_hyp acc source in + aux in_hyp acc target + | Cic.LetIn (_, term, target) -> + aux in_hyp acc (CicSubstitution.subst term target) + | Cic.Appl [] -> assert false + | Cic.Appl (hd :: tl) -> + let acc = aux in_hyp acc hd in + List.fold_left (fun acc term -> aux in_hyp acc term) acc tl + | Cic.Const (_, subst) + | Cic.MutInd (_, _, subst) + | Cic.MutConstruct (_, _, _, subst) -> + List.fold_left (fun acc (_, term) -> aux in_hyp acc term) acc subst + | Cic.MutCase (uri, _, outtype, term, pats) -> + let acc = aux in_hyp acc term in + let acc = aux in_hyp acc outtype in + List.fold_left (fun acc term -> aux in_hyp acc term) acc pats + | Cic.Fix (_, funs) -> + List.fold_left + (fun acc (_, _, ty, body) -> + let acc = aux in_hyp acc ty in + aux in_hyp acc body) + acc funs + | Cic.CoFix (_, funs) -> + List.fold_left + (fun acc (_, ty, body) -> + let acc = aux in_hyp acc ty in + aux in_hyp acc body) + acc funs + in + aux false (IntSet.empty, IntSet.empty) term + + (** 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 @@ -189,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) - -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 + 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 (_, 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)