aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-07-04 18:05:17 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-07-04 18:05:17 +0000
commit4bc80f8513d05f3aceb8d052b8dd59a6b00e3e60 (patch)
tree2c6ccbb12bbae750782ca8542a1fb62316040617
parent44160f6e16c9597b203e13e10f45dc346c96b1d3 (diff)
Set Extraction KeepSingleton: an option for not decapsulating singleton types
A informative inductive type with one constructor C and one informative arg to C is normally extracted as an identity, with C removed, see for example the "sig" type. When this new option is set, these singleton types are left untouch, providing extracted code which is closer to the initial Coq development. Feature requested by Wouter Swiestra. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14260 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--plugins/extraction/extraction.ml3
-rw-r--r--plugins/extraction/haskell.ml3
-rw-r--r--plugins/extraction/ocaml.ml3
-rw-r--r--plugins/extraction/table.ml4
-rw-r--r--plugins/extraction/table.mli4
5 files changed, 14 insertions, 3 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 455965af4..8433bf9d2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -402,7 +402,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
if Array.length p.ip_types <> 1 then raise (I Standard);
let typ = p.ip_types.(0) in
let l = List.filter (fun t -> not (isDummy (expand env t))) typ in
- if List.length l = 1 && not (type_mem_kn kn (List.hd l))
+ if not (keep_singleton ()) &&
+ List.length l = 1 && not (type_mem_kn kn (List.hd l))
then raise (I Singleton);
if l = [] then raise (I Standard);
if not mib.mind_record then raise (I Standard);
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index b51a957af..32ad45c93 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -83,7 +83,8 @@ let rec pp_type par vl t =
| Tmeta _ | Tvar' _ -> assert false
| Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
| Tglob (r,[]) -> pp_global Type r
- | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" ->
+ | Tglob (IndRef(kn,0),l)
+ when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
pp_type true vl (List.hd l)
| Tglob (r,l) ->
pp_par par
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 902e8bbb3..f34bcf1e9 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -126,7 +126,8 @@ let rec pp_type par vl t =
| Tglob (r,[a1;a2]) when is_infix r ->
pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
| Tglob (r,[]) -> pp_global Type r
- | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" ->
+ | Tglob (IndRef(kn,0),l)
+ when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
pp_tuple_light pp_rec l
| Tglob (r,l) ->
pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index aa312321b..c58672ca0 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -421,6 +421,10 @@ let auto_inline = my_bool_option "AutoInline" false
let type_expand = my_bool_option "TypeExpand" true
+(*s Extraction KeepSingleton *)
+
+let keep_singleton = my_bool_option "KeepSingleton" false
+
(*s Extraction Optimize *)
type opt_flag =
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index d656edfb7..7860dd6a5 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -103,6 +103,10 @@ val auto_inline : unit -> bool
val type_expand : unit -> bool
+(*s KeepSingleton parameter *)
+
+val keep_singleton : unit -> bool
+
(*s Optimize parameter *)
type opt_flag =