aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-02-17 14:32:50 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-01-11 09:49:32 +0100
commitd15d8cc0ce584a6d80d878faf84314c6712ccf69 (patch)
tree0042925526cfd801451cdbe5472f44cd2169a57c
parentb858f939f33dc4bc4c8e470ed62310ef15c59a99 (diff)
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
-rw-r--r--plugins/extraction/common.ml6
-rw-r--r--plugins/extraction/common.mli1
-rw-r--r--plugins/extraction/extraction.ml3
-rw-r--r--plugins/extraction/table.ml7
-rw-r--r--plugins/extraction/table.mli3
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