let compute_term pos term =
let rec aux (pos: position) set = function
- | Cic.Rel _ ->
+ | 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 ->
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)
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))
+ S.elements (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)))
+ (uri, name, S.elements
+ (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.concat
+ (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
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 (_, body, 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
+ | `InHypothesis ->
+ (compute pos ~body ~ty)@metadata_of_vars
+ | _ -> 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 (List.length params)) in
+ let metadata = compute pos ~body ~ty
+ in
+ let metadata_of_vars =
+ List.flatten
+ (List.map (compute_var (`MainHypothesis (Some 0))) params)
+ in
+ [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 metadata_of_vars =
+ List.flatten
+ (List.map (compute_var (`MainHypothesis (Some 0))) params) in
+ let metadata = compute_ind pos ~uri ~types in
+ List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata
+ | Cic.CurrentProof _ -> assert false
+
+
+let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty