From: Claudio Sacerdoti Coen 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