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 =
| 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
(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
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
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
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 0) ->
- let pos = `MainHypothesis (Some (depth_offset params)) in
- (compute pos ~body:None ~ty)@metadata_of_vars
+ | `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 ->
- (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
match o with
| Cic.Variable (_, body, ty, params, _)
| Cic.Constant (_, body, ty, params, _) ->
- let pos = `MainConclusion (Some (depth_offset params)) in
- let metadata = compute pos ~body ~ty
- in
- let metadata_of_vars =
- List.flatten
- (List.map (compute_var (`MainHypothesis (Some 0))) 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
- [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 (depth_offset params)) in
- let metadata_of_vars =
- List.flatten
- (List.map (compute_var (`MainHypothesis (Some 0))) params) in
+ let pos = `MainConclusion(Some (Eq (depth_offset 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 0)) ~body ~ty
projects / helm.git / blobdiff