Added count_occurrences.

Type of does_not_occur corrected.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index c57055365dc72def70dcbfd3683e63f32f6d52ca..a0c9272845e9fbd29d58d29e5104a8db5796a556 100644 (file)
--- 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 524a00cd35f73cdd4477b8e3191f30ceff7bca31..b110d0651adff6d6afd61978a43d8589fe1f6900 100644 (file)
--- 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 cb0b54b82ef18e72451b275c3e7912989e46cbb7..01c522ba0a557eb496c70ed1433331e4a2c025f4 100644 (file)
--- 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