added filtering criteria on differences between number of constants in

[helm.git] / helm / ocaml / metadata / metadataExtractor.ml

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index 8db0d74f5e47ef15b808025f14388981ec10924a..784de4db63853cc469e8416234b7991b46a4d30f 100644 (file)
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -158,6 +158,77 @@ let compute_term pos term =
   in
   aux pos S.empty term
 
+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
+
 let compute_type uri typeno (name, _, ty, constructors) =
   let consno = ref 0 in
   let type_metadata =