Added is_closed.

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index a8195a311079922607949411fb77add571e8a2cb..fb40ad3ba123d6b28afb1dd1592ecc151016d8e7 100644 (file)
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -30,3 +30,45 @@ let lookup_meta index metasenv =
     List.find (fun (index', _, _) -> index = index') metasenv
   with Not_found -> raise (Meta_not_found index)
 
+let is_closed =
+ let module C = Cic in
+ let rec is_closed k =
+  function
+      C.Rel m when m > k -> false
+    | C.Rel m -> true
+    | C.Meta (_,l) ->
+       List.fold_left
+        (fun i t -> i && (match t with None -> true | Some t -> is_closed k t)
+        ) true l
+    | C.Sort _ -> true
+    | C.Implicit _ -> assert false
+    | C.Cast (te,ty) -> is_closed k te && is_closed k ty
+    | C.Prod (name,so,dest) -> is_closed k so && is_closed (k+1) dest
+    | C.Lambda (_,so,dest) -> is_closed k so && is_closed (k+1) dest
+    | C.LetIn (_,so,dest) -> is_closed k so && is_closed (k+1) dest
+    | C.Appl l ->
+       List.fold_right (fun x i -> i && is_closed k x) l true
+    | C.Var (_,exp_named_subst)
+    | C.Const (_,exp_named_subst)
+    | C.MutInd (_,_,exp_named_subst)
+    | C.MutConstruct (_,_,_,exp_named_subst) ->
+       List.fold_right (fun (_,x) i -> i && is_closed k x)
+        exp_named_subst true
+    | C.MutCase (_,_,out,te,pl) ->
+       is_closed k out && is_closed k te &&
+        List.fold_right (fun x i -> i && is_closed k x) pl true
+    | C.Fix (_,fl) ->
+       let len = List.length fl in
+        let k_plus_len = k + len in
+         List.fold_right
+          (fun (_,_,ty,bo) i -> i && is_closed k ty && is_closed k_plus_len bo
+          ) fl true
+    | C.CoFix (_,fl) ->
+       let len = List.length fl in
+        let k_plus_len = k + len in
+         List.fold_right
+          (fun (_,ty,bo) i -> i && is_closed k ty && is_closed k_plus_len bo
+          ) fl true
+in 
+ is_closed 0
+;;

diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index a2548f933026e528f30413882e1f24e876441ae7..7db463b7d4fe3ea7641cca7f775a96fa1813c985 100644 (file)
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -26,3 +26,4 @@ exception Meta_not_found of int
 
 val lookup_meta: int -> Cic.metasenv -> Cic.conjecture
 
+val is_closed : Cic.term -> bool