reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_type

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

8 files changed, 59 insertions, 82 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 0d1c70c8b..139f849c8 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -71,8 +71,7 @@ let ast_get_modules m a =
 
 let mltype_get_modules m t = 
   let rec get_rec = function 
-    | Tglob r -> m := Idset.add (short_module r) !m
-    | Tapp l -> List.iter get_rec l
+    | Tglob (r,l) -> m := Idset.add (short_module r) !m; List.iter get_rec l
     | Tarr (a,b) -> get_rec a; get_rec b 
     | _ -> () 
   in get_rec t
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 7e798bef7..206de8a28 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -139,8 +139,7 @@ let rec visit_reference m eenv r =
     
 and visit_type m eenv t =
   let rec visit = function
-    | Tglob r -> visit_reference m eenv r
-    | Tapp l -> List.iter visit l
+    | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l  
     | Tarr (t1,t2) -> visit t1; visit t2
     | Tvar _ | Tdummy | Tunknown -> ()
   in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 9c2fb983b..8b842c5b5 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -200,9 +200,9 @@ let signature_of_sp sp =
 
 (*S Management of type variable contexts. *)
 
-(*s From a signature toward a type variable context (ctx). *)
+(*s From a signature toward a type variable context (db). *)
 
-let ctx_from_sign s = 
+let db_from_sign s = 
   let rec f i = function 
     | [] -> [] 
     | true :: l -> i :: (f (i+1) l)
@@ -212,11 +212,11 @@ let ctx_from_sign s =
 (*s Create a type variable context from indications taken from 
   an inductive type (see just below). *) 
 
-let ctx_from_ind rels n d = 
+let db_from_ind dbmap params_nb length_sign = 
   let rec f i = 
-    if i > n then [] 
+    if i > params_nb then [] 
     else try 
-      Intmap.find (i+d) rels :: (f (i+1))
+      Intmap.find (i+length_sign) dbmap :: (f (i+1))
     with Not_found -> 0 :: (f (i+1))
   in f 1
 
@@ -235,42 +235,42 @@ let parse_ind_args si args =
 
 (*S Extraction of a type. *)
 
-(*s [extract_type env c args ctx] is used to produce an ML type from the 
+(*s [extract_type env db c args] is used to produce an ML type from the 
    coq term [(c args)], which is supposed to be a Coq type. *)
 
-(* [ctx] is a context for translating Coq [Rel] into ML type [Tvar]. *)
+(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-let rec extract_type env c args ctx = 
+let rec extract_type env db c args = 
   match kind_of_term (whd_betaiotazeta c) with
     | Lambda (_,_,d) -> 
 	(match args with 
 	   | [] -> assert false (* otherwise the lambda would be reductible. *)
-	   | a :: args -> extract_type env (subst1 a d) args ctx)
+	   | a :: args -> extract_type env db (subst1 a d) args)
     | Prod (n,t,d) ->
-	let mld = extract_type (push_rel_assum (n,t) env) d [] (0::ctx) in 
+	let mld = extract_type (push_rel_assum (n,t) env) (0::db) d [] in 
 	if mld = Tdummy then Tdummy 
 	else if not (is_default env t) then Tarr (Tdummy, mld)
-	else Tarr (extract_type env t [] ctx, mld)
+	else Tarr (extract_type env db t [], mld)
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
-	extract_type env d (Array.to_list args' @ args) ctx
+	extract_type env db d (Array.to_list args' @ args)
     | Rel n -> 
 	(match lookup_rel n env with
 	   | (_,Some t,_) -> 
-	       extract_type env (lift n t) args ctx
+	       extract_type env db (lift n t) args
 	   | _ -> 
-	       let n' = List.nth ctx (n-1) in 
+	       let n' = List.nth db (n-1) in 
 	       if n' = 0 then Tunknown else Tvar n')
     | Const sp ->
 	let t = constant_type env sp in 
 	(match flag_of_type env t with 
 	   | (Info,Arity) -> 
-	       extract_type_app env (ConstRef sp, type_sign env t) args ctx
+	       extract_type_app env db (ConstRef sp, type_sign env t) args
 	   | (Info,_) -> Tunknown
 	   | (Logic,_) -> Tdummy)
     | Ind spi ->
 	(match extract_inductive spi with 
-	   | Iml (si,_) -> extract_type_app env (IndRef spi,si) args ctx
+	   | Iml (si,_) -> extract_type_app env db (IndRef spi,si) args
 	   | Iprop -> Tdummy)
     | Sort _ -> Tdummy 
     | Case _ | Fix _ | CoFix _ -> Tunknown
@@ -281,52 +281,52 @@ let rec extract_type env c args ctx =
   Precondition: [r] is of type an arity represented by the signature [s], 
   and is completely applied: [List.length args = List.length s]. *)
 		  
-and extract_type_app env (r,s) args ctx =
+and extract_type_app env db (r,s) args =
   let ml_args = 
     List.fold_right 
       (fun (b,c) a -> if b then 
 	 let p = List.length (fst (splay_prod env none (type_of env c))) in
-	 let ctx = iterate (fun l -> 0 :: l) p ctx in
-	 (extract_type_arity env c ctx p) :: a
+	 let db = iterate (fun l -> 0 :: l) p db in
+	 (extract_type_arity env db c p) :: a
        else a)
       (List.combine s args) []
-  in Tapp ((Tglob r) :: ml_args)
+  in Tglob (r,  ml_args)
 
-(*s [extract_type_arity env c ctx p] works on a Coq term [c] whose 
+(*s [extract_type_arity env db c p] works on a Coq term [c] whose 
   type is an arity. It means that [c] is not a Coq type, but will 
   be when applied to sufficiently many arguments ([p] in fact).  
   This function decomposes p lambdas, with eta-expansion if needed. *)
 
-(* [ctx] is a context for translating Coq [Rel] into ML type [Tvar]. *)
+(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-and extract_type_arity env c ctx p = 
-  if p=0 then extract_type env c [] ctx 
+and extract_type_arity env db c p = 
+  if p=0 then extract_type env db c [] 
   else 
     let c = whd_betaiotazeta c in 
     match kind_of_term c with 
       | Lambda (n,t,d) -> 
-	  extract_type_arity (push_rel_assum (n,t) env) d ctx (p-1)
+	  extract_type_arity (push_rel_assum (n,t) env) db d (p-1)
       | _ ->  
 	  let rels = fst (splay_prod env none (type_of env c)) in
 	  let env = push_rels_assum rels env in  
 	  let eta_args = List.rev_map mkRel (interval 1 p) in 
-	  extract_type env (lift p c) eta_args ctx
+	  extract_type env db (lift p c) eta_args
 
 (*s [extract_type_ind] extracts the type of an inductive 
   constructor toward the corresponding list of ML types. *)
 
-(* [p] is the number of product in [c] and [ctx] is a context for 
-  translating Coq [Rel] into ML type [Tvar] and [db] is a translation 
+(* [p] is the number of product in [c] and [db] is a context for 
+  translating Coq [Rel] into ML type [Tvar] and [dbmap] is a translation 
   map (produced by a call to [parse_in_args]). *)
 
-and extract_type_ind env c ctx db p = 
+and extract_type_ind env db dbmap c p = 
   match kind_of_term (whd_betadeltaiota env none c) with 
     | Prod (n,t,d) -> 
 	let env' = push_rel_assum (n,t) env in
-	let ctx' = (try Intmap.find p db with Not_found -> 0) :: ctx in
-	let l = extract_type_ind env' d ctx' db (p-1) in 
+	let db' = (try Intmap.find p dbmap with Not_found -> 0) :: db in
+	let l = extract_type_ind env' db' dbmap d (p-1) in 
 	if is_default env t then
-	  let mlt = extract_type env t [] ctx in 
+	  let mlt = extract_type env db t [] in 
 	  if mlt = Tdummy then l else mlt :: l 
 	else l 
     | _ -> [] 
@@ -378,16 +378,13 @@ and extract_mib sp =
 	      let t = snd (decompose_prod_n params_nb t) in
 	      let s = term_sign params_env t in
 	      let n = List.length s in 
-	      let db,ctx = 
-		if si=[] then Intmap.empty,[]
-		else match find_conclusion params_env none t with 
-		  | App (f, args) -> 
-		      (*i assert (kind_of_term f = Ind ip); i*)
-		      let db = parse_ind_args si args in 
-		      db, ctx_from_ind db params_nb n 
-		  | _ -> assert false 
+	      let args = match find_conclusion params_env none t with
+		| App (f,args) -> args (* [kind_of_term f = Ind ip] *)
+		| _ -> [||]
 	      in 
-	      let l = extract_type_ind params_env t ctx db n in	      
+	      let dbmap = parse_ind_args si args in 
+	      let db = db_from_ind dbmap params_nb n in 
+	      let l = extract_type_ind params_env db dbmap t n in	      
 	      add_constructor cp (Cml (l,s,params_nb))
 	    done
     done
@@ -528,7 +525,8 @@ and apply_constructor env cp args =
 	  let mla2 = extract_eta_args n2 s2 in 
 	  anonym_or_dummy_lams (head (mla1 @ mla2)) s2
 	else (* [la < params_nb] *)
-	  dummy_lams (head (extract_eta_args ls s)) (ls + params_nb - la)
+	  let head' = head (extract_eta_args ls s) in 
+	  dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)
 	    
 (*S Extraction of a term. *)
 
@@ -671,8 +669,8 @@ let extract_constant sp r =
 	   | (Logic, Arity) -> DdummyType r
 	   | (Info, Arity) -> 
 	       let s,vl = type_sign_vl env typ in 
-	       let ctx = ctx_from_sign s in 
-	       let t = extract_type_arity env body ctx (List.length s)
+	       let db = db_from_sign s in 
+	       let t = extract_type_arity env db body (List.length s)
 	       in Dtype (r, vl, t)
 	   | (Logic, _) -> Dterm (r, MLdummy')
 	   | (Info, _) -> 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 877961018..286747c6f 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -70,22 +70,16 @@ let empty_env () = [], P.globals()
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
-    | Tapp l ->
-	(match collapse_type_app l with
-	   | [] -> assert false
-	   | [t] -> pp_rec par t
-	   | t::l -> 
-	       (open_par par ++
-		  pp_rec false t ++ spc () ++
-		  prlist_with_sep (fun () -> (spc ())) (pp_type true vl) l ++ 
-		  close_par par))
+    | Tglob (r,[]) -> pp_type_global r	
+    | Tglob (r,l) -> 
+	open_par par ++ pp_type_global r ++ spc () ++
+	prlist_with_sep spc (pp_type true vl) l ++ close_par par
     | Tarr (t1,t2) ->
-	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
-	   pp_rec false t2 ++ close_par par)
-    | Tglob r -> pp_type_global r
+	open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
+	pp_rec false t2 ++ close_par par
     | Tdummy -> str "()"
     | Tunknown -> str "()"
-  in 
+ in 
   hov 0 (pp_rec par t)
 
 (*s Pretty-printing of expressions. [par] indicates whether
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 9cdb10980..f87f11ed2 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -18,10 +18,9 @@ open Nametab
 (*s ML type expressions. *)
 
 type ml_type = 
-  | Tvar  of int
-  | Tapp  of ml_type list
   | Tarr  of ml_type * ml_type
-  | Tglob of global_reference
+  | Tvar  of int
+  | Tglob of global_reference * ml_type list 
   | Tdummy
   | Tunknown
       
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 5f954d776..544d8af6e 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -47,8 +47,7 @@ let sp_of_r r = match r with
     | _ -> assert false
 
 let rec type_mem_sp sp = function 
-  | Tglob r when (sp_of_r r)=sp -> true
-  | Tapp l -> List.exists (type_mem_sp sp) l
+  | Tglob (r,l) -> (sp_of_r r) = sp || List.exists (type_mem_sp sp) l
   | Tarr (a,b) -> (type_mem_sp sp a) || (type_mem_sp sp b)
   | _ -> false
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 553b2b68d..1e4033704 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -27,10 +27,6 @@ let cons_cofix = ref Refset.empty
 
 (*s Some utility functions. *)
 
-let rec collapse_type_app = function
-  | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2)
-  | l -> l
-
 let open_par = function true -> str "(" | false -> (mt ())
 
 let close_par = function true -> str ")" | false -> (mt ())
@@ -151,17 +147,12 @@ let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
 		 with _ -> (str "'a" ++ int i))
-    | Tapp l ->
-	(match collapse_type_app l with
-	   | [] -> assert false
-	   | [t] -> pp_rec par t
-	   | [t;u] -> pp_rec true u ++ spc () ++ pp_rec false t 
-	   | t::l -> (pp_tuple (pp_rec false) l ++ spc () ++  
-		      pp_rec false t))
+    | Tglob (r,[]) -> pp_type_global r
+    | Tglob (r,[u]) -> pp_rec true u ++ spc () ++ pp_type_global r
+    | Tglob (r,l) -> pp_tuple (pp_rec false) l ++ spc () ++ pp_type_global r
     | Tarr (t1,t2) ->
-	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
-	   pp_rec false t2 ++ close_par par)
-    | Tglob r -> pp_type_global r
+	open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
+	pp_rec false t2 ++ close_par par
     | Tdummy -> str "Obj.t"
     | Tunknown -> str "Obj.t"
   in 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 2a9170bb0..5304199b7 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -20,8 +20,6 @@ open Table
 val current_module : identifier option ref
 val cons_cofix : Refset.t ref
 
-val collapse_type_app : ml_type list -> ml_type list
-
 val open_par : bool -> std_ppcmds
 val close_par : bool -> std_ppcmds
 val pp_abst : identifier list -> std_ppcmds