From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 17 Sep 2004 12:49:43 +0000 (+0000)
Subject: meta_closed added
X-Git-Tag: moogle_mathql~2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d6e620f90542cc84eb7a1c8ae0127871fbea93f9;p=helm.git

meta_closed added
---

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index ad01110c4..29b03a07e 100644
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -102,3 +102,42 @@ let is_closed =
 in 
  is_closed 0
 ;;
+
+(* CPS iterators on Cic.term ************************************************)
+
+let rec visit_l visit_t map f r = function
+   | []        -> f r
+   | h :: tail -> 
+      let f r = visit_l visit_t map f r tail in 
+      visit_t f r (map h) 
+
+let meta_closed t =
+   let rec visit_t f r = function
+      | Cic.Meta _                     -> raise Exit
+      | Cic.Implicit _
+      | Cic.Sort _      
+      | Cic.Rel _                      -> f r 
+      | Cic.Cast (t, u) 
+      | Cic.Prod (_, t, u) 
+      | Cic.Lambda (_, t, u) 
+      | Cic.LetIn (_, t, u)            -> 
+         let f r = visit_t f r u in visit_t f r t 
+      | Cic.Appl tl                    -> 
+         visit_l visit_t (fun x -> x) f r tl 
+      | Cic.Fix (_, tl)                ->  
+         let f r = visit_l visit_t (fun (_, _, _, u) -> u) f r tl in
+         visit_l visit_t (fun (_, _, t, _) -> t) f r tl
+      | Cic.CoFix (_, tl)              -> 
+         let f r = visit_l visit_t (fun (_, _, u) -> u) f r tl in
+         visit_l visit_t (fun (_, t, _) -> t) f r tl
+      | Cic.Var (k, tl)
+      | Cic.Const (k, tl)             
+      | Cic.MutInd (k, _, tl) 
+      | Cic.MutConstruct (k, _, _, tl) -> 
+         visit_l visit_t (fun (_, u) -> u) f r tl
+      | Cic.MutCase (_, _, t, u, tl)   -> 
+         let f r = visit_l visit_t (fun u -> u) f r tl in
+         let f r = visit_t f r u in
+         visit_t f r t
+   in	  
+   try visit_t (fun x -> x) () t; false with Exit -> true
diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index c03783b86..24383061c 100644
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -35,3 +35,4 @@ val clean_up_local_context :
 
 val is_closed : Cic.term -> bool
 
+val meta_closed : Cic.term -> bool