mlutil

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1472 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 27 insertions, 0 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
new file mode 100644
index 000000000..33c1e32bf
--- /dev/null
+++ b/contrib/extraction/mlutil.ml
@@ -0,0 +1,23 @@
+
+open Util
+open Miniml
+
+(* [occurs : int -> ml_ast -> bool]
+   [occurs k M] returns true if (Rel k) occurs in M. *)
+
+let rec occurs k = function
+  | MLrel i          -> i=k
+  | MLapp(t,argl)    -> (occurs k t) or (occurs_list k argl)
+  | MLlam(_,t)       -> occurs (k+1) t
+  | MLcons(_,_,argl) -> occurs_list k argl
+  | MLcase(t,pv)     -> 
+      (occurs k t) or
+      (List.exists (fun (k',t') -> occurs (k+k') t')
+      	 (array_map_to_list (fun (_,l,t') -> 
+      	       	           let k' = List.length l in (k',t')) pv))
+  | MLfix(_,_,l,cl)  -> let k' = List.length l in occurs_list (k+k') cl
+  | _                -> false
+
+and occurs_list k l =
+  List.exists (fun t -> occurs k t) l
+
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
new file mode 100644
index 000000000..224236fec
--- /dev/null
+++ b/contrib/extraction/mlutil.mli
@@ -0,0 +1,4 @@
+
+open Miniml
+
+val occurs : int -> ml_ast -> bool