diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-12 09:46:37 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-12 09:46:37 +0000 |
commit | 9e89f4d44bf82f2879573057c319c0376c76a698 (patch) | |
tree | fbf16ce00efe042d793de5819c15b5d3356fcbc9 /contrib/extraction/mlutil.ml | |
parent | e44c3268a30669522422a13c0c8acc485bc8f331 (diff) |
Test & correction de la production de code Haskell
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/mlutil.ml')
-rw-r--r-- | contrib/extraction/mlutil.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 5656a4285..26c88726e 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -28,6 +28,17 @@ exception Impossible let anonymous = id_of_string "x" let prop_name = id_of_string "_" +(*s Get all type variables from a ML type *) + +let get_tvars t = + let rec get_rec s = function + | Tvar i -> Idset.add i s + | Tapp l -> List.fold_left get_rec s l + | Tarr (a,b) -> get_rec (get_rec s a) b + | a -> s + in Idset.elements (get_rec Idset.empty t) + + (*s In an ML type, update the arguments to all inductive types [(sp,_)] *) let rec update_args sp vl = function |