diff options
| -rw-r--r-- | plugins/extraction/extraction.ml | 3 | ||||
| -rw-r--r-- | plugins/extraction/haskell.ml | 3 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 3 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 4 |
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 = |