debut de support des records caml

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

4 files changed, 94 insertions, 35 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 6917b1380c..e863e52c1c 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -20,14 +20,15 @@ open Environ
 open Reductionops
 open Inductive
 open Inductiveops
-open Instantiate
+(* open Instantiate *)
 open Miniml
 open Table
 open Mlutil
-open Closure
+(* open Closure *)
 open Summary
 open Libnames
 open Nametab
+open Recordops
 (*i*)
 
 (*S Extraction results. *)
@@ -350,7 +351,20 @@ and extract_mib kn =
   for i = 0 to mib.mind_ntypes - 1 do
     let mip = snd (Global.lookup_inductive (kn,i)) in 
     if mip.mind_sort <> (Prop Null) then 
-      add_inductive (kn,i) (type_sign_vl env mip.mind_nf_arity)
+      let ip = (kn,i) in 
+      let s,vl = type_sign_vl env mip.mind_nf_arity in 
+      add_inductive ip (s,vl); 
+      (* Record tables: *)
+      if not (is_singleton_inductive ip) then 
+	try 
+	  let l = (find_structure ip).s_PROJ in 
+	  assert (List.length s = List.length l); 
+	  let check (_,o) = match o with 
+	    | None -> raise Not_found 
+	    | Some kn -> ConstRef kn 
+	  in 
+	  add_record ip (List.map check (List.filter fst (List.combine s l)))
+	with Not_found  -> () 
   done;
   (* Second pass: we extract constructors *)
   for i = 0 to mib.mind_ntypes - 1 do
@@ -390,6 +404,24 @@ and extract_type_cons env db dbmap c i =
 	(extract_type env db 0 t []) :: l 
     | _ -> [] 
 
+(*s Looking for informative singleton case, i.e. an inductive with one 
+   constructor which has one informative argument. This dummy case will 
+   be simplified. *)
+
+and is_singleton_inductive ip = 
+  let (mib,mip) = Global.lookup_inductive ip in 
+  mib.mind_finite &&
+  (mib.mind_ntypes = 1) &&
+  (Array.length mip.mind_consnames = 1) && 
+  try 
+    let l = 
+      List.filter (type_neq mlt_env Tdummy) (fst (extract_constructor (ip,1)))
+    in List.length l = 1 && not (type_mem_kn (fst ip) (List.hd l))
+  with Not_found -> false
+          
+and is_singleton_constructor ((kn,i),_) = 
+  is_singleton_inductive (kn,i) 
+
 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
 
 and mlt_env r = match r with 
@@ -429,23 +461,6 @@ let record_constant_type kn =
     let schema = (type_maxvar mlt, mlt)
     in add_cst_type kn schema; schema
 
-(*s Looking for informative singleton case, i.e. an inductive with one 
-   constructor which has one informative argument. This dummy case will 
-   be simplified. *)
-
-let is_singleton_inductive ip = 
-  let (mib,mip) = Global.lookup_inductive ip in 
-  mib.mind_finite &&
-  (mib.mind_ntypes = 1) &&
-  (Array.length mip.mind_consnames = 1) && 
-  try 
-    let l = List.filter (type_neq Tdummy) (fst (extract_constructor (ip,1))) in
-    List.length l = 1 && not (type_mem_kn (fst ip) (List.hd l))
-  with Not_found -> false
-          
-let is_singleton_constructor ((kn,i),_) = 
-  is_singleton_inductive (kn,i) 
-
 (*S Extraction of a term. *)
 
 (* Precondition: [(c args)] is not a type scheme, and is informative. *)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 20a1d37769..72a34a65d7 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -20,6 +20,7 @@ open Table
 open Mlutil
 open Options
 open Nametab
+open Libnames
 
 let current_module = ref None
 
@@ -31,6 +32,8 @@ let open_par = function true -> str "(" | false -> (mt ())
 
 let close_par = function true -> str ")" | false -> (mt ())
 
+let pp_par par st = function true -> str "(" ++ st ++ str ")" | false -> mt ()
+
 let pp_tvar id = 
   let s = string_of_id id in 
   if String.length s < 2 || s.[1]<>'\'' 
@@ -181,14 +184,15 @@ let expr_needs_par = function
   | MLcase _ -> true
   | _        -> false 
 
+let pp_apply st par args = match args with
+  | [] -> st
+  | _  -> hov 2 (open_par par ++ st ++ spc () ++
+                 prlist_with_sep (fun () -> (spc ())) (fun s -> s) args ++
+                 close_par par) 
+
 let rec pp_expr par env args = 
   let par' = args <> [] || par in 
-  let apply st = match args with
-    | [] -> st
-    | _  -> hov 2 (open_par par ++ st ++ spc () ++
-                     prlist_with_sep (fun () -> (spc ())) (fun s -> s) args ++
-                     close_par par) 
-  in
+  let apply st = pp_apply st par args in 
   function
     | MLrel n -> 
 	let id = get_db_name n env in apply (pr_id id)
@@ -211,6 +215,9 @@ let rec pp_expr par env args =
 			++ pp_expr false env [] a1) ++ 
 		    spc () ++ str "in") ++ 
 	      spc () ++ hov 0 (pp_expr par2 env' [] a2) ++ close_par par'))
+    | MLglob r when is_proj r && args <> [] ->
+	let record = List.hd args in 
+	pp_apply (record ++ str "." ++ pp_type_global r) par (List.tl args)
     | MLglob r -> 
 	apply (pp_global r env )
     | MLcons (r,[]) ->
@@ -371,6 +378,13 @@ let pp_ind il =
    prlist_with_sep (fun () -> (fnl () ++ str "and ")) (pp_one_ind "") il
    ++ fnl ())
 
+let pp_record ip pl l = 
+  let pl = rename_tvars keywords pl in 
+  (str "type " ++ pp_parameters pl ++ pp_type_global (IndRef ip) ++ str " = { "++
+   hov 0 (prlist_with_sep (fun () -> (str ";" ++ spc ())) 
+	    (fun (r,t) -> pp_type_global r ++ str " : " ++ pp_type true pl t) l)
+   ++ str " }") 
+
 let pp_coind_preamble (pl,name,_) = 
   let pl = rename_tvars keywords pl in
   (pp_parameters pl ++ pp_type_global name ++ str " = " ++ 
@@ -387,15 +401,18 @@ let pp_coind il =
 
 let pp_decl = function
   | Dind ([], _) -> mt ()
-  | Dind (i, cofix) -> 
-      if cofix then begin
-	List.iter   
-	  (fun (_,_,l) -> 
-	     List.iter (fun (r,_) -> 
-			  cons_cofix := Refset.add r !cons_cofix)  l) i; 
-	hov 0 (pp_coind i)
-      end else 
-	hov 0 (pp_ind i)
+  | Dind (i, true) -> 
+      List.iter   
+	(fun (_,_,l) -> 
+	   List.iter (fun (r,_) -> 
+			cons_cofix := Refset.add r !cons_cofix)  l) i; 
+      hov 0 (pp_coind i)
+  | Dind ([vl, IndRef ip, [_,l]] as i, _) -> 
+      (try 
+	 let projs = find_proj ip in 
+	 hov 0 (pp_record ip vl (List.combine projs l))
+       with Not_found -> hov 0 (pp_ind i)) 
+  | Dind (i,_) -> hov 0 (pp_ind i)
   | Dtype (r, l, t) ->
       let l = rename_tvars keywords l in 
       hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index fbc088f202..a0dde32b7b 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -258,3 +258,26 @@ let extract_inductive r (s,l) =
   | _ -> 
       errorlabstrm "extract_inductive"
 	(Printer.pr_global g ++ spc () ++ str "is not an inductive type.")
+
+(*s Record Inductive tables. *)
+
+let record_type_table = 
+  ref (Gmap.empty : (inductive, global_reference list) Gmap.t)
+
+let record_proj_table = ref Refset.empty
+
+let add_record i l = 
+  record_type_table := Gmap.add i l !record_type_table; 
+  record_proj_table := List.fold_right Refset.add l !record_proj_table
+
+let find_proj i = Gmap.find i !record_type_table
+
+let is_proj r = Refset.mem r !record_proj_table 
+
+let _ = declare_summary "Extraction Record tables"
+	  { freeze_function = (fun () -> !record_type_table,!record_proj_table); 
+	    unfreeze_function = 
+	      (fun (x,y) -> record_type_table := x; record_proj_table := y); 
+	    init_function = (fun () -> ()); 
+	    survive_section = true }
+
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 4a21619ac2..d8b17f5d56 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -72,4 +72,8 @@ val extract_constant_inline : bool -> reference -> string -> unit
 
 val extract_inductive : reference -> string * string list -> unit
 
+val add_record : inductive -> global_reference list -> unit
 
+val find_proj : inductive -> global_reference list
+
+val is_proj : global_reference -> bool