eliminiation des singletons du genre sig + divers

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

5 files changed, 35 insertions, 9 deletions

diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 827a62c2d6..2680724a3d 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -1,14 +1,8 @@
 
- 2. Inductifs singletons
-
- 3. Axiomes : vérifier les flexibles sortant d'une constante
-
  4. Cofix : seulement en Haskell
 
  5. Syntaxe Haskell
 
- 6. Renommage des var de type caml
-
  7. Eta expansion pour contourner typage Caml
 
-
+ 8. Synchroniser Reset & les tables 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 5a06982bf7..6936f24707 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -65,6 +65,7 @@ let rec ast_map f = function
 
 and ast_map_eqn f (c,ids,a) = (c,ids,f a)
 
+
 (*s Lifting on terms.
     [ml_lift k t] lifts the binding depth of [t] across [k] bindings. 
     We use a generalization [ml_lift k n t] lifting the vars
@@ -140,6 +141,26 @@ let nb_occur a =
   in 
   count 1 a; !cpt
 
+(* elimination of inductive type with one constructor expecting
+   one argument (such as [Exist]) *)
+
+let rec elim_singleton_ast rl = function 
+  | MLcase (t, [|r,[a],t'|]) when (List.mem r rl) 
+      -> MLletin (a,elim_singleton_ast rl t,elim_singleton_ast rl t')   
+  | MLcons (r, n, [t]) when (List.mem r rl) 
+      -> elim_singleton_ast rl t
+  | t -> ast_map (elim_singleton_ast rl) t
+
+let elim_singleton = 
+  let rec elim_rec rl = function 
+    | [] -> [] 
+    | Dtype [il, ir, [cr,[t]]] :: dl -> 
+	Dabbrev (ir, il, t) :: (elim_rec (cr::rl) dl) 
+    | Dglob (r, a) :: dl -> 
+	Dglob (r, elim_singleton_ast rl a)  :: (elim_rec rl dl)
+    | d:: dl ->	d :: (elim_rec rl dl)
+  in elim_rec []
+
 (*s Beta-reduction *)
 
 let rec betared_ast = function
@@ -258,7 +279,10 @@ let rec optimize prm = function
       if expand prm r t' then begin
 	warning_expansion r;
 	let l' = List.map (subst_glob_decl r t') l in
-        optimize prm l'
+	if prm.modular then 
+	  (Dglob (r,t')) :: (optimize prm l')
+	else
+	  optimize prm l'
       end else 
 	(Dglob(r,t')) :: (optimize prm l)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 768695e0a8..7305a44f31 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -33,6 +33,11 @@ val ml_lift : int -> ml_ast -> ml_ast
 
 val ml_subst : ml_ast -> ml_ast -> ml_ast
 
+(* Simplification of singleton inductive types: one contructor
+   with one argument is isomorphic to identity *)
+
+val elim_singleton : ml_decl list -> ml_decl list
+
 (*s Some transformations of ML terms. [betared_ast] and [betared_ecl] reduce
     all beta redexes (when the argument does not occur, it is just
     thrown away; when it occurs exactly once it is substituted; otherwise
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 2d0518d92a..5562e4e67d 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -439,6 +439,9 @@ let ocaml_preamble () =
      'sTR "let arity = ()"; 'fNL; 'fNL >]
 
 let extract_to_file f prm decls =
+  let decls = List.map 
+		(fun d -> betared_decl (uncurrify_decl d)) decls in
+  let decls = elim_singleton decls in 
   let decls = optimize prm decls in
   let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in
   let cout = open_out f in
diff --git a/contrib/extraction/test/bench b/contrib/extraction/test/bench
index 8b29f5f155..bff9bd77a5 100755
--- a/contrib/extraction/test/bench
+++ b/contrib/extraction/test/bench
@@ -1,5 +1,5 @@
 #!/bin/sh
-../../../bin/coqtop.byte -batch -load-vernac-source ../Extraction.v -load-vernac-source ./bench.v
+../../../bin/coqtop.byte -batch -load-vernac-source ./bench.v
 ocamlc -c -i polylist.ml
 ocamlc -c -i zarith.ml
 ocamlc -c -i even.ml