From 2da35c1dc1aff5f852886ac64d641774f2f187cf Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 4 Feb 2010 11:23:52 +0000
Subject: [PATCH] Added count_occurrences. Type of does_not_occur corrected.

---
 .../components/ng_kernel/nCicTypeChecker.mli  |  3 +--
 .../components/ng_kernel/nCicUntrusted.ml     | 25 +++++++++++++++++++
 .../components/ng_kernel/nCicUntrusted.mli    |  3 +++
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index c57055365..a0c927284 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -61,5 +61,4 @@ val are_all_occurrences_positive:
   NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool
 
 val does_not_occur :
-    subst:NCic.substitution ->
-    ('a * NCic.context_entry) list -> int -> int -> NCic.term -> bool
+    subst:NCic.substitution -> NCic.context -> int -> int -> NCic.term -> bool
diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 524a00cd3..b110d0651 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -312,3 +312,28 @@ let relations_of_menv subst m c =
 let sort_metasenv subst (m : NCic.metasenv) =
   (MS.topological_sort m (relations_of_menv subst m) : NCic.metasenv)
 ;;
+
+let count_occurrences ~subst context n t = 
+  let occurrences = ref 0 in
+  let rec aux k _ = function
+    | C.Rel m when m = n+k -> incr occurrences
+    | C.Rel m ->
+        (try match List.nth context (m-1-k) with
+          | _,C.Def (bo,_) -> aux (n-m) () bo
+          | _ -> ()
+         with Failure _ -> assert false)
+    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
+    | C.Meta (mno,(s,l)) ->
+         (try
+            (* possible optimization here: try does_not_occur on l and
+               perform substitution only if DoesOccur is raised *)
+            let _,_,term,_ = NCicUtils.lookup_subst mno subst in
+            aux (k-s) () (NCicSubstitution.subst_meta (0,l) term)
+          with NCicUtils.Subst_not_found _ -> () (*match l with
+          | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
+          | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
+    | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
+  in
+   aux 0 () t;
+   !occurrences
+;;
diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index cb0b54b82..01c522ba0 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -40,3 +40,6 @@ val apply_subst : NCic.substitution -> NCic.context -> NCic.term -> NCic.term
 val apply_subst_context : fix_projections:bool -> 
   NCic.substitution -> NCic.context -> NCic.context
 val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv
+
+val count_occurrences :
+    subst:NCic.substitution -> NCic.context -> int -> NCic.term -> int
-- 
2.39.2