meta_closed added

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index ad01110c403f8b178ab91ddb7cdea3953d9b067e..29b03a07ea130a687d097e9d6a4d9228ef26c95c 100644 (file)
--- 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 c03783b86419eeed18ff52f6a2333641df4ff874..24383061caa120b0b01ffa146497b8aa858afde8 100644 (file)
--- 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