diff options
| -rw-r--r-- | contrib/extraction/mlutil.ml | 23 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.mli | 4 |
2 files changed, 27 insertions, 0 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml new file mode 100644 index 0000000000..33c1e32bfe --- /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 0000000000..224236fecf --- /dev/null +++ b/contrib/extraction/mlutil.mli @@ -0,0 +1,4 @@ + +open Miniml + +val occurs : int -> ml_ast -> bool |