Extraction: minor tweaks to ease ongoing experiments about Lambda

 - Common.get_native_char instead of just a pp function of this char

 - Enrich the record projection table

5 files changed, 13 insertions, 7 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 135d3fc7c..4f78ffe97 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -642,11 +642,13 @@ let is_native_char = function
     MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l
   | _ -> false
 
-let pp_native_char c =
+let get_native_char c =
   let rec cumul = function
     | [] -> 0
     | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
     | _ -> assert false
   in
   let l = match c with MLcons(_,_,l) -> l | _ -> assert false in
-  str ("'"^Char.escaped (Char.chr (cumul l))^"'")
+  Char.chr (cumul l)
+
+let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'")
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 3058b91b6..ffb6029b2 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -79,4 +79,5 @@ val mk_ind : string -> string -> mutual_inductive
     the constants are directly turned into chars *)
 
 val is_native_char : ml_ast -> bool
+val get_native_char : ml_ast -> char
 val pp_native_char : ml_ast -> std_ppcmds
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cae7f0999..0be0a882b 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -484,7 +484,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  let n = nb_default_params env
             (Inductive.type_of_inductive env ((mib,mip0),u))
 	  in
-	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn in
+	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
+          in
 	  List.iter (Option.iter check_proj) (lookup_projections ip)
 	with Not_found -> ()
 	end;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2f64a24ab..f2d8c3bc0 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -189,11 +189,12 @@ let is_recursor = function
 
 (* NB: here, working modulo name equivalence is ok *)
 
-let projs = ref (Refmap.empty : int Refmap.t)
+let projs = ref (Refmap.empty : (inductive*int) Refmap.t)
 let init_projs () = projs := Refmap.empty
-let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
+let add_projection n kn ip = projs := Refmap.add (ConstRef kn) (ip,n) !projs
 let is_projection r = Refmap.mem r !projs
-let projection_arity r = Refmap.find r !projs
+let projection_arity r = snd (Refmap.find r !projs)
+let projection_info r = Refmap.find r !projs
 
 (*s Table of used axioms *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 823b710cf..e8513e4d4 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -85,9 +85,10 @@ val record_fields_of_type : ml_type -> global_reference option list
 val add_recursors : Environ.env -> mutual_inductive -> unit
 val is_recursor : global_reference -> bool
 
-val add_projection : int -> constant -> unit
+val add_projection : int -> constant -> inductive -> unit
 val is_projection : global_reference -> bool
 val projection_arity : global_reference -> int
+val projection_info : global_reference -> inductive * int (* arity *)
 
 val add_info_axiom : global_reference -> unit
 val remove_info_axiom : global_reference -> unit