From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 9 Feb 2004 16:37:16 +0000 (+0000)
Subject: Added is_closed.
X-Git-Tag: V_0_3_0~48
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a6b369829925668130b977a0abd737bf34ae74ba;p=helm.git

Added is_closed.
---

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index a8195a311..fb40ad3ba 100644
--- 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 a2548f933..7db463b7d 100644
--- 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